Skip to main content

cranelift_isle/
parser.rs

1//! Parser for ISLE language.
2
3use crate::ast::*;
4
5use crate::error::{Error, Span};
6use crate::lexer::{Lexer, Pos, Token};
7
8type Result<T> = std::result::Result<T, Error>;
9
10/// Parse the top-level ISLE definitions and return their AST.
11pub fn parse(lexer: Lexer) -> Result<Vec<Def>> {
12    let mut parser = Parser::new(lexer);
13    let result = parser.parse_defs()?;
14    Ok(result)
15}
16
17/// Parse without positional information. Provided mainly to support testing, to
18/// enable equality testing on structure alone.
19pub fn parse_without_pos(lexer: Lexer) -> Result<Vec<Def>> {
20    let mut parser = Parser::new_without_pos_tracking(lexer);
21    parser.parse_defs()
22}
23
24/// The ISLE parser.
25///
26/// Takes in a lexer and creates an AST.
27#[derive(Clone, Debug)]
28pub struct Parser<'a> {
29    lexer: Lexer<'a>,
30    disable_pos: bool,
31}
32
33/// Used during parsing a `(rule ...)` to encapsulate some form that
34/// comes after the top-level pattern: an if-let clause, or the final
35/// top-level expr.
36enum IfLetOrExpr {
37    IfLet(IfLet),
38    Expr(Expr),
39}
40
41impl<'a> Parser<'a> {
42    /// Construct a new parser from the given lexer.
43    pub fn new(lexer: Lexer<'a>) -> Parser<'a> {
44        Parser {
45            lexer,
46            disable_pos: false,
47        }
48    }
49
50    fn new_without_pos_tracking(lexer: Lexer<'a>) -> Parser<'a> {
51        Parser {
52            lexer,
53            disable_pos: true,
54        }
55    }
56
57    fn error(&self, pos: Pos, msg: String) -> Error {
58        Error::ParseError {
59            msg,
60            span: Span::new_single(pos),
61        }
62    }
63
64    fn expect<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Token> {
65        if let Some(&(pos, ref peek)) = self.lexer.peek() {
66            if !f(peek) {
67                return Err(self.error(pos, format!("Unexpected token {peek:?}")));
68            }
69            Ok(self.lexer.next()?.unwrap().1)
70        } else {
71            Err(self.error(self.lexer.pos(), "Unexpected EOF".to_string()))
72        }
73    }
74
75    fn eat<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Option<Token>> {
76        if let Some(&(_pos, ref peek)) = self.lexer.peek() {
77            if !f(peek) {
78                return Ok(None);
79            }
80            Ok(Some(self.lexer.next()?.unwrap().1))
81        } else {
82            Ok(None) // EOF
83        }
84    }
85
86    fn is<F: Fn(&Token) -> bool>(&self, f: F) -> bool {
87        if let Some((_, peek)) = self.lexer.peek() {
88            f(peek)
89        } else {
90            false
91        }
92    }
93
94    fn pos(&self) -> Pos {
95        if !self.disable_pos {
96            self.lexer
97                .peek()
98                .map_or_else(|| self.lexer.pos(), |(pos, _)| *pos)
99        } else {
100            Pos::default()
101        }
102    }
103
104    fn is_lparen(&self) -> bool {
105        self.is(|tok| *tok == Token::LParen)
106    }
107    fn is_rparen(&self) -> bool {
108        self.is(|tok| *tok == Token::RParen)
109    }
110    fn is_at(&self) -> bool {
111        self.is(|tok| *tok == Token::At)
112    }
113    fn is_sym(&self) -> bool {
114        self.is(Token::is_sym)
115    }
116    fn is_int(&self) -> bool {
117        self.is(Token::is_int)
118    }
119
120    fn is_const(&self) -> bool {
121        self.is(|tok| match tok {
122            Token::Symbol(tok_s) if tok_s.starts_with('$') => true,
123            _ => false,
124        })
125    }
126
127    fn is_spec_bit_vector(&self) -> bool {
128        self.is(|tok| match tok {
129            Token::Symbol(tok_s) if tok_s.starts_with("#x") || tok_s.starts_with("#b") => true,
130            _ => false,
131        })
132    }
133
134    fn is_spec_bool(&self) -> bool {
135        self.is(|tok| match tok {
136            Token::Symbol(tok_s) if tok_s == "true" || tok_s == "false" => true,
137            _ => false,
138        })
139    }
140
141    fn expect_lparen(&mut self) -> Result<()> {
142        self.expect(|tok| *tok == Token::LParen).map(|_| ())
143    }
144    fn expect_rparen(&mut self) -> Result<()> {
145        self.expect(|tok| *tok == Token::RParen).map(|_| ())
146    }
147    fn expect_at(&mut self) -> Result<()> {
148        self.expect(|tok| *tok == Token::At).map(|_| ())
149    }
150
151    fn expect_symbol(&mut self) -> Result<String> {
152        match self.expect(Token::is_sym)? {
153            Token::Symbol(s) => Ok(s),
154            _ => unreachable!(),
155        }
156    }
157
158    fn eat_sym_str(&mut self, s: &str) -> Result<bool> {
159        self.eat(|tok| match tok {
160            Token::Symbol(tok_s) if tok_s == s => true,
161            _ => false,
162        })
163        .map(|token| token.is_some())
164    }
165
166    fn expect_int(&mut self) -> Result<i128> {
167        match self.expect(Token::is_int)? {
168            Token::Int(i) => Ok(i),
169            _ => unreachable!(),
170        }
171    }
172
173    fn parse_defs(&mut self) -> Result<Vec<Def>> {
174        let mut defs = vec![];
175        while !self.lexer.eof() {
176            defs.push(self.parse_def()?);
177        }
178        Ok(defs)
179    }
180
181    fn parse_def(&mut self) -> Result<Def> {
182        self.expect_lparen()?;
183        let pos = self.pos();
184        let def = match &self.expect_symbol()?[..] {
185            "pragma" => Def::Pragma(self.parse_pragma()?),
186            "type" => Def::Type(self.parse_type()?),
187            "decl" => Def::Decl(self.parse_decl()?),
188            "attr" => Def::Attr(self.parse_attr()?),
189            "spec" => Def::Spec(self.parse_spec()?),
190            "macro" => Def::SpecMacro(self.parse_spec_macro()?),
191            "state" => Def::State(self.parse_state()?),
192            "model" => Def::Model(self.parse_model()?),
193            "form" => Def::Form(self.parse_form()?),
194            "instantiate" => Def::Instantiation(self.parse_instantiation()?),
195            "rule" => Def::Rule(self.parse_rule()?),
196            "extractor" => Def::Extractor(self.parse_etor()?),
197            "extern" => Def::Extern(self.parse_extern()?),
198            "convert" => Def::Converter(self.parse_converter()?),
199            s => {
200                return Err(self.error(pos, format!("Unexpected identifier: {s}")));
201            }
202        };
203        self.expect_rparen()?;
204        Ok(def)
205    }
206
207    fn str_to_ident(&self, pos: Pos, s: &str) -> Result<Ident> {
208        let first = s
209            .chars()
210            .next()
211            .ok_or_else(|| self.error(pos, "empty symbol".into()))?;
212        if !first.is_alphabetic() && first != '_' && first != '$' {
213            return Err(self.error(
214                pos,
215                format!("Identifier '{s}' does not start with letter or _ or $"),
216            ));
217        }
218        if s.chars()
219            .skip(1)
220            .any(|c| !c.is_alphanumeric() && c != '_' && c != '.' && c != '$')
221        {
222            return Err(self.error(
223                pos,
224                format!("Identifier '{s}' contains invalid character (not a-z, A-Z, 0-9, _, ., $)"),
225            ));
226        }
227        Ok(Ident(s.to_string(), pos))
228    }
229
230    fn parse_ident(&mut self) -> Result<Ident> {
231        let pos = self.pos();
232        let s = self.expect_symbol()?;
233        self.str_to_ident(pos, &s)
234    }
235
236    fn parse_const(&mut self) -> Result<Ident> {
237        let pos = self.pos();
238        let ident = self.parse_ident()?;
239        if let Some(s) = ident.0.strip_prefix('$') {
240            Ok(Ident(s.to_string(), ident.1))
241        } else {
242            Err(self.error(
243                pos,
244                "Not a constant identifier; must start with a '$'".to_string(),
245            ))
246        }
247    }
248
249    fn parse_pragma(&mut self) -> Result<Pragma> {
250        let ident = self.parse_ident()?;
251        // currently, no pragmas are defined, but the infrastructure is useful to keep around
252        let pragma = ident.0.as_str();
253        Err(self.error(ident.1, format!("Unknown pragma '{pragma}'")))
254    }
255
256    fn parse_type(&mut self) -> Result<Type> {
257        let pos = self.pos();
258        let name = self.parse_ident()?;
259
260        let mut is_extern = false;
261        let mut is_nodebug = false;
262
263        while self.lexer.peek().map_or(false, |(_pos, tok)| tok.is_sym()) {
264            let sym = self.expect_symbol()?;
265            if sym == "extern" {
266                is_extern = true;
267            } else if sym == "nodebug" {
268                is_nodebug = true;
269            } else {
270                return Err(self.error(
271                    self.pos(),
272                    format!("unknown type declaration modifier: {sym}"),
273                ));
274            }
275        }
276
277        let ty = self.parse_typevalue()?;
278        Ok(Type {
279            name,
280            is_extern,
281            is_nodebug,
282            ty,
283            pos,
284        })
285    }
286
287    fn parse_typevalue(&mut self) -> Result<TypeValue> {
288        let pos = self.pos();
289        self.expect_lparen()?;
290        if self.eat_sym_str("primitive")? {
291            let primitive_ident = self.parse_ident()?;
292            self.expect_rparen()?;
293            Ok(TypeValue::Primitive(primitive_ident, pos))
294        } else if self.eat_sym_str("enum")? {
295            let mut variants = vec![];
296            while !self.is_rparen() {
297                let variant = self.parse_type_variant()?;
298                variants.push(variant);
299            }
300            self.expect_rparen()?;
301            Ok(TypeValue::Enum(variants, pos))
302        } else if self.eat_sym_str("struct")? {
303            let fields = self.parse_fields()?;
304            self.expect_rparen()?;
305            Ok(TypeValue::Struct(fields, pos))
306        } else {
307            Err(self.error(pos, "Unknown type definition".to_string()))
308        }
309    }
310
311    fn parse_type_variant(&mut self) -> Result<Variant> {
312        if self.is_sym() {
313            let pos = self.pos();
314            let name = self.parse_ident()?;
315            Ok(Variant {
316                name,
317                fields: Fields::Unit,
318                pos,
319            })
320        } else {
321            let pos = self.pos();
322            self.expect_lparen()?;
323            let name = self.parse_ident()?;
324            let fields = self.parse_fields()?;
325            self.expect_rparen()?;
326            Ok(Variant { name, fields, pos })
327        }
328    }
329
330    fn parse_fields(&mut self) -> Result<Fields> {
331        if self.is_rparen() {
332            Ok(Fields::Unit)
333        } else if self.is_lparen() {
334            Ok(Fields::Struct(self.parse_struct_fields()?))
335        } else {
336            Ok(Fields::Tuple(self.parse_tuple_fields()?))
337        }
338    }
339
340    fn parse_struct_fields(&mut self) -> Result<StructFields> {
341        let pos = self.pos();
342        let mut fields = vec![];
343        while !self.is_rparen() {
344            fields.push(self.parse_struct_field()?);
345        }
346        Ok(StructFields { fields, pos })
347    }
348
349    fn parse_struct_field(&mut self) -> Result<StructField> {
350        let pos = self.pos();
351        self.expect_lparen()?;
352        let name = self.parse_ident()?;
353        let ty = self.parse_ident()?;
354        self.expect_rparen()?;
355        Ok(StructField { name, ty, pos })
356    }
357
358    fn parse_tuple_fields(&mut self) -> Result<TupleFields> {
359        let pos = self.pos();
360        let mut fields = vec![];
361        while !self.is_rparen() {
362            fields.push(self.parse_tuple_field(fields.len())?);
363        }
364        Ok(TupleFields { fields, pos })
365    }
366
367    fn parse_tuple_field(&mut self, index: usize) -> Result<TupleField> {
368        let pos = self.pos();
369        let ty = self.parse_ident()?;
370        Ok(TupleField { index, ty, pos })
371    }
372
373    fn parse_decl(&mut self) -> Result<Decl> {
374        let pos = self.pos();
375
376        let pure = self.eat_sym_str("pure")?;
377        let multi = self.eat_sym_str("multi")?;
378        let partial = self.eat_sym_str("partial")?;
379        let rec = self.eat_sym_str("rec")?;
380
381        let term = self.parse_ident()?;
382
383        self.expect_lparen()?;
384        let mut arg_tys = vec![];
385        while !self.is_rparen() {
386            arg_tys.push(self.parse_ident()?);
387        }
388        self.expect_rparen()?;
389
390        let ret_ty = self.parse_ident()?;
391
392        Ok(Decl {
393            term,
394            arg_tys,
395            ret_ty,
396            pure,
397            multi,
398            partial,
399            rec,
400            pos,
401        })
402    }
403
404    fn parse_attr(&mut self) -> Result<Attr> {
405        let pos = self.pos();
406        let rule = self.eat_sym_str("rule")?;
407        let name = self.parse_ident()?;
408        let target = if rule {
409            AttrTarget::Rule(name)
410        } else {
411            AttrTarget::Term(name)
412        };
413        let mut kinds = Vec::new();
414        while !self.is_rparen() {
415            kinds.push(self.parse_attr_kind()?);
416        }
417        Ok(Attr { target, kinds, pos })
418    }
419
420    fn parse_attr_kind(&mut self) -> Result<AttrKind> {
421        self.expect_lparen()?;
422        let pos = self.pos();
423        let kind = match &self.expect_symbol()?[..] {
424            "veri" => self.parse_attr_kind_veri()?,
425            "tag" => AttrKind::Tag(self.parse_ident()?),
426            x => return Err(self.error(pos, format!("Not a valid attribute: {x}"))),
427        };
428        self.expect_rparen()?;
429        Ok(kind)
430    }
431
432    fn parse_attr_kind_veri(&mut self) -> Result<AttrKind> {
433        let pos = self.pos();
434        match &self.expect_symbol()?[..] {
435            "chain" => Ok(AttrKind::Chain),
436            "priority" => Ok(AttrKind::Priority),
437            x => Err(self.error(pos, format!("Not a valid verification attribute: {x}"))),
438        }
439    }
440
441    fn parse_spec(&mut self) -> Result<Spec> {
442        let pos = self.pos();
443        self.expect_lparen()?; // term with args: (spec (<term> <args>) (provide ...) ...)
444        let term = self.parse_ident()?;
445        let mut args = vec![];
446        while !self.is_rparen() {
447            args.push(self.parse_ident()?);
448        }
449        self.expect_rparen()?; // end term with args
450
451        let mut provides = Vec::new();
452        let mut requires = Vec::new();
453        let mut matches = Vec::new();
454        let mut modifies = Vec::new();
455        while self.is_lparen() {
456            self.expect_lparen()?;
457            match &self.expect_symbol()?[..] {
458                "provide" => {
459                    while !self.is_rparen() {
460                        provides.push(self.parse_spec_expr()?);
461                    }
462                }
463                "require" => {
464                    while !self.is_rparen() {
465                        requires.push(self.parse_spec_expr()?);
466                    }
467                }
468                "match" => {
469                    while !self.is_rparen() {
470                        matches.push(self.parse_spec_expr()?);
471                    }
472                }
473                "modifies" => {
474                    let state = self.parse_ident()?;
475                    let cond = if self.is_sym() {
476                        Some(self.parse_ident().map_err(|err| {
477                            self.error(pos, format!("Invalid modifies condition: {err:?}"))
478                        })?)
479                    } else {
480                        None
481                    };
482                    modifies.push(Modifies { state, cond });
483                }
484                field => {
485                    return Err(self.error(
486                        pos,
487                        format!("Invalid spec: unexpected field {field}. Expect (provide ...), (require ...) or (match ...)"),
488                    ));
489                }
490            }
491            self.expect_rparen()?;
492        }
493
494        Ok(Spec {
495            term,
496            args,
497            provides,
498            requires,
499            matches,
500            modifies,
501            pos,
502        })
503    }
504
505    fn parse_spec_macro(&mut self) -> Result<SpecMacro> {
506        let pos = self.pos();
507
508        // Signature.
509        self.expect_lparen()?;
510        let name = self.parse_ident()?;
511        let mut params = vec![];
512        while !self.is_rparen() {
513            params.push(self.parse_ident()?);
514        }
515        self.expect_rparen()?;
516
517        // Body.
518        let body = self.parse_spec_expr()?;
519
520        Ok(SpecMacro {
521            name,
522            params,
523            body,
524            pos,
525        })
526    }
527
528    fn parse_spec_expr(&mut self) -> Result<SpecExpr> {
529        let pos = self.pos();
530        if self.is_spec_bit_vector() {
531            let (val, width) = self.parse_spec_bit_vector()?;
532            Ok(SpecExpr::ConstBitVec { val, width, pos })
533        } else if self.is_int() {
534            Ok(SpecExpr::ConstInt {
535                val: self.expect_int()?,
536                pos,
537            })
538        } else if self.is_spec_bool() {
539            let val = self.parse_spec_bool()?;
540            Ok(SpecExpr::ConstBool { val, pos })
541        } else if self.is_sym() {
542            let var = self.parse_ident()?;
543            Ok(SpecExpr::Var { var, pos })
544        } else if self.is_lparen() {
545            self.expect_lparen()?;
546            if self.eat_sym_str("switch")? {
547                let mut args = vec![];
548                args.push(self.parse_spec_expr()?);
549                while !(self.is_rparen()) {
550                    self.expect_lparen()?;
551                    let pos = self.pos();
552                    let l = Box::new(self.parse_spec_expr()?);
553                    let r = Box::new(self.parse_spec_expr()?);
554                    self.expect_rparen()?;
555                    args.push(SpecExpr::Pair { l, r, pos });
556                }
557                self.expect_rparen()?;
558                Ok(SpecExpr::Op {
559                    op: SpecOp::Switch,
560                    args,
561                    pos,
562                })
563            } else if self.eat_sym_str("let")? {
564                let mut defs = Vec::new();
565                self.expect_lparen()?;
566                while !(self.is_rparen()) {
567                    self.expect_lparen()?;
568                    let ident = self.parse_ident()?;
569                    let x = self.parse_spec_expr()?;
570                    self.expect_rparen()?;
571                    defs.push((ident, x));
572                }
573                self.expect_rparen()?;
574                let body = Box::new(self.parse_spec_expr()?);
575                self.expect_rparen()?;
576                Ok(SpecExpr::Let { defs, body, pos })
577            } else if self.eat_sym_str("with")? {
578                let mut decls = Vec::new();
579                self.expect_lparen()?;
580                while !(self.is_rparen()) {
581                    let ident = self.parse_ident()?;
582                    decls.push(ident);
583                }
584                self.expect_rparen()?;
585                let body = Box::new(self.parse_spec_expr()?);
586                self.expect_rparen()?;
587                Ok(SpecExpr::With { decls, body, pos })
588            } else if self.eat_sym_str("match")? {
589                let x = Box::new(self.parse_spec_expr()?);
590                let mut arms = Vec::new();
591                while !(self.is_rparen()) {
592                    let arm = self.parse_arm()?;
593                    arms.push(arm);
594                }
595                self.expect_rparen()?;
596                Ok(SpecExpr::Match { x, arms, pos })
597            } else if self.eat_sym_str("struct")? {
598                let mut fields = Vec::new();
599                while !(self.is_rparen()) {
600                    let field = self.parse_field_init()?;
601                    fields.push(field);
602                }
603                self.expect_rparen()?;
604                Ok(SpecExpr::Struct { fields, pos })
605            } else if self.eat_sym_str("macro")? {
606                self.expect_lparen()?;
607                let mut params = vec![];
608                while !self.is_rparen() {
609                    params.push(self.parse_ident()?);
610                }
611                self.expect_rparen()?;
612                let body = Box::new(self.parse_spec_expr()?);
613                self.expect_rparen()?;
614                Ok(SpecExpr::Macro { params, body, pos })
615            } else if self.eat_sym_str("as")? {
616                let x = Box::new(self.parse_spec_expr()?);
617                let ty = self.parse_model_type()?;
618                self.expect_rparen()?;
619                Ok(SpecExpr::As { x, ty, pos })
620            } else if self.is_sym() && !self.is_spec_bit_vector() {
621                let sym_pos = self.pos();
622                let sym = self.expect_symbol()?;
623                if let Some(variant) = sym.strip_suffix('?') {
624                    let variant = self.str_to_ident(sym_pos, variant)?;
625                    let x = Box::new(self.parse_spec_expr()?);
626                    self.expect_rparen()?;
627                    Ok(SpecExpr::Discriminator { variant, x, pos })
628                } else if let Some(name) = sym.strip_suffix('!') {
629                    let name = self.str_to_ident(sym_pos, name)?;
630                    let mut args: Vec<SpecExpr> = vec![];
631                    while !self.is_rparen() {
632                        args.push(self.parse_spec_expr()?);
633                    }
634                    self.expect_rparen()?;
635                    Ok(SpecExpr::Expand { name, args, pos })
636                } else if let Ok(op) = self.parse_spec_op(sym.as_str()) {
637                    let mut args: Vec<SpecExpr> = vec![];
638                    while !self.is_rparen() {
639                        args.push(self.parse_spec_expr()?);
640                    }
641                    self.expect_rparen()?;
642                    Ok(SpecExpr::Op { op, args, pos })
643                } else if let Some(field) = sym.strip_prefix(':') {
644                    let field = self.str_to_ident(sym_pos, field)?;
645                    let x = Box::new(self.parse_spec_expr()?);
646                    self.expect_rparen()?;
647                    Ok(SpecExpr::Field { field, x, pos })
648                } else if let Some((name, variant)) = sym.split_once('.') {
649                    let name = self.str_to_ident(pos, &name)?;
650                    let variant = self.str_to_ident(pos, &variant)?;
651                    let mut args: Vec<SpecExpr> = vec![];
652                    while !self.is_rparen() {
653                        args.push(self.parse_spec_expr()?);
654                    }
655                    self.expect_rparen()?;
656                    Ok(SpecExpr::Enum {
657                        name,
658                        variant,
659                        args,
660                        pos,
661                    })
662                } else {
663                    Err(self.error(pos, "Unexpected spec expression".into()))
664                }
665            } else {
666                Err(self.error(pos, "Unexpected spec expression".into()))
667            }
668        } else {
669            Err(self.error(pos, "Unexpected spec expression".into()))
670        }
671    }
672
673    fn parse_spec_op(&mut self, s: &str) -> Result<SpecOp> {
674        let pos = self.pos();
675        match s {
676            "=" => Ok(SpecOp::Eq),
677            "and" => Ok(SpecOp::And),
678            "not" => Ok(SpecOp::Not),
679            "=>" => Ok(SpecOp::Imp),
680            "or" => Ok(SpecOp::Or),
681            "+" => Ok(SpecOp::Add),
682            "-" => Ok(SpecOp::Sub),
683            "*" => Ok(SpecOp::Mul),
684            "<=" => Ok(SpecOp::Lte),
685            "<" => Ok(SpecOp::Lt),
686            ">=" => Ok(SpecOp::Gte),
687            ">" => Ok(SpecOp::Gt),
688            "bvnot" => Ok(SpecOp::BVNot),
689            "bvand" => Ok(SpecOp::BVAnd),
690            "bvor" => Ok(SpecOp::BVOr),
691            "bvxor" => Ok(SpecOp::BVXor),
692            "bvneg" => Ok(SpecOp::BVNeg),
693            "bvadd" => Ok(SpecOp::BVAdd),
694            "bvsub" => Ok(SpecOp::BVSub),
695            "bvmul" => Ok(SpecOp::BVMul),
696            "bvudiv" => Ok(SpecOp::BVUdiv),
697            "bvurem" => Ok(SpecOp::BVUrem),
698            "bvsdiv" => Ok(SpecOp::BVSdiv),
699            "bvsrem" => Ok(SpecOp::BVSrem),
700            "bvshl" => Ok(SpecOp::BVShl),
701            "bvlshr" => Ok(SpecOp::BVLshr),
702            "bvashr" => Ok(SpecOp::BVAshr),
703            "bvsaddo" => Ok(SpecOp::BVSaddo),
704            "bvule" => Ok(SpecOp::BVUle),
705            "bvult" => Ok(SpecOp::BVUlt),
706            "bvugt" => Ok(SpecOp::BVUgt),
707            "bvuge" => Ok(SpecOp::BVUge),
708            "bvslt" => Ok(SpecOp::BVSlt),
709            "bvsle" => Ok(SpecOp::BVSle),
710            "bvsgt" => Ok(SpecOp::BVSgt),
711            "bvsge" => Ok(SpecOp::BVSge),
712            "rotr" => Ok(SpecOp::Rotr),
713            "rotl" => Ok(SpecOp::Rotl),
714            "extract" => Ok(SpecOp::Extract),
715            "zero_ext" => Ok(SpecOp::ZeroExt),
716            "sign_ext" => Ok(SpecOp::SignExt),
717            "concat" => Ok(SpecOp::Concat),
718            "replicate" => Ok(SpecOp::Replicate),
719            "conv_to" => Ok(SpecOp::ConvTo),
720            "int2bv" => Ok(SpecOp::Int2BV),
721            "bv2nat" => Ok(SpecOp::BV2Nat),
722            "widthof" => Ok(SpecOp::WidthOf),
723            "if" => Ok(SpecOp::If),
724            "switch" => Ok(SpecOp::Switch),
725            "popcnt" => Ok(SpecOp::Popcnt),
726            "rev" => Ok(SpecOp::Rev),
727            "cls" => Ok(SpecOp::Cls),
728            "clz" => Ok(SpecOp::Clz),
729            "to_fp" => Ok(SpecOp::ToFP),
730            "fp.to_ubv" => Ok(SpecOp::FPToUBV),
731            "fp.to_sbv" => Ok(SpecOp::FPToSBV),
732            "to_fp_unsigned" => Ok(SpecOp::ToFPUnsigned),
733            "to_fp_from_fp" => Ok(SpecOp::ToFPFromFP),
734            "fp.+oo" => Ok(SpecOp::FPPositiveInfinity),
735            "fp.-oo" => Ok(SpecOp::FPNegativeInfinity),
736            "fp.+zero" => Ok(SpecOp::FPPositiveZero),
737            "fp.-zero" => Ok(SpecOp::FPNegativeZero),
738            "fp.NaN" => Ok(SpecOp::FPNaN),
739            "fp.eq" => Ok(SpecOp::FPEq),
740            "fp.ne" => Ok(SpecOp::FPNe),
741            "fp.lt" => Ok(SpecOp::FPLt),
742            "fp.gt" => Ok(SpecOp::FPGt),
743            "fp.le" => Ok(SpecOp::FPLe),
744            "fp.ge" => Ok(SpecOp::FPGe),
745            "fp.add" => Ok(SpecOp::FPAdd),
746            "fp.sub" => Ok(SpecOp::FPSub),
747            "fp.mul" => Ok(SpecOp::FPMul),
748            "fp.div" => Ok(SpecOp::FPDiv),
749            "fp.min" => Ok(SpecOp::FPMin),
750            "fp.max" => Ok(SpecOp::FPMax),
751            "fp.neg" => Ok(SpecOp::FPNeg),
752            "fp.ceil" => Ok(SpecOp::FPCeil),
753            "fp.floor" => Ok(SpecOp::FPFloor),
754            "fp.sqrt" => Ok(SpecOp::FPSqrt),
755            "fp.trunc" => Ok(SpecOp::FPTrunc),
756            "fp.nearest" => Ok(SpecOp::FPNearest),
757            "fp.isZero" => Ok(SpecOp::FPIsZero),
758            "fp.isInfinite" => Ok(SpecOp::FPIsInfinite),
759            "fp.isNaN" => Ok(SpecOp::FPIsNaN),
760            "fp.isNegative" => Ok(SpecOp::FPIsNegative),
761            "fp.isPositive" => Ok(SpecOp::FPIsPositive),
762            x => Err(self.error(pos, format!("Not a valid spec operator: {x}"))),
763        }
764    }
765
766    fn parse_arm(&mut self) -> Result<Arm> {
767        self.expect_lparen()?;
768        let pos = self.pos();
769        self.expect_lparen()?;
770        let variant = self.parse_ident()?;
771        let mut args = Vec::new();
772        while !self.is_rparen() {
773            args.push(self.parse_ident()?);
774        }
775        self.expect_rparen()?;
776        let body = self.parse_spec_expr()?;
777        self.expect_rparen()?;
778        Ok(Arm {
779            variant,
780            args,
781            body,
782            pos,
783        })
784    }
785
786    fn parse_field_init(&mut self) -> Result<FieldInit> {
787        self.expect_lparen()?;
788        let pos = self.pos();
789        let name = self.parse_ident()?;
790        let value = Box::new(self.parse_spec_expr()?);
791        self.expect_rparen()?;
792        Ok(FieldInit { name, value, pos })
793    }
794
795    fn parse_spec_bit_vector(&mut self) -> Result<(u128, usize)> {
796        let pos = self.pos();
797        let s = self.expect_symbol()?;
798        if let Some(s) = s.strip_prefix("#b") {
799            match u128::from_str_radix(s, 2) {
800                Ok(i) => Ok((i, s.len())),
801                Err(_) => Err(self.error(pos, "Not a constant binary bit vector".to_string())),
802            }
803        } else if let Some(s) = s.strip_prefix("#x") {
804            match u128::from_str_radix(s, 16) {
805                Ok(i) => Ok((i, s.len() * 4)),
806                Err(_) => Err(self.error(pos, "Not a constant hex bit vector".to_string())),
807            }
808        } else {
809            Err(self.error(
810                pos,
811                "Not a constant bit vector; must start with `#x` (hex) or `#b` (binary)"
812                    .to_string(),
813            ))
814        }
815    }
816
817    fn parse_spec_bool(&mut self) -> Result<bool> {
818        let pos = self.pos();
819        let s = self.expect_symbol()?;
820        match s.as_str() {
821            "true" => Ok(true),
822            "false" => Ok(false),
823            x => Err(self.error(pos, format!("Not a valid spec boolean: {x}"))),
824        }
825    }
826
827    fn parse_model(&mut self) -> Result<Model> {
828        let pos = self.pos();
829        let name = self.parse_ident()?;
830        self.expect_lparen()?; // body
831        let val = if self.eat_sym_str("type")? {
832            let ty = self.parse_model_type()?;
833            ModelValue::TypeValue(ty)
834        } else if self.eat_sym_str("const")? {
835            let val = self.parse_spec_expr()?;
836            ModelValue::ConstValue(val)
837        } else {
838            return Err(self.error(pos, "Model must be a type or const".to_string()));
839        };
840
841        self.expect_rparen()?; // end body
842        Ok(Model { name, val })
843    }
844
845    fn parse_model_type(&mut self) -> Result<ModelType> {
846        let pos = self.pos();
847        if self.eat_sym_str("!")? {
848            Ok(ModelType::Unspecified)
849        } else if self.eat_sym_str("_")? {
850            Ok(ModelType::Auto)
851        } else if self.eat_sym_str("Bool")? {
852            Ok(ModelType::Bool)
853        } else if self.eat_sym_str("Int")? {
854            Ok(ModelType::Int)
855        } else if self.eat_sym_str("Unit")? {
856            Ok(ModelType::Unit)
857        } else if self.is_lparen() {
858            self.expect_lparen()?;
859            if self.eat_sym_str("bv")? {
860                let width = if self.is_rparen() {
861                    None
862                } else if self.is_int() {
863                    Some(usize::try_from(self.expect_int()?).map_err(|err| {
864                        self.error(pos, format!("Invalid BitVector width: {err}"))
865                    })?)
866                } else {
867                    return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()));
868                };
869                self.expect_rparen()?;
870                Ok(ModelType::BitVec(width))
871            } else if self.eat_sym_str("struct")? {
872                let mut fields = Vec::new();
873                while !self.is_rparen() {
874                    self.expect_lparen()?;
875                    let name = self.parse_ident()?;
876                    let ty = self.parse_model_type()?;
877                    self.expect_rparen()?;
878                    fields.push(ModelField { name, ty });
879                }
880                self.expect_rparen()?;
881                Ok(ModelType::Struct(fields))
882            } else if self.eat_sym_str("named")? {
883                let name = self.parse_ident()?;
884                self.expect_rparen()?;
885                Ok(ModelType::Named(name))
886            } else {
887                Err(self.error(
888                    pos,
889                    "Badly formed model: should be BitVector (bv ...) or Struct (struct ...)"
890                        .to_string(),
891                ))
892            }
893        } else {
894            Err(self.error(
895                pos,
896                "Model type be a Bool, Int, BitVector (bv ...) or Struct (struct ...)".to_string(),
897            ))
898        }
899    }
900
901    fn parse_state(&mut self) -> Result<State> {
902        let pos = self.pos();
903        let name = self.parse_ident()?;
904        let ty = self.parse_tagged_type("type")?;
905
906        self.expect_lparen()?;
907        if !self.eat_sym_str("default")? {
908            return Err(self.error(
909                self.pos(),
910                format!("Invalid default: expected (default <expr>)"),
911            ));
912        };
913        let default = self.parse_spec_expr()?;
914        self.expect_rparen()?;
915
916        Ok(State {
917            name,
918            ty,
919            default,
920            pos,
921        })
922    }
923
924    fn parse_form(&mut self) -> Result<Form> {
925        let pos = self.pos();
926        let name = self.parse_ident()?;
927        let signatures = self.parse_signatures()?;
928        Ok(Form {
929            name,
930            signatures,
931            pos,
932        })
933    }
934
935    fn parse_signatures(&mut self) -> Result<Vec<Signature>> {
936        let mut signatures = vec![];
937        while !self.is_rparen() {
938            signatures.push(self.parse_signature()?);
939        }
940        Ok(signatures)
941    }
942
943    fn parse_signature(&mut self) -> Result<Signature> {
944        self.expect_lparen()?;
945        let pos = self.pos();
946        let args = self.parse_tagged_types("args")?;
947        let ret = self.parse_tagged_type("ret")?;
948        self.expect_rparen()?;
949        Ok(Signature { args, ret, pos })
950    }
951
952    fn parse_tagged_types(&mut self, tag: &str) -> Result<Vec<ModelType>> {
953        self.expect_lparen()?;
954        let pos = self.pos();
955        if !self.eat_sym_str(tag)? {
956            return Err(self.error(pos, format!("Invalid {tag}: expected ({tag} <arg> ...)")));
957        };
958        let mut params = vec![];
959        while !self.is_rparen() {
960            params.push(self.parse_model_type()?);
961        }
962        self.expect_rparen()?;
963        Ok(params)
964    }
965
966    fn parse_tagged_type(&mut self, tag: &str) -> Result<ModelType> {
967        self.expect_lparen()?;
968        let pos = self.pos();
969        if !self.eat_sym_str(tag)? {
970            return Err(self.error(pos, format!("Invalid {tag}: expected ({tag} <arg>)")));
971        };
972        let ty = self.parse_model_type()?;
973        self.expect_rparen()?;
974        Ok(ty)
975    }
976
977    fn parse_instantiation(&mut self) -> Result<Instantiation> {
978        let pos = self.pos();
979        let term = self.parse_ident()?;
980        // Instantiation either has an explicit signatures list, which would
981        // open with a left paren. Or it has an identifier referencing a
982        // predefined set of signatures, optionally followed by `(tag <name>)`
983        // attributes gating when that set applies.
984        if self.is_lparen() {
985            let signatures = self.parse_signatures()?;
986            Ok(Instantiation {
987                term,
988                form: None,
989                signatures,
990                tags: vec![],
991                pos,
992            })
993        } else {
994            let form = self.parse_ident()?;
995            let mut tags = Vec::new();
996            while self.is_lparen() {
997                self.expect_lparen()?;
998                let attr_pos = self.pos();
999                match &self.expect_symbol()?[..] {
1000                    "tag" => tags.push(self.parse_ident()?),
1001                    x => {
1002                        return Err(
1003                            self.error(attr_pos, format!("Not a valid instantiate attribute: {x}"))
1004                        );
1005                    }
1006                }
1007                self.expect_rparen()?;
1008            }
1009            Ok(Instantiation {
1010                term,
1011                form: Some(form),
1012                signatures: vec![],
1013                tags,
1014                pos,
1015            })
1016        }
1017    }
1018
1019    fn parse_extern(&mut self) -> Result<Extern> {
1020        let pos = self.pos();
1021        if self.eat_sym_str("constructor")? {
1022            let term = self.parse_ident()?;
1023            let func = self.parse_ident()?;
1024            Ok(Extern::Constructor { term, func, pos })
1025        } else if self.eat_sym_str("extractor")? {
1026            let infallible = self.eat_sym_str("infallible")?;
1027
1028            let term = self.parse_ident()?;
1029            let func = self.parse_ident()?;
1030
1031            Ok(Extern::Extractor {
1032                term,
1033                func,
1034                pos,
1035                infallible,
1036            })
1037        } else if self.eat_sym_str("const")? {
1038            let pos = self.pos();
1039            let name = self.parse_const()?;
1040            let ty = self.parse_ident()?;
1041            Ok(Extern::Const { name, ty, pos })
1042        } else {
1043            Err(self.error(
1044                pos,
1045                "Invalid extern: must be (extern constructor ...), (extern extractor ...) or (extern const ...)"
1046                    .to_string(),
1047            ))
1048        }
1049    }
1050
1051    fn parse_etor(&mut self) -> Result<Extractor> {
1052        let pos = self.pos();
1053        self.expect_lparen()?;
1054        let term = self.parse_ident()?;
1055        let mut args = vec![];
1056        while !self.is_rparen() {
1057            args.push(self.parse_ident()?);
1058        }
1059        self.expect_rparen()?;
1060        let template = self.parse_pattern()?;
1061        Ok(Extractor {
1062            term,
1063            args,
1064            template,
1065            pos,
1066        })
1067    }
1068
1069    fn parse_rule(&mut self) -> Result<Rule> {
1070        let pos = self.pos();
1071        let name = if self.is_sym() {
1072            Some(
1073                self.parse_ident()
1074                    .map_err(|err| self.error(pos, format!("Invalid rule name: {err:?}")))?,
1075            )
1076        } else {
1077            None
1078        };
1079        let prio = if self.is_int() {
1080            Some(
1081                i64::try_from(self.expect_int()?)
1082                    .map_err(|err| self.error(pos, format!("Invalid rule priority: {err}")))?,
1083            )
1084        } else {
1085            None
1086        };
1087        let pattern = self.parse_pattern()?;
1088        let mut iflets = vec![];
1089        loop {
1090            match self.parse_iflet_or_expr()? {
1091                IfLetOrExpr::IfLet(iflet) => {
1092                    iflets.push(iflet);
1093                }
1094                IfLetOrExpr::Expr(expr) => {
1095                    return Ok(Rule {
1096                        pattern,
1097                        iflets,
1098                        expr,
1099                        pos,
1100                        prio,
1101                        name,
1102                    });
1103                }
1104            }
1105        }
1106    }
1107
1108    fn parse_pattern(&mut self) -> Result<Pattern> {
1109        let pos = self.pos();
1110        if self.is_int() {
1111            Ok(Pattern::ConstInt {
1112                val: self.expect_int()?,
1113                pos,
1114            })
1115        } else if self.is_const() {
1116            let val = self.parse_const()?;
1117            Ok(Pattern::ConstPrim { val, pos })
1118        } else if self.eat_sym_str("_")? {
1119            Ok(Pattern::Wildcard { pos })
1120        } else if self.eat_sym_str("true")? {
1121            Ok(Pattern::ConstBool { val: true, pos })
1122        } else if self.eat_sym_str("false")? {
1123            Ok(Pattern::ConstBool { val: false, pos })
1124        } else if self.is_sym() {
1125            let var = self.parse_ident()?;
1126            if self.is_at() {
1127                self.expect_at()?;
1128                let subpat = Box::new(self.parse_pattern()?);
1129                Ok(Pattern::BindPattern { var, subpat, pos })
1130            } else {
1131                Ok(Pattern::Var { var, pos })
1132            }
1133        } else if self.is_lparen() {
1134            self.expect_lparen()?;
1135            if self.eat_sym_str("and")? {
1136                let mut subpats = vec![];
1137                while !self.is_rparen() {
1138                    subpats.push(self.parse_pattern()?);
1139                }
1140                self.expect_rparen()?;
1141                Ok(Pattern::And { subpats, pos })
1142            } else {
1143                let sym = self.parse_ident()?;
1144                let mut args = vec![];
1145                while !self.is_rparen() {
1146                    args.push(self.parse_pattern()?);
1147                }
1148                self.expect_rparen()?;
1149                Ok(Pattern::Term { sym, args, pos })
1150            }
1151        } else {
1152            Err(self.error(pos, "Unexpected pattern".into()))
1153        }
1154    }
1155
1156    fn parse_iflet_or_expr(&mut self) -> Result<IfLetOrExpr> {
1157        let pos = self.pos();
1158        if self.is_lparen() {
1159            self.expect_lparen()?;
1160            let ret = if self.eat_sym_str("if-let")? {
1161                IfLetOrExpr::IfLet(self.parse_iflet()?)
1162            } else if self.eat_sym_str("if")? {
1163                // Shorthand form: `(if (x))` desugars to `(if-let _
1164                // (x))`.
1165                IfLetOrExpr::IfLet(self.parse_iflet_if()?)
1166            } else {
1167                IfLetOrExpr::Expr(self.parse_expr_inner_parens(pos)?)
1168            };
1169            self.expect_rparen()?;
1170            Ok(ret)
1171        } else {
1172            self.parse_expr().map(IfLetOrExpr::Expr)
1173        }
1174    }
1175
1176    fn parse_iflet(&mut self) -> Result<IfLet> {
1177        let pos = self.pos();
1178        let pattern = self.parse_pattern()?;
1179        let expr = self.parse_expr()?;
1180        Ok(IfLet { pattern, expr, pos })
1181    }
1182
1183    fn parse_iflet_if(&mut self) -> Result<IfLet> {
1184        let pos = self.pos();
1185        let expr = self.parse_expr()?;
1186        Ok(IfLet {
1187            pattern: Pattern::Wildcard { pos },
1188            expr,
1189            pos,
1190        })
1191    }
1192
1193    fn parse_expr(&mut self) -> Result<Expr> {
1194        let pos = self.pos();
1195        if self.is_lparen() {
1196            self.expect_lparen()?;
1197            let ret = self.parse_expr_inner_parens(pos)?;
1198            self.expect_rparen()?;
1199            Ok(ret)
1200        } else if self.is_const() {
1201            let val = self.parse_const()?;
1202            Ok(Expr::ConstPrim { val, pos })
1203        } else if self.eat_sym_str("true")? {
1204            Ok(Expr::ConstBool { val: true, pos })
1205        } else if self.eat_sym_str("false")? {
1206            Ok(Expr::ConstBool { val: false, pos })
1207        } else if self.is_sym() {
1208            let name = self.parse_ident()?;
1209            Ok(Expr::Var { name, pos })
1210        } else if self.is_int() {
1211            let val = self.expect_int()?;
1212            Ok(Expr::ConstInt { val, pos })
1213        } else {
1214            Err(self.error(pos, "Invalid expression".into()))
1215        }
1216    }
1217
1218    fn parse_expr_inner_parens(&mut self, pos: Pos) -> Result<Expr> {
1219        if self.eat_sym_str("let")? {
1220            self.expect_lparen()?;
1221            let mut defs = vec![];
1222            while !self.is_rparen() {
1223                let def = self.parse_letdef()?;
1224                defs.push(def);
1225            }
1226            self.expect_rparen()?;
1227            let body = Box::new(self.parse_expr()?);
1228            Ok(Expr::Let { defs, body, pos })
1229        } else {
1230            let sym = self.parse_ident()?;
1231            let mut args = vec![];
1232            while !self.is_rparen() {
1233                args.push(self.parse_expr()?);
1234            }
1235            Ok(Expr::Term { sym, args, pos })
1236        }
1237    }
1238
1239    fn parse_letdef(&mut self) -> Result<LetDef> {
1240        let pos = self.pos();
1241        self.expect_lparen()?;
1242        let var = self.parse_ident()?;
1243        let ty = self.parse_ident()?;
1244        let val = Box::new(self.parse_expr()?);
1245        self.expect_rparen()?;
1246        Ok(LetDef { var, ty, val, pos })
1247    }
1248
1249    fn parse_converter(&mut self) -> Result<Converter> {
1250        let pos = self.pos();
1251        let inner_ty = self.parse_ident()?;
1252        let outer_ty = self.parse_ident()?;
1253        let term = self.parse_ident()?;
1254        Ok(Converter {
1255            term,
1256            inner_ty,
1257            outer_ty,
1258            pos,
1259        })
1260    }
1261}