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 { 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 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); }
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 assert_eq!(atom_shapes(&prog(flat)), atom_shapes(&prog(indented)));
509 }
510
511 #[test]
512 fn top_level_statements_may_be_indented() {
513 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 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 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 assert!(parse("FACT 2cats has fur\n").is_err());
602 }
603
604 #[test]
605 fn punctuation_is_rejected_in_identifier() {
606 assert!(parse("FACT cat! has fur\n").is_err());
608 }
609
610 #[test]
611 fn reserved_word_cannot_be_identifier() {
612 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 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 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 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}