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

use super::ast::*;

fn transform_stmt(stmt: &FlatIfStmt) -> FlatIfStmt {
    let rel = match &stmt.rel {
        FlatInRel::Rel(rel) => *rel,
        FlatInRel::TypeSet(_) | FlatInRel::RelWithDiagonals { .. } => {
            return stmt.clone();
        }
        FlatInRel::Equality(_) => {
            let [lhs, rhs]: &[FlatVar; 2] = stmt.args.as_slice().try_into().unwrap();
            // Could also transform a diagonal equality into a typeset here, but we're not
            // generating Equality diagonals at the moment, so it shouldn't ever happen anyway.
            assert!(lhs != rhs);
            return stmt.clone();
        }
    };

    let equalities: Vec<usize> = stmt
        .args
        .iter()
        .map(|arg| stmt.args.iter().position(|arg0| arg == arg0).unwrap())
        .collect();

    let args: Vec<FlatVar> = stmt
        .args
        .iter()
        .zip(equalities.iter())
        .enumerate()
        .filter_map(
            |(i, (arg, j))| {
                if i == *j {
                    Some(arg.clone())
                } else {
                    None
                }
            },
        )
        .collect();

    if args.len() == stmt.args.len() {
        // Only trivial equalities.
        return stmt.clone();
    }

    let rel = FlatInRel::RelWithDiagonals {
        rel,
        equalities: equalities.into(),
    };
    FlatIfStmt {
        rel,
        args: args,
        age: stmt.age,
    }
}

pub fn use_rels_with_diagonals(flat_rule: &mut FlatRule) {
    for stmt in flat_rule.premise.iter_mut() {
        *stmt = transform_stmt(stmt);
    }
}