1 | ||
2 | ||
3 | :- module(subtree_compare, [ | |
4 | prepare_operation/5, | |
5 | build_map_list/3, | |
6 | lookup/3, | |
7 | unpack_operation/2, | |
8 | expressions/4, | |
9 | substitutions/4, | |
10 | remove_key/3 | |
11 | ]). | |
12 | ||
13 | ||
14 | :- use_module(probsrc(module_information),[module_info/2]). | |
15 | :- module_info(group,misc). | |
16 | :- module_info(description,'Utilities for trace replay refactoring for ProB2-UI.'). | |
17 | ||
18 | :- use_module(library(lists)). | |
19 | ||
20 | % Recevives an operation and replaces the identifiers with free variables | |
21 | % + Old -Preped -CollectedVars -FreeVars | |
22 | prepare_operation(Old, Preped, FoundVars, FreeVars, Errors) :- | |
23 | prep_operation(Old, Preped, Substitutions),!, | |
24 | keys_and_values(Substitutions, FoundVars, FreeVars), | |
25 | get_st_errors(Errors). | |
26 | ||
27 | %P means prepeared | |
28 | prep_operation(b(operation(Name, OutParas, InParas, Body)), | |
29 | b(operation(PName, POutParas, PInParas, PBody)), Substitutions) :- | |
30 | ||
31 | build_map_list(OutParas, MapOut, POutParas), | |
32 | build_map_list(InParas, MapIn, PInParas), | |
33 | append(MapIn, MapOut, Paras), | |
34 | substitutions(Body, PBody, [Name-PName|Paras], Substitutions). | |
35 | ||
36 | prep_operation(b(initialisation(Body)), b(initialisation(PBody)), Substitutions) :- | |
37 | substitutions(Body, PBody, [], Substitutions). | |
38 | ||
39 | ||
40 | % Gets a names of the given operations | |
41 | unpack_operation(ListOfOperation, NamesOfOperations) :- | |
42 | unpack_operation_aux(ListOfOperation, NamesOfOperations). | |
43 | ||
44 | unpack_operation_aux([b(operation(Name, _, _, _))|T], [Name|T1]):- | |
45 | unpack_operation_aux(T, T1). | |
46 | ||
47 | unpack_operation_aux([], []). | |
48 | ||
49 | %% constructs a map like structure from a list of atoms | |
50 | build_map_list([], [], []). | |
51 | build_map_list([b(identifier(X),Type,_)|T1], [X-F|T2], [b(identifier(F),Type,_)|T3]) :- | |
52 | build_map_list(T1,T2, T3). | |
53 | ||
54 | ||
55 | %% TO DO: Rewrite using ast map_over_expr or similar predicate !! | |
56 | %% <---------------- should be much, much shorter | |
57 | ||
58 | %Substitutions - nothing special to do, just go down until we find identifieres | |
59 | substitutions(b(sequence(List), Type, _), b(sequence(PList), Type, _), Before, After) :- | |
60 | process_all_substitutions(List, PList, Before, After). | |
61 | ||
62 | ||
63 | substitutions(b(select(WhenClauses), Type, _), b(select(PWhenClauses), Type, _), Before, After) :- | |
64 | process_all_substitutions(WhenClauses, PWhenClauses, Before, After). | |
65 | ||
66 | substitutions(b(any(IdentifierList, Predicate, Substitution), Type, _), b(any(PIdentifierList, PPredicate, PSubstitution), Type, _), Before, After) :- | |
67 | process_all_expressions(IdentifierList, PIdentifierList, Before, After1), | |
68 | predicates(Predicate, PPredicate, After1, After2), | |
69 | substitutions(Substitution, PSubstitution, After2, After). | |
70 | ||
71 | ||
72 | substitutions(b(assertion(Condition, Then), Type, _), b(assertion(PCondition, PThen), Type, _), Before, After2) :- | |
73 | predicates(Condition, PCondition, Before, After1), | |
74 | substitutions(Then, PThen, After1, After2). | |
75 | ||
76 | ||
77 | substitutions(b(precondition(Condition, Then), Type,_), b(precondition(PCondition, PThen), Type,_), Before, After2) :- | |
78 | predicates(Condition, PCondition, Before, After1), | |
79 | substitutions(Then, PThen, After1, After2). | |
80 | ||
81 | ||
82 | substitutions(b(skip, Type, _), b(skip, Type, _), _, _). | |
83 | ||
84 | ||
85 | substitutions(b(parallel(Substitutions), _, _), b(parallel(PSubstitutions), _, _), Before, After) :- | |
86 | process_all_substitutions(Substitutions, PSubstitutions, Before, After). | |
87 | ||
88 | ||
89 | substitutions(b(select_when(Condition, Then), _, _), b(select_when(PCondition, PThen), _, _), Before, After) :- | |
90 | predicates(Condition, PCondition, Before, After1), | |
91 | substitutions(Then, PThen, After1, After). | |
92 | ||
93 | ||
94 | substitutions(b(assign(Vars, Vals), Type, _), b(assign(PVars, PVals), Type, _), Before, After2) :- | |
95 | process_all_expressions(Vars, PVars, Before, After1), | |
96 | process_all_expressions(Vals, PVals, After1, After2). | |
97 | ||
98 | ||
99 | substitutions(b(assign_single_id(Var, Val), Type, _), b(assign_single_id(PVar, PVal), Type, _), Before, After2) :- | |
100 | expressions(Var, PVar, Before, After1), | |
101 | expressions(Val, PVal, After1, After2). | |
102 | ||
103 | ||
104 | substitutions(b(choice(Choices), _ ,_), b(choice(PChoices), _ ,_), Before, After) :- | |
105 | process_all_substitutions(Choices, PChoices, Before, After). | |
106 | ||
107 | ||
108 | substitutions(b(becomes_such(Variables, Predicate), _ , _), b(becomes_such(PVariables, PPredicate), _ , _), Before, After) :- | |
109 | process_all_expressions(Variables, PVariables, Before, After1), | |
110 | predicates(Predicate, PPredicate, After1, After). | |
111 | ||
112 | ||
113 | substitutions(b(becomes_element_of(Variables, Expression), _ , _), b(becomes_element_of(PVariables, PExpression), _ , _), Before, After) :- | |
114 | process_all_expressions(Variables, PVariables, Before, After1), | |
115 | expressions(Expression, PExpression, After1, After). | |
116 | ||
117 | substitutions(b(operation_call(ID, Input, Output), _, _), b(operation_call(PID , PInput, POutput), _, _), Before, After) :- | |
118 | expressions(ID, PID, Before, After1), | |
119 | process_all_expressions(Input, PInput, After1, After2), | |
120 | process_all_expressions(Output, POutput, After2, After). | |
121 | ||
122 | ||
123 | substitutions(b(let(Variables, Values, Body), _, _), b(let(PVariables, PValues, PBody), _, _), Before, After) :- | |
124 | process_all_expressions(Variables, PVariables, [], LetAfter), | |
125 | append(Before, LetAfter, BeforeWithLet), | |
126 | process_all_predicates(Values, PValues, BeforeWithLet, After1), | |
127 | substitutions(Body, PBody, After1, After2), | |
128 | keys_and_values(LetAfter, LetKeys,_), | |
129 | maplist(remove_key, LetKeys, After2, After). | |
130 | ||
131 | ||
132 | substitutions(b(if([IF | Rest]), _, _), b(if([PIF | PRest]), _, _), Before, After) :- | |
133 | handle_if(IF, PIF, Before, After1), | |
134 | (Rest = [] -> !,PRest = [], After = After1; | |
135 | !, handle_rest(Rest, PRest, After1, After)). | |
136 | ||
137 | ||
138 | substitutions(b(while(Condition, Body, Invariant, Variant), _,_), b(while(PCondition, PBody, PInvariant, PVariant), _,_), Before, After) :- | |
139 | predicates(Condition, PCondition, Before, After1), | |
140 | substitutions(Body, PBody, After1, After2), | |
141 | predicates(Invariant, PInvariant, After2, After3), | |
142 | expressions(Variant, PVariant, After3, After). | |
143 | ||
144 | ||
145 | substitutions(b(var(Variables, Body), _, _), b(var(PVariables, PBody), _, _), Before, After) :- | |
146 | process_all_expressions(Variables, PVariables, Before, After1), | |
147 | substitutions(Body, PBody, After1, After). | |
148 | ||
149 | ||
150 | substitutions(X,_,_,_) :- !, add_st_error(X). | |
151 | ||
152 | ||
153 | handle_if(b(if_elsif(Condition, Then),_ ,_), b(if_elsif(PCondition, PThen),_ ,_), Before, After) :- | |
154 | predicates(Condition, PCondition, Before, After1), | |
155 | substitutions(Then, PThen, After1, After). | |
156 | ||
157 | ||
158 | % Else is always the last | |
159 | handle_rest([b(if_elsif(b(truth,_,_), Then), _,_)], [b(if_elsif(b(truth,_,_), PThen), _,_)], Before, After) :- !, | |
160 | substitutions(Then, PThen, Before, After). | |
161 | ||
162 | ||
163 | % ElsIf | |
164 | handle_rest([b(if_elsif(Condition, Then), _,_) | Rest], [b(if_elsif(PCondition, PThen), _,_) | PRest], Before, After) :- !, | |
165 | predicates(Condition, PCondition, Before, After1), | |
166 | substitutions(Then, PThen, After1, After2), | |
167 | handle_rest(Rest, PRest, After2, After). | |
168 | ||
169 | ||
170 | %Predicates same as substitutions, just go down until finding identifieres | |
171 | predicates(b(conjunct(Left, Right), Type, _), b(conjunct(PLeft, PRight), Type,_), Before, After2) :- | |
172 | predicates(Left, PLeft, Before, After1), | |
173 | predicates(Right, PRight, After1, After2). | |
174 | ||
175 | ||
176 | predicates(b(disjunct(Left, Right), Type, _), b(disjunct(PLeft, PRight), Type, _), Before, After2) :- | |
177 | predicates(Left, PLeft, Before, After1), | |
178 | predicates(Right, PRight, After1, After2). | |
179 | ||
180 | ||
181 | predicates(b(subset(Left, Right), _, _), b(subset(PLeft, PRight), _, _), Before, After) :- | |
182 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
183 | ||
184 | ||
185 | predicates(b(not_subset(Left, Right), _, _), b(not_subset(PLeft, PRight), _, _), Before, After) :- | |
186 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
187 | ||
188 | ||
189 | predicates(b(implication(Left, Right), _, _), b(implication(PLeft, PRight), _, _), Before, After) :- | |
190 | process_all_predicates([Left, Right], [PLeft, PRight], Before, After). | |
191 | ||
192 | ||
193 | predicates(b(equivalence(Left, Right), _,_), b(equivalence(PLeft, PRight), _,_), Before, After) :- | |
194 | process_all_predicates([Left, Right], [PLeft, PRight], Before, After). | |
195 | ||
196 | ||
197 | predicates(b(not_member(Left, Right), _, _), b(not_member(PLeft, PRight), _, _), Before, After) :- | |
198 | handle_two_expr(Left, Right,PLeft, PRight, Before, After). | |
199 | ||
200 | predicates(b(member(Left, Right), _, _), b(member(PLeft, PRight), _, _), Before, After) :- | |
201 | handle_two_expr(Left, Right,PLeft, PRight, Before, After). | |
202 | ||
203 | ||
204 | predicates(b(not_subset_strict(Left, Right), _, _), b(not_subset_strict(PLeft, PRight), _, _), Before, After) :- | |
205 | handle_two_expr(Left, Right,PLeft, PRight, Before, After). | |
206 | ||
207 | ||
208 | predicates(b(subset_strict(Left, Right), _, _), b(subset_strict(PLeft, PRight), _, _), Before, After) :- | |
209 | handle_two_expr(Left, Right,PLeft, PRight, Before, After). | |
210 | ||
211 | ||
212 | predicates(b(greater_equal(Left, Right), _, _), b(greater_equal(PLeft, PRight), _, _), Before, After):- | |
213 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
214 | ||
215 | predicates(b(less_equal(Left, Right), _, _), b(less_equal(PLeft, PRight), _, _), Before, After):- | |
216 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
217 | ||
218 | predicates(b(less(Left, Right), Type, _), b(less(PLeft, PRight), Type, _), Before, After):- | |
219 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
220 | ||
221 | predicates(b(greater(Left, Right), Type, _), b(greater(PLeft, PRight), Type, _), Before, After):- | |
222 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
223 | ||
224 | predicates(b(equal(Left, Right), _,_), b(equal(PLeft, PRight), _,_), Before, After) :- | |
225 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
226 | ||
227 | predicates(b(not_equal(Left, Right), _,_), b(not_equal(PLeft, PRight), _,_), Before, After) :- | |
228 | handle_two_expr(Left, Right, PLeft, PRight, Before, After). | |
229 | ||
230 | predicates(b(exists(VarList, Predicate), _, _), b(exists(PLeft, PRight), _, _), Before, After) :- | |
231 | handle_two_expr(VarList, Predicate, PLeft, PRight, Before, After). | |
232 | ||
233 | predicates(b(forall(VarList, Predicate1, Predicate2), _, _), b(forall(PVarList, PPredicate1, PPredicate2), _, _), Before, After) :- | |
234 | process_all_expressions(VarList, PVarList, Before, After1), | |
235 | predicates(Predicate1, PPredicate1, After1, After2), | |
236 | predicates(Predicate2, PPredicate2, After2, After). | |
237 | ||
238 | ||
239 | predicates(b(truth, TruthType,_),b(truth, TruthType,_),Before,Before). | |
240 | ||
241 | ||
242 | predicates(b(let_predicate(Variables, SubValues, Predicate), _, _), b(let_predicate(PVariables, PSubValues, PPredicate), _, _), Before, After) :- | |
243 | process_all_expressions(Variables, PVariables, [], LetAfter), | |
244 | append(Before, LetAfter, BeforeWithLet), | |
245 | process_all_predicates(SubValues, PSubValues, BeforeWithLet, After1), | |
246 | predicates(Predicate, PPredicate, After1, After2), | |
247 | keys_and_values(LetAfter, LetKeys,_), | |
248 | maplist(remove_key, LetKeys, After2, After). | |
249 | ||
250 | ||
251 | predicates(b(negation(Predicate), _,_), b(negation(PPredicate), _,_), Before, After) :- | |
252 | predicates(Predicate, PPredicate, Before, After). | |
253 | ||
254 | predicates(X, _,_,_) :- !, add_st_error(X). | |
255 | ||
256 | handle_two_expr(Left, Right, PLeft, PRight, Before, After2):- | |
257 | expressions(Left , PLeft, Before, After1), | |
258 | expressions(Right, PRight, After1, After2). | |
259 | ||
260 | ||
261 | %Expressions - We need to check if our identifier has a suffix | |
262 | ||
263 | %Operation calls need to be replaced - the operation might be renamed, but not stored as operation calls are not directly important for the trace | |
264 | expressions(b(identifier(op(_)), Type, _), b(identifier(op(_)), Type, _), Before, Before) :- !. | |
265 | ||
266 | ||
267 | expressions(b(identifier(Val), Type, _), b(identifier(PVal), Type, _), Before, After) :- !, | |
268 | (lookup(Val, Before, PVal)-> After=Before; insert(Val, PVal, Before, After)). | |
269 | ||
270 | ||
271 | %Special case of identifier where no typeref is needed | |
272 | expressions(b(identifier(Val)), b(identifier(PVal)), Before, After) :- !, | |
273 | (lookup(Val, Before, PVal)-> After=Before; insert(Val, PVal, Before, After)). | |
274 | ||
275 | ||
276 | expressions(b(unary_minus(Exp), Type,_), b(unary_minus(PExp), Type,_), Before, After) :- | |
277 | expressions(Exp, PExp, Before, After). | |
278 | ||
279 | ||
280 | expressions(b(integer(Val), Type, _ ), b(integer(Val), Type, _), Before, Before ) :- !. | |
281 | ||
282 | ||
283 | expressions(b(boolean_false, Type, _), b(boolean_false, Type, _), Before, Before). | |
284 | ||
285 | expressions(b(boolean_true, Type, _), b(boolean_true, Type, _), Before, Before). | |
286 | ||
287 | expressions(b(min_int, Type, _), b(min_int, Type, _), Before, Before). | |
288 | ||
289 | expressions(b(max_int, Type, _), b(max_int, Type, _), Before, Before). | |
290 | ||
291 | expressions(b(integer_set(Var), Type, _), b(integer_set(Var), Type, _), Before, Before). | |
292 | ||
293 | expressions(b(interval(A, B), Type, [was(integer_set('NAT')),_]), | |
294 | b(interval(NewA, NewB), Type, [was(integer_set('NAT')),_]), Before, Before) :- | |
295 | expressions(A, NewA, _,_), | |
296 | expressions(B, NewB, _,_). | |
297 | ||
298 | ||
299 | expressions(b(interval(A, B), Type, [was(integer_set('INT')),_]), | |
300 | b(interval(NewA, NewB), Type, [was(integer_set('INT')),_]), Before, Before) :- | |
301 | expressions(A, NewA, _,_), | |
302 | expressions(B, NewB, _,_). | |
303 | ||
304 | ||
305 | expressions(b(bool_set,Type,_), b(bool_set,Type,_), Before, Before). | |
306 | ||
307 | /* | |
308 | % Nary Exp | |
309 | expressions(b(value(Value), _, _), TypeInfo, ResultString, Tabs) :- | |
310 | handle_avl(Value, _, TypeInfo, ResultString, Tabs). | |
311 | */ | |
312 | ||
313 | expressions(b(set_extension(SetElements), Type, _), b(set_extension(PSetElements), Type, _), Before, After) :- | |
314 | process_all_expressions(SetElements, PSetElements, Before, After). | |
315 | ||
316 | ||
317 | % Binary Exp | |
318 | expressions(b(relations(Left, Right), Type, _), b(relations(PLeft, PRight), Type, _), Before, After) :- | |
319 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
320 | ||
321 | ||
322 | expressions(b(couple(Left, Right), Type , _), b(couple(PLeft, PRight), Type , _), Before, After) :- | |
323 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
324 | ||
325 | ||
326 | expressions(b(union(Left, Right), Type, Info), b(union(PLeft, PRight), Type, Info), Before, After) :- | |
327 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
328 | ||
329 | ||
330 | expressions(b(event_b_identity, _, _), b(event_b_identity, _, _), Before, Before). | |
331 | ||
332 | ||
333 | expressions(b(total_function(From, To), Type, _), b(total_function(PFrom, PTo), Type, _), Before, After) :- | |
334 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
335 | ||
336 | ||
337 | expressions(b(partial_function(From, To), Type, _), b(partial_function(PFrom, PTo), Type, _), Before, After) :- | |
338 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
339 | ||
340 | ||
341 | expressions(b(total_injection(From, To), Type, _), b(total_injection(PFrom, PTo), Type, _), Before, After) :- | |
342 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
343 | ||
344 | ||
345 | expressions(b(partial_injection(From, To), Type, _), b(partial_injection(PFrom, PTo), Type, _), Before, After) :- | |
346 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
347 | ||
348 | ||
349 | expressions(b(total_surjection(From, To), Type, _), b(total_surjection(PFrom, PTo), Type, _), Before, After) :- | |
350 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
351 | ||
352 | ||
353 | expressions(b(partial_surjection(From, To), Type, _), b(partial_surjection(PFrom, PTo), Type, _), Before, After) :- | |
354 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
355 | ||
356 | ||
357 | expressions(b(total_bijection(From, To), Type, _), b(total_bijection(PFrom, PTo), Type, _), Before, After) :- | |
358 | handle_binary_exp(From, To, PFrom, PTo, Before, After). | |
359 | ||
360 | ||
361 | %%%%%%%%%%%%b(partial_bijection(From, To), Type, _) | |
362 | % This operator does not exists in AtelierB bxml format, we simulate it | |
363 | expressions(b(partial_bijection(Left, Right), Type, _), b(partial_bijection(PLeft, PRight), Type, _), Before, After) :- | |
364 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
365 | ||
366 | ||
367 | expressions(b(interval(Left, Right), Type, _), b(interval(PLeft, PRight), Type, _), Before,After) :- | |
368 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
369 | ||
370 | ||
371 | expressions(b(add(Left, Right), Type, _), b(add(PLeft, PRight), Type, _), Before, After) :- | |
372 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
373 | ||
374 | ||
375 | expressions(b(minus(Left, Right), Type, _), b(minus(PLeft, PRight), Type, _), Before, After) :- | |
376 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
377 | ||
378 | ||
379 | expressions(b(Left div Right, Type, _), b(PLeft div PRight, Type, _), Before, After) :- | |
380 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
381 | ||
382 | ||
383 | expressions(b(multiplication(Left, Right), Type, _), b(multiplication(PLeft, PRight), Type, _), Before, After) :- | |
384 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
385 | ||
386 | ||
387 | expressions(b(modulo(Left, Right), Type, _), b(modulo(PLeft, PRight), Type, _), Before, After) :- | |
388 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
389 | ||
390 | ||
391 | expressions(b(set_subtraction(Left, Right), Type, _), b(set_subtraction(PLeft, PRight), Type, _), Before, After) :- | |
392 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
393 | ||
394 | ||
395 | expressions(b(intersection(Left, Right), Type, _), b(intersection(PLeft, PRight), Type, _), Before, After) :- | |
396 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
397 | ||
398 | ||
399 | expressions(b(direct_product(Left, Right), Type, _), b(direct_product(PLeft, PRight), Type, _), Before, After) :- | |
400 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
401 | ||
402 | ||
403 | expressions(b(composition(Left,Right), Type, _), b(composition(PLeft,PRight), Type, _), Before, After) :- | |
404 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
405 | ||
406 | ||
407 | expressions(b(cartesian_product(Left, Right), Type, _), b(cartesian_product(PLeft, PRight), Type, _), Before, After) :- | |
408 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
409 | ||
410 | ||
411 | expressions(b(concat(Left, Right), Type, _), b(concat(PLeft, PRight), Type, _), Before, After) :- | |
412 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
413 | ||
414 | ||
415 | expressions(b(domain_restriction(Left, Right), Type, _), b(domain_restriction(PLeft, PRight), Type, _), Before, After) :- | |
416 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
417 | ||
418 | ||
419 | expressions(b(domain_subtraction(Left, Right), Type, _), b(domain_subtraction(PLeft, PRight), Type, _), Before, After) :- | |
420 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
421 | ||
422 | ||
423 | expressions(b(range_restriction(Left, Right), Type, _), b(range_restriction(PLeft, PRight), Type, _), Before, After) :- | |
424 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
425 | ||
426 | ||
427 | expressions(b(range_subtraction(Left, Right), Type, _), b(range_subtraction(PLeft, PRight), Type, _), Before, After) :- | |
428 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
429 | ||
430 | ||
431 | expressions(b(restrict_tail(Left, Right), Type, _), b(restrict_tail(PLeft, PRight), Type, _), Before, After) :- | |
432 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
433 | ||
434 | ||
435 | expressions(b(restrict_front(Left, Right), Type, _), b(restrict_front(PLeft, PRight), Type, _), Before, After) :- | |
436 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
437 | ||
438 | ||
439 | expressions(b(function(Left, Right), Type, _), b(function(PLeft, PRight), Type, _), Before, After) :- | |
440 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
441 | ||
442 | ||
443 | expressions(b(overwrite(Left, Right), Type, _), b(overwrite(PLeft, PRight), Type, _), Before, After) :- | |
444 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
445 | ||
446 | ||
447 | expressions(b(parallel_product(Left, Right), Type, _), b(parallel_product(PLeft, PRight), Type, _), Before, After) :- | |
448 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
449 | ||
450 | ||
451 | expressions(b(image(Left, Right), Type, _), b(image(PLeft, PRight), Type, _), Before, After) :- | |
452 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
453 | ||
454 | ||
455 | expressions(b(first_of_pair(Exp), _, _), b(first_of_pair(PExp), _, _), Before, After) :- | |
456 | expressions(Exp, PExp, Before, After). | |
457 | ||
458 | ||
459 | expressions(b(second_of_pair(Exp), _, _), b(first_of_pair(PExp), _, _), Before, After) :- | |
460 | expressions(Exp, PExp, Before, After). | |
461 | ||
462 | ||
463 | expressions(b(iteration(Left, Right), Type, _), b(iteration(PLeft, PRight), Type, _), Before, After) :- | |
464 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After). | |
465 | ||
466 | ||
467 | % Unary Exp | |
468 | expressions(b(range(Exp), Type, _), b(range(PExp), Type, _), Before, After) :- | |
469 | expressions(Exp, PExp, Before, After). | |
470 | ||
471 | ||
472 | expressions(b(domain(Exp), Type, _), b(domain(PExp), Type, _), Before, After) :- | |
473 | expressions(Exp, PExp, Before, After). | |
474 | ||
475 | ||
476 | expressions(b(card(Exp), Type, _), b(card(PExp), Type, _), Before, After) :- | |
477 | expressions(Exp, PExp, Before, After). | |
478 | ||
479 | ||
480 | expressions(b(reflexive_closure(Exp), Type, _), b(reflexive_closure(PExp), Type, _), Before, After) :- | |
481 | expressions(Exp, PExp, Before, After). | |
482 | ||
483 | ||
484 | expressions(b(closure(Exp), Type, _), b(closure(PExp), Type, _), Before, After) :- | |
485 | expressions(Exp, PExp, Before, After). | |
486 | ||
487 | ||
488 | expressions(b(min(Exp), Type, _), b(min(PExp), Type, _), Before, After) :- | |
489 | expressions(Exp, PExp, Before, After). | |
490 | ||
491 | ||
492 | expressions(b(max(Exp), Type, _), b(max(PExp), Type, _), Before, After) :- | |
493 | expressions(Exp, PExp, Before, After). | |
494 | ||
495 | ||
496 | expressions(b(pow_subset(Exp), Type, _), b(pow_subset(PExp), Type, _), Before, After) :- | |
497 | expressions(Exp, PExp, Before, After). | |
498 | ||
499 | ||
500 | expressions(b(pow1_subset(Exp), Type, _), b(pow1_subset(PExp), Type, _), Before, After) :- | |
501 | expressions(Exp, PExp, Before, After). | |
502 | ||
503 | ||
504 | expressions(b(fin_subset(Exp), Type, _), b(fin_subset(PExp), Type, _), Before, After) :- | |
505 | expressions(Exp, PExp, Before, After). | |
506 | ||
507 | ||
508 | expressions(b(fin1_subset(Exp), Type, _), b(fin1_subset(PExp), Type, _), Before, After) :- | |
509 | expressions(Exp, PExp, Before, After). | |
510 | ||
511 | ||
512 | expressions(b(general_concat(Exp), Type, _), b(general_concat(PExp), Type, _), Before, After) :- | |
513 | expressions(Exp, PExp, Before, After). | |
514 | ||
515 | ||
516 | expressions(b(first(Exp), Type, _), b(first(PExp), Type, _), Before, After) :- | |
517 | expressions(Exp, PExp, Before, After). | |
518 | ||
519 | ||
520 | expressions(b(last(Exp), Type, _), b(last(PExp), Type, _), Before, After) :- | |
521 | expressions(Exp, PExp, Before, After). | |
522 | ||
523 | ||
524 | expressions(b(front(Exp), Type, _), b(front(PExp), Type, _), Before, After) :- | |
525 | expressions(Exp, PExp, Before, After). | |
526 | ||
527 | ||
528 | expressions(b(tail(Exp), Type, _), b(tail(PExp), Type, _), Before, After) :- | |
529 | expressions(Exp, PExp, Before, After). | |
530 | ||
531 | ||
532 | expressions(b(identity(Exp), Type, _), b(identity(PExp), Type, _), Before, After) :- | |
533 | expressions(Exp, PExp, Before, After). | |
534 | ||
535 | ||
536 | expressions(b(reverse(Exp), Type, _), b(reverse(PExp), Type, _), Before, After) :- | |
537 | expressions(Exp, PExp, Before, After). | |
538 | ||
539 | ||
540 | expressions(b(rev(Exp), Type, _), b(rev(PExp), Type, _), Before, After) :- | |
541 | expressions(Exp, PExp, Before, After). | |
542 | ||
543 | ||
544 | expressions(b(size(Exp), Type, _), b(size(PExp), Type, _), Before, After) :- | |
545 | expressions(Exp, PExp, Before, After). | |
546 | ||
547 | ||
548 | expressions(b(convert_bool(Pred), Type, _), b(convert_bool(PPred), Type, _), Before, After) :- | |
549 | predicates(Pred, PPred, Before, After). | |
550 | ||
551 | ||
552 | expressions(b(let_expression(Variables, SubValues, Expression), Type, _), b(let_expression(PVariables, PSubValues, PExpression), Type, _), Before, After) :- | |
553 | process_all_expressions(Variables, PVariables, [], LetAfter), | |
554 | append(Before, LetAfter, BeforeWithLet), | |
555 | process_all_predicates(SubValues, PSubValues, BeforeWithLet, After1), | |
556 | expressions(Expression, PExpression, After1, After2), | |
557 | keys_and_values(LetAfter, LetKeys,_), | |
558 | maplist(remove_key, LetKeys, After2, After). | |
559 | ||
560 | ||
561 | expressions(b(empty_set, Type, _), b(empty_set, Type, _), Before, Before). | |
562 | ||
563 | ||
564 | expressions(b(empty_sequence, seq(Type), _), b(empty_sequence, seq(Type), _), Before, Before). | |
565 | ||
566 | ||
567 | expressions(b(surjection_relation(S, T), Type, _), b(surjection_relation(PS, PT), Type, _), Before, After) :- | |
568 | handle_binary_exp(S, T, PS, PT, Before, After). | |
569 | ||
570 | ||
571 | expressions(b(total_relation(S, T), Type, _), b(total_relation(PS, PT), Type, _), Before, After) :- | |
572 | handle_binary_exp(S, T, PS, PT, Before, After). | |
573 | ||
574 | ||
575 | expressions(b(total_surjection_relation(S, T), Type, _), b(total_surjection_relation(PS, PT), Type, _), Before, After) :- | |
576 | handle_binary_exp(S, T, PS, PT, Before, After). | |
577 | ||
578 | ||
579 | ||
580 | expressions(b(record_field(Expr, Id), Type, _), b(record_field(PExpr, PId), Type, _), Before, After) :- | |
581 | expressions(Expr, PExpr, Before, After1), | |
582 | expressions(Id, PId, After1, After). | |
583 | ||
584 | ||
585 | %Special case to recognize records | |
586 | expressions(b(rec(Fields), Type, _), b(rec(PFields), Type, _), Before, After) :- | |
587 | process_all_expressions(Fields, PFields, Before, After). | |
588 | ||
589 | ||
590 | expressions(field(Label, Carrier), field(Label, PCarrier), Before, After) :- | |
591 | expressions(Carrier, PCarrier, Before, After). | |
592 | ||
593 | ||
594 | expressions(b(struct(Exp), Type, _), b(struct(PExp), Type, _), Before, After) :- | |
595 | process_all_expressions(Exp, PExp, Before, After). | |
596 | ||
597 | ||
598 | expressions(b(seq(Exp), Type, _), b(seq(PExp), Type, _), Before, After) :- | |
599 | expressions(Exp, PExp, Before, After). | |
600 | ||
601 | ||
602 | expressions(b(insert_tail(Left, Rigth), Type, _), b(insert_tail(PLeft, PRigth), Type, _), Before, After) :- | |
603 | handle_binary_exp(Left, Rigth, PLeft, PRigth, Before, After). | |
604 | ||
605 | ||
606 | expressions(b(insert_front(Left, Rigth), Type, _), b(insert_front(PLeft, PRight), Type, _), Before, After) :- | |
607 | handle_binary_exp(Left, Rigth, PLeft, PRight, Before, After). | |
608 | ||
609 | ||
610 | expressions(b(general_sum(IdList, Pred, Result), Type, _), b(general_sum(PIdList, PPred, PResult), Type, _), Before, After) :- | |
611 | handle_quantified_set_exp(IdList, Pred, Result, PIdList, PPred, PResult, Before, After). | |
612 | ||
613 | ||
614 | expressions(b(general_product(IdList, Pred, Result), Type, _), b(general_product(PIdList, PPred, PResult), Type, _), Before, After) :- | |
615 | handle_quantified_set_exp(IdList, Pred, Result, PIdList, PPred, PResult, Before, After). | |
616 | ||
617 | ||
618 | expressions(b(general_union(Set), Type, _), b(general_union(PSet), Type, _), Before, After) :- | |
619 | expressions(Set, PSet, Before, After). | |
620 | ||
621 | ||
622 | expressions(b(general_intersection(Set), Type, _), b(general_intersection(PSet), Type, _), Before, After) :- | |
623 | expressions(Set, PSet, Before, After). | |
624 | ||
625 | ||
626 | expressions(b(comprehension_set(VarList, Predicate), Type, _), b(comprehension_set(PVarList, PPredicate), Type, _), Before, After) :- | |
627 | process_all_expressions(VarList, PVarList, Before, After1), | |
628 | predicates(Predicate, PPredicate, After1, After). | |
629 | ||
630 | /* | |
631 | expressions(b(assertion_expression(_,_,b(card(A),_,_)), Type, Info), TypeInfo, ResultString, Tabs) :- | |
632 | memberchk(was(sizet), Info), !, | |
633 | Sizet = b(identifier('sizet')), | |
634 | handle_binary_exp(Sizet, A, Type, '(', TypeInfo, ResultString, Tabs). | |
635 | */ | |
636 | ||
637 | expressions(b(operation_call_in_expr(Id,Paras),_,_), b(operation_call_in_expr(PId,PParas),_,_), Before, After) :- !, | |
638 | expressions(Id, PId, Before, After1), | |
639 | process_all_expressions(Paras, PParas, After1, After). | |
640 | ||
641 | expressions(set(Exp), set(PExp), Before, After) :- | |
642 | expressions(Exp, PExp, Before, After). | |
643 | ||
644 | ||
645 | expressions(seq(Exp), seq(PExp), Before, After) :- | |
646 | expressions(set(couple(Exp, Exp)), set(couple(PExp, PExp)), Before, After). | |
647 | ||
648 | ||
649 | expressions(couple(Left, Right), couple(PLeft, PRight), Before, After) :- | |
650 | expressions(Left, PLeft, Before, After1), | |
651 | expressions(Right, PRight, After1, After). | |
652 | ||
653 | /* | |
654 | expressions(record(Records), ResultString, Tabs) :- | |
655 | MoreTabs = ['\t'|Tabs], | |
656 | maplist(expressions_wrapper(MoreTabs), Records, RecordItemString), | |
657 | insert_newline(RecordItemString, RecordItemStringWithNew), | |
658 | struct_template(RecordItemStringWithNew, Tabs, ResultString). | |
659 | */ | |
660 | ||
661 | expressions(empty_set,empty_set, Before, Before). | |
662 | ||
663 | expressions(X, _,_,_) :- !, add_st_error(X). | |
664 | ||
665 | ||
666 | :- dynamic errors/1. | |
667 | add_st_error(MissingClause) :- | |
668 | (retract(errors(X)) -> true ; X=[]), | |
669 | assertz(errors([MissingClause|X])). | |
670 | ||
671 | get_st_errors(errors(X)) :- | |
672 | (retract(errors(X)) -> true | |
673 | ; X = []). | |
674 | ||
675 | %%%When things go wrong | |
676 | ||
677 | ||
678 | % Handler to reduce code repetition | |
679 | handle_binary_exp(Left, Right, PLeft, PRight, Before, After2) :- | |
680 | expressions(Left , PLeft, Before, After1), | |
681 | expressions(Right, PRight, After1, After2). | |
682 | ||
683 | ||
684 | handle_quantified_set_exp(VarList, Predicate, Expressions, PVarList, PPredicate, PExpression, Before, After) :- | |
685 | process_all_expressions(VarList, PVarList, Before, After1), | |
686 | predicates(Predicate, PPredicate, After1, After2), | |
687 | expressions(Expressions, PExpression, After2, After). | |
688 | ||
689 | ||
690 | ||
691 | % For processing lists of elements and dealing with the results | |
692 | process_all_expressions([], [], Before, Before). | |
693 | ||
694 | ||
695 | process_all_expressions([Frist|Rest], [PFirst|PRest], Before, After) :- | |
696 | expressions(Frist, PFirst, Before, After1), | |
697 | process_all_expressions(Rest, PRest, After1, After). | |
698 | ||
699 | ||
700 | process_all_substitutions([], [], Before, Before). | |
701 | ||
702 | ||
703 | process_all_substitutions([Frist|Rest], [PFirst|PRest], Before, After) :- | |
704 | substitutions(Frist, PFirst, Before, After1), | |
705 | process_all_substitutions(Rest, PRest, After1, After). | |
706 | ||
707 | ||
708 | process_all_predicates([], [], Before, Before). | |
709 | ||
710 | ||
711 | process_all_predicates([Frist|Rest], [PFirst|PRest], Before, After) :- | |
712 | predicates(Frist, PFirst, Before, After1), | |
713 | process_all_predicates(Rest, PRest, After1, After). | |
714 | ||
715 | ||
716 | % makes a lookup if the variable is a parameter. If so the placeholder is returned, else the variable | |
717 | lookup(Variable, [Variable-VAR|_], VAR):-!. | |
718 | ||
719 | lookup(Variable, [Variable2-_|T], VAR) :- | |
720 | Variable \= Variable2, | |
721 | lookup(Variable, T, VAR), !. | |
722 | ||
723 | ||
724 | insert(Var, PVal, [], [Var-PVal]) :- !. | |
725 | insert(Var, PVal, [H1|T], [Var-PVal, H1|T]). | |
726 | ||
727 | remove_key(_, [], []) :- !. | |
728 | remove_key(Key, [NKey-Val| Rest], NewList) :- | |
729 | (Key \= NKey -> | |
730 | remove_key(Key, Rest, RestOfNew), | |
731 | NewList = [NKey-Val|RestOfNew] | |
732 | ; NewList = Rest). | |
733 | ||
734 | ||
735 | ||
736 | ||
737 | ||
738 |