1:- use_module(library(pairs)). 2:- use_module(library(edcg)). 3:- use_module(library(debug)). 4
5edcg:acc_info(egraph, Node, In, Out, add_node(Node, In, Out), t(black('', A, B, ''), black('', A, B, '')), _).
6edcg:acc_info(right, Node, In, Out, quick_add_node(Node, In, Out), t(black('', A, B, ''), black('', A, B, '')), _).
7edcg:acc_info(nodes, T, In, Out, In = [T | Out]).
8edcg:acc_info(unifs, T, In, Out, In = [T | Out]).
9edcg:pass_info(left).
10edcg:pass_info(index).
11
12edcg:pred_info(add_term, 2, [egraph]).
13edcg:pred_info(add_terms, 2, [egraph]).
14edcg:pred_info(saturate, 2, [egraph]).
15edcg:pred_info(match_goals, 2, [left, index, right, unifs]).
16edcg:pred_info(rebuild, 1, [egraph]).
17edcg:pred_info(rebuild_egraph, 2, [unifs]).
18edcg:pred_info(rebuild_egraph, 3, [unifs]).
19edcg:pred_info(rebuild_nodes, 0, [nodes, unifs]).
20edcg:pred_info(congruence_closure, 0, [nodes, unifs]).
21edcg:pred_info(merge_groups, 2, [unifs]).
22edcg:pred_info(merge_ids, 2, [unifs]).
23
24lookup(Node-Class, [N-C | L]) :-
25 ( Node == N
26 -> Class = C
27 ; lookup(Node-Class, L)
28 ).
29
30add_node(Node-Id, In, Out) :-
31 ( compound(Node)
32 -> compound_name_arity(Node, Name, Arity),
33 Key = Name/Arity
34 ; Key = Node
35 ),
36 ( rb_lookup(Key, NodesIn, In)
37 -> true
38 ; NodesIn = []
39 ),
40 ( lookup(Node-Id, NodesIn)
41 -> Out = In
42 ; ord_add_element(NodesIn, Node-Id, NodesOut),
43 rb_insert(In, Key, NodesOut, Out)
44 ).
45
46quick_add_node(Node-Id, In, Out) :-
47 ( compound(Node)
48 -> compound_name_arity(Node, Name, Arity),
49 Key = Name/Arity
50 ; Key = Node
51 ),
52 ( rb_update(In, Key, Nodes, [Node-Id | Nodes], Out)
53 -> true
54 ; rb_insert(In, Key, [Node-Id], Out)
55 ).
56
57add_term(Term, Id), ? compound(Term) ==>>
58 compound_name_arguments(Term, F, Args),
59 foldl(add_term, Args, Ids):egraph,
60 compound_name_arguments(Node, F, Ids),
61 [Node-Id]:egraph.
62add_term(Term, Id) ==>>
63 [Term-Id]:egraph.
64
65:- meta_predicate saturate(:, +, ?, ?). 66
67saturate(Module:Goals, N) -->>
68 insert(In, Right):egraph, variant_hash(In, L1),
69 make_index(In, Index),
70 match_goals(Module, Goals):[left(In), index(Index), right(In, Right), unifs(Unifs, [])],
71 rebuild(Unifs),
72 Out/egraph, variant_hash(Out, L2),
73 debug(saturate, "~p", [L1-L2]),
74 ( ( L1 == L2 ; N =< 0)
75 -> []
76 ; ( N =:= inf -> N1 = N ; N1 is N - 1),
77 saturate(Module:Goals, N1)
78 ).
79
80make_index(EGraph, Index) :-
81 rb_fold(append_nodes, EGraph, [], Nodes),
82 sort(Nodes, Sort),
83 group_pairs_by_key(Sort, Groups),
84 ord_list_to_rbtree(Groups, Index).
85
86append_nodes(_Key-Nodes, In, Out) :-
87 foldl(append_node, Nodes, In, Out).
88
89append_node(Node-Id, In, [Id-Node | In]).
90
91match_goals(_Module, []) -->> [].
92match_goals(Module, [Goal | Goals]) -->>
93 call(Module:Goal):[left, index, right, unifs],
94 match_goals(Module, Goals).
95
96rebuild([A=B | Unifs]) -->>
97 A = B,
98 rebuild(Unifs).
99rebuild([]) -->>
100 rebuild_egraph:[egraph, unifs(Unifs, [])],
101 ( Unifs == []
102 -> []
103 ; rebuild(Unifs)
104 ).
105
106rebuild_egraph(t(Nil, Tree), NewTree2) ==>>
107 NewTree2 = t(Nil, NewTree),
108 rebuild_egraph(Tree, NewTree, Nil).
109rebuild_egraph(black('', _, _, ''), Nil0, Nil) ==>> Nil0 = Nil.
110rebuild_egraph(red(L, K, V, R), NewTree, Nil) ==>>
111 NewTree = red(NL, K, NV, NR),
112 rebuild_nodes:nodes(V, NV),
113 rebuild_egraph(L, NL, Nil),
114 rebuild_egraph(R, NR, Nil).
115rebuild_egraph(black(L, K, V, R), NewTree, Nil) ==>>
116 NewTree = black(NL, K, NV, NR),
117 rebuild_nodes:nodes(V, NV),
118 rebuild_egraph(L, NL, Nil),
119 rebuild_egraph(R, NR, Nil).
120
121rebuild_nodes ==>>
122 sort:nodes,
123 congruence_closure:[nodes, unifs].
124
125congruence_closure -->>
126 group_pairs_by_key:nodes,
127 merge_groups:[nodes, unifs].
128
129merge_groups([], []) -->> [].
130merge_groups([Node-[Id | Ids] | Groups], [Node-Id | Out]) -->>
131 merge_ids(Ids, Id),
132 merge_groups(Groups, Out).
133
134merge_ids([], _) -->> [].
135merge_ids([B | Ids], A) -->>
136 [A=B]:unifs,
137 merge_ids(Ids, A).
138
139edcg:pred_info(comm, 0, [left, index, right, unifs]).
140edcg:pred_info(comm_, 1, [right, unifs]).
141
142comm -->>
143 rb_lookup('+'/2, Nodes):left,
144 comm_(Nodes).
145
146comm_([]) ==>> [].
147comm_([A+B-AB | Nodes]) ==>>
148 [B+A-BA]:right,
149 [AB=BA]:unifs,
150 comm_(Nodes).
151comm_([_ | Nodes]) ==>>
152 comm_(Nodes).
153
154edcg:pred_info(assoc, 0, [left, index, right, unifs]).
155edcg:pred_info(assoc_, 1, [index, right, unifs]).
156edcg:pred_info(assoc__, 2, [right, unifs]).
157
158assoc -->>
159 rb_lookup('+'/2, Nodes):left,
160 assoc_(Nodes).
161assoc_([]) ==>> [].
162assoc_([A+BC-ABC | Rest]) ==>>
163 rb_lookup(BC, Nodes):index,
164 assoc__(A+BC-ABC, Nodes),
165 assoc_(Rest).
166assoc__(_, []) ==>> [].
167assoc__(A+BC-ABC, [B+C | Nodes]) ==>>
168 [A+B-AB, AB+C-ABC_]:right,
169 [ABC=ABC_]:unifs,
170 assoc__(A+BC-ABC, Nodes).
171assoc__(Node, [_ | Nodes])