| 1 | % (c) 2009-2016 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(weakest_preconditions, [weakest_precondition/3,set_reference_machine/1,delete_reference_machine/0]). | |
| 6 | ||
| 7 | :- use_module(module_information,[module_info/2]). | |
| 8 | :- module_info(group,cbc). | |
| 9 | :- module_info(description,'This module provides weakest precondition calculation for B and Event-B operations.'). | |
| 10 | ||
| 11 | :- use_module(library(lists)). | |
| 12 | :- use_module(library(sets), [subset/2]). | |
| 13 | ||
| 14 | :- use_module(bsyntaxtree, [get_texpr_expr/2, | |
| 15 | get_texpr_id/2, get_texpr_ids/2, | |
| 16 | get_texpr_type/2, | |
| 17 | create_texpr/4, safe_create_texpr/3, | |
| 18 | create_forall/3, | |
| 19 | create_negation/2, | |
| 20 | conjunct_predicates/2, | |
| 21 | replace_id_by_expr/4, | |
| 22 | replace_ids_by_exprs/4, | |
| 23 | find_typed_identifier_uses/2, | |
| 24 | remove_all_infos/2]). | |
| 25 | :- use_module(b_read_write_info, [get_accessed_vars/4]). | |
| 26 | :- use_module(bmachine_eventb, [prime_variables/2, | |
| 27 | prime_variable/2, is_primed_id/1]). | |
| 28 | :- use_module(error_manager, [add_error_fail/3]). | |
| 29 | :- use_module(tools, [assert_once/1]). | |
| 30 | :- use_module(bmachine, [b_get_machine_operation/4]). | |
| 31 | :- use_module(bmachine_structure, [get_section/3]). | |
| 32 | ||
| 33 | :- use_module(probsrc(translate),[translate_substitution/2,print_subst/1]). | |
| 34 | :- use_module(probsrc(debug),[debug_mode/1]). | |
| 35 | ||
| 36 | % dynamic predicate may contain a machine in which operations are looked up | |
| 37 | % this is nessasary for the wp of operation calls, if the operation does not | |
| 38 | % belong to the currently loaded machine | |
| 39 | % (but for example to a refinement/abstraction) | |
| 40 | :- volatile machine/1. | |
| 41 | :- dynamic machine/1. | |
| 42 | ||
| 43 | set_reference_machine(M) :- | |
| 44 | delete_reference_machine, | |
| 45 | assert_once(machine(M)). | |
| 46 | delete_reference_machine :- | |
| 47 | retractall(machine(_)). | |
| 48 | ||
| 49 | % lookup operations in the reference machine if it exists | |
| 50 | % otherwise, lookup in loaded machine | |
| 51 | lookup_operation(Name,Results,Parameters,Body) :- | |
| 52 | ground(Name), % only for lookup of operations | |
| 53 | get_texpr_id(Name,op(OperationName)), | |
| 54 | (machine(M) | |
| 55 | -> get_section(operation_bodies,M,Ops), | |
| 56 | get_texpr_expr(Op,operation(TId,Results,Parameters,Body)), | |
| 57 | get_texpr_id(TId,op(Name)), | |
| 58 | member(Op,Ops) | |
| 59 | ; b_get_machine_operation(OperationName,Results,Parameters,Body)). | |
| 60 | ||
| 61 | :- mode weakest_precondition(+Action, +Pred,-WP). | |
| 62 | weakest_precondition(Action,Pred,WP) :- | |
| 63 | get_texpr_expr(Action,Expr), | |
| 64 | weakest_precondition2(Expr,Pred,WP). | |
| 65 | ||
| 66 | % any statement. see schneider p. 126 | |
| 67 | weakest_precondition2(any(Parameters,PreCond,Body),Pred,WP) :- !, | |
| 68 | weakest_precondition(Body,Pred,InnerWP), | |
| 69 | safe_create_texpr(implication(PreCond,InnerWP),pred,UnquantifiedWP), | |
| 70 | create_forall(Parameters,UnquantifiedWP,WP). | |
| 71 | weakest_precondition2(assign(TIds,Exprs),Pred,WP) :- !, | |
| 72 | function_assignment_to_overwrite(TIds,Exprs,TIds2,Exprs2), | |
| 73 | get_texpr_ids(TIds2,StrippedIDs), | |
| 74 | replace_ids_by_exprs(Pred,StrippedIDs,Exprs2,WP). | |
| 75 | weakest_precondition2(assign_single_id(TId,Expr),Pred,WP) :- !, | |
| 76 | function_assignment_to_overwrite([TId],[Expr],[TId2],[Expr2]), | |
| 77 | get_texpr_id(TId2,Id), | |
| 78 | replace_id_by_expr(Pred,Id,Expr2,WP). | |
| 79 | % nondeterministic choice. see schneider p. 126 | |
| 80 | weakest_precondition2(becomes_element_of(IDs,Set),Pred,WP) :- !, | |
| 81 | create_members(Set,IDs,MemberOf), | |
| 82 | safe_create_texpr(implication(MemberOf,Pred),pred,InnerWP), | |
| 83 | create_forall(IDs,InnerWP,WP). | |
| 84 | % nondet choice of action. see schneider p. 129 | |
| 85 | weakest_precondition2(choice(Choices),Pred,WP) :- !, | |
| 86 | choice_wps(Choices,Pred,WPs), | |
| 87 | conjunct_predicates(WPs,WP). | |
| 88 | weakest_precondition2(if(IfList),Pred,WP) :- !, | |
| 89 | if_wp(IfList,Pred,WP). | |
| 90 | % let statement: local variable with value. see schneider p. 125 | |
| 91 | weakest_precondition2(let(Parameters,Defs,Body),Pred,WP) :- !, | |
| 92 | weakest_precondition(Body,Pred,InnerWP), | |
| 93 | safe_create_texpr(implication(Defs,InnerWP),pred,UnquantifiedWP), | |
| 94 | create_forall(Parameters,UnquantifiedWP,WP). | |
| 95 | weakest_precondition2(operation_call(Operation,ResultsCall,ParametersCall),Pred,WP) :- !, | |
| 96 | lookup_operation(Operation,ResultsOperation,ParametersOperation,Body), | |
| 97 | % replace parameter/results identifiers | |
| 98 | append([ResultsOperation,ParametersOperation],IDs), append([ResultsCall,ParametersCall],Replacements), | |
| 99 | get_texpr_ids(IDs,StrippedIDs), | |
| 100 | replace_ids_by_exprs(Body,StrippedIDs,Replacements,NewBody), | |
| 101 | weakest_precondition(NewBody,Pred,WP). | |
| 102 | weakest_precondition2(parallel(Actions),Pred,WP) :- !, | |
| 103 | merge_parallels(Actions,Action), | |
| 104 | weakest_precondition(Action,Pred,WP). | |
| 105 | weakest_precondition2(precondition(Condition,Action),Pred,WP) :- !, | |
| 106 | weakest_precondition(Action,Pred,InnerWP), | |
| 107 | conjunct_predicates([Condition,InnerWP],WP). | |
| 108 | % weakest precondition for event-b events | |
| 109 | weakest_precondition2(rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents),Pred,WP) :- !, | |
| 110 | (is_list(Act) | |
| 111 | -> create_texpr(parallel(Act),subst,[],NewAct) | |
| 112 | ; NewAct=Act | |
| 113 | ), | |
| 114 | weakest_precondition2(any(Parameters,Guard,NewAct),Pred,WP). | |
| 115 | % there are two kinds of selects: just whens and whens/else | |
| 116 | % the else case just collects all guards and negates them | |
| 117 | % see schneider p. 132 | |
| 118 | weakest_precondition2(select(Whens),Pred,WP) :- !, | |
| 119 | select_whens_wps(Whens,Pred,WPs), | |
| 120 | conjunct_predicates(WPs,WP). | |
| 121 | weakest_precondition2(select(Whens,Else),Pred,WP) :- !, | |
| 122 | select_whens_wps(Whens,Pred,WPs), | |
| 123 | conjunct_predicates(WPs,WhensWP), | |
| 124 | % collect all guards and negate them | |
| 125 | % => precondition for else-case | |
| 126 | findall(PC,(member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds), | |
| 127 | maplist(create_negation,AllPreconds,NegAllPreconds), | |
| 128 | conjunct_predicates(NegAllPreconds,ElsePrecond), | |
| 129 | % imply [T_n]S | |
| 130 | weakest_precondition(Else,Pred,InnerWP), | |
| 131 | safe_create_texpr(implication(ElsePrecond,InnerWP),pred,ElseWP), | |
| 132 | conjunct_predicates([WhensWP,ElseWP],WP). | |
| 133 | weakest_precondition2(sequence(Actions),Pred,WP) :- !, | |
| 134 | sequence_wp(Actions,Pred,WP). | |
| 135 | weakest_precondition2(skip,Pred,WP) :- !,WP=Pred. | |
| 136 | weakest_precondition2(var(IDs,Subst),Pred,WP) :- !, | |
| 137 | weakest_precondition(Subst,Pred,InnerWP), | |
| 138 | create_forall(IDs,InnerWP,WP). | |
| 139 | weakest_precondition2(while(P,S,I,V),R,WP) :- !, | |
| 140 | % [while P DO S INVARIANT I VARIANT V END] R | |
| 141 | % see abrial, b-book, p. 395: | |
| 142 | % there are five predicates. their conjunction is equal to the weakest precondition | |
| 143 | % first, create the list of all variables modified by the Stmt (used in forall) | |
| 144 | find_typed_identifier_uses(S,AllIdentifiersInStmt), | |
| 145 | get_accessed_vars(S,[],ModifiedVarsInStmt,_Reads), | |
| 146 | % the identifiers in ModifiedVarsInStmt are not typed. fetch the types from the list of all identifiers | |
| 147 | % TypedModifiedVarsInStmt = X | |
| 148 | get_texpr_ids(TypedModifiedVarsInStmt,ModifiedVarsInStmt), | |
| 149 | subset(TypedModifiedVarsInStmt,AllIdentifiersInStmt), | |
| 150 | ||
| 151 | ForAlls = TypedModifiedVarsInStmt, | |
| 152 | ||
| 153 | % first obligation: the invariant | |
| 154 | WP1 = I, | |
| 155 | ||
| 156 | % second obligation: forall x in X: (I & P => [S]I) | |
| 157 | conjunct_predicates([I,P],LHS2), | |
| 158 | weakest_precondition(S,I,RHS2), | |
| 159 | safe_create_texpr(implication(LHS2,RHS2),pred,Inner2), | |
| 160 | create_forall(ForAlls,Inner2,WP2), | |
| 161 | ||
| 162 | % third obligation: forall x in X: (I => v in N) | |
| 163 | safe_create_texpr(member(V,b(integer_set('NATURAL'),set(integer),[])),pred,RHS3), | |
| 164 | safe_create_texpr(implication(I,RHS3),pred,Inner3), | |
| 165 | create_forall(ForAlls,Inner3,WP3), | |
| 166 | ||
| 167 | % fourth obligation: forall x in X: I & P => [gamma:=V][S](V<gamma) | |
| 168 | create_texpr(identifier('gamma\''),integer,[],Gamma), | |
| 169 | create_texpr(assign_single_id(Gamma,V),subst,[],AssignVariantToGamma), | |
| 170 | safe_create_texpr(less(V,Gamma),pred,VLessGamma), | |
| 171 | weakest_precondition(S,VLessGamma,RHS4T), | |
| 172 | weakest_precondition(AssignVariantToGamma,RHS4T,RHS4), | |
| 173 | LHS4 = LHS2, | |
| 174 | safe_create_texpr(implication(LHS4,RHS4),pred,Inner4), | |
| 175 | create_forall(ForAlls,Inner4,WP4), | |
| 176 | ||
| 177 | % fifth obligation: forall x in X: (I & not P) => R | |
| 178 | create_negation(P,NotP), conjunct_predicates([I,NotP],LHS5), | |
| 179 | safe_create_texpr(implication(LHS5,R),pred,Inner5), | |
| 180 | create_forall(ForAlls,Inner5,WP5), | |
| 181 | ||
| 182 | % conjunct them all together | |
| 183 | conjunct_predicates([WP1,WP2,WP3,WP4,WP5],WP). | |
| 184 | weakest_precondition2(Action,Pred,_WeakestPrecondition) :- !, | |
| 185 | get_texpr_expr(Action,ActionExpr), | |
| 186 | add_error_fail(weakest_precondition,'weakest-precondition implementation missing: ',[ActionExpr,Pred]). | |
| 187 | ||
| 188 | choice_wps([],_Pred,[]). | |
| 189 | choice_wps([Choice|Choices],Pred,[ChoiceWP|WPs]) :- | |
| 190 | weakest_precondition(Choice,Pred,ChoiceWP), | |
| 191 | choice_wps(Choices,Pred,WPs). | |
| 192 | ||
| 193 | % see schneider p. 38 | |
| 194 | % [if E then S else T end] P = (E => [S]P) & (not E => [T]P) | |
| 195 | if_wp([IF|IFs],Pred,WP) :- | |
| 196 | get_texpr_expr(IF,if_elsif(Test,Body)), | |
| 197 | % if-part | |
| 198 | weakest_precondition(Body,Pred,InnerWP), | |
| 199 | safe_create_texpr(implication(Test,InnerWP),pred,IfWP), | |
| 200 | % if there are further else/elseif parts, create pos | |
| 201 | (if_wp(IFs,Pred,SubWP) | |
| 202 | -> create_negation(Test,NegTest), | |
| 203 | safe_create_texpr(implication(NegTest,SubWP),pred,ElseWP), | |
| 204 | conjunct_predicates([IfWP,ElseWP],WP) | |
| 205 | ; WP = IfWP). | |
| 206 | ||
| 207 | merge_parallels(ParallelAssigns,Result) :- %trace, | |
| 208 | create_texpr(truth,pred,[],True), | |
| 209 | create_texpr(parallel([]),subst,[],Body), | |
| 210 | EmptyAny = any([],True,Body), | |
| 211 | EmptyAssign = assign([],[]), | |
| 212 | merge_parallels1(ParallelAssigns,EmptyAssign,EmptyAny,Assigns,Anys,Rest), | |
| 213 | (Rest == [] -> | |
| 214 | merge_assigns_and_anys(Assigns,Anys,Res), | |
| 215 | create_texpr(Res,subst,[],Result), | |
| 216 | (debug_mode(on) -> print_subst(Result),nl; true) | |
| 217 | ; otherwise -> | |
| 218 | add_error_fail(merge_parallels, 'merging of parallel executions failed (implementation missing?):', Rest) | |
| 219 | ). | |
| 220 | ||
| 221 | merge_parallels1([],Assigns,Anys,Assigns,Anys,[]). | |
| 222 | merge_parallels1([Subst|Substs],assign(IDs2,Exprs2),any(Par2,PreCond2,Body2),ResAssigns,ResAnys,Rest) :- | |
| 223 | get_texpr_expr(Subst,Expr), | |
| 224 | merge_parallels_normalize(Expr,ExprN), | |
| 225 | (ExprN = assign(IDs1,Exprs1) -> | |
| 226 | append(IDs2,IDs1,IDs3), | |
| 227 | append(Exprs2,Exprs1,Exprs3), | |
| 228 | NewAssign = assign(IDs3,Exprs3), | |
| 229 | NewAny = any(Par2,PreCond2,Body2), | |
| 230 | Rest = Rest1 | |
| 231 | ; ExprN = any(Par1,PreCond1,Body1) -> | |
| 232 | append(Par2,Par1,Par3), | |
| 233 | conjunct_predicates([PreCond2,PreCond1],PreCond3), | |
| 234 | get_texpr_expr(Body2,parallel(AnySubsts2)), | |
| 235 | create_texpr(parallel([Body1|AnySubsts2]),subst,[],Body3), | |
| 236 | NewAny = any(Par3,PreCond3,Body3), | |
| 237 | NewAssign = assign(IDs2,Exprs2), | |
| 238 | Rest = Rest1 | |
| 239 | ; ExprN = skip -> | |
| 240 | NewAssign = assign(IDs2,Exprs2), | |
| 241 | NewAny = any(Par2,PreCond2,Body2), | |
| 242 | Rest = Rest1 | |
| 243 | ; otherwise -> | |
| 244 | NewAssign = assign(IDs2,Exprs2), | |
| 245 | NewAny = any(Par2,PreCond2,Body2), | |
| 246 | Rest = [Subst|Rest1] | |
| 247 | ), !, % do not backtrack once the a substitution is merged to the assignment or any generator | |
| 248 | merge_parallels1(Substs,NewAssign,NewAny,ResAssigns,ResAnys,Rest1). | |
| 249 | ||
| 250 | merge_assigns_and_anys(Assign,Any,Result) :- | |
| 251 | (empty_any_statement(Any),empty_assign_statement(Assign) -> | |
| 252 | add_error_fail(merge_assigns_and_anys,'merging of parallel executions failed (empty assignment and any statements): ', (Assign,Any)) | |
| 253 | ; empty_any_statement(Any) -> | |
| 254 | Result = Assign | |
| 255 | ; empty_assign_statement(Assign) -> | |
| 256 | Result = Any | |
| 257 | ; otherwise -> | |
| 258 | Any = any(Par,PreCond,Body), | |
| 259 | get_texpr_expr(Body,parallel(Actions)), | |
| 260 | create_texpr(Assign,subst,[],BAssign), | |
| 261 | create_texpr(parallel([BAssign|Actions]),subst,[],NewBody), | |
| 262 | Result = any(Par,PreCond,NewBody) | |
| 263 | ). | |
| 264 | ||
| 265 | empty_any_statement(any([],_Precond,b(parallel([]),subst,_))). | |
| 266 | ||
| 267 | empty_assign_statement(assign([],[])). | |
| 268 | ||
| 269 | % The old implementation for merging parallel assignments | |
| 270 | ||
| 271 | %% merge_parallels([X],X) :- !. | |
| 272 | %% merge_parallels([A1,A2|As],X) :- | |
| 273 | %% merge_parallels2(A1,A2,AMerged), !, | |
| 274 | %% merge_parallels([AMerged|As],X). | |
| 275 | %% merge_parallels([A1,A2|As],X) :- | |
| 276 | %% merge_parallels2(A2,A1,AMerged), !, | |
| 277 | %% merge_parallels([AMerged|As],X). | |
| 278 | %% merge_parallels([A1,A2|_As],_X) :- | |
| 279 | %% get_texpr_expr(A1,A1E), get_texpr_expr(A2,A2E), | |
| 280 | %% add_error_fail(merge_parallels,'merging of parallel executions failed (implementation missing?): ',(A1E,A2E)). | |
| 281 | ||
| 282 | %% merge_parallels2(A1,A2,AMerged) :- | |
| 283 | %% get_texpr_expr(A1,A1Expr), get_texpr_expr(A2,A2Expr), | |
| 284 | %% merge_parallels_normalize(A1Expr,A1ExprN), | |
| 285 | %% merge_parallels_normalize(A2Expr,A2ExprN), | |
| 286 | %% merge_parallels3(A1ExprN,A2ExprN,AMergedExpr), | |
| 287 | %% create_texpr(AMergedExpr,subst,[],AMerged). | |
| 288 | ||
| 289 | %% merge_parallels3(assign(IDs1,Exprs1),assign(IDs2,Exprs2),assign(IDs3,Exprs3)) :- | |
| 290 | %% append(IDs1,IDs2,IDs3), append(Exprs1,Exprs2,Exprs3). | |
| 291 | %% merge_parallels3(any(Parameters,PreCond,Body),SomeSubstitution,any(Parameters,PreCond,NewBody)) :- | |
| 292 | %% create_texpr(SomeSubstitution,subst,[],SomeSubstitutionTExpr), | |
| 293 | %% create_texpr(parallel([Body,SomeSubstitutionTExpr]),subst,[],NewBody). | |
| 294 | % in case we have more than two substitutions in a parallel block (see for example B/Ivo/WeakestPreconditon/Tickets/MergeParallels.mch WP: [Evt1](G(Evt2))) | |
| 295 | ||
| 296 | merge_parallels_normalize(assign_single_id(ID,Expr),assign([ID],[Expr])) :- !. | |
| 297 | merge_parallels_normalize(becomes_element_of(IDs,Set), any(Parameters,PreCond,Body)) :- !, | |
| 298 | prime_variables(IDs,Parameters), create_members(Set,Parameters,PreCond), | |
| 299 | create_texpr(assign(IDs,Parameters),subst,[],Body). | |
| 300 | merge_parallels_normalize(becomes_such(Vars,Condition),any(PrimedIDs,Condition,Body)) :- !, | |
| 301 | find_typed_identifier_uses(Condition,UsedIDs), | |
| 302 | get_primed_ids(UsedIDs,PrimedIDs), | |
| 303 | get_non_represented_vars(Vars,PrimedIDs,NonRepresented), | |
| 304 | (NonRepresented\=[] -> | |
| 305 | get_texpr_ids(NonRepresented,VarsIDs), | |
| 306 | create_texpr(becomes_such(Vars,Condition),subst,[],TExpr), | |
| 307 | translate_substitution(TExpr,Subst), | |
| 308 | add_error_fail(merge_parallels_normalize,'Normalising becomes_such(...) costruct failed because the following variables were not reprsented by prime variables: ', (VarsIDs,Subst)) | |
| 309 | ;otherwise -> | |
| 310 | create_texpr(assign(Vars,PrimedIDs),subst,[],Body) | |
| 311 | ). | |
| 312 | % Functional overrides in Event-B will be translated to assignments using the override operator (<+) | |
| 313 | merge_parallels_normalize(X,X). | |
| 314 | ||
| 315 | get_non_represented_vars([],_PrimedVars,[]). | |
| 316 | get_non_represented_vars([Var|Vars],PrimedVars,NonRepresented) :- | |
| 317 | prime_variable(Var,VarPrimed), | |
| 318 | remove_all_infos(VarPrimed,VarPrimedNoInfos), | |
| 319 | (member(VarPrimedNoInfos,PrimedVars) -> | |
| 320 | NonRepresented = NonRepresented1 | |
| 321 | ; otherwise -> | |
| 322 | NonRepresented = [Var|NonRepresented1] | |
| 323 | ), | |
| 324 | get_non_represented_vars(Vars,PrimedVars,NonRepresented1). | |
| 325 | ||
| 326 | get_primed_ids([],[]). | |
| 327 | get_primed_ids([ID|IDs],[ID|Rest]) :- | |
| 328 | get_texpr_id(ID,I), | |
| 329 | is_primed_id(I),!, | |
| 330 | get_primed_ids(IDs,Rest). | |
| 331 | get_primed_ids([_ID|IDs],Rest) :- | |
| 332 | get_primed_ids(IDs,Rest). | |
| 333 | ||
| 334 | sequence_wp(Actions,Pred,WP) :- | |
| 335 | reverse(Actions,ReversedActions), | |
| 336 | sequence_wp2(ReversedActions,Pred,WP). | |
| 337 | sequence_wp2([],Pred,Pred). | |
| 338 | sequence_wp2([Action|Actions],PredIn,PredOut) :- | |
| 339 | weakest_precondition(Action,PredIn,PredT), | |
| 340 | sequence_wp2(Actions,PredT,PredOut). | |
| 341 | ||
| 342 | select_whens_wps([],_Pred,[]). | |
| 343 | select_whens_wps([When|Whens],Pred,[WP|WPs]) :- | |
| 344 | get_texpr_expr(When,select_when(PreCond, Body)), | |
| 345 | weakest_precondition(Body,Pred,InnerWP), | |
| 346 | safe_create_texpr(implication(PreCond,InnerWP),pred,WP), | |
| 347 | select_whens_wps(Whens,Pred,WPs). | |
| 348 | ||
| 349 | create_members(Set,IDs,MemberOf) :- | |
| 350 | maplist(create_member(Set),IDs,Preds), | |
| 351 | conjunct_predicates(Preds,MemberOf). | |
| 352 | create_member(Set,ID,Res) :- | |
| 353 | safe_create_texpr(member(ID,Set),pred,Res). | |
| 354 | ||
| 355 | %create_renaming(I1,I2,rename(I1,I2)). | |
| 356 | ||
| 357 | function_assignment_to_overwrite([],[],[],[]). | |
| 358 | function_assignment_to_overwrite([b(identifier(ID),Type,Infos)|IdOrFuns],[Expr|Exprs],[b(identifier(ID),Type,Infos)|IdOuts],[Expr|ExprOuts]) :- | |
| 359 | function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts). | |
| 360 | function_assignment_to_overwrite([b(function(Function,Argument),_Type,_Infos)|IdOrFuns],[Expr|Exprs],[Function|IdOuts],[ExprOut|ExprOuts]) :- | |
| 361 | get_texpr_type(Argument,ArgumentType), get_texpr_type(Expr,ExprType), | |
| 362 | get_texpr_type(Function,FunctionType), | |
| 363 | CoupleType = couple(ArgumentType,ExprType), | |
| 364 | safe_create_texpr(couple(Argument,Expr),CoupleType,OverwriteCouple), | |
| 365 | safe_create_texpr(set_extension([OverwriteCouple]),set(CoupleType),CoupleInSet), | |
| 366 | safe_create_texpr(overwrite(Function,CoupleInSet),FunctionType,ExprOut), | |
| 367 | function_assignment_to_overwrite(IdOrFuns,Exprs,IdOuts,ExprOuts). |