Skip to main content

elenchus_parser/
lib.rs

1//! elenchus-parser — parses the English-like elenchus DSL into an AST.
2//!
3//! Style mirrors `vsm-parser`: zero-copy over `&str`, `nom` + `nom_locate`
4//! for line/column tracking, and human-friendly syntax diagnostics. Syntax is
5//! line/keyword-oriented (not S-expressions) so small models cannot trip on
6//! parentheses or indentation.
7//!
8//! Grammar (see docs/SPEC.md, "Grammar (EBNF)"):
9//! - statements are newline-terminated; indentation is cosmetic, not significant;
10//! - keywords are ALWAYS CAPS (ASCII); identifiers are content (case-sensitive,
11//!   verbatim, any-script letters — e.g. `условие`, `名前`);
12//! - block boundaries (PREMISE/RULE bodies) are found by keywords, never by indent.
13//!
14//! On error, [`parse`] returns [`Diagnostics`]: *every* syntax error from one
15//! pass, each rendered as a caret block with the keyword's correct syntax (see
16//! [`diag`] and [`syntax`]).
17//!
18//! The crate is split into focused modules — [`ast`] (the tree), [`keywords`]
19//! (the single keyword table: spellings, roles, syntax cards), [`diag`] (error
20//! rendering), and `grammar` (the nom parser + recovering driver) — re-exported
21//! here as a flat public surface.
22//!
23//! # Example
24//!
25//! ```
26//! use elenchus_parser::{Statement, parse};
27//!
28//! // One statement per line; the result is a flat list of `Statement`s.
29//! let program = parse("FACT socrates is human\nCHECK socrates\n").unwrap();
30//! assert_eq!(program.statements.len(), 2);
31//! assert!(matches!(program.statements[0], Statement::Fact(_)));
32//! ```
33#![no_std]
34// Every public item is documented; CI (`clippy -D warnings`) keeps it that way.
35#![warn(missing_docs)]
36
37extern crate alloc;
38
39pub mod ast;
40pub mod diag;
41mod grammar;
42pub mod keywords;
43
44pub use ast::{
45    Atom, Body, CloseKind, Conn, ListOp, Literal, Located, Program, Quant, Span, Statement,
46};
47pub use diag::{Diagnostic, Diagnostics};
48pub use grammar::parse;
49pub use keywords::{Card, KEYWORDS, Keyword, card_for, is_reserved, kw};
50
51#[cfg(test)]
52mod tests {
53    use super::*;
54    use alloc::format;
55
56    fn prog(src: &str) -> Program<'_> {
57        parse(src).expect("should parse")
58    }
59
60    /// `(subject, predicate?, object?)` of one atom, borrowed from the source.
61    /// `predicate` is `None` for a bare proposition (a `VAR` port used in a body).
62    type AtomShape<'a> = (&'a str, Option<&'a str>, Option<&'a str>);
63    /// A list premise flattened to `(operator, its atoms)`.
64    type ListShape<'a> = (ListOp, Vec<AtomShape<'a>>);
65
66    use alloc::vec::Vec;
67
68    /// Atom data flattened to owned tuples — span-independent, for structural
69    /// comparison (spans differ by offset, which is exactly what "cosmetic" means).
70    fn atom_shapes<'a>(p: &Program<'a>) -> Vec<ListShape<'a>> {
71        p.statements
72            .iter()
73            .filter_map(|s| match s {
74                Statement::Premise {
75                    body: Body::List { op, atoms },
76                    ..
77                } => Some((
78                    *op,
79                    atoms
80                        .iter()
81                        .map(|a| (a.data.subject, a.data.predicate, a.data.object))
82                        .collect(),
83                )),
84                _ => None,
85            })
86            .collect()
87    }
88
89    #[test]
90    fn parses_fact_and_negation() {
91        let p = prog(
92            r#"
93        FACT Creature_A has flying
94        NOT Creature_A has cold_blood
95        "#,
96        );
97        assert_eq!(p.statements.len(), 2);
98        match &p.statements[0] {
99            Statement::Fact(a) => {
100                assert_eq!(a.data.subject, "Creature_A");
101                assert_eq!(a.data.predicate, Some("has"));
102                assert_eq!(a.data.object, Some("flying"));
103            }
104            other => panic!("expected fact, got {:?}", other),
105        }
106        match &p.statements[1] {
107            Statement::Negation(a) => {
108                assert_eq!(a.data.object, Some("cold_blood"));
109            }
110            other => panic!("expected negation, got {:?}", other),
111        }
112    }
113
114    #[test]
115    fn fact_without_object() {
116        let p = prog("FACT Motor over_100\n");
117        match &p.statements[0] {
118            Statement::Fact(a) => {
119                assert_eq!(a.data.subject, "Motor");
120                assert_eq!(a.data.predicate, Some("over_100"));
121                assert_eq!(a.data.object, None);
122            }
123            other => panic!("expected fact, got {:?}", other),
124        }
125    }
126
127    #[test]
128    fn bare_proposition_parses_with_no_predicate() {
129        // A lone identifier is a bare proposition (a VAR port used as an atom):
130        // predicate and object both None. Legality (declared VAR) is the compiler's.
131        let p = prog("FACT db_ready\n");
132        match &p.statements[0] {
133            Statement::Fact(a) => {
134                assert_eq!(a.data.subject, "db_ready");
135                assert_eq!(a.data.predicate, None);
136                assert_eq!(a.data.object, None);
137            }
138            other => panic!("expected fact, got {:?}", other),
139        }
140    }
141
142    #[test]
143    fn var_parses_with_and_without_default() {
144        let p = prog(
145            r#"
146        VAR db_ready DEFAULT false
147        VAR deploy_ok
148        "#,
149        );
150        assert_eq!(p.statements.len(), 2);
151        match &p.statements[0] {
152            Statement::Var { name, default } => {
153                assert_eq!(name.data, "db_ready");
154                assert_eq!(*default, Some(false));
155            }
156            other => panic!("expected var, got {:?}", other),
157        }
158        match &p.statements[1] {
159            Statement::Var { name, default } => {
160                assert_eq!(name.data, "deploy_ok");
161                assert_eq!(*default, None);
162            }
163            other => panic!("expected var, got {:?}", other),
164        }
165    }
166
167    #[test]
168    fn provide_parses_name_and_value() {
169        let p = prog("PROVIDE db_ready: true\nPROVIDE deploy_ok: false\n");
170        assert_eq!(p.statements.len(), 2);
171        match &p.statements[0] {
172            Statement::Provide { name, value } => {
173                assert_eq!(name.data, "db_ready");
174                assert!(*value);
175            }
176            other => panic!("expected provide, got {:?}", other),
177        }
178        match &p.statements[1] {
179            Statement::Provide { value, .. } => assert!(!*value),
180            other => panic!("expected provide, got {:?}", other),
181        }
182    }
183
184    #[test]
185    fn parses_assume_positive_and_negated() {
186        let p = prog(
187            r#"
188        ASSUME rel in_prod
189        ASSUME NOT rel has_rollback
190        "#,
191        );
192        assert_eq!(p.statements.len(), 2);
193        match &p.statements[0] {
194            Statement::Assume(l) => {
195                assert!(!l.data.negated);
196                assert_eq!(l.data.atom.subject, "rel");
197                assert_eq!(l.data.atom.predicate, Some("in_prod"));
198                assert_eq!(l.data.atom.object, None);
199            }
200            other => panic!("expected assume, got {:?}", other),
201        }
202        match &p.statements[1] {
203            Statement::Assume(l) => {
204                assert!(l.data.negated);
205                assert_eq!(l.data.atom.predicate, Some("has_rollback"));
206            }
207            other => panic!("expected negated assume, got {:?}", other),
208        }
209    }
210
211    #[test]
212    fn assume_is_a_reserved_word() {
213        assert!(parse("FACT ASSUME has x\n").is_err());
214    }
215
216    #[test]
217    fn parses_import() {
218        let p = prog("IMPORT \"physics.vrf\"\n");
219        match &p.statements[0] {
220            Statement::Import { path, alias } => {
221                assert_eq!(path.data, "physics.vrf");
222                assert!(alias.is_none());
223            }
224            other => panic!("expected import, got {:?}", other),
225        }
226    }
227
228    #[test]
229    fn parses_import_with_alias() {
230        let p = prog("IMPORT \"physics.vrf\" AS phys\n");
231        match &p.statements[0] {
232            Statement::Import { path, alias } => {
233                assert_eq!(path.data, "physics.vrf");
234                assert_eq!(alias.as_ref().unwrap().data, "phys");
235            }
236            other => panic!("expected import, got {:?}", other),
237        }
238    }
239
240    #[test]
241    fn parses_domain_declaration() {
242        let p = prog("DOMAIN physics\n");
243        match &p.statements[0] {
244            Statement::Domain(name) => assert_eq!(name.data, "physics"),
245            other => panic!("expected domain, got {:?}", other),
246        }
247    }
248
249    #[test]
250    fn parses_domain_qualified_atom() {
251        // `physics.Motor over_200` → domain prefix split from the subject.
252        let p = prog("FACT physics.Motor over_200\n");
253        match &p.statements[0] {
254            Statement::Fact(a) => {
255                assert_eq!(a.data.domain, Some("physics"));
256                assert_eq!(a.data.subject, "Motor");
257                assert_eq!(a.data.predicate, Some("over_200"));
258            }
259            other => panic!("expected fact, got {:?}", other),
260        }
261    }
262
263    #[test]
264    fn bare_atom_has_no_domain() {
265        let p = prog("FACT engine has_fuel\n");
266        match &p.statements[0] {
267            Statement::Fact(a) => {
268                assert_eq!(a.data.domain, None);
269                assert_eq!(a.data.subject, "engine");
270            }
271            other => panic!("expected fact, got {:?}", other),
272        }
273    }
274
275    #[test]
276    fn domain_is_a_reserved_word() {
277        assert!(parse("FACT DOMAIN has x\n").is_err());
278        assert!(parse("FACT AS has x\n").is_err());
279    }
280
281    #[test]
282    fn parses_exclusive_premise() {
283        let src = r#"
284        PREMISE fly_xor_swim:
285            EXCLUSIVE
286                Creature_A has flying
287                Creature_A has swimming
288        "#;
289        let p = prog(src);
290        match &p.statements[0] {
291            Statement::Premise { name, body, .. } => {
292                assert_eq!(name.data, "fly_xor_swim");
293                match body {
294                    Body::List { op, atoms } => {
295                        assert_eq!(*op, ListOp::Exclusive);
296                        assert_eq!(atoms.len(), 2);
297                        assert_eq!(atoms[1].data.object, Some("swimming"));
298                    }
299                    other => panic!("expected list body, got {:?}", other),
300                }
301            }
302            other => panic!("expected premise, got {:?}", other),
303        }
304    }
305
306    #[test]
307    fn parses_implication_premise_with_and() {
308        let src = r#"
309        PREMISE wings_need_bone:
310            WHEN Creature_A has flying
311            THEN Creature_A has wing
312            AND  Creature_A has bone
313        "#;
314        let p = prog(src);
315        match &p.statements[0] {
316            Statement::Premise {
317                body:
318                    Body::Impl {
319                        antecedent,
320                        consequent,
321                        ..
322                    },
323                ..
324            } => {
325                assert_eq!(antecedent.len(), 1);
326                assert_eq!(antecedent[0].data.atom.object, Some("flying"));
327                assert_eq!(consequent.len(), 2);
328                assert_eq!(consequent[0].data.atom.object, Some("wing"));
329                assert_eq!(consequent[1].data.atom.object, Some("bone"));
330            }
331            other => panic!("expected impl premise, got {:?}", other),
332        }
333    }
334
335    #[test]
336    fn antecedent_and_goes_before_then() {
337        let src = r#"
338        PREMISE deploy:
339            WHEN s tested
340            AND s reviewed
341            THEN s can_deploy
342        "#;
343        let p = prog(src);
344        match &p.statements[0] {
345            Statement::Premise {
346                body:
347                    Body::Impl {
348                        antecedent,
349                        consequent,
350                        ..
351                    },
352                ..
353            } => {
354                assert_eq!(antecedent.len(), 2);
355                assert_eq!(consequent.len(), 1);
356            }
357            other => panic!("unexpected: {:?}", other),
358        }
359    }
360
361    #[test]
362    fn when_or_sets_disjunctive_antecedent() {
363        let src = r#"
364        PREMISE p:
365            WHEN x a
366            OR x b
367            THEN x c
368        "#;
369        match &prog(src).statements[0] {
370            Statement::Premise {
371                body:
372                    Body::Impl {
373                        antecedent,
374                        ante_conn,
375                        consequent,
376                        cons_conn,
377                    },
378                ..
379            } => {
380                assert_eq!(antecedent.len(), 2);
381                assert_eq!(*ante_conn, Conn::Or);
382                assert_eq!(consequent.len(), 1);
383                assert_eq!(*cons_conn, Conn::And); // single consequent → AND
384            }
385            other => panic!("expected impl premise, got {:?}", other),
386        }
387    }
388
389    #[test]
390    fn then_or_sets_disjunctive_consequent() {
391        let src = r#"
392        PREMISE p:
393            WHEN x a
394            THEN x b
395            OR x c
396        "#;
397        match &prog(src).statements[0] {
398            Statement::Premise {
399                body:
400                    Body::Impl {
401                        consequent,
402                        cons_conn,
403                        ..
404                    },
405                ..
406            } => {
407                assert_eq!(consequent.len(), 2);
408                assert_eq!(*cons_conn, Conn::Or);
409            }
410            other => panic!("expected impl premise, got {:?}", other),
411        }
412    }
413
414    #[test]
415    fn mixing_and_or_in_one_group_is_an_error() {
416        let mixed_when = r#"
417        PREMISE p:
418            WHEN x a
419            AND x b
420            OR x c
421            THEN x d
422        "#;
423        let mixed_then = r#"
424        PREMISE p:
425            WHEN x a
426            THEN x b
427            AND x c
428            OR x d
429        "#;
430        assert!(parse(mixed_when).is_err());
431        assert!(parse(mixed_then).is_err());
432    }
433
434    #[test]
435    fn or_is_a_reserved_word() {
436        assert!(parse("FACT OR has x\n").is_err());
437    }
438
439    #[test]
440    fn parses_negated_literal_in_rule() {
441        let src = r#"
442        RULE pick_slow:
443            WHEN NOT Motor over_100
444            THEN Motor uses slow_path
445        "#;
446        let p = prog(src);
447        match &p.statements[0] {
448            Statement::Rule {
449                body: Body::Impl { antecedent, .. },
450                ..
451            } => {
452                assert!(antecedent[0].data.negated);
453                assert_eq!(antecedent[0].data.atom.predicate, Some("over_100"));
454            }
455            other => panic!("expected rule, got {:?}", other),
456        }
457    }
458
459    #[test]
460    fn parses_check_variants() {
461        let p = prog("CHECK Creature_A BIDIRECTIONAL\n");
462        match &p.statements[0] {
463            Statement::Check {
464                subject,
465                bidirectional,
466            } => {
467                assert_eq!(subject.as_ref().unwrap().data, "Creature_A");
468                assert!(bidirectional);
469            }
470            other => panic!("expected check, got {:?}", other),
471        }
472
473        let p = prog("CHECK\n");
474        match &p.statements[0] {
475            Statement::Check {
476                subject,
477                bidirectional,
478            } => {
479                assert!(subject.is_none());
480                assert!(!bidirectional);
481            }
482            other => panic!("expected check, got {:?}", other),
483        }
484    }
485
486    #[test]
487    fn comments_and_blanks_are_ignored() {
488        let src = "// header\n\nFACT a b   // trailing comment\n\n// tail\n";
489        let p = prog(src);
490        assert_eq!(p.statements.len(), 1);
491    }
492
493    #[test]
494    fn indentation_is_cosmetic() {
495        let flat = r#"
496        PREMISE x:
497        EXCLUSIVE
498        a b
499        a c
500        "#;
501        let indented = r#"
502        PREMISE x:
503                EXCLUSIVE
504          a b
505                    a c
506        "#;
507        // Spans differ by offset (cosmetic); the parsed structure must be identical.
508        assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
509    }
510
511    #[test]
512    fn top_level_statements_may_be_indented() {
513        // Leading indentation on the FACT/PREMISE/CHECK lines themselves is also
514        // cosmetic (so a whole program can be pasted indented inside a here-doc).
515        let flat = r#"
516        FACT x a
517        NOT x b
518        CHECK x
519        "#;
520        let indented = r#"
521            FACT x a
522                NOT x b
523            CHECK x
524        "#;
525        assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
526        assert_eq!(prog(indented).statements.len(), 3);
527    }
528
529    #[test]
530    fn full_creature_example_parses() {
531        let src = include_str!("../../../docs/examples/creature.vrf");
532        let p = prog(src);
533        // 1 DOMAIN + 2 FACT + 3 PREMISE + 1 RULE + 1 CHECK = 8
534        assert_eq!(p.statements.len(), 8);
535    }
536
537    #[test]
538    fn import_demo_example_parses() {
539        let src = include_str!("../../../docs/examples/import-demo.vrf");
540        let p = prog(src);
541        assert!(matches!(p.statements[0], Statement::Domain(_)));
542        assert!(matches!(p.statements[1], Statement::Import { .. }));
543    }
544
545    #[test]
546    fn unicode_identifiers_any_script() {
547        // Cyrillic subject/predicate/object, mixed with `_` and digits (not first).
548        let p = prog(
549            r#"
550        FACT кот пушистый2
551        NOT собака has крылья
552        "#,
553        );
554        match &p.statements[0] {
555            Statement::Fact(a) => {
556                assert_eq!(a.data.subject, "кот");
557                assert_eq!(a.data.predicate, Some("пушистый2"));
558                assert_eq!(a.data.object, None);
559            }
560            other => panic!("expected fact, got {:?}", other),
561        }
562        match &p.statements[1] {
563            Statement::Negation(a) => {
564                assert_eq!(a.data.subject, "собака");
565                assert_eq!(a.data.object, Some("крылья"));
566            }
567            other => panic!("expected negation, got {:?}", other),
568        }
569    }
570
571    #[test]
572    fn unicode_premise_name_and_body() {
573        let src = r#"
574        PREMISE правило_лая:
575            WHEN собака has хвост
576            THEN собака умеет_лаять
577        "#;
578        match &prog(src).statements[0] {
579            Statement::Premise { name, body, .. } => {
580                assert_eq!(name.data, "правило_лая");
581                match body {
582                    Body::Impl {
583                        antecedent,
584                        consequent,
585                        ..
586                    } => {
587                        assert_eq!(antecedent[0].data.atom.subject, "собака");
588                        assert_eq!(consequent[0].data.atom.subject, "собака");
589                        assert_eq!(consequent[0].data.atom.predicate, Some("умеет_лаять"));
590                    }
591                    other => panic!("expected impl body, got {:?}", other),
592                }
593            }
594            other => panic!("expected premise, got {:?}", other),
595        }
596    }
597
598    #[test]
599    fn identifier_cannot_start_with_digit() {
600        // `2cats` is not a valid subject — first char must be a letter.
601        assert!(parse("FACT 2cats has fur\n").is_err());
602    }
603
604    #[test]
605    fn punctuation_is_rejected_in_identifier() {
606        // `!` and other symbols are not identifier characters.
607        assert!(parse("FACT cat! has fur\n").is_err());
608    }
609
610    #[test]
611    fn reserved_word_cannot_be_identifier() {
612        // `WHEN` as a subject is illegal.
613        assert!(parse("FACT WHEN has x\n").is_err());
614    }
615
616    #[test]
617    fn pretty_error_points_at_offending_line() {
618        let src = r#"FACT a b
619!garbage here
620FACT c d
621"#;
622        let err = parse(src).expect_err("should fail");
623        let shown = format!("{}", err);
624        // The new diagnostic format: a RESULT header, the line number, the
625        // verbatim offending line, and a caret pointing at it.
626        assert!(shown.contains("RESULT: 1 syntax error"));
627        assert!(shown.contains("line 2"));
628        assert!(shown.contains("!garbage here"));
629        assert!(shown.contains('^'));
630    }
631
632    #[test]
633    fn collects_every_error_in_one_pass() {
634        // Three broken top-level lines among valid ones → exactly three errors,
635        // no cascade from recovery. (Single-word atoms are NOT errors anymore —
636        // they are bare propositions — so each broken line is broken for a real
637        // reason: a non-statement line, an unquoted IMPORT path, and trailing text.)
638        let src = "!nope\nFACT a b\nIMPORT nothx\nNOT a b c d\n";
639        let diags = parse(src).expect_err("should fail");
640        assert_eq!(diags.len(), 3);
641    }
642
643    #[test]
644    fn crlf_line_endings() {
645        let p = prog(
646            r#"
647        FACT a b
648        CHECK a
649        "#,
650        );
651        assert_eq!(p.statements.len(), 2);
652    }
653
654    #[test]
655    fn tabs_as_indentation() {
656        let p = prog(
657            r#"
658        PREMISE e:
659	EXCLUSIVE
660		x a
661		x b
662        "#,
663        );
664        assert!(matches!(
665            p.statements[0],
666            Statement::Premise {
667                body: Body::List {
668                    op: ListOp::Exclusive,
669                    ..
670                },
671                ..
672            }
673        ));
674    }
675
676    #[test]
677    fn parses_all_list_ops() {
678        for (kw, want) in [
679            ("EXCLUSIVE", ListOp::Exclusive),
680            ("FORBIDS", ListOp::Forbids),
681            ("ONEOF", ListOp::OneOf),
682            ("ATLEAST", ListOp::AtLeast),
683        ] {
684            let src = alloc::format!("PREMISE a:\n    {kw}\n        x a\n        x b\n");
685            match &prog(&src).statements[0] {
686                Statement::Premise {
687                    body: Body::List { op, .. },
688                    ..
689                } => assert_eq!(*op, want),
690                other => panic!("{kw}: unexpected {other:?}"),
691            }
692        }
693    }
694
695    #[test]
696    fn check_bidirectional_without_subject() {
697        match &prog("CHECK BIDIRECTIONAL\n").statements[0] {
698            Statement::Check {
699                subject,
700                bidirectional,
701            } => {
702                assert!(subject.is_none());
703                assert!(bidirectional);
704            }
705            other => panic!("unexpected {other:?}"),
706        }
707    }
708
709    #[test]
710    fn empty_and_comment_only_input_yield_no_statements() {
711        assert_eq!(prog("").statements.len(), 0);
712        assert_eq!(prog("// just a comment\n\n   \n").statements.len(), 0);
713    }
714
715    #[test]
716    fn negation_with_object() {
717        match &prog("NOT Creature_A has wing\n").statements[0] {
718            Statement::Negation(a) => {
719                assert_eq!(a.data.subject, "Creature_A");
720                assert_eq!(a.data.object, Some("wing"));
721            }
722            other => panic!("unexpected {other:?}"),
723        }
724    }
725
726    #[test]
727    fn negated_consequent_then_not() {
728        let src = r#"
729        PREMISE a:
730            WHEN x on
731            THEN NOT x off
732        "#;
733        match &prog(src).statements[0] {
734            Statement::Premise {
735                body: Body::Impl { consequent, .. },
736                ..
737            } => {
738                assert!(consequent[0].data.negated);
739                assert_eq!(consequent[0].data.atom.predicate, Some("off"));
740            }
741            other => panic!("unexpected {other:?}"),
742        }
743    }
744
745    #[test]
746    fn multiple_imports_then_facts() {
747        let p = prog(
748            r#"
749        IMPORT "a.vrf"
750        IMPORT "b.vrf"
751        FACT x y
752        "#,
753        );
754        assert!(matches!(p.statements[0], Statement::Import { .. }));
755        assert!(matches!(p.statements[1], Statement::Import { .. }));
756        assert!(matches!(p.statements[2], Statement::Fact(_)));
757    }
758
759    #[test]
760    fn trailing_comment_without_final_newline() {
761        let p = prog("FACT a b\n// trailing, no newline");
762        assert_eq!(p.statements.len(), 1);
763    }
764
765    #[test]
766    fn set_declaration_parses() {
767        let p = prog(
768            r"
769        SET tasks
770            deploy
771            backup
772        ",
773        );
774        match &p.statements[0] {
775            Statement::Set { name, elements } => {
776                assert_eq!(name.data, "tasks");
777                let got: Vec<&str> = elements.iter().map(|e| e.data).collect();
778                assert_eq!(got, ["deploy", "backup"]);
779            }
780            other => panic!("expected a SET, got {other:?}"),
781        }
782    }
783
784    #[test]
785    fn close_statement_parses() {
786        let p = prog("CLOSE depends_on TRANSITIVE\n");
787        match &p.statements[0] {
788            Statement::Close { relation, kind } => {
789                assert_eq!(relation.data, "depends_on");
790                assert_eq!(*kind, CloseKind::Transitive);
791            }
792            other => panic!("expected a CLOSE, got {other:?}"),
793        }
794    }
795
796    #[test]
797    fn for_each_header_parses_into_a_quant() {
798        let p = prog(
799            r"
800        PREMISE p FOR EACH t IN tasks:
801            ONEOF
802                t s a
803                t s b
804        ",
805        );
806        match &p.statements[0] {
807            Statement::Premise {
808                quant: Some(Quant::InSet { binder, set }),
809                ..
810            } => {
811                assert_eq!(binder.data, "t");
812                assert_eq!(set.data, "tasks");
813            }
814            other => panic!("expected a quantified premise, got {other:?}"),
815        }
816    }
817
818    #[test]
819    fn for_each_relation_header_parses_into_a_quant() {
820        let p = prog(
821            r"
822        PREMISE p FOR EACH x linked y:
823            FORBIDS
824                x a
825                y a
826        ",
827        );
828        match &p.statements[0] {
829            Statement::Premise {
830                quant:
831                    Some(Quant::Relation {
832                        left,
833                        predicate,
834                        right,
835                    }),
836                ..
837            } => {
838                assert_eq!(left.data, "x");
839                assert_eq!(predicate.data, "linked");
840                assert_eq!(right.data, "y");
841            }
842            other => panic!("expected a relation-quantified premise, got {other:?}"),
843        }
844    }
845
846    #[test]
847    fn an_unquantified_premise_has_no_quant() {
848        let p = prog(
849            r"
850        PREMISE p:
851            ONEOF
852                x s a
853                x s b
854        ",
855        );
856        assert!(matches!(
857            &p.statements[0],
858            Statement::Premise { quant: None, .. }
859        ));
860    }
861
862    #[test]
863    fn a_malformed_for_each_is_a_committed_error() {
864        // FOR without EACH commits (FOR is reserved, only a quantifier here).
865        assert!(
866            parse(
867                r"
868        PREMISE p FOR t IN tasks:
869            ONEOF
870                t s a
871                t s b
872        "
873            )
874            .is_err()
875        );
876    }
877}