| 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 |