eqlog 0.1.2

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
75
76
77
78
79
80
81
82
83
84

This is a rough sketch for the phases in the surjective closure algorithm works. 
It assumes we maintain the following data structures:
- For each relation:
  * all_table, to enumerate all tuples, including indices for projections/diagonals/elements.
  * dirty_tuples, enumerating all tuples added in the last step of the closure algorithm.
  * new_tuples, enumerating all tuples we found in the current step of the closure algorithm.
- For each sort
  * all_list and dirty_list, similarly to all_table and dirty_tuples for relations.
	* unrooted_elements, containing those elements that were roots prior to this
	  phase, but have since been merged into other elements.


fn apply_surjective_non_injective_steps() {
  for axiom in surjectve_non_injective_axioms {
    for vars in enumerate(axiom.query) {
      for atom in axiom.action {
        match atom {
          Equate(lhs, rhs) => {
            merge_into(lhs, rhs);
            unrooted_elements.push(lhs);
          }
          Relation(rel, args) => {
            new_tuples[rel].push(args);
          }
        }
      }
    }
  }
}

fn apply_surjective_injective_axioms() {
  for axiom in surjectve_injective_axioms {
    for vars in enumerate(axiom.query) {
      for atom in axiom.action {
        match atom {
          Equate(lhs, rhs) => panic!(),
          Relation(rel, args) => {
            new_tuples[rel].push(canonicalize(args));
          }
        }
      }
    }
  }
}

fn canonicalize_new_tuples() {
  for rel in relations {
    new_tuples =
      new_tuples
      .drain()
      .map(canonicalize)
      .filter(not_in_model_already)
      .collect();
  }
}

fn clean_unrooted_elements() {
  for sort in sorts { 
    for el in unrooted_elements[sort] {
      for rel in relations.filter(|r| arity(r).contains(sort)) {
        new_tuples[rel].extend(all_table[rel].drain_with_element(el).map(canonicalize));
      }
    }
    unrooted_elements[sort].clear();
  }
}

fn rotate_dirty_tuples() {
  for rel in relations {
    all_table[rel].extend(new_tuples[rel]);
    dirty_tuples[rel] = new_tuples[rel];
    new_tuples[rel].clear();
  }
}

fn close() {
  loop {
    apply_surjective_non_injective_axioms();
    canonicalize_new_tuples();
    apply_surjective_injective_axioms();
    clean_unrooted_elements();
    rotate_dirty_tuples();
  }
}