eqlog 0.9.0

Datalog with equality
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

mod ast;
mod diagonals;
mod index_selection;
mod semi_naive;
mod sort;

use std::{iter::once, sync::Arc};

use crate::algebra::signature::{FuncId, Signature};

pub use ast::*;
pub use diagonals::*;
pub use index_selection::*;
pub use semi_naive::*;
pub use sort::*;

pub fn semi_naive_functionality(
    func: FuncId,
    signature: &Signature,
    rule_name: impl Into<String>,
) -> FlatRule {
    let domain = flat_domain(func, signature);
    let codomain = signature.func(func).codomain;

    let func_rel = FlatInRel::Rel(FlatRel::Func(func));

    let func_args: Vec<FlatVar> = (0..domain.len())
        .map(|i| {
            let typ = domain[i];
            let name = Arc::from(format!("arg{i}"));
            FlatVar { name, typ }
        })
        .collect();

    let result0 = FlatVar {
        name: Arc::from("result0".to_string()),
        typ: codomain,
    };
    let result1 = FlatVar {
        name: Arc::from("result1".to_string()),
        typ: codomain,
    };

    let rel_args0: Vec<FlatVar> = func_args
        .iter()
        .cloned()
        .chain(once(result0.clone()))
        .collect();
    let rel_args1: Vec<FlatVar> = func_args.into_iter().chain(once(result1.clone())).collect();

    let premise = vec![
        FlatIfStmt {
            rel: func_rel.clone(),
            args: rel_args0,
            age: QueryAge::New,
        },
        FlatIfStmt {
            rel: func_rel.clone(),
            args: rel_args1,
            age: QueryAge::All,
        },
    ];

    let conclusion = vec![FlatThenStmt {
        rel: FlatOutRel::Equality(codomain),
        args: vec![result0, result1],
    }];

    FlatRule {
        name: rule_name.into(),
        premise,
        conclusion,
    }
}