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

use crate::engine::Engine;
use crate::SourceType;

#[test]
fn invalid_parent_type_in_type_definition_should_be_rejected() {
    let mut engine = Engine::new();
    let code = r#"
spec test
data invalid: nonexistent -> minimum 0
data value: invalid
rule result: value
"#;

    let result = engine.load(code, SourceType::Labeled("test.lemma"));
    assert!(result.is_err(), "Engine should reject invalid parent types");

    let load_err = result.unwrap_err();
    assert!(!load_err.errors.is_empty(), "expected at least one error");
    let msg = load_err.errors[0].to_string();
    assert!(
        msg.contains("Unknown type: 'nonexistent'"),
        "Error should mention unknown type. Got: {}",
        msg
    );
}

#[test]
fn unknown_type_used_in_data_type_declaration_should_be_rejected() {
    let mut engine = Engine::new();
    let code = r#"
spec test
data value: invalid_parent_type
rule result: value
"#;

    let result = engine.load(code, SourceType::Labeled("test.lemma"));
    assert!(
        result.is_err(),
        "Engine should reject unknown types used in type declarations"
    );

    let load_err = result.unwrap_err();
    assert!(!load_err.errors.is_empty(), "expected at least one error");
    let msg = load_err.errors[0].to_string();
    assert!(
        msg.contains("Unknown type: 'invalid_parent_type'"),
        "Error should mention unknown type. Got: {}",
        msg
    );
}

#[test]
fn duplicate_spec_names_should_be_rejected() {
    let mut engine = Engine::new();
    let code = r#"
spec test
data x: 1

spec test
data x: 2
"#;

    let result = engine.load(code, SourceType::Labeled("test.lemma"));
    assert!(
        result.is_err(),
        "Duplicate spec names should be rejected (no silent overwrites)"
    );
    let load_err = result.unwrap_err();
    assert!(!load_err.errors.is_empty(), "expected at least one error");
    let msg = load_err.errors[0].to_string();
    assert!(
        msg.contains("Duplicate spec") && msg.contains("test"),
        "Error should mention the duplicate spec name. Got: {}",
        msg
    );
}