1use crate::ast::*;
4
5use crate::error::{Error, Span};
6use crate::lexer::{Lexer, Pos, Token};
7
8type Result<T> = std::result::Result<T, Error>;
9
10pub 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
17pub 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#[derive(Clone, Debug)]
28pub struct Parser<'a> {
29 lexer: Lexer<'a>,
30 disable_pos: bool,
31}
32
33enum IfLetOrExpr {
37 IfLet(IfLet),
38 Expr(Expr),
39}
40
41impl<'a> Parser<'a> {
42 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) }
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 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()?; 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()?; 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 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 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()?; 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()?; 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 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 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}