Skip to main content

intent_lang_syntax/
parser.rs

1use logos::Logos;
2
3use crate::ast::*;
4use crate::lexer::Token;
5
6// ── Error type ───────────────────────────────────────────────
7
8#[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
26// ── Parser state ─────────────────────────────────────────────
27
28pub 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    // ── Helpers ──────────────────────────────────────────
61
62    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    // ── Program ──────────────────────────────────────────
126
127    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        // Collect annotations
137        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    // ── Import ───────────────────────────────────────────
207
208    fn parse_import(&mut self) -> Result<ImportDecl, ParseError> {
209        self.expect(&Token::Import)?;
210        let (path, _default_alias) = match self.peek() {
211            // File import: `import "./path/to/file.intent"`
212            Some(Token::StringLit(_)) => {
213                let (tok, _) = self.advance();
214                let s = match tok {
215                    Token::StringLit(s) => s,
216                    _ => unreachable!(),
217                };
218                // Default alias is the file stem (filename without .intent)
219                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            // Plugin import: `import smarthome` or `import finance.currency`
227            _ => {
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        // Optional alias: `as name`
239        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    // ── Type ─────────────────────────────────────────────
249
250    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    // ── Enum ─────────────────────────────────────────────
287
288    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            // Allow trailing comma
301            if self.at(&Token::RBrace) {
302                break;
303            }
304        }
305        self.expect(&Token::RBrace)?;
306
307        Ok(EnumDecl { name, variants })
308    }
309
310    // ── Function ─────────────────────────────────────────
311
312    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    // ── Intent ───────────────────────────────────────────
331
332    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    // ── Safety ───────────────────────────────────────────
381
382    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    // ── Theorem / Axiom ──────────────────────────────────
404
405    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    // ── Goal (RFC A1) ────────────────────────────────────
424
425    fn parse_goal_decl(&mut self) -> Result<GoalDecl, ParseError> {
426        self.expect(&Token::Goal)?;
427        // Name must be a string literal: `goal "User balance never negative" { ... }`
428        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                    // Accept either single string or [a, b, c]
458                    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                        // Comma-separated string list inside one string
470                        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            // Optional semicolon-like: comma between fields is allowed
504            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    // ── Coverage (RFC A3) ────────────────────────────────
528
529    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    // ── Annotations ──────────────────────────────────────
589
590    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                    // Check for named arg: `key: value`
599                    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    // ── Param list ───────────────────────────────────────
626
627    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    // ── Type expressions ─────────────────────────────────
646
647    fn parse_type_expr(&mut self) -> Result<TypeExpr, ParseError> {
648        let (name, _) = self.expect_ident()?;
649        // Check for qualified type: `module.TypeName`
650        if self.at(&Token::Dot) {
651            // Peek ahead: if next is Dot then Ident (then NOT Dot again), it's qualified
652            // But we also need to distinguish from field access in expressions.
653            // In type position, `ident.Ident` is always qualified.
654            let saved = self.pos;
655            self.advance(); // eat dot
656            match self.peek() {
657                Some(Token::Ident(type_name)) => {
658                    let type_name = type_name.clone();
659                    // Check if the type_name starts with uppercase (convention)
660                    // or if followed by `<` (generic). In type position after dot,
661                    // this is always a qualified reference.
662                    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                        // Qualified generic not yet supported — treat as Generic with qualified base
673                        // For now, just use the type_name as generic
674                        Ok(TypeExpr::Generic(format!("{name}.{type_name}"), args))
675                    } else {
676                        Ok(TypeExpr::Qualified(name, type_name))
677                    }
678                }
679                _ => {
680                    // Not a qualified type, backtrack
681                    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    // ── Expression parsing (Pratt) ───────────────────────
701
702    pub fn parse_expr(&mut self) -> Result<Spanned<Expr>, ParseError> {
703        self.parse_pratt(0)
704    }
705
706    /// Pratt parser: parse expression with minimum binding power.
707    fn parse_pratt(&mut self, min_bp: u8) -> Result<Spanned<Expr>, ParseError> {
708        let mut lhs = self.parse_prefix()?;
709
710        loop {
711            // Postfix: `.field`, `'`, `[index]`
712            lhs = match self.peek() {
713                Some(Token::Dot) => {
714                    self.advance();
715                    let (field, field_span) = self.expect_ident()?;
716                    // Check for field prime: `expr.field'`
717                    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        // Infix binary operators
744        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(); // consume operator
769            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    /// Parse prefix / atom expressions.
778    fn parse_prefix(&mut self) -> Result<Spanned<Expr>, ParseError> {
779        let start = self.peek_span();
780        match self.peek().cloned() {
781            // Unary !
782            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            // Unary -
792            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            // Parenthesized
802            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            // If-then-else
810            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            // Forall / Exists
824            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            // `after(expr)` — desugar to Prime
841            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            // Integer literal
850            Some(Token::IntLit(v)) => {
851                self.advance();
852                Ok(Spanned::new(Expr::IntLit(v), start))
853            }
854            // Boolean
855            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            // String
864            Some(Token::StringLit(s)) => {
865                self.advance();
866                Ok(Spanned::new(Expr::StringLit(s), start))
867            }
868            // Identifier or function call
869            Some(Token::Ident(name)) => {
870                self.advance();
871                if self.at(&Token::LParen) {
872                    // Function call
873                    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    /// Parse typed variable list for quantifiers: `x: T, y: U`
895    /// Stops when next comma is not followed by `ident : type` pattern.
896    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            // Peek ahead: if next is comma then ident then colon, more typed vars
904            if self.at(&Token::Comma) && self.is_typed_var_ahead() {
905                self.advance(); // eat comma
906            } else {
907                break;
908            }
909        }
910        Ok(vars)
911    }
912
913    /// Look ahead to check if comma is followed by `ident : type` (another typed var).
914    fn is_typed_var_ahead(&self) -> bool {
915        // We're at a comma. Check pos+1 is ident and pos+2 is colon.
916        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
925// ── Binding power tables ─────────────────────────────────────
926
927const PREFIX_BP: u8 = 15;
928
929fn infix_binding_power(op: BinOp) -> (u8, u8) {
930    match op {
931        // ==> is right-associative: (l=2, r=1)
932        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
942// ── Public convenience ───────────────────────────────────────
943
944pub 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                // The ensure clause should contain a Prime node
1064                match &i.clauses[0].node {
1065                    Clause::Ensure(e) => match &e.node {
1066                        Expr::BinOp(lhs, BinOp::Eq, _) => match &lhs.node {
1067                            Expr::Prime(_) => {} // correct
1068                            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}