1#![no_std]
34#![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 type AtomShape<'a> = (&'a str, Option<&'a str>, Option<&'a str>);
63 type ListShape<'a> = (ListOp, Vec<AtomShape<'a>>);
65
66 use alloc::vec::Vec;
67
68 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 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 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); }
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 assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
510 }
511
512 #[test]
513 fn top_level_statements_may_be_indented() {
514 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 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 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 assert!(parse("FACT 2cats has fur\n").is_err());
603 }
604
605 #[test]
606 fn punctuation_is_rejected_in_identifier() {
607 assert!(parse("FACT cat! has fur\n").is_err());
609 }
610
611 #[test]
612 fn reserved_word_cannot_be_identifier() {
613 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 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 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 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}