| 1 | % (c) 2009-2024 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(bmachine_eventb,[check_event_b_project/4 | |
| 6 | ,deferred_set_equality_without_enumeration_axioms/2 | |
| 7 | ,is_eventb_additional_info/1 | |
| 8 | ,raw_event/11 | |
| 9 | ,stored_operator_direct_definition/8 % stored operator defs, mainly for bvisual2 | |
| 10 | ,stored_operator/2 % a simpler form | |
| 11 | ,some_operator_uses_reals/0 % true if some operator definitely uses reals | |
| 12 | %,get_operator_arity_from_callback/3 % not yet used | |
| 13 | ]). | |
| 14 | ||
| 15 | :- use_module(library(lists)). | |
| 16 | :- use_module(library(ordsets)). | |
| 17 | :- use_module(library(avl)). | |
| 18 | :- use_module(library(codesio),[read_from_codes/2]). | |
| 19 | ||
| 20 | :- use_module(error_manager). | |
| 21 | :- use_module(tools,[remove_all/3,foldl/4,foldl/5,foldl/6,ajoin_with_sep/3,unique_id/2]). | |
| 22 | :- use_module(self_check). | |
| 23 | :- use_module(btypechecker). | |
| 24 | :- use_module(b_ast_cleanup). | |
| 25 | :- use_module(bsyntaxtree). | |
| 26 | :- use_module(debug). | |
| 27 | :- use_module(bmachine_construction). | |
| 28 | :- use_module(preferences,[get_preference/2]). | |
| 29 | :- use_module(input_syntax_tree,[extract_raw_identifiers/2,create_fresh_identifier/3]). | |
| 30 | :- use_module(translate,[translate_bexpression/2]). | |
| 31 | :- use_module(kernel_freetypes,[create_freetype_typeid/3]). | |
| 32 | :- use_module(pragmas,[extract_pragmas_from_event_b_extensions/2,apply_pragmas_to_event_b_machine/3]). | |
| 33 | :- use_module(input_syntax_tree,[map_over_raw_expr/3]). | |
| 34 | ||
| 35 | :- use_module(module_information,[module_info/2]). | |
| 36 | :- module_info(group,typechecker). | |
| 37 | :- module_info(description,'This module contains the rules for loading a Event-B machine or context. '). | |
| 38 | ||
| 39 | :- set_prolog_flag(double_quotes, codes). | |
| 40 | ||
| 41 | :- use_module(specfile,[eventb_mode/0]). | |
| 42 | deferred_set_equality_without_enumeration_axioms(Set,ExtSet) :- | |
| 43 | eventb_mode, | |
| 44 | deferred_set_eq_wo_enumeration_axioms(Set,ExtSet), | |
| 45 | % there is a single equality Set = {id1,...,idn} and no partition or not enough disequalities | |
| 46 | % quite often the user forgot to add those disequalities | |
| 47 | \+ (deferred_set_eq_wo_enumeration_axioms(Set,ExtS2), ExtS2 \= ExtSet). | |
| 48 | ||
| 49 | :- dynamic deferred_set_eq_wo_enumeration_axioms/2. | |
| 50 | ||
| 51 | check_event_b_project(RawModels,RawContextes,Extensions,MachineWithPragmas) :- | |
| 52 | retractall(deferred_set_eq_wo_enumeration_axioms(_,_)), | |
| 53 | catch( check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas), | |
| 54 | typecheck_errors(Errors), | |
| 55 | ( add_all_perrors(Errors), NoError=false )), % a cut here does not work ! | |
| 56 | !, NoError=true. | |
| 57 | check_event_b_project(_,_,_,_) :- | |
| 58 | add_internal_error('Checking Event-B Model failed; Please submit bug report.',check_event_b_project(_,_,_,_)), | |
| 59 | fail. | |
| 60 | check_event_b_project1([],RawContextes,Extensions,MachineWithPragmas) :- | |
| 61 | !, | |
| 62 | check_theory_extensions(Extensions,Freetypes,Ops,InitEnv), % Theories | |
| 63 | check_contextes(InitEnv,RawContextes,Contextes), | |
| 64 | convert_event_b(context,Freetypes,Ops,Contextes,[],[],Machine), | |
| 65 | extract_pragmas_from_event_b_extensions(Extensions,Pragmas), | |
| 66 | apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas). | |
| 67 | check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas) :- | |
| 68 | compute_animation_chain(RawModels,AnimationChain), | |
| 69 | check_event_b_project2(RawModels,RawContextes,Extensions, | |
| 70 | AnimationChain,Machine), | |
| 71 | extract_pragmas_from_event_b_extensions(Extensions,Pragmas), | |
| 72 | apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas). | |
| 73 | ||
| 74 | check_event_b_project2(RawModels,RawContextes,Extensions,AnimationChain,Machine) :- | |
| 75 | RawModels=[event_b_model(_,Main,_)|_], | |
| 76 | check_theory_extensions(Extensions,Freetypes,Ops,InitEnv), % related to Theory plugin | |
| 77 | % generate type-checked contextes | |
| 78 | check_contextes(InitEnv,RawContextes,Contextes), | |
| 79 | % generate type-checked models | |
| 80 | check_models(InitEnv,RawModels,Contextes,Models), | |
| 81 | % merge all the constants/vars/predicates and events into one machine | |
| 82 | convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine). | |
| 83 | ||
| 84 | % the filter chain contains the name of all models that | |
| 85 | % should be contained in the animation | |
| 86 | compute_animation_chain(Models,AnimationChain) :- | |
| 87 | get_preference(number_skipped_refined_machines,NS), % TODO: also use it for constants if possible | |
| 88 | get_preference(number_animated_abstractions,N), | |
| 89 | debug_println(9,compute_animation_chain(N,skipping(NS))), | |
| 90 | (NS=0 -> NonSkippedModels = Models | |
| 91 | ; append_length(SkippedModels,NonSkippedModels,Models,NS), | |
| 92 | NonSkippedModels = [_|_] | |
| 93 | -> extract_model_names(SkippedModels,SkippedNames), | |
| 94 | add_message(bmachine_eventb,'Skipping animation of refinement machines: ',SkippedNames) | |
| 95 | ; last(Models,AnimatedModel), | |
| 96 | NonSkippedModels = [AnimatedModel], | |
| 97 | extract_model_names(NonSkippedModels,[AName]), | |
| 98 | ajoin(['Cannot skip ',NS,' refinement machines; animating topmost machine only: '],Msg), | |
| 99 | add_warning(bmachine_eventb,Msg,AName) | |
| 100 | ), | |
| 101 | length(NonSkippedModels,L), | |
| 102 | N1 is min(N+1,L), | |
| 103 | prefix_length(NonSkippedModels, AnimatedModels, N1), | |
| 104 | extract_model_names(AnimatedModels,AnimationChain). | |
| 105 | extract_model_names([],[]). | |
| 106 | extract_model_names([event_b_model(_,Name,_)|MRest],[Name|NRest]) :- | |
| 107 | extract_model_names(MRest,NRest). | |
| 108 | ||
| 109 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 110 | % context | |
| 111 | ||
| 112 | check_contextes(InitEnv,RawContextes,Contextes) :- | |
| 113 | debug_println(9,'Checking Contextes'), | |
| 114 | % make sure that a extended context is treated before | |
| 115 | % the extending context | |
| 116 | topological_sort(RawContextes,SortedContextes), | |
| 117 | check_contextes2(SortedContextes,InitEnv,[],Contextes). | |
| 118 | check_contextes2([],_,_,[]). | |
| 119 | check_contextes2([RawContext|Rrest],InitEnv,PrevContextes,[Context|Crest]) :- | |
| 120 | check_context(RawContext,InitEnv,PrevContextes,Context), | |
| 121 | check_contextes2(Rrest,InitEnv,[Context|PrevContextes],Crest). | |
| 122 | ||
| 123 | check_context(RawContext,InitEnv,PrevContextes,Context) :- | |
| 124 | extract_ctx_sections(RawContext,Name,Extends, | |
| 125 | RawSets,RawConstants,RawAbstractConstants,RawAxioms,RawTheorems), | |
| 126 | Context = context(Name,Extends,Sets,Constants,AbstractConstants,Axioms,Theorems), | |
| 127 | ||
| 128 | debug_format(9,'Checking context ~w~n',[Name]), | |
| 129 | % create deferred sets | |
| 130 | create_sets(RawSets,Name,Sets), | |
| 131 | % and constants | |
| 132 | IdInfos = [loc(Name,constants),section(Name)], | |
| 133 | create_identifiers(RawConstants,IdInfos,Constants), | |
| 134 | create_identifiers(RawAbstractConstants,IdInfos,AbstractConstants), | |
| 135 | ||
| 136 | % with the constants and set of seen contextes, | |
| 137 | create_ctx_env(Extends,PrevContextes,InitEnv,PrevEnv), | |
| 138 | % and the sets and constants | |
| 139 | add_unique_variables(Sets,PrevEnv,SetEnv), | |
| 140 | add_unique_variables(Constants,SetEnv,EnvT), | |
| 141 | add_unique_variables(AbstractConstants,EnvT,Env), | |
| 142 | ||
| 143 | % now typecheck the axioms and theorems, | |
| 144 | % this should determine the constant's types | |
| 145 | debug_format(9,'Typechecking axioms and theorems for ~w~n',[Name]), | |
| 146 | typecheck_together([RawAxioms,RawTheorems],Env,[Axioms,Theorems],axioms). | |
| 147 | ||
| 148 | extract_ctx_sections(RawContext,Name,Extends,RawSets,RawConstants,RawAbstractConstants,RawAxioms,RawTheorems) :- | |
| 149 | RawContext = event_b_context(_Pos,Name,Sections), | |
| 150 | optional_rawmachine_section(extends,Sections,[],Extends), | |
| 151 | optional_rawmachine_section(sets,Sections,[],RawSets), | |
| 152 | optional_rawmachine_section(constants,Sections,[],RawConstants), | |
| 153 | optional_rawmachine_section(abstract_constants,Sections,[],RawAbstractConstants), | |
| 154 | optional_rawmachine_section(axioms,Sections,[],RawAxioms), | |
| 155 | optional_rawmachine_section(theorems,Sections,[],RawTheorems). | |
| 156 | ||
| 157 | ||
| 158 | create_sets([],_,[]). | |
| 159 | create_sets([RawSet|RSrest],CtxName,[Set|Srest]) :- | |
| 160 | ext2int_with_pragma(RawSet,deferred_set(SetName),_,set(global(SetName)), | |
| 161 | identifier(SetName),[section(CtxName),given_set],Set), | |
| 162 | create_sets(RSrest,CtxName,Srest). | |
| 163 | ||
| 164 | create_identifiers([],_,[]). | |
| 165 | create_identifiers([RawIdentifier|RIrest],Infos,[Identifier|Irest]) :- | |
| 166 | ext2int_with_pragma(RawIdentifier,I,_,_,I,Infos,Identifier), | |
| 167 | I=identifier(_), | |
| 168 | create_identifiers(RIrest,Infos,Irest). | |
| 169 | ||
| 170 | create_ctx_env(Extends, Contextes, Old, New) :- | |
| 171 | % find all seen contextes (and their extended contextes, | |
| 172 | % and again their extended contextes, ...) | |
| 173 | transitive_contextes(Extends,Contextes,TransExt), | |
| 174 | % and all variables of extended machines | |
| 175 | add_env_vars_for_extended2(TransExt,Contextes,Old,New). | |
| 176 | transitive_contextes(Extends,Contextes,All) :- | |
| 177 | findall(E, transext(Extends,Contextes,E), All1), sort(All1, All). | |
| 178 | transext(Extends,_,E) :- member(E,Extends). | |
| 179 | transext(Extends,Contextes,E) :- | |
| 180 | member(Name,Extends), | |
| 181 | internal_context_extends(Context,Name,NewExtends), | |
| 182 | member(Context,Contextes), | |
| 183 | transext(NewExtends,Contextes,E). | |
| 184 | % add_env_vars_for_extended2(Names,Contextes,OldEnv,NewEnv): | |
| 185 | % Names: a list of the names of the contextes whose constants and sets | |
| 186 | % should be added to the type environment | |
| 187 | % Contextes: a list of all existing contextes | |
| 188 | % OldEnv: the input environment | |
| 189 | % NewEnv: the input environment plus the constants and sets | |
| 190 | add_env_vars_for_extended2([],_,Env,Env). | |
| 191 | add_env_vars_for_extended2([Name|Erest],Contextes,Old,New) :- | |
| 192 | internal_context_sets(Context,Name,Sets), | |
| 193 | internal_context_constants(Context,Name,Constants), | |
| 194 | internal_context_abstract_constants(Context,Name,AbstractConstants), | |
| 195 | member(Context,Contextes),!, | |
| 196 | add_unique_variables(Sets,Old,Env1), | |
| 197 | add_unique_variables(Constants,Env1,Env2), | |
| 198 | add_unique_variables(AbstractConstants,Env2,Env), | |
| 199 | add_env_vars_for_extended2(Erest,Contextes,Env,New). | |
| 200 | ||
| 201 | % copy&paste from bmachine_construction | |
| 202 | add_unique_variables([],Env,Env). | |
| 203 | add_unique_variables([Var|Rest],Old,New) :- | |
| 204 | def_get_texpr_id(Var,Name), | |
| 205 | get_texpr_type(Var,Type), | |
| 206 | get_texpr_info(Var,Infos), | |
| 207 | ( env_lookup_type(Name,Old,_) -> | |
| 208 | add_error(bmachine_eventb,'Identifier declared twice',Name), | |
| 209 | fail | |
| 210 | ; true), | |
| 211 | env_store(Name,Type,Infos,Old,Env), | |
| 212 | add_unique_variables(Rest,Env,New). | |
| 213 | ||
| 214 | % add the primed (') versions of the variables to the | |
| 215 | % type environment | |
| 216 | add_primed_variables(Variables,OrigEnv,NewEnv) :- | |
| 217 | prime_variables(Variables,Primed), | |
| 218 | add_unique_variables(Primed,OrigEnv,NewEnv). | |
| 219 | ||
| 220 | ||
| 221 | :- use_module(btypechecker,[prime_identifiers/2,prime_id/2,is_primed_id/1,prime_identifiers0/2]). | |
| 222 | ||
| 223 | % add a prime (') to each typed identifier | |
| 224 | prime_variables(V,PV) :- prime_identifiers(V,PV). | |
| 225 | % add a prime (') to a typed identifier | |
| 226 | %prime_variable(V,P) :- btypechecker:prime_identifier(V,P). | |
| 227 | ||
| 228 | ||
| 229 | % unprime_id( ListoPrimedIds, CorrespondingIds, PossiblyPrimedID, UnprimedID) | |
| 230 | unprime_id(AtomicIds0,AtomicIds,Id0,Id) :- nth1(N,AtomicIds0,Id0),!, nth1(N,AtomicIds,Id). | |
| 231 | unprime_id(_,_,Id,Id). | |
| 232 | ||
| 233 | check_for_errors(Errors) :- | |
| 234 | % TO DO: extract and add warnings in list | |
| 235 | Errors = [_|_],!,throw(typecheck_errors(Errors)). | |
| 236 | check_for_errors([]). | |
| 237 | ||
| 238 | typecheck_l(Untyped,Env,Type,Typed,Context) :- | |
| 239 | all_same_type(Untyped,Type,Types), | |
| 240 | btype_ground_dl(Untyped,Env,[],Types,Typed1,Errors,[]), | |
| 241 | check_for_errors(Errors), | |
| 242 | maplist(update_eventb_position_infos(Context),Typed1,Typed2), | |
| 243 | clean_up_l_with_optimizations(Typed2,[],Typed,Context),!. | |
| 244 | typecheck_l(Untyped,Env,Type,Typed,Context) :- | |
| 245 | add_failed_call_error(typecheck_l(Untyped,Env,Type,Typed,Context)),fail. | |
| 246 | all_same_type([],_,[]). | |
| 247 | all_same_type([_|R],E,[E|T]) :- all_same_type(R,E,T). | |
| 248 | ||
| 249 | typecheck(Untyped,Env,Type,Typed,Context) :- | |
| 250 | typecheck_with_freevars(Untyped,Env,[],Type,Typed,Context). | |
| 251 | typecheck_with_freevars(Untyped,Env,Freevars,Type,Typed,Context) :- | |
| 252 | btype_ground_dl([Untyped],Env,Freevars,[Type],[Typed1],Errors,[]), | |
| 253 | update_eventb_position_infos(Context,Typed1,Typed2), | |
| 254 | clean_up_pred_or_expr_with_path(Freevars,Typed2,Typed,Context), | |
| 255 | check_for_errors(Errors). | |
| 256 | ||
| 257 | ||
| 258 | :- use_module(probsrc(bsyntaxtree),[transform_bexpr/3, get_rodin_name/2, get_rodin_model_name/2]). | |
| 259 | :- public add_eventb_pos_aux/5. | |
| 260 | add_eventb_pos_aux(Model,LabelName,Context,b(E,T,I),b(E,T,NewInfo)) :- | |
| 261 | nonmember(nodeid(_),I), | |
| 262 | NewInfo = [nodeid(rodin_derived_context_pos(Model,Context,LabelName))|I]. | |
| 263 | % TO DO: we could also try and improve ordinary rodinpos infos by adding context (useful if label names not unique) | |
| 264 | ||
| 265 | % try and improve position information using the context | |
| 266 | update_eventb_position_infos(Context,TE,Res) :- | |
| 267 | get_rodin_model_name(TE,Model), get_rodin_name(TE,LabelName), | |
| 268 | transform_bexpr(add_eventb_pos_aux(Model,LabelName,Context),TE,NewTE),!, | |
| 269 | Res=NewTE. | |
| 270 | update_eventb_position_infos(Context,b(conjunct(A,B),pred,I),b(conjunct(A2,B2),pred,I)) :- !, % useful for guard labels | |
| 271 | update_eventb_position_infos(Context,A,A2), | |
| 272 | update_eventb_position_infos(Context,B,B2). | |
| 273 | update_eventb_position_infos(_,TE,TE). | |
| 274 | ||
| 275 | ||
| 276 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 277 | % models | |
| 278 | ||
| 279 | check_models(InitEnv,RawModels,Contextes,Models) :- | |
| 280 | debug_println(9,'CHECKING MODELS'), | |
| 281 | topological_sort(RawModels,SortedModels), | |
| 282 | check_models2(SortedModels,InitEnv,[],Contextes,Models). | |
| 283 | ||
| 284 | check_models2([],_,_,_,[]). | |
| 285 | check_models2([RawModel|RMrest],InitEnv,PrevModels,Contextes,[Model|Mrest]) :- | |
| 286 | (check_model(RawModel,InitEnv,PrevModels,Contextes,Model) -> true | |
| 287 | ; add_failed_call_error(check_model(RawModel,InitEnv,PrevModels,Contextes,Model)), | |
| 288 | fail), | |
| 289 | check_models2(RMrest,InitEnv,[Model|PrevModels],Contextes,Mrest). | |
| 290 | ||
| 291 | check_model(RawModel,InitEnv,PrevModels,Contextes,Model) :- | |
| 292 | extract_model_sections(RawModel,Name,Refines,Sees, | |
| 293 | RawVariables,RawInvariant, | |
| 294 | RawTheorems,RawVariant,RawEvents), | |
| 295 | Model = model(Name,Refines,Sees,ConcreteVariables,NewVariables,Invariant,Theorems,Events), | |
| 296 | get_refined_model(Refines,PrevModels,RefinedModel), | |
| 297 | ||
| 298 | get_all_abstract_variables(Refines,PrevModels,AbstractionVariables), | |
| 299 | length(PrevModels,Level), | |
| 300 | IdInfos = [loc(Name,variables),section(Name),level(Level)], | |
| 301 | create_identifiers(RawVariables,IdInfos,ConcreteVariables), | |
| 302 | split_abstract_vars(AbstractionVariables,ConcreteVariables, | |
| 303 | NewVariables,DroppedAbstractVars), | |
| 304 | ||
| 305 | create_ctx_env(Sees,Contextes,InitEnv,CtxEnv), | |
| 306 | add_unique_variables(ConcreteVariables,CtxEnv,ModelEnv), | |
| 307 | add_unique_variables(DroppedAbstractVars,ModelEnv,InvEnv), | |
| 308 | % add primed versions of the concrete variables to | |
| 309 | % permit before-after predicates in the witnesses | |
| 310 | add_primed_variables(ConcreteVariables,InvEnv,BeforeAfterEnv), | |
| 311 | ||
| 312 | typecheck_together([RawInvariant,RawTheorems],InvEnv,[Invariant,Theorems],invariant), | |
| 313 | ||
| 314 | typecheck_variant(RawVariant,InvEnv,Variant), | |
| 315 | ||
| 316 | get_abstract_events(RefinedModel,AbstractEvents), | |
| 317 | ||
| 318 | check_events(RawEvents,Name,ModelEnv,BeforeAfterEnv,InvEnv, | |
| 319 | DroppedAbstractVars,ConcreteVariables,AbstractEvents, | |
| 320 | NewVariables,Variant,Events). | |
| 321 | ||
| 322 | % Context is just an information term about the context (axioms, ...) | |
| 323 | typecheck_together(Raws,Env,Typed,Context) :- | |
| 324 | maplist(same_length, Raws, Typed), | |
| 325 | append(Raws,RawL), append(Typed,TypedL), | |
| 326 | typecheck_l(RawL,Env,pred,TypedL,Context). | |
| 327 | ||
| 328 | typecheck_variant(-, _Env, -) :- !. | |
| 329 | typecheck_variant(RawVariant, Env, Variant) :- | |
| 330 | typecheck(RawVariant, Env, Type, Variant,variant), | |
| 331 | ( Type==integer -> true | |
| 332 | ; functor(Type,set,1) -> true | |
| 333 | ; | |
| 334 | add_error(bmachine_eventb,'Invalid type of variant ',Type), | |
| 335 | fail). | |
| 336 | ||
| 337 | remove_linking_parts([],_AnimationChain,[]). | |
| 338 | remove_linking_parts([Inv|Irest],AnimationChain,Invariants) :- | |
| 339 | ( abstraction_var_occures(Inv,AnimationChain) -> | |
| 340 | Invariants = RestInvariants | |
| 341 | ; | |
| 342 | Invariants = [Inv|RestInvariants]), | |
| 343 | remove_linking_parts(Irest,AnimationChain,RestInvariants). | |
| 344 | ||
| 345 | abstraction_var_occures(TExpr,AnimationChain) :- | |
| 346 | get_texpr_expr(TExpr,identifier(_)),!, | |
| 347 | get_texpr_section(TExpr,Section), | |
| 348 | \+ member(Section,AnimationChain). | |
| 349 | abstraction_var_occures(TExpr,AnimationChain) :- | |
| 350 | syntaxtraversion(TExpr,_,_,_,Subs,_), | |
| 351 | abstraction_var_occures_l(Subs,AnimationChain). | |
| 352 | abstraction_var_occures_l([Sub|_],AnimationChain) :- | |
| 353 | abstraction_var_occures(Sub,AnimationChain),!. | |
| 354 | abstraction_var_occures_l([_|Srest],AnimationChain) :- | |
| 355 | abstraction_var_occures_l(Srest,AnimationChain). | |
| 356 | ||
| 357 | get_texpr_section(TExpr,Section) :- | |
| 358 | get_texpr_info(TExpr,Info),member(section(Section),Info),!. | |
| 359 | ||
| 360 | extract_model_sections(RawModel,Name,Refines,Sees,Variables,Invariant,Theorems,Variant,Events) :- | |
| 361 | RawModel = event_b_model(_Pos,Name,Sections), | |
| 362 | optional_rawmachine_section(refines,Sections,-,Refines), | |
| 363 | optional_rawmachine_section(sees,Sections,[],Sees), | |
| 364 | optional_rawmachine_section(variables,Sections,[],Variables), | |
| 365 | optional_rawmachine_section(invariant,Sections,[],Invariant), | |
| 366 | optional_rawmachine_section(theorems,Sections,[],Theorems), | |
| 367 | optional_rawmachine_section(variant,Sections,-,Variant), | |
| 368 | optional_rawmachine_section(events,Sections,[],Events). | |
| 369 | ||
| 370 | %get_abstraction_variables(-,[]). | |
| 371 | %get_abstraction_variables(Model,Variables) :- | |
| 372 | % internal_model_vars(Model,_Name,Variables). | |
| 373 | ||
| 374 | get_abstract_events(-,[]). | |
| 375 | get_abstract_events(Model,Events) :- internal_model_events(Model,_Name,Events). | |
| 376 | ||
| 377 | get_refined_model(-,_Models,-) :- !. | |
| 378 | get_refined_model(Name,Models,Model) :- | |
| 379 | internal_model(M,Name), | |
| 380 | ( memberchk(M,Models) -> | |
| 381 | M=Model | |
| 382 | ; | |
| 383 | add_error(bmachine_eventb,'Unable to find refined model ',Name), | |
| 384 | fail). | |
| 385 | ||
| 386 | split_abstract_vars(AbstractVars,ConcreteVars,NewVars,DroppedVars) :- | |
| 387 | split_abstract_vars2(AbstractVars,ConcreteVars,DroppedVars), | |
| 388 | find_new_variables(ConcreteVars,AbstractVars,NewVars). | |
| 389 | split_abstract_vars2([],_,[]). | |
| 390 | split_abstract_vars2([AbstractVar|AVrest],ConcreteVars,Dropped) :- | |
| 391 | ( find_identifier_in_list(AbstractVar,ConcreteVars,ConcreteVar) -> | |
| 392 | % Both variables have the same type | |
| 393 | get_texpr_type(AbstractVar,Type), | |
| 394 | get_texpr_type(ConcreteVar,Type), | |
| 395 | Dropped = DroppedRest | |
| 396 | ; | |
| 397 | Dropped = [AbstractVar|DroppedRest]), | |
| 398 | split_abstract_vars2(AVrest,ConcreteVars,DroppedRest). | |
| 399 | find_new_variables([],_,[]). | |
| 400 | find_new_variables([ConcreteVar|CVrest],AbstractVars,NewVars) :- | |
| 401 | ( find_identifier_in_list(ConcreteVar,AbstractVars,_AbstractVar) -> NewVars = Nrest | |
| 402 | ; NewVars = [ConcreteVar|Nrest]), | |
| 403 | find_new_variables(CVrest,AbstractVars,Nrest). | |
| 404 | ||
| 405 | % find_identifier_in_list(TypedIdToFind,List,Elem): | |
| 406 | % search for a typed identifier Elem in List wich | |
| 407 | % has the same id as TypedIdToFind, but type and informations | |
| 408 | % may be different | |
| 409 | find_identifier_in_list(TypedIdToFind,List,Found) :- | |
| 410 | def_get_texpr_id(TypedIdToFind,Id), | |
| 411 | get_texpr_id(Found,Id), | |
| 412 | member(Found,List). | |
| 413 | ||
| 414 | get_all_abstract_variables(Refines,AbstractModels,AbstractVariables) :- | |
| 415 | get_all_abstract_variables2(Refines,AbstractModels,_EncounteredIds,AbstractVariables,[]). | |
| 416 | get_all_abstract_variables2(-,_AbstractModels,EncounteredIds) --> | |
| 417 | {!,empty_avl(EncounteredIds)}. | |
| 418 | get_all_abstract_variables2(Name,AbstractModels,EncounteredIds) --> | |
| 419 | {get_refined_model(Name,AbstractModels,Model), | |
| 420 | internal_model_refines(Model,_,Refines)}, | |
| 421 | get_all_abstract_variables2(Refines,AbstractModels,EncounteredIdsAbs), | |
| 422 | get_all_abstract_variables3(Model,EncounteredIdsAbs,EncounteredIds). | |
| 423 | get_all_abstract_variables3(Model,EncounteredIdsIn,EncounteredIdsOut, | |
| 424 | FoundVarsIn,FoundVarsOut) :- | |
| 425 | internal_model_vars(Model,_,Vars), | |
| 426 | extract_new_variables(Vars,EncounteredIdsIn,NewVars), | |
| 427 | get_texpr_ids(NewVars,NewIds), | |
| 428 | add_all_to_avl(NewIds,EncounteredIdsIn,EncounteredIdsOut), | |
| 429 | add_all(NewVars,FoundVarsIn,FoundVarsOut). | |
| 430 | add_all_to_avl([],Avl,Avl). | |
| 431 | add_all_to_avl([H|T],In,Out) :- | |
| 432 | avl_store(H,In,1,Inter), | |
| 433 | add_all_to_avl(T,Inter,Out). | |
| 434 | add_all([],L,L). | |
| 435 | add_all([H|T],[H|L1],L2) :- add_all(T,L1,L2). | |
| 436 | extract_new_variables([],_EncounteredIdsIn,[]). | |
| 437 | extract_new_variables([Var|Vrest],EncounteredIds,NewVars) :- | |
| 438 | get_texpr_id(Var,Id), | |
| 439 | ( avl_fetch(Id,EncounteredIds) -> | |
| 440 | NewVars = NewRest | |
| 441 | ; | |
| 442 | NewVars = [Var|NewRest]), | |
| 443 | extract_new_variables(Vrest,EncounteredIds,NewRest). | |
| 444 | ||
| 445 | ||
| 446 | ||
| 447 | ||
| 448 | ||
| 449 | check_events([],_ModelName,_Env,_GEnv,_InvEnv,_Dropped,_ConcreteVars,_AbstractEvents,_NewVars,_Variant,[]). | |
| 450 | check_events([RawEvent|RawRest],ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,[Event|Erest]) :- | |
| 451 | (check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event) | |
| 452 | -> true | |
| 453 | ; add_failed_call_error(check_event(RawEvent,ModelName,Env,GEnv,InvEnv, | |
| 454 | DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event))), | |
| 455 | check_events(RawRest,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Erest). | |
| 456 | ||
| 457 | ||
| 458 | check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVariables,Variant, | |
| 459 | tc_event(EvName,ModelName,Status,TParameters,TGuard,TTheorems,MActions, | |
| 460 | TVarWitnesses,TParamWitnesses,Unmodifiables,Refines,Desc) % type_checked internal event term | |
| 461 | ) :- | |
| 462 | raw_event(RawEvent,_,EvName,RawStatus,Refines,Params,Guards,Theorems,Actions,Witnesses,Desc), | |
| 463 | check_status(RawStatus, Variant, Status, Refines, AbstractEvents, eventlocation(ModelName,EvName)), | |
| 464 | get_abstract_parameters(Refines,AbstractEvents,AbstractParameters), | |
| 465 | create_identifiers(Params,[loc(ModelName,event(EvName))],TParameters), | |
| 466 | split_abstract_vars(AbstractParameters,TParameters, | |
| 467 | _NewParameters,DroppedParameters1), | |
| 468 | annotate_dropped_parameters(DroppedParameters1,Refines,AbstractEvents,DroppedParameters), | |
| 469 | conjunct_guards(Guards,Guard), % TODO: we could see if the guards appear at the abstract level with same label and use the abstract machine name, see M2_test_extends_grd_labels | |
| 470 | maplist(adapt_becomes_such,Actions,Actions1), | |
| 471 | % add new parameters to the typing environments: | |
| 472 | add_identifiers_to_environment(TParameters,Env,Subenv), | |
| 473 | add_identifiers_to_environment(TParameters,GEnv,SubGenv), | |
| 474 | add_identifiers_to_environment(TParameters,InvEnv,SubTheoremsEnv), % theorems can access dropped abstract variables; just like the invariant | |
| 475 | typecheck(Guard,Subenv,pred,TGuard,event(EvName,guard)), | |
| 476 | typecheck_l(Theorems,SubTheoremsEnv,pred,TTheorems,event(EvName,theorems)), | |
| 477 | typecheck_l(Actions1,Subenv,subst,TActions,event(EvName,actions)), | |
| 478 | check_witnesses(Witnesses,SubGenv,DroppedParameters,DroppedVars,TVarWitnesses,TParamWitnesses), | |
| 479 | % add checks that some variables may not be modified, e.g | |
| 480 | % if skip is refined | |
| 481 | get_abstract_actions(Refines,AbstractEvents,AbstractActions), | |
| 482 | add_modified_vars_to_actions(TActions,MActions1), | |
| 483 | add_unmodified_assignments(AbstractActions,MActions1,ConcreteVars,MActions), | |
| 484 | add_equality_check(MActions,AbstractActions,NewVariables,ConcreteVars,Unmodifiables). | |
| 485 | ||
| 486 | ||
| 487 | ||
| 488 | % -------------- | |
| 489 | ||
| 490 | % add assignments of the form x:=x if a not dropped abstract variable | |
| 491 | % is modified by the abstract event, but not the dropped event | |
| 492 | add_unmodified_assignments(AbstractActions,ConcreteActions,ConcreteVars,NewActions) :- | |
| 493 | get_modified_vars_of_actions(AbstractActions,AbstractModified), | |
| 494 | get_modified_vars_of_actions(ConcreteActions,ConcreteModified), | |
| 495 | remove_all(AbstractModified,ConcreteModified,OnlyAbstractModified), | |
| 496 | findall( Var, | |
| 497 | ( member(Id,OnlyAbstractModified), get_texpr_id(Var,Id), memberchk(Var,ConcreteVars)), | |
| 498 | ToKeep), | |
| 499 | ( ToKeep = [] -> NewActions = ConcreteActions | |
| 500 | ; ToKeep = [_|_] -> | |
| 501 | create_texpr(assign(ToKeep,ToKeep),subst,[],Action1), | |
| 502 | add_modified_vars_to_action(Action1,Action), | |
| 503 | NewActions = [Action|ConcreteActions]). | |
| 504 | ||
| 505 | check_status(RawStatus, Variant, TConv, Refines, AbstractEvents, Location) :- | |
| 506 | remove_pos(RawStatus,Status), | |
| 507 | check_status2(Status, Variant, Refines, AbstractEvents, Location, Conv, Infos), | |
| 508 | create_texpr(Conv, status, Infos, TConv). | |
| 509 | check_status2(ordinary, _Variant, _Refines, _AbstractEvents, _Location, ordinary, []). | |
| 510 | check_status2(convergent, _Variant, Refines, AbstractEvents, _Location, ordinary, [convergence_proved]) :- | |
| 511 | % if the refined event is also convergent, we can (or must because the | |
| 512 | % variant may be missing in the refinement) omit the check for decreasing the | |
| 513 | % variant. We do this by treating the event as ordinary. | |
| 514 | convergence_ensured_by_abstract_event(Refines, AbstractEvents),!. | |
| 515 | check_status2(convergent, Variant, _Refines, _AbstractEvents, Location, convergent(RVariant), [convergence_proved]) :- | |
| 516 | variant_must_be_set(Variant,Location,RVariant). | |
| 517 | check_status2(anticipated, Variant, _Refines, _AbstractEvents, _Location, anticipated(RVariant), []) :- | |
| 518 | get_variant(Variant,RVariant). | |
| 519 | ||
| 520 | :- use_module(tools_strings,[ajoin/2]). | |
| 521 | variant_must_be_set(-,Location,RVariant) :- !, | |
| 522 | Location = eventlocation(Model,Name), | |
| 523 | ajoin(['No variant defined for ', Name, ' in model ', Model],Msg), | |
| 524 | add_error(bmachine_eventb,Msg), | |
| 525 | get_variant(-,RVariant). | |
| 526 | % removed fail to allow animation | |
| 527 | variant_must_be_set(V,_,V). | |
| 528 | ||
| 529 | % get_variant(ModelVariant,Variant) checks profides a default variant (0) if | |
| 530 | % the model does not have a variant | |
| 531 | get_variant(-,V) :- !, create_texpr(integer(0),integer,[default_variant],V). | |
| 532 | get_variant(V,V). | |
| 533 | ||
| 534 | convergence_ensured_by_abstract_event(Refines, AbstractEvents) :- | |
| 535 | % find a refined event which status is convergent | |
| 536 | internal_event_status(Event,Ref,Status), | |
| 537 | get_texpr_info(Status,StatusInfo), | |
| 538 | member(Event, AbstractEvents), | |
| 539 | member(Ref, Refines), | |
| 540 | member(convergence_proved,StatusInfo),!. | |
| 541 | ||
| 542 | annotate_dropped_parameters([],_,_,[]). | |
| 543 | annotate_dropped_parameters([P|PRest],Refines,AbstractEvents,[A|ARest]) :- | |
| 544 | def_get_texpr_id(P,Id), | |
| 545 | add_texpr_infos(P,[droppedby(DropList)],A), | |
| 546 | findall(Event, event_drops_param(Event,Refines,AbstractEvents,Id), DropList), | |
| 547 | annotate_dropped_parameters(PRest,Refines,AbstractEvents,ARest). | |
| 548 | event_drops_param(Event,Refines,AbstractEvents,Id) :- | |
| 549 | get_texpr_id(Pattern,Id), | |
| 550 | member(Event,Refines), | |
| 551 | get_event_parameters(Event,AbstractEvents,AbParams), | |
| 552 | member(Pattern,AbParams). | |
| 553 | ||
| 554 | get_abstract_parameters([],_,R) :- !,R=[]. | |
| 555 | get_abstract_parameters([Refines|Rest],Events,Params) :- !, | |
| 556 | get_event_parameters(Refines,Events,LocalParams), | |
| 557 | append(LocalParams,RestParams,Params), | |
| 558 | get_abstract_parameters(Rest,Events,RestParams). | |
| 559 | get_abstract_parameters(Refines,_,Params) :- add_error(get_abstract_parameters,'Illegal Refines List: ',Refines), | |
| 560 | Params=[]. | |
| 561 | get_event_parameters(Refines,Events,Params) :- | |
| 562 | internal_event_params(Event,Refines,Params), | |
| 563 | member(Event,Events),!. | |
| 564 | ||
| 565 | get_abstract_actions([],_,[]). | |
| 566 | get_abstract_actions([Refines|Rest],Events,Actions) :- | |
| 567 | get_event_action(Refines,Events,LocalActions), | |
| 568 | append(LocalActions,RestActions,Actions), | |
| 569 | get_abstract_actions(Rest,Events,RestActions). | |
| 570 | get_event_action(Refines,Events,Actions) :- | |
| 571 | internal_event_actions(Event,Refines,Actions), | |
| 572 | member(Event,Events),!. | |
| 573 | ||
| 574 | check_witnesses([],_Env,_DroppedParams,_DroppedVars,[],[]). | |
| 575 | check_witnesses([Witness|Rest],Env,DroppedParams,DroppedVars,TVarWitnesses,TParamWitnesses) :- | |
| 576 | check_witness(Witness,Env,DroppedParams,DroppedVars,TWitness,WType), | |
| 577 | ( WType = droppedvar -> | |
| 578 | TVarWitnesses = [TWitness|TWVRest], | |
| 579 | TParamWitnesses = TWPRest | |
| 580 | ; WType = droppedparam(_DropList) -> | |
| 581 | TVarWitnesses = TWVRest, | |
| 582 | TParamWitnesses = [TWitness|TWPRest]), | |
| 583 | check_witnesses(Rest,Env,DroppedParams,DroppedVars,TWVRest,TWPRest). | |
| 584 | check_witness(witness(_Pos,RawId,Pred),Env,DroppedParams,DroppedVars,TWitness,WType) :- | |
| 585 | RawId = identifier(_,WitnessId), | |
| 586 | get_witness_identifier(WitnessId,DroppedParams,DroppedVars,TId,Info,WType), | |
| 587 | get_texpr_type(TId,Type), | |
| 588 | env_store(WitnessId,Type,Info,Env,Subenv), | |
| 589 | typecheck(Pred,Subenv,pred,TPred,witness), | |
| 590 | create_texpr(witness(TId,TPred),witness,[],TWitness). | |
| 591 | get_witness_identifier(PrimedId,_DroppedParams,DroppedVars,TPrimeId,[],droppedvar) :- | |
| 592 | prime_id(Id,PrimedId), | |
| 593 | get_texpr_id(TId,Id), | |
| 594 | member(TId,DroppedVars),!, | |
| 595 | prime_variables([TId],[TPrimeId]). | |
| 596 | get_witness_identifier(Id,DroppedParams,_DroppedVars,TId,Info,droppedparam(DropList)) :- | |
| 597 | get_texpr_id(TId,Id), | |
| 598 | member(TId,DroppedParams),!, | |
| 599 | get_texpr_info(TId,Info), | |
| 600 | member(droppedby(DropList),Info),!. | |
| 601 | ||
| 602 | conjunct_guards([],truth(none)). | |
| 603 | conjunct_guards([H|T],Result) :- conjunct_guards2(T,H,Result). | |
| 604 | conjunct_guards2([],G,G). | |
| 605 | conjunct_guards2([H|T],G,Result) :- conjunct_guards2(T,conjunct(none,G,H),Result). | |
| 606 | ||
| 607 | /* | |
| 608 | parallel_actions(Actions,Pos,Action) :- | |
| 609 | ( Actions = [] -> Action = skip(Pos) | |
| 610 | ; Actions = [S] -> Action = S | |
| 611 | ; Action = parallel(Pos,Actions)). | |
| 612 | */ | |
| 613 | ||
| 614 | % eventb becomes_such uses primed identifiers: distinguish it from normal becomes_such | |
| 615 | % ast_cleanup will translate it back to becomes_such, but with $0 instead of primes (so that it conforms to classical B) | |
| 616 | adapt_becomes_such(becomes_such(Pos,Ids,Pred),evb2_becomes_such(Pos,Ids,Pred)) :- !. | |
| 617 | adapt_becomes_such(Subst,Subst). | |
| 618 | ||
| 619 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 620 | % convert B project to classical B machine | |
| 621 | ||
| 622 | :- use_module(bmachine_structure,[create_machine/2]). | |
| 623 | ||
| 624 | convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine) :- | |
| 625 | debug_println(9,'Converting to classical B'), | |
| 626 | select_models(AnimationChain,Models,AnimatedModels), | |
| 627 | % todo: access to private elements of bmachine_construction | |
| 628 | create_machine(Main,Empty), | |
| 629 | convert_event_b2(Freetypes,Ops,AnimatedModels,Contextes,AnimationChain, | |
| 630 | Empty,Machine),!. | |
| 631 | convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine) :- | |
| 632 | add_failed_call_error(convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine)), | |
| 633 | fail. | |
| 634 | convert_event_b2(Freetypes,Ops,AnimatedModels,Contextes,AnimationChain) --> | |
| 635 | append_to_section(freetypes,Freetypes), | |
| 636 | %{format('Appending freetypes: ~w~n',[Freetypes])}, | |
| 637 | append_to_section(operators,Ops), | |
| 638 | %{format('Appending operators: ~w~n',[Ops])}, | |
| 639 | create_constants(AnimatedModels,Contextes,AnimatedContextNames), | |
| 640 | {append(AnimatedContextNames,AnimationChain,AnimatedSectionNames)}, | |
| 641 | create_variables(AnimatedModels,AnimatedSectionNames), | |
| 642 | create_events(AnimatedModels,AnimatedSectionNames), | |
| 643 | create_animated_section_info(AnimatedContextNames,AnimationChain). | |
| 644 | ||
| 645 | create_animated_section_info(Contextes,Models) --> | |
| 646 | {reverse(Models,FromAbstractToConcrete), | |
| 647 | maplist(mark_as_model,FromAbstractToConcrete,MarkedModels), | |
| 648 | maplist(mark_as_context,Contextes,MarkedContextes), | |
| 649 | append(MarkedContextes,MarkedModels,Sections)}, | |
| 650 | append_to_section(meta,[animated_sections(Sections)]). | |
| 651 | ||
| 652 | mark_as_model(Name,model(Name)). | |
| 653 | mark_as_context(Name,context(Name)). | |
| 654 | ||
| 655 | /* | |
| 656 | get_operation_identifiers([],[]). | |
| 657 | get_operation_identifiers([TExpr|Rest],[Id|IdRest]) :- | |
| 658 | get_texpr_expr(TExpr,operation(Id,_,_,_)), | |
| 659 | get_operation_identifiers(Rest,IdRest). | |
| 660 | */ | |
| 661 | ||
| 662 | create_variables(Models,AnimatedSectionNames) --> | |
| 663 | {collect_model_infos(Models,AnimatedSectionNames,Variables,Invariants,Theorems)}, | |
| 664 | append_to_section(abstract_variables,Variables), | |
| 665 | conjunct_to_section(invariant,Invariants), | |
| 666 | append_to_section(assertions,Theorems). | |
| 667 | ||
| 668 | select_contexts([],_Contexts,[]). | |
| 669 | select_contexts([Name|NRest],Contexts,[Context|CRest]) :- | |
| 670 | internal_context(Context,Name), | |
| 671 | memberchk(Context,Contexts), | |
| 672 | select_contexts(NRest,Contexts,CRest). | |
| 673 | ||
| 674 | select_models([],_Models,[]). | |
| 675 | select_models([Name|NRest],Models,[Model|MRest]) :- | |
| 676 | internal_model(Model,Name), memberchk(Model,Models), | |
| 677 | select_models(NRest,Models,MRest). | |
| 678 | ||
| 679 | % collect_model_infos(Models,Variables,Invariants,Theorems): | |
| 680 | % collect all variables, invariants and theorems of the given models | |
| 681 | collect_model_infos([],_,[],[],[]) :- !. | |
| 682 | collect_model_infos(Models,AnimatedSectionNames,Vars,Invs,Thms) :- | |
| 683 | collect_model_infos2(Models,AnimatedSectionNames,AllVars,Vars1,Invs,Thms), | |
| 684 | % add to every variable the information in which models | |
| 685 | % it is present | |
| 686 | add_var_model_occurrences(Vars1,AllVars,Vars). | |
| 687 | collect_model_infos2([],_,[],[],[],[]). | |
| 688 | collect_model_infos2([Model|MRest],AnimatedSectionNames,Vars,NewVars,Invs,Thms) :- | |
| 689 | internal_model_vars(Model,_,LVars), append(LVars,RVars,Vars), | |
| 690 | % use only newly introduced variables of a model, to prevent | |
| 691 | % double declarations | |
| 692 | % in case of a limited animation chain, it is important to introduce | |
| 693 | % all variables for the most abstract model | |
| 694 | (MRest == [] -> LNewVars = LVars ; internal_model_newvars(Model,_,LNewVars)), | |
| 695 | append(LNewVars,RNewVars,NewVars), | |
| 696 | internal_model_invs(Model,_,LInvs1), append_stripped_predicates(LInvs1,AnimatedSectionNames,RInvs,Invs), | |
| 697 | internal_model_thms(Model,_,LThms1), append_stripped_predicates(LThms1,AnimatedSectionNames,RThms,Thms), | |
| 698 | collect_model_infos2(MRest,AnimatedSectionNames,RVars,RNewVars,RInvs,RThms). | |
| 699 | add_var_model_occurrences([],_,[]). | |
| 700 | add_var_model_occurrences([Var|Vrest],AllVars,[MVar|Mrest]) :- | |
| 701 | add_var_model_occurrence(Var,AllVars,MVar), | |
| 702 | add_var_model_occurrences(Vrest,AllVars,Mrest). | |
| 703 | add_var_model_occurrence(Var,AllVars,MVar) :- | |
| 704 | findall(Section, | |
| 705 | ( find_identifier_in_list(Var,AllVars,M), | |
| 706 | get_texpr_info(M,Infos), | |
| 707 | member(section(Section),Infos)), | |
| 708 | Sections), | |
| 709 | reverse(Sections,FromAbstractToConcrete), | |
| 710 | add_texpr_infos(Var,[occurrences(FromAbstractToConcrete)],MVar). | |
| 711 | append_stripped_predicates(PredsIn,AnimatedSectionNames,RestPreds,Preds) :- | |
| 712 | remove_linking_parts(PredsIn,AnimatedSectionNames,LPreds), | |
| 713 | append(LPreds,RestPreds,Preds). | |
| 714 | ||
| 715 | all_used_contextes(AnimatedModels,Contextes,Sees) :- | |
| 716 | ( AnimatedModels = [] -> | |
| 717 | all_context_names(Contextes,Sees) | |
| 718 | ; | |
| 719 | collect_sees(AnimatedModels,Sees)). | |
| 720 | all_context_names([],[]). | |
| 721 | all_context_names([Context|Crest],[Name|Nrest]) :- | |
| 722 | internal_context(Context,Name), | |
| 723 | all_context_names(Crest,Nrest). | |
| 724 | collect_sees([],[]). | |
| 725 | collect_sees([Model|MRest],Sees) :- | |
| 726 | internal_model_sees(Model,_,LocalSees), append(LocalSees,RestSees,Sees), | |
| 727 | collect_sees(MRest,RestSees). | |
| 728 | ||
| 729 | create_constants(AnimatedModels,Contextes,AnimatedContextNames) --> | |
| 730 | {all_used_contextes(AnimatedModels,Contextes,Sees), | |
| 731 | get_constants(Sees,Contextes,DefSets,EnumSets,EnumElems,Constants,AbstractConstants,Axioms,Theorems,AnimatedContextNames)}, | |
| 732 | append_to_section(deferred_sets,DefSets), | |
| 733 | append_to_section(enumerated_sets,EnumSets), | |
| 734 | append_to_section(enumerated_elements,EnumElems), | |
| 735 | append_to_section(concrete_constants,Constants), | |
| 736 | append_to_section(abstract_constants,AbstractConstants), | |
| 737 | conjunct_to_section(properties,Axioms), | |
| 738 | append_to_section(assertions,Theorems). | |
| 739 | ||
| 740 | get_constants(Sees,Contextes,DefSets,EnumSets,EnumElems,Constants,AbstractConstants,Axioms,Theorems,AllContextNames) :- | |
| 741 | transitive_contextes(Sees,Contextes,AllContextNames), | |
| 742 | select_contexts(AllContextNames,Contextes,AllContextes), | |
| 743 | collect_context_infos(AllContextes,Sets,Constants1,AbstractConstants,Axioms1,Theorems), | |
| 744 | enumerated_deferred_sets(Sets,Constants1,Axioms1,DefSets,Constants,Axioms, | |
| 745 | EnumSets,EnumElems). | |
| 746 | ||
| 747 | collect_context_infos([],[],[],[],[],[]). | |
| 748 | collect_context_infos([context(Name,_Ex,LSets1,LCsts1,LAbsCsts1,LAxms,LThms)|Rest],Sets,Constants,AbstractConstants,Axioms,Theorems) :- | |
| 749 | add_context_occurrences(LSets1,Name,LSets), | |
| 750 | add_context_occurrences(LCsts1,Name,LCsts), | |
| 751 | add_context_occurrences(LAbsCsts1,Name,LAbsCsts), | |
| 752 | append(LSets,RSets,Sets), | |
| 753 | append(LCsts,RCsts,Constants), | |
| 754 | append(LAbsCsts,RAbsCsts,AbstractConstants), | |
| 755 | append(LAxms,RAxms,Axioms), | |
| 756 | append(LThms,RThms,Theorems), | |
| 757 | collect_context_infos(Rest,RSets,RCsts,RAbsCsts,RAxms,RThms). | |
| 758 | add_context_occurrences([],_,[]). | |
| 759 | add_context_occurrences([Constant|Crest],Name,[CC|CCrest]) :- | |
| 760 | add_texpr_infos(Constant,[occurrences([Name])],CC), | |
| 761 | add_context_occurrences(Crest,Name,CCrest). | |
| 762 | ||
| 763 | ||
| 764 | % merge the events and write them to a machine | |
| 765 | create_events(AnimatedModels,AnimatedSectionNames) --> | |
| 766 | {get_events(AnimatedModels,AnimatedSectionNames,Events,Initialisation,Promoted)}, | |
| 767 | append_to_section(operation_bodies,Events), | |
| 768 | bmachine_construction:write_section(initialisation,Initialisation), | |
| 769 | append_to_section(promoted,Promoted). | |
| 770 | ||
| 771 | % merge the events of multiple refinement levels | |
| 772 | get_events([],_,[],Initialisation,[]) :- !, | |
| 773 | create_texpr(skip,subst,[],Initialisation). | |
| 774 | get_events(AnimatedModels,AnimatedSectionNames,Events,Initialisation,Promoted) :- | |
| 775 | get_events_to_animate(AnimatedModels,AnimEvents), | |
| 776 | merge_refinement_levels(AnimEvents,AnimatedModels,AnimatedSectionNames,MergedEvents,Promoted1), | |
| 777 | remove_initialisation(Promoted1,Promoted2), | |
| 778 | add_op_parenthesis(Promoted2,Promoted), | |
| 779 | select_initialisation(MergedEvents,PreOps,Initialisation), | |
| 780 | create_operations(PreOps,Events). | |
| 781 | remove_initialisation(In,Out) :- | |
| 782 | get_texpr_id(Expr,'INITIALISATION'), | |
| 783 | select(Expr,In,Out),!. | |
| 784 | remove_initialisation(In,Out) :- | |
| 785 | % add_error(check_event_b_project,'Model has no INITIALISATION'), %err msg already generated below | |
| 786 | Out=In. | |
| 787 | add_op_parenthesis([],[]). | |
| 788 | add_op_parenthesis([Old|ORest],[New|NRest]) :- | |
| 789 | def_get_texpr_id(Old,Id), | |
| 790 | rename_bt(Old,[rename(Id,op(Id))],New), | |
| 791 | add_op_parenthesis(ORest,NRest). | |
| 792 | ||
| 793 | select_initialisation(In,Ops,Init) :- | |
| 794 | select(eventop('INITIALISATION',Section,[],Init1,op([],[]),_),In,Ops),!, | |
| 795 | add_texpr_infos(Init1,[eventb(Section)],Init). | |
| 796 | select_initialisation(In,Ops,Init) :- | |
| 797 | add_error(select_initialisation,'Model has no INITIALISATION'), | |
| 798 | Init = b(skip,subst,[]), % replace skip by non-det assign | |
| 799 | Ops=In. | |
| 800 | create_operations([],[]). | |
| 801 | create_operations([E|ERest],[O|ORest]) :- | |
| 802 | create_operation(E,O), | |
| 803 | create_operations(ERest,ORest). | |
| 804 | create_operation(eventop(Name,Section,Parameters,Subst,Type,Refines),Operation) :- | |
| 805 | create_texpr(identifier(op(Name)),Type,[],Id), | |
| 806 | get_texpr_info(Subst,SubstInfo), | |
| 807 | Mod=modifies(_),memberchk(Mod,SubstInfo), | |
| 808 | Reads=reads(_),memberchk(Reads,SubstInfo), | |
| 809 | (Refines == [] -> RefInfo = RestInfo ; RefInfo = [refines(Refines)|RestInfo]), | |
| 810 | (extract_description(Subst,Desc) -> RestInfo = [description(Desc)] ; RestInfo=[]), % we could also do a findall | |
| 811 | create_texpr(operation(Id,[],Parameters,Subst),Type,[eventb(Section),Mod,Reads|RefInfo],Operation). | |
| 812 | ||
| 813 | :- use_module(probsrc(bsyntaxtree),[get_texpr_description/2, get_texpr_labels/2]). | |
| 814 | extract_description(Subst,Desc) :- | |
| 815 | get_texpr_description(Subst,Desc). | |
| 816 | extract_description(Subst,Desc) :- get_direct_abstract_event(Subst,ASubst), | |
| 817 | extract_description(ASubst,Desc). | |
| 818 | ||
| 819 | get_direct_abstract_event(b(RefLvlEvent,subst,_),AbsEvent) :- | |
| 820 | RefLvlEvent = rlevent(_Name,_Sect,_Stat,_Paras,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,AbsEvents), | |
| 821 | member(AbsEvent,AbsEvents). | |
| 822 | ||
| 823 | get_events_to_animate([Model|_],Events) :- internal_model_events(Model,_,Events). | |
| 824 | ||
| 825 | merge_refinement_levels([],_,_,[],[]). | |
| 826 | merge_refinement_levels([Event|ERest],AnimModels,AnimatedSectionNames,[Merged|MRest],[Prom|PRest]) :- | |
| 827 | merge_refinement_levels2(Event,AnimModels,AnimatedSectionNames,Merged,Prom), | |
| 828 | merge_refinement_levels(ERest,AnimModels,AnimatedSectionNames,MRest,PRest). | |
| 829 | ||
| 830 | merge_refinement_levels2(Event,AnimatedLevels,AnimatedSectionNames, | |
| 831 | eventop(Name,Section,Parameters,Subst,OpType,Refines),Prom) :- | |
| 832 | AnimatedLevels = [CurrentLevel|_Abstractions], | |
| 833 | internal_model(CurrentLevel,Section), | |
| 834 | internal_event_params(Event,Name,Parameters), | |
| 835 | internal_event_refined(Event,Name,Refines), | |
| 836 | %merge_parameters(Refines,Parameters,_Abstractions,MergedParameters), | |
| 837 | merge_events_to_subst(Name,AnimatedLevels,AnimatedSectionNames,[],Subst1), | |
| 838 | optimise_events(Subst1,Subst), | |
| 839 | get_texpr_types(Parameters,Types),OpType = op(Types,[]), | |
| 840 | create_texpr(identifier(Name),OpType,[],Prom). | |
| 841 | ||
| 842 | gen_description_term(Desc,description(Desc)). | |
| 843 | ||
| 844 | merge_events_to_subst(Name,[CurrentLevel|Abstractions],AnimatedSectionNames,RefinedParameters,TEvent) :- | |
| 845 | create_texpr(RefLevelEvent,subst,[modifies(Vars),reads(Reads)|RestInfos],TEvent), | |
| 846 | RefLevelEvent = rlevent(Name,Section,Status,Params,Guard,Theorems,Actions, | |
| 847 | VWitnesses,PWitnesses,Unmodifiables,AbstractEvents), | |
| 848 | InternalEvent = tc_event(Name,Section,Status,AllParams,Guard,Theorems,Actions, | |
| 849 | VWitnesses1,PWitnesses1,Unmodifiables,Refines,Desc), | |
| 850 | get_event_from_model(Name,CurrentLevel,InternalEvent), | |
| 851 | strip_witnesses(VWitnesses1,AnimatedSectionNames,VWitnesses), | |
| 852 | strip_witnesses(PWitnesses1,AnimatedSectionNames,PWitnesses), | |
| 853 | remove_refined_parameters(AllParams,RefinedParameters,Params), | |
| 854 | maplist(gen_description_term,Desc,RestInfos), | |
| 855 | ( Abstractions = [] -> | |
| 856 | AbstractEvents = [] | |
| 857 | ; | |
| 858 | append(RefinedParameters,Params,NewRefinedParameters), | |
| 859 | merge_events_to_subst_l(Refines,Abstractions,AnimatedSectionNames,NewRefinedParameters,AbstractEvents1), | |
| 860 | normalise_merged_events(AbstractEvents1,AbstractEvents) | |
| 861 | ), | |
| 862 | collect_modified_vars(Actions,AbstractEvents,Vars), | |
| 863 | collect_read_vars(Status,AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents,Reads). | |
| 864 | merge_events_to_subst_l([],_,_,_,[]). | |
| 865 | merge_events_to_subst_l([Name|NRest],Abstractions,AnimatedSectionNames,RefinedParameters,[TEvent|TRest]) :- | |
| 866 | merge_events_to_subst(Name,Abstractions,AnimatedSectionNames,RefinedParameters,TEvent), | |
| 867 | merge_events_to_subst_l(NRest,Abstractions,AnimatedSectionNames,RefinedParameters,TRest). | |
| 868 | ||
| 869 | % removes a witness completely if the witnessed variable belongs | |
| 870 | % to a refinement level that is not animated or removes part of the | |
| 871 | % witness-predicate if references to not animated levels are made. | |
| 872 | strip_witnesses([],_AnimatedSectionNames,[]). | |
| 873 | strip_witnesses([Witness|WRest],AnimatedSectionNames,Result) :- | |
| 874 | strip_witness(Witness,AnimatedSectionNames,StrippedWitness), | |
| 875 | append(StrippedWitness,SWRest,Result), | |
| 876 | strip_witnesses(WRest,AnimatedSectionNames,SWRest). | |
| 877 | strip_witness(Witness,AnimatedSectionNames,StrippedWitness) :- | |
| 878 | get_texpr_expr(Witness,witness(W,P)), | |
| 879 | ( abstraction_var_occures(W,AnimatedSectionNames) -> | |
| 880 | % The abstract variable is not animated, skip the complete witness | |
| 881 | StrippedWitness = [] | |
| 882 | ; | |
| 883 | conjunction_to_list(P,Preds), | |
| 884 | remove_linking_parts(Preds,AnimatedSectionNames,SPreds), | |
| 885 | conjunct_predicates(SPreds,SP), | |
| 886 | get_texpr_type(Witness,Type), | |
| 887 | get_texpr_info(Witness,Info), | |
| 888 | create_texpr(witness(W,SP),Type,Info,TWitness), | |
| 889 | StrippedWitness = [TWitness]). | |
| 890 | ||
| 891 | remove_refined_parameters([],_RefinedParameters,[]). | |
| 892 | remove_refined_parameters([Param|APRest],RefinedParameters,Parameters) :- | |
| 893 | ( find_identifier_in_list(Param,RefinedParameters,_RefParam) -> | |
| 894 | Parameters = PRest | |
| 895 | ; | |
| 896 | Parameters = [Param|PRest]), | |
| 897 | remove_refined_parameters(APRest,RefinedParameters,PRest). | |
| 898 | ||
| 899 | /* currently commented out : | |
| 900 | merge_parameters([],Parameters,_Abstractions,Parameters). | |
| 901 | merge_parameters([_|_],Parameters,[],Parameters) :- !. | |
| 902 | merge_parameters([Refines|Rest],OldParameters,Abstractions,Parameters) :- | |
| 903 | Abstractions = [Abstract|FurtherAbstractions], | |
| 904 | get_event_from_model(Refines,Abstract,Event), | |
| 905 | internal_event_params(Event,_,NewParameters), | |
| 906 | internal_event_refined(Event,_,NewRefines), | |
| 907 | add_unique_parameters(NewParameters,OldParameters,Parameters2), | |
| 908 | merge_parameters(NewRefines,Parameters2,FurtherAbstractions,Parameters3), | |
| 909 | merge_parameters(Rest,Parameters3,Abstractions,Parameters). | |
| 910 | add_unique_parameters([],Parameters,Parameters). | |
| 911 | add_unique_parameters([P|PRest],InParameters,OutParameters) :- | |
| 912 | ( find_identifier_in_list(P,InParameters,_) -> | |
| 913 | !,Parameters = InParameters | |
| 914 | ; | |
| 915 | Parameters = [P|InParameters]), | |
| 916 | add_unique_parameters(PRest,Parameters,OutParameters). | |
| 917 | */ | |
| 918 | ||
| 919 | get_event_from_model(Name,Model,Event) :- | |
| 920 | internal_model_events(Model,_,Events), | |
| 921 | internal_event(Event,Name), | |
| 922 | member(Event,Events),!. | |
| 923 | ||
| 924 | collect_modified_vars(Actions,Events,Vars) :- | |
| 925 | get_modified_vars_of_actions(Actions,M1), | |
| 926 | append_modified_vars_of_events(Events,M2), | |
| 927 | append(M1,M2,M3),sort(M3,Vars). | |
| 928 | get_modified_vars_of_actions([],[]). | |
| 929 | get_modified_vars_of_actions([Action|Arest],Vars) :- | |
| 930 | get_modified_vars_of_action(Action,Vlocal), | |
| 931 | append(Vlocal,Vrest,Vars), | |
| 932 | get_modified_vars_of_actions(Arest,Vrest). | |
| 933 | get_modified_vars_of_action(Action,Vars) :- | |
| 934 | get_texpr_info(Action,Infos), | |
| 935 | member(modifies(Vars), Infos),!. | |
| 936 | ||
| 937 | add_modified_vars_to_actions([],[]). | |
| 938 | %add_modified_vars_to_actions([TAction|ARest],MRest) :- | |
| 939 | % get_texpr_expr(TAction,skip),!, % remove skip actions % for Daniel: is this better than keeping them ?? | |
| 940 | % add_modified_vars_to_actions(ARest,MRest). | |
| 941 | add_modified_vars_to_actions([TAction|ARest],[MAction|MRest]) :- | |
| 942 | (add_modified_vars_to_action(TAction,MAction) ->true | |
| 943 | ; add_internal_error('Call failed: ',add_modified_vars_to_action(TAction,MAction)), | |
| 944 | MAction = TAction), | |
| 945 | add_modified_vars_to_actions(ARest,MRest). | |
| 946 | add_modified_vars_to_action(TAction,MAction) :- | |
| 947 | get_lhs_ids(TAction,Vars), | |
| 948 | maplist(prime_id,Vars,Primed), | |
| 949 | add_texpr_infos(TAction,[assigned_after(Primed),modifies(Vars)],MAction). | |
| 950 | ||
| 951 | get_lhs_ids(TAction,Ids) :- | |
| 952 | get_lhs_tids(TAction,Vars), | |
| 953 | get_texpr_ids(Vars,Ids). | |
| 954 | get_lhs_tids(TAction,Vars) :- | |
| 955 | get_texpr_expr(TAction,Action), | |
| 956 | split_lhs_rhs(Action,Lhs,_), | |
| 957 | extract_lhs_ids(Lhs,Vars). | |
| 958 | ||
| 959 | split_lhs_rhs(skip,[],[]). % not needed as skip removed above | |
| 960 | split_lhs_rhs(assign(Ids,Exprs),Ids,Exprs). | |
| 961 | split_lhs_rhs(assign_single_id(Id,Expr),[Id],[Expr]). | |
| 962 | split_lhs_rhs(becomes_element_of(Ids,Expr),Ids,[Expr]). | |
| 963 | split_lhs_rhs(becomes_such(Ids,Pred),Ids,[Pred]). | |
| 964 | split_lhs_rhs(evb2_becomes_such(Ids,Pred),Ids,[Pred]). | |
| 965 | extract_lhs_ids([],[]). | |
| 966 | extract_lhs_ids([TId|TRest],[Var|VRest]) :- | |
| 967 | extract_lhs_id(TId,Var), | |
| 968 | extract_lhs_ids(TRest,VRest). | |
| 969 | extract_lhs_id(Id,Var) :- | |
| 970 | get_texpr_id(Id,_),!,Var=Id. | |
| 971 | extract_lhs_id(Func,Var) :- | |
| 972 | get_texpr_expr(Func,function(Id,_)), | |
| 973 | get_texpr_id(Id,Var). | |
| 974 | ||
| 975 | append_modified_vars_of_events(Events,Vars) :- | |
| 976 | append_modified_vars_of_events2(Events,Unsorted), | |
| 977 | sort(Unsorted,Vars). | |
| 978 | append_modified_vars_of_events2([],[]). | |
| 979 | append_modified_vars_of_events2([TEvent|ERest],Vars) :- | |
| 980 | get_modified_vars_of_event(TEvent,Local), | |
| 981 | append(Local,VRest,Vars), | |
| 982 | append_modified_vars_of_events2(ERest,VRest). | |
| 983 | get_modified_vars_of_event(TEvent,Local) :- | |
| 984 | get_texpr_info(TEvent,Info), | |
| 985 | memberchk(modifies(Local),Info). | |
| 986 | ||
| 987 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 988 | % get all the variables that are accessed in an event (cf also get_accessed_vars2 in b_read_write_info.pl) | |
| 989 | collect_read_vars(Status,AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents,Reads) :- | |
| 990 | find_variant_reads([],Status,VariantVars), % the variant cannot use params (!?) | |
| 991 | get_texpr_ids(AllParams,Params), % access to parameters is not reading a variable | |
| 992 | find_identifier_uses(Guard,Params,GrdVars), | |
| 993 | find_identifier_uses_l(Theorems,Params,ThmVars), | |
| 994 | find_identifier_uses_l(Unmodifiables,Params,UnmodVars), % for check_if_invalid_vars_are_modified we need read access | |
| 995 | maplist(find_all_action_reads(Params),Actions,ActVars0), ord_union(ActVars0, ActVars), | |
| 996 | maplist(find_all_witness_reads(Params),VWitnesses,VWitVars0), ord_union(VWitVars0,VWitVars), | |
| 997 | maplist(find_all_witness_reads(Params),PWitnesses,PWitVars0), ord_union(PWitVars0,PWitVars), | |
| 998 | join_abstract_reads(AbstractEvents,AbstrVars), | |
| 999 | ord_union([VariantVars,GrdVars,ThmVars,UnmodVars,ActVars,VWitVars,PWitVars,AbstrVars],Reads). | |
| 1000 | ||
| 1001 | find_variant_reads(Ignore,TVariant,Res) :- | |
| 1002 | get_texpr_expr(TVariant,Variant), | |
| 1003 | (find_variant_reads2(Variant,Ignore,Vars) -> Res=Vars | |
| 1004 | ; add_internal_error('Illegal variant: ',find_variant_reads2(Variant,Ignore,_)),Res=[]). | |
| 1005 | find_variant_reads2(convergent(TExpr),Ignore,Vars) :- find_identifier_uses(TExpr,Ignore,Vars). | |
| 1006 | find_variant_reads2(anticipated(TExpr),Ignore,Vars) :- find_identifier_uses(TExpr,Ignore,Vars). | |
| 1007 | find_variant_reads2(ordinary,_,[]). | |
| 1008 | ||
| 1009 | %find_all_identifiers(Ignore,Expr,Vars) :- | |
| 1010 | % find_identifier_uses(Expr,Ignore,Vars). % Just switch arguments to allow the use of maplist | |
| 1011 | find_all_action_reads(Ignore,TAction,Res) :- | |
| 1012 | get_texpr_expr(TAction,Action), | |
| 1013 | (find_action_reads2(Action,Ignore,Vars) -> Res=Vars | |
| 1014 | ; add_internal_error('Illegal action: ',find_action_reads2(Action,Ignore,_)),Res=[]). | |
| 1015 | find_action_reads2(skip,_,Vars) :- Vars=[]. | |
| 1016 | find_action_reads2(assign(_,Exprs),Ignore,Vars) :- find_identifier_uses_l(Exprs,Ignore,Vars). | |
| 1017 | find_action_reads2(assign_single_id(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars). | |
| 1018 | find_action_reads2(becomes_element_of(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars). | |
| 1019 | find_action_reads2(becomes_such(Ids,Pred),Ignore,Vars1) :- | |
| 1020 | % all references to Ids are to the state after: not a read | |
| 1021 | get_texpr_ids(Ids,AtomicIds), | |
| 1022 | append(AtomicIds,Ignore,Ignore0),sort(Ignore0,Ignore1), | |
| 1023 | find_identifier_uses(Pred,Ignore1,Vars), | |
| 1024 | prime_identifiers0(Ids,Ids0), % Ids with $0 afterwards | |
| 1025 | get_texpr_ids(Ids0,AtomicIds0), | |
| 1026 | maplist(unprime_id(AtomicIds0,AtomicIds),Vars,Vars1). | |
| 1027 | %find_action_reads2(evb2_becomes_such(Ids,Pred),Ignore,Vars) :- | |
| 1028 | % prime_variables(Ids,PIds),get_texpr_ids(PIds,Primes), | |
| 1029 | % append(Primes,Ignore,Ignore0),sort(Ignore0,Ignore1), | |
| 1030 | % find_identifier_uses(Pred,Ignore1,Vars). | |
| 1031 | find_all_witness_reads(Ignore,Witness,Vars) :- | |
| 1032 | get_texpr_expr(Witness,witness(I,P)), | |
| 1033 | get_texpr_id(I,Id), | |
| 1034 | sort([Id|Ignore],Ignore2), | |
| 1035 | find_identifier_uses(P,Ignore2,Vars1), | |
| 1036 | % a small hack to remove the primed variables that refer to the after-state | |
| 1037 | % without the need to put all variables in the Ingore list: | |
| 1038 | exclude(is_primed_id,Vars1,Vars). | |
| 1039 | ||
| 1040 | join_abstract_reads([],[]) :- !. | |
| 1041 | join_abstract_reads(AbstractEvents,Reads) :- | |
| 1042 | maplist(get_read_from_info,AbstractEvents,AbsReads), | |
| 1043 | ord_union(AbsReads,ReadBySome), | |
| 1044 | maplist(get_modifies_from_info,AbstractEvents,AbsModifies), | |
| 1045 | ord_union(AbsModifies,ModifiedBySome), | |
| 1046 | ord_intersection(AbsModifies,ModifiedByAll), | |
| 1047 | ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll), | |
| 1048 | ord_union(ReadBySome,ModifiedByNotAll,Reads). | |
| 1049 | get_read_from_info(AbstrEvents,Reads) :- | |
| 1050 | get_texpr_info(AbstrEvents,Info),memberchk(reads(Reads),Info). | |
| 1051 | get_modifies_from_info(AbstrEvents,Modifies) :- | |
| 1052 | get_texpr_info(AbstrEvents,Info),memberchk(modifies(Modifies),Info). | |
| 1053 | ||
| 1054 | add_equality_check(Actions,AbstractActions,NewVars,Variables,Unmodifiables) :- | |
| 1055 | get_modified_vars_of_actions(Actions,Modified), | |
| 1056 | get_modified_vars_of_actions(AbstractActions,AbstractModified), | |
| 1057 | unmodifiables(Modified,AbstractModified,NewVars,Variables,Unmodifiables). | |
| 1058 | unmodifiables([],_AbstractModified,_NewVars,_Variables,[]). | |
| 1059 | unmodifiables([UM|Modified],AbstractModified,NewVars,Variables,Unmodifiables) :- | |
| 1060 | ( is_modifiable(UM,AbstractModified,NewVars) -> | |
| 1061 | Unmodifiables = UMrest | |
| 1062 | ; | |
| 1063 | get_texpr_id(TUM,UM), | |
| 1064 | member(TUM,Variables),!, | |
| 1065 | Unmodifiables = [TUM|UMrest]), | |
| 1066 | unmodifiables(Modified,AbstractModified,NewVars,Variables,UMrest). | |
| 1067 | % the abstract event modifies it, so we can do it, too | |
| 1068 | is_modifiable(UM,AbstractModified,_NewVars) :- member(UM,AbstractModified),!. | |
| 1069 | % the variables is newly introduced, so we can modifiy it | |
| 1070 | is_modifiable(UM,_AbstractModified,NewVars) :- | |
| 1071 | get_texpr_id(TUM,UM), member(TUM,NewVars). | |
| 1072 | ||
| 1073 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1074 | % normalising merged events means that if two refined events A and B | |
| 1075 | % change a different set of variables then the event A gets an additional | |
| 1076 | % assignment of the form x:=x with x as a variable that is changed in B | |
| 1077 | % but not in A. | |
| 1078 | % This can happen even though merged events have the same assignments because | |
| 1079 | % they again can refine events that have different assignments. | |
| 1080 | ||
| 1081 | % None or one refined event do not have to be normalised | |
| 1082 | normalise_merged_events([],[]) :- !. | |
| 1083 | normalise_merged_events([E],[E]) :- !. | |
| 1084 | normalise_merged_events(Events,Normalised) :- | |
| 1085 | append_modified_vars_of_events(Events,AllModifiedVars), | |
| 1086 | find_typed_version_in_events(AllModifiedVars,Events,TypedVars), | |
| 1087 | normalise_merged_events2(Events,AllModifiedVars,TypedVars,Normalised). | |
| 1088 | normalise_merged_events2([],_AllModifiedVars,_TypedVars,[]). | |
| 1089 | normalise_merged_events2([Event|Erest],AllModifiedVars,TypedVars,[Normalised|Nrest]) :- | |
| 1090 | normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised), | |
| 1091 | normalise_merged_events2(Erest,AllModifiedVars,TypedVars,Nrest). | |
| 1092 | normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised) :- | |
| 1093 | get_modified_vars_of_event(Event,Modified), | |
| 1094 | remove_all(AllModifiedVars,Modified,MissingVars), | |
| 1095 | add_missing_assignments(MissingVars,Event,AllModifiedVars,TypedVars,Normalised). | |
| 1096 | add_missing_assignments([],Event,_,_,Event) :- !. | |
| 1097 | add_missing_assignments(MissingVars,TEvent,AllModifiedVars,TypedVars,Normalised) :- | |
| 1098 | get_texpr_expr(TEvent,Event), | |
| 1099 | get_texpr_type(TEvent,Type), | |
| 1100 | get_texpr_info(TEvent,Infos), | |
| 1101 | selectchk(modifies(_),Infos,RestInfos), % TO DO: also add reads Information | |
| 1102 | create_texpr(NewEvent,Type,[modifies(AllModifiedVars)|RestInfos],Normalised), | |
| 1103 | Event = rlevent(Name,Sec,St,Prm,Grd,Thm,Actions,VWit,PWit,Unmod,AbsEvents), | |
| 1104 | NewEvent = rlevent(Name,Sec,St,Prm,Grd,Thm,NewActions,VWit,PWit,Unmod,AbsEvents), | |
| 1105 | append(Actions,NewAssignments,NewActions), | |
| 1106 | create_missing_assignments(MissingVars,TypedVars,NewAssignments). | |
| 1107 | create_missing_assignments([],_TypedVars,[]). | |
| 1108 | create_missing_assignments([MissingVar|Mrest],TypedVars,[Assign|Arest]) :- | |
| 1109 | create_missing_assignment(MissingVar,TypedVars,Assign), | |
| 1110 | create_missing_assignments(Mrest,TypedVars,Arest). | |
| 1111 | create_missing_assignment(Var,TypedVars,Assignment) :- | |
| 1112 | get_texpr_id(TId,Var), | |
| 1113 | memberchk(TId,TypedVars), | |
| 1114 | prime_id(Var,Primed), | |
| 1115 | create_texpr(assign([TId],[TId]),subst,[assigned_after(Primed),modifies(Var)],Assignment). | |
| 1116 | ||
| 1117 | find_typed_version_in_events([],_Events,[]). | |
| 1118 | find_typed_version_in_events([Name|Nrest],Events,[Typed|Trest]) :- | |
| 1119 | find_typed_version_in_events2(Name,Events,Typed), | |
| 1120 | find_typed_version_in_events(Nrest,Events,Trest). | |
| 1121 | find_typed_version_in_events2(Name,Events,Typed) :- | |
| 1122 | get_texpr_id(Typed,Name), | |
| 1123 | member(Event,Events), | |
| 1124 | get_texpr_expr(Event,rlevent(_Name,_Sec,_St,_Prm,_Grd,_Thm,Actions,_VWit,_PWit,_Unmod,AbsEvents)), | |
| 1125 | find_typed_version_in_events3(Name,Actions,AbsEvents,Typed),!. | |
| 1126 | find_typed_version_in_events3(_Name,Actions,_AbsEvents,Typed) :- | |
| 1127 | member(Action,Actions), | |
| 1128 | get_lhs_tids(Action,Vars), | |
| 1129 | member(Typed,Vars),!. | |
| 1130 | find_typed_version_in_events3(Name,_Actions,AbsEvents,Typed) :- | |
| 1131 | find_typed_version_in_events2(Name,AbsEvents,Typed). | |
| 1132 | ||
| 1133 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1134 | % optimisation of guards: | |
| 1135 | % A guard in a refinement does not need to be evaluated in in an abstract event | |
| 1136 | % again. This happens quiet frequently, especially if "extends" is used. | |
| 1137 | % The same applies for assignments: If in a refinement an action is performed, | |
| 1138 | % we do not have to check if the same action can be performed in a more abstract | |
| 1139 | % level. | |
| 1140 | optimise_events(TEvent,NTEvent) :- | |
| 1141 | empty_avl(Empty), | |
| 1142 | optimise_events2(Empty,TEvent,NTEvent). | |
| 1143 | optimise_events2(KnownElements,TEvent,NTEvent) :- | |
| 1144 | create_texpr(Event,Type,Infos,TEvent), | |
| 1145 | create_texpr(NewEvent,Type,Infos,NTEvent), | |
| 1146 | Event = rlevent(Name,Section,Status,Params,OldGuard,OldTheorems,OldActions, | |
| 1147 | VWitnesses,PWitnesses,Unmodifiables,OldAbstractEvents), | |
| 1148 | NewEvent = rlevent(Name,Section,Status,Params,NewGuard,NewTheorems,NewActions, | |
| 1149 | VWitnesses,PWitnesses,Unmodifiables,NewAbstractEvents), | |
| 1150 | optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,KnownElements1), | |
| 1151 | optimise_formulas(OldActions,KnownElements1,NewActions,NewKnownElements), | |
| 1152 | maplist(optimise_events2(NewKnownElements),OldAbstractEvents,NewAbstractEvents). | |
| 1153 | optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,NewKnownElements) :- | |
| 1154 | conjunction_to_list(OldGuard,OldGuards), | |
| 1155 | optimise_formulas(OldGuards,KnownElements,NewGuards,KnownElements1), | |
| 1156 | % If no elements were removed, we just use the old guard | |
| 1157 | (OldGuards=NewGuards -> OldGuard=NewGuard ; conjunct_predicates(NewGuards,NewGuard)), | |
| 1158 | optimise_formulas(OldTheorems,KnownElements1,NewTheorems,NewKnownElements). | |
| 1159 | % optimise_formulas(+AllFormulas,+KnownElements,-NewFormulas,-NewNormed) | |
| 1160 | % AllFormulas: A list of formulas | |
| 1161 | % KnownElementes: A list of normed versions of already encountered elements | |
| 1162 | % NewFormulas: A sub-list of AllFormulas which are new (not in KnownElements) | |
| 1163 | % NewKnownElements: The updated list of already encountered elements | |
| 1164 | % If no formulas are removed, it is guaranteed that NewFormulas=AllFormulas | |
| 1165 | optimise_formulas(AllFormulas,KnownElements,NewFormulas,NewKnownElements) :- | |
| 1166 | % convert formulas to a list: Formula/Normed where Normed is a normalised form | |
| 1167 | maplist(add_stripped_ast,AllFormulas,AllFormNormed), | |
| 1168 | % remove the already known formulas | |
| 1169 | exclude(is_duplicate_formula(KnownElements),AllFormNormed,NewFormNormed), | |
| 1170 | % split the list [Form/Normed] into [Form] and [Normed] | |
| 1171 | maplist(unzipslash,NewFormNormed,NewFormulas1,NewNormed), | |
| 1172 | ( AllFormNormed = NewFormNormed -> % No formulas removed, keep everything as it is | |
| 1173 | NewFormulas = AllFormulas | |
| 1174 | ; | |
| 1175 | NewFormulas = NewFormulas1 | |
| 1176 | ), | |
| 1177 | foldl(add_to_known_elements,NewNormed,KnownElements,NewKnownElements). | |
| 1178 | add_stripped_ast(Formula,Formula/Stripped) :- | |
| 1179 | strip_and_norm_ast(Formula,Stripped). | |
| 1180 | is_duplicate_formula(KnownElements,_Formula/Stripped) :- | |
| 1181 | avl_fetch(Stripped,KnownElements). % remark: if some ast_cleanup operations introduce fresh identifiers (e.g., comp_result) then we may not detect formulas as identical here ! | |
| 1182 | unzipslash(A/B,A,B). | |
| 1183 | add_to_known_elements(New,In,Out) :- | |
| 1184 | avl_store(New,In,true,Out). | |
| 1185 | ||
| 1186 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1187 | % internal event handling (just data structure) | |
| 1188 | internal_event(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name). | |
| 1189 | internal_event_status(tc_event(Name,_Section,Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Status). | |
| 1190 | internal_event_params(tc_event(Name,_Section,_Status,Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Params). | |
| 1191 | %internal_event_guards(tc_event(Name,_Section,_Status,_Params,Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Grd). | |
| 1192 | internal_event_actions(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Act). | |
| 1193 | internal_event_refined(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,Ref,_),Name,Ref). | |
| 1194 | %internal_event_description(tc_event(_,_,_,_,_,_,_,_,_,_,_,DescList),Desc) :- member(Desc,DescList). | |
| 1195 | ||
| 1196 | internal_context(context(Name,_Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name). | |
| 1197 | internal_context_extends(context(Name,Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Extends). | |
| 1198 | internal_context_sets(context(Name,_Extends,Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Sets). | |
| 1199 | internal_context_constants(context(Name,_Extends,_Sets,Constants,_AbstractConstants,_Axioms,_Theorems),Name,Constants). | |
| 1200 | internal_context_abstract_constants(context(Name,_Extends,_Sets,_Constants,AbstractConstants,_Axioms,_Theorems),Name,AbstractConstants). | |
| 1201 | ||
| 1202 | internal_model(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name). | |
| 1203 | internal_model_refines(model(Name,Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Refines). | |
| 1204 | internal_model_sees(model(Name,_Refines,Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Sees). | |
| 1205 | internal_model_vars(model(Name,_Refines,_Sees,Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Variables). | |
| 1206 | internal_model_newvars(model(Name,_Refines,_Sees,_Variables,NewVariables,_Invariants,_Theorems,_Events),Name,NewVariables). | |
| 1207 | internal_model_invs(model(Name,_Refines,_Sees,_Variables,_NewVariables,Invariants,_Theorems,_Events),Name,Invariants). | |
| 1208 | internal_model_thms(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,Theorems,_Events),Name,Theorems). | |
| 1209 | internal_model_events(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,Events),Name,Events). | |
| 1210 | ||
| 1211 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1212 | % analyse deferred sets and generate enumerated sets if possible | |
| 1213 | ||
| 1214 | ||
| 1215 | ||
| 1216 | ||
| 1217 | %% :- include(bmachine_eventb_common). | |
| 1218 | %% code below used to be in separate file, as there was the single-level and multi-level mode: | |
| 1219 | ||
| 1220 | ||
| 1221 | ||
| 1222 | extract_name(event_b_model(_,Name,_Sections),Res) :- !, Res=Name. | |
| 1223 | extract_name(event_b_context(_,Name,_Sections),Res) :- !, Res=Name. | |
| 1224 | extract_name(MODEL,_) :- add_error(extract_name,'Could not extract model name: ',MODEL),fail. | |
| 1225 | ||
| 1226 | extract_sections(event_b_model(_,_Name,Sections),Sections). | |
| 1227 | extract_sections(event_b_context(_,_Name,Sections),Sections). | |
| 1228 | ||
| 1229 | % topological sort | |
| 1230 | ||
| 1231 | topological_sort(List,Sorted) :- | |
| 1232 | get_dependencies(List,Dependencies), | |
| 1233 | topolsort(Dependencies,[],SortedNames), | |
| 1234 | get_sorted(SortedNames,List,Sorted),!. | |
| 1235 | topological_sort(List,Sorted) :- add_failed_call_error(topological_sort(List,Sorted)),fail. | |
| 1236 | ||
| 1237 | get_dependencies([],[]). | |
| 1238 | get_dependencies([E|Rest],[dep(Name,Deps)|Drest]) :- | |
| 1239 | extract_name(E,Name), | |
| 1240 | findall(D,dependency(E,D),Deps1), | |
| 1241 | sort(Deps1,Deps), | |
| 1242 | get_dependencies(Rest,Drest). | |
| 1243 | ||
| 1244 | dependency(Elem,Dependend) :- | |
| 1245 | extract_sections(Elem,Sections), | |
| 1246 | ( rawmachine_section(extends,Sections,Extends), | |
| 1247 | member(Dependend,Extends) | |
| 1248 | ; rawmachine_section(refines,Sections,Dependend)). | |
| 1249 | ||
| 1250 | topolsort([],_,[]) :- !. | |
| 1251 | topolsort(Deps,Fulfilled,[First|Rest]) :- | |
| 1252 | select(dep(First,Before),Deps,Drest), | |
| 1253 | is_sublist(Before,Fulfilled),!, | |
| 1254 | sort([First|Fulfilled],NewFulfilled), | |
| 1255 | topolsort(Drest,NewFulfilled,Rest). | |
| 1256 | is_sublist([],_). | |
| 1257 | is_sublist([H|T],[F|R]) :- | |
| 1258 | (H=F -> is_sublist(T,R) ; is_sublist([H|T],R)). | |
| 1259 | ||
| 1260 | get_sorted([],_,[]). | |
| 1261 | get_sorted([Name|Nrest],Elems,[First|Srest]) :- | |
| 1262 | member(First,Elems), | |
| 1263 | extract_name(First,Name),!, | |
| 1264 | get_sorted(Nrest,Elems,Srest). | |
| 1265 | ||
| 1266 | % copy&paste from bmachine_construction | |
| 1267 | rawmachine_section(Elem,List,Result) :- | |
| 1268 | functor(Pattern,Elem,2), | |
| 1269 | arg(2,Pattern,Result), | |
| 1270 | member(Pattern,List),!. | |
| 1271 | ||
| 1272 | optional_rawmachine_section(Elem,List,Default,Result) :- | |
| 1273 | ( rawmachine_section(Elem,List,Result1) -> true | |
| 1274 | ; Result1=Default), | |
| 1275 | Result1=Result. | |
| 1276 | ||
| 1277 | % ---------------------------------------- | |
| 1278 | ||
| 1279 | ||
| 1280 | % older versions of the .eventb files do not have a status included | |
| 1281 | raw_event(event(Pos,Name,RawRefines,Params,Guards,Actions,Witnesses), % event/7 | |
| 1282 | Pos,Name,ordinary(none),Refines,Params,Guards,[],Actions,Witnesses,[]) :- | |
| 1283 | (\+((RawRefines==[] ; RawRefines=[_|_])) | |
| 1284 | -> add_error(b_machine_eventb,'Outdated .eventb format, ignoring refines:',RawRefines), | |
| 1285 | Refines = [] | |
| 1286 | ; Refines=RawRefines). | |
| 1287 | raw_event(event(Pos,Name,Status,Refines,Params,Guards,Actions,Witnesses), % event/8 | |
| 1288 | Pos,Name,Status,Refines,Params,Guards,[],Actions,Witnesses,[]). | |
| 1289 | raw_event(event(Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses), % event/9 | |
| 1290 | Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,[]). | |
| 1291 | raw_event(description_event(_,Desc,Event), | |
| 1292 | Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,[DescText|TD]) :- | |
| 1293 | unwrap_desc_pragma(Desc,DescText), | |
| 1294 | raw_event(Event, Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,TD), | |
| 1295 | debug_format(19,'New style event ~w with description "~w"~n',[Name,DescText]). | |
| 1296 | ||
| 1297 | % new parser now has specific position info here: | |
| 1298 | unwrap_desc_pragma(description_text(_Pos,Desc),Res) :- !, Res=Desc. | |
| 1299 | unwrap_desc_pragma(D,D). | |
| 1300 | ||
| 1301 | % code common to bmachine_eventb.pl and bmachine_eventb_ml.pl | |
| 1302 | ||
| 1303 | :- use_module(bmachine_structure,[select_section/5]). | |
| 1304 | append_to_section(Section,List,Old,New) :- | |
| 1305 | % todo: access to private elements of bmachine_construction | |
| 1306 | select_section(Section,OldList,NewList,Old,New), | |
| 1307 | append(OldList,List,NewList). | |
| 1308 | conjunct_to_section(Section,Preds,Old,New) :- | |
| 1309 | % todo: access to private elements of bmachine_construction | |
| 1310 | select_section(Section,OldPred,NewPred,Old,New), | |
| 1311 | conjunct_predicates([OldPred|Preds],NewPred). | |
| 1312 | ||
| 1313 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1314 | % analyse Event-B deferred sets and generate enumerated sets if possible | |
| 1315 | ||
| 1316 | enumerated_deferred_sets(Sets,Constants,Axioms,NewSets,NewConstants,NewAxioms,TSet,TElements) :- | |
| 1317 | conjunct_predicates(Axioms,Axiom), | |
| 1318 | conjunction_to_list(Axiom,Axiom2), | |
| 1319 | enumerated_deferred_sets2(Sets,Constants,Axiom2,NewSets,NewConstants,NewAxioms,TSet,TElements). | |
| 1320 | ||
| 1321 | enumerated_deferred_sets2([],Csts,Axioms,[],Csts,Axioms,[],[]). | |
| 1322 | enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,NewSets,NewCsts,NewAxioms,[TSet|TSetRest],TElementsAll) :- | |
| 1323 | % case 1: the set is an enumerated set | |
| 1324 | enumerated_deferred_set(Set,Csts,Axioms,ICsts,IAxioms,TSet,TElements),!, | |
| 1325 | append(TElements,TElementsRest,TElementsAll), | |
| 1326 | enumerated_deferred_sets2(SetRest,ICsts,IAxioms,NewSets,NewCsts,NewAxioms,TSetRest,TElementsRest). | |
| 1327 | enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,[Set|NewSets],NewCsts,NewAxioms,TSets,TElements) :- | |
| 1328 | % case 2: the set is a normal deferred set | |
| 1329 | enumerated_deferred_sets2(SetRest,Csts,Axioms,NewSets,NewCsts,NewAxioms,TSets,TElements). | |
| 1330 | ||
| 1331 | enumerated_deferred_set(Set,Constants,Axioms,NewConstants,NewAxioms,Set,TElements) :- | |
| 1332 | %% print(checking_for_enumerated_deferred_sets(Axioms)),nl, | |
| 1333 | has_enumeration_axioms(Set,Elements,Axioms,NewAxioms), | |
| 1334 | %% print(found_enumerated_set(Set)),nl, %% | |
| 1335 | % remove Elem1,...,ElemN from the constants | |
| 1336 | remove_constants(Elements,Constants,NewConstants), | |
| 1337 | % add enumerated set information to the elements | |
| 1338 | get_texpr_type(Set,SType), | |
| 1339 | (SType=set(global(Type)) -> true | |
| 1340 | ; add_error_and_fail(enumerated_deferred_set,'Unexpected Set: ',(Set:SType))), | |
| 1341 | (typeset_enumerated(Elements,Type,TElements) -> true | |
| 1342 | ; add_error_and_fail(enumerated_deferred_set,'Could not typeset: ',(Type,Elements))). | |
| 1343 | ||
| 1344 | ||
| 1345 | has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :- | |
| 1346 | has_partition_axioms(Set,Elements,AxiomsIn,AxiomsOut),!. | |
| 1347 | has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :- | |
| 1348 | % there in an axiom Set = {Elem1,...,ElemN} | |
| 1349 | select_equal_extension_set_of_ids(Set,AxiomsIn,Axioms1,ExtSet,Elements), | |
| 1350 | % check if all axioms needed for an enumeration are | |
| 1351 | % present, and remove them | |
| 1352 | % second case: All elements of the set are mutually unequal | |
| 1353 | ||
| 1354 | % generate the unequalities we have to check for | |
| 1355 | generate_unequals(Elements,Unequals), | |
| 1356 | % check if they are all in the axioms, and remove them from the axioms | |
| 1357 | (all_unequals_present(Unequals,Axioms1,AxiomsOut) -> true | |
| 1358 | ; assertz(deferred_set_eq_wo_enumeration_axioms(Set,ExtSet)), | |
| 1359 | write('Deferred set with equality but *not* recognized as enumerated set: '), | |
| 1360 | translate:print_bexpr(Set), write(' = '), translate:print_bexpr(ExtSet),nl, | |
| 1361 | fail | |
| 1362 | ). | |
| 1363 | ||
| 1364 | has_partition_axioms(Set,PartitionElements,AxiomsIn,AxiomsOut) :- | |
| 1365 | % print(checking_for_enumeration_axioms(Set)),nl, | |
| 1366 | % first case: A partion predicate is present with | |
| 1367 | % all elements of the set as its arguments | |
| 1368 | % ( e.g. partition(S,{a},{b},...) ) | |
| 1369 | ||
| 1370 | % create a pattern for the partition: | |
| 1371 | get_texpr_id(Set,SetId),get_texpr_id(SetRef,SetId), | |
| 1372 | create_texpr(partition(SetRef,Singletons),pred,_,Partition), | |
| 1373 | % remove the partition from the axioms | |
| 1374 | % print(looking_for_partition(SetId,Partition)),nl,nl, | |
| 1375 | select(Partition,AxiomsIn,AxiomsOut1), | |
| 1376 | %%print(found_partition(SetID,Partition)),nl, | |
| 1377 | % check if all arguments are singletons and get the | |
| 1378 | % singleton elements | |
| 1379 | all_singletons(Singletons,PartitionElements,AxiomsOut1,AxiomsOut2,Recursive), | |
| 1380 | (Recursive==true | |
| 1381 | -> AxiomsOut=AxiomsIn /* then we still need the partition axioms */ | |
| 1382 | ; AxiomsOut=AxiomsOut2). | |
| 1383 | %% ,print(all_singletons(Singletons)),nl. | |
| 1384 | %% print(singletons(PartitionElements)),nl, | |
| 1385 | % check if all arguments and the identifiers | |
| 1386 | % of the set are the same | |
| 1387 | % same_elements(Elements,PartitionElements). | |
| 1388 | ||
| 1389 | ||
| 1390 | % all elements of a list are singletons, the second argument | |
| 1391 | % returns the list of elements without the set around it | |
| 1392 | all_singletons([],[],Ax,Ax,_). | |
| 1393 | all_singletons([Set|SRest],[Expr|ERest],AxiomsIn,AxiomsOut,Recursive) :- | |
| 1394 | get_texpr_expr(Set,set_extension([Expr])),!, | |
| 1395 | all_singletons(SRest,ERest,AxiomsIn,AxiomsOut,Recursive). | |
| 1396 | all_singletons([ID1|SRest],Result,AxiomsIn,AxiomsOut,Recursive) :- | |
| 1397 | ID1 = b(identifier(_ID),set(global(_)),_Info), | |
| 1398 | Recursive=true, | |
| 1399 | % print(trying_to_look_for_recursive_partition(_ID)),nl, %% | |
| 1400 | has_enumeration_axioms(ID1,PartitionElements,AxiomsIn,AxiomsOut1), | |
| 1401 | % print(recursive_partition(ID,PartitionElements)),nl, | |
| 1402 | append(PartitionElements,ERest,Result), | |
| 1403 | all_singletons(SRest,ERest,AxiomsOut1,AxiomsOut,_). | |
| 1404 | ||
| 1405 | % the two lists of typed identifiers have the same identifiers | |
| 1406 | %same_elements(ElemsA,ElemsB) :- | |
| 1407 | % get_texpr_ids(ElemsA,IdsA),sort(IdsA,A), | |
| 1408 | % get_texpr_ids(ElemsB,IdsB),sort(IdsB,B), | |
| 1409 | % A=B. | |
| 1410 | ||
| 1411 | typeset_enumerated([],_Type,[]). | |
| 1412 | typeset_enumerated([Elem|Erest],Type,[TElem|Trest]) :- | |
| 1413 | create_texpr(identifier(Id),global(Type),Infos,Elem), | |
| 1414 | create_texpr(identifier(Id),global(Type),[enumerated_set_element|Infos],TElem), | |
| 1415 | typeset_enumerated(Erest,Type,Trest). | |
| 1416 | ||
| 1417 | remove_constants([],Cst,Cst). | |
| 1418 | remove_constants([TId|Erest],In,Out) :- | |
| 1419 | get_texpr_id(TId,Id), | |
| 1420 | get_texpr_id(Pattern,Id), | |
| 1421 | select(Pattern,In,Env), | |
| 1422 | remove_constants(Erest,Env,Out). | |
| 1423 | ||
| 1424 | % find an equality Set = {id1,...,idk} | |
| 1425 | select_equal_extension_set_of_ids(Set,In,Out,Ext,Elements) :- | |
| 1426 | get_texpr_id(Set,SetId), | |
| 1427 | get_texpr_id(Expr,SetId), | |
| 1428 | create_texpr(set_extension(Elements),_,_,Ext), | |
| 1429 | create_texpr(Equal,_,_,TEqual), | |
| 1430 | ( Equal = equal(Expr,Ext); Equal = equal(Ext,Expr) ), | |
| 1431 | select(TEqual,In,Out),!. | |
| 1432 | ||
| 1433 | generate_unequals(Elements,Unequals) :- | |
| 1434 | get_texpr_ids(Elements,Ids), | |
| 1435 | findall(unequal(A,B),two_ids(Ids,A,B),Unequals). | |
| 1436 | two_ids([A|Rest],A,B) :- member(B,Rest). | |
| 1437 | two_ids([_|Rest],A,B) :- two_ids(Rest,A,B). | |
| 1438 | ||
| 1439 | all_unequals_present([],Axioms,Axioms). | |
| 1440 | all_unequals_present([unequal(A,B)|Rest],InAxioms,OutAxioms) :- | |
| 1441 | remove_unequalities(InAxioms,A,B,IntAxioms,0,N), N>0,!, % at least one occurrence | |
| 1442 | all_unequals_present(Rest,IntAxioms,OutAxioms). | |
| 1443 | ||
| 1444 | remove_unequalities([],_,_,[],N,N). | |
| 1445 | remove_unequalities([TAxiom|T],A,B,Rest,NrRemoved,R) :- | |
| 1446 | get_texpr_id(AExpr,A), get_texpr_id(BExpr,B), | |
| 1447 | get_texpr_expr(TAxiom,Axiom), | |
| 1448 | is_unequality(Axiom,AExpr,BExpr),!, N1 is NrRemoved+1, | |
| 1449 | remove_unequalities(T,A,B,Rest,N1,R). | |
| 1450 | remove_unequalities([Axiom|T],A,B,[Axiom|TR],N,R) :- % not an unequality between A and B | |
| 1451 | remove_unequalities(T,A,B,TR,N,R). | |
| 1452 | ||
| 1453 | is_unequality(not_equal(A,B),A,B) :- !. | |
| 1454 | is_unequality(not_equal(B,A),A,B) :- !. | |
| 1455 | is_unequality(negation(TEqual),A,B) :- | |
| 1456 | get_texpr_expr(TEqual,Equal), | |
| 1457 | is_direct_equality(Equal,A,B). | |
| 1458 | is_direct_equality(equal(A,B),A,B) :- !. | |
| 1459 | is_direct_equality(equal(B,A),A,B) :- !. | |
| 1460 | ||
| 1461 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1462 | % creating a type environment with information about theories inside | |
| 1463 | ||
| 1464 | check_theory_extensions(Infos,Freetypes,Ops,TheoryEnv) :- | |
| 1465 | findall( T, (member(T,Infos),is_eventb_additional_info(T)), Theories), | |
| 1466 | default_theory_ops(InitialEnv), | |
| 1467 | foldl(check_theory,Theories,FreetypesL,OpsL,InitialEnv,TheoryEnv), | |
| 1468 | append(FreetypesL,Freetypes), | |
| 1469 | append(OpsL,Ops). | |
| 1470 | is_eventb_additional_info(Term) :- | |
| 1471 | nonvar(Term),functor(Term,theory,Arity), | |
| 1472 | memberchk(Arity,[3,4,5,7]). | |
| 1473 | default_theory_ops(Env) :- | |
| 1474 | env_empty(Empty), | |
| 1475 | cond_operator(Id,Op), | |
| 1476 | env_store_operator(Id,Op,Empty,Env). | |
| 1477 | cond_operator('COND',bmachine_eventb:axiomatic_definition('COND',Params,DirectDef,[PT])) :- | |
| 1478 | PT = '__IFTHENELSETYPE', | |
| 1479 | TypeExpr = identifier(none,PT), | |
| 1480 | Params = [argument('THEN',TypeExpr), | |
| 1481 | argument('ELSE',TypeExpr), | |
| 1482 | argument('IF',set_extension(none,[truth(none)]))], | |
| 1483 | DirectDef = if_then_else(none,identifier(none,'IF'), | |
| 1484 | identifier(none,'THEN'),identifier(none,'ELSE')). | |
| 1485 | check_theory(Theory,Freetypes,Ops,Env,OutEnv) :- | |
| 1486 | get_theory_name(Theory,Proj,Name), | |
| 1487 | debug_format(19,'Checking theory ~w:~w~n',[Proj,Name]), | |
| 1488 | (check_theory2(Theory,Env,_DefSets,Freetypes,Ops) -> true | |
| 1489 | ; add_internal_error('Theory check failed:',Theory),fail), | |
| 1490 | store_operator_list(Ops,Env,OutEnv), | |
| 1491 | check_theory_axioms(Theory,OutEnv,_). | |
| 1492 | ||
| 1493 | store_operator_list(Ops,Env,OutEnv) :- | |
| 1494 | keys_and_values(Ops,Ids,Operators), | |
| 1495 | foldl(env_store_operator,Ids,Operators,Env,OutEnv). | |
| 1496 | ||
| 1497 | check_theory2(theory(PT,Datatypes,OP),Env,DefSets,Freetypes,Ops) :- | |
| 1498 | % just to be backward-compatible to a version without axiomatic definitions | |
| 1499 | check_theory2(theory(PT,Datatypes,OP,[]),Env,DefSets,Freetypes,Ops). | |
| 1500 | check_theory2(theory(PT,Datatypes,OP,AxDefs),Env,DefSets,Freetypes,Ops) :- | |
| 1501 | % just to be backward-compatible to a version without operator mapping | |
| 1502 | % definitions | |
| 1503 | check_theory2(theory(PT,Datatypes,OP,AxDefs,[]),Env,DefSets,Freetypes,Ops). | |
| 1504 | check_theory2(theory(PT,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,Ops) :- | |
| 1505 | check_theory2(theory(unknown,unknown,PT,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,Ops). | |
| 1506 | check_theory2(theory(TheoryId,_Imported,TypeParameters,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,AllOps) :- | |
| 1507 | %print_theory_axioms(TheoryId,TypeParameters,AxDefs), | |
| 1508 | extract_freetypes(TheoryId,Env,Datatypes,Freetypes,FreetypeOps), | |
| 1509 | (Mappings \= [_|_] | |
| 1510 | -> generate_default_mappings(AxDefs,TheoryId,ML) | |
| 1511 | ; debug_format(19,'Mappings in .ptm file: ~w~n',[Mappings]), | |
| 1512 | ML=Mappings), % some older .eventb files seem to have none here, e.g., Theory/SumProduct_m1_mch.eventb | |
| 1513 | debug_println(9,operator_mappings(ML)), | |
| 1514 | findall(VirtualDefSet,unmapped_axiomatic_def_set(VirtualDefSet,AxDefs,ML),DefSets), | |
| 1515 | maplist(store_virtual_deferred_set(TheoryId,TypeParameters),DefSets,DefSetOps), | |
| 1516 | foldl(handle_mappings(TheoryId,TypeParameters),ML,MappedOpsL,OP/AxDefs,OP1/AxDefs1), | |
| 1517 | append(MappedOpsL,MappedOps), | |
| 1518 | maplist(store_operator(TheoryId,TypeParameters),OP1,DefinedOps), | |
| 1519 | maplist(store_axiomatic_operator(TheoryId,TypeParameters),AxDefs1,AxOpsL), | |
| 1520 | append(AxOpsL,AxOps), | |
| 1521 | append([DefSetOps,FreetypeOps,MappedOps,DefinedOps,AxOps],AllOps1), | |
| 1522 | % The operators are used for call-backs, a module prefix is mandatory | |
| 1523 | maplist(prefix_with_module,AllOps1,AllOps). | |
| 1524 | ||
| 1525 | unmapped_axiomatic_def_set(VirtualDefSet,AxDefs,ML) :- | |
| 1526 | member(axiomatic_def_block(_AxDefId,AxTypes,_,_),AxDefs), | |
| 1527 | member(VirtualDefSet,AxTypes), nonmember(tag(VirtualDefSet,_),ML). | |
| 1528 | ||
| 1529 | % axiomatic blocks can contain new types; these seem to be just deferred sets (cf R0-MovingTrains_mch.eventb) | |
| 1530 | store_virtual_deferred_set(TheoryId,TypeParameters,DefSet,Res) :- Parameters=[],RawWDCond=truth(none), | |
| 1531 | ((DefSet='Real' ; DefSet='REAL') % in case no .ptm file exists, e.g., for Abrial's Real theory | |
| 1532 | -> DirectDef=real_set(none), | |
| 1533 | add_message(bmachine_eventb,'Translating axiomatic type to REAL: ',DefSet) | |
| 1534 | ; DirectDef=string_set(none), | |
| 1535 | add_message(bmachine_eventb,'Translating axiomatic type to STRING: ',DefSet) | |
| 1536 | ), % TODO: translate to propert def. set! | |
| 1537 | store_operator(TheoryId,TypeParameters,operator(DefSet,Parameters,RawWDCond,[DirectDef],[]),Res). | |
| 1538 | ||
| 1539 | prefix_with_module(Id-Op,Id-(bmachine_eventb:Op)). | |
| 1540 | ||
| 1541 | :- public print_theory_axioms/3. | |
| 1542 | print_theory_axioms(TheoryId,TypeParameters,AxDefs) :- member(axiomatic_def_block(Id,Types,_OpDefsIn,Axioms),AxDefs), | |
| 1543 | format('~nAxDef Block ~w (~w) in theory ~w (~w)~n',[Id,Types,TheoryId,TypeParameters]), | |
| 1544 | translate:l_print_raw_bexpr(Axioms), | |
| 1545 | fail. | |
| 1546 | print_theory_axioms(_,_,_). | |
| 1547 | ||
| 1548 | ||
| 1549 | check_theory_axioms(theory(TheoryId,_Imported,TypeParameters,_Datatypes,_OP,AxDefs,_Mappings),Env,TheoryAxioms) :- | |
| 1550 | fail, % disabled; for tests 2295, 2379, 2382 there are unsupported axiomatic operators in the axioms | |
| 1551 | maplist(create_deferred_set,TypeParameters,RawIds), | |
| 1552 | create_sets(RawIds,TheoryId,Sets), | |
| 1553 | add_unique_variables(Sets,Env,Env2), | |
| 1554 | member(axiomatic_def_block(AxDefId,_Types,_OpDefsIn,RawAxioms),AxDefs), | |
| 1555 | get_theory_name(TheoryId,Proj,Name), format('Typechecking block ~w in ~w:~w~n',[AxDefId,Proj,Name]), | |
| 1556 | typecheck_l(RawAxioms,Env2,pred,TheoryAxioms,theory_axioms), | |
| 1557 | translate:l_print_bexpr_or_subst(TheoryAxioms),nl, | |
| 1558 | fail. | |
| 1559 | check_theory_axioms(_,_Env,[]). | |
| 1560 | ||
| 1561 | create_deferred_set(Atom,deferred_set(unknown,Atom)). | |
| 1562 | ||
| 1563 | get_theory_name(theory_name(Project,TheoryName),ResP,ResN) :- !, | |
| 1564 | ResP=Project, ResN=TheoryName. | |
| 1565 | get_theory_name(Theory,ResP,ResN) :- | |
| 1566 | functor(Theory,theory,_), arg(1,Theory,TN),!, | |
| 1567 | get_theory_name(TN,ResP,ResN). | |
| 1568 | get_theory_name(N,'','') :- format('Could not extract theory name: ~w~n',[N]). | |
| 1569 | ||
| 1570 | store_operator(TheoryId,TypeParameters,operator(Id,Parameters,RawWDCond,DirectDef,RecursiveDef),Id-Op) :- | |
| 1571 | store_operator2(TheoryId,TypeParameters,Id,DirectDef,RecursiveDef,Parameters,RawWDCond,TypeParameters,Op). | |
| 1572 | ||
| 1573 | store_operator2(_,_,_,_,RecursiveDef,Parameters,_WD,TypeParameters,Op) :- | |
| 1574 | RecursiveDef=[_|_],!, | |
| 1575 | Op=recursive_operator(Parameters,RecursiveDef,TypeParameters). | |
| 1576 | store_operator2(TheoryId,_,Id,[Def],_,Parameters,Raw_WDCond,TypeParameters,Op) :- !, | |
| 1577 | %format('Storing direct definition operator ~w with WD: ~w~n',[Id,Raw_WDCond]), | |
| 1578 | store_operator_definition(TheoryId,Id,Parameters,Def,Raw_WDCond,TypeParameters,direct_definition), % store for bvisual2 | |
| 1579 | Op=direct_definition(Parameters,Raw_WDCond,Def,TypeParameters). | |
| 1580 | store_operator2(TheoryId,TypeParas,_Id,_,Parameters,_,_WD,_,Op) :- | |
| 1581 | get_theory_name(TheoryId,Project,Theory), | |
| 1582 | Op = unsupported_operator(Project,Theory,TypeParas,Parameters, | |
| 1583 | 'Only operators with direct or recursive definition are currently supported'). | |
| 1584 | ||
| 1585 | :- dynamic stored_operator_direct_definition/8. | |
| 1586 | % store definition for bvisual2, ...; not used in typechecker or interpreter | |
| 1587 | store_operator_definition(TheoryId,Id,Parameters,Def,Raw_WDCond,TypeParameters,Kind) :- | |
| 1588 | get_theory_name(TheoryId,Proj,Theory), | |
| 1589 | assertz(stored_operator_direct_definition(Id,Proj,Theory,Parameters,Def,Raw_WDCond,TypeParameters,Kind)). | |
| 1590 | ||
| 1591 | reset_stored_defs :- retractall(stored_operator_direct_definition(_,_,_,_,_,_,_,_)), | |
| 1592 | retractall(some_operator_uses_reals). | |
| 1593 | ||
| 1594 | stored_operator(Id,Kind) :- | |
| 1595 | stored_operator_direct_definition(Id,_,_,_,_,_,_,Kind). | |
| 1596 | ||
| 1597 | :- dynamic some_operator_uses_reals/0. | |
| 1598 | check_if_operator_expr_uses_reals(Raw) :- | |
| 1599 | \+some_operator_uses_reals, | |
| 1600 | raw_term_uses_reals(Raw), | |
| 1601 | !, | |
| 1602 | assert(some_operator_uses_reals). % this may be important for type checking later | |
| 1603 | check_if_operator_expr_uses_reals(_). | |
| 1604 | ||
| 1605 | raw_term_uses_reals(real_set(_)). | |
| 1606 | raw_term_uses_reals(float_set(_)). | |
| 1607 | raw_term_uses_reals(real(_,_)). | |
| 1608 | raw_term_uses_reals(external_pred_call_auto(_,ExtFun,_)) :- ext_fun_uses_reals(ExtFun). | |
| 1609 | raw_term_uses_reals(external_function_call_auto(_,ExtFun,_)) :- ext_fun_uses_reals(ExtFun). | |
| 1610 | % TODO: detect more and detect nested usage | |
| 1611 | :- use_module(external_functions, [external_fun_type/3]). | |
| 1612 | ext_fun_uses_reals(ExtFun) :- external_fun_type(ExtFun,_,Types), member(R,Types),R==real. | |
| 1613 | ||
| 1614 | :- use_module(eventhandling,[register_event_listener/3]). | |
| 1615 | :- register_event_listener(clear_specification,reset_stored_defs, | |
| 1616 | 'Reset stored Event-B operators.'). | |
| 1617 | ||
| 1618 | % extract inductive data types as freetypes | |
| 1619 | extract_freetypes(TheoryId,ParamEnv,DataTypes,Freetypes,FreetypeOps) :- | |
| 1620 | maplist(extract_freetype(TheoryId,DataTypes,ParamEnv),DataTypes,Freetypes,FreetypeOpsL), | |
| 1621 | append(FreetypeOpsL,FreetypeOps). | |
| 1622 | extract_freetype(TheoryId,AllDataTypes,Env, | |
| 1623 | datatype(Id,TypeParams,Constructors), | |
| 1624 | freetype(FreetypeId,Cases), | |
| 1625 | [Id-freetype_operator(FreetypeId,Types,TypeParams,Usage)|CaseOps]) :- | |
| 1626 | debug_format(19,'Converting data type ~w with type parameters ~w to freetype~n',[Id,TypeParams]), | |
| 1627 | foldl(add_datatype_to_env,AllDataTypes,Env,Env1), | |
| 1628 | foldl(add_type_parameter,TypeParams,Types,Env1,ParamEnv), | |
| 1629 | create_freetype_typeid(Id,Types,FreetypeId), | |
| 1630 | Type = freetype(FreetypeId), | |
| 1631 | extract_used_type_parameters(Constructors,TypeParams,Usage), | |
| 1632 | %store_eventb_operator(Id,freetype_operator_as_identifier(Id),ParamEnv,ParamEnv2), % now done in add_datatype_to_env | |
| 1633 | WD=truth(none), | |
| 1634 | maplist(get_raw_id,TypeParams,TypeParaIds), | |
| 1635 | store_operator_definition(TheoryId,Id,TypeParaIds,identifier(none,'Datatype'),WD,TypeParaIds,datatype_definition), % store for bvisual2 | |
| 1636 | maplist(extract_case(TheoryId,ParamEnv,Type,Types),Constructors,Cases,CaseOpsL), | |
| 1637 | append(CaseOpsL,CaseOps). | |
| 1638 | get_raw_id(identifier(_,ID),R) :- !, R=ID. | |
| 1639 | get_raw_id(I,I). | |
| 1640 | ||
| 1641 | add_datatype_to_env(datatype(Id,Params,_ConstructorList),In,Out) :- | |
| 1642 | length(Params,NumberOfParams), | |
| 1643 | functor(FreetypeId,Id,NumberOfParams), | |
| 1644 | debug_format(19,'Generating freetype ~w/~w for inductive datatype from Rodin theory~n',[Id,NumberOfParams]), | |
| 1645 | env_store(Id,set(freetype(FreetypeId)),[],In,In2), | |
| 1646 | store_eventb_operator(Id,freetype_operator_as_identifier(Id),In2,Out). | |
| 1647 | ||
| 1648 | add_type_parameter(TypeParam,Type,In,Out) :- | |
| 1649 | extract_id(TypeParam,ParameterId), | |
| 1650 | debug_format(19,'Generating paramater type ~w for Rodin theory~n',[ParameterId]), | |
| 1651 | env_store(ParameterId,set(Type),[],In,Out). | |
| 1652 | extract_id(identifier(_,Id),Id). | |
| 1653 | % constructor without parameters | |
| 1654 | extract_case(_TheoryId,_ParamEnv,freetype(TypeId),_Types, constructor(Id,[]), | |
| 1655 | case(Id,constant([Id])),Ops) :- !, | |
| 1656 | Ops=[Id-constructor_operator(TypeId,[])]. | |
| 1657 | % constructor with parameters | |
| 1658 | extract_case(TheoryId,ParamEnv,Freetype,ParamTypes,constructor(Id,Destructors), | |
| 1659 | case(Id,Type), | |
| 1660 | [Id-constructor_operator(FreetypeId,Types)|DestructOps]) :- | |
| 1661 | maplist(extract_destructor(TheoryId,ParamEnv,Freetype,ParamTypes,Id,Type), | |
| 1662 | Destructors,Projections,TypesAndOps), | |
| 1663 | maplist(split_type_and_op,TypesAndOps,Types,DestructOps), | |
| 1664 | Freetype=freetype(FreetypeId), | |
| 1665 | debug_format(19,'Generated constructor ~w ~w for freetype ~w~n',[Id,Types, FreetypeId]), | |
| 1666 | combine_typelist_with_prj(Types,Type,Projections). | |
| 1667 | extract_destructor(TheoryId,Env,freetype(FreetypeId),ParamTypes,Case,CType, | |
| 1668 | destructor(Name,RawTypeExpr),Projection,Type-Name-Op) :- | |
| 1669 | typecheck_with_freevars(RawTypeExpr,Env,ParamTypes,set(Type),_,destructor(FreetypeId)), | |
| 1670 | Op = destructor_operator(Name,FreetypeId,Projection,Case,CType), | |
| 1671 | debug_format(19,'Generated destructor ~w (type ~w) for case ~w of freetype ~w~n', [Name,Type, Case, FreetypeId]), | |
| 1672 | ||
| 1673 | WD = truth(none), | |
| 1674 | functor(FreetypeId,FF,_), | |
| 1675 | ajoin(['Destructor for ', FF],InfoID), | |
| 1676 | store_operator_definition(TheoryId,Name,[argument(Case,CType)],identifier(none,InfoID),WD,ParamTypes, | |
| 1677 | destructor(FreetypeId,Type)). | |
| 1678 | ||
| 1679 | split_type_and_op(Type-Name-Op,Type,Name-Op). | |
| 1680 | ||
| 1681 | ||
| 1682 | :- assert_must_succeed(( combine_typelist_with_prj([a,b],T,P), | |
| 1683 | T == couple(a,b), P == [[prj1],[prj2]] )). | |
| 1684 | :- assert_must_succeed(( combine_typelist_with_prj([a,b,c],T,P), | |
| 1685 | T == couple(a,couple(b,c)), | |
| 1686 | P == [[prj1],[prj2,prj1],[prj2,prj2]] )). | |
| 1687 | :- assert_must_succeed(( combine_typelist_with_prj([a,b,c,d],T,P), | |
| 1688 | T == couple(couple(a,b),couple(c,d)), | |
| 1689 | P == [[prj1,prj1],[prj1,prj2],[prj2,prj1],[prj2,prj2]] )). | |
| 1690 | combine_typelist_with_prj([T],R,Projections) :- !,R=T,Projections=[[]]. | |
| 1691 | combine_typelist_with_prj(Types,couple(TypeL,TypeR),Projections) :- | |
| 1692 | split_list_in_middle(Types,TypesLeft,TypesRight), | |
| 1693 | same_length(TypesLeft,PrjLeft),same_length(TypesRight,PrjRight), | |
| 1694 | append(PrjLeft,PrjRight,Projections), | |
| 1695 | maplist(cons(prj1),PrjLeft1,PrjLeft), | |
| 1696 | maplist(cons(prj2),PrjRight1,PrjRight), | |
| 1697 | combine_typelist_with_prj(TypesLeft,TypeL,PrjLeft1), | |
| 1698 | combine_typelist_with_prj(TypesRight,TypeR,PrjRight1). | |
| 1699 | split_list_in_middle(List,Left,Right) :- | |
| 1700 | length(List,N), | |
| 1701 | Half is floor(N / 2), | |
| 1702 | append_length(Left,Right,List,Half). | |
| 1703 | ||
| 1704 | combine_exprlist_to_couple([T],R) :- !,T=R. | |
| 1705 | combine_exprlist_to_couple(Exprs,R) :- | |
| 1706 | split_list_in_middle(Exprs,ExprsLeft,ExprsRight), | |
| 1707 | combine_exprlist_to_couple(ExprsLeft,TL), | |
| 1708 | combine_exprlist_to_couple(ExprsRight,TR), | |
| 1709 | get_texpr_types([TL,TR],[TypeL,TypeR]), | |
| 1710 | create_texpr(couple(TL,TR),couple(TypeL,TypeR),[],R). | |
| 1711 | ||
| 1712 | combine_exprlist_to_cprod([T],R) :- !,T=R. | |
| 1713 | combine_exprlist_to_cprod(Exprs,R) :- | |
| 1714 | split_list_in_middle(Exprs,ExprsLeft,ExprsRight), | |
| 1715 | combine_exprlist_to_cprod(ExprsLeft,TL), | |
| 1716 | combine_exprlist_to_cprod(ExprsRight,TR), | |
| 1717 | get_texpr_types([TL,TR],[set(TypeL),set(TypeR)]), | |
| 1718 | create_texpr(cartesian_product(TL,TR),set(couple(TypeL,TypeR)),[],R). | |
| 1719 | ||
| 1720 | extract_used_type_parameters(Constructors,TypeParams,Usages) :- | |
| 1721 | maplist(extract_id,TypeParams,TypeParamIds), | |
| 1722 | convlist(used_type_parameters_of_constructor(TypeParamIds),Constructors,Usages). | |
| 1723 | used_type_parameters_of_constructor(TypeParamIds,constructor(Id,Destructors), | |
| 1724 | used_param_types(Id,UsedParamTypes,DestructorExprs)) :- | |
| 1725 | maplist(destructor_expr,Destructors,DestructorExprs), | |
| 1726 | maplist(used_type_parameters_of_destructor(TypeParamIds), | |
| 1727 | DestructorExprs,UsedParamTypeL), | |
| 1728 | UsedParamTypeL = [_|_], % store the information only for constructors that actually use | |
| 1729 | % type parameters | |
| 1730 | ord_union(UsedParamTypeL,UsedParamTypes). | |
| 1731 | used_type_parameters_of_destructor(TypeParamIds,TypeExpr,UsedTypes) :- | |
| 1732 | extract_raw_identifiers(TypeExpr,UsedIds), | |
| 1733 | findall( N, (nth1(N,TypeParamIds,T),memberchk(T,UsedIds)), UsedTypes1), | |
| 1734 | sort(UsedTypes1,UsedTypes). | |
| 1735 | destructor_expr(destructor(_,Expr),Expr). | |
| 1736 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1737 | % callback predicates for operators | |
| 1738 | ||
| 1739 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1740 | ||
| 1741 | :- public unsupported_operator/13. | |
| 1742 | % called by btypechecker:lookup_eventb_operator | |
| 1743 | unsupported_operator(Project,Theory,_TypeParas,Params,_Msg,OpName,Args,Pos,_Env,ExPr,Result,TRin,TRout) :- | |
| 1744 | match_args_and_params(Args,Params,NewArgs), | |
| 1745 | get_typed_default_operator(OpName,NewArgs,ExPr,NewOpName,Result),!, | |
| 1746 | add_default_operator_warning(OpName,NewOpName,Theory,Project,Pos), | |
| 1747 | TRin=TRout. | |
| 1748 | unsupported_operator(_,_,_,_Parameters,Msg,Id,_Args,Pos,_Env,ExPr,Result,TRin,TRout) :- | |
| 1749 | %format('Unsupported ~w~n args:~w',[Id,_Args]), | |
| 1750 | store_typecheck_error(Msg,Pos,TRin,TRout), | |
| 1751 | failure_syntax_element(ExPr,Id,F,Type), % just to make sure that the result | |
| 1752 | create_texpr(F,Type,[],Result). % is nonvar, to prevent later errors | |
| 1753 | failure_syntax_element(expr,Id,identifier(Id),_). | |
| 1754 | failure_syntax_element(pred,_Id,falsity,pred). | |
| 1755 | ||
| 1756 | % in contrast to the default mappings handled earlier, | |
| 1757 | % this code as access to the actual arguments and their types | |
| 1758 | % and is called once for each use of the operator | |
| 1759 | get_typed_default_operator(Op,[A,B],ExPr,NewOp,Result) :- | |
| 1760 | get_texpr_type(A,TA), get_texpr_type(B,TB), | |
| 1761 | (nonvar(TA) ; nonvar(TB)), | |
| 1762 | binary_typed_operator_to_ast(Op,TA,TB,ExPr,NewOp,NewType), | |
| 1763 | ResExpr =.. [NewOp,A,B], | |
| 1764 | create_texpr(ResExpr,NewType,[],Result). | |
| 1765 | ||
| 1766 | ||
| 1767 | binary_typed_operator_to_ast(Op,T,T,expr,NewOp,T) :- binary_expr_op(Op,T,NewOp). | |
| 1768 | %binary_typed_operator_to_ast(Op,T,T,pred,NewOp,pred) :- binary_pred_op(Op,T,NewOp). | |
| 1769 | ||
| 1770 | binary_expr_op(pow,integer,power_of). | |
| 1771 | binary_expr_op(pow,real,power_of_real). | |
| 1772 | binary_expr_op(power_of,integer,power_of). | |
| 1773 | binary_expr_op(power_of,real,power_of_real). | |
| 1774 | binary_expr_op(div,integer,floored_div). | |
| 1775 | binary_expr_op(div,real,div_real). | |
| 1776 | ||
| 1777 | %binary_pred_op('less',real,less_real). | |
| 1778 | ||
| 1779 | ||
| 1780 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1781 | ||
| 1782 | :- use_module(probsrc(bsyntaxtree),[safe_create_texpr/4, is_truth/1, | |
| 1783 | add_texpr_infos_if_new/3, conjunct_predicates_with_pos_info/3]). | |
| 1784 | :- use_module(probsrc(bsyntaxtree_quantifiers),[create_z_let/6]). | |
| 1785 | ||
| 1786 | % get params and type parameters from operator callback registered in the typechecker environment | |
| 1787 | % for use by btypechecker:lookup_eventb_operator | |
| 1788 | % it would be a bit cleaner to store infos separately from callback or get rid of the call back completely | |
| 1789 | get_operator_arity_from_callback(direct_definition(Params,_WD,_DirectDef,_PT),direct_definition,Arity) :- | |
| 1790 | length(Params,Arity). | |
| 1791 | get_operator_arity_from_callback(axiomatic_definition(_TagName,Params,_DirectDef,_PT),axiomatic_definition,Arity) :- | |
| 1792 | length(Params,Arity). | |
| 1793 | get_operator_arity_from_callback(recursive_operator(Params,_Cases,_PT),recursive_operator,Arity) :- | |
| 1794 | length(Params,Arity). | |
| 1795 | get_operator_arity_from_callback(freetype_operator(_FId1,Types1,_PT,_Usage1),freetype_operator,Arity) :- | |
| 1796 | length(Types1,Arity). | |
| 1797 | get_operator_arity_from_callback(freetype_operator_as_identifier(_RecId),freetype_operator_as_identifier,0). | |
| 1798 | get_operator_arity_from_callback(freetype_operator_as_function(_RecId,_RType),freetype_operator_as_function,1). | |
| 1799 | get_operator_arity_from_callback(freetype_operator_as_set(_RecId),freetype_operator_as_function,0). | |
| 1800 | get_operator_arity_from_callback(constructor_operator(_FId,_TP),constructor_operator,0). | |
| 1801 | get_operator_arity_from_callback(destructor_operator(_Name,_FId,_Projections,_Case,_CType1),destructor_operator,1). | |
| 1802 | get_operator_arity_from_callback(make_inductive_natural(_ArgId,_ZeroOp,_SuccOp),make_inductive_natural,1). | |
| 1803 | get_operator_arity_from_callback(unsupported_operator(_Project,_Theory,_TP,Paras,_Msg),unsupported_operator,Len) :- | |
| 1804 | length(Paras,Len). | |
| 1805 | ||
| 1806 | %%%%%%%%%%%%%%%%%% | |
| 1807 | ||
| 1808 | % Theory plug-in: direct definitions | |
| 1809 | :- public direct_definition/12. | |
| 1810 | % called by btypechecker:lookup_eventb_operator | |
| 1811 | direct_definition(Params, % e.g. [argument(a,bool_set(none))] | |
| 1812 | RawWD, % Raw AST of WD condition (currently only implicit WDs from body; not yet user-defined ones) | |
| 1813 | DirectDef, % Raw AST of DirectDefinition Body, e.g., convert_bool(none,negation(none,equal(none,identifier(none,a),boolean_true(none)))) | |
| 1814 | PT, | |
| 1815 | OpId, TArgs, Pos, | |
| 1816 | Env, % environment of operators | |
| 1817 | ExPr,Result,TRin,TRout) :- | |
| 1818 | (Params,DirectDef) = (NewParams,NewDirectDefBody), %gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody), | |
| 1819 | apply_direct_definition(OpId,TArgs,NewParams, | |
| 1820 | NewDirectDefBody,RawWD, | |
| 1821 | PT,Env,Pos,TLetIds,TLetValues, | |
| 1822 | TDef,InferredType,TWDPred, | |
| 1823 | TRin,TRout), | |
| 1824 | NewInfos = [nodeid(Pos),was(extended_expr(OpId))], | |
| 1825 | (is_truth(TWDPred) -> add_texpr_infos_if_new(TDef,NewInfos,LetBody) | |
| 1826 | ; get_preference(find_abort_values,false) -> LetBody=TDef % currently tests 1201, 2232 would fail | |
| 1827 | % TODO: should we disable the inclusion of the WD condition for older .eventb files? | |
| 1828 | ; InferredType=pred | |
| 1829 | -> ajoin(['Well-definedness error for predicate operator ',OpId],MsgStr), | |
| 1830 | TMsg = b(string(MsgStr),string,[]), | |
| 1831 | safe_create_texpr(convert_bool(TWDPred),boolean,[nodeid(Pos)],WDBool), % we require an expression argument | |
| 1832 | safe_create_texpr(external_pred_call('ASSERT_TRUE',[WDBool,TMsg]),pred,NewInfos,TAssert), | |
| 1833 | conjunct_predicates_with_pos_info(TAssert,TDef,LetBody) | |
| 1834 | ; ajoin(['Well-definedness error for expression operator ',OpId],MsgStr), | |
| 1835 | safe_create_texpr(assertion_expression(TWDPred,MsgStr,TDef),InferredType,NewInfos,LetBody) | |
| 1836 | ), | |
| 1837 | %write(op(OpId,InferredType)),nl, translate:print_bexpr(LetBody),nl, | |
| 1838 | create_z_let(ExPr,TLetIds,TLetValues,LetBody,NewInfos,Result). | |
| 1839 | ||
| 1840 | ||
| 1841 | :- public axiomatic_definition/12. | |
| 1842 | % just a "dummy" interface predicate for better pretty-printing of operators in translate_eventb_operator | |
| 1843 | axiomatic_definition(_TagName, Params, DirectDef, PT, | |
| 1844 | Id, TArgs, Pos, Env, ExPr,Result,TRin,TRout) :- | |
| 1845 | direct_definition(Params, truth(none), DirectDef, PT, Id, TArgs, Pos, Env, ExPr,Result,TRin,TRout). | |
| 1846 | ||
| 1847 | % Example: ddef([argument(R,pow_subset(none,identifier(none,T)))],seq(none,identifier(none,R)),[T],seq) | |
| 1848 | ||
| 1849 | % this code not needed as we now systematically rename in create_z_let | |
| 1850 | %:- use_module(input_syntax_tree,[raw_replace/3]). | |
| 1851 | %gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody) :- | |
| 1852 | % maplist(alpha_rename,Params,NewParams,RenameList), %print(replaces(RenameList)),nl, | |
| 1853 | % raw_replace(DirectDef,RenameList,NewDirectDefBody,unknown). | |
| 1854 | %:- use_module(gensym,[gensym/2]). | |
| 1855 | %alpha_rename(argument(OldID,Type),argument(FreshID,Type),replace(OldID,identifier(none,FreshID))) :- | |
| 1856 | % gensym(OldID,FreshID). | |
| 1857 | ||
| 1858 | % Args are the arguments of the operator where it is used | |
| 1859 | % Params are the parameters in the operator definition | |
| 1860 | apply_direct_definition(OpId,TArgs,Params,DirectDef,RawWD,PT,Env,_Pos, | |
| 1861 | TLetIds,TLetValues,TDef,Type,TWDPred,TRin,TRout) :- | |
| 1862 | match_args_and_params(TArgs,Params,NewTArgs),!, %TArgs are the concrete arguments in the operator call | |
| 1863 | create_typed_ids(PT,ParametricTypes,TPT), | |
| 1864 | add_identifiers_to_environment(TPT,Env,SubEnv), | |
| 1865 | % type check the arguments given in the operator usage | |
| 1866 | get_texpr_types(NewTArgs,ArgTypes), | |
| 1867 | typecheck_arguments(Params,SubEnv,ArgTypes,TParams,TRin,TR2), | |
| 1868 | % type check the direct definition of the operator. To do this we need the parameters of the operators | |
| 1869 | % in the type environment. Their type is determined by the arguments of the operator call. | |
| 1870 | add_identifiers_to_environment(TParams,SubEnv,DefEnv), | |
| 1871 | btype(apply_direct_definition,DirectDef,DefEnv,Type,TDef,TR2,TR3), | |
| 1872 | debug_format(9,'Inferred type of direct definition ~w application: ~w~n',[OpId,Type]), | |
| 1873 | append(TParams,TPT,TLetIds), | |
| 1874 | maplist(create_typeset,ParametricTypes,TypeValues), | |
| 1875 | append(NewTArgs,TypeValues,TLetValues), | |
| 1876 | btype(apply_direct_definition,RawWD,DefEnv,_PredType,TWDPred,TR3,TRout). % now type check WD predicate | |
| 1877 | apply_direct_definition(OpId,TArgs,Arguments,_DirectDef,_WD,_PT,_Env,Pos, | |
| 1878 | _TParams,_,_TDef,_,_TWD,TRin,TRout) :- | |
| 1879 | length(TArgs,Len1), | |
| 1880 | length(Arguments,Len2), | |
| 1881 | write(targs(TArgs)),nl, | |
| 1882 | write(args(Arguments)),nl, | |
| 1883 | ajoin(['Wrong number of arguments (',Len1,') for call to operator ',OpId, | |
| 1884 | ', expected ',Len2],Msg), | |
| 1885 | store_typecheck_error(Msg,Pos,TRin,TRout). | |
| 1886 | ||
| 1887 | ||
| 1888 | match_args_and_params(TArgs,Params,NewTArgs) :- | |
| 1889 | same_length(TArgs,Params),!, NewTArgs=TArgs. | |
| 1890 | match_args_and_params([TArg],Params,NewTArgs) :- % can happen when calling operator in REPL using maplets | |
| 1891 | nested_couple_to_list(TArg,NewTArgs), | |
| 1892 | same_length(NewTArgs,Params). | |
| 1893 | ||
| 1894 | split_arg_and_typedef(argument(Id,TypeExpr),Id,TypeExpr). | |
| 1895 | map_to_set_type(Type,set(Type)). | |
| 1896 | typecheck_arguments(Params,Env,ArgTypes,TParams,TRin,TRout) :- | |
| 1897 | % type check the parameters' type expressions of the operator definition, they should have the same type | |
| 1898 | % as the arguments (except being a set) | |
| 1899 | % E.g. an operator "o" has one argument "arg" and type expression "T**BOOL" (with T being a parameter type of the theory), | |
| 1900 | % then for "o(5|->TRUE)" we have "couple(integer,boolean)" as the argument's type, | |
| 1901 | % we add "T" to the type environment (with type set(_)), | |
| 1902 | % then we type check the parameter expression "T**BOOL", expecting the type set(coule(integer,boolean)), | |
| 1903 | % the type check results in T being of type set(integer). | |
| 1904 | maplist(split_arg_and_typedef,Params,ParamIds,ParamTypeExprs), | |
| 1905 | same_length(Params,ArgTypes), | |
| 1906 | maplist(map_to_set_type,ArgTypes,SetArgTypes), | |
| 1907 | btype_l(ParamTypeExprs,Env,SetArgTypes,_TParamTypeExprs,TRin,TRout), | |
| 1908 | create_typed_ids(ParamIds,ArgTypes,TParams). | |
| 1909 | create_typeset(Type,TExpr) :- create_texpr(typeset,Type,[],TExpr). | |
| 1910 | ||
| 1911 | ||
| 1912 | ||
| 1913 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 1914 | % Theory plug-in: Recursive operators | |
| 1915 | :- public recursive_operator/11. | |
| 1916 | % called by btypechecker:lookup_eventb_operator | |
| 1917 | recursive_operator(Arguments,Cases,PT, | |
| 1918 | Id,TArgs,_Pos,Env,ExPr,Result,TRin,TRout) :- | |
| 1919 | % parameter types | |
| 1920 | create_typed_ids(PT,ParametricTypes,TPT), | |
| 1921 | add_identifiers_to_environment(TPT,Env,Env1), | |
| 1922 | maplist(create_typeset,ParametricTypes,LetValues), % needed for the LET | |
| 1923 | typecheck_arguments(Arguments,Env1,ArgTypes,TParamIds,TRin,TR1), | |
| 1924 | % TArgs: A,B,Cf | |
| 1925 | % TArg: A|->B|->C | |
| 1926 | get_texpr_types(TArgs,ArgTypes), | |
| 1927 | create_couple(TArgs,TArg), | |
| 1928 | length(TArgs,NumberOfArgs),OpInfo = [theory_operator(Id,NumberOfArgs)], | |
| 1929 | unique_id("opresult.",ResultId),create_typed_id(ResultId,Type,TResultId), | |
| 1930 | % TODO: infer ExPr if variable from extended_formula | |
| 1931 | ( ExPr=expr -> % Result: Comp(x|->y|->z) | |
| 1932 | % we need to append a result parameter in the comprehension set | |
| 1933 | create_texpr(function(TCompSet,TArg),Type,OpInfo,InnerResult), | |
| 1934 | append(TParamIds,[TResultId],CompSetIds),append(ArgTypes,[Type],CompSetTypes), | |
| 1935 | % make sure that we do not run into an infinite loop | |
| 1936 | store_eventb_operator(Id,freetype_operator_as_function(RecId,Type),Env1,Env2) | |
| 1937 | ; ExPr=pred -> % Result: x|->y|->z : Comp | |
| 1938 | create_texpr(member(TArg,TCompSet),pred,OpInfo,InnerResult), | |
| 1939 | CompSetIds = TParamIds,ArgTypes=CompSetTypes, | |
| 1940 | % make sure that we do not run into an infinite loop | |
| 1941 | store_eventb_operator(Id,freetype_operator_as_set(RecId),Env1,Env2) | |
| 1942 | ), | |
| 1943 | couplise_list(CompSetTypes,CompSetType), | |
| 1944 | % Comp: {i,r| Cond} | |
| 1945 | create_recursive_compset(CompSetIds,Cond,set(CompSetType),[],RecId,TCompSet), | |
| 1946 | % Params: a,b,c | |
| 1947 | % i = a|->b|->c | |
| 1948 | add_identifiers_to_environment(TParamIds,Env2,Subenv), | |
| 1949 | foldl(recursive_operator_case(Subenv,TResultId),Cases,TCases,TR1,TRout), | |
| 1950 | conjunct_predicates(TCases,Cond), | |
| 1951 | create_z_let(ExPr,TPT,LetValues,InnerResult,OpInfo,Result). | |
| 1952 | ||
| 1953 | ||
| 1954 | recursive_operator_case(Env,TResultId,case(ParamId,_,Expression,Formula),Cond,TRin,TRout) :- | |
| 1955 | % Add free identifiers of case to environment | |
| 1956 | extract_free_identifiers(Expression,TFreeIdentifiers,Env,Subenv), | |
| 1957 | % IsCase => CaseCheck | |
| 1958 | create_texpr(implication(IsCase,TCaseCheck),pred,[],Cond), | |
| 1959 | % IsCase: ParamId = constructor(x,y,z) | |
| 1960 | typecheck_parameter(ParamId,Env,TParamId), | |
| 1961 | recop_create_is_case(Expression,Subenv,IsCase,TParamId,FT,Case,TRin,TR1), | |
| 1962 | % CaseCheck: #x,y,z | Destruction & Predicate | |
| 1963 | recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,TCaseCheck,TR1,TRout). | |
| 1964 | extract_free_identifiers(typeof(_Pos,ExtExpr,_TypeExpr),TIds,In,Out) :- | |
| 1965 | extract_free_identifiers(ExtExpr,TIds,In,Out). | |
| 1966 | extract_free_identifiers(extended_expr(_Pos,_Case,Exprs,Preds),TIds,In,Out) :- | |
| 1967 | append(Exprs,Preds,Ids), | |
| 1968 | maplist(extract_free_identifier,Ids,TIds), | |
| 1969 | add_identifiers_to_environment(TIds,In,Out). | |
| 1970 | extract_free_identifier(identifier(_Pos,Id),TId) :- | |
| 1971 | create_typed_id(Id,_,TId). | |
| 1972 | typecheck_parameter(ParamId,Env,TParamId) :- | |
| 1973 | env_lookup_type(ParamId,Env,ParamType), | |
| 1974 | create_typed_id(ParamId,ParamType,TParamId). | |
| 1975 | %env_store_type(Id,Type,In,Out) :- | |
| 1976 | % % Version without Info field | |
| 1977 | % env_store(Id,Type,[],In,Out). | |
| 1978 | recop_create_is_case(typeof(_,Expr,_TypeExpr),Env,IsCase,TParamId,FT,Case,TRin,TRout) :- | |
| 1979 | recop_create_is_case(Expr,Env,IsCase,TParamId,FT,Case,TRin,TRout). | |
| 1980 | recop_create_is_case(Expression,Env,IsCase,TParamId,FT,Case,TRin,TRout) :- | |
| 1981 | Expression = extended_expr(_,Case,_,_), | |
| 1982 | get_texpr_type(TParamId,freetype(FT)), | |
| 1983 | btype(recop_create_is_case,Expression,Env,freetype(FT),_TCons,TRin,TRout), | |
| 1984 | create_texpr(freetype_case(FT,Case,TParamId),pred,[],IsCase). | |
| 1985 | recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,Cond,TRin,TRout) :- | |
| 1986 | % Predicate | |
| 1987 | btype(recop_create_in_case,Formula,Subenv,Type,TFormula,TRin,TRout), | |
| 1988 | ( Type=pred -> Predicate = TFormula | |
| 1989 | ; | |
| 1990 | get_texpr_types([TResultId,TFormula],[TypeA,TypeB]), | |
| 1991 | unify_types_strict(TypeA,TypeB), | |
| 1992 | create_texpr(equal(TResultId,TFormula),pred,[],Predicate)), | |
| 1993 | % Destruction: x->y|->z = destructor(ParamId) | |
| 1994 | ( TFreeIdentifiers = [] -> | |
| 1995 | Cond = Predicate | |
| 1996 | ; TFreeIdentifiers = [_|_] -> | |
| 1997 | get_texpr_types(TFreeIdentifiers,FTypes), | |
| 1998 | combine_typelist_with_prj(FTypes,FType,Projections), | |
| 1999 | unique_id("destructed",DId),create_typed_id(DId,FType,TDId), | |
| 2000 | create_texpr(freetype_destructor(FT,Case,TParamId),FType,[],Destructor), | |
| 2001 | maplist(create_inner_let(TDId),Projections,TLetExpressions), | |
| 2002 | create_z_let(pred,TFreeIdentifiers,TLetExpressions,Predicate,[],InnerLets), | |
| 2003 | create_z_let(pred,[TDId], [Destructor], InnerLets,[],Cond) | |
| 2004 | ). | |
| 2005 | ||
| 2006 | create_inner_let(TOrig,Projections,TExpr) :- | |
| 2007 | apply_projections(Projections,TOrig,TExpr). | |
| 2008 | ||
| 2009 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2010 | % Theory plug-in: datatype sets | |
| 2011 | :- public freetype_operator/12. | |
| 2012 | % called by btypechecker:lookup_eventb_operator | |
| 2013 | freetype_operator(FreetypeId1,Types1,TypeParams1,Usage1, | |
| 2014 | Id,TArgs,_Pos,Env,_ExPr,Result,TR,TR) :- | |
| 2015 | % make a fresh copy to prevent that several instances of the freetype propagate | |
| 2016 | % their types to each other (resulting in spurious typing errors) | |
| 2017 | copy_term(freetype(FreetypeId1,Types1,TypeParams1,Usage1), | |
| 2018 | freetype(FreetypeId, Types, TypeParams, Usage)), | |
| 2019 | maplist(map_to_set_type,Types,SetTypes), | |
| 2020 | get_texpr_types(TArgs,SetTypes), | |
| 2021 | create_freetype_compset(TArgs,Id,FreetypeId,TypeParams,Usage,Env,Result). | |
| 2022 | create_freetype_compset(TArgs,SetId,FreetypeId,TypeParams,Usage,Env,Result) :- | |
| 2023 | find_constructors_with_complex_types(TArgs,Usage,Constructors), | |
| 2024 | ( Constructors = [] -> | |
| 2025 | create_texpr(freetype_set(FreetypeId),set(freetype(FreetypeId)),[],Result) | |
| 2026 | ; | |
| 2027 | create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result)). | |
| 2028 | create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result) :- | |
| 2029 | btypechecker:add_ext_variables(TypeParams,Env,TParams,Subenv,TRin,TRout), | |
| 2030 | get_texpr_types(TParams,Types),get_texpr_types(TArgs,Types), | |
| 2031 | Type=freetype(FreetypeId), | |
| 2032 | create_texpr(identifier(freetype_element),Type,[],TId), | |
| 2033 | do_prettyprint_freetype(FreetypeId,TArgs,PP), | |
| 2034 | create_recursive_compset([TId],Let,set(Type),[freetype(PP)],RecId,Result), | |
| 2035 | store_eventb_operator(SetId,freetype_operator_as_identifier(RecId),Subenv,Subenv2), | |
| 2036 | foldl(create_cons_check(FreetypeId,Subenv2,TId),Constructors,Checks,TRin,TRout), | |
| 2037 | conjunct_predicates(Checks,Cond), | |
| 2038 | create_z_let(pred,TParams,TArgs,Cond,[],Let). | |
| 2039 | create_cons_check(FreetypeId,Env,TId,cons(Case,Exprs),Check,TRin,TRout) :- | |
| 2040 | btype_l(Exprs,Env,_Types,TExprs,TRin,TRout), | |
| 2041 | combine_exprlist_to_cprod(TExprs,Set), | |
| 2042 | get_texpr_type(Set,set(Type)), | |
| 2043 | create_texpr(freetype_case(FreetypeId,Case,TId),pred,[],CheckCase), | |
| 2044 | create_texpr(freetype_destructor(FreetypeId,Case,TId),Type,[],Value), | |
| 2045 | create_texpr(member(Value,Set),pred,[],Membercheck), | |
| 2046 | create_texpr(implication(CheckCase,Membercheck),pred,[],Check). | |
| 2047 | % this is used to pretty-print the resulting comprehension set | |
| 2048 | do_prettyprint_freetype(Id,Params,R) :- | |
| 2049 | maplist(translate_bexpression,Params,Strs), | |
| 2050 | ajoin_with_sep(Strs,',',S), | |
| 2051 | functor(Id,I,_), | |
| 2052 | ajoin([I,'(',S,')'],R). | |
| 2053 | ||
| 2054 | find_constructors_with_complex_types(TArgs,Usage,Constructors) :- | |
| 2055 | find_complex_type_params(TArgs,ComplexTP), | |
| 2056 | findall(cons(Id,DestructorExprs), | |
| 2057 | ( member(used_param_types(Id,UsedParamTypes,DestructorExprs),Usage), | |
| 2058 | ord_intersect(UsedParamTypes,ComplexTP)), | |
| 2059 | Constructors). | |
| 2060 | % returns the indeces of the type arguments that are not only types | |
| 2061 | find_complex_type_params(TArgs,ComplexTP) :- | |
| 2062 | findall(N,(nth1(N,TArgs,TArg),\+ is_just_type(TArg)),ComplexTP1), | |
| 2063 | sort(ComplexTP1,ComplexTP). | |
| 2064 | ||
| 2065 | :- public freetype_operator_as_identifier/9. | |
| 2066 | freetype_operator_as_identifier(RecId,Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :- | |
| 2067 | get_texpr_types(TArgs,SetTypes), | |
| 2068 | maplist(map_to_set_type,Types,SetTypes), | |
| 2069 | create_freetype_typeid(Id,Types,FreetypeId), | |
| 2070 | create_recursion_ref(RecId,set(freetype(FreetypeId)),Result). | |
| 2071 | ||
| 2072 | :- public freetype_operator_as_function/10. | |
| 2073 | freetype_operator_as_function(RecId,RType,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :- | |
| 2074 | create_couple(TArgs,TArg), get_texpr_type(TArg,Type), | |
| 2075 | create_recursion_ref(RecId,set(couple(Type,RType)),TFunction), | |
| 2076 | create_texpr(function(TFunction,TArg),RType,[],Result). | |
| 2077 | ||
| 2078 | :- public freetype_operator_as_set/9. | |
| 2079 | freetype_operator_as_set(RecId,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :- | |
| 2080 | create_couple(TArgs,TArg), get_texpr_type(TArg,Type), | |
| 2081 | create_recursion_ref(RecId,set(Type),TSet), | |
| 2082 | create_texpr(member(TArg,TSet),pred,[],Result). | |
| 2083 | ||
| 2084 | create_recursion_ref(RecId,Type,TId) :- | |
| 2085 | create_texpr(identifier(RecId),Type,[for_recursion],TId). | |
| 2086 | ||
| 2087 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2088 | % Theory plug-in: datatype constructors | |
| 2089 | :- public constructor_operator/10. % TO DO: ensure by another mechanism that Spider detects that this is called | |
| 2090 | % called by btypechecker:lookup_eventb_operator | |
| 2091 | constructor_operator(FreetypeId1,[],Id,[],_Pos,_Env,_ExPr,Result,TRin,TRout) :- | |
| 2092 | !, copy_term(FreetypeId1,FreetypeId), | |
| 2093 | create_texpr(value(freeval(FreetypeId,Id,term(Id))), | |
| 2094 | freetype(FreetypeId),[],Result), | |
| 2095 | TRin = TRout. | |
| 2096 | constructor_operator(FreetypeId1,ParamTypes1, | |
| 2097 | Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :- | |
| 2098 | copy_term(constructor(FreetypeId1,ParamTypes1),constructor(FreetypeId,ParamTypes)), | |
| 2099 | get_texpr_types(TArgs,ParamTypes), | |
| 2100 | combine_exprlist_to_couple(TArgs,TArg), | |
| 2101 | %format('Generated freetype constructor call ~w for Rodin theory datatype ~w~n',[Id,FreetypeId]), | |
| 2102 | create_texpr(freetype_constructor(FreetypeId,Id,TArg),freetype(FreetypeId),[],Result). | |
| 2103 | ||
| 2104 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2105 | % Theory plug-in: datatype destructors | |
| 2106 | :- public destructor_operator/13. % TO DO: ensure by another mechanism that Spider detects that this is called | |
| 2107 | % called by btypechecker:lookup_eventb_operator | |
| 2108 | destructor_operator(OpName,FreetypeId1,Projections,Case,CType1, | |
| 2109 | _Id,[TArg],_Pos,_Env,_ExPr,Result,TR,TR) :- | |
| 2110 | copy_term(destructor(FreetypeId1,CType1),destructor(FreetypeId,CType)), | |
| 2111 | get_texpr_type(TArg,freetype(FreetypeId)), | |
| 2112 | debug_format(19,'Generated freetype destructor ~w call ~w for Rodin theory datatype ~w~n',[OpName,Case,FreetypeId]), | |
| 2113 | create_texpr(freetype_destructor(FreetypeId,Case,TArg),CType,[],Destructed), | |
| 2114 | apply_projections(Projections,Destructed,Result0), | |
| 2115 | add_texpr_infos(Result0,[was(extended_expr(OpName))],Result). | |
| 2116 | ||
| 2117 | % create an projection expression (or a combination of arbitrary many) to | |
| 2118 | % access a part of a couple. The input is a list of prj1/prj2 atoms, | |
| 2119 | % e.g. [prj1,prj1,prj2]: Take the first of the first of the second element. | |
| 2120 | apply_projections(Projections,Expr,Result) :- | |
| 2121 | reverse(Projections,Prjs), | |
| 2122 | apply_projections1(Prjs,Expr,Result). | |
| 2123 | apply_projections1([],Expr,Expr). | |
| 2124 | apply_projections1([P|Rest],Expr,Result) :- | |
| 2125 | get_texpr_type(Inner,couple(A,B)), | |
| 2126 | apply_projections2(P,A,B,Result,Inner), | |
| 2127 | apply_projections1(Rest,Expr,Inner). | |
| 2128 | apply_projections2(prj1,A,_B,Result,Inner) :- | |
| 2129 | create_texpr(first_of_pair(Inner),A,[],Result). | |
| 2130 | apply_projections2(prj2,_A,B,Result,Inner) :- | |
| 2131 | create_texpr(second_of_pair(Inner),B,[],Result). | |
| 2132 | ||
| 2133 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2134 | % Theory plug-in: axiomatic definitions of operators | |
| 2135 | store_axiomatic_operator(Id,TypeParas,axiomatic_def_block(_Id,_Types,OpDefs,_Axioms),Ops) :- | |
| 2136 | % in case we do not recognize the operator, we store an error message | |
| 2137 | % that is shown as soon the operator is used somewhere | |
| 2138 | get_theory_name(Id,Project,Theory), % extract project and theory name | |
| 2139 | maplist(store_axdef_error(Project,Theory,TypeParas),OpDefs,Ops). | |
| 2140 | store_axdef_error(Project,Theory,TypeParas, | |
| 2141 | opdef(Id,Arguments,_WD),Id-unsupported_operator(Project,Theory,TypeParas,Arguments,Msg)) :- | |
| 2142 | % The opdef information from the Rodin export is missing the result type | |
| 2143 | % TODO fix this so that we could still typecheck and delay the error message until the operator is used | |
| 2144 | length(Arguments,Len), %write(opdef(Id,Arguments)),nl, | |
| 2145 | ajoin(['Axiomatic defined operator \"',Id,'\" of arity ', Len,' not recognized. Be sure to add a ', | |
| 2146 | Theory,'.ptm file to your Theory project ', | |
| 2147 | Project],Msg). | |
| 2148 | ||
| 2149 | % generate default mappings for axiomatic operators in case no .ptm file is provided and the args match | |
| 2150 | is_axiomatic_def(Id,Arguments,axiomatic_def_block(_Id,_Types,OpDefs,_Axioms)) :- | |
| 2151 | member(opdef(Id,Arguments,_WD),OpDefs). | |
| 2152 | is_axiomatic_def(Id,[],axiomatic_def_block(_Id,Types,_OpDefs,_Axioms)) :- | |
| 2153 | member(Id,Types). | |
| 2154 | ||
| 2155 | generate_default_mappings(AxDefs,TheoryId,DefMappings) :- | |
| 2156 | findall(tag(OpName,NewOpName), (member(Block,AxDefs), | |
| 2157 | is_axiomatic_def(OpName,Args,Block), | |
| 2158 | default_operator(OpName,NewOpName,TheoryId,Args)), DefMappings). | |
| 2159 | ||
| 2160 | default_operator(OpName,NewOpName,TheoryId,A) :- | |
| 2161 | get_theory_name(TheoryId,Project,Theory), | |
| 2162 | get_default_operator(OpName,NewOpName,A,Theory), | |
| 2163 | add_default_operator_warning(OpName,NewOpName,Theory,Project,unknown). | |
| 2164 | get_default_operator('\x211D\','REAL',Args,_) :- !, | |
| 2165 | Args=[]. % Real unicode symbol, in .ptm file the Prolog internal name cannot use unicode | |
| 2166 | get_default_operator('SUM','SIGMA',[argument(_,ArgT)],_) :- !, | |
| 2167 | relation_to_integer_type(ArgT). % from StandardLibrary SUMandPRODUCT | |
| 2168 | get_default_operator('PRODUCT','PI',[argument(_,ArgT)],_) :- !, relation_to_integer_type(ArgT). | |
| 2169 | get_default_operator(cls,closure1,[argument(_,ArgT)],'closure') :- !, | |
| 2170 | % from Standard Library theory "closure"; but it uses a direct_definition and this rewriting does not trigger! | |
| 2171 | binary_relation_type(ArgT). | |
| 2172 | get_default_operator(Name,NewName,[_,_],_) :- binary_external_function(Name,NewName),!. | |
| 2173 | get_default_operator(Name,NewName,[_,_],_) :- binary_external_predicate(Name,NewName),!. | |
| 2174 | get_default_operator(Name,Name,Args,_) :- default_operator_aux(Name,Args). | |
| 2175 | ||
| 2176 | add_default_operator_warning(OpName,NewOpName,Theory,Project,Pos) :- | |
| 2177 | ajoin(['operator "',OpName,'" internal {',NewOpName,'}'],Decl), | |
| 2178 | (get_preference(auto_detect_theory_ops,true) | |
| 2179 | -> MW = 'message' | |
| 2180 | ; MW = 'warning set AUTO_DETECT_THEORY_MAPPING to TRUE or' | |
| 2181 | ), | |
| 2182 | ajoin(['Automatically translating axiomatic operator ',OpName, | |
| 2183 | '; to get rid of this ', MW, ' add a ', | |
| 2184 | Theory,'.ptm file to your project ', | |
| 2185 | Project, ' with this line: '],Msg), | |
| 2186 | (get_preference(auto_detect_theory_ops,true) | |
| 2187 | -> add_message(bmachine_eventb,Msg,Decl,Pos) | |
| 2188 | ; add_warning(bmachine_eventb,Msg,Decl,Pos) | |
| 2189 | ). | |
| 2190 | ||
| 2191 | default_operator_aux(choose,Args) :- !, Args = [argument(_,pow_subset(_,_))]. | |
| 2192 | default_operator_aux(mu,Args) :- !, Args=[argument(_,pow_subset(_,_))]. | |
| 2193 | default_operator_aux(closure,[argument(_,ArgT)]) :- !, | |
| 2194 | binary_relation_type(ArgT). | |
| 2195 | default_operator_aux(closure1,[argument(_,ArgT)]) :- !, | |
| 2196 | binary_relation_type(ArgT). | |
| 2197 | default_operator_aux(OpName,[]) :- constant_operator_raw_term(OpName,_). | |
| 2198 | default_operator_aux(OpName,[A1]) :- unary_operator_raw_term(OpName,A1,_). | |
| 2199 | default_operator_aux(OpName,[A1,A2]) :- | |
| 2200 | binary_operator_raw_term(OpName,A1,A2,_,_), | |
| 2201 | \+ binary_expr_op(OpName,_,_). % we have typed default rules; delay decision until typing info is available | |
| 2202 | ||
| 2203 | ||
| 2204 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2205 | % Theory plug-in: Tagged operators that can be replaced by internal constructs | |
| 2206 | handle_mappings(TheoryId,PT,tag(Opname,Tag),Ops,OPin/AxDefsin,OPout/AxDefsOut) :- !, | |
| 2207 | ( extract_operator(Opname,Operator,OPin/AxDefsin,OPout/AxDefsOut,Kind) -> | |
| 2208 | (Tag=[_|_] -> debug_format(19,"Mapping Theory Operator ~s -> ~w~n",[Tag,Opname]) | |
| 2209 | ; debug_format(19,"Mapping Theory Operator ~w -> ~w~n",[Tag,Opname])), | |
| 2210 | (store_operator_by_tag(Tag,Opname,Operator,TheoryId,PT,Ops,Kind) | |
| 2211 | -> true | |
| 2212 | ; | |
| 2213 | ajoin(['Error mapping theory operator ',Opname, | |
| 2214 | ' to ProB tag (the *.ptm file maybe incorrect or you need a newer version of ProB):'],Msg), | |
| 2215 | add_error(bmachine_eventb,Msg,Tag)) | |
| 2216 | ; | |
| 2217 | ajoin(['ProB theory mapping: operator ',Opname,' not found, mapping to ',Tag,' ignored.'],Msg), | |
| 2218 | add_warning(bmachine_eventb,Msg), | |
| 2219 | OPin/AxDefsin=OPout/AxDefsOut,Ops=[] | |
| 2220 | ). | |
| 2221 | handle_mappings(_TheoryID,_ParamTypes,Mapping,[],X,X) :- | |
| 2222 | functor(Mapping,Functor,Arity), | |
| 2223 | ajoin(['ProB theory mapping: unexpected entry of type ',Functor,'/',Arity,', entry ignored.'],Msg), | |
| 2224 | add_error(bmachine_eventb,Msg). | |
| 2225 | ||
| 2226 | extract_operator(Opname,Operator,OPin/AxDefs,OPout/AxDefs,Kind) :- | |
| 2227 | % a regular non-axiomatic operator (direct definition or recursive definition): | |
| 2228 | Operator = operator(Opname,_Parameters,_WD,DirectDef,_RecursiveDef), | |
| 2229 | selectchk(Operator,OPin,OPout),!, | |
| 2230 | % TODO: we could try and infer/store type of operator from Definition and check against axiomatic one | |
| 2231 | (DirectDef=[] -> Kind='RECURSIVE-DEF-OVERRIDE' ; Kind = 'DIRECT-DEF-OVERRIDE'), | |
| 2232 | debug_format(19,'Overriding non-axiomatic operator ~w with new definition from .ptm file~n',[Opname]). | |
| 2233 | extract_operator(Opname,Operator,OP/AxDefsIn,OP/AxDefsOut,'AXIOMATIC-DEF') :- | |
| 2234 | Operator = axdef(Opname,Parameters,WD,block(Id,Types,Axioms)), % block/3 does not seem to be used | |
| 2235 | select(axiomatic_def_block(Id,Types,OpDefsIn,Axioms),AxDefsIn, | |
| 2236 | axiomatic_def_block(Id,Types,OpDefsOut,Axioms),AxDefsOut), | |
| 2237 | select(opdef(Opname,Parameters,WD),OpDefsIn,OpDefsOut),!. | |
| 2238 | extract_operator(Opname,Operator,OP/AxDefsIn,OP/AxDefsOut,'AXIOMATIC-TYPE') :- | |
| 2239 | % we treat a type of an axiomatic definition also as a potential operator that can be mapped | |
| 2240 | Operator = axdef(Opname,[],WD,block(Id,TypesOut,Axioms)), WD=[], | |
| 2241 | select(axiomatic_def_block(Id,TypesIn,OpDefs,Axioms),AxDefsIn, | |
| 2242 | axiomatic_def_block(Id,TypesOut,OpDefs,Axioms),AxDefsOut), | |
| 2243 | select(Opname,TypesIn,TypesOut),!. | |
| 2244 | ||
| 2245 | % two versions are supported: The older one expects an atom Tag, the new one a string | |
| 2246 | % The string version is then parsed as a Prolog term. | |
| 2247 | % as of 2023 we also support the bexpr(RawExpr) tag generated from $Expr$ in the .ptm file | |
| 2248 | store_operator_by_tag(Tag,Opname,Operator,TheoryID,PT,Ops,Kind) :- | |
| 2249 | is_list(Tag),!, % A string | |
| 2250 | append(Tag,".",Tag1), % read_from_codes/2 needs a full-stop at the end | |
| 2251 | read_from_codes(Tag1,Term), | |
| 2252 | store_operator_by_tag(Term,Opname,Operator,TheoryID,PT,Ops,Kind). | |
| 2253 | store_operator_by_tag(Tag,Opname,Operator,TheoryID,PT,Ops,Kind) :- | |
| 2254 | store_operator_by_tag1(Tag,Opname,Operator,PT,Ops), | |
| 2255 | get_operator_parameters(Operator,Parameters), | |
| 2256 | pretty_print_tag(Tag,PrettyTag), | |
| 2257 | store_operator_definition(TheoryID,Opname,Parameters, | |
| 2258 | function(none,identifier(none,Kind),[identifier(none,PrettyTag)]),truth(none),[], | |
| 2259 | axiomatic). % for bvisual2: todo pass type params PT | |
| 2260 | ||
| 2261 | :- use_module(translate,[translate_raw_bexpr_with_limit/3]). | |
| 2262 | pretty_print_tag(bexpr(Raw),TS) :- translate_raw_bexpr_with_limit(Raw,100,TS),!. % TODO: unicode | |
| 2263 | pretty_print_tag(Tag,Tag). | |
| 2264 | ||
| 2265 | store_operator_by_tag1(Tag,Opname,Operator,PT,Ops) :- | |
| 2266 | debug_format(19,'Storing tag ~w for operator ~w~n',[Tag,Opname]), | |
| 2267 | % SIGMA or PI | |
| 2268 | aggregation_operator(Tag,Functor),!, | |
| 2269 | get_operator_parameters(Operator,Parameters), | |
| 2270 | ( Parameters = [Arg] -> | |
| 2271 | create_raw_aggregation_op(Functor,Arg,ClassicalBOp), | |
| 2272 | Ops=[Opname-axiomatic_definition(Tag,[Arg],ClassicalBOp,PT)] | |
| 2273 | ; | |
| 2274 | parameter_error(Parameters,1,Opname),Ops=[] | |
| 2275 | ). | |
| 2276 | store_operator_by_tag1(mkinat,OpName,Operator,PT,Ops) :- !, | |
| 2277 | store_operator_by_tag1(mkinat(iZero,iSucc),OpName,Operator,PT,Ops). | |
| 2278 | store_operator_by_tag1(mkinat(ZeroOp,SuccOp),OpName,Operator,_PT,Ops) :- !, | |
| 2279 | get_operator_parameters(Operator,Parameters), | |
| 2280 | ( Parameters = [argument(Arg,_ArgType)] -> | |
| 2281 | Ops=[OpName-make_inductive_natural(Arg,ZeroOp,SuccOp)] | |
| 2282 | ; | |
| 2283 | parameter_error(Parameters,1,OpName),Ops=[] | |
| 2284 | ). | |
| 2285 | store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :- | |
| 2286 | unary_operator_raw_term(BOperator,Arg1,Expr), !, | |
| 2287 | check_if_operator_expr_uses_reals(Expr), | |
| 2288 | get_operator_parameters(Operator,Parameters), | |
| 2289 | ( Parameters = [argument(Arg1,_ArgType)] -> | |
| 2290 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,Expr,PT)] | |
| 2291 | ; Parameters = [] -> % The Rodin theory operator is a constant without arguments | |
| 2292 | Arg1='OpArg1', | |
| 2293 | CArgs = [identifier(none,Arg1)], | |
| 2294 | % try and generate lambda if we have an expression and relation for predicate | |
| 2295 | % we assume they are all expressions: | |
| 2296 | CurryExpr = lambda(none,CArgs,truth(none),Expr), | |
| 2297 | % TODO: use ArgType1 in CurryExpr | |
| 2298 | add_message(bmachine_eventb,'Lifting ProB unary operator to lambda expression (Rodin theory operator has no arguments): ',BOperator), | |
| 2299 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,CurryExpr,PT)] | |
| 2300 | ; | |
| 2301 | parameter_error(Parameters,1,Opname),Ops=[] | |
| 2302 | ). | |
| 2303 | store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :- | |
| 2304 | binary_operator_raw_term(BOperator,Arg1,Arg2,Expr,Kind), !, | |
| 2305 | check_if_operator_expr_uses_reals(Expr), | |
| 2306 | get_operator_parameters(Operator,Parameters), | |
| 2307 | ( Parameters = [argument(Arg1,_ArgType1), argument(Arg2,_ArgType2)] -> | |
| 2308 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,Expr,PT)] | |
| 2309 | ; Parameters = [] -> % The Rodin theory operator is a constant without arguments | |
| 2310 | Arg1='OpArg1', Arg2='OpArg2', | |
| 2311 | CArgs = [identifier(none,Arg1),identifier(none,Arg2)], | |
| 2312 | % try and generate lambda if we have an expression and relation for predicate | |
| 2313 | (Kind=expression | |
| 2314 | -> CurryExpr = lambda(none,CArgs,truth(none),Expr) | |
| 2315 | ; CurryExpr = comprehension_set(none,CArgs,Expr) | |
| 2316 | ), | |
| 2317 | % TODO: use ArgType1/2 in CurryExpr | |
| 2318 | add_message(bmachine_eventb,'Lifting ProB binary operator to lambda expression (Rodin theory operator has no arguments): ',BOperator), | |
| 2319 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,CurryExpr,PT)] | |
| 2320 | ; | |
| 2321 | parameter_error(Parameters,2,Opname),Ops=[] | |
| 2322 | ). | |
| 2323 | store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :- | |
| 2324 | constant_operator_raw_term(BOperator,Expr), !, | |
| 2325 | check_if_operator_expr_uses_reals(Expr), | |
| 2326 | get_operator_parameters(Operator,Parameters), | |
| 2327 | map_over_raw_expr(Expr,detect_external_fun_calls,RewrittenExpr), | |
| 2328 | length(Parameters,NrParas), | |
| 2329 | %format('Mapping operator ~w (~w paras: ~w) to: ',[Opname,NrParas,Parameters]), translate:print_raw_bexpr(RewrittenExpr),nl, | |
| 2330 | ( Parameters = [] -> | |
| 2331 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,RewrittenExpr,PT)] | |
| 2332 | ; can_be_predicate(RewrittenExpr,NrParas), | |
| 2333 | maplist(argument_to_raw_id,Parameters,ParIds), | |
| 2334 | couplise_raw_list(ParIds,ParCouple) -> | |
| 2335 | % the operator is a predicate operator, in the .ptm file is a set comprehension defining it | |
| 2336 | MembershipTest = member(none,ParCouple,RewrittenExpr), | |
| 2337 | debug_println(19,created_membership_for_predicate_operator_call(Opname)), | |
| 2338 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,MembershipTest,PT)] | |
| 2339 | ; % Create function application for set comprehensions / lambdas as parameters expected in Rodin | |
| 2340 | can_be_function(RewrittenExpr,NrParas), | |
| 2341 | maplist(argument_to_raw_id,Parameters,ParIds), | |
| 2342 | couplise_raw_list(ParIds,ParCouple) -> | |
| 2343 | Fapp = function(none,RewrittenExpr,ParCouple), | |
| 2344 | debug_println(19,created_function_application_for_operator_call(Opname)), | |
| 2345 | Ops=[Opname-axiomatic_definition(BOperator,Parameters,Fapp,PT)] | |
| 2346 | ; %unreachable at the moment: | |
| 2347 | parameter_error(Parameters,0,Opname),Ops=[] | |
| 2348 | ). | |
| 2349 | ||
| 2350 | argument_to_raw_id(argument(Arg,_),identifier(none,Arg)). | |
| 2351 | ||
| 2352 | % TODO: maybe store/lookup type of operator and check if it is a predicate operator | |
| 2353 | can_be_predicate(comprehension_set(_,Paras,_),NrParas) :- | |
| 2354 | length(Paras,NrParas). | |
| 2355 | can_be_predicate(symbolic_comprehension_set(Pos,Paras,B),NrParas) :- | |
| 2356 | can_be_predicate(comprehension_set(Pos,Paras,B),NrParas). | |
| 2357 | can_be_predicate(event_b_comprehension_set(Pos,Paras,B,_E),NrParas) :- | |
| 2358 | can_be_predicate(comprehension_set(Pos,Paras,B),NrParas). | |
| 2359 | can_be_predicate(symbolic_event_b_comprehension_set(Pos,Paras,B,E),NrParas) :- | |
| 2360 | can_be_predicate(event_b_comprehension_set(Pos,Paras,B,E),NrParas). | |
| 2361 | ||
| 2362 | ||
| 2363 | % TODO: check if NrParas compatible | |
| 2364 | can_be_function(comprehension_set(_,_,_),_NrParas) :- !. | |
| 2365 | can_be_function(lambda(_,_,_,_),_) :- !. | |
| 2366 | can_be_function(symbolic_comprehension_set(_,_,_),_) :- !. | |
| 2367 | can_be_function(event_b_comprehension_set(_,_,_),_NrParas) :- !. | |
| 2368 | can_be_function(symbolic_event_b_comprehension_set(_,_,_,_),_) :- !. | |
| 2369 | can_be_function(sequence_extension(_,_),_) :- !. | |
| 2370 | can_be_function(E,_) :- functor(E,F,N), add_message(bmachine_eventb,'Attempting function application for:',F/N). | |
| 2371 | ||
| 2372 | couplise_raw_list([Arg],Res) :- !, Res=Arg. | |
| 2373 | couplise_raw_list([A,B],Res) :- !, Res=couple(none,A,B). | |
| 2374 | couplise_raw_list([A,B|Rest],Result) :- | |
| 2375 | couplise_raw_list([couple(A,B)|Rest],Result). | |
| 2376 | ||
| 2377 | ||
| 2378 | :- use_module(external_functions, [get_external_function_type/3]). | |
| 2379 | % traverse raw AST to detect calls to external functions which would not be visible in regular typechecking | |
| 2380 | % these expressions come from the .ptm files where we want to be able to have access to external functions | |
| 2381 | % TODO: also allow access to external predicates and external constants like REULER | |
| 2382 | detect_external_fun_calls(function(Pos,TID,Args),external_function_call_auto(Pos,ID,NewArgs)) :- | |
| 2383 | TID = identifier(_IdPos,ID), | |
| 2384 | get_external_function_type(ID,ExpectedArgTypes,_OutputType), % TODO: check visible | |
| 2385 | length(Args,Len), | |
| 2386 | length(ExpectedArgTypes,ExtExpectedLen), | |
| 2387 | (Len=ExtExpectedLen -> true | |
| 2388 | ; parameter_error(Args,ExtExpectedLen,ID),fail), | |
| 2389 | !, | |
| 2390 | debug_println(19,detected_external_function_call(ID,Len)), | |
| 2391 | map_over_args(Args,NewArgs). % we need to inspect tree of arguments as well, map_over_raw_expr works top-down | |
| 2392 | ||
| 2393 | map_over_args([],[]). | |
| 2394 | map_over_args([Arg1|T],[NewArg1|NT]) :- map_over_raw_expr(Arg1,detect_external_fun_calls,NewArg1), | |
| 2395 | map_over_args(T,NT). | |
| 2396 | ||
| 2397 | ||
| 2398 | % TO DO ternary operator ?? son/3 if_then_else | |
| 2399 | ||
| 2400 | % construct a raw term with arguments for replacement in AST | |
| 2401 | % first argument is functor name as it appears in the theory mapping file *.ptm | |
| 2402 | binary_operator_raw_term(Functor,Arg1,Arg2,Term,Kind) :- | |
| 2403 | binary_operator_to_ast(Functor,ASTFunctor,Kind), % TODO: return Kind | |
| 2404 | Term =.. [ASTFunctor,none,identifier(none,Arg1),identifier(none,Arg2)]. | |
| 2405 | binary_operator_raw_term(Functor,Arg1,Arg2,Term,predicate) :- | |
| 2406 | binary_external_predicate(Functor,ASTFunctor), | |
| 2407 | Term = external_pred_call_auto(none, ASTFunctor, [identifier(none,Arg1),identifier(none,Arg2)]). | |
| 2408 | binary_operator_raw_term(Functor,Arg1,Arg2,Term,expression) :- | |
| 2409 | binary_external_function(Functor,ASTFunctor), | |
| 2410 | Term = external_function_call_auto(none, ASTFunctor, [identifier(none,Arg1),identifier(none,Arg2)]). | |
| 2411 | ||
| 2412 | binary_operator_to_ast(BOP,ASTFunctor,expression) :- | |
| 2413 | binary_expr_operator_to_ast(BOP,ASTFunctor). | |
| 2414 | binary_operator_to_ast(BOP,ASTFunctor,predicate) :- | |
| 2415 | binary_pred_operator_to_ast(BOP,ASTFunctor). | |
| 2416 | binary_expr_operator_to_ast('^',concat). | |
| 2417 | binary_expr_operator_to_ast(concat,concat). | |
| 2418 | %binary_expr_operator_to_ast(div,floored_div). % now dealt with in get_typed_default_operator | |
| 2419 | binary_expr_operator_to_ast(restrict_front,restrict_front). | |
| 2420 | binary_expr_operator_to_ast(restrict_tail,restrict_tail). | |
| 2421 | % binary tree operators | |
| 2422 | binary_expr_operator_to_ast(arity,arity). | |
| 2423 | binary_expr_operator_to_ast(bin,bin). | |
| 2424 | binary_expr_operator_to_ast(const,const). | |
| 2425 | binary_expr_operator_to_ast(father,father). | |
| 2426 | binary_expr_operator_to_ast(rank,rank). | |
| 2427 | binary_expr_operator_to_ast(subtree,subtree). | |
| 2428 | % real operators | |
| 2429 | binary_expr_operator_to_ast(rdiv,div_real). | |
| 2430 | binary_expr_operator_to_ast(plus,add_real). | |
| 2431 | binary_expr_operator_to_ast(power_of_real,power_of_real). | |
| 2432 | binary_expr_operator_to_ast(power_of,power_of). % also in get_typed_default_operator | |
| 2433 | binary_expr_operator_to_ast(pow,power_of). % ditto | |
| 2434 | binary_expr_operator_to_ast(minus,minus_real). | |
| 2435 | binary_expr_operator_to_ast(mul,multiplication_real). | |
| 2436 | binary_expr_operator_to_ast(mult,multiplication_real). | |
| 2437 | % real predicates: | |
| 2438 | binary_pred_operator_to_ast(less,less_real). | |
| 2439 | binary_pred_operator_to_ast(less_equal,less_equal_real). | |
| 2440 | binary_pred_operator_to_ast('smr',less_real). % from Rodin Real Theory v.2.1 | |
| 2441 | binary_pred_operator_to_ast(leq,less_equal_real). % from Rodin Real Theory v.2.1 | |
| 2442 | % Note: there is currently no greater_real and greater_equal_real | |
| 2443 | ||
| 2444 | binary_external_predicate('\x22D7\','RGT'). % 8919 - greater with dot | |
| 2445 | binary_external_predicate(greater,'RGT'). | |
| 2446 | binary_external_predicate(greater_equal,'RGEQ'). | |
| 2447 | binary_external_predicate('\x22D6\','RLT'). % 8918 - less with dot | |
| 2448 | %binary_external_predicate(less,'RLT'). | |
| 2449 | %binary_external_predicate(less_equal,'RLEQ'). | |
| 2450 | binary_external_predicate(geq,'RGEQ'). | |
| 2451 | %binary_external_predicate(leq,'RLEQ'). % from Rodin Real Theory v.2.1 | |
| 2452 | %binary_external_predicate(smr,'RLT'). % ditto | |
| 2453 | binary_external_predicate(gtr,'RGT'). % ditto | |
| 2454 | binary_external_predicate(inv,'RINV'). % ditto | |
| 2455 | binary_external_predicate(FUN,FUN) :- | |
| 2456 | treat_as_external_pred(FUN). | |
| 2457 | ||
| 2458 | treat_as_external_pred('REQ'). | |
| 2459 | treat_as_external_pred('RGT'). | |
| 2460 | treat_as_external_pred('RGEQ'). | |
| 2461 | treat_as_external_pred('RLT'). | |
| 2462 | treat_as_external_pred('RLEQ'). | |
| 2463 | treat_as_external_pred('RNEQ'). | |
| 2464 | ||
| 2465 | treat_as_external_pred('LESS'). % Prolog term order | |
| 2466 | treat_as_external_pred('LEQ_SYM_BREAK'). | |
| 2467 | treat_as_external_pred('STRING_IS_INT'). | |
| 2468 | treat_as_external_pred('STRING_IS_NUMBER'). | |
| 2469 | treat_as_external_pred('STRING_IS_DECIMAL'). | |
| 2470 | treat_as_external_pred('STRING_IS_ALPHANUMERIC'). % TODO: provide more external predicates | |
| 2471 | ||
| 2472 | binary_external_function('\x2295\','RADD'). % Unicode + with circle | |
| 2473 | binary_external_function('\x2296\','RSUB'). | |
| 2474 | binary_external_function('\x2297\','RMUL'). % has a pre-defined Rodin meaning as direct product | |
| 2475 | binary_external_function('\x2298\','RDIV'). | |
| 2476 | binary_external_function('\x2299\','RMUL'). % dot with circle | |
| 2477 | binary_external_function(FUN,FUN) :- visible_external_function(FUN,2), | |
| 2478 | \+ treat_as_external_pred(FUN). | |
| 2479 | ||
| 2480 | :- use_module(tools,[arg_is_number/2]). | |
| 2481 | % Already parsed B expression: | |
| 2482 | constant_operator_raw_term(bexpr(Tree),Tree). | |
| 2483 | % some types not available in Event-B: | |
| 2484 | constant_operator_raw_term('FLOAT',float_set(none)). | |
| 2485 | constant_operator_raw_term('REAL',real_set(none)). | |
| 2486 | constant_operator_raw_term('\x211D\',real_set(none)). % unicode Real symbol 8477 in decimal | |
| 2487 | constant_operator_raw_term('STRING',string_set(none)). | |
| 2488 | % direct encodings: | |
| 2489 | %constant_operator_raw_term('RONE',real(none,'1.0')). | |
| 2490 | %constant_operator_raw_term('RZERO',real(none,'1.0')). | |
| 2491 | constant_operator_raw_term(empty_string,string(none,'')). | |
| 2492 | constant_operator_raw_term('EMPTY_STRING',string(none,'')). | |
| 2493 | % some synonyms: | |
| 2494 | constant_operator_raw_term(zero,T) :- T = real(none,'0.0'). %constant_operator_raw_term('RZERO',T). | |
| 2495 | constant_operator_raw_term(one,T) :- T = real(none,'1.0'). %constant_operator_raw_term('RONE',T). | |
| 2496 | constant_operator_raw_term(two,T) :- T=real(none,'2.0'). | |
| 2497 | constant_operator_raw_term(pi,T) :- constant_operator_raw_term('RPI',T). | |
| 2498 | constant_operator_raw_term(euler,T) :- constant_operator_raw_term('REULER',T). | |
| 2499 | constant_operator_raw_term(Name,external_function_call_auto(none,Name,[])) :- | |
| 2500 | visible_external_function(Name,0). | |
| 2501 | constant_operator_raw_term(Atom,T) :- | |
| 2502 | arg_is_number(Atom,Number), | |
| 2503 | (integer(Number) -> T=integer(none,Number) | |
| 2504 | ; atom(Atom), % otherwise we would need to convert it to an atom for the AST | |
| 2505 | T=real(none,Atom)). | |
| 2506 | % This case shouldn't be needed anymore. | |
| 2507 | % The theorymapping library now parses formulas ahead of time | |
| 2508 | % and sends the parsed AST in a bexpr/1 term. | |
| 2509 | constant_operator_raw_term(Atom,Tree) :- | |
| 2510 | atom(Atom), atom_codes(Atom,Codes), | |
| 2511 | %format('Tag string: ~s~n',[Codes]), | |
| 2512 | get_formula_codes(Codes,FCodes), | |
| 2513 | %format('Stripped delimiter: ~s~n',[FCodes]), | |
| 2514 | parsercall:parse_formula(FCodes,Tree). | |
| 2515 | % TODO: allow B formulas also for binary/unary operators | |
| 2516 | ||
| 2517 | get_formula_codes([Del|T],Codes) :- delimiter(Del),!,skip_last(T,Codes,Del). % strip leading and trailing delimiter | |
| 2518 | skip_last([H],[],Last) :- !, Last=H. | |
| 2519 | skip_last([H|T],[H|ST],Last) :- skip_last(T,ST,Last). | |
| 2520 | ||
| 2521 | %delimiter(0'"). | |
| 2522 | delimiter(36). % dollar $ | |
| 2523 | %delimiter(39). % simple quote | |
| 2524 | ||
| 2525 | ||
| 2526 | :- use_module(external_function_declarations,[external_function_library/4]). | |
| 2527 | visible_external_function(Name,Arity) :- | |
| 2528 | external_function_library(Name,Arity,expression,Lib), | |
| 2529 | visible_lib(Lib). | |
| 2530 | ||
| 2531 | visible_lib('LibraryMath.def'). | |
| 2532 | visible_lib('LibraryRandom.def'). | |
| 2533 | visible_lib('LibraryReals.def'). | |
| 2534 | visible_lib('LibraryStrings.def'). | |
| 2535 | visible_lib('CHOOSE.def'). | |
| 2536 | visible_lib('SCCS.def'). | |
| 2537 | visible_lib('SORT.def'). | |
| 2538 | % visible_lib('LibrarySoftfloats.def'). % comment in to make Softfloats available for theory mapping | |
| 2539 | ||
| 2540 | ||
| 2541 | % construct a raw term with argument for replacement in AST | |
| 2542 | % first argument is functor name as it appears in the theory mapping file *.ptm | |
| 2543 | unary_operator_raw_term(Functor,Arg,Term) :- | |
| 2544 | unary_operator_to_ast(Functor,ASTFunctor), | |
| 2545 | Term =.. [ASTFunctor,none,identifier(none,Arg)]. | |
| 2546 | unary_operator_raw_term(Functor,Arg,Term) :- | |
| 2547 | unary_external_function(Functor,AstFunctor), | |
| 2548 | Term = external_function_call_auto(none, AstFunctor, [identifier(none,Arg)]). | |
| 2549 | unary_operator_to_ast(closure,reflexive_closure). % reflexive_closure corresponds to closure B operator ! | |
| 2550 | unary_operator_to_ast(closure1,closure). | |
| 2551 | unary_operator_to_ast(conc,general_concat). | |
| 2552 | unary_operator_to_ast(fnc,trans_function). | |
| 2553 | unary_operator_to_ast(rel,trans_relation). | |
| 2554 | unary_operator_to_ast(succ,successor). % also exist in Event-B | |
| 2555 | unary_operator_to_ast(pred,predecessor). % also exist in Event-B | |
| 2556 | unary_operator_to_ast(bool,convert_bool). % also exist in Event-B | |
| 2557 | unary_operator_to_ast(id,identity). % exists in similar way in Event-B | |
| 2558 | unary_operator_to_ast(union,general_union). | |
| 2559 | unary_operator_to_ast(inter,general_intersection). | |
| 2560 | % real operators | |
| 2561 | unary_operator_to_ast(real,convert_real). | |
| 2562 | unary_operator_to_ast(floor,convert_int_floor). | |
| 2563 | unary_operator_to_ast(ceiling,convert_int_ceiling). | |
| 2564 | unary_operator_to_ast(minus,unary_minus_real). % minus also maps to binary minus | |
| 2565 | unary_operator_to_ast(max,max_real). | |
| 2566 | unary_operator_to_ast(min,min_real). | |
| 2567 | unary_operator_to_ast(F,F) :- unary_operator(F). % operators that have same name in B and AST | |
| 2568 | ||
| 2569 | ||
| 2570 | unary_external_function(choose,'CHOOSE'). | |
| 2571 | unary_external_function(length,'STRING_LENGTH'). | |
| 2572 | unary_external_function(inv,'RINV'). | |
| 2573 | unary_external_function(Functor,Functor) :- visible_external_function(Functor,1). | |
| 2574 | ||
| 2575 | % sequence operators | |
| 2576 | unary_operator(seq). | |
| 2577 | unary_operator(seq1). | |
| 2578 | unary_operator(iseq). | |
| 2579 | unary_operator(iseq1). | |
| 2580 | unary_operator(perm). | |
| 2581 | unary_operator(first). | |
| 2582 | unary_operator(size). | |
| 2583 | unary_operator(front). | |
| 2584 | unary_operator(tail). | |
| 2585 | unary_operator(rev). | |
| 2586 | unary_operator(last). | |
| 2587 | unary_operator(mu). | |
| 2588 | % tree operators | |
| 2589 | unary_operator(tree). | |
| 2590 | unary_operator(btree). | |
| 2591 | unary_operator(top). | |
| 2592 | unary_operator(sons). | |
| 2593 | unary_operator(bin). | |
| 2594 | unary_operator(left). | |
| 2595 | unary_operator(right). | |
| 2596 | unary_operator(sizet). | |
| 2597 | unary_operator(prefix). | |
| 2598 | unary_operator(postfix). | |
| 2599 | %unary_operator(infix). % not yet supported | |
| 2600 | %unary_operator(mirror). % not yet supported | |
| 2601 | % general operators | |
| 2602 | unary_operator(min). % also exist in Event-B | |
| 2603 | unary_operator(max). % also exist in Event-B | |
| 2604 | unary_operator(domain). | |
| 2605 | unary_operator(range). | |
| 2606 | % z operators | |
| 2607 | unary_operator(compaction). | |
| 2608 | unary_operator(bag_items). | |
| 2609 | ||
| 2610 | % in the SUMandPRODUCT theory provided on https://prob.hhu.de/w/index.php?title=Event-B_Theories | |
| 2611 | % the SIGMA and PI operators work on relations TYPE <-> INTEGER | |
| 2612 | % we actually create SIGMA(I,N).(I|->N:Arg | N) or PI | |
| 2613 | % However, we now also support SIGMA and PI to work directly on integer sets | |
| 2614 | aggregation_operator('SIGMA',general_sum). | |
| 2615 | aggregation_operator('PI',general_product). | |
| 2616 | ||
| 2617 | integer_set_type(pow_subset(_,integer_set(_))). | |
| 2618 | relation_to_integer_type(pow_subset(_,cartesian_product(_,_,integer_set(_)))). | |
| 2619 | binary_relation_type(pow_subset(_,cartesian_product(_,_A,_B))). | |
| 2620 | ||
| 2621 | ||
| 2622 | create_raw_aggregation_op(Op,argument(Arg,ArgType),Result) :- | |
| 2623 | integer_set_type(ArgType),!, | |
| 2624 | % we have an operator acting directly on sets of integers | |
| 2625 | % we translate it as SIGMA(N).(N:Arg|N) | |
| 2626 | A = identifier(none,Arg), % User-given argument | |
| 2627 | create_fresh_identifier('_agg_op1',[A],I1), % starting with _ ensures user cannot create such an id | |
| 2628 | N = identifier(none,I1), % N is the integer to sum or multiply | |
| 2629 | Pred = member(none,N,A), % I|->N : Arg | |
| 2630 | Result =.. [Op,none,[N],Pred,N]. % SIGMA(I,N).(I|->N:Arg | N) (or PI) | |
| 2631 | create_raw_aggregation_op(Op,argument(Arg,_ArgType),Result) :- | |
| 2632 | % this construction will immediately wrap _agg_op1/2 inside Sigma or Pi, and thus _agg_op1/2 will not be visibile outside | |
| 2633 | A = identifier(none,Arg), % User-given argument | |
| 2634 | create_fresh_identifier('_agg_op1',[A],I1), % starting with _ ensures user cannot create such an id | |
| 2635 | create_fresh_identifier('_agg_op2',[A],I2), % (in Camille at least) | |
| 2636 | I = identifier(none,I1), % I is the (not used) index variable | |
| 2637 | N = identifier(none,I2), % N is the integer to sum or multiply | |
| 2638 | Pred = member(none,couple(none,I,N),A), % I|->N : Arg | |
| 2639 | Result =.. [Op,none,[I,N],Pred,N]. % SIGMA(I,N).(I|->N:Arg | N) (or PI) | |
| 2640 | ||
| 2641 | parameter_error(RodinParameters,ExpectedByProB,Opname) :- | |
| 2642 | length(RodinParameters,N), | |
| 2643 | ajoin(['ProB theory mapping: ProB translation expects ',ExpectedByProB,' parameter(s) for operator ', | |
| 2644 | Opname,' but Rodin definition has ',N],Msg), | |
| 2645 | add_error(bmachine_eventb,Msg). | |
| 2646 | ||
| 2647 | get_operator_parameters(operator(_Opname,Parameters,_WD,_DirectDef,_RecursiveDef),Parameters). | |
| 2648 | get_operator_parameters(axdef(_Opname,Parameters,_WD,_Block),Parameters). | |
| 2649 | ||
| 2650 | store_eventb_operator(Id,Op,Ein,Eout) :- | |
| 2651 | env_store_operator(Id,bmachine_eventb:Op,Ein,Eout). | |
| 2652 | ||
| 2653 | ||
| 2654 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2655 | % Operator for constructing inductive natural numbers (mkinat in Rodin .ptm theory mapping file) | |
| 2656 | :- public make_inductive_natural/11. | |
| 2657 | % called by btypechecker:lookup_eventb_operator | |
| 2658 | make_inductive_natural(ArgId,ZeroOp,SuccOp, | |
| 2659 | Id,[TParam],_Pos,Env,expr,Result,TRin,TRout) :- | |
| 2660 | unique_id("opresult.",ResultId), | |
| 2661 | create_typed_id(ResultId,NatType,TResult), | |
| 2662 | create_typed_id(ArgId,integer,TArgId), | |
| 2663 | % prepare environment: | |
| 2664 | add_identifiers_to_environment([TArgId,TResult],Env,Env1), | |
| 2665 | % we create a recursive function by using a (as recursive annotated) comprehension | |
| 2666 | % set. We can refer to the compset with RecId. | |
| 2667 | create_recursive_compset([TArgId,TResult],Cond,set(couple(integer,NatType)),[],RecId,TCompSet), | |
| 2668 | % used for recursive call: | |
| 2669 | env_store(RecId,set(couple(integer,NatType)),[],Env1,SubEnv), | |
| 2670 | % just type iZero to retrieve its type: | |
| 2671 | IZero=extended_expr(none,ZeroOp,[],[]), | |
| 2672 | btype(make_inductive_natural,IZero,SubEnv,NatType,_,TRin,TR1), | |
| 2673 | % Arg=0 => Result=iZero | |
| 2674 | RawCase1=implication(none, | |
| 2675 | equal(none,identifier(none,ArgId),integer(none,0)), | |
| 2676 | equal(none,identifier(none,ResultId),IZero)), | |
| 2677 | btype(make_inductive_natural,RawCase1,SubEnv,pred,Case1,TR1,TR2), | |
| 2678 | % Arg>0 => Result=iSucc( recursive_call(Arg-1) ) | |
| 2679 | RawCase2=implication(none, | |
| 2680 | greater(none,identifier(none,ArgId),integer(none,0)), | |
| 2681 | equal(none,identifier(none,ResultId),extended_expr(none,SuccOp,[Minus1],[]))), | |
| 2682 | Minus1=function(none,identifier(none,RecId),minus(none,identifier(none,ArgId),integer(none,1))), | |
| 2683 | btype(make_inductive_natural,RawCase2,SubEnv,pred,Case2,TR2,TRout), | |
| 2684 | % {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )} | |
| 2685 | conjunct_predicates([Case1,Case2],Cond), | |
| 2686 | % {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )}(TParam) | |
| 2687 | create_texpr(function(TCompSet,TParam),NatType,[theory_operator(Id,1)],Result). |