datalog-structural-model 1.0.0

Typed Datalog rule IR, validation, and stratification
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

//! All expression positions participate in structural safety validation.
use datalog_structural_model::{
    Atom, BindExpr, BuiltinFilter, ConstantSymbol, Literal, MAX_TRIPLE_TERM_NESTING,
    PredicateSymbol, Program, Rule, Term, VariableSymbol,
};
fn var(s: &str) -> Term {
    Term::Variable(VariableSymbol::new(s))
}
fn atom(term: Term) -> Atom {
    Atom {
        predicate: PredicateSymbol::new("p"),
        terms: vec![term],
    }
}
fn triple(term: Term) -> Term {
    Term::TripleTerm(Box::new(atom(term)))
}
fn program(literal: Literal) -> Program {
    Program {
        rules: vec![Rule::new(
            atom(var("bound")),
            vec![Literal::Positive(atom(var("bound"))), literal],
        )],
    }
}
#[test]
fn variables_inside_filter_triple_terms_must_be_bound() {
    assert!(
        program(Literal::Filter(BuiltinFilter::IsIri(triple(var(
            "unbound"
        )))))
        .validate()
        .is_err()
    );
}
#[test]
fn variables_inside_bind_triple_terms_must_be_bound() {
    assert!(
        program(Literal::Bind {
            var: VariableSymbol::new("result"),
            expr: BindExpr::Term(triple(var("unbound")))
        })
        .validate()
        .is_err()
    );
}
#[test]
fn triple_depth_inside_expression_trees_is_checked() {
    let mut term = Term::Constant(ConstantSymbol::new("value"));
    for _ in 0..=MAX_TRIPLE_TERM_NESTING {
        term = triple(term);
    }
    assert!(
        program(Literal::Filter(BuiltinFilter::IsIri(term.clone())))
            .validate()
            .is_err()
    );
    assert!(
        program(Literal::Bind {
            var: VariableSymbol::new("result"),
            expr: BindExpr::Term(term)
        })
        .validate()
        .is_err()
    );
}
#[test]
fn nested_skolem_arguments_are_rejected() {
    let inner = Term::Skolem {
        name: ConstantSymbol::new("inner"),
        args: vec![var("x")],
    };
    let outer = Term::Skolem {
        name: ConstantSymbol::new("outer"),
        args: vec![inner],
    };
    assert!(
        Program {
            rules: vec![Rule::positive(atom(outer), vec![atom(var("x"))])]
        }
        .validate()
        .is_err()
    );
}

#[test]
fn skolem_terms_in_filters_and_bindings_are_rejected() {
    let skolem = Term::Skolem {
        name: ConstantSymbol::new("label"),
        args: vec![],
    };
    assert!(
        program(Literal::Filter(BuiltinFilter::IsIri(skolem.clone())))
            .validate()
            .is_err()
    );
    assert!(
        program(Literal::Bind {
            var: VariableSymbol::new("out"),
            expr: BindExpr::Term(skolem)
        })
        .validate()
        .is_err()
    );
}