lemma-engine 0.8.19

/// Integration tests for `with` bindings (import-path LHS) and local-with rejection.
use lemma::DateTimeValue;
use lemma::Engine;
use std::collections::HashMap;

fn rule_value(result: &lemma::Response, rule_name: &str) -> String {
    let rr = result
        .results
        .get(rule_name)
        .unwrap_or_else(|| panic!("rule '{}' not found", rule_name));
    if rr.vetoed {
        return format!("VETO({})", rr.veto_reason.as_deref().unwrap_or("Vetoed"));
    }
    rr.display.clone().expect("display")
}

fn load_err_joined(engine_res: Result<(), lemma::Errors>) -> String {
    let err = engine_res.expect_err("expected load to fail");
    err.iter()
        .map(|e| e.to_string())
        .collect::<Vec<_>>()
        .join("\n")
}

#[test]
fn local_fill_literal_rejected_at_parse() {
    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        r#"spec s
with x: 42"#,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));
    assert!(
        joined.contains("imported spec") || joined.contains("alias.field"),
        "local with must be rejected at parse, got: {joined}"
    );
}

#[test]
fn local_fill_import_reference_rejected_at_parse() {
    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        r#"spec inner
data v: number

spec outer
uses i: inner
with copy: i.v"#,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));
    assert!(
        joined.contains("imported spec") || joined.contains("alias.field"),
        "local with must be rejected at parse, got: {joined}"
    );
}

#[test]
fn binding_reference_copies_cross_spec_target_value() {
    let code = r#"
spec law
data other: number -> default 99

spec inner
uses l: law
data slot: number

spec top
uses lic: inner
uses lw: law
with lic.slot: lw.other
rule answer: lic.slot
"#;

    let mut engine = Engine::new();
    engine
        .load(
            code,
            lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
                "reference.lemma",
            ))),
        )
        .unwrap();

    let now = DateTimeValue::now();
    let result = engine
        .run(None, "top", Some(&now), HashMap::new(), false, None)
        .expect("should run");

    assert_eq!(rule_value(&result, "answer"), "99");
}

#[test]
fn closed_reference_cycle_is_rejected() {
    let code = r#"
spec inner
data a: number
data b: number

spec outer
uses i: inner
with i.a: i.b
with i.b: i.a
"#;

    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));

    assert!(
        joined.contains("Circular data reference"),
        "closed reference cycle must be reported as a circular data reference, got: {joined}"
    );
}

#[test]
fn self_referential_binding_reference_is_rejected() {
    let code = r#"
spec inner
data x: number

spec outer
uses i: inner
with i.x: i.x
"#;

    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));

    assert!(
        joined.contains("Circular data reference"),
        "self-referential binding reference must be reported as a circular data reference, got: {joined}"
    );
}

#[test]
fn binding_reference_target_type_incompatible_with_child_declared_type_is_rejected() {
    let code = r#"
spec inner
data n: number

spec source_spec
data s: text -> default "hello"

spec outer
uses i: inner
uses src: source_spec
with i.n: src.s
rule r: i.n
"#;

    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));

    assert!(
        joined.contains("type mismatch"),
        "binding reference with target of a different base kind must be rejected, got: {joined}"
    );
}

#[test]
fn rule_target_binding_reference_cycle_through_self_is_rejected() {
    let code = r#"
spec inner
data slot: number

spec outer
uses i: inner
with i.slot: r
rule r: i.slot
"#;

    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));

    assert!(
        joined.to_lowercase().contains("circular") || joined.to_lowercase().contains("cycle"),
        "rule-target binding forming a cycle must be rejected, got: {joined}"
    );
}

#[test]
fn rule_target_binding_reference_lhs_type_mismatch_is_rejected() {
    let code = r#"
spec inner
data v: number

spec source_spec
rule greeting: "hello"

spec outer
uses i: inner
uses src: source_spec
with i.v: src.greeting
rule r: i.v
"#;

    let mut engine = Engine::new();
    let joined = load_err_joined(engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    ));

    assert!(
        joined.contains("type mismatch"),
        "rule-target binding with type kind mismatch must be rejected, got: {joined}"
    );
}

