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 { atom, value } => {
173                assert_eq!(atom.data.subject, "db_ready");
174                assert_eq!(atom.data.predicate, None);
175                assert!(*value);
176            }
177            other => panic!("expected provide, got {:?}", other),
178        }
179        match &p.statements[1] {
180            Statement::Provide { value, .. } => assert!(!*value),
181            other => panic!("expected provide, got {:?}", other),
182        }
183    }
184
185    #[test]
186    fn parses_assume_positive_and_negated() {
187        let p = prog(
188            r#"
189        ASSUME rel in_prod
190        ASSUME NOT rel has_rollback
191        "#,
192        );
193        assert_eq!(p.statements.len(), 2);
194        match &p.statements[0] {
195            Statement::Assume(l) => {
196                assert!(!l.data.negated);
197                assert_eq!(l.data.atom.subject, "rel");
198                assert_eq!(l.data.atom.predicate, Some("in_prod"));
199                assert_eq!(l.data.atom.object, None);
200            }
201            other => panic!("expected assume, got {:?}", other),
202        }
203        match &p.statements[1] {
204            Statement::Assume(l) => {
205                assert!(l.data.negated);
206                assert_eq!(l.data.atom.predicate, Some("has_rollback"));
207            }
208            other => panic!("expected negated assume, got {:?}", other),
209        }
210    }
211
212    #[test]
213    fn assume_is_a_reserved_word() {
214        assert!(parse("FACT ASSUME has x\n").is_err());
215    }
216
217    #[test]
218    fn parses_import() {
219        let p = prog("IMPORT \"physics.vrf\"\n");
220        match &p.statements[0] {
221            Statement::Import { path, alias } => {
222                assert_eq!(path.data, "physics.vrf");
223                assert!(alias.is_none());
224            }
225            other => panic!("expected import, got {:?}", other),
226        }
227    }
228
229    #[test]
230    fn parses_import_with_alias() {
231        let p = prog("IMPORT \"physics.vrf\" AS phys\n");
232        match &p.statements[0] {
233            Statement::Import { path, alias } => {
234                assert_eq!(path.data, "physics.vrf");
235                assert_eq!(alias.as_ref().unwrap().data, "phys");
236            }
237            other => panic!("expected import, got {:?}", other),
238        }
239    }
240
241    #[test]
242    fn parses_domain_declaration() {
243        let p = prog("DOMAIN physics\n");
244        match &p.statements[0] {
245            Statement::Domain(name) => assert_eq!(name.data, "physics"),
246            other => panic!("expected domain, got {:?}", other),
247        }
248    }
249
250    #[test]
251    fn parses_domain_qualified_atom() {
252        // `physics.Motor over_200` → domain prefix split from the subject.
253        let p = prog("FACT physics.Motor over_200\n");
254        match &p.statements[0] {
255            Statement::Fact(a) => {
256                assert_eq!(a.data.domain, Some("physics"));
257                assert_eq!(a.data.subject, "Motor");
258                assert_eq!(a.data.predicate, Some("over_200"));
259            }
260            other => panic!("expected fact, got {:?}", other),
261        }
262    }
263
264    #[test]
265    fn bare_atom_has_no_domain() {
266        let p = prog("FACT engine has_fuel\n");
267        match &p.statements[0] {
268            Statement::Fact(a) => {
269                assert_eq!(a.data.domain, None);
270                assert_eq!(a.data.subject, "engine");
271            }
272            other => panic!("expected fact, got {:?}", other),
273        }
274    }
275
276    #[test]
277    fn domain_is_a_reserved_word() {
278        assert!(parse("FACT DOMAIN has x\n").is_err());
279        assert!(parse("FACT AS has x\n").is_err());
280    }
281
282    #[test]
283    fn parses_exclusive_premise() {
284        let src = r#"
285        PREMISE fly_xor_swim:
286            EXCLUSIVE
287                Creature_A has flying
288                Creature_A has swimming
289        "#;
290        let p = prog(src);
291        match &p.statements[0] {
292            Statement::Premise { name, body, .. } => {
293                assert_eq!(name.data, "fly_xor_swim");
294                match body {
295                    Body::List { op, atoms } => {
296                        assert_eq!(*op, ListOp::Exclusive);
297                        assert_eq!(atoms.len(), 2);
298                        assert_eq!(atoms[1].data.object, Some("swimming"));
299                    }
300                    other => panic!("expected list body, got {:?}", other),
301                }
302            }
303            other => panic!("expected premise, got {:?}", other),
304        }
305    }
306
307    #[test]
308    fn parses_implication_premise_with_and() {
309        let src = r#"
310        PREMISE wings_need_bone:
311            WHEN Creature_A has flying
312            THEN Creature_A has wing
313            AND  Creature_A has bone
314        "#;
315        let p = prog(src);
316        match &p.statements[0] {
317            Statement::Premise {
318                body:
319                    Body::Impl {
320                        antecedent,
321                        consequent,
322                        ..
323                    },
324                ..
325            } => {
326                assert_eq!(antecedent.len(), 1);
327                assert_eq!(antecedent[0].data.atom.object, Some("flying"));
328                assert_eq!(consequent.len(), 2);
329                assert_eq!(consequent[0].data.atom.object, Some("wing"));
330                assert_eq!(consequent[1].data.atom.object, Some("bone"));
331            }
332            other => panic!("expected impl premise, got {:?}", other),
333        }
334    }
335
336    #[test]
337    fn antecedent_and_goes_before_then() {
338        let src = r#"
339        PREMISE deploy:
340            WHEN s tested
341            AND s reviewed
342            THEN s can_deploy
343        "#;
344        let p = prog(src);
345        match &p.statements[0] {
346            Statement::Premise {
347                body:
348                    Body::Impl {
349                        antecedent,
350                        consequent,
351                        ..
352                    },
353                ..
354            } => {
355                assert_eq!(antecedent.len(), 2);
356                assert_eq!(consequent.len(), 1);
357            }
358            other => panic!("unexpected: {:?}", other),
359        }
360    }
361
362    #[test]
363    fn when_or_sets_disjunctive_antecedent() {
364        let src = r#"
365        PREMISE p:
366            WHEN x a
367            OR x b
368            THEN x c
369        "#;
370        match &prog(src).statements[0] {
371            Statement::Premise {
372                body:
373                    Body::Impl {
374                        antecedent,
375                        ante_conn,
376                        consequent,
377                        cons_conn,
378                    },
379                ..
380            } => {
381                assert_eq!(antecedent.len(), 2);
382                assert_eq!(*ante_conn, Conn::Or);
383                assert_eq!(consequent.len(), 1);
384                assert_eq!(*cons_conn, Conn::And); // single consequent → AND
385            }
386            other => panic!("expected impl premise, got {:?}", other),
387        }
388    }
389
390    #[test]
391    fn then_or_sets_disjunctive_consequent() {
392        let src = r#"
393        PREMISE p:
394            WHEN x a
395            THEN x b
396            OR x c
397        "#;
398        match &prog(src).statements[0] {
399            Statement::Premise {
400                body:
401                    Body::Impl {
402                        consequent,
403                        cons_conn,
404                        ..
405                    },
406                ..
407            } => {
408                assert_eq!(consequent.len(), 2);
409                assert_eq!(*cons_conn, Conn::Or);
410            }
411            other => panic!("expected impl premise, got {:?}", other),
412        }
413    }
414
415    #[test]
416    fn mixing_and_or_in_one_group_is_an_error() {
417        let mixed_when = r#"
418        PREMISE p:
419            WHEN x a
420            AND x b
421            OR x c
422            THEN x d
423        "#;
424        let mixed_then = r#"
425        PREMISE p:
426            WHEN x a
427            THEN x b
428            AND x c
429            OR x d
430        "#;
431        assert!(parse(mixed_when).is_err());
432        assert!(parse(mixed_then).is_err());
433    }
434
435    #[test]
436    fn or_is_a_reserved_word() {
437        assert!(parse("FACT OR has x\n").is_err());
438    }
439
440    #[test]
441    fn parses_negated_literal_in_rule() {
442        let src = r#"
443        RULE pick_slow:
444            WHEN NOT Motor over_100
445            THEN Motor uses slow_path
446        "#;
447        let p = prog(src);
448        match &p.statements[0] {
449            Statement::Rule {
450                body: Body::Impl { antecedent, .. },
451                ..
452            } => {
453                assert!(antecedent[0].data.negated);
454                assert_eq!(antecedent[0].data.atom.predicate, Some("over_100"));
455            }
456            other => panic!("expected rule, got {:?}", other),
457        }
458    }
459
460    #[test]
461    fn parses_check_variants() {
462        let p = prog("CHECK Creature_A BIDIRECTIONAL\n");
463        match &p.statements[0] {
464            Statement::Check {
465                subject,
466                bidirectional,
467            } => {
468                assert_eq!(subject.as_ref().unwrap().data, "Creature_A");
469                assert!(bidirectional);
470            }
471            other => panic!("expected check, got {:?}", other),
472        }
473
474        let p = prog("CHECK\n");
475        match &p.statements[0] {
476            Statement::Check {
477                subject,
478                bidirectional,
479            } => {
480                assert!(subject.is_none());
481                assert!(!bidirectional);
482            }
483            other => panic!("expected check, got {:?}", other),
484        }
485    }
486
487    #[test]
488    fn comments_and_blanks_are_ignored() {
489        let src = "// header\n\nFACT a b   // trailing comment\n\n// tail\n";
490        let p = prog(src);
491        assert_eq!(p.statements.len(), 1);
492    }
493
494    #[test]
495    fn indentation_is_cosmetic() {
496        let flat = r#"
497        PREMISE x:
498        EXCLUSIVE
499        a b
500        a c
501        "#;
502        let indented = r#"
503        PREMISE x:
504                EXCLUSIVE
505          a b
506                    a c
507        "#;
508        // Spans differ by offset (cosmetic); the parsed structure must be identical.
509        assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
510    }
511
512    #[test]
513    fn top_level_statements_may_be_indented() {
514        // Leading indentation on the FACT/PREMISE/CHECK lines themselves is also
515        // cosmetic (so a whole program can be pasted indented inside a here-doc).
516        let flat = r#"
517        FACT x a
518        NOT x b
519        CHECK x
520        "#;
521        let indented = r#"
522            FACT x a
523                NOT x b
524            CHECK x
525        "#;
526        assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
527        assert_eq!(prog(indented).statements.len(), 3);
528    }
529
530    #[test]
531    fn full_creature_example_parses() {
532        let src = include_str!("../../../docs/examples/creature.vrf");
533        let p = prog(src);
534        // 1 DOMAIN + 2 FACT + 3 PREMISE + 1 RULE + 1 CHECK = 8
535        assert_eq!(p.statements.len(), 8);
536    }
537
538    #[test]
539    fn import_demo_example_parses() {
540        let src = include_str!("../../../docs/examples/import-demo.vrf");
541        let p = prog(src);
542        assert!(matches!(p.statements[0], Statement::Domain(_)));
543        assert!(matches!(p.statements[1], Statement::Import { .. }));
544    }
545
546    #[test]
547    fn unicode_identifiers_any_script() {
548        // Cyrillic subject/predicate/object, mixed with `_` and digits (not first).
549        let p = prog(
550            r#"
551        FACT кот пушистый2
552        NOT собака has крылья
553        "#,
554        );
555        match &p.statements[0] {
556            Statement::Fact(a) => {
557                assert_eq!(a.data.subject, "кот");
558                assert_eq!(a.data.predicate, Some("пушистый2"));
559                assert_eq!(a.data.object, None);
560            }
561            other => panic!("expected fact, got {:?}", other),
562        }
563        match &p.statements[1] {
564            Statement::Negation(a) => {
565                assert_eq!(a.data.subject, "собака");
566                assert_eq!(a.data.object, Some("крылья"));
567            }
568            other => panic!("expected negation, got {:?}", other),
569        }
570    }
571
572    #[test]
573    fn unicode_premise_name_and_body() {
574        let src = r#"
575        PREMISE правило_лая:
576            WHEN собака has хвост
577            THEN собака умеет_лаять
578        "#;
579        match &prog(src).statements[0] {
580            Statement::Premise { name, body, .. } => {
581                assert_eq!(name.data, "правило_лая");
582                match body {
583                    Body::Impl {
584                        antecedent,
585                        consequent,
586                        ..
587                    } => {
588                        assert_eq!(antecedent[0].data.atom.subject, "собака");
589                        assert_eq!(consequent[0].data.atom.subject, "собака");
590                        assert_eq!(consequent[0].data.atom.predicate, Some("умеет_лаять"));
591                    }
592                    other => panic!("expected impl body, got {:?}", other),
593                }
594            }
595            other => panic!("expected premise, got {:?}", other),
596        }
597    }
598
599    #[test]
600    fn identifier_cannot_start_with_digit() {
601        // `2cats` is not a valid subject — first char must be a letter.
602        assert!(parse("FACT 2cats has fur\n").is_err());
603    }
604
605    #[test]
606    fn punctuation_is_rejected_in_identifier() {
607        // `!` and other symbols are not identifier characters.
608        assert!(parse("FACT cat! has fur\n").is_err());
609    }
610
611    #[test]
612    fn reserved_word_cannot_be_identifier() {
613        // `WHEN` as a subject is illegal.
614        assert!(parse("FACT WHEN has x\n").is_err());
615    }
616
617    #[test]
618    fn pretty_error_points_at_offending_line() {
619        let src = r#"FACT a b
620!garbage here
621FACT c d
622"#;
623        let err = parse(src).expect_err("should fail");
624        let shown = format!("{}", err);
625        // The new diagnostic format: a RESULT header, the line number, the
626        // verbatim offending line, and a caret pointing at it.
627        assert!(shown.contains("RESULT: 1 syntax error"));
628        assert!(shown.contains("line 2"));
629        assert!(shown.contains("!garbage here"));
630        assert!(shown.contains('^'));
631    }
632
633    #[test]
634    fn collects_every_error_in_one_pass() {
635        // Three broken top-level lines among valid ones → exactly three errors,
636        // no cascade from recovery. (Single-word atoms are NOT errors anymore —
637        // they are bare propositions — so each broken line is broken for a real
638        // reason: a non-statement line, an unquoted IMPORT path, and trailing text.)
639        let src = "!nope\nFACT a b\nIMPORT nothx\nNOT a b c d\n";
640        let diags = parse(src).expect_err("should fail");
641        assert_eq!(diags.len(), 3);
642    }
643
644    #[test]
645    fn crlf_line_endings() {
646        let p = prog(
647            r#"
648        FACT a b
649        CHECK a
650        "#,
651        );
652        assert_eq!(p.statements.len(), 2);
653    }
654
655    #[test]
656    fn tabs_as_indentation() {
657        let p = prog(
658            r#"
659        PREMISE e:
660	EXCLUSIVE
661		x a
662		x b
663        "#,
664        );
665        assert!(matches!(
666            p.statements[0],
667            Statement::Premise {
668                body: Body::List {
669                    op: ListOp::Exclusive,
670                    ..
671                },
672                ..
673            }
674        ));
675    }
676
677    #[test]
678    fn parses_all_list_ops() {
679        for (kw, want) in [
680            ("EXCLUSIVE", ListOp::Exclusive),
681            ("FORBIDS", ListOp::Forbids),
682            ("ONEOF", ListOp::OneOf),
683            ("ATLEAST", ListOp::AtLeast),
684        ] {
685            let src = alloc::format!("PREMISE a:\n    {kw}\n        x a\n        x b\n");
686            match &prog(&src).statements[0] {
687                Statement::Premise {
688                    body: Body::List { op, .. },
689                    ..
690                } => assert_eq!(*op, want),
691                other => panic!("{kw}: unexpected {other:?}"),
692            }
693        }
694    }
695
696    #[test]
697    fn check_bidirectional_without_subject() {
698        match &prog("CHECK BIDIRECTIONAL\n").statements[0] {
699            Statement::Check {
700                subject,
701                bidirectional,
702            } => {
703                assert!(subject.is_none());
704                assert!(bidirectional);
705            }
706            other => panic!("unexpected {other:?}"),
707        }
708    }
709
710    #[test]
711    fn empty_and_comment_only_input_yield_no_statements() {
712        assert_eq!(prog("").statements.len(), 0);
713        assert_eq!(prog("// just a comment\n\n   \n").statements.len(), 0);
714    }
715
716    #[test]
717    fn negation_with_object() {
718        match &prog("NOT Creature_A has wing\n").statements[0] {
719            Statement::Negation(a) => {
720                assert_eq!(a.data.subject, "Creature_A");
721                assert_eq!(a.data.object, Some("wing"));
722            }
723            other => panic!("unexpected {other:?}"),
724        }
725    }
726
727    #[test]
728    fn negated_consequent_then_not() {
729        let src = r#"
730        PREMISE a:
731            WHEN x on
732            THEN NOT x off
733        "#;
734        match &prog(src).statements[0] {
735            Statement::Premise {
736                body: Body::Impl { consequent, .. },
737                ..
738            } => {
739                assert!(consequent[0].data.negated);
740                assert_eq!(consequent[0].data.atom.predicate, Some("off"));
741            }
742            other => panic!("unexpected {other:?}"),
743        }
744    }
745
746    #[test]
747    fn multiple_imports_then_facts() {
748        let p = prog(
749            r#"
750        IMPORT "a.vrf"
751        IMPORT "b.vrf"
752        FACT x y
753        "#,
754        );
755        assert!(matches!(p.statements[0], Statement::Import { .. }));
756        assert!(matches!(p.statements[1], Statement::Import { .. }));
757        assert!(matches!(p.statements[2], Statement::Fact(_)));
758    }
759
760    #[test]
761    fn trailing_comment_without_final_newline() {
762        let p = prog("FACT a b\n// trailing, no newline");
763        assert_eq!(p.statements.len(), 1);
764    }
765
766    #[test]
767    fn set_declaration_parses() {
768        let p = prog(
769            r"
770        SET tasks
771            deploy
772            backup
773        ",
774        );
775        match &p.statements[0] {
776            Statement::Set { name, elements } => {
777                assert_eq!(name.data, "tasks");
778                let got: Vec<&str> = elements.iter().map(|e| e.data).collect();
779                assert_eq!(got, ["deploy", "backup"]);
780            }
781            other => panic!("expected a SET, got {other:?}"),
782        }
783    }
784
785    #[test]
786    fn close_statement_parses() {
787        let p = prog("CLOSE depends_on TRANSITIVE\n");
788        match &p.statements[0] {
789            Statement::Close { relation, kind } => {
790                assert_eq!(relation.data, "depends_on");
791                assert_eq!(*kind, CloseKind::Transitive);
792            }
793            other => panic!("expected a CLOSE, got {other:?}"),
794        }
795    }
796
797    #[test]
798    fn for_each_header_parses_into_a_quant() {
799        let p = prog(
800            r"
801        PREMISE p FOR EACH t IN tasks:
802            ONEOF
803                t s a
804                t s b
805        ",
806        );
807        match &p.statements[0] {
808            Statement::Premise {
809                quant: Some(Quant::InSet { binder, set }),
810                ..
811            } => {
812                assert_eq!(binder.data, "t");
813                assert_eq!(set.data, "tasks");
814            }
815            other => panic!("expected a quantified premise, got {other:?}"),
816        }
817    }
818
819    #[test]
820    fn for_each_relation_header_parses_into_a_quant() {
821        let p = prog(
822            r"
823        PREMISE p FOR EACH x linked y:
824            FORBIDS
825                x a
826                y a
827        ",
828        );
829        match &p.statements[0] {
830            Statement::Premise {
831                quant:
832                    Some(Quant::Relation {
833                        left,
834                        predicate,
835                        right,
836                    }),
837                ..
838            } => {
839                assert_eq!(left.data, "x");
840                assert_eq!(predicate.data, "linked");
841                assert_eq!(right.data, "y");
842            }
843            other => panic!("expected a relation-quantified premise, got {other:?}"),
844        }
845    }
846
847    #[test]
848    fn an_unquantified_premise_has_no_quant() {
849        let p = prog(
850            r"
851        PREMISE p:
852            ONEOF
853                x s a
854                x s b
855        ",
856        );
857        assert!(matches!(
858            &p.statements[0],
859            Statement::Premise { quant: None, .. }
860        ));
861    }
862
863    #[test]
864    fn a_malformed_for_each_is_a_committed_error() {
865        // FOR without EACH commits (FOR is reserved, only a quantifier here).
866        assert!(
867            parse(
868                r"
869        PREMISE p FOR t IN tasks:
870            ONEOF
871                t s a
872                t s b
873        "
874            )
875            .is_err()
876        );
877    }
878}