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(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(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) :- get_texpr_description(Subst,Desc).
815 ?extract_description(Subst,Desc) :- get_direct_abstract_event(Subst,ASubst),
816 extract_description(ASubst,Desc).
817
818 get_direct_abstract_event(b(RefLvlEvent,subst,_),AbsEvent) :-
819 RefLvlEvent = rlevent(_Name,_Sect,_Stat,_Paras,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,AbsEvents),
820 ? member(AbsEvent,AbsEvents).
821
822 get_events_to_animate([Model|_],Events) :- internal_model_events(Model,_,Events).
823
824 merge_refinement_levels([],_,_,[],[]).
825 merge_refinement_levels([Event|ERest],AnimModels,AnimatedSectionNames,[Merged|MRest],[Prom|PRest]) :-
826 merge_refinement_levels2(Event,AnimModels,AnimatedSectionNames,Merged,Prom),
827 merge_refinement_levels(ERest,AnimModels,AnimatedSectionNames,MRest,PRest).
828
829 merge_refinement_levels2(Event,AnimatedLevels,AnimatedSectionNames,
830 eventop(Name,Section,Parameters,Subst,OpType,Refines),Prom) :-
831 AnimatedLevels = [CurrentLevel|_Abstractions],
832 internal_model(CurrentLevel,Section),
833 internal_event_params(Event,Name,Parameters),
834 internal_event_refined(Event,Name,Refines),
835 %merge_parameters(Refines,Parameters,_Abstractions,MergedParameters),
836 merge_events_to_subst(Name,AnimatedLevels,AnimatedSectionNames,[],Subst1),
837 optimise_events(Subst1,Subst),
838 get_texpr_types(Parameters,Types),OpType = op(Types,[]),
839 create_texpr(identifier(Name),OpType,[],Prom).
840
841 gen_description_term(Desc,description(Desc)).
842
843 merge_events_to_subst(Name,[CurrentLevel|Abstractions],AnimatedSectionNames,RefinedParameters,TEvent) :-
844 create_texpr(RefLevelEvent,subst,[modifies(Vars),reads(Reads)|RestInfos],TEvent),
845 RefLevelEvent = rlevent(Name,Section,Status,Params,Guard,Theorems,Actions,
846 VWitnesses,PWitnesses,Unmodifiables,AbstractEvents),
847 InternalEvent = tc_event(Name,Section,Status,AllParams,Guard,Theorems,Actions,
848 VWitnesses1,PWitnesses1,Unmodifiables,Refines,Desc),
849 get_event_from_model(Name,CurrentLevel,InternalEvent),
850 strip_witnesses(VWitnesses1,AnimatedSectionNames,VWitnesses),
851 strip_witnesses(PWitnesses1,AnimatedSectionNames,PWitnesses),
852 remove_refined_parameters(AllParams,RefinedParameters,Params),
853 maplist(gen_description_term,Desc,RestInfos),
854 ( Abstractions = [] ->
855 AbstractEvents = []
856 ;
857 append(RefinedParameters,Params,NewRefinedParameters),
858 merge_events_to_subst_l(Refines,Abstractions,AnimatedSectionNames,NewRefinedParameters,AbstractEvents1),
859 normalise_merged_events(AbstractEvents1,AbstractEvents)
860 ),
861 collect_modified_vars(Actions,AbstractEvents,Vars),
862 collect_read_vars(Status,AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents,Reads).
863 merge_events_to_subst_l([],_,_,_,[]).
864 merge_events_to_subst_l([Name|NRest],Abstractions,AnimatedSectionNames,RefinedParameters,[TEvent|TRest]) :-
865 merge_events_to_subst(Name,Abstractions,AnimatedSectionNames,RefinedParameters,TEvent),
866 merge_events_to_subst_l(NRest,Abstractions,AnimatedSectionNames,RefinedParameters,TRest).
867
868 % removes a witness completely if the witnessed variable belongs
869 % to a refinement level that is not animated or removes part of the
870 % witness-predicate if references to not animated levels are made.
871 strip_witnesses([],_AnimatedSectionNames,[]).
872 strip_witnesses([Witness|WRest],AnimatedSectionNames,Result) :-
873 strip_witness(Witness,AnimatedSectionNames,StrippedWitness),
874 append(StrippedWitness,SWRest,Result),
875 strip_witnesses(WRest,AnimatedSectionNames,SWRest).
876 strip_witness(Witness,AnimatedSectionNames,StrippedWitness) :-
877 get_texpr_expr(Witness,witness(W,P)),
878 ( abstraction_var_occures(W,AnimatedSectionNames) ->
879 % The abstract variable is not animated, skip the complete witness
880 StrippedWitness = []
881 ;
882 conjunction_to_list(P,Preds),
883 remove_linking_parts(Preds,AnimatedSectionNames,SPreds),
884 conjunct_predicates(SPreds,SP),
885 get_texpr_type(Witness,Type),
886 get_texpr_info(Witness,Info),
887 create_texpr(witness(W,SP),Type,Info,TWitness),
888 StrippedWitness = [TWitness]).
889
890 remove_refined_parameters([],_RefinedParameters,[]).
891 remove_refined_parameters([Param|APRest],RefinedParameters,Parameters) :-
892 ? ( find_identifier_in_list(Param,RefinedParameters,_RefParam) ->
893 Parameters = PRest
894 ;
895 Parameters = [Param|PRest]),
896 remove_refined_parameters(APRest,RefinedParameters,PRest).
897
898 /* currently commented out :
899 merge_parameters([],Parameters,_Abstractions,Parameters).
900 merge_parameters([_|_],Parameters,[],Parameters) :- !.
901 merge_parameters([Refines|Rest],OldParameters,Abstractions,Parameters) :-
902 Abstractions = [Abstract|FurtherAbstractions],
903 get_event_from_model(Refines,Abstract,Event),
904 internal_event_params(Event,_,NewParameters),
905 internal_event_refined(Event,_,NewRefines),
906 add_unique_parameters(NewParameters,OldParameters,Parameters2),
907 merge_parameters(NewRefines,Parameters2,FurtherAbstractions,Parameters3),
908 merge_parameters(Rest,Parameters3,Abstractions,Parameters).
909 add_unique_parameters([],Parameters,Parameters).
910 add_unique_parameters([P|PRest],InParameters,OutParameters) :-
911 ( find_identifier_in_list(P,InParameters,_) ->
912 !,Parameters = InParameters
913 ;
914 Parameters = [P|InParameters]),
915 add_unique_parameters(PRest,Parameters,OutParameters).
916 */
917
918 get_event_from_model(Name,Model,Event) :-
919 internal_model_events(Model,_,Events),
920 internal_event(Event,Name),
921 ? member(Event,Events),!.
922
923 collect_modified_vars(Actions,Events,Vars) :-
924 get_modified_vars_of_actions(Actions,M1),
925 append_modified_vars_of_events(Events,M2),
926 append(M1,M2,M3),sort(M3,Vars).
927 get_modified_vars_of_actions([],[]).
928 get_modified_vars_of_actions([Action|Arest],Vars) :-
929 get_modified_vars_of_action(Action,Vlocal),
930 append(Vlocal,Vrest,Vars),
931 get_modified_vars_of_actions(Arest,Vrest).
932 get_modified_vars_of_action(Action,Vars) :-
933 get_texpr_info(Action,Infos),
934 ? member(modifies(Vars), Infos),!.
935
936 add_modified_vars_to_actions([],[]).
937 %add_modified_vars_to_actions([TAction|ARest],MRest) :-
938 % get_texpr_expr(TAction,skip),!, % remove skip actions % for Daniel: is this better than keeping them ??
939 % add_modified_vars_to_actions(ARest,MRest).
940 add_modified_vars_to_actions([TAction|ARest],[MAction|MRest]) :-
941 (add_modified_vars_to_action(TAction,MAction) ->true
942 ; add_internal_error('Call failed: ',add_modified_vars_to_action(TAction,MAction)),
943 MAction = TAction),
944 add_modified_vars_to_actions(ARest,MRest).
945 add_modified_vars_to_action(TAction,MAction) :-
946 get_lhs_ids(TAction,Vars),
947 maplist(prime_id,Vars,Primed),
948 add_texpr_infos(TAction,[assigned_after(Primed),modifies(Vars)],MAction).
949
950 get_lhs_ids(TAction,Ids) :-
951 get_lhs_tids(TAction,Vars),
952 get_texpr_ids(Vars,Ids).
953 get_lhs_tids(TAction,Vars) :-
954 get_texpr_expr(TAction,Action),
955 split_lhs_rhs(Action,Lhs,_),
956 extract_lhs_ids(Lhs,Vars).
957
958 split_lhs_rhs(skip,[],[]). % not needed as skip removed above
959 split_lhs_rhs(assign(Ids,Exprs),Ids,Exprs).
960 split_lhs_rhs(assign_single_id(Id,Expr),[Id],[Expr]).
961 split_lhs_rhs(becomes_element_of(Ids,Expr),Ids,[Expr]).
962 split_lhs_rhs(becomes_such(Ids,Pred),Ids,[Pred]).
963 split_lhs_rhs(evb2_becomes_such(Ids,Pred),Ids,[Pred]).
964 extract_lhs_ids([],[]).
965 extract_lhs_ids([TId|TRest],[Var|VRest]) :-
966 extract_lhs_id(TId,Var),
967 extract_lhs_ids(TRest,VRest).
968 extract_lhs_id(Id,Var) :-
969 get_texpr_id(Id,_),!,Var=Id.
970 extract_lhs_id(Func,Var) :-
971 get_texpr_expr(Func,function(Id,_)),
972 get_texpr_id(Id,Var).
973
974 append_modified_vars_of_events(Events,Vars) :-
975 append_modified_vars_of_events2(Events,Unsorted),
976 sort(Unsorted,Vars).
977 append_modified_vars_of_events2([],[]).
978 append_modified_vars_of_events2([TEvent|ERest],Vars) :-
979 get_modified_vars_of_event(TEvent,Local),
980 append(Local,VRest,Vars),
981 append_modified_vars_of_events2(ERest,VRest).
982 get_modified_vars_of_event(TEvent,Local) :-
983 get_texpr_info(TEvent,Info),
984 memberchk(modifies(Local),Info).
985
986 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
987 % get all the variables that are accessed in an event (cf also get_accessed_vars2 in b_read_write_info.pl)
988 collect_read_vars(Status,AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents,Reads) :-
989 find_variant_reads([],Status,VariantVars), % the variant cannot use params (!?)
990 get_texpr_ids(AllParams,Params), % access to parameters is not reading a variable
991 find_identifier_uses(Guard,Params,GrdVars),
992 find_identifier_uses_l(Theorems,Params,ThmVars),
993 find_identifier_uses_l(Unmodifiables,Params,UnmodVars), % for check_if_invalid_vars_are_modified we need read access
994 maplist(find_all_action_reads(Params),Actions,ActVars0), ord_union(ActVars0, ActVars),
995 maplist(find_all_witness_reads(Params),VWitnesses,VWitVars0), ord_union(VWitVars0,VWitVars),
996 maplist(find_all_witness_reads(Params),PWitnesses,PWitVars0), ord_union(PWitVars0,PWitVars),
997 join_abstract_reads(AbstractEvents,AbstrVars),
998 ord_union([VariantVars,GrdVars,ThmVars,UnmodVars,ActVars,VWitVars,PWitVars,AbstrVars],Reads).
999
1000 find_variant_reads(Ignore,TVariant,Res) :-
1001 get_texpr_expr(TVariant,Variant),
1002 (find_variant_reads2(Variant,Ignore,Vars) -> Res=Vars
1003 ; add_internal_error('Illegal variant: ',find_variant_reads2(Variant,Ignore,_)),Res=[]).
1004 find_variant_reads2(convergent(TExpr),Ignore,Vars) :- find_identifier_uses(TExpr,Ignore,Vars).
1005 find_variant_reads2(anticipated(TExpr),Ignore,Vars) :- find_identifier_uses(TExpr,Ignore,Vars).
1006 find_variant_reads2(ordinary,_,[]).
1007
1008 %find_all_identifiers(Ignore,Expr,Vars) :-
1009 % find_identifier_uses(Expr,Ignore,Vars). % Just switch arguments to allow the use of maplist
1010 find_all_action_reads(Ignore,TAction,Res) :-
1011 get_texpr_expr(TAction,Action),
1012 (find_action_reads2(Action,Ignore,Vars) -> Res=Vars
1013 ; add_internal_error('Illegal action: ',find_action_reads2(Action,Ignore,_)),Res=[]).
1014 find_action_reads2(skip,_,Vars) :- Vars=[].
1015 find_action_reads2(assign(_,Exprs),Ignore,Vars) :- find_identifier_uses_l(Exprs,Ignore,Vars).
1016 find_action_reads2(assign_single_id(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars).
1017 find_action_reads2(becomes_element_of(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars).
1018 find_action_reads2(becomes_such(Ids,Pred),Ignore,Vars1) :-
1019 % all references to Ids are to the state after: not a read
1020 get_texpr_ids(Ids,AtomicIds),
1021 append(AtomicIds,Ignore,Ignore0),sort(Ignore0,Ignore1),
1022 find_identifier_uses(Pred,Ignore1,Vars),
1023 prime_identifiers0(Ids,Ids0), % Ids with $0 afterwards
1024 get_texpr_ids(Ids0,AtomicIds0),
1025 maplist(unprime_id(AtomicIds0,AtomicIds),Vars,Vars1).
1026 %find_action_reads2(evb2_becomes_such(Ids,Pred),Ignore,Vars) :-
1027 % prime_variables(Ids,PIds),get_texpr_ids(PIds,Primes),
1028 % append(Primes,Ignore,Ignore0),sort(Ignore0,Ignore1),
1029 % find_identifier_uses(Pred,Ignore1,Vars).
1030 find_all_witness_reads(Ignore,Witness,Vars) :-
1031 get_texpr_expr(Witness,witness(I,P)),
1032 get_texpr_id(I,Id),
1033 sort([Id|Ignore],Ignore2),
1034 find_identifier_uses(P,Ignore2,Vars1),
1035 % a small hack to remove the primed variables that refer to the after-state
1036 % without the need to put all variables in the Ingore list:
1037 exclude(is_primed_id,Vars1,Vars).
1038
1039 join_abstract_reads([],[]) :- !.
1040 join_abstract_reads(AbstractEvents,Reads) :-
1041 maplist(get_read_from_info,AbstractEvents,AbsReads),
1042 ord_union(AbsReads,ReadBySome),
1043 maplist(get_modifies_from_info,AbstractEvents,AbsModifies),
1044 ord_union(AbsModifies,ModifiedBySome),
1045 ord_intersection(AbsModifies,ModifiedByAll),
1046 ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll),
1047 ord_union(ReadBySome,ModifiedByNotAll,Reads).
1048 get_read_from_info(AbstrEvents,Reads) :-
1049 get_texpr_info(AbstrEvents,Info),memberchk(reads(Reads),Info).
1050 get_modifies_from_info(AbstrEvents,Modifies) :-
1051 get_texpr_info(AbstrEvents,Info),memberchk(modifies(Modifies),Info).
1052
1053 add_equality_check(Actions,AbstractActions,NewVars,Variables,Unmodifiables) :-
1054 get_modified_vars_of_actions(Actions,Modified),
1055 get_modified_vars_of_actions(AbstractActions,AbstractModified),
1056 unmodifiables(Modified,AbstractModified,NewVars,Variables,Unmodifiables).
1057 unmodifiables([],_AbstractModified,_NewVars,_Variables,[]).
1058 unmodifiables([UM|Modified],AbstractModified,NewVars,Variables,Unmodifiables) :-
1059 ? ( is_modifiable(UM,AbstractModified,NewVars) ->
1060 Unmodifiables = UMrest
1061 ;
1062 get_texpr_id(TUM,UM),
1063 ? member(TUM,Variables),!,
1064 Unmodifiables = [TUM|UMrest]),
1065 unmodifiables(Modified,AbstractModified,NewVars,Variables,UMrest).
1066 % the abstract event modifies it, so we can do it, too
1067 ?is_modifiable(UM,AbstractModified,_NewVars) :- member(UM,AbstractModified),!.
1068 % the variables is newly introduced, so we can modifiy it
1069 is_modifiable(UM,_AbstractModified,NewVars) :-
1070 ? get_texpr_id(TUM,UM), member(TUM,NewVars).
1071
1072 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1073 % normalising merged events means that if two refined events A and B
1074 % change a different set of variables then the event A gets an additional
1075 % assignment of the form x:=x with x as a variable that is changed in B
1076 % but not in A.
1077 % This can happen even though merged events have the same assignments because
1078 % they again can refine events that have different assignments.
1079
1080 % None or one refined event do not have to be normalised
1081 normalise_merged_events([],[]) :- !.
1082 normalise_merged_events([E],[E]) :- !.
1083 normalise_merged_events(Events,Normalised) :-
1084 append_modified_vars_of_events(Events,AllModifiedVars),
1085 find_typed_version_in_events(AllModifiedVars,Events,TypedVars),
1086 normalise_merged_events2(Events,AllModifiedVars,TypedVars,Normalised).
1087 normalise_merged_events2([],_AllModifiedVars,_TypedVars,[]).
1088 normalise_merged_events2([Event|Erest],AllModifiedVars,TypedVars,[Normalised|Nrest]) :-
1089 normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised),
1090 normalise_merged_events2(Erest,AllModifiedVars,TypedVars,Nrest).
1091 normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised) :-
1092 get_modified_vars_of_event(Event,Modified),
1093 remove_all(AllModifiedVars,Modified,MissingVars),
1094 add_missing_assignments(MissingVars,Event,AllModifiedVars,TypedVars,Normalised).
1095 add_missing_assignments([],Event,_,_,Event) :- !.
1096 add_missing_assignments(MissingVars,TEvent,AllModifiedVars,TypedVars,Normalised) :-
1097 get_texpr_expr(TEvent,Event),
1098 get_texpr_type(TEvent,Type),
1099 get_texpr_info(TEvent,Infos),
1100 selectchk(modifies(_),Infos,RestInfos), % TO DO: also add reads Information
1101 create_texpr(NewEvent,Type,[modifies(AllModifiedVars)|RestInfos],Normalised),
1102 Event = rlevent(Name,Sec,St,Prm,Grd,Thm,Actions,VWit,PWit,Unmod,AbsEvents),
1103 NewEvent = rlevent(Name,Sec,St,Prm,Grd,Thm,NewActions,VWit,PWit,Unmod,AbsEvents),
1104 append(Actions,NewAssignments,NewActions),
1105 create_missing_assignments(MissingVars,TypedVars,NewAssignments).
1106 create_missing_assignments([],_TypedVars,[]).
1107 create_missing_assignments([MissingVar|Mrest],TypedVars,[Assign|Arest]) :-
1108 create_missing_assignment(MissingVar,TypedVars,Assign),
1109 create_missing_assignments(Mrest,TypedVars,Arest).
1110 create_missing_assignment(Var,TypedVars,Assignment) :-
1111 get_texpr_id(TId,Var),
1112 memberchk(TId,TypedVars),
1113 prime_id(Var,Primed),
1114 create_texpr(assign([TId],[TId]),subst,[assigned_after(Primed),modifies(Var)],Assignment).
1115
1116 find_typed_version_in_events([],_Events,[]).
1117 find_typed_version_in_events([Name|Nrest],Events,[Typed|Trest]) :-
1118 find_typed_version_in_events2(Name,Events,Typed),
1119 find_typed_version_in_events(Nrest,Events,Trest).
1120 find_typed_version_in_events2(Name,Events,Typed) :-
1121 get_texpr_id(Typed,Name),
1122 ? member(Event,Events),
1123 get_texpr_expr(Event,rlevent(_Name,_Sec,_St,_Prm,_Grd,_Thm,Actions,_VWit,_PWit,_Unmod,AbsEvents)),
1124 find_typed_version_in_events3(Name,Actions,AbsEvents,Typed),!.
1125 find_typed_version_in_events3(_Name,Actions,_AbsEvents,Typed) :-
1126 ? member(Action,Actions),
1127 get_lhs_tids(Action,Vars),
1128 member(Typed,Vars),!.
1129 find_typed_version_in_events3(Name,_Actions,AbsEvents,Typed) :-
1130 find_typed_version_in_events2(Name,AbsEvents,Typed).
1131
1132 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1133 % optimisation of guards:
1134 % A guard in a refinement does not need to be evaluated in in an abstract event
1135 % again. This happens quiet frequently, especially if "extends" is used.
1136 % The same applies for assignments: If in a refinement an action is performed,
1137 % we do not have to check if the same action can be performed in a more abstract
1138 % level.
1139 optimise_events(TEvent,NTEvent) :-
1140 empty_avl(Empty),
1141 optimise_events2(Empty,TEvent,NTEvent).
1142 optimise_events2(KnownElements,TEvent,NTEvent) :-
1143 create_texpr(Event,Type,Infos,TEvent),
1144 create_texpr(NewEvent,Type,Infos,NTEvent),
1145 Event = rlevent(Name,Section,Status,Params,OldGuard,OldTheorems,OldActions,
1146 VWitnesses,PWitnesses,Unmodifiables,OldAbstractEvents),
1147 NewEvent = rlevent(Name,Section,Status,Params,NewGuard,NewTheorems,NewActions,
1148 VWitnesses,PWitnesses,Unmodifiables,NewAbstractEvents),
1149 optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,KnownElements1),
1150 optimise_formulas(OldActions,KnownElements1,NewActions,NewKnownElements),
1151 maplist(optimise_events2(NewKnownElements),OldAbstractEvents,NewAbstractEvents).
1152 optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,NewKnownElements) :-
1153 conjunction_to_list(OldGuard,OldGuards),
1154 optimise_formulas(OldGuards,KnownElements,NewGuards,KnownElements1),
1155 % If no elements were removed, we just use the old guard
1156 (OldGuards=NewGuards -> OldGuard=NewGuard ; conjunct_predicates(NewGuards,NewGuard)),
1157 optimise_formulas(OldTheorems,KnownElements1,NewTheorems,NewKnownElements).
1158 % optimise_formulas(+AllFormulas,+KnownElements,-NewFormulas,-NewNormed)
1159 % AllFormulas: A list of formulas
1160 % KnownElementes: A list of normed versions of already encountered elements
1161 % NewFormulas: A sub-list of AllFormulas which are new (not in KnownElements)
1162 % NewKnownElements: The updated list of already encountered elements
1163 % If no formulas are removed, it is guaranteed that NewFormulas=AllFormulas
1164 optimise_formulas(AllFormulas,KnownElements,NewFormulas,NewKnownElements) :-
1165 % convert formulas to a list: Formula/Normed where Normed is a normalised form
1166 maplist(add_stripped_ast,AllFormulas,AllFormNormed),
1167 % remove the already known formulas
1168 exclude(is_duplicate_formula(KnownElements),AllFormNormed,NewFormNormed),
1169 % split the list [Form/Normed] into [Form] and [Normed]
1170 maplist(unzipslash,NewFormNormed,NewFormulas1,NewNormed),
1171 ( AllFormNormed = NewFormNormed -> % No formulas removed, keep everything as it is
1172 NewFormulas = AllFormulas
1173 ;
1174 NewFormulas = NewFormulas1
1175 ),
1176 foldl(add_to_known_elements,NewNormed,KnownElements,NewKnownElements).
1177 add_stripped_ast(Formula,Formula/Stripped) :-
1178 strip_and_norm_ast(Formula,Stripped).
1179 is_duplicate_formula(KnownElements,_Formula/Stripped) :-
1180 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 !
1181 unzipslash(A/B,A,B).
1182 add_to_known_elements(New,In,Out) :-
1183 avl_store(New,In,true,Out).
1184
1185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1186 % internal event handling (just data structure)
1187 internal_event(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name).
1188 internal_event_status(tc_event(Name,_Section,Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Status).
1189 internal_event_params(tc_event(Name,_Section,_Status,Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Params).
1190 %internal_event_guards(tc_event(Name,_Section,_Status,_Params,Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Grd).
1191 internal_event_actions(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,Act,_VWit,_PWit,_Unmod,_Ref,_),Name,Act).
1192 internal_event_refined(tc_event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,Ref,_),Name,Ref).
1193 internal_event_description(tc_event(_,_,_,_,_,_,_,_,_,_,_,DescList),Desc) :- member(Desc,DescList).
1194
1195 internal_context(context(Name,_Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name).
1196 internal_context_extends(context(Name,Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Extends).
1197 internal_context_sets(context(Name,_Extends,Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Sets).
1198 internal_context_constants(context(Name,_Extends,_Sets,Constants,_AbstractConstants,_Axioms,_Theorems),Name,Constants).
1199 internal_context_abstract_constants(context(Name,_Extends,_Sets,_Constants,AbstractConstants,_Axioms,_Theorems),Name,AbstractConstants).
1200
1201 internal_model(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name).
1202 internal_model_refines(model(Name,Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Refines).
1203 internal_model_sees(model(Name,_Refines,Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Sees).
1204 internal_model_vars(model(Name,_Refines,_Sees,Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Variables).
1205 internal_model_newvars(model(Name,_Refines,_Sees,_Variables,NewVariables,_Invariants,_Theorems,_Events),Name,NewVariables).
1206 internal_model_invs(model(Name,_Refines,_Sees,_Variables,_NewVariables,Invariants,_Theorems,_Events),Name,Invariants).
1207 internal_model_thms(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,Theorems,_Events),Name,Theorems).
1208 internal_model_events(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,Events),Name,Events).
1209
1210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1211 % analyse deferred sets and generate enumerated sets if possible
1212
1213
1214
1215
1216 %% :- include(bmachine_eventb_common).
1217 %% code below used to be in separate file, as there was the single-level and multi-level mode:
1218
1219
1220
1221 extract_name(event_b_model(_,Name,_Sections),Res) :- !, Res=Name.
1222 extract_name(event_b_context(_,Name,_Sections),Res) :- !, Res=Name.
1223 extract_name(MODEL,_) :- add_error(extract_name,'Could not extract model name: ',MODEL),fail.
1224
1225 extract_sections(event_b_model(_,_Name,Sections),Sections).
1226 extract_sections(event_b_context(_,_Name,Sections),Sections).
1227
1228 % topological sort
1229
1230 topological_sort(List,Sorted) :-
1231 get_dependencies(List,Dependencies),
1232 topolsort(Dependencies,[],SortedNames),
1233 get_sorted(SortedNames,List,Sorted),!.
1234 topological_sort(List,Sorted) :- add_failed_call_error(topological_sort(List,Sorted)),fail.
1235
1236 get_dependencies([],[]).
1237 get_dependencies([E|Rest],[dep(Name,Deps)|Drest]) :-
1238 extract_name(E,Name),
1239 findall(D,dependency(E,D),Deps1),
1240 sort(Deps1,Deps),
1241 get_dependencies(Rest,Drest).
1242
1243 dependency(Elem,Dependend) :-
1244 extract_sections(Elem,Sections),
1245 ( rawmachine_section(extends,Sections,Extends),
1246 ? member(Dependend,Extends)
1247 ; rawmachine_section(refines,Sections,Dependend)).
1248
1249 topolsort([],_,[]) :- !.
1250 topolsort(Deps,Fulfilled,[First|Rest]) :-
1251 ? select(dep(First,Before),Deps,Drest),
1252 is_sublist(Before,Fulfilled),!,
1253 sort([First|Fulfilled],NewFulfilled),
1254 topolsort(Drest,NewFulfilled,Rest).
1255 is_sublist([],_).
1256 is_sublist([H|T],[F|R]) :-
1257 (H=F -> is_sublist(T,R) ; is_sublist([H|T],R)).
1258
1259 get_sorted([],_,[]).
1260 get_sorted([Name|Nrest],Elems,[First|Srest]) :-
1261 ? member(First,Elems),
1262 extract_name(First,Name),!,
1263 get_sorted(Nrest,Elems,Srest).
1264
1265 % copy&paste from bmachine_construction
1266 rawmachine_section(Elem,List,Result) :-
1267 functor(Pattern,Elem,2),
1268 arg(2,Pattern,Result),
1269 ? member(Pattern,List),!.
1270
1271 optional_rawmachine_section(Elem,List,Default,Result) :-
1272 ( rawmachine_section(Elem,List,Result1) -> true
1273 ; Result1=Default),
1274 Result1=Result.
1275
1276 % ----------------------------------------
1277
1278
1279 % older versions of the .eventb files do not have a status included
1280 raw_event(event(Pos,Name,RawRefines,Params,Guards,Actions,Witnesses), % event/7
1281 Pos,Name,ordinary(none),Refines,Params,Guards,[],Actions,Witnesses,[]) :-
1282 (\+((RawRefines==[] ; RawRefines=[_|_]))
1283 -> add_error(b_machine_eventb,'Outdated .eventb format, ignoring refines:',RawRefines),
1284 Refines = []
1285 ; Refines=RawRefines).
1286 raw_event(event(Pos,Name,Status,Refines,Params,Guards,Actions,Witnesses), % event/8
1287 Pos,Name,Status,Refines,Params,Guards,[],Actions,Witnesses,[]).
1288 raw_event(event(Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses), % event/9
1289 Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,[]).
1290 raw_event(description_event(_,Desc,Event),
1291 Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,[Desc|TD]) :-
1292 raw_event(Event, Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses,TD),
1293 debug_format(19,'New style event ~w with description "~w"~n',[Name,Desc]).
1294
1295 % code common to bmachine_eventb.pl and bmachine_eventb_ml.pl
1296
1297 :- use_module(bmachine_structure,[select_section/5]).
1298 append_to_section(Section,List,Old,New) :-
1299 % todo: access to private elements of bmachine_construction
1300 select_section(Section,OldList,NewList,Old,New),
1301 append(OldList,List,NewList).
1302 conjunct_to_section(Section,Preds,Old,New) :-
1303 % todo: access to private elements of bmachine_construction
1304 select_section(Section,OldPred,NewPred,Old,New),
1305 conjunct_predicates([OldPred|Preds],NewPred).
1306
1307 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1308 % analyse Event-B deferred sets and generate enumerated sets if possible
1309
1310 enumerated_deferred_sets(Sets,Constants,Axioms,NewSets,NewConstants,NewAxioms,TSet,TElements) :-
1311 conjunct_predicates(Axioms,Axiom),
1312 conjunction_to_list(Axiom,Axiom2),
1313 enumerated_deferred_sets2(Sets,Constants,Axiom2,NewSets,NewConstants,NewAxioms,TSet,TElements).
1314
1315 enumerated_deferred_sets2([],Csts,Axioms,[],Csts,Axioms,[],[]).
1316 enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,NewSets,NewCsts,NewAxioms,[TSet|TSetRest],TElementsAll) :-
1317 % case 1: the set is an enumerated set
1318 ? enumerated_deferred_set(Set,Csts,Axioms,ICsts,IAxioms,TSet,TElements),!,
1319 append(TElements,TElementsRest,TElementsAll),
1320 enumerated_deferred_sets2(SetRest,ICsts,IAxioms,NewSets,NewCsts,NewAxioms,TSetRest,TElementsRest).
1321 enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,[Set|NewSets],NewCsts,NewAxioms,TSets,TElements) :-
1322 % case 2: the set is a normal deferred set
1323 enumerated_deferred_sets2(SetRest,Csts,Axioms,NewSets,NewCsts,NewAxioms,TSets,TElements).
1324
1325 enumerated_deferred_set(Set,Constants,Axioms,NewConstants,NewAxioms,Set,TElements) :-
1326 %% print(checking_for_enumerated_deferred_sets(Axioms)),nl,
1327 has_enumeration_axioms(Set,Elements,Axioms,NewAxioms),
1328 %% print(found_enumerated_set(Set)),nl, %%
1329 % remove Elem1,...,ElemN from the constants
1330 ? remove_constants(Elements,Constants,NewConstants),
1331 % add enumerated set information to the elements
1332 get_texpr_type(Set,SType),
1333 (SType=set(global(Type)) -> true
1334 ; add_error_and_fail(enumerated_deferred_set,'Unexpected Set: ',(Set:SType))),
1335 (typeset_enumerated(Elements,Type,TElements) -> true
1336 ; add_error_and_fail(enumerated_deferred_set,'Could not typeset: ',(Type,Elements))).
1337
1338
1339 has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :-
1340 ? has_partition_axioms(Set,Elements,AxiomsIn,AxiomsOut),!.
1341 has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :-
1342 % there in an axiom Set = {Elem1,...,ElemN}
1343 select_equal_extension_set_of_ids(Set,AxiomsIn,Axioms1,ExtSet,Elements),
1344 % check if all axioms needed for an enumeration are
1345 % present, and remove them
1346 % second case: All elements of the set are mutually unequal
1347
1348 % generate the unequalities we have to check for
1349 generate_unequals(Elements,Unequals),
1350 % check if they are all in the axioms, and remove them from the axioms
1351 (all_unequals_present(Unequals,Axioms1,AxiomsOut) -> true
1352 ; assertz(deferred_set_eq_wo_enumeration_axioms(Set,ExtSet)),
1353 write('Deferred set with equality but *not* recognized as enumerated set: '),
1354 translate:print_bexpr(Set), write(' = '), translate:print_bexpr(ExtSet),nl,
1355 fail
1356 ).
1357
1358 has_partition_axioms(Set,PartitionElements,AxiomsIn,AxiomsOut) :-
1359 % print(checking_for_enumeration_axioms(Set)),nl,
1360 % first case: A partion predicate is present with
1361 % all elements of the set as its arguments
1362 % ( e.g. partition(S,{a},{b},...) )
1363
1364 % create a pattern for the partition:
1365 get_texpr_id(Set,SetId),get_texpr_id(SetRef,SetId),
1366 create_texpr(partition(SetRef,Singletons),pred,_,Partition),
1367 % remove the partition from the axioms
1368 % print(looking_for_partition(SetId,Partition)),nl,nl,
1369 ? select(Partition,AxiomsIn,AxiomsOut1),
1370 %%print(found_partition(SetID,Partition)),nl,
1371 % check if all arguments are singletons and get the
1372 % singleton elements
1373 all_singletons(Singletons,PartitionElements,AxiomsOut1,AxiomsOut2,Recursive),
1374 (Recursive==true
1375 -> AxiomsOut=AxiomsIn /* then we still need the partition axioms */
1376 ; AxiomsOut=AxiomsOut2).
1377 %% ,print(all_singletons(Singletons)),nl.
1378 %% print(singletons(PartitionElements)),nl,
1379 % check if all arguments and the identifiers
1380 % of the set are the same
1381 % same_elements(Elements,PartitionElements).
1382
1383
1384 % all elements of a list are singletons, the second argument
1385 % returns the list of elements without the set around it
1386 all_singletons([],[],Ax,Ax,_).
1387 all_singletons([Set|SRest],[Expr|ERest],AxiomsIn,AxiomsOut,Recursive) :-
1388 get_texpr_expr(Set,set_extension([Expr])),!,
1389 all_singletons(SRest,ERest,AxiomsIn,AxiomsOut,Recursive).
1390 all_singletons([ID1|SRest],Result,AxiomsIn,AxiomsOut,Recursive) :-
1391 ID1 = b(identifier(_ID),set(global(_)),_Info),
1392 Recursive=true,
1393 % print(trying_to_look_for_recursive_partition(_ID)),nl, %%
1394 has_enumeration_axioms(ID1,PartitionElements,AxiomsIn,AxiomsOut1),
1395 % print(recursive_partition(ID,PartitionElements)),nl,
1396 append(PartitionElements,ERest,Result),
1397 all_singletons(SRest,ERest,AxiomsOut1,AxiomsOut,_).
1398
1399 % the two lists of typed identifiers have the same identifiers
1400 %same_elements(ElemsA,ElemsB) :-
1401 % get_texpr_ids(ElemsA,IdsA),sort(IdsA,A),
1402 % get_texpr_ids(ElemsB,IdsB),sort(IdsB,B),
1403 % A=B.
1404
1405 typeset_enumerated([],_Type,[]).
1406 typeset_enumerated([Elem|Erest],Type,[TElem|Trest]) :-
1407 create_texpr(identifier(Id),global(Type),Infos,Elem),
1408 create_texpr(identifier(Id),global(Type),[enumerated_set_element|Infos],TElem),
1409 typeset_enumerated(Erest,Type,Trest).
1410
1411 remove_constants([],Cst,Cst).
1412 remove_constants([TId|Erest],In,Out) :-
1413 get_texpr_id(TId,Id),
1414 get_texpr_id(Pattern,Id),
1415 ? select(Pattern,In,Env),
1416 ? remove_constants(Erest,Env,Out).
1417
1418 % find an equality Set = {id1,...,idk}
1419 select_equal_extension_set_of_ids(Set,In,Out,Ext,Elements) :-
1420 get_texpr_id(Set,SetId),
1421 get_texpr_id(Expr,SetId),
1422 create_texpr(set_extension(Elements),_,_,Ext),
1423 create_texpr(Equal,_,_,TEqual),
1424 ( Equal = equal(Expr,Ext); Equal = equal(Ext,Expr) ),
1425 ? select(TEqual,In,Out),!.
1426
1427 generate_unequals(Elements,Unequals) :-
1428 get_texpr_ids(Elements,Ids),
1429 findall(unequal(A,B),two_ids(Ids,A,B),Unequals).
1430 ?two_ids([A|Rest],A,B) :- member(B,Rest).
1431 ?two_ids([_|Rest],A,B) :- two_ids(Rest,A,B).
1432
1433 all_unequals_present([],Axioms,Axioms).
1434 all_unequals_present([unequal(A,B)|Rest],InAxioms,OutAxioms) :-
1435 remove_unequalities(InAxioms,A,B,IntAxioms,0,N), N>0,!, % at least one occurrence
1436 all_unequals_present(Rest,IntAxioms,OutAxioms).
1437
1438 remove_unequalities([],_,_,[],N,N).
1439 remove_unequalities([TAxiom|T],A,B,Rest,NrRemoved,R) :-
1440 get_texpr_id(AExpr,A), get_texpr_id(BExpr,B),
1441 get_texpr_expr(TAxiom,Axiom),
1442 is_unequality(Axiom,AExpr,BExpr),!, N1 is NrRemoved+1,
1443 remove_unequalities(T,A,B,Rest,N1,R).
1444 remove_unequalities([Axiom|T],A,B,[Axiom|TR],N,R) :- % not an unequality between A and B
1445 remove_unequalities(T,A,B,TR,N,R).
1446
1447 is_unequality(not_equal(A,B),A,B) :- !.
1448 is_unequality(not_equal(B,A),A,B) :- !.
1449 is_unequality(negation(TEqual),A,B) :-
1450 get_texpr_expr(TEqual,Equal),
1451 is_direct_equality(Equal,A,B).
1452 is_direct_equality(equal(A,B),A,B) :- !.
1453 is_direct_equality(equal(B,A),A,B) :- !.
1454
1455 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1456 % creating a type environment with information about theories inside
1457
1458 check_theory_extensions(Infos,Freetypes,Ops,TheoryEnv) :-
1459 findall( T, (member(T,Infos),is_eventb_additional_info(T)), Theories),
1460 default_theory_ops(InitialEnv),
1461 foldl(check_theory,Theories,FreetypesL,OpsL,InitialEnv,TheoryEnv),
1462 append(FreetypesL,Freetypes),
1463 append(OpsL,Ops).
1464 is_eventb_additional_info(Term) :-
1465 nonvar(Term),functor(Term,theory,Arity),
1466 memberchk(Arity,[3,4,5,7]).
1467 default_theory_ops(Env) :-
1468 env_empty(Empty),
1469 cond_operator(Id,Op),
1470 env_store_operator(Id,Op,Empty,Env).
1471 cond_operator('COND',bmachine_eventb:axiomatic_definition('COND',Params,DirectDef,[PT])) :-
1472 PT = '__IFTHENELSETYPE',
1473 TypeExpr = identifier(none,PT),
1474 Params = [argument('THEN',TypeExpr),
1475 argument('ELSE',TypeExpr),
1476 argument('IF',set_extension(none,[truth(none)]))],
1477 DirectDef = if_then_else(none,identifier(none,'IF'),
1478 identifier(none,'THEN'),identifier(none,'ELSE')).
1479 check_theory(Theory,Freetypes,Ops,Env,OutEnv) :-
1480 get_theory_name(Theory,Proj,Name),
1481 debug_format(19,'Checking theory ~w:~w~n',[Proj,Name]),
1482 (check_theory2(Theory,Env,_DefSets,Freetypes,Ops) -> true
1483 ; add_internal_error('Theory check failed:',Theory),fail),
1484 store_operator_list(Ops,Env,OutEnv),
1485 check_theory_axioms(Theory,OutEnv,_).
1486
1487 store_operator_list(Ops,Env,OutEnv) :-
1488 keys_and_values(Ops,Ids,Operators),
1489 foldl(env_store_operator,Ids,Operators,Env,OutEnv).
1490
1491 check_theory2(theory(PT,Datatypes,OP),Env,DefSets,Freetypes,Ops) :-
1492 % just to be backward-compatible to a version without axiomatic definitions
1493 check_theory2(theory(PT,Datatypes,OP,[]),Env,DefSets,Freetypes,Ops).
1494 check_theory2(theory(PT,Datatypes,OP,AxDefs),Env,DefSets,Freetypes,Ops) :-
1495 % just to be backward-compatible to a version without operator mapping
1496 % definitions
1497 check_theory2(theory(PT,Datatypes,OP,AxDefs,[]),Env,DefSets,Freetypes,Ops).
1498 check_theory2(theory(PT,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,Ops) :-
1499 check_theory2(theory(unknown,unknown,PT,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,Ops).
1500 check_theory2(theory(TheoryId,_Imported,TypeParameters,Datatypes,OP,AxDefs,Mappings),Env,DefSets,Freetypes,AllOps) :-
1501 %print_theory_axioms(TheoryId,TypeParameters,AxDefs),
1502 extract_freetypes(TheoryId,Env,Datatypes,Freetypes,FreetypeOps),
1503 (Mappings \= [_|_]
1504 -> generate_default_mappings(AxDefs,TheoryId,ML)
1505 ; debug_format(19,'Mappings in .ptm file: ~w~n',[Mappings]),
1506 ML=Mappings), % some older .eventb files seem to have none here, e.g., Theory/SumProduct_m1_mch.eventb
1507 debug_println(9,operator_mappings(ML)),
1508 findall(VirtualDefSet,unmapped_axiomatic_def_set(VirtualDefSet,AxDefs,ML),DefSets),
1509 maplist(store_virtual_deferred_set(TheoryId,TypeParameters),DefSets,DefSetOps),
1510 foldl(handle_mappings(TheoryId,TypeParameters),ML,MappedOpsL,OP/AxDefs,OP1/AxDefs1),
1511 append(MappedOpsL,MappedOps),
1512 maplist(store_operator(TheoryId,TypeParameters),OP1,DefinedOps),
1513 maplist(store_axiomatic_operator(TheoryId,TypeParameters),AxDefs1,AxOpsL),
1514 append(AxOpsL,AxOps),
1515 append([DefSetOps,FreetypeOps,MappedOps,DefinedOps,AxOps],AllOps1),
1516 % The operators are used for call-backs, a module prefix is mandatory
1517 maplist(prefix_with_module,AllOps1,AllOps).
1518
1519 unmapped_axiomatic_def_set(VirtualDefSet,AxDefs,ML) :-
1520 member(axiomatic_def_block(_AxDefId,AxTypes,_,_),AxDefs),
1521 member(VirtualDefSet,AxTypes), nonmember(tag(VirtualDefSet,_),ML).
1522
1523 % axiomatic blocks can contain new types; these seem to be just deferred sets (cf R0-MovingTrains_mch.eventb)
1524 store_virtual_deferred_set(TheoryId,TypeParameters,DefSet,Res) :- Parameters=[],RawWDCond=truth(none),
1525 ((DefSet='Real' ; DefSet='REAL') % in case no .ptm file exists, e.g., for Abrial's Real theory
1526 -> DirectDef=real_set(none),
1527 add_message(bmachine_eventb,'Translating axiomatic type to REAL: ',DefSet)
1528 ; DirectDef=string_set(none),
1529 add_message(bmachine_eventb,'Translating axiomatic type to STRING: ',DefSet)
1530 ), % TODO: translate to propert def. set!
1531 store_operator(TheoryId,TypeParameters,operator(DefSet,Parameters,RawWDCond,[DirectDef],[]),Res).
1532
1533 prefix_with_module(Id-Op,Id-(bmachine_eventb:Op)).
1534
1535 :- public print_theory_axioms/3.
1536 print_theory_axioms(TheoryId,TypeParameters,AxDefs) :- member(axiomatic_def_block(Id,Types,_OpDefsIn,Axioms),AxDefs),
1537 format('~nAxDef Block ~w (~w) in theory ~w (~w)~n',[Id,Types,TheoryId,TypeParameters]),
1538 translate:l_print_raw_bexpr(Axioms),
1539 fail.
1540 print_theory_axioms(_,_,_).
1541
1542
1543 check_theory_axioms(theory(TheoryId,_Imported,TypeParameters,_Datatypes,_OP,AxDefs,_Mappings),Env,TheoryAxioms) :-
1544 fail, % disabled; for tests 2295, 2379, 2382 there are unsupported axiomatic operators in the axioms
1545 maplist(create_deferred_set,TypeParameters,RawIds),
1546 create_sets(RawIds,TheoryId,Sets),
1547 add_unique_variables(Sets,Env,Env2),
1548 member(axiomatic_def_block(AxDefId,_Types,_OpDefsIn,RawAxioms),AxDefs),
1549 get_theory_name(TheoryId,Proj,Name), format('Typechecking block ~w in ~w:~w~n',[AxDefId,Proj,Name]),
1550 typecheck_l(RawAxioms,Env2,pred,TheoryAxioms,theory_axioms),
1551 translate:l_print_bexpr_or_subst(TheoryAxioms),nl,
1552 fail.
1553 check_theory_axioms(_,_Env,[]).
1554
1555 create_deferred_set(Atom,deferred_set(unknown,Atom)).
1556
1557 get_theory_name(theory_name(Project,TheoryName),ResP,ResN) :- !,
1558 ResP=Project, ResN=TheoryName.
1559 get_theory_name(Theory,ResP,ResN) :-
1560 functor(Theory,theory,_), arg(1,Theory,TN),!,
1561 get_theory_name(TN,ResP,ResN).
1562 get_theory_name(N,'','') :- format('Could not extract theory name: ~w~n',[N]).
1563
1564 store_operator(TheoryId,TypeParameters,operator(Id,Parameters,RawWDCond,DirectDef,RecursiveDef),Id-Op) :-
1565 store_operator2(TheoryId,TypeParameters,Id,DirectDef,RecursiveDef,Parameters,RawWDCond,TypeParameters,Op).
1566
1567 store_operator2(_,_,_,_,RecursiveDef,Parameters,_WD,TypeParameters,Op) :-
1568 RecursiveDef=[_|_],!,
1569 Op=recursive_operator(Parameters,RecursiveDef,TypeParameters).
1570 store_operator2(TheoryId,_,Id,[Def],_,Parameters,Raw_WDCond,TypeParameters,Op) :- !,
1571 %format('Storing direct definition operator ~w with WD: ~w~n',[Id,Raw_WDCond]),
1572 store_operator_definition(TheoryId,Id,Parameters,Def,Raw_WDCond,TypeParameters,direct_definition), % store for bvisual2
1573 Op=direct_definition(Parameters,Raw_WDCond,Def,TypeParameters).
1574 store_operator2(TheoryId,TypeParas,_Id,_,Parameters,_,_WD,_,Op) :-
1575 get_theory_name(TheoryId,Project,Theory),
1576 Op = unsupported_operator(Project,Theory,TypeParas,Parameters,
1577 'Only operators with direct or recursive definition are currently supported').
1578
1579 :- dynamic stored_operator_direct_definition/8.
1580 % store definition for bvisual2, ...; not used in typechecker or interpreter
1581 store_operator_definition(TheoryId,Id,Parameters,Def,Raw_WDCond,TypeParameters,Kind) :-
1582 get_theory_name(TheoryId,Proj,Theory),
1583 assertz(stored_operator_direct_definition(Id,Proj,Theory,Parameters,Def,Raw_WDCond,TypeParameters,Kind)).
1584
1585 reset_stored_defs :- retractall(stored_operator_direct_definition(_,_,_,_,_,_,_,_)),
1586 retractall(some_operator_uses_reals).
1587
1588 stored_operator(Id,Kind) :-
1589 stored_operator_direct_definition(Id,_,_,_,_,_,_,Kind).
1590
1591 :- dynamic some_operator_uses_reals/0.
1592 check_if_operator_expr_uses_reals(Raw) :-
1593 \+some_operator_uses_reals,
1594 raw_term_uses_reals(Raw),
1595 !,
1596 assert(some_operator_uses_reals). % this may be important for type checking later
1597 check_if_operator_expr_uses_reals(_).
1598
1599 raw_term_uses_reals(real_set(_)).
1600 raw_term_uses_reals(float_set(_)).
1601 raw_term_uses_reals(real(_,_)).
1602 raw_term_uses_reals(external_pred_call_auto(_,ExtFun,_)) :- ext_fun_uses_reals(ExtFun).
1603 raw_term_uses_reals(external_function_call_auto(_,ExtFun,_)) :- ext_fun_uses_reals(ExtFun).
1604 % TODO: detect more and detect nested usage
1605 :- use_module(external_functions, [external_fun_type/3]).
1606 ?ext_fun_uses_reals(ExtFun) :- external_fun_type(ExtFun,_,Types), member(R,Types),R==real.
1607
1608 :- use_module(eventhandling,[register_event_listener/3]).
1609 :- register_event_listener(clear_specification,reset_stored_defs,
1610 'Reset stored Event-B operators.').
1611
1612 % extract inductive data types as freetypes
1613 extract_freetypes(TheoryId,ParamEnv,DataTypes,Freetypes,FreetypeOps) :-
1614 maplist(extract_freetype(TheoryId,DataTypes,ParamEnv),DataTypes,Freetypes,FreetypeOpsL),
1615 append(FreetypeOpsL,FreetypeOps).
1616 extract_freetype(TheoryId,AllDataTypes,Env,
1617 datatype(Id,TypeParams,Constructors),
1618 freetype(FreetypeId,Cases),
1619 [Id-freetype_operator(FreetypeId,Types,TypeParams,Usage)|CaseOps]) :-
1620 debug_format(19,'Converting data type ~w with type parameters ~w to freetype~n',[Id,TypeParams]),
1621 foldl(add_datatype_to_env,AllDataTypes,Env,Env1),
1622 foldl(add_type_parameter,TypeParams,Types,Env1,ParamEnv),
1623 create_freetype_typeid(Id,Types,FreetypeId),
1624 Type = freetype(FreetypeId),
1625 extract_used_type_parameters(Constructors,TypeParams,Usage),
1626 %store_eventb_operator(Id,freetype_operator_as_identifier(Id),ParamEnv,ParamEnv2), % now done in add_datatype_to_env
1627 WD=truth(none),
1628 maplist(get_raw_id,TypeParams,TypeParaIds),
1629 store_operator_definition(TheoryId,Id,TypeParaIds,identifier(none,'Datatype'),WD,TypeParaIds,datatype_definition), % store for bvisual2
1630 maplist(extract_case(TheoryId,ParamEnv,Type,Types),Constructors,Cases,CaseOpsL),
1631 append(CaseOpsL,CaseOps).
1632 get_raw_id(identifier(_,ID),R) :- !, R=ID.
1633 get_raw_id(I,I).
1634
1635 add_datatype_to_env(datatype(Id,Params,_ConstructorList),In,Out) :-
1636 length(Params,NumberOfParams),
1637 functor(FreetypeId,Id,NumberOfParams),
1638 debug_format(19,'Generating freetype ~w/~w for inductive datatype from Rodin theory~n',[Id,NumberOfParams]),
1639 env_store(Id,set(freetype(FreetypeId)),[],In,In2),
1640 store_eventb_operator(Id,freetype_operator_as_identifier(Id),In2,Out).
1641
1642 add_type_parameter(TypeParam,Type,In,Out) :-
1643 extract_id(TypeParam,ParameterId),
1644 debug_format(19,'Generating paramater type ~w for Rodin theory~n',[ParameterId]),
1645 env_store(ParameterId,set(Type),[],In,Out).
1646 extract_id(identifier(_,Id),Id).
1647 % constructor without parameters
1648 extract_case(_TheoryId,_ParamEnv,freetype(TypeId),_Types, constructor(Id,[]),
1649 case(Id,constant([Id])),Ops) :- !,
1650 Ops=[Id-constructor_operator(TypeId,[])].
1651 % constructor with parameters
1652 extract_case(TheoryId,ParamEnv,Freetype,ParamTypes,constructor(Id,Destructors),
1653 case(Id,Type),
1654 [Id-constructor_operator(FreetypeId,Types)|DestructOps]) :-
1655 maplist(extract_destructor(TheoryId,ParamEnv,Freetype,ParamTypes,Id,Type),
1656 Destructors,Projections,TypesAndOps),
1657 maplist(split_type_and_op,TypesAndOps,Types,DestructOps),
1658 Freetype=freetype(FreetypeId),
1659 debug_format(19,'Generated constructor ~w ~w for freetype ~w~n',[Id,Types, FreetypeId]),
1660 combine_typelist_with_prj(Types,Type,Projections).
1661 extract_destructor(TheoryId,Env,freetype(FreetypeId),ParamTypes,Case,CType,
1662 destructor(Name,RawTypeExpr),Projection,Type-Name-Op) :-
1663 typecheck_with_freevars(RawTypeExpr,Env,ParamTypes,set(Type),_,destructor(FreetypeId)),
1664 Op = destructor_operator(Name,FreetypeId,Projection,Case,CType),
1665 debug_format(19,'Generated destructor ~w (type ~w) for case ~w of freetype ~w~n', [Name,Type, Case, FreetypeId]),
1666
1667 WD = truth(none),
1668 functor(FreetypeId,FF,_),
1669 ajoin(['Destructor for ', FF],InfoID),
1670 store_operator_definition(TheoryId,Name,[argument(Case,CType)],identifier(none,InfoID),WD,ParamTypes,
1671 destructor(FreetypeId,Type)).
1672
1673 split_type_and_op(Type-Name-Op,Type,Name-Op).
1674
1675
1676 :- assert_must_succeed(( combine_typelist_with_prj([a,b],T,P),
1677 T == couple(a,b), P == [[prj1],[prj2]] )).
1678 :- assert_must_succeed(( combine_typelist_with_prj([a,b,c],T,P),
1679 T == couple(a,couple(b,c)),
1680 P == [[prj1],[prj2,prj1],[prj2,prj2]] )).
1681 :- assert_must_succeed(( combine_typelist_with_prj([a,b,c,d],T,P),
1682 T == couple(couple(a,b),couple(c,d)),
1683 P == [[prj1,prj1],[prj1,prj2],[prj2,prj1],[prj2,prj2]] )).
1684 combine_typelist_with_prj([T],R,Projections) :- !,R=T,Projections=[[]].
1685 combine_typelist_with_prj(Types,couple(TypeL,TypeR),Projections) :-
1686 split_list_in_middle(Types,TypesLeft,TypesRight),
1687 same_length(TypesLeft,PrjLeft),same_length(TypesRight,PrjRight),
1688 append(PrjLeft,PrjRight,Projections),
1689 maplist(cons(prj1),PrjLeft1,PrjLeft),
1690 maplist(cons(prj2),PrjRight1,PrjRight),
1691 combine_typelist_with_prj(TypesLeft,TypeL,PrjLeft1),
1692 combine_typelist_with_prj(TypesRight,TypeR,PrjRight1).
1693 split_list_in_middle(List,Left,Right) :-
1694 length(List,N),
1695 Half is floor(N / 2),
1696 append_length(Left,Right,List,Half).
1697
1698 combine_exprlist_to_couple([T],R) :- !,T=R.
1699 combine_exprlist_to_couple(Exprs,R) :-
1700 split_list_in_middle(Exprs,ExprsLeft,ExprsRight),
1701 combine_exprlist_to_couple(ExprsLeft,TL),
1702 combine_exprlist_to_couple(ExprsRight,TR),
1703 get_texpr_types([TL,TR],[TypeL,TypeR]),
1704 create_texpr(couple(TL,TR),couple(TypeL,TypeR),[],R).
1705
1706 combine_exprlist_to_cprod([T],R) :- !,T=R.
1707 combine_exprlist_to_cprod(Exprs,R) :-
1708 split_list_in_middle(Exprs,ExprsLeft,ExprsRight),
1709 combine_exprlist_to_cprod(ExprsLeft,TL),
1710 combine_exprlist_to_cprod(ExprsRight,TR),
1711 get_texpr_types([TL,TR],[set(TypeL),set(TypeR)]),
1712 create_texpr(cartesian_product(TL,TR),set(couple(TypeL,TypeR)),[],R).
1713
1714 extract_used_type_parameters(Constructors,TypeParams,Usages) :-
1715 maplist(extract_id,TypeParams,TypeParamIds),
1716 convlist(used_type_parameters_of_constructor(TypeParamIds),Constructors,Usages).
1717 used_type_parameters_of_constructor(TypeParamIds,constructor(Id,Destructors),
1718 used_param_types(Id,UsedParamTypes,DestructorExprs)) :-
1719 maplist(destructor_expr,Destructors,DestructorExprs),
1720 maplist(used_type_parameters_of_destructor(TypeParamIds),
1721 DestructorExprs,UsedParamTypeL),
1722 UsedParamTypeL = [_|_], % store the information only for constructors that actually use
1723 % type parameters
1724 ord_union(UsedParamTypeL,UsedParamTypes).
1725 used_type_parameters_of_destructor(TypeParamIds,TypeExpr,UsedTypes) :-
1726 extract_raw_identifiers(TypeExpr,UsedIds),
1727 findall( N, (nth1(N,TypeParamIds,T),memberchk(T,UsedIds)), UsedTypes1),
1728 sort(UsedTypes1,UsedTypes).
1729 destructor_expr(destructor(_,Expr),Expr).
1730 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1731 % callback predicates for operators
1732
1733 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1734
1735 :- public unsupported_operator/13.
1736 % called by btypechecker:lookup_eventb_operator
1737 unsupported_operator(Project,Theory,_TypeParas,Params,_Msg,OpName,Args,Pos,_Env,ExPr,Result,TRin,TRout) :-
1738 match_args_and_params(Args,Params,NewArgs),
1739 get_typed_default_operator(OpName,NewArgs,ExPr,NewOpName,Result),!,
1740 add_default_operator_warning(OpName,NewOpName,Theory,Project,Pos),
1741 TRin=TRout.
1742 unsupported_operator(_,_,_,_Parameters,Msg,Id,_Args,Pos,_Env,ExPr,Result,TRin,TRout) :-
1743 %format('Unsupported ~w~n args:~w',[Id,_Args]),
1744 store_typecheck_error(Msg,Pos,TRin,TRout),
1745 failure_syntax_element(ExPr,Id,F,Type), % just to make sure that the result
1746 create_texpr(F,Type,[],Result). % is nonvar, to prevent later errors
1747 failure_syntax_element(expr,Id,identifier(Id),_).
1748 failure_syntax_element(pred,_Id,falsity,pred).
1749
1750 % in contrast to the default mappings handled earlier,
1751 % this code as access to the actual arguments and their types
1752 % and is called once for each use of the operator
1753 get_typed_default_operator(Op,[A,B],ExPr,NewOp,Result) :-
1754 get_texpr_type(A,TA), get_texpr_type(B,TB),
1755 (nonvar(TA) ; nonvar(TB)),
1756 binary_typed_operator_to_ast(Op,TA,TB,ExPr,NewOp,NewType),
1757 ResExpr =.. [NewOp,A,B],
1758 create_texpr(ResExpr,NewType,[],Result).
1759
1760
1761 binary_typed_operator_to_ast(Op,T,T,expr,NewOp,T) :- binary_expr_op(Op,T,NewOp).
1762 %binary_typed_operator_to_ast(Op,T,T,pred,NewOp,pred) :- binary_pred_op(Op,T,NewOp).
1763
1764 binary_expr_op(pow,integer,power_of).
1765 binary_expr_op(pow,real,power_of_real).
1766 binary_expr_op(power_of,integer,power_of).
1767 binary_expr_op(power_of,real,power_of_real).
1768 binary_expr_op(div,integer,floored_div).
1769 binary_expr_op(div,real,div_real).
1770
1771 %binary_pred_op('less',real,less_real).
1772
1773
1774 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1775
1776 :- use_module(probsrc(bsyntaxtree),[safe_create_texpr/4, is_truth/1,
1777 add_texpr_infos_if_new/3, conjunct_predicates_with_pos_info/3]).
1778 :- use_module(probsrc(bsyntaxtree_quantifiers),[create_z_let/6]).
1779
1780 % get params and type parameters from operator callback registered in the typechecker environment
1781 % for use by btypechecker:lookup_eventb_operator
1782 % it would be a bit cleaner to store infos separately from callback or get rid of the call back completely
1783 get_operator_arity_from_callback(direct_definition(Params,_WD,_DirectDef,_PT),direct_definition,Arity) :-
1784 length(Params,Arity).
1785 get_operator_arity_from_callback(axiomatic_definition(_TagName,Params,_DirectDef,_PT),axiomatic_definition,Arity) :-
1786 length(Params,Arity).
1787 get_operator_arity_from_callback(recursive_operator(Params,_Cases,_PT),recursive_operator,Arity) :-
1788 length(Params,Arity).
1789 get_operator_arity_from_callback(freetype_operator(_FId1,Types1,_PT,_Usage1),freetype_operator,Arity) :-
1790 length(Types1,Arity).
1791 get_operator_arity_from_callback(freetype_operator_as_identifier(_RecId),freetype_operator_as_identifier,0).
1792 get_operator_arity_from_callback(freetype_operator_as_function(_RecId,_RType),freetype_operator_as_function,1).
1793 get_operator_arity_from_callback(freetype_operator_as_set(_RecId),freetype_operator_as_function,0).
1794 get_operator_arity_from_callback(constructor_operator(_FId,_TP),constructor_operator,0).
1795 get_operator_arity_from_callback(destructor_operator(_Name,_FId,_Projections,_Case,_CType1),destructor_operator,1).
1796 get_operator_arity_from_callback(make_inductive_natural(_ArgId,_ZeroOp,_SuccOp),make_inductive_natural,1).
1797 get_operator_arity_from_callback(unsupported_operator(_Project,_Theory,_TP,Paras,_Msg),unsupported_operator,Len) :-
1798 length(Paras,Len).
1799
1800 %%%%%%%%%%%%%%%%%%
1801
1802 % Theory plug-in: direct definitions
1803 :- public direct_definition/12.
1804 % called by btypechecker:lookup_eventb_operator
1805 direct_definition(Params, % e.g. [argument(a,bool_set(none))]
1806 RawWD, % Raw AST of WD condition (currently only implicit WDs from body; not yet user-defined ones)
1807 DirectDef, % Raw AST of DirectDefinition Body, e.g., convert_bool(none,negation(none,equal(none,identifier(none,a),boolean_true(none))))
1808 PT,
1809 OpId, TArgs, Pos,
1810 Env, % environment of operators
1811 ExPr,Result,TRin,TRout) :-
1812 (Params,DirectDef) = (NewParams,NewDirectDefBody), %gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody),
1813 ? apply_direct_definition(OpId,TArgs,NewParams,
1814 NewDirectDefBody,RawWD,
1815 PT,Env,Pos,TLetIds,TLetValues,
1816 TDef,InferredType,TWDPred,
1817 TRin,TRout),
1818 NewInfos = [nodeid(Pos),was(extended_expr(OpId))],
1819 (is_truth(TWDPred) -> add_texpr_infos_if_new(TDef,NewInfos,LetBody)
1820 ; get_preference(find_abort_values,false) -> LetBody=TDef % currently tests 1201, 2232 would fail
1821 % TODO: should we disable the inclusion of the WD condition for older .eventb files?
1822 ; InferredType=pred
1823 -> ajoin(['Well-definedness error for predicate operator ',OpId],MsgStr),
1824 TMsg = b(string(MsgStr),string,[]),
1825 safe_create_texpr(convert_bool(TWDPred),boolean,[nodeid(Pos)],WDBool), % we require an expression argument
1826 safe_create_texpr(external_pred_call('ASSERT_TRUE',[WDBool,TMsg]),pred,NewInfos,TAssert),
1827 conjunct_predicates_with_pos_info(TAssert,TDef,LetBody)
1828 ; ajoin(['Well-definedness error for expression operator ',OpId],MsgStr),
1829 safe_create_texpr(assertion_expression(TWDPred,MsgStr,TDef),InferredType,NewInfos,LetBody)
1830 ),
1831 %write(op(OpId,InferredType)),nl, translate:print_bexpr(LetBody),nl,
1832 create_z_let(ExPr,TLetIds,TLetValues,LetBody,NewInfos,Result).
1833
1834
1835 :- public axiomatic_definition/12.
1836 % just a "dummy" interface predicate for better pretty-printing of operators in translate_eventb_operator
1837 axiomatic_definition(_TagName, Params, DirectDef, PT,
1838 Id, TArgs, Pos, Env, ExPr,Result,TRin,TRout) :-
1839 ? direct_definition(Params, truth(none), DirectDef, PT, Id, TArgs, Pos, Env, ExPr,Result,TRin,TRout).
1840
1841 % Example: ddef([argument(R,pow_subset(none,identifier(none,T)))],seq(none,identifier(none,R)),[T],seq)
1842
1843 % this code not needed as we now systematically rename in create_z_let
1844 %:- use_module(input_syntax_tree,[raw_replace/3]).
1845 %gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody) :-
1846 % maplist(alpha_rename,Params,NewParams,RenameList), %print(replaces(RenameList)),nl,
1847 % raw_replace(DirectDef,RenameList,NewDirectDefBody).
1848 %:- use_module(gensym,[gensym/2]).
1849 %alpha_rename(argument(OldID,Type),argument(FreshID,Type),replace(OldID,identifier(none,FreshID))) :-
1850 % gensym(OldID,FreshID).
1851
1852 % Args are the arguments of the operator where it is used
1853 % Params are the parameters in the operator definition
1854 apply_direct_definition(OpId,TArgs,Params,DirectDef,RawWD,PT,Env,_Pos,
1855 TLetIds,TLetValues,TDef,Type,TWDPred,TRin,TRout) :-
1856 match_args_and_params(TArgs,Params,NewTArgs),!, %TArgs are the concrete arguments in the operator call
1857 maplist(create_typed_id,PT,ParametricTypes,TPT),
1858 add_identifiers_to_environment(TPT,Env,SubEnv),
1859 % type check the arguments given in the operator usage
1860 get_texpr_types(NewTArgs,ArgTypes),
1861 typecheck_arguments(Params,SubEnv,ArgTypes,TParams,TRin,TR2),
1862 % type check the direct definition of the operator. To do this we need the parameters of the operators
1863 % in the type environment. Their type is determined by the arguments of the operator call.
1864 add_identifiers_to_environment(TParams,SubEnv,DefEnv),
1865 ? btype(apply_direct_definition,DirectDef,DefEnv,Type,TDef,TR2,TR3),
1866 debug_format(9,'Inferred type of direct definition ~w application: ~w~n',[OpId,Type]),
1867 append(TParams,TPT,TLetIds),
1868 maplist(create_typeset,ParametricTypes,TypeValues),
1869 append(NewTArgs,TypeValues,TLetValues),
1870 btype(apply_direct_definition,RawWD,DefEnv,_PredType,TWDPred,TR3,TRout). % now type check WD predicate
1871 apply_direct_definition(OpId,TArgs,Arguments,_DirectDef,_WD,_PT,_Env,Pos,
1872 _TParams,_,_TDef,_,_TWD,TRin,TRout) :-
1873 length(TArgs,Len1),
1874 length(Arguments,Len2),
1875 write(targs(TArgs)),nl,
1876 write(args(Arguments)),nl,
1877 ajoin(['Wrong number of arguments (',Len1,') for call to operator ',OpId,
1878 ', expected ',Len2],Msg),
1879 store_typecheck_error(Msg,Pos,TRin,TRout).
1880
1881
1882 match_args_and_params(TArgs,Params,NewTArgs) :-
1883 same_length(TArgs,Params),!, NewTArgs=TArgs.
1884 match_args_and_params([TArg],Params,NewTArgs) :- % can happen when calling operator in REPL using maplets
1885 nested_couple_to_list(TArg,NewTArgs),
1886 same_length(NewTArgs,Params).
1887
1888 split_arg_and_typedef(argument(Id,TypeExpr),Id,TypeExpr).
1889 map_to_set_type(Type,set(Type)).
1890 typecheck_arguments(Params,Env,ArgTypes,TParams,TRin,TRout) :-
1891 % type check the parameters' type expressions of the operator definition, they should have the same type
1892 % as the arguments (except being a set)
1893 % E.g. an operator "o" has one argument "arg" and type expression "T**BOOL" (with T being a parameter type of the theory),
1894 % then for "o(5|->TRUE)" we have "couple(integer,boolean)" as the argument's type,
1895 % we add "T" to the type environment (with type set(_)),
1896 % then we type check the parameter expression "T**BOOL", expecting the type set(coule(integer,boolean)),
1897 % the type check results in T being of type set(integer).
1898 maplist(split_arg_and_typedef,Params,ParamIds,ParamTypeExprs),
1899 same_length(Params,ArgTypes),
1900 maplist(map_to_set_type,ArgTypes,SetArgTypes),
1901 btype_l(ParamTypeExprs,Env,SetArgTypes,_TParamTypeExprs,TRin,TRout),
1902 maplist(create_typed_id,ParamIds,ArgTypes,TParams).
1903 create_typeset(Type,TExpr) :- create_texpr(typeset,Type,[],TExpr).
1904
1905
1906
1907 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1908 % Theory plug-in: Recursive operators
1909 :- public recursive_operator/11.
1910 % called by btypechecker:lookup_eventb_operator
1911 recursive_operator(Arguments,Cases,PT,
1912 Id,TArgs,_Pos,Env,ExPr,Result,TRin,TRout) :-
1913 % parameter types
1914 maplist(create_typed_id,PT,ParametricTypes,TPT),
1915 add_identifiers_to_environment(TPT,Env,Env1),
1916 maplist(create_typeset,ParametricTypes,LetValues), % needed for the LET
1917 typecheck_arguments(Arguments,Env1,ArgTypes,TParamIds,TRin,TR1),
1918 % TArgs: A,B,Cf
1919 % TArg: A|->B|->C
1920 get_texpr_types(TArgs,ArgTypes),
1921 create_couple(TArgs,TArg),
1922 length(TArgs,NumberOfArgs),OpInfo = [theory_operator(Id,NumberOfArgs)],
1923 unique_id("opresult.",ResultId),create_typed_id(ResultId,Type,TResultId),
1924 % TODO: infer ExPr if variable from extended_formula
1925 ( ExPr=expr -> % Result: Comp(x|->y|->z)
1926 % we need to append a result parameter in the comprehension set
1927 create_texpr(function(TCompSet,TArg),Type,OpInfo,InnerResult),
1928 append(TParamIds,[TResultId],CompSetIds),append(ArgTypes,[Type],CompSetTypes),
1929 % make sure that we do not run into an infinite loop
1930 store_eventb_operator(Id,freetype_operator_as_function(RecId,Type),Env1,Env2)
1931 ; ExPr=pred -> % Result: x|->y|->z : Comp
1932 create_texpr(member(TArg,TCompSet),pred,OpInfo,InnerResult),
1933 CompSetIds = TParamIds,ArgTypes=CompSetTypes,
1934 % make sure that we do not run into an infinite loop
1935 store_eventb_operator(Id,freetype_operator_as_set(RecId),Env1,Env2)
1936 ),
1937 couplise_list(CompSetTypes,CompSetType),
1938 % Comp: {i,r| Cond}
1939 create_recursive_compset(CompSetIds,Cond,set(CompSetType),[],RecId,TCompSet),
1940 % Params: a,b,c
1941 % i = a|->b|->c
1942 add_identifiers_to_environment(TParamIds,Env2,Subenv),
1943 foldl(recursive_operator_case(Subenv,TResultId),Cases,TCases,TR1,TRout),
1944 conjunct_predicates(TCases,Cond),
1945 create_z_let(ExPr,TPT,LetValues,InnerResult,OpInfo,Result).
1946
1947
1948 recursive_operator_case(Env,TResultId,case(ParamId,_,Expression,Formula),Cond,TRin,TRout) :-
1949 % Add free identifiers of case to environment
1950 extract_free_identifiers(Expression,TFreeIdentifiers,Env,Subenv),
1951 % IsCase => CaseCheck
1952 create_texpr(implication(IsCase,TCaseCheck),pred,[],Cond),
1953 % IsCase: ParamId = constructor(x,y,z)
1954 typecheck_parameter(ParamId,Env,TParamId),
1955 recop_create_is_case(Expression,Subenv,IsCase,TParamId,FT,Case,TRin,TR1),
1956 % CaseCheck: #x,y,z | Destruction & Predicate
1957 recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,TCaseCheck,TR1,TRout).
1958 extract_free_identifiers(typeof(_Pos,ExtExpr,_TypeExpr),TIds,In,Out) :-
1959 extract_free_identifiers(ExtExpr,TIds,In,Out).
1960 extract_free_identifiers(extended_expr(_Pos,_Case,Exprs,Preds),TIds,In,Out) :-
1961 append(Exprs,Preds,Ids),
1962 maplist(extract_free_identifier,Ids,TIds),
1963 add_identifiers_to_environment(TIds,In,Out).
1964 extract_free_identifier(identifier(_Pos,Id),TId) :-
1965 create_typed_id(Id,_,TId).
1966 typecheck_parameter(ParamId,Env,TParamId) :-
1967 env_lookup_type(ParamId,Env,ParamType),
1968 create_typed_id(ParamId,ParamType,TParamId).
1969 %env_store_type(Id,Type,In,Out) :-
1970 % % Version without Info field
1971 % env_store(Id,Type,[],In,Out).
1972 recop_create_is_case(typeof(_,Expr,_TypeExpr),Env,IsCase,TParamId,FT,Case,TRin,TRout) :-
1973 recop_create_is_case(Expr,Env,IsCase,TParamId,FT,Case,TRin,TRout).
1974 recop_create_is_case(Expression,Env,IsCase,TParamId,FT,Case,TRin,TRout) :-
1975 Expression = extended_expr(_,Case,_,_),
1976 get_texpr_type(TParamId,freetype(FT)),
1977 btype(recop_create_is_case,Expression,Env,freetype(FT),_TCons,TRin,TRout),
1978 create_texpr(freetype_case(FT,Case,TParamId),pred,[],IsCase).
1979 recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,Cond,TRin,TRout) :-
1980 % Predicate
1981 btype(recop_create_in_case,Formula,Subenv,Type,TFormula,TRin,TRout),
1982 ( Type=pred -> Predicate = TFormula
1983 ;
1984 get_texpr_types([TResultId,TFormula],[TypeA,TypeB]),
1985 unify_types_strict(TypeA,TypeB),
1986 create_texpr(equal(TResultId,TFormula),pred,[],Predicate)),
1987 % Destruction: x->y|->z = destructor(ParamId)
1988 ( TFreeIdentifiers = [] ->
1989 Cond = Predicate
1990 ; TFreeIdentifiers = [_|_] ->
1991 get_texpr_types(TFreeIdentifiers,FTypes),
1992 combine_typelist_with_prj(FTypes,FType,Projections),
1993 unique_id("destructed",DId),create_typed_id(DId,FType,TDId),
1994 create_texpr(freetype_destructor(FT,Case,TParamId),FType,[],Destructor),
1995 maplist(create_inner_let(TDId),Projections,TLetExpressions),
1996 create_z_let(pred,TFreeIdentifiers,TLetExpressions,Predicate,[],InnerLets),
1997 create_z_let(pred,[TDId], [Destructor], InnerLets,[],Cond)
1998 ).
1999
2000 create_inner_let(TOrig,Projections,TExpr) :-
2001 apply_projections(Projections,TOrig,TExpr).
2002
2003 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2004 % Theory plug-in: datatype sets
2005 :- public freetype_operator/12.
2006 % called by btypechecker:lookup_eventb_operator
2007 freetype_operator(FreetypeId1,Types1,TypeParams1,Usage1,
2008 Id,TArgs,_Pos,Env,_ExPr,Result,TR,TR) :-
2009 % make a fresh copy to prevent that several instances of the freetype propagate
2010 % their types to each other (resulting in spurious typing errors)
2011 copy_term(freetype(FreetypeId1,Types1,TypeParams1,Usage1),
2012 freetype(FreetypeId, Types, TypeParams, Usage)),
2013 maplist(map_to_set_type,Types,SetTypes),
2014 get_texpr_types(TArgs,SetTypes),
2015 create_freetype_compset(TArgs,Id,FreetypeId,TypeParams,Usage,Env,Result).
2016 create_freetype_compset(TArgs,SetId,FreetypeId,TypeParams,Usage,Env,Result) :-
2017 find_constructors_with_complex_types(TArgs,Usage,Constructors),
2018 ( Constructors = [] ->
2019 create_texpr(freetype_set(FreetypeId),set(freetype(FreetypeId)),[],Result)
2020 ;
2021 create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result)).
2022 create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result) :-
2023 btypechecker:add_ext_variables(TypeParams,Env,TParams,Subenv,TRin,TRout),
2024 get_texpr_types(TParams,Types),get_texpr_types(TArgs,Types),
2025 Type=freetype(FreetypeId),
2026 create_texpr(identifier(freetype_element),Type,[],TId),
2027 do_prettyprint_freetype(FreetypeId,TArgs,PP),
2028 create_recursive_compset([TId],Let,set(Type),[freetype(PP)],RecId,Result),
2029 store_eventb_operator(SetId,freetype_operator_as_identifier(RecId),Subenv,Subenv2),
2030 foldl(create_cons_check(FreetypeId,Subenv2,TId),Constructors,Checks,TRin,TRout),
2031 conjunct_predicates(Checks,Cond),
2032 create_z_let(pred,TParams,TArgs,Cond,[],Let).
2033 create_cons_check(FreetypeId,Env,TId,cons(Case,Exprs),Check,TRin,TRout) :-
2034 btype_l(Exprs,Env,_Types,TExprs,TRin,TRout),
2035 combine_exprlist_to_cprod(TExprs,Set),
2036 get_texpr_type(Set,set(Type)),
2037 create_texpr(freetype_case(FreetypeId,Case,TId),pred,[],CheckCase),
2038 create_texpr(freetype_destructor(FreetypeId,Case,TId),Type,[],Value),
2039 create_texpr(member(Value,Set),pred,[],Membercheck),
2040 create_texpr(implication(CheckCase,Membercheck),pred,[],Check).
2041 % this is used to pretty-print the resulting comprehension set
2042 do_prettyprint_freetype(Id,Params,R) :-
2043 maplist(translate_bexpression,Params,Strs),
2044 ajoin_with_sep(Strs,',',S),
2045 functor(Id,I,_),
2046 ajoin([I,'(',S,')'],R).
2047
2048 find_constructors_with_complex_types(TArgs,Usage,Constructors) :-
2049 find_complex_type_params(TArgs,ComplexTP),
2050 findall(cons(Id,DestructorExprs),
2051 ( member(used_param_types(Id,UsedParamTypes,DestructorExprs),Usage),
2052 ord_intersect(UsedParamTypes,ComplexTP)),
2053 Constructors).
2054 % returns the indeces of the type arguments that are not only types
2055 find_complex_type_params(TArgs,ComplexTP) :-
2056 findall(N,(nth1(N,TArgs,TArg),\+ is_just_type(TArg)),ComplexTP1),
2057 sort(ComplexTP1,ComplexTP).
2058
2059 :- public freetype_operator_as_identifier/9.
2060 freetype_operator_as_identifier(RecId,Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
2061 get_texpr_types(TArgs,SetTypes),
2062 maplist(map_to_set_type,Types,SetTypes),
2063 create_freetype_typeid(Id,Types,FreetypeId),
2064 create_recursion_ref(RecId,set(freetype(FreetypeId)),Result).
2065
2066 :- public freetype_operator_as_function/10.
2067 freetype_operator_as_function(RecId,RType,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
2068 create_couple(TArgs,TArg), get_texpr_type(TArg,Type),
2069 create_recursion_ref(RecId,set(couple(Type,RType)),TFunction),
2070 create_texpr(function(TFunction,TArg),RType,[],Result).
2071
2072 :- public freetype_operator_as_set/9.
2073 freetype_operator_as_set(RecId,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
2074 create_couple(TArgs,TArg), get_texpr_type(TArg,Type),
2075 create_recursion_ref(RecId,set(Type),TSet),
2076 create_texpr(member(TArg,TSet),pred,[],Result).
2077
2078 create_recursion_ref(RecId,Type,TId) :-
2079 create_texpr(identifier(RecId),Type,[for_recursion],TId).
2080
2081 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2082 % Theory plug-in: datatype constructors
2083 :- public constructor_operator/10. % TO DO: ensure by another mechanism that Spider detects that this is called
2084 % called by btypechecker:lookup_eventb_operator
2085 constructor_operator(FreetypeId1,[],Id,[],_Pos,_Env,_ExPr,Result,TRin,TRout) :-
2086 !, copy_term(FreetypeId1,FreetypeId),
2087 create_texpr(value(freeval(FreetypeId,Id,term(Id))),
2088 freetype(FreetypeId),[],Result),
2089 TRin = TRout.
2090 constructor_operator(FreetypeId1,ParamTypes1,
2091 Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
2092 copy_term(constructor(FreetypeId1,ParamTypes1),constructor(FreetypeId,ParamTypes)),
2093 get_texpr_types(TArgs,ParamTypes),
2094 combine_exprlist_to_couple(TArgs,TArg),
2095 %format('Generated freetype constructor call ~w for Rodin theory datatype ~w~n',[Id,FreetypeId]),
2096 create_texpr(freetype_constructor(FreetypeId,Id,TArg),freetype(FreetypeId),[],Result).
2097
2098 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2099 % Theory plug-in: datatype destructors
2100 :- public destructor_operator/13. % TO DO: ensure by another mechanism that Spider detects that this is called
2101 % called by btypechecker:lookup_eventb_operator
2102 destructor_operator(OpName,FreetypeId1,Projections,Case,CType1,
2103 _Id,[TArg],_Pos,_Env,_ExPr,Result,TR,TR) :-
2104 copy_term(destructor(FreetypeId1,CType1),destructor(FreetypeId,CType)),
2105 get_texpr_type(TArg,freetype(FreetypeId)),
2106 debug_format(19,'Generated freetype destructor ~w call ~w for Rodin theory datatype ~w~n',[OpName,Case,FreetypeId]),
2107 create_texpr(freetype_destructor(FreetypeId,Case,TArg),CType,[],Destructed),
2108 apply_projections(Projections,Destructed,Result0),
2109 add_texpr_infos(Result0,[was(extended_expr(OpName))],Result).
2110
2111 % create an projection expression (or a combination of arbitrary many) to
2112 % access a part of a couple. The input is a list of prj1/prj2 atoms,
2113 % e.g. [prj1,prj1,prj2]: Take the first of the first of the second element.
2114 apply_projections(Projections,Expr,Result) :-
2115 reverse(Projections,Prjs),
2116 apply_projections1(Prjs,Expr,Result).
2117 apply_projections1([],Expr,Expr).
2118 apply_projections1([P|Rest],Expr,Result) :-
2119 get_texpr_type(Inner,couple(A,B)),
2120 apply_projections2(P,A,B,Result,Inner),
2121 apply_projections1(Rest,Expr,Inner).
2122 apply_projections2(prj1,A,_B,Result,Inner) :-
2123 create_texpr(first_of_pair(Inner),A,[],Result).
2124 apply_projections2(prj2,_A,B,Result,Inner) :-
2125 create_texpr(second_of_pair(Inner),B,[],Result).
2126
2127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2128 % Theory plug-in: axiomatic definitions of operators
2129 store_axiomatic_operator(Id,TypeParas,axiomatic_def_block(_Id,_Types,OpDefs,_Axioms),Ops) :-
2130 % in case we do not recognize the operator, we store an error message
2131 % that is shown as soon the operator is used somewhere
2132 get_theory_name(Id,Project,Theory), % extract project and theory name
2133 maplist(store_axdef_error(Project,Theory,TypeParas),OpDefs,Ops).
2134 store_axdef_error(Project,Theory,TypeParas,
2135 opdef(Id,Arguments,_WD),Id-unsupported_operator(Project,Theory,TypeParas,Arguments,Msg)) :-
2136 % The opdef information from the Rodin export is missing the result type
2137 % TODO fix this so that we could still typecheck and delay the error message until the operator is used
2138 length(Arguments,Len), %write(opdef(Id,Arguments)),nl,
2139 ajoin(['Axiomatic defined operator \"',Id,'\" of arity ', Len,' not recognized. Be sure to add a ',
2140 Theory,'.ptm file to your Theory project ',
2141 Project],Msg).
2142
2143 % generate default mappings for axiomatic operators in case no .ptm file is provided and the args match
2144 is_axiomatic_def(Id,Arguments,axiomatic_def_block(_Id,_Types,OpDefs,_Axioms)) :-
2145 ? member(opdef(Id,Arguments,_WD),OpDefs).
2146 is_axiomatic_def(Id,[],axiomatic_def_block(_Id,Types,_OpDefs,_Axioms)) :-
2147 member(Id,Types).
2148
2149 generate_default_mappings(AxDefs,TheoryId,DefMappings) :-
2150 findall(tag(OpName,NewOpName), (member(Block,AxDefs),
2151 is_axiomatic_def(OpName,Args,Block),
2152 default_operator(OpName,NewOpName,TheoryId,Args)), DefMappings).
2153
2154 default_operator(OpName,NewOpName,TheoryId,A) :-
2155 get_theory_name(TheoryId,Project,Theory),
2156 ? get_default_operator(OpName,NewOpName,A,Theory),
2157 add_default_operator_warning(OpName,NewOpName,Theory,Project,unknown).
2158 get_default_operator('\x211D\','REAL',Args,_) :- !,
2159 Args=[]. % Real unicode symbol, in .ptm file the Prolog internal name cannot use unicode
2160 get_default_operator('SUM','SIGMA',[argument(_,ArgT)],_) :- !,
2161 relation_to_integer_type(ArgT). % from StandardLibrary SUMandPRODUCT
2162 get_default_operator('PRODUCT','PI',[argument(_,ArgT)],_) :- !, relation_to_integer_type(ArgT).
2163 get_default_operator(cls,closure1,[argument(_,ArgT)],'closure') :- !,
2164 % from Standard Library theory "closure"; but it uses a direct_definition and this rewriting does not trigger!
2165 binary_relation_type(ArgT).
2166 ?get_default_operator(Name,NewName,[_,_],_) :- binary_external_function(Name,NewName),!.
2167 ?get_default_operator(Name,NewName,[_,_],_) :- binary_external_predicate(Name,NewName),!.
2168 ?get_default_operator(Name,Name,Args,_) :- default_operator_aux(Name,Args).
2169
2170 add_default_operator_warning(OpName,NewOpName,Theory,Project,Pos) :-
2171 ajoin(['operator "',OpName,'" internal {',NewOpName,'}'],Decl),
2172 (get_preference(auto_detect_theory_ops,true)
2173 -> MW = 'message'
2174 ; MW = 'warning set AUTO_DETECT_THEORY_MAPPING to TRUE or'
2175 ),
2176 ajoin(['Automatically translating axiomatic operator ',OpName,
2177 '; to get rid of this ', MW, ' add a ',
2178 Theory,'.ptm file to your project ',
2179 Project, ' with this line: '],Msg),
2180 (get_preference(auto_detect_theory_ops,true)
2181 -> add_message(bmachine_eventb,Msg,Decl,Pos)
2182 ; add_warning(bmachine_eventb,Msg,Decl,Pos)
2183 ).
2184
2185 default_operator_aux(choose,Args) :- !, Args = [argument(_,pow_subset(_,_))].
2186 default_operator_aux(mu,Args) :- !, Args=[argument(_,pow_subset(_,_))].
2187 default_operator_aux(closure,[argument(_,ArgT)]) :- !,
2188 binary_relation_type(ArgT).
2189 default_operator_aux(closure1,[argument(_,ArgT)]) :- !,
2190 binary_relation_type(ArgT).
2191 ?default_operator_aux(OpName,[]) :- constant_operator_raw_term(OpName,_).
2192 ?default_operator_aux(OpName,[A1]) :- unary_operator_raw_term(OpName,A1,_).
2193 default_operator_aux(OpName,[A1,A2]) :-
2194 ? binary_operator_raw_term(OpName,A1,A2,_,_),
2195 \+ binary_expr_op(OpName,_,_). % we have typed default rules; delay decision until typing info is available
2196
2197
2198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2199 % Theory plug-in: Tagged operators that can be replaced by internal constructs
2200 handle_mappings(TheoryId,PT,tag(Opname,Tag),Ops,OPin/AxDefsin,OPout/AxDefsOut) :- !,
2201 ( extract_operator(Opname,Operator,OPin/AxDefsin,OPout/AxDefsOut,Kind) ->
2202 (Tag=[_|_] -> debug_format(19,"Mapping Theory Operator ~s -> ~w~n",[Tag,Opname])
2203 ; debug_format(19,"Mapping Theory Operator ~w -> ~w~n",[Tag,Opname])),
2204 (store_operator_by_tag(Tag,Opname,Operator,TheoryId,PT,Ops,Kind)
2205 -> true
2206 ;
2207 ajoin(['Error mapping theory operator ',Opname,
2208 ' to ProB tag (the *.ptm file maybe incorrect or you need a newer version of ProB):'],Msg),
2209 add_error(bmachine_eventb,Msg,Tag))
2210 ;
2211 ajoin(['ProB theory mapping: operator ',Opname,' not found, mapping to ',Tag,' ignored.'],Msg),
2212 add_warning(bmachine_eventb,Msg),
2213 OPin/AxDefsin=OPout/AxDefsOut,Ops=[]
2214 ).
2215 handle_mappings(_TheoryID,_ParamTypes,Mapping,[],X,X) :-
2216 functor(Mapping,Functor,Arity),
2217 ajoin(['ProB theory mapping: unexpected entry of type ',Functor,'/',Arity,', entry ignored.'],Msg),
2218 add_error(bmachine_eventb,Msg).
2219
2220 extract_operator(Opname,Operator,OPin/AxDefs,OPout/AxDefs,Kind) :-
2221 % a regular non-axiomatic operator (direct definition or recursive definition):
2222 Operator = operator(Opname,_Parameters,_WD,DirectDef,_RecursiveDef),
2223 selectchk(Operator,OPin,OPout),!,
2224 % TODO: we could try and infer/store type of operator from Definition and check against axiomatic one
2225 (DirectDef=[] -> Kind='RECURSIVE-DEF-OVERRIDE' ; Kind = 'DIRECT-DEF-OVERRIDE'),
2226 debug_format(19,'Overriding non-axiomatic operator ~w with new definition from .ptm file~n',[Opname]).
2227 extract_operator(Opname,Operator,OP/AxDefsIn,OP/AxDefsOut,'AXIOMATIC-DEF') :-
2228 Operator = axdef(Opname,Parameters,WD,block(Id,Types,Axioms)), % block/3 does not seem to be used
2229 ? select(axiomatic_def_block(Id,Types,OpDefsIn,Axioms),AxDefsIn,
2230 axiomatic_def_block(Id,Types,OpDefsOut,Axioms),AxDefsOut),
2231 ? select(opdef(Opname,Parameters,WD),OpDefsIn,OpDefsOut),!.
2232 extract_operator(Opname,Operator,OP/AxDefsIn,OP/AxDefsOut,'AXIOMATIC-TYPE') :-
2233 % we treat a type of an axiomatic definition also as a potential operator that can be mapped
2234 Operator = axdef(Opname,[],WD,block(Id,TypesOut,Axioms)), WD=[],
2235 ? select(axiomatic_def_block(Id,TypesIn,OpDefs,Axioms),AxDefsIn,
2236 axiomatic_def_block(Id,TypesOut,OpDefs,Axioms),AxDefsOut),
2237 ? select(Opname,TypesIn,TypesOut),!.
2238
2239 % two versions are supported: The older one expects an atom Tag, the new one a string
2240 % The string version is then parsed as a Prolog term.
2241 % as of 2023 we also support the bexpr(RawExpr) tag generated from $Expr$ in the .ptm file
2242 store_operator_by_tag(Tag,Opname,Operator,TheoryID,PT,Ops,Kind) :-
2243 is_list(Tag),!, % A string
2244 append(Tag,".",Tag1), % read_from_codes/2 needs a full-stop at the end
2245 read_from_codes(Tag1,Term),
2246 store_operator_by_tag(Term,Opname,Operator,TheoryID,PT,Ops,Kind).
2247 store_operator_by_tag(Tag,Opname,Operator,TheoryID,PT,Ops,Kind) :-
2248 store_operator_by_tag1(Tag,Opname,Operator,PT,Ops),
2249 get_operator_parameters(Operator,Parameters),
2250 pretty_print_tag(Tag,PrettyTag),
2251 store_operator_definition(TheoryID,Opname,Parameters,
2252 function(none,identifier(none,Kind),[identifier(none,PrettyTag)]),truth(none),[],
2253 axiomatic). % for bvisual2: todo pass type params PT
2254
2255 :- use_module(translate,[translate_raw_bexpr_with_limit/3]).
2256 pretty_print_tag(bexpr(Raw),TS) :- translate_raw_bexpr_with_limit(Raw,100,TS),!. % TODO: unicode
2257 pretty_print_tag(Tag,Tag).
2258
2259 store_operator_by_tag1(Tag,Opname,Operator,PT,Ops) :-
2260 debug_format(19,'Storing tag ~w for operator ~w~n',[Tag,Opname]),
2261 % SIGMA or PI
2262 aggregation_operator(Tag,Functor),!,
2263 get_operator_parameters(Operator,Parameters),
2264 ( Parameters = [Arg] ->
2265 create_raw_aggregation_op(Functor,Arg,ClassicalBOp),
2266 Ops=[Opname-axiomatic_definition(Tag,[Arg],ClassicalBOp,PT)]
2267 ;
2268 parameter_error(Parameters,1,Opname),Ops=[]
2269 ).
2270 store_operator_by_tag1(mkinat,OpName,Operator,PT,Ops) :- !,
2271 store_operator_by_tag1(mkinat(iZero,iSucc),OpName,Operator,PT,Ops).
2272 store_operator_by_tag1(mkinat(ZeroOp,SuccOp),OpName,Operator,_PT,Ops) :- !,
2273 get_operator_parameters(Operator,Parameters),
2274 ( Parameters = [argument(Arg,_ArgType)] ->
2275 Ops=[OpName-make_inductive_natural(Arg,ZeroOp,SuccOp)]
2276 ;
2277 parameter_error(Parameters,1,OpName),Ops=[]
2278 ).
2279 store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :-
2280 ? unary_operator_raw_term(BOperator,Arg1,Expr), !,
2281 check_if_operator_expr_uses_reals(Expr),
2282 get_operator_parameters(Operator,Parameters),
2283 ( Parameters = [argument(Arg1,_ArgType)] ->
2284 Ops=[Opname-axiomatic_definition(BOperator,Parameters,Expr,PT)]
2285 ; Parameters = [] -> % The Rodin theory operator is a constant without arguments
2286 Arg1='OpArg1',
2287 CArgs = [identifier(none,Arg1)],
2288 % try and generate lambda if we have an expression and relation for predicate
2289 % we assume they are all expressions:
2290 CurryExpr = lambda(none,CArgs,truth(none),Expr),
2291 % TODO: use ArgType1 in CurryExpr
2292 add_message(bmachine_eventb,'Lifting ProB unary operator to lambda expression (Rodin theory operator has no arguments): ',BOperator),
2293 Ops=[Opname-axiomatic_definition(BOperator,Parameters,CurryExpr,PT)]
2294 ;
2295 parameter_error(Parameters,1,Opname),Ops=[]
2296 ).
2297 store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :-
2298 ? binary_operator_raw_term(BOperator,Arg1,Arg2,Expr,Kind), !,
2299 check_if_operator_expr_uses_reals(Expr),
2300 get_operator_parameters(Operator,Parameters),
2301 ( Parameters = [argument(Arg1,_ArgType1), argument(Arg2,_ArgType2)] ->
2302 Ops=[Opname-axiomatic_definition(BOperator,Parameters,Expr,PT)]
2303 ; Parameters = [] -> % The Rodin theory operator is a constant without arguments
2304 Arg1='OpArg1', Arg2='OpArg2',
2305 CArgs = [identifier(none,Arg1),identifier(none,Arg2)],
2306 % try and generate lambda if we have an expression and relation for predicate
2307 (Kind=expression
2308 -> CurryExpr = lambda(none,CArgs,truth(none),Expr)
2309 ; CurryExpr = comprehension_set(none,CArgs,Expr)
2310 ),
2311 % TODO: use ArgType1/2 in CurryExpr
2312 add_message(bmachine_eventb,'Lifting ProB binary operator to lambda expression (Rodin theory operator has no arguments): ',BOperator),
2313 Ops=[Opname-axiomatic_definition(BOperator,Parameters,CurryExpr,PT)]
2314 ;
2315 parameter_error(Parameters,2,Opname),Ops=[]
2316 ).
2317 store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :-
2318 ? constant_operator_raw_term(BOperator,Expr), !,
2319 check_if_operator_expr_uses_reals(Expr),
2320 get_operator_parameters(Operator,Parameters),
2321 map_over_raw_expr(Expr,detect_external_fun_calls,RewrittenExpr),
2322 length(Parameters,NrParas),
2323 %format('Mapping operator ~w (~w paras: ~w) to: ',[Opname,NrParas,Parameters]), translate:print_raw_bexpr(RewrittenExpr),nl,
2324 ( Parameters = [] ->
2325 Ops=[Opname-axiomatic_definition(BOperator,Parameters,RewrittenExpr,PT)]
2326 ; can_be_predicate(RewrittenExpr,NrParas),
2327 maplist(argument_to_raw_id,Parameters,ParIds),
2328 couplise_raw_list(ParIds,ParCouple) ->
2329 % the operator is a predicate operator, in the .ptm file is a set comprehension defining it
2330 MembershipTest = member(none,ParCouple,RewrittenExpr),
2331 debug_println(19,created_membership_for_predicate_operator_call(Opname)),
2332 Ops=[Opname-axiomatic_definition(BOperator,Parameters,MembershipTest,PT)]
2333 ; % Create function application for set comprehensions / lambdas as parameters expected in Rodin
2334 can_be_function(RewrittenExpr,NrParas),
2335 maplist(argument_to_raw_id,Parameters,ParIds),
2336 couplise_raw_list(ParIds,ParCouple) ->
2337 Fapp = function(none,RewrittenExpr,ParCouple),
2338 debug_println(19,created_function_application_for_operator_call(Opname)),
2339 Ops=[Opname-axiomatic_definition(BOperator,Parameters,Fapp,PT)]
2340 ; %unreachable at the moment:
2341 parameter_error(Parameters,0,Opname),Ops=[]
2342 ).
2343
2344 argument_to_raw_id(argument(Arg,_),identifier(none,Arg)).
2345
2346 % TODO: maybe store/lookup type of operator and check if it is a predicate operator
2347 can_be_predicate(comprehension_set(_,Paras,_),NrParas) :-
2348 length(Paras,NrParas).
2349 can_be_predicate(symbolic_comprehension_set(Pos,Paras,B),NrParas) :-
2350 can_be_predicate(comprehension_set(Pos,Paras,B),NrParas).
2351
2352 % TODO: check if NrParas compatible
2353 can_be_function(comprehension_set(_,_,_),_NrParas) :- !.
2354 can_be_function(lambda(_,_,_,_),_) :- !.
2355 can_be_function(symbolic_comprehension_set(_,_,_),_) :- !.
2356 can_be_function(sequence_extension(_,_),_) :- !.
2357 can_be_function(E,_) :- functor(E,F,N), add_message(bmachine_eventb,'Attempting function application for:',F/N).
2358
2359 couplise_raw_list([Arg],Res) :- !, Res=Arg.
2360 couplise_raw_list([A,B],Res) :- !, Res=couple(none,A,B).
2361 couplise_raw_list([A,B|Rest],Result) :-
2362 couplise_raw_list([couple(A,B)|Rest],Result).
2363
2364
2365 :- use_module(external_functions, [get_external_function_type/3]).
2366 % traverse raw AST to detect calls to external functions which would not be visible in regular typechecking
2367 % these expressions come from the .ptm files where we want to be able to have access to external functions
2368 % TODO: also allow access to external predicates and external constants like REULER
2369 detect_external_fun_calls(function(Pos,TID,Args),external_function_call_auto(Pos,ID,NewArgs)) :-
2370 TID = identifier(_IdPos,ID),
2371 get_external_function_type(ID,ExpectedArgTypes,_OutputType), % TODO: check visible
2372 length(Args,Len),
2373 length(ExpectedArgTypes,ExtExpectedLen),
2374 (Len=ExtExpectedLen -> true
2375 ; parameter_error(Args,ExtExpectedLen,ID),fail),
2376 !,
2377 debug_println(19,detected_external_function_call(ID,Len)),
2378 map_over_args(Args,NewArgs). % we need to inspect tree of arguments as well, map_over_raw_expr works top-down
2379
2380 map_over_args([],[]).
2381 map_over_args([Arg1|T],[NewArg1|NT]) :- map_over_raw_expr(Arg1,detect_external_fun_calls,NewArg1),
2382 map_over_args(T,NT).
2383
2384
2385 % TO DO ternary operator ?? son/3 if_then_else
2386
2387 % construct a raw term with arguments for replacement in AST
2388 % first argument is functor name as it appears in the theory mapping file *.ptm
2389 binary_operator_raw_term(Functor,Arg1,Arg2,Term,Kind) :-
2390 ? binary_operator_to_ast(Functor,ASTFunctor,Kind), % TODO: return Kind
2391 Term =.. [ASTFunctor,none,identifier(none,Arg1),identifier(none,Arg2)].
2392 binary_operator_raw_term(Functor,Arg1,Arg2,Term,predicate) :-
2393 binary_external_predicate(Functor,ASTFunctor),
2394 Term = external_pred_call_auto(none, ASTFunctor, [identifier(none,Arg1),identifier(none,Arg2)]).
2395 binary_operator_raw_term(Functor,Arg1,Arg2,Term,expression) :-
2396 ? binary_external_function(Functor,ASTFunctor),
2397 Term = external_function_call_auto(none, ASTFunctor, [identifier(none,Arg1),identifier(none,Arg2)]).
2398
2399 binary_operator_to_ast(BOP,ASTFunctor,expression) :-
2400 binary_expr_operator_to_ast(BOP,ASTFunctor).
2401 binary_operator_to_ast(BOP,ASTFunctor,predicate) :-
2402 binary_pred_operator_to_ast(BOP,ASTFunctor).
2403 binary_expr_operator_to_ast('^',concat).
2404 binary_expr_operator_to_ast(concat,concat).
2405 %binary_expr_operator_to_ast(div,floored_div). % now dealt with in get_typed_default_operator
2406 binary_expr_operator_to_ast(restrict_front,restrict_front).
2407 binary_expr_operator_to_ast(restrict_tail,restrict_tail).
2408 % binary tree operators
2409 binary_expr_operator_to_ast(arity,arity).
2410 binary_expr_operator_to_ast(bin,bin).
2411 binary_expr_operator_to_ast(const,const).
2412 binary_expr_operator_to_ast(father,father).
2413 binary_expr_operator_to_ast(rank,rank).
2414 binary_expr_operator_to_ast(subtree,subtree).
2415 % real operators
2416 binary_expr_operator_to_ast(rdiv,div_real).
2417 binary_expr_operator_to_ast(plus,add_real).
2418 binary_expr_operator_to_ast(power_of_real,power_of_real).
2419 binary_expr_operator_to_ast(power_of,power_of). % also in get_typed_default_operator
2420 binary_expr_operator_to_ast(pow,power_of). % ditto
2421 binary_expr_operator_to_ast(minus,minus_real).
2422 binary_expr_operator_to_ast(mul,multiplication_real).
2423 binary_expr_operator_to_ast(mult,multiplication_real).
2424 % real predicates:
2425 binary_pred_operator_to_ast(less,less_real).
2426 binary_pred_operator_to_ast(less_equal,less_equal_real).
2427 binary_pred_operator_to_ast('smr',less_real). % from Rodin Real Theory v.2.1
2428 binary_pred_operator_to_ast(leq,less_equal_real). % from Rodin Real Theory v.2.1
2429 % Note: there is currently no greater_real and greater_equal_real
2430
2431 binary_external_predicate('\x22D7\','RGT'). % 8919 - greater with dot
2432 binary_external_predicate(greater,'RGT').
2433 binary_external_predicate(greater_equal,'RGEQ').
2434 binary_external_predicate('\x22D6\','RLT'). % 8918 - less with dot
2435 %binary_external_predicate(less,'RLT').
2436 %binary_external_predicate(less_equal,'RLEQ').
2437 binary_external_predicate(geq,'RGEQ').
2438 %binary_external_predicate(leq,'RLEQ'). % from Rodin Real Theory v.2.1
2439 %binary_external_predicate(smr,'RLT'). % ditto
2440 binary_external_predicate(gtr,'RGT'). % ditto
2441 binary_external_predicate(inv,'RINV'). % ditto
2442 binary_external_predicate(FUN,FUN) :-
2443 treat_as_external_pred(FUN).
2444
2445 treat_as_external_pred('REQ').
2446 treat_as_external_pred('RGT').
2447 treat_as_external_pred('RGEQ').
2448 treat_as_external_pred('RLT').
2449 treat_as_external_pred('RLEQ').
2450 treat_as_external_pred('RNEQ').
2451
2452 treat_as_external_pred('LESS'). % Prolog term order
2453 treat_as_external_pred('LEQ_SYM_BREAK').
2454 treat_as_external_pred('STRING_IS_INT').
2455 treat_as_external_pred('STRING_IS_NUMBER').
2456 treat_as_external_pred('STRING_IS_DECIMAL').
2457 treat_as_external_pred('STRING_IS_ALPHANUMERIC'). % TODO: provide more external predicates
2458
2459 binary_external_function('\x2295\','RADD'). % Unicode + with circle
2460 binary_external_function('\x2296\','RSUB').
2461 binary_external_function('\x2297\','RMUL'). % has a pre-defined Rodin meaning as direct product
2462 binary_external_function('\x2298\','RDIV').
2463 binary_external_function('\x2299\','RMUL'). % dot with circle
2464 ?binary_external_function(FUN,FUN) :- visible_external_function(FUN,2),
2465 \+ treat_as_external_pred(FUN).
2466
2467 :- use_module(tools,[arg_is_number/2]).
2468 % Already parsed B expression:
2469 constant_operator_raw_term(bexpr(Tree),Tree).
2470 % some types not available in Event-B:
2471 constant_operator_raw_term('FLOAT',float_set(none)).
2472 constant_operator_raw_term('REAL',real_set(none)).
2473 constant_operator_raw_term('\x211D\',real_set(none)). % unicode Real symbol 8477 in decimal
2474 constant_operator_raw_term('STRING',string_set(none)).
2475 % direct encodings:
2476 %constant_operator_raw_term('RONE',real(none,'1.0')).
2477 %constant_operator_raw_term('RZERO',real(none,'1.0')).
2478 constant_operator_raw_term(empty_string,string(none,'')).
2479 constant_operator_raw_term('EMPTY_STRING',string(none,'')).
2480 % some synonyms:
2481 constant_operator_raw_term(zero,T) :- T = real(none,'0.0'). %constant_operator_raw_term('RZERO',T).
2482 constant_operator_raw_term(one,T) :- T = real(none,'1.0'). %constant_operator_raw_term('RONE',T).
2483 constant_operator_raw_term(two,T) :- T=real(none,'2.0').
2484 constant_operator_raw_term(pi,T) :- constant_operator_raw_term('RPI',T).
2485 constant_operator_raw_term(euler,T) :- constant_operator_raw_term('REULER',T).
2486 constant_operator_raw_term(Name,external_function_call_auto(none,Name,[])) :-
2487 ? visible_external_function(Name,0).
2488 constant_operator_raw_term(Atom,T) :-
2489 arg_is_number(Atom,Number),
2490 (integer(Number) -> T=integer(none,Number)
2491 ; atom(Atom), % otherwise we would need to convert it to an atom for the AST
2492 T=real(none,Atom)).
2493 % This case shouldn't be needed anymore.
2494 % The theorymapping library now parses formulas ahead of time
2495 % and sends the parsed AST in a bexpr/1 term.
2496 constant_operator_raw_term(Atom,Tree) :-
2497 atom(Atom), atom_codes(Atom,Codes),
2498 %format('Tag string: ~s~n',[Codes]),
2499 get_formula_codes(Codes,FCodes),
2500 %format('Stripped delimiter: ~s~n',[FCodes]),
2501 parsercall:parse_formula(FCodes,Tree).
2502 % TODO: allow B formulas also for binary/unary operators
2503
2504 get_formula_codes([Del|T],Codes) :- delimiter(Del),!,skip_last(T,Codes,Del). % strip leading and trailing delimiter
2505 skip_last([H],[],Last) :- !, Last=H.
2506 skip_last([H|T],[H|ST],Last) :- skip_last(T,ST,Last).
2507
2508 %delimiter(0'").
2509 delimiter(36). % dollar $
2510 %delimiter(39). % simple quote
2511
2512
2513 :- use_module(external_function_declarations,[external_function_library/4]).
2514 visible_external_function(Name,Arity) :-
2515 ? external_function_library(Name,Arity,expression,Lib),
2516 visible_lib(Lib).
2517
2518 visible_lib('LibraryMath.def').
2519 visible_lib('LibraryRandom.def').
2520 visible_lib('LibraryReals.def').
2521 visible_lib('LibraryStrings.def').
2522 visible_lib('CHOOSE.def').
2523 visible_lib('SCCS.def').
2524 visible_lib('SORT.def').
2525 % visible_lib('LibrarySoftfloats.def'). % comment in to make Softfloats available for theory mapping
2526
2527
2528 % construct a raw term with argument for replacement in AST
2529 % first argument is functor name as it appears in the theory mapping file *.ptm
2530 unary_operator_raw_term(Functor,Arg,Term) :-
2531 ? unary_operator_to_ast(Functor,ASTFunctor),
2532 Term =.. [ASTFunctor,none,identifier(none,Arg)].
2533 unary_operator_raw_term(Functor,Arg,Term) :-
2534 ? unary_external_function(Functor,AstFunctor),
2535 Term = external_function_call_auto(none, AstFunctor, [identifier(none,Arg)]).
2536 unary_operator_to_ast(closure,reflexive_closure). % reflexive_closure corresponds to closure B operator !
2537 unary_operator_to_ast(closure1,closure).
2538 unary_operator_to_ast(conc,general_concat).
2539 unary_operator_to_ast(fnc,trans_function).
2540 unary_operator_to_ast(rel,trans_relation).
2541 unary_operator_to_ast(succ,successor). % also exist in Event-B
2542 unary_operator_to_ast(pred,predecessor). % also exist in Event-B
2543 unary_operator_to_ast(bool,convert_bool). % also exist in Event-B
2544 unary_operator_to_ast(id,identity). % exists in similar way in Event-B
2545 unary_operator_to_ast(union,general_union).
2546 unary_operator_to_ast(inter,general_intersection).
2547 % real operators
2548 unary_operator_to_ast(real,convert_real).
2549 unary_operator_to_ast(floor,convert_int_floor).
2550 unary_operator_to_ast(ceiling,convert_int_ceiling).
2551 unary_operator_to_ast(minus,unary_minus_real). % minus also maps to binary minus
2552 unary_operator_to_ast(max,max_real).
2553 unary_operator_to_ast(min,min_real).
2554 unary_operator_to_ast(F,F) :- unary_operator(F). % operators that have same name in B and AST
2555
2556
2557 unary_external_function(choose,'CHOOSE').
2558 unary_external_function(length,'STRING_LENGTH').
2559 unary_external_function(inv,'RINV').
2560 ?unary_external_function(Functor,Functor) :- visible_external_function(Functor,1).
2561
2562 % sequence operators
2563 unary_operator(seq).
2564 unary_operator(seq1).
2565 unary_operator(iseq).
2566 unary_operator(iseq1).
2567 unary_operator(perm).
2568 unary_operator(first).
2569 unary_operator(size).
2570 unary_operator(front).
2571 unary_operator(tail).
2572 unary_operator(rev).
2573 unary_operator(last).
2574 unary_operator(mu).
2575 % tree operators
2576 unary_operator(tree).
2577 unary_operator(btree).
2578 unary_operator(top).
2579 unary_operator(sons).
2580 unary_operator(bin).
2581 unary_operator(left).
2582 unary_operator(right).
2583 unary_operator(sizet).
2584 unary_operator(prefix).
2585 unary_operator(postfix).
2586 %unary_operator(infix). % not yet supported
2587 %unary_operator(mirror). % not yet supported
2588 % general operators
2589 unary_operator(min). % also exist in Event-B
2590 unary_operator(max). % also exist in Event-B
2591 unary_operator(domain).
2592 unary_operator(range).
2593 % z operators
2594 unary_operator(compaction).
2595 unary_operator(bag_items).
2596
2597 % in the SUMandPRODUCT theory provided on https://prob.hhu.de/w/index.php?title=Event-B_Theories
2598 % the SIGMA and PI operators work on relations TYPE <-> INTEGER
2599 % we actually create SIGMA(I,N).(I|->N:Arg | N) or PI
2600 % However, we now also support SIGMA and PI to work directly on integer sets
2601 aggregation_operator('SIGMA',general_sum).
2602 aggregation_operator('PI',general_product).
2603
2604 integer_set_type(pow_subset(_,integer_set(_))).
2605 relation_to_integer_type(pow_subset(_,cartesian_product(_,_,integer_set(_)))).
2606 binary_relation_type(pow_subset(_,cartesian_product(_,_A,_B))).
2607
2608
2609 create_raw_aggregation_op(Op,argument(Arg,ArgType),Result) :-
2610 integer_set_type(ArgType),!,
2611 % we have an operator acting directly on sets of integers
2612 % we translate it as SIGMA(N).(N:Arg|N)
2613 A = identifier(none,Arg), % User-given argument
2614 create_fresh_identifier('_agg_op1',[A],I1), % starting with _ ensures user cannot create such an id
2615 N = identifier(none,I1), % N is the integer to sum or multiply
2616 Pred = member(none,N,A), % I|->N : Arg
2617 Result =.. [Op,none,[N],Pred,N]. % SIGMA(I,N).(I|->N:Arg | N) (or PI)
2618 create_raw_aggregation_op(Op,argument(Arg,_ArgType),Result) :-
2619 % this construction will immediately wrap _agg_op1/2 inside Sigma or Pi, and thus _agg_op1/2 will not be visibile outside
2620 A = identifier(none,Arg), % User-given argument
2621 create_fresh_identifier('_agg_op1',[A],I1), % starting with _ ensures user cannot create such an id
2622 create_fresh_identifier('_agg_op2',[A],I2), % (in Camille at least)
2623 I = identifier(none,I1), % I is the (not used) index variable
2624 N = identifier(none,I2), % N is the integer to sum or multiply
2625 Pred = member(none,couple(none,I,N),A), % I|->N : Arg
2626 Result =.. [Op,none,[I,N],Pred,N]. % SIGMA(I,N).(I|->N:Arg | N) (or PI)
2627
2628 parameter_error(RodinParameters,ExpectedByProB,Opname) :-
2629 length(RodinParameters,N),
2630 ajoin(['ProB theory mapping: ProB translation expects ',ExpectedByProB,' parameter(s) for operator ',
2631 Opname,' but Rodin definition has ',N],Msg),
2632 add_error(bmachine_eventb,Msg).
2633
2634 get_operator_parameters(operator(_Opname,Parameters,_WD,_DirectDef,_RecursiveDef),Parameters).
2635 get_operator_parameters(axdef(_Opname,Parameters,_WD,_Block),Parameters).
2636
2637 store_eventb_operator(Id,Op,Ein,Eout) :-
2638 env_store_operator(Id,bmachine_eventb:Op,Ein,Eout).
2639
2640
2641 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2642 % Operator for constructing inductive natural numbers (mkinat in Rodin .ptm theory mapping file)
2643 :- public make_inductive_natural/11.
2644 % called by btypechecker:lookup_eventb_operator
2645 make_inductive_natural(ArgId,ZeroOp,SuccOp,
2646 Id,[TParam],_Pos,Env,expr,Result,TRin,TRout) :-
2647 unique_id("opresult.",ResultId),
2648 create_typed_id(ResultId,NatType,TResult),
2649 create_typed_id(ArgId,integer,TArgId),
2650 % prepare environment:
2651 add_identifiers_to_environment([TArgId,TResult],Env,Env1),
2652 % we create a recursive function by using a (as recursive annotated) comprehension
2653 % set. We can refer to the compset with RecId.
2654 create_recursive_compset([TArgId,TResult],Cond,set(couple(integer,NatType)),[],RecId,TCompSet),
2655 % used for recursive call:
2656 env_store(RecId,set(couple(integer,NatType)),[],Env1,SubEnv),
2657 % just type iZero to retrieve its type:
2658 IZero=extended_expr(none,ZeroOp,[],[]),
2659 btype(make_inductive_natural,IZero,SubEnv,NatType,_,TRin,TR1),
2660 % Arg=0 => Result=iZero
2661 RawCase1=implication(none,
2662 equal(none,identifier(none,ArgId),integer(none,0)),
2663 equal(none,identifier(none,ResultId),IZero)),
2664 btype(make_inductive_natural,RawCase1,SubEnv,pred,Case1,TR1,TR2),
2665 % Arg>0 => Result=iSucc( recursive_call(Arg-1) )
2666 RawCase2=implication(none,
2667 greater(none,identifier(none,ArgId),integer(none,0)),
2668 equal(none,identifier(none,ResultId),extended_expr(none,SuccOp,[Minus1],[]))),
2669 Minus1=function(none,identifier(none,RecId),minus(none,identifier(none,ArgId),integer(none,1))),
2670 btype(make_inductive_natural,RawCase2,SubEnv,pred,Case2,TR2,TRout),
2671 % {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )}
2672 conjunct_predicates([Case1,Case2],Cond),
2673 % {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )}(TParam)
2674 create_texpr(function(TCompSet,TParam),NatType,[theory_operator(Id,1)],Result).