lemma-engine 0.8.12

A language that means business.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

//! Adversarial: dependency cycles must surface as errors, never panic during
//! `validate_dependency_interfaces` (missing `SpecSetPlanningResult` for a dep name).

use lemma::{Engine, Error, SourceType};

#[test]
fn cross_spec_data_reference_cycle_surfaces_error_not_panic() {
    let mut engine = Engine::new();
    let err = engine
        .load(
            r#"
spec a
data x: number from b

spec b
data x: number from a
"#,
            SourceType::Labeled("cycle.lemma"),
        )
        .expect_err("cross-spec data cycle must fail load");

    let joined = err
        .errors
        .iter()
        .map(|e| e.to_string())
        .collect::<Vec<_>>()
        .join(" ");
    assert!(
        joined.to_lowercase().contains("cycle") || joined.to_lowercase().contains("circular"),
        "expected cycle wording, got: {joined}"
    );
}

#[test]
fn third_spec_depending_on_cyclic_pair_gets_error_not_panic() {
    let mut engine = Engine::new();
    let err = engine
        .load(
            r#"
spec a
data x: number from b

spec b
data x: number from a

spec c 2025-01-01
data y: number from b
rule r: y
"#,
            SourceType::Labeled("cycle2.lemma"),
        )
        .expect_err("must fail");

    let joined = err
        .errors
        .iter()
        .map(|e| e.to_string())
        .collect::<Vec<_>>()
        .join(" ");
    assert!(
        joined.to_lowercase().contains("cycle") || joined.to_lowercase().contains("circular"),
        "expected cycle in errors: {joined}"
    );
}

#[test]
fn rule_only_cycle_still_errors_without_panic() {
    let mut engine = Engine::new();
    let err = engine
        .load(
            r#"
spec t
rule x: y
rule y: x
"#,
            SourceType::Labeled("rule_cycle.lemma"),
        )
        .expect_err("rule cycle");

    assert!(err.errors.iter().any(|e| matches!(e, Error::Validation(_))));
}