#[test]
fn reference_value_violating_child_declared_max_is_rejected() {
    let code = r#"
spec inner
data limited: number -> maximum 5

spec source_spec
data v: number -> default 10

spec outer
uses i: inner
uses src: source_spec
with i.limited: src.v
rule r: i.limited
"#;

    let mut engine = Engine::new();
    let load_result = engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    );

    match load_result {
        Ok(()) => {
            let now = DateTimeValue::now();
            let run_result = engine.run(None, "outer", Some(&now), HashMap::new(), false, None);

            match run_result {
                Ok(resp) => {
                    let rr = resp.results.get("r").expect("rule 'r'");
                    if rr.vetoed {
                        let s = rr.veto_reason.as_deref().expect("veto reason");
                        assert!(
                            s.contains("maximum") || s.contains("exceeds"),
                            "expected max-constraint veto, got: {s}"
                        );
                    } else {
                        panic!("expected constraint-violation veto; got {:?}", rr.display);
                    }
                }
                Err(err) => {
                    let s = err.to_string();
                    assert!(
                        s.contains("maximum") || s.contains("exceeds") || s.contains("constraint"),
                        "expected constraint error at run time, got: {s}"
                    );
                }
            }
        }
        Err(errors) => {
            let joined = errors
                .iter()
                .map(|e| e.to_string())
                .collect::<Vec<_>>()
                .join("\n");
            assert!(
                joined.contains("maximum")
                    || joined.contains("exceeds")
                    || joined.contains("constraint"),
                "expected constraint error at load time, got: {joined}"
            );
        }
    }
}

#[test]
fn local_non_dotted_rhs_stays_definition() {
    let code = r#"
spec s
data age: number -> default 30
data person: age
rule r: person
"#;

    let mut engine = Engine::new();
    engine
        .load(
            code,
            lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
                "reference.lemma",
            ))),
        )
        .expect("loads: `data person: age` is a typedef reference, not a value-copy reference");

    let now = DateTimeValue::now();
    let result = engine
        .run(None, "s", Some(&now), HashMap::new(), false, None)
        .expect("evaluates; `person` is typed 'age' and inherits its default");

    assert_eq!(rule_value(&result, "r"), "30");
}

#[test]
fn binding_non_dotted_rhs_resolves_in_enclosing_spec() {
    let code = r#"
spec inner
data slot: number

spec outer
uses i: inner
data src: number -> default 123
with i.slot: src
rule r: i.slot
"#;

    let mut engine = Engine::new();
    engine
        .load(
            code,
            lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
                "reference.lemma",
            ))),
        )
        .expect("non-dotted RHS in binding context must resolve in the enclosing spec");

    let now = DateTimeValue::now();
    let result = engine
        .run(None, "outer", Some(&now), HashMap::new(), false, None)
        .expect("evaluates");
    assert_eq!(rule_value(&result, "r"), "123");
}

#[test]
fn binding_reference_quantity_family_mismatch_is_rejected() {
    let code = r#"
spec inner
data money: quantity -> unit eur 1.00
data payment: money

spec source_spec
data temp_unit: quantity -> unit celsius 1.0
data temperature: temp_unit

spec outer
uses i: inner
uses src: source_spec
with i.payment: src.temperature
rule r: i.payment
"#;

    let mut engine = Engine::new();
    let res = engine.load(
        code,
        lemma::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
            "reference.lemma",
        ))),
    );
    let joined = load_err_joined(res);
    assert!(
        joined.contains("quantity family")
            || joined.contains("quantity_family")
            || joined.contains("family")
            || joined.contains("type mismatch"),
        "expected quantity-family-mismatch error, got: {joined}"
    );
}