1 //! Parser for ISLE language.
2 
3 use crate::ast::*;
4 use crate::error::{Error, Span};
5 use crate::lexer::{Lexer, Pos, Token};
6 
7 type Result<T> = std::result::Result<T, Error>;
8 
9 /// Parse the top-level ISLE definitions and return their AST.
parse(lexer: Lexer) -> Result<Vec<Def>>10 pub fn parse(lexer: Lexer) -> Result<Vec<Def>> {
11     let parser = Parser::new(lexer);
12     parser.parse_defs()
13 }
14 
15 /// Parse without positional information. Provided mainly to support testing, to
16 /// enable equality testing on structure alone.
parse_without_pos(lexer: Lexer) -> Result<Vec<Def>>17 pub fn parse_without_pos(lexer: Lexer) -> Result<Vec<Def>> {
18     let parser = Parser::new_without_pos_tracking(lexer);
19     parser.parse_defs()
20 }
21 
22 /// The ISLE parser.
23 ///
24 /// Takes in a lexer and creates an AST.
25 #[derive(Clone, Debug)]
26 struct Parser<'a> {
27     lexer: Lexer<'a>,
28     disable_pos: bool,
29 }
30 
31 /// Used during parsing a `(rule ...)` to encapsulate some form that
32 /// comes after the top-level pattern: an if-let clause, or the final
33 /// top-level expr.
34 enum IfLetOrExpr {
35     IfLet(IfLet),
36     Expr(Expr),
37 }
38 
39 impl<'a> Parser<'a> {
40     /// Construct a new parser from the given lexer.
new(lexer: Lexer<'a>) -> Parser<'a>41     pub fn new(lexer: Lexer<'a>) -> Parser<'a> {
42         Parser {
43             lexer,
44             disable_pos: false,
45         }
46     }
47 
new_without_pos_tracking(lexer: Lexer<'a>) -> Parser<'a>48     fn new_without_pos_tracking(lexer: Lexer<'a>) -> Parser<'a> {
49         Parser {
50             lexer,
51             disable_pos: true,
52         }
53     }
54 
error(&self, pos: Pos, msg: String) -> Error55     fn error(&self, pos: Pos, msg: String) -> Error {
56         Error::ParseError {
57             msg,
58             span: Span::new_single(pos),
59         }
60     }
61 
expect<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Token>62     fn expect<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Token> {
63         if let Some(&(pos, ref peek)) = self.lexer.peek() {
64             if !f(peek) {
65                 return Err(self.error(pos, format!("Unexpected token {peek:?}")));
66             }
67             Ok(self.lexer.next()?.unwrap().1)
68         } else {
69             Err(self.error(self.lexer.pos(), "Unexpected EOF".to_string()))
70         }
71     }
72 
eat<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Option<Token>>73     fn eat<F: Fn(&Token) -> bool>(&mut self, f: F) -> Result<Option<Token>> {
74         if let Some(&(_pos, ref peek)) = self.lexer.peek() {
75             if !f(peek) {
76                 return Ok(None);
77             }
78             Ok(Some(self.lexer.next()?.unwrap().1))
79         } else {
80             Ok(None) // EOF
81         }
82     }
83 
is<F: Fn(&Token) -> bool>(&self, f: F) -> bool84     fn is<F: Fn(&Token) -> bool>(&self, f: F) -> bool {
85         if let Some((_, peek)) = self.lexer.peek() {
86             f(peek)
87         } else {
88             false
89         }
90     }
91 
pos(&self) -> Pos92     fn pos(&self) -> Pos {
93         if !self.disable_pos {
94             self.lexer
95                 .peek()
96                 .map_or_else(|| self.lexer.pos(), |(pos, _)| *pos)
97         } else {
98             Pos::default()
99         }
100     }
101 
is_lparen(&self) -> bool102     fn is_lparen(&self) -> bool {
103         self.is(|tok| *tok == Token::LParen)
104     }
is_rparen(&self) -> bool105     fn is_rparen(&self) -> bool {
106         self.is(|tok| *tok == Token::RParen)
107     }
is_at(&self) -> bool108     fn is_at(&self) -> bool {
109         self.is(|tok| *tok == Token::At)
110     }
is_sym(&self) -> bool111     fn is_sym(&self) -> bool {
112         self.is(Token::is_sym)
113     }
is_int(&self) -> bool114     fn is_int(&self) -> bool {
115         self.is(Token::is_int)
116     }
117 
is_const(&self) -> bool118     fn is_const(&self) -> bool {
119         self.is(|tok| match tok {
120             Token::Symbol(tok_s) if tok_s.starts_with('$') => true,
121             _ => false,
122         })
123     }
124 
is_spec_bit_vector(&self) -> bool125     fn is_spec_bit_vector(&self) -> bool {
126         self.is(|tok| match tok {
127             Token::Symbol(tok_s) if tok_s.starts_with("#x") || tok_s.starts_with("#b") => true,
128             _ => false,
129         })
130     }
131 
is_spec_bool(&self) -> bool132     fn is_spec_bool(&self) -> bool {
133         self.is(|tok| match tok {
134             Token::Symbol(tok_s) if tok_s == "true" || tok_s == "false" => true,
135             _ => false,
136         })
137     }
138 
expect_lparen(&mut self) -> Result<()>139     fn expect_lparen(&mut self) -> Result<()> {
140         self.expect(|tok| *tok == Token::LParen).map(|_| ())
141     }
expect_rparen(&mut self) -> Result<()>142     fn expect_rparen(&mut self) -> Result<()> {
143         self.expect(|tok| *tok == Token::RParen).map(|_| ())
144     }
expect_at(&mut self) -> Result<()>145     fn expect_at(&mut self) -> Result<()> {
146         self.expect(|tok| *tok == Token::At).map(|_| ())
147     }
148 
expect_symbol(&mut self) -> Result<String>149     fn expect_symbol(&mut self) -> Result<String> {
150         match self.expect(Token::is_sym)? {
151             Token::Symbol(s) => Ok(s),
152             _ => unreachable!(),
153         }
154     }
155 
eat_sym_str(&mut self, s: &str) -> Result<bool>156     fn eat_sym_str(&mut self, s: &str) -> Result<bool> {
157         self.eat(|tok| match tok {
158             Token::Symbol(tok_s) if tok_s == s => true,
159             _ => false,
160         })
161         .map(|token| token.is_some())
162     }
163 
expect_int(&mut self) -> Result<i128>164     fn expect_int(&mut self) -> Result<i128> {
165         match self.expect(Token::is_int)? {
166             Token::Int(i) => Ok(i),
167             _ => unreachable!(),
168         }
169     }
170 
parse_defs(mut self) -> Result<Vec<Def>>171     fn parse_defs(mut self) -> Result<Vec<Def>> {
172         let mut defs = vec![];
173         while !self.lexer.eof() {
174             defs.push(self.parse_def()?);
175         }
176         Ok(defs)
177     }
178 
parse_def(&mut self) -> Result<Def>179     fn parse_def(&mut self) -> Result<Def> {
180         self.expect_lparen()?;
181         let pos = self.pos();
182         let def = match &self.expect_symbol()?[..] {
183             "pragma" => Def::Pragma(self.parse_pragma()?),
184             "type" => Def::Type(self.parse_type()?),
185             "decl" => Def::Decl(self.parse_decl()?),
186             "spec" => Def::Spec(self.parse_spec()?),
187             "model" => Def::Model(self.parse_model()?),
188             "form" => Def::Form(self.parse_form()?),
189             "instantiate" => Def::Instantiation(self.parse_instantiation()?),
190             "rule" => Def::Rule(self.parse_rule()?),
191             "extractor" => Def::Extractor(self.parse_etor()?),
192             "extern" => Def::Extern(self.parse_extern()?),
193             "convert" => Def::Converter(self.parse_converter()?),
194             s => {
195                 return Err(self.error(pos, format!("Unexpected identifier: {s}")));
196             }
197         };
198         self.expect_rparen()?;
199         Ok(def)
200     }
201 
str_to_ident(&self, pos: Pos, s: &str) -> Result<Ident>202     fn str_to_ident(&self, pos: Pos, s: &str) -> Result<Ident> {
203         let first = s
204             .chars()
205             .next()
206             .ok_or_else(|| self.error(pos, "empty symbol".into()))?;
207         if !first.is_alphabetic() && first != '_' && first != '$' {
208             return Err(self.error(
209                 pos,
210                 format!("Identifier '{s}' does not start with letter or _ or $"),
211             ));
212         }
213         if s.chars()
214             .skip(1)
215             .any(|c| !c.is_alphanumeric() && c != '_' && c != '.' && c != '$')
216         {
217             return Err(self.error(
218                 pos,
219                 format!("Identifier '{s}' contains invalid character (not a-z, A-Z, 0-9, _, ., $)"),
220             ));
221         }
222         Ok(Ident(s.to_string(), pos))
223     }
224 
parse_ident(&mut self) -> Result<Ident>225     fn parse_ident(&mut self) -> Result<Ident> {
226         let pos = self.pos();
227         let s = self.expect_symbol()?;
228         self.str_to_ident(pos, &s)
229     }
230 
parse_const(&mut self) -> Result<Ident>231     fn parse_const(&mut self) -> Result<Ident> {
232         let pos = self.pos();
233         let ident = self.parse_ident()?;
234         if let Some(s) = ident.0.strip_prefix('$') {
235             Ok(Ident(s.to_string(), ident.1))
236         } else {
237             Err(self.error(
238                 pos,
239                 "Not a constant identifier; must start with a '$'".to_string(),
240             ))
241         }
242     }
243 
parse_pragma(&mut self) -> Result<Pragma>244     fn parse_pragma(&mut self) -> Result<Pragma> {
245         let ident = self.parse_ident()?;
246         // currently, no pragmas are defined, but the infrastructure is useful to keep around
247         let pragma = ident.0.as_str();
248         Err(self.error(ident.1, format!("Unknown pragma '{pragma}'")))
249     }
250 
parse_type(&mut self) -> Result<Type>251     fn parse_type(&mut self) -> Result<Type> {
252         let pos = self.pos();
253         let name = self.parse_ident()?;
254 
255         let mut is_extern = false;
256         let mut is_nodebug = false;
257 
258         while self.lexer.peek().map_or(false, |(_pos, tok)| tok.is_sym()) {
259             let sym = self.expect_symbol()?;
260             if sym == "extern" {
261                 is_extern = true;
262             } else if sym == "nodebug" {
263                 is_nodebug = true;
264             } else {
265                 return Err(self.error(
266                     self.pos(),
267                     format!("unknown type declaration modifier: {sym}"),
268                 ));
269             }
270         }
271 
272         let ty = self.parse_typevalue()?;
273         Ok(Type {
274             name,
275             is_extern,
276             is_nodebug,
277             ty,
278             pos,
279         })
280     }
281 
parse_typevalue(&mut self) -> Result<TypeValue>282     fn parse_typevalue(&mut self) -> Result<TypeValue> {
283         let pos = self.pos();
284         self.expect_lparen()?;
285         if self.eat_sym_str("primitive")? {
286             let primitive_ident = self.parse_ident()?;
287             self.expect_rparen()?;
288             Ok(TypeValue::Primitive(primitive_ident, pos))
289         } else if self.eat_sym_str("enum")? {
290             let mut variants = vec![];
291             while !self.is_rparen() {
292                 let variant = self.parse_type_variant()?;
293                 variants.push(variant);
294             }
295             self.expect_rparen()?;
296             Ok(TypeValue::Enum(variants, pos))
297         } else {
298             Err(self.error(pos, "Unknown type definition".to_string()))
299         }
300     }
301 
parse_type_variant(&mut self) -> Result<Variant>302     fn parse_type_variant(&mut self) -> Result<Variant> {
303         if self.is_sym() {
304             let pos = self.pos();
305             let name = self.parse_ident()?;
306             Ok(Variant {
307                 name,
308                 fields: vec![],
309                 pos,
310             })
311         } else {
312             let pos = self.pos();
313             self.expect_lparen()?;
314             let name = self.parse_ident()?;
315             let mut fields = vec![];
316             while !self.is_rparen() {
317                 fields.push(self.parse_type_field()?);
318             }
319             self.expect_rparen()?;
320             Ok(Variant { name, fields, pos })
321         }
322     }
323 
parse_type_field(&mut self) -> Result<Field>324     fn parse_type_field(&mut self) -> Result<Field> {
325         let pos = self.pos();
326         self.expect_lparen()?;
327         let name = self.parse_ident()?;
328         let ty = self.parse_ident()?;
329         self.expect_rparen()?;
330         Ok(Field { name, ty, pos })
331     }
332 
parse_decl(&mut self) -> Result<Decl>333     fn parse_decl(&mut self) -> Result<Decl> {
334         let pos = self.pos();
335 
336         let pure = self.eat_sym_str("pure")?;
337         let multi = self.eat_sym_str("multi")?;
338         let partial = self.eat_sym_str("partial")?;
339         let rec = self.eat_sym_str("rec")?;
340 
341         let term = self.parse_ident()?;
342 
343         self.expect_lparen()?;
344         let mut arg_tys = vec![];
345         while !self.is_rparen() {
346             arg_tys.push(self.parse_ident()?);
347         }
348         self.expect_rparen()?;
349 
350         let ret_ty = self.parse_ident()?;
351 
352         Ok(Decl {
353             term,
354             arg_tys,
355             ret_ty,
356             pure,
357             multi,
358             partial,
359             rec,
360             pos,
361         })
362     }
363 
parse_spec(&mut self) -> Result<Spec>364     fn parse_spec(&mut self) -> Result<Spec> {
365         let pos = self.pos();
366         self.expect_lparen()?; // term with args: (spec (<term> <args>) (provide ...) ...)
367         let term = self.parse_ident()?;
368         let mut args = vec![];
369         while !self.is_rparen() {
370             args.push(self.parse_ident()?);
371         }
372         self.expect_rparen()?; // end term with args
373 
374         self.expect_lparen()?; // provide
375         if !self.eat_sym_str("provide")? {
376             return Err(self.error(
377                 pos,
378                 "Invalid spec: expected (spec (<term> <args>) (provide ...) ...)".to_string(),
379             ));
380         };
381         let mut provides = vec![];
382         while !self.is_rparen() {
383             provides.push(self.parse_spec_expr()?);
384         }
385         self.expect_rparen()?; // end provide
386 
387         let requires = if self.is_lparen() {
388             self.expect_lparen()?;
389             if !self.eat_sym_str("require")? {
390                 return Err(self.error(
391                     pos,
392                     "Invalid spec: expected (spec (<term> <args>) (provide ...) (require ...))"
393                         .to_string(),
394                 ));
395             }
396             let mut require = vec![];
397             while !self.is_rparen() {
398                 require.push(self.parse_spec_expr()?);
399             }
400             self.expect_rparen()?; // end provide
401             require
402         } else {
403             vec![]
404         };
405 
406         Ok(Spec {
407             term,
408             args,
409             provides,
410             requires,
411         })
412     }
413 
parse_spec_expr(&mut self) -> Result<SpecExpr>414     fn parse_spec_expr(&mut self) -> Result<SpecExpr> {
415         let pos = self.pos();
416         if self.is_spec_bit_vector() {
417             let (val, width) = self.parse_spec_bit_vector()?;
418             return Ok(SpecExpr::ConstBitVec { val, width, pos });
419         } else if self.is_int() {
420             return Ok(SpecExpr::ConstInt {
421                 val: self.expect_int()?,
422                 pos,
423             });
424         } else if self.is_spec_bool() {
425             let val = self.parse_spec_bool()?;
426             return Ok(SpecExpr::ConstBool { val, pos });
427         } else if self.is_sym() {
428             let var = self.parse_ident()?;
429             return Ok(SpecExpr::Var { var, pos });
430         } else if self.is_lparen() {
431             self.expect_lparen()?;
432             if self.eat_sym_str("switch")? {
433                 let mut args = vec![];
434                 args.push(self.parse_spec_expr()?);
435                 while !(self.is_rparen()) {
436                     self.expect_lparen()?;
437                     let l = Box::new(self.parse_spec_expr()?);
438                     let r = Box::new(self.parse_spec_expr()?);
439                     self.expect_rparen()?;
440                     args.push(SpecExpr::Pair { l, r });
441                 }
442                 self.expect_rparen()?;
443                 return Ok(SpecExpr::Op {
444                     op: SpecOp::Switch,
445                     args,
446                     pos,
447                 });
448             }
449             if self.is_sym() && !self.is_spec_bit_vector() {
450                 let sym = self.expect_symbol()?;
451                 if let Ok(op) = self.parse_spec_op(sym.as_str()) {
452                     let mut args: Vec<SpecExpr> = vec![];
453                     while !self.is_rparen() {
454                         args.push(self.parse_spec_expr()?);
455                     }
456                     self.expect_rparen()?;
457                     return Ok(SpecExpr::Op { op, args, pos });
458                 };
459                 let ident = self.str_to_ident(pos, &sym)?;
460                 if self.is_rparen() {
461                     self.expect_rparen()?;
462                     return Ok(SpecExpr::Enum { name: ident });
463                 };
464             }
465             // Unit
466             if self.is_rparen() {
467                 self.expect_rparen()?;
468                 return Ok(SpecExpr::ConstUnit { pos });
469             }
470         }
471         Err(self.error(pos, "Unexpected spec expression".into()))
472     }
473 
parse_spec_op(&mut self, s: &str) -> Result<SpecOp>474     fn parse_spec_op(&mut self, s: &str) -> Result<SpecOp> {
475         let pos = self.pos();
476         match s {
477             "=" => Ok(SpecOp::Eq),
478             "and" => Ok(SpecOp::And),
479             "not" => Ok(SpecOp::Not),
480             "=>" => Ok(SpecOp::Imp),
481             "or" => Ok(SpecOp::Or),
482             "<=" => Ok(SpecOp::Lte),
483             "<" => Ok(SpecOp::Lt),
484             ">=" => Ok(SpecOp::Gte),
485             ">" => Ok(SpecOp::Gt),
486             "bvnot" => Ok(SpecOp::BVNot),
487             "bvand" => Ok(SpecOp::BVAnd),
488             "bvor" => Ok(SpecOp::BVOr),
489             "bvxor" => Ok(SpecOp::BVXor),
490             "bvneg" => Ok(SpecOp::BVNeg),
491             "bvadd" => Ok(SpecOp::BVAdd),
492             "bvsub" => Ok(SpecOp::BVSub),
493             "bvmul" => Ok(SpecOp::BVMul),
494             "bvudiv" => Ok(SpecOp::BVUdiv),
495             "bvurem" => Ok(SpecOp::BVUrem),
496             "bvsdiv" => Ok(SpecOp::BVSdiv),
497             "bvsrem" => Ok(SpecOp::BVSrem),
498             "bvshl" => Ok(SpecOp::BVShl),
499             "bvlshr" => Ok(SpecOp::BVLshr),
500             "bvashr" => Ok(SpecOp::BVAshr),
501             "bvsaddo" => Ok(SpecOp::BVSaddo),
502             "bvule" => Ok(SpecOp::BVUle),
503             "bvult" => Ok(SpecOp::BVUlt),
504             "bvugt" => Ok(SpecOp::BVUgt),
505             "bvuge" => Ok(SpecOp::BVUge),
506             "bvslt" => Ok(SpecOp::BVSlt),
507             "bvsle" => Ok(SpecOp::BVSle),
508             "bvsgt" => Ok(SpecOp::BVSgt),
509             "bvsge" => Ok(SpecOp::BVSge),
510             "rotr" => Ok(SpecOp::Rotr),
511             "rotl" => Ok(SpecOp::Rotl),
512             "extract" => Ok(SpecOp::Extract),
513             "zero_ext" => Ok(SpecOp::ZeroExt),
514             "sign_ext" => Ok(SpecOp::SignExt),
515             "concat" => Ok(SpecOp::Concat),
516             "conv_to" => Ok(SpecOp::ConvTo),
517             "int2bv" => Ok(SpecOp::Int2BV),
518             "bv2int" => Ok(SpecOp::BV2Int),
519             "widthof" => Ok(SpecOp::WidthOf),
520             "if" => Ok(SpecOp::If),
521             "switch" => Ok(SpecOp::Switch),
522             "subs" => Ok(SpecOp::Subs),
523             "popcnt" => Ok(SpecOp::Popcnt),
524             "rev" => Ok(SpecOp::Rev),
525             "cls" => Ok(SpecOp::Cls),
526             "clz" => Ok(SpecOp::Clz),
527             "load_effect" => Ok(SpecOp::LoadEffect),
528             "store_effect" => Ok(SpecOp::StoreEffect),
529             x => Err(self.error(pos, format!("Not a valid spec operator: {x}"))),
530         }
531     }
532 
parse_spec_bit_vector(&mut self) -> Result<(i128, i8)>533     fn parse_spec_bit_vector(&mut self) -> Result<(i128, i8)> {
534         let pos = self.pos();
535         let s = self.expect_symbol()?;
536         if let Some(s) = s.strip_prefix("#b") {
537             match i128::from_str_radix(s, 2) {
538                 Ok(i) => Ok((i, s.len() as i8)),
539                 Err(_) => Err(self.error(pos, "Not a constant binary bit vector".to_string())),
540             }
541         } else if let Some(s) = s.strip_prefix("#x") {
542             match i128::from_str_radix(s, 16) {
543                 Ok(i) => Ok((i, (s.len() as i8) * 4)),
544                 Err(_) => Err(self.error(pos, "Not a constant hex bit vector".to_string())),
545             }
546         } else {
547             Err(self.error(
548                 pos,
549                 "Not a constant bit vector; must start with `#x` (hex) or `#b` (binary)"
550                     .to_string(),
551             ))
552         }
553     }
554 
parse_spec_bool(&mut self) -> Result<bool>555     fn parse_spec_bool(&mut self) -> Result<bool> {
556         let pos = self.pos();
557         let s = self.expect_symbol()?;
558         match s.as_str() {
559             "true" => Ok(true),
560             "false" => Ok(false),
561             x => Err(self.error(pos, format!("Not a valid spec boolean: {x}"))),
562         }
563     }
564 
parse_model(&mut self) -> Result<Model>565     fn parse_model(&mut self) -> Result<Model> {
566         let pos = self.pos();
567         let name = self.parse_ident()?;
568         self.expect_lparen()?; // body
569         let val = if self.eat_sym_str("type")? {
570             let ty = self.parse_model_type();
571             ModelValue::TypeValue(ty?)
572         } else if self.eat_sym_str("enum")? {
573             let mut variants = vec![];
574             let mut has_explicit_value = false;
575             let mut implicit_idx = None;
576 
577             while !self.is_rparen() {
578                 self.expect_lparen()?; // enum value
579                 let name = self.parse_ident()?;
580                 let val = if self.is_rparen() {
581                     // has implicit enum value
582                     if has_explicit_value {
583                         return Err(self.error(
584                             pos,
585                             format!(
586                                 "Spec enum has unexpected implicit value after implicit value."
587                             ),
588                         ));
589                     }
590                     implicit_idx = Some(if let Some(idx) = implicit_idx {
591                         idx + 1
592                     } else {
593                         0
594                     });
595                     SpecExpr::ConstInt {
596                         val: implicit_idx.unwrap(),
597                         pos,
598                     }
599                 } else {
600                     if implicit_idx.is_some() {
601                         return Err(self.error(
602                             pos,
603                             format!(
604                                 "Spec enum has unexpected explicit value after implicit value."
605                             ),
606                         ));
607                     }
608                     has_explicit_value = true;
609                     self.parse_spec_expr()?
610                 };
611                 self.expect_rparen()?;
612                 variants.push((name, val));
613             }
614             ModelValue::EnumValues(variants)
615         } else {
616             return Err(self.error(pos, "Model must be a type or enum".to_string()));
617         };
618 
619         self.expect_rparen()?; // end body
620         Ok(Model { name, val })
621     }
622 
parse_model_type(&mut self) -> Result<ModelType>623     fn parse_model_type(&mut self) -> Result<ModelType> {
624         let pos = self.pos();
625         if self.eat_sym_str("Bool")? {
626             Ok(ModelType::Bool)
627         } else if self.eat_sym_str("Int")? {
628             Ok(ModelType::Int)
629         } else if self.eat_sym_str("Unit")? {
630             Ok(ModelType::Unit)
631         } else if self.is_lparen() {
632             self.expect_lparen()?;
633             let width = if self.eat_sym_str("bv")? {
634                 if self.is_rparen() {
635                     None
636                 } else if self.is_int() {
637                     Some(usize::try_from(self.expect_int()?).map_err(|err| {
638                         self.error(pos, format!("Invalid BitVector width: {err}"))
639                     })?)
640                 } else {
641                     return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()));
642                 }
643             } else {
644                 return Err(self.error(pos, "Badly formed BitVector (bv ...)".to_string()));
645             };
646             self.expect_rparen()?;
647             Ok(ModelType::BitVec(width))
648         } else {
649             Err(self.error(
650                 pos,
651                 "Model type be a Bool, Int, or BitVector (bv ...)".to_string(),
652             ))
653         }
654     }
655 
parse_form(&mut self) -> Result<Form>656     fn parse_form(&mut self) -> Result<Form> {
657         let pos = self.pos();
658         let name = self.parse_ident()?;
659         let signatures = self.parse_signatures()?;
660         Ok(Form {
661             name,
662             signatures,
663             pos,
664         })
665     }
666 
parse_signatures(&mut self) -> Result<Vec<Signature>>667     fn parse_signatures(&mut self) -> Result<Vec<Signature>> {
668         let mut signatures = vec![];
669         while !self.is_rparen() {
670             signatures.push(self.parse_signature()?);
671         }
672         Ok(signatures)
673     }
674 
parse_signature(&mut self) -> Result<Signature>675     fn parse_signature(&mut self) -> Result<Signature> {
676         self.expect_lparen()?;
677         let pos = self.pos();
678         let args = self.parse_tagged_types("args")?;
679         let ret = self.parse_tagged_type("ret")?;
680         let canonical = self.parse_tagged_type("canon")?;
681         self.expect_rparen()?;
682         Ok(Signature {
683             args,
684             ret,
685             canonical,
686             pos,
687         })
688     }
689 
parse_tagged_types(&mut self, tag: &str) -> Result<Vec<ModelType>>690     fn parse_tagged_types(&mut self, tag: &str) -> Result<Vec<ModelType>> {
691         self.expect_lparen()?;
692         let pos = self.pos();
693         if !self.eat_sym_str(tag)? {
694             return Err(self.error(pos, format!("Invalid {tag}: expected ({tag} <arg> ...)")));
695         };
696         let mut params = vec![];
697         while !self.is_rparen() {
698             params.push(self.parse_model_type()?);
699         }
700         self.expect_rparen()?;
701         Ok(params)
702     }
703 
parse_tagged_type(&mut self, tag: &str) -> Result<ModelType>704     fn parse_tagged_type(&mut self, tag: &str) -> Result<ModelType> {
705         self.expect_lparen()?;
706         let pos = self.pos();
707         if !self.eat_sym_str(tag)? {
708             return Err(self.error(pos, format!("Invalid {tag}: expected ({tag} <arg>)")));
709         };
710         let ty = self.parse_model_type()?;
711         self.expect_rparen()?;
712         Ok(ty)
713     }
714 
parse_instantiation(&mut self) -> Result<Instantiation>715     fn parse_instantiation(&mut self) -> Result<Instantiation> {
716         let pos = self.pos();
717         let term = self.parse_ident()?;
718         // Instantiation either has an explicit signatures list, which would
719         // open with a left paren. Or it has an identifier referencing a
720         // predefined set of signatures.
721         if self.is_lparen() {
722             let signatures = self.parse_signatures()?;
723             Ok(Instantiation {
724                 term,
725                 form: None,
726                 signatures,
727                 pos,
728             })
729         } else {
730             let form = self.parse_ident()?;
731             Ok(Instantiation {
732                 term,
733                 form: Some(form),
734                 signatures: vec![],
735                 pos,
736             })
737         }
738     }
739 
parse_extern(&mut self) -> Result<Extern>740     fn parse_extern(&mut self) -> Result<Extern> {
741         let pos = self.pos();
742         if self.eat_sym_str("constructor")? {
743             let term = self.parse_ident()?;
744             let func = self.parse_ident()?;
745             Ok(Extern::Constructor { term, func, pos })
746         } else if self.eat_sym_str("extractor")? {
747             let infallible = self.eat_sym_str("infallible")?;
748 
749             let term = self.parse_ident()?;
750             let func = self.parse_ident()?;
751 
752             Ok(Extern::Extractor {
753                 term,
754                 func,
755                 pos,
756                 infallible,
757             })
758         } else if self.eat_sym_str("const")? {
759             let pos = self.pos();
760             let name = self.parse_const()?;
761             let ty = self.parse_ident()?;
762             Ok(Extern::Const { name, ty, pos })
763         } else {
764             Err(self.error(
765                 pos,
766                 "Invalid extern: must be (extern constructor ...), (extern extractor ...) or (extern const ...)"
767                     .to_string(),
768             ))
769         }
770     }
771 
parse_etor(&mut self) -> Result<Extractor>772     fn parse_etor(&mut self) -> Result<Extractor> {
773         let pos = self.pos();
774         self.expect_lparen()?;
775         let term = self.parse_ident()?;
776         let mut args = vec![];
777         while !self.is_rparen() {
778             args.push(self.parse_ident()?);
779         }
780         self.expect_rparen()?;
781         let template = self.parse_pattern()?;
782         Ok(Extractor {
783             term,
784             args,
785             template,
786             pos,
787         })
788     }
789 
parse_rule(&mut self) -> Result<Rule>790     fn parse_rule(&mut self) -> Result<Rule> {
791         let pos = self.pos();
792         let name = if self.is_sym() {
793             Some(
794                 self.parse_ident()
795                     .map_err(|err| self.error(pos, format!("Invalid rule name: {err:?}")))?,
796             )
797         } else {
798             None
799         };
800         let prio = if self.is_int() {
801             Some(
802                 i64::try_from(self.expect_int()?)
803                     .map_err(|err| self.error(pos, format!("Invalid rule priority: {err}")))?,
804             )
805         } else {
806             None
807         };
808         let pattern = self.parse_pattern()?;
809         let mut iflets = vec![];
810         loop {
811             match self.parse_iflet_or_expr()? {
812                 IfLetOrExpr::IfLet(iflet) => {
813                     iflets.push(iflet);
814                 }
815                 IfLetOrExpr::Expr(expr) => {
816                     return Ok(Rule {
817                         pattern,
818                         iflets,
819                         expr,
820                         pos,
821                         prio,
822                         name,
823                     });
824                 }
825             }
826         }
827     }
828 
parse_pattern(&mut self) -> Result<Pattern>829     fn parse_pattern(&mut self) -> Result<Pattern> {
830         let pos = self.pos();
831         if self.is_int() {
832             Ok(Pattern::ConstInt {
833                 val: self.expect_int()?,
834                 pos,
835             })
836         } else if self.is_const() {
837             let val = self.parse_const()?;
838             Ok(Pattern::ConstPrim { val, pos })
839         } else if self.eat_sym_str("_")? {
840             Ok(Pattern::Wildcard { pos })
841         } else if self.eat_sym_str("true")? {
842             Ok(Pattern::ConstBool { val: true, pos })
843         } else if self.eat_sym_str("false")? {
844             Ok(Pattern::ConstBool { val: false, pos })
845         } else if self.is_sym() {
846             let var = self.parse_ident()?;
847             if self.is_at() {
848                 self.expect_at()?;
849                 let subpat = Box::new(self.parse_pattern()?);
850                 Ok(Pattern::BindPattern { var, subpat, pos })
851             } else {
852                 Ok(Pattern::Var { var, pos })
853             }
854         } else if self.is_lparen() {
855             self.expect_lparen()?;
856             if self.eat_sym_str("and")? {
857                 let mut subpats = vec![];
858                 while !self.is_rparen() {
859                     subpats.push(self.parse_pattern()?);
860                 }
861                 self.expect_rparen()?;
862                 Ok(Pattern::And { subpats, pos })
863             } else {
864                 let sym = self.parse_ident()?;
865                 let mut args = vec![];
866                 while !self.is_rparen() {
867                     args.push(self.parse_pattern()?);
868                 }
869                 self.expect_rparen()?;
870                 Ok(Pattern::Term { sym, args, pos })
871             }
872         } else {
873             Err(self.error(pos, "Unexpected pattern".into()))
874         }
875     }
876 
parse_iflet_or_expr(&mut self) -> Result<IfLetOrExpr>877     fn parse_iflet_or_expr(&mut self) -> Result<IfLetOrExpr> {
878         let pos = self.pos();
879         if self.is_lparen() {
880             self.expect_lparen()?;
881             let ret = if self.eat_sym_str("if-let")? {
882                 IfLetOrExpr::IfLet(self.parse_iflet()?)
883             } else if self.eat_sym_str("if")? {
884                 // Shorthand form: `(if (x))` desugars to `(if-let _
885                 // (x))`.
886                 IfLetOrExpr::IfLet(self.parse_iflet_if()?)
887             } else {
888                 IfLetOrExpr::Expr(self.parse_expr_inner_parens(pos)?)
889             };
890             self.expect_rparen()?;
891             Ok(ret)
892         } else {
893             self.parse_expr().map(IfLetOrExpr::Expr)
894         }
895     }
896 
parse_iflet(&mut self) -> Result<IfLet>897     fn parse_iflet(&mut self) -> Result<IfLet> {
898         let pos = self.pos();
899         let pattern = self.parse_pattern()?;
900         let expr = self.parse_expr()?;
901         Ok(IfLet { pattern, expr, pos })
902     }
903 
parse_iflet_if(&mut self) -> Result<IfLet>904     fn parse_iflet_if(&mut self) -> Result<IfLet> {
905         let pos = self.pos();
906         let expr = self.parse_expr()?;
907         Ok(IfLet {
908             pattern: Pattern::Wildcard { pos },
909             expr,
910             pos,
911         })
912     }
913 
parse_expr(&mut self) -> Result<Expr>914     fn parse_expr(&mut self) -> Result<Expr> {
915         let pos = self.pos();
916         if self.is_lparen() {
917             self.expect_lparen()?;
918             let ret = self.parse_expr_inner_parens(pos)?;
919             self.expect_rparen()?;
920             Ok(ret)
921         } else if self.is_const() {
922             let val = self.parse_const()?;
923             Ok(Expr::ConstPrim { val, pos })
924         } else if self.eat_sym_str("true")? {
925             Ok(Expr::ConstBool { val: true, pos })
926         } else if self.eat_sym_str("false")? {
927             Ok(Expr::ConstBool { val: false, pos })
928         } else if self.is_sym() {
929             let name = self.parse_ident()?;
930             Ok(Expr::Var { name, pos })
931         } else if self.is_int() {
932             let val = self.expect_int()?;
933             Ok(Expr::ConstInt { val, pos })
934         } else {
935             Err(self.error(pos, "Invalid expression".into()))
936         }
937     }
938 
parse_expr_inner_parens(&mut self, pos: Pos) -> Result<Expr>939     fn parse_expr_inner_parens(&mut self, pos: Pos) -> Result<Expr> {
940         if self.eat_sym_str("let")? {
941             self.expect_lparen()?;
942             let mut defs = vec![];
943             while !self.is_rparen() {
944                 let def = self.parse_letdef()?;
945                 defs.push(def);
946             }
947             self.expect_rparen()?;
948             let body = Box::new(self.parse_expr()?);
949             Ok(Expr::Let { defs, body, pos })
950         } else {
951             let sym = self.parse_ident()?;
952             let mut args = vec![];
953             while !self.is_rparen() {
954                 args.push(self.parse_expr()?);
955             }
956             Ok(Expr::Term { sym, args, pos })
957         }
958     }
959 
parse_letdef(&mut self) -> Result<LetDef>960     fn parse_letdef(&mut self) -> Result<LetDef> {
961         let pos = self.pos();
962         self.expect_lparen()?;
963         let var = self.parse_ident()?;
964         let ty = self.parse_ident()?;
965         let val = Box::new(self.parse_expr()?);
966         self.expect_rparen()?;
967         Ok(LetDef { var, ty, val, pos })
968     }
969 
parse_converter(&mut self) -> Result<Converter>970     fn parse_converter(&mut self) -> Result<Converter> {
971         let pos = self.pos();
972         let inner_ty = self.parse_ident()?;
973         let outer_ty = self.parse_ident()?;
974         let term = self.parse_ident()?;
975         Ok(Converter {
976             term,
977             inner_ty,
978             outer_ty,
979             pos,
980         })
981     }
982 }
983