1use logos::Logos;
2
3use crate::ast::*;
4use crate::lexer::Token;
5
6#[derive(Debug, Clone)]
9pub struct ParseError {
10 pub message: String,
11 pub span: Span,
12}
13
14impl std::fmt::Display for ParseError {
15 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16 write!(
17 f,
18 "parse error at {}..{}: {}",
19 self.span.start, self.span.end, self.message
20 )
21 }
22}
23
24impl std::error::Error for ParseError {}
25
26pub struct Parser<'src> {
29 tokens: Vec<(Token, Span)>,
30 pos: usize,
31 source: &'src str,
32}
33
34impl<'src> Parser<'src> {
35 pub fn new(source: &'src str) -> Result<Self, ParseError> {
36 let mut tokens = Vec::new();
37 let mut lex = Token::lexer(source);
38 while let Some(tok) = lex.next() {
39 let span = Span::new(lex.span().start, lex.span().end);
40 match tok {
41 Ok(t) => tokens.push((t, span)),
42 Err(()) => {
43 return Err(ParseError {
44 message: format!(
45 "unexpected character: {:?}",
46 &source[lex.span().start..lex.span().end]
47 ),
48 span,
49 });
50 }
51 }
52 }
53 Ok(Parser {
54 tokens,
55 pos: 0,
56 source,
57 })
58 }
59
60 fn peek(&self) -> Option<&Token> {
63 self.tokens.get(self.pos).map(|(t, _)| t)
64 }
65
66 fn peek_span(&self) -> Span {
67 self.tokens
68 .get(self.pos)
69 .map(|(_, s)| s.clone())
70 .unwrap_or_else(|| Span::new(self.source.len(), self.source.len()))
71 }
72
73 fn advance(&mut self) -> (Token, Span) {
74 let item = self.tokens[self.pos].clone();
75 self.pos += 1;
76 item
77 }
78
79 fn expect(&mut self, expected: &Token) -> Result<Span, ParseError> {
80 if self.peek() == Some(expected) {
81 let (_, span) = self.advance();
82 Ok(span)
83 } else {
84 Err(self.error(format!("expected `{expected}`, found {}", self.found())))
85 }
86 }
87
88 fn expect_ident(&mut self) -> Result<(String, Span), ParseError> {
89 match self.peek().cloned() {
90 Some(Token::Ident(name)) => {
91 let (_, span) = self.advance();
92 Ok((name, span))
93 }
94 _ => Err(self.error(format!("expected identifier, found {}", self.found()))),
95 }
96 }
97
98 fn found(&self) -> String {
99 match self.peek() {
100 Some(t) => format!("`{t}`"),
101 None => "end of file".to_string(),
102 }
103 }
104
105 fn error(&self, message: String) -> ParseError {
106 ParseError {
107 message,
108 span: self.peek_span(),
109 }
110 }
111
112 fn at(&self, tok: &Token) -> bool {
113 self.peek() == Some(tok)
114 }
115
116 fn eat(&mut self, tok: &Token) -> bool {
117 if self.at(tok) {
118 self.advance();
119 true
120 } else {
121 false
122 }
123 }
124
125 pub fn parse_program(&mut self) -> Result<Program, ParseError> {
128 let mut declarations = Vec::new();
129 while self.peek().is_some() {
130 declarations.push(self.parse_declaration()?);
131 }
132 Ok(Program { declarations })
133 }
134
135 fn parse_declaration(&mut self) -> Result<Spanned<Declaration>, ParseError> {
136 let mut annotations = Vec::new();
138 while self.at(&Token::At) {
139 annotations.push(self.parse_annotation()?);
140 }
141
142 let start_span = self.peek_span();
143 match self.peek() {
144 Some(Token::Import) => {
145 let decl = self.parse_import()?;
146 let span = start_span.merge(&self.prev_span());
147 Ok(Spanned::new(Declaration::Import(decl), span))
148 }
149 Some(Token::Type) => {
150 let decl = self.parse_type_decl()?;
151 let span = start_span.merge(&self.prev_span());
152 Ok(Spanned::new(Declaration::Type(decl), span))
153 }
154 Some(Token::Enum) => {
155 let decl = self.parse_enum_decl()?;
156 let span = start_span.merge(&self.prev_span());
157 Ok(Spanned::new(Declaration::Enum(decl), span))
158 }
159 Some(Token::Function) => {
160 let decl = self.parse_function_decl()?;
161 let span = start_span.merge(&self.prev_span());
162 Ok(Spanned::new(Declaration::Function(decl), span))
163 }
164 Some(Token::Intent) => {
165 let decl = self.parse_intent_decl(annotations)?;
166 let span = start_span.merge(&self.prev_span());
167 Ok(Spanned::new(Declaration::Intent(decl), span))
168 }
169 Some(Token::Safety) => {
170 let decl = self.parse_safety_decl()?;
171 let span = start_span.merge(&self.prev_span());
172 Ok(Spanned::new(Declaration::Safety(decl), span))
173 }
174 Some(Token::Theorem) => {
175 let decl = self.parse_theorem_decl()?;
176 let span = start_span.merge(&self.prev_span());
177 Ok(Spanned::new(Declaration::Theorem(decl), span))
178 }
179 Some(Token::Axiom) => {
180 let decl = self.parse_axiom_decl()?;
181 let span = start_span.merge(&self.prev_span());
182 Ok(Spanned::new(Declaration::Axiom(decl), span))
183 }
184 Some(Token::Goal) => {
185 let decl = self.parse_goal_decl()?;
186 let span = start_span.merge(&self.prev_span());
187 Ok(Spanned::new(Declaration::Goal(decl), span))
188 }
189 Some(Token::Coverage) => {
190 let decl = self.parse_coverage_decl()?;
191 let span = start_span.merge(&self.prev_span());
192 Ok(Spanned::new(Declaration::Coverage(decl), span))
193 }
194 _ => Err(self.error(format!("expected declaration, found {}", self.found()))),
195 }
196 }
197
198 fn prev_span(&self) -> Span {
199 if self.pos > 0 {
200 self.tokens[self.pos - 1].1.clone()
201 } else {
202 Span::new(0, 0)
203 }
204 }
205
206 fn parse_import(&mut self) -> Result<ImportDecl, ParseError> {
209 self.expect(&Token::Import)?;
210 let (path, _default_alias) = match self.peek() {
211 Some(Token::StringLit(_)) => {
213 let (tok, _) = self.advance();
214 let s = match tok {
215 Token::StringLit(s) => s,
216 _ => unreachable!(),
217 };
218 let default = std::path::Path::new(&s)
220 .file_stem()
221 .and_then(|s| s.to_str())
222 .unwrap_or("unknown")
223 .to_string();
224 (ImportPath::File(s), default)
225 }
226 _ => {
228 let (first, _) = self.expect_ident()?;
229 let mut segments = vec![first];
230 while self.eat(&Token::Dot) {
231 let (seg, _) = self.expect_ident()?;
232 segments.push(seg);
233 }
234 let default = segments.last().cloned().unwrap_or_default();
235 (ImportPath::Plugin(segments), default)
236 }
237 };
238 let alias = if self.eat(&Token::As) {
240 let (name, _) = self.expect_ident()?;
241 Some(name)
242 } else {
243 None
244 };
245 Ok(ImportDecl { path, alias })
246 }
247
248 fn parse_type_decl(&mut self) -> Result<TypeDecl, ParseError> {
251 self.expect(&Token::Type)?;
252 let (name, _) = self.expect_ident()?;
253
254 let type_params = if self.eat(&Token::Lt) {
255 let mut params = Vec::new();
256 loop {
257 let (p, _) = self.expect_ident()?;
258 params.push(p);
259 if !self.eat(&Token::Comma) {
260 break;
261 }
262 }
263 self.expect(&Token::Gt)?;
264 params
265 } else {
266 Vec::new()
267 };
268
269 self.expect(&Token::LBrace)?;
270 let mut fields = Vec::new();
271 while !self.at(&Token::RBrace) {
272 let (fname, _) = self.expect_ident()?;
273 self.expect(&Token::Colon)?;
274 let ty = self.parse_type_expr()?;
275 fields.push(Field { name: fname, ty });
276 }
277 self.expect(&Token::RBrace)?;
278
279 Ok(TypeDecl {
280 name,
281 type_params,
282 fields,
283 })
284 }
285
286 fn parse_enum_decl(&mut self) -> Result<EnumDecl, ParseError> {
289 self.expect(&Token::Enum)?;
290 let (name, _) = self.expect_ident()?;
291 self.expect(&Token::LBrace)?;
292
293 let mut variants = Vec::new();
294 loop {
295 let (v, _) = self.expect_ident()?;
296 variants.push(v);
297 if !self.eat(&Token::Comma) {
298 break;
299 }
300 if self.at(&Token::RBrace) {
302 break;
303 }
304 }
305 self.expect(&Token::RBrace)?;
306
307 Ok(EnumDecl { name, variants })
308 }
309
310 fn parse_function_decl(&mut self) -> Result<FunctionDecl, ParseError> {
313 self.expect(&Token::Function)?;
314 let (name, _) = self.expect_ident()?;
315 let params = self.parse_param_list()?;
316 self.expect(&Token::Arrow)?;
317 let return_type = self.parse_type_expr()?;
318 self.expect(&Token::LBrace)?;
319 let body = self.parse_expr()?;
320 self.expect(&Token::RBrace)?;
321
322 Ok(FunctionDecl {
323 name,
324 params,
325 return_type,
326 body,
327 })
328 }
329
330 fn parse_intent_decl(
333 &mut self,
334 annotations: Vec<Annotation>,
335 ) -> Result<IntentDecl, ParseError> {
336 self.expect(&Token::Intent)?;
337 let (name, _) = self.expect_ident()?;
338 let params = self.parse_param_list()?;
339 self.expect(&Token::LBrace)?;
340
341 let mut clauses = Vec::new();
342 while !self.at(&Token::RBrace) {
343 let clause_start = self.peek_span();
344 let clause = match self.peek() {
345 Some(Token::Require) => {
346 self.advance();
347 let e = self.parse_expr()?;
348 Clause::Require(e)
349 }
350 Some(Token::Ensure) => {
351 self.advance();
352 let e = self.parse_expr()?;
353 Clause::Ensure(e)
354 }
355 Some(Token::Invariant) => {
356 self.advance();
357 let e = self.parse_expr()?;
358 Clause::Invariant(e)
359 }
360 _ => {
361 return Err(self.error(format!(
362 "expected require/ensure/invariant, found {}",
363 self.found()
364 )));
365 }
366 };
367 let span = clause_start.merge(&self.prev_span());
368 clauses.push(Spanned::new(clause, span));
369 }
370 self.expect(&Token::RBrace)?;
371
372 Ok(IntentDecl {
373 name,
374 annotations,
375 params,
376 clauses,
377 })
378 }
379
380 fn parse_safety_decl(&mut self) -> Result<SafetyDecl, ParseError> {
383 self.expect(&Token::Safety)?;
384 let (name, _) = self.expect_ident()?;
385 let params = self.parse_param_list()?;
386 self.expect(&Token::LBrace)?;
387
388 let mut invariants = Vec::new();
389 while !self.at(&Token::RBrace) {
390 self.expect(&Token::Invariant)?;
391 let e = self.parse_expr()?;
392 invariants.push(e);
393 }
394 self.expect(&Token::RBrace)?;
395
396 Ok(SafetyDecl {
397 name,
398 params,
399 invariants,
400 })
401 }
402
403 fn parse_theorem_decl(&mut self) -> Result<TheoremDecl, ParseError> {
406 self.expect(&Token::Theorem)?;
407 let (name, _) = self.expect_ident()?;
408 self.expect(&Token::LBrace)?;
409 let body = self.parse_expr()?;
410 self.expect(&Token::RBrace)?;
411 Ok(TheoremDecl { name, body })
412 }
413
414 fn parse_axiom_decl(&mut self) -> Result<AxiomDecl, ParseError> {
415 self.expect(&Token::Axiom)?;
416 let (name, _) = self.expect_ident()?;
417 self.expect(&Token::LBrace)?;
418 let body = self.parse_expr()?;
419 self.expect(&Token::RBrace)?;
420 Ok(AxiomDecl { name, body })
421 }
422
423 fn parse_goal_decl(&mut self) -> Result<GoalDecl, ParseError> {
426 self.expect(&Token::Goal)?;
427 let name = match self.peek().cloned() {
429 Some(Token::StringLit(s)) => {
430 self.advance();
431 s
432 }
433 _ => {
434 return Err(self.error(format!(
435 "expected string literal goal name, found {}",
436 self.found()
437 )));
438 }
439 };
440 self.expect(&Token::LBrace)?;
441
442 let mut rationale = None;
443 let mut stakeholder = Vec::new();
444 let mut measure = None;
445 let mut realized_by = Vec::new();
446
447 while !self.at(&Token::RBrace) {
448 match self.peek() {
449 Some(Token::Rationale) => {
450 self.advance();
451 self.expect(&Token::Colon)?;
452 rationale = Some(self.expect_string_lit()?);
453 }
454 Some(Token::Stakeholder) => {
455 self.advance();
456 self.expect(&Token::Colon)?;
457 if self.eat(&Token::LBracket) {
459 if !self.at(&Token::RBracket) {
460 loop {
461 stakeholder.push(self.expect_string_lit()?);
462 if !self.eat(&Token::Comma) {
463 break;
464 }
465 }
466 }
467 self.expect(&Token::RBracket)?;
468 } else {
469 let s = self.expect_string_lit()?;
471 for part in s.split(',') {
472 stakeholder.push(part.trim().to_string());
473 }
474 }
475 }
476 Some(Token::Measure) => {
477 self.advance();
478 self.expect(&Token::Colon)?;
479 measure = Some(self.expect_string_lit()?);
480 }
481 Some(Token::RealizedBy) => {
482 self.advance();
483 self.expect(&Token::Colon)?;
484 self.expect(&Token::LBracket)?;
485 if !self.at(&Token::RBracket) {
486 loop {
487 let (id, _) = self.expect_ident()?;
488 realized_by.push(id);
489 if !self.eat(&Token::Comma) {
490 break;
491 }
492 }
493 }
494 self.expect(&Token::RBracket)?;
495 }
496 _ => {
497 return Err(self.error(format!(
498 "expected rationale/stakeholder/measure/realized_by, found {}",
499 self.found()
500 )));
501 }
502 }
503 self.eat(&Token::Comma);
505 }
506 self.expect(&Token::RBrace)?;
507
508 Ok(GoalDecl {
509 name,
510 rationale,
511 stakeholder,
512 measure,
513 realized_by,
514 })
515 }
516
517 fn expect_string_lit(&mut self) -> Result<String, ParseError> {
518 match self.peek().cloned() {
519 Some(Token::StringLit(s)) => {
520 self.advance();
521 Ok(s)
522 }
523 _ => Err(self.error(format!("expected string literal, found {}", self.found()))),
524 }
525 }
526
527 fn parse_coverage_decl(&mut self) -> Result<CoverageDecl, ParseError> {
530 self.expect(&Token::Coverage)?;
531 let name = match self.peek().cloned() {
532 Some(Token::StringLit(s)) => {
533 self.advance();
534 s
535 }
536 _ => {
537 return Err(self.error(format!(
538 "expected string literal coverage name, found {}",
539 self.found()
540 )));
541 }
542 };
543 self.expect(&Token::LBrace)?;
544
545 let mut dimensions = Vec::new();
546
547 while !self.at(&Token::RBrace) {
548 match self.peek() {
549 Some(Token::Dimensions) => {
550 self.advance();
551 self.expect(&Token::Colon)?;
552 self.expect(&Token::LBrace)?;
553 while !self.at(&Token::RBrace) {
554 let (dname, _) = self.expect_ident()?;
555 self.expect(&Token::Colon)?;
556 self.expect(&Token::LBracket)?;
557 let mut values = Vec::new();
558 if !self.at(&Token::RBracket) {
559 loop {
560 values.push(self.parse_expr()?);
561 if !self.eat(&Token::Comma) {
562 break;
563 }
564 }
565 }
566 self.expect(&Token::RBracket)?;
567 self.eat(&Token::Comma);
568 dimensions.push(CoverageDim {
569 name: dname,
570 values,
571 });
572 }
573 self.expect(&Token::RBrace)?;
574 }
575 _ => {
576 return Err(
577 self.error(format!("expected `dimensions`, found {}", self.found()))
578 );
579 }
580 }
581 self.eat(&Token::Comma);
582 }
583 self.expect(&Token::RBrace)?;
584
585 Ok(CoverageDecl { name, dimensions })
586 }
587
588 fn parse_annotation(&mut self) -> Result<Annotation, ParseError> {
591 self.expect(&Token::At)?;
592 let (name, _) = self.expect_ident()?;
593 let mut args = Vec::new();
594
595 if self.eat(&Token::LParen) {
596 if !self.at(&Token::RParen) {
597 loop {
598 let saved = self.pos;
600 if let Some(Token::Ident(key)) = self.peek().cloned() {
601 self.advance();
602 if self.eat(&Token::Colon) {
603 let val = self.parse_expr()?;
604 args.push(AnnotationArg::Named(key, val));
605 } else {
606 self.pos = saved;
607 let val = self.parse_expr()?;
608 args.push(AnnotationArg::Positional(val));
609 }
610 } else {
611 let val = self.parse_expr()?;
612 args.push(AnnotationArg::Positional(val));
613 }
614 if !self.eat(&Token::Comma) {
615 break;
616 }
617 }
618 }
619 self.expect(&Token::RParen)?;
620 }
621
622 Ok(Annotation { name, args })
623 }
624
625 fn parse_param_list(&mut self) -> Result<Vec<Param>, ParseError> {
628 self.expect(&Token::LParen)?;
629 let mut params = Vec::new();
630 if !self.at(&Token::RParen) {
631 loop {
632 let (name, _) = self.expect_ident()?;
633 self.expect(&Token::Colon)?;
634 let ty = self.parse_type_expr()?;
635 params.push(Param { name, ty });
636 if !self.eat(&Token::Comma) {
637 break;
638 }
639 }
640 }
641 self.expect(&Token::RParen)?;
642 Ok(params)
643 }
644
645 fn parse_type_expr(&mut self) -> Result<TypeExpr, ParseError> {
648 let (name, _) = self.expect_ident()?;
649 if self.at(&Token::Dot) {
651 let saved = self.pos;
655 self.advance(); match self.peek() {
657 Some(Token::Ident(type_name)) => {
658 let type_name = type_name.clone();
659 self.advance();
663 if self.eat(&Token::Lt) {
664 let mut args = Vec::new();
665 loop {
666 args.push(self.parse_type_expr()?);
667 if !self.eat(&Token::Comma) {
668 break;
669 }
670 }
671 self.expect(&Token::Gt)?;
672 Ok(TypeExpr::Generic(format!("{name}.{type_name}"), args))
675 } else {
676 Ok(TypeExpr::Qualified(name, type_name))
677 }
678 }
679 _ => {
680 self.pos = saved;
682 Ok(TypeExpr::Named(name))
683 }
684 }
685 } else if self.eat(&Token::Lt) {
686 let mut args = Vec::new();
687 loop {
688 args.push(self.parse_type_expr()?);
689 if !self.eat(&Token::Comma) {
690 break;
691 }
692 }
693 self.expect(&Token::Gt)?;
694 Ok(TypeExpr::Generic(name, args))
695 } else {
696 Ok(TypeExpr::Named(name))
697 }
698 }
699
700 pub fn parse_expr(&mut self) -> Result<Spanned<Expr>, ParseError> {
703 self.parse_pratt(0)
704 }
705
706 fn parse_pratt(&mut self, min_bp: u8) -> Result<Spanned<Expr>, ParseError> {
708 let mut lhs = self.parse_prefix()?;
709
710 loop {
711 lhs = match self.peek() {
713 Some(Token::Dot) => {
714 self.advance();
715 let (field, field_span) = self.expect_ident()?;
716 if self.eat(&Token::Prime) {
718 let span = lhs.span.merge(&self.prev_span());
719 let field_access =
720 Spanned::new(Expr::FieldAccess(Box::new(lhs), field), span.clone());
721 Spanned::new(Expr::Prime(Box::new(field_access)), span)
722 } else {
723 let span = lhs.span.merge(&field_span);
724 Spanned::new(Expr::FieldAccess(Box::new(lhs), field), span)
725 }
726 }
727 Some(Token::Prime) => {
728 self.advance();
729 let span = lhs.span.merge(&self.prev_span());
730 Spanned::new(Expr::Prime(Box::new(lhs)), span)
731 }
732 Some(Token::LBracket) => {
733 self.advance();
734 let index = self.parse_expr()?;
735 let end = self.expect(&Token::RBracket)?;
736 let span = lhs.span.merge(&end);
737 Spanned::new(Expr::Index(Box::new(lhs), Box::new(index)), span)
738 }
739 _ => break,
740 };
741 }
742
743 loop {
745 let op = match self.peek() {
746 Some(Token::Implies) => BinOp::Implies,
747 Some(Token::PipePipe) => BinOp::Or,
748 Some(Token::AmpAmp) => BinOp::And,
749 Some(Token::EqEq) => BinOp::Eq,
750 Some(Token::BangEq) => BinOp::Neq,
751 Some(Token::Lt) => BinOp::Lt,
752 Some(Token::LtEq) => BinOp::Le,
753 Some(Token::Gt) => BinOp::Gt,
754 Some(Token::GtEq) => BinOp::Ge,
755 Some(Token::Plus) => BinOp::Add,
756 Some(Token::Minus) => BinOp::Sub,
757 Some(Token::Star) => BinOp::Mul,
758 Some(Token::Slash) => BinOp::Div,
759 Some(Token::Percent) => BinOp::Mod,
760 _ => break,
761 };
762
763 let (l_bp, r_bp) = infix_binding_power(op);
764 if l_bp < min_bp {
765 break;
766 }
767
768 self.advance(); let rhs = self.parse_pratt(r_bp)?;
770 let span = lhs.span.merge(&rhs.span);
771 lhs = Spanned::new(Expr::BinOp(Box::new(lhs), op, Box::new(rhs)), span);
772 }
773
774 Ok(lhs)
775 }
776
777 fn parse_prefix(&mut self) -> Result<Spanned<Expr>, ParseError> {
779 let start = self.peek_span();
780 match self.peek().cloned() {
781 Some(Token::Bang) => {
783 self.advance();
784 let operand = self.parse_pratt(PREFIX_BP)?;
785 let span = start.merge(&operand.span);
786 Ok(Spanned::new(
787 Expr::UnaryOp(UnaryOp::Not, Box::new(operand)),
788 span,
789 ))
790 }
791 Some(Token::Minus) => {
793 self.advance();
794 let operand = self.parse_pratt(PREFIX_BP)?;
795 let span = start.merge(&operand.span);
796 Ok(Spanned::new(
797 Expr::UnaryOp(UnaryOp::Neg, Box::new(operand)),
798 span,
799 ))
800 }
801 Some(Token::LParen) => {
803 self.advance();
804 let inner = self.parse_expr()?;
805 let end = self.expect(&Token::RParen)?;
806 let span = start.merge(&end);
807 Ok(Spanned::new(Expr::Paren(Box::new(inner)), span))
808 }
809 Some(Token::If) => {
811 self.advance();
812 let cond = self.parse_expr()?;
813 self.expect(&Token::Then)?;
814 let then_expr = self.parse_expr()?;
815 self.expect(&Token::Else)?;
816 let else_expr = self.parse_expr()?;
817 let span = start.merge(&else_expr.span);
818 Ok(Spanned::new(
819 Expr::IfThenElse(Box::new(cond), Box::new(then_expr), Box::new(else_expr)),
820 span,
821 ))
822 }
823 Some(Token::Forall) => {
825 self.advance();
826 let vars = self.parse_typed_vars()?;
827 self.expect(&Token::Comma)?;
828 let body = self.parse_expr()?;
829 let span = start.merge(&body.span);
830 Ok(Spanned::new(Expr::Forall(vars, Box::new(body)), span))
831 }
832 Some(Token::Exists) => {
833 self.advance();
834 let vars = self.parse_typed_vars()?;
835 self.expect(&Token::Comma)?;
836 let body = self.parse_expr()?;
837 let span = start.merge(&body.span);
838 Ok(Spanned::new(Expr::Exists(vars, Box::new(body)), span))
839 }
840 Some(Token::After) => {
842 self.advance();
843 self.expect(&Token::LParen)?;
844 let inner = self.parse_expr()?;
845 let end = self.expect(&Token::RParen)?;
846 let span = start.merge(&end);
847 Ok(Spanned::new(Expr::Prime(Box::new(inner)), span))
848 }
849 Some(Token::IntLit(v)) => {
851 self.advance();
852 Ok(Spanned::new(Expr::IntLit(v), start))
853 }
854 Some(Token::True) => {
856 self.advance();
857 Ok(Spanned::new(Expr::BoolLit(true), start))
858 }
859 Some(Token::False) => {
860 self.advance();
861 Ok(Spanned::new(Expr::BoolLit(false), start))
862 }
863 Some(Token::StringLit(s)) => {
865 self.advance();
866 Ok(Spanned::new(Expr::StringLit(s), start))
867 }
868 Some(Token::Ident(name)) => {
870 self.advance();
871 if self.at(&Token::LParen) {
872 self.advance();
874 let mut args = Vec::new();
875 if !self.at(&Token::RParen) {
876 loop {
877 args.push(self.parse_expr()?);
878 if !self.eat(&Token::Comma) {
879 break;
880 }
881 }
882 }
883 let end = self.expect(&Token::RParen)?;
884 let span = start.merge(&end);
885 Ok(Spanned::new(Expr::Call(name, args), span))
886 } else {
887 Ok(Spanned::new(Expr::Ident(name), start))
888 }
889 }
890 _ => Err(self.error(format!("expected expression, found {}", self.found()))),
891 }
892 }
893
894 fn parse_typed_vars(&mut self) -> Result<Vec<TypedVar>, ParseError> {
897 let mut vars = Vec::new();
898 loop {
899 let (name, _) = self.expect_ident()?;
900 self.expect(&Token::Colon)?;
901 let ty = self.parse_type_expr()?;
902 vars.push(TypedVar { name, ty });
903 if self.at(&Token::Comma) && self.is_typed_var_ahead() {
905 self.advance(); } else {
907 break;
908 }
909 }
910 Ok(vars)
911 }
912
913 fn is_typed_var_ahead(&self) -> bool {
915 let after_comma = self.pos + 1;
917 if after_comma + 1 >= self.tokens.len() {
918 return false;
919 }
920 matches!(self.tokens[after_comma].0, Token::Ident(_))
921 && matches!(self.tokens[after_comma + 1].0, Token::Colon)
922 }
923}
924
925const PREFIX_BP: u8 = 15;
928
929fn infix_binding_power(op: BinOp) -> (u8, u8) {
930 match op {
931 BinOp::Implies => (2, 1),
933 BinOp::Or => (3, 4),
934 BinOp::And => (5, 6),
935 BinOp::Eq | BinOp::Neq => (7, 8),
936 BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => (9, 10),
937 BinOp::Add | BinOp::Sub => (11, 12),
938 BinOp::Mul | BinOp::Div | BinOp::Mod => (13, 14),
939 }
940}
941
942pub fn parse(source: &str) -> Result<Program, ParseError> {
945 let mut parser = Parser::new(source)?;
946 parser.parse_program()
947}
948
949#[cfg(test)]
950mod tests {
951 use super::*;
952
953 #[test]
954 fn parse_type_decl() {
955 let src = r#"type Account { balance: Int owner: String active: Bool }"#;
956 let prog = parse(src).unwrap();
957 assert_eq!(prog.declarations.len(), 1);
958 match &prog.declarations[0].node {
959 Declaration::Type(t) => {
960 assert_eq!(t.name, "Account");
961 assert_eq!(t.fields.len(), 3);
962 }
963 _ => panic!("expected type decl"),
964 }
965 }
966
967 #[test]
968 fn parse_enum_decl() {
969 let src = "enum Role { Admin, Editor, Viewer }";
970 let prog = parse(src).unwrap();
971 assert_eq!(prog.declarations.len(), 1);
972 match &prog.declarations[0].node {
973 Declaration::Enum(e) => {
974 assert_eq!(e.name, "Role");
975 assert_eq!(e.variants, vec!["Admin", "Editor", "Viewer"]);
976 }
977 _ => panic!("expected enum decl"),
978 }
979 }
980
981 #[test]
982 fn parse_intent_basic() {
983 let src = r#"
984intent TransferSafe(sender: Account, receiver: Account, amount: Int) {
985 require amount > 0
986 require sender.balance >= amount
987 ensure sender.balance' == sender.balance - amount
988 ensure receiver.balance' == receiver.balance + amount
989 invariant sender.balance' >= 0
990}
991"#;
992 let prog = parse(src).unwrap();
993 assert_eq!(prog.declarations.len(), 1);
994 match &prog.declarations[0].node {
995 Declaration::Intent(i) => {
996 assert_eq!(i.name, "TransferSafe");
997 assert_eq!(i.params.len(), 3);
998 assert_eq!(i.clauses.len(), 5);
999 }
1000 _ => panic!("expected intent decl"),
1001 }
1002 }
1003
1004 #[test]
1005 fn parse_theorem_with_forall() {
1006 let src = r#"
1007theorem TransferPreservesTotal {
1008 forall s: Account, r: Account, a: Int,
1009 TransferSafe(s, r, a) ==>
1010 s.balance' + r.balance' == s.balance + r.balance
1011}
1012"#;
1013 let prog = parse(src).unwrap();
1014 assert_eq!(prog.declarations.len(), 1);
1015 match &prog.declarations[0].node {
1016 Declaration::Theorem(t) => {
1017 assert_eq!(t.name, "TransferPreservesTotal");
1018 }
1019 _ => panic!("expected theorem decl"),
1020 }
1021 }
1022
1023 #[test]
1024 fn parse_function_decl() {
1025 let src = "function max(a: Int, b: Int) -> Int { if a >= b then a else b }";
1026 let prog = parse(src).unwrap();
1027 match &prog.declarations[0].node {
1028 Declaration::Function(f) => {
1029 assert_eq!(f.name, "max");
1030 assert_eq!(f.params.len(), 2);
1031 }
1032 _ => panic!("expected function decl"),
1033 }
1034 }
1035
1036 #[test]
1037 fn parse_safety_decl() {
1038 let src = r#"
1039safety HomeSafety(home: Home) {
1040 invariant !home.occupied ==> home.frontDoor.locked
1041}
1042"#;
1043 let prog = parse(src).unwrap();
1044 match &prog.declarations[0].node {
1045 Declaration::Safety(s) => {
1046 assert_eq!(s.name, "HomeSafety");
1047 assert_eq!(s.invariants.len(), 1);
1048 }
1049 _ => panic!("expected safety decl"),
1050 }
1051 }
1052
1053 #[test]
1054 fn parse_after_desugar() {
1055 let src = r#"
1056intent T(x: Account) {
1057 ensure after(x.balance) == x.balance - 1
1058}
1059"#;
1060 let prog = parse(src).unwrap();
1061 match &prog.declarations[0].node {
1062 Declaration::Intent(i) => {
1063 match &i.clauses[0].node {
1065 Clause::Ensure(e) => match &e.node {
1066 Expr::BinOp(lhs, BinOp::Eq, _) => match &lhs.node {
1067 Expr::Prime(_) => {} other => panic!("expected Prime, got {other:?}"),
1069 },
1070 other => panic!("expected BinOp, got {other:?}"),
1071 },
1072 _ => panic!("expected ensure"),
1073 }
1074 }
1075 _ => panic!("expected intent decl"),
1076 }
1077 }
1078
1079 #[test]
1080 fn parse_import() {
1081 let src = "import smarthome";
1082 let prog = parse(src).unwrap();
1083 match &prog.declarations[0].node {
1084 Declaration::Import(i) => {
1085 assert!(matches!(&i.path, ImportPath::Plugin(p) if p == &["smarthome"]));
1086 assert_eq!(i.alias, None);
1087 }
1088 _ => panic!("expected import"),
1089 }
1090 }
1091
1092 #[test]
1093 fn parse_import_dotted() {
1094 let src = "import finance.currency";
1095 let prog = parse(src).unwrap();
1096 match &prog.declarations[0].node {
1097 Declaration::Import(i) => {
1098 assert!(matches!(&i.path, ImportPath::Plugin(p) if p == &["finance", "currency"]));
1099 assert_eq!(i.alias, None);
1100 }
1101 _ => panic!("expected import"),
1102 }
1103 }
1104
1105 #[test]
1106 fn parse_import_file() {
1107 let src = r#"import "./domains/payment/types.intent""#;
1108 let prog = parse(src).unwrap();
1109 match &prog.declarations[0].node {
1110 Declaration::Import(i) => {
1111 assert!(
1112 matches!(&i.path, ImportPath::File(p) if p == "./domains/payment/types.intent")
1113 );
1114 assert_eq!(i.alias, None);
1115 }
1116 _ => panic!("expected import"),
1117 }
1118 }
1119
1120 #[test]
1121 fn parse_import_file_with_alias() {
1122 let src = r#"import "./domains/payment/types.intent" as payment"#;
1123 let prog = parse(src).unwrap();
1124 match &prog.declarations[0].node {
1125 Declaration::Import(i) => {
1126 assert!(
1127 matches!(&i.path, ImportPath::File(p) if p == "./domains/payment/types.intent")
1128 );
1129 assert_eq!(i.alias, Some("payment".to_string()));
1130 }
1131 _ => panic!("expected import"),
1132 }
1133 }
1134
1135 #[test]
1136 fn parse_import_plugin_with_alias() {
1137 let src = "import finance.currency as money";
1138 let prog = parse(src).unwrap();
1139 match &prog.declarations[0].node {
1140 Declaration::Import(i) => {
1141 assert!(matches!(&i.path, ImportPath::Plugin(p) if p == &["finance", "currency"]));
1142 assert_eq!(i.alias, Some("money".to_string()));
1143 }
1144 _ => panic!("expected import"),
1145 }
1146 }
1147
1148 #[test]
1149 fn parse_qualified_type() {
1150 let src = r#"
1151intent Checkout(wallet: payment.Account, profile: user.Account) {
1152 require wallet.balance >= 0
1153}
1154"#;
1155 let prog = parse(src).unwrap();
1156 match &prog.declarations[0].node {
1157 Declaration::Intent(i) => {
1158 assert_eq!(
1159 i.params[0].ty,
1160 TypeExpr::Qualified("payment".into(), "Account".into())
1161 );
1162 assert_eq!(
1163 i.params[1].ty,
1164 TypeExpr::Qualified("user".into(), "Account".into())
1165 );
1166 }
1167 _ => panic!("expected intent"),
1168 }
1169 }
1170
1171 #[test]
1172 fn parse_exists_expr() {
1173 let src = r#"
1174intent Arrive(home: Home) {
1175 ensure exists l: Light, l.room == "living" && l.on' == true
1176}
1177"#;
1178 let prog = parse(src).unwrap();
1179 match &prog.declarations[0].node {
1180 Declaration::Intent(i) => {
1181 assert_eq!(i.clauses.len(), 1);
1182 }
1183 _ => panic!("expected intent"),
1184 }
1185 }
1186}