1		% (c) 2009-2019 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		,prime_variable/2
7		,prime_variables/2
8		,deferred_set_equality_without_enumeration_axioms/2
9		,is_eventb_additional_info/1
10		,raw_event/10
11		,is_primed_id/1
12		]).
13
14		:- use_module(library(lists)).
15		:- use_module(library(ordsets)).
16		:- use_module(library(avl)).
17		:- use_module(library(codesio),[read_from_codes/2]).
18
19		:- use_module(error_manager).
20		:- use_module(tools,[remove_all/3,foldl/4,foldl/5,foldl/6,ajoin_with_sep/3,unique_id/2]).
21		:- use_module(self_check).
22		:- use_module(btypechecker).
23		:- use_module(b_ast_cleanup).
24		:- use_module(bsyntaxtree).
25		:- use_module(debug).
26		:- use_module(bmachine_construction).
27		:- use_module(preferences,[get_preference/2]).
28		:- use_module(input_syntax_tree,[extract_raw_identifiers/2,create_fresh_identifier/3]).
29		:- use_module(translate,[translate_bexpression/2]).
30		:- use_module(pragmas,[extract_pragmas_from_event_b_extensions/2,apply_pragmas_to_event_b_machine/3]).
31
32		:- use_module(module_information,[module_info/2]).
33		:- module_info(group,typechecker).
34		:- module_info(description,'This module contains the rules for loading a Event-B machine or context. ').
35
36		:- use_module(specfile,[eventb_mode/0]).
37		deferred_set_equality_without_enumeration_axioms(Set,ExtSet) :-
38		eventb_mode,
39		deferred_set_eq_wo_enumeration_axioms(Set,ExtSet),
40		% there is a single equality Set = {id1,...,idn} and no partition or not enough disequalities
41		% quite often the user forgot to add those disequalities
42		\+ (deferred_set_eq_wo_enumeration_axioms(Set,ExtS2), ExtS2 \= ExtSet).
43
44		:- dynamic deferred_set_eq_wo_enumeration_axioms/2.
45
46		check_event_b_project(RawModels,RawContextes,Extensions,MachineWithPragmas) :-
47		retractall(deferred_set_eq_wo_enumeration_axioms(_,_)),
48		catch( check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas),
49		typecheck_errors(Errors),
50		( add_all_perrors(Errors),fail )).
51		check_event_b_project1([],RawContextes,Extensions,MachineWithPragmas) :-
52		!,
53		check_extensions(Extensions,Freetypes,Ops,InitEnv), % Theories
54		check_contextes(InitEnv,RawContextes,Contextes),
55		convert_event_b(context,Freetypes,Ops,Contextes,[],[],Machine),
56		extract_pragmas_from_event_b_extensions(Extensions,Pragmas),
57		apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas).
58		check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas) :-
59		compute_animation_chain(RawModels,AnimationChain),
60		check_event_b_project2(RawModels,RawContextes,Extensions,
61		AnimationChain,Machine),
62		extract_pragmas_from_event_b_extensions(Extensions,Pragmas),
63		apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas).
64
65		check_event_b_project2(RawModels,RawContextes,Extensions,AnimationChain,Machine) :-
66		RawModels=[event_b_model(_,Main,_)|_],
67		check_extensions(Extensions,Freetypes,Ops,InitEnv), % related to Theory plugin
68		% generate type-checked contextes
69		check_contextes(InitEnv,RawContextes,Contextes),
70		% generate type-checked models
71		check_models(InitEnv,RawModels,Contextes,Models),
72		% merge all the constants/vars/predicates and events into one machine
73		convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine).
74
75		% the filter chain contains the name of all models that
76		% should be contained in the animation
77		compute_animation_chain(Models,AnimationChain) :-
78		get_preference(number_animated_abstractions,N),
79		debug_println(9,compute_animation_chain(N)),
80		length(Models,L),
81		N1 is min(N+1,L),
82		prefix_length(Models, AnimatedModels, N1),
83		extract_model_names(AnimatedModels,AnimationChain).
84		extract_model_names([],[]).
85		extract_model_names([event_b_model(_,Name,_)|MRest],[Name|NRest]) :-
86		extract_model_names(MRest,NRest).
87
88		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
89		% context
90
91		check_contextes(InitEnv,RawContextes,Contextes) :-
92		debug_println(9,'Checking Contextes'),
93		% make sure that a extended context is treated before
94		% the extending context
95		topological_sort(RawContextes,SortedContextes),
96		check_contextes2(SortedContextes,InitEnv,[],Contextes).
97		check_contextes2([],_,_,[]).
98		check_contextes2([RawContext|Rrest],InitEnv,PrevContextes,[Context|Crest]) :-
99		check_context(RawContext,InitEnv,PrevContextes,Context),
100		check_contextes2(Rrest,InitEnv,[Context|PrevContextes],Crest).
101
102		check_context(RawContext,InitEnv,PrevContextes,Context) :-
103		extract_ctx_sections(RawContext,Name,Extends,
104		RawSets,RawConstants,RawAbstractConstants,RawAxioms,RawTheorems),
105		Context = context(Name,Extends,Sets,Constants,AbstractConstants,Axioms,Theorems),
106
107		% create deferred sets
108		create_sets(RawSets,Name,Sets),
109		% and constants
110		IdInfos = [loc(Name,constants),section(Name)],
111		create_identifiers(RawConstants,IdInfos,Constants),
112		create_identifiers(RawAbstractConstants,IdInfos,AbstractConstants),
113
114		% with the constants and set of seen contextes,
115		create_ctx_env(Extends,PrevContextes,InitEnv,PrevEnv),
116		% and the sets and constants
117		add_unique_variables(Sets,PrevEnv,SetEnv),
118		add_unique_variables(Constants,SetEnv,EnvT),
119		add_unique_variables(AbstractConstants,EnvT,Env),
120
121		% now typecheck the axioms and theorems,
122		% this should determine the constant's types
123		typecheck_together([RawAxioms,RawTheorems],Env,[Axioms,Theorems],axioms).
124
125		extract_ctx_sections(RawContext,Name,Extends,RawSets,RawConstants,RawAbstractConstants,RawAxioms,RawTheorems) :-
126		RawContext = event_b_context(_Pos,Name,Sections),
127		optional_rawmachine_section(extends,Sections,[],Extends),
128		optional_rawmachine_section(sets,Sections,[],RawSets),
129		optional_rawmachine_section(constants,Sections,[],RawConstants),
130		optional_rawmachine_section(abstract_constants,Sections,[],RawAbstractConstants),
131		optional_rawmachine_section(axioms,Sections,[],RawAxioms),
132		optional_rawmachine_section(theorems,Sections,[],RawTheorems).
133
134
135		create_sets([],_,[]).
136		create_sets([RawSet|RSrest],CtxName,[Set|Srest]) :-
137		ext2int(RawSet,deferred_set(SetName),_,set(global(SetName)),
138		identifier(SetName),[section(CtxName),given_set],Set),
139		create_sets(RSrest,CtxName,Srest).
140
141		create_identifiers([],_,[]).
142		create_identifiers([RawIdentifier|RIrest],Infos,[Identifier|Irest]) :-
143		ext2int(RawIdentifier,I,_,_,I,Infos,Identifier),
144		I=identifier(_),
145		create_identifiers(RIrest,Infos,Irest).
146
147		create_ctx_env(Extends, Contextes, Old, New) :-
148		% find all seen contextes (and their extended contextes,
149		% and again their extended contextes, ...)
150		transitive_contextes(Extends,Contextes,TransExt),
151		% and all variables of extended machines
152		add_env_vars_for_extended2(TransExt,Contextes,Old,New).
153		transitive_contextes(Extends,Contextes,All) :-
154		findall(E, transext(Extends,Contextes,E), All1), sort(All1, All).
155		transext(Extends,_,E) :- member(E,Extends).
156		transext(Extends,Contextes,E) :-
157		member(Name,Extends),
158		internal_context_extends(Context,Name,NewExtends),
159		member(Context,Contextes),
160		transext(NewExtends,Contextes,E).
161		% add_env_vars_for_extended2(Names,Contextes,OldEnv,NewEnv):
162		% Names: a list of the names of the contextes whose constants and sets
163		% should be added to the type environment
164		% Contextes: a list of all existing contextes
165		% OldEnv: the input environment
166		% NewEnv: the input environment plus the constants and sets
167		add_env_vars_for_extended2([],_,Env,Env).
168		add_env_vars_for_extended2([Name|Erest],Contextes,Old,New) :-
169		internal_context_sets(Context,Name,Sets),
170		internal_context_constants(Context,Name,Constants),
171		internal_context_abstract_constants(Context,Name,AbstractConstants),
172		member(Context,Contextes),!,
173		add_unique_variables(Sets,Old,Env1),
174		add_unique_variables(Constants,Env1,Env2),
175		add_unique_variables(AbstractConstants,Env2,Env),
176		add_env_vars_for_extended2(Erest,Contextes,Env,New).
177
178		% copy&paste from bmachine_construction
179		add_unique_variables([],Env,Env).
180		add_unique_variables([Var|Rest],Old,New) :-
181		def_get_texpr_id(Var,Name),
182		get_texpr_type(Var,Type),
183		get_texpr_info(Var,Infos),
184		( env_lookup_type(Name,Old,_) ->
185		add_error(bmachine_eventb,'Identifier declared twice',Name),
186		fail
187		; otherwise -> true),
188		env_store(Name,Type,Infos,Old,Env),
189		add_unique_variables(Rest,Env,New).
190
191		% add the primed (') versions of the variables to the
192		% type environment
193		add_primed_variables(Variables,OrigEnv,NewEnv) :-
194		prime_variables(Variables,Primed),
195		add_unique_variables(Primed,OrigEnv,NewEnv).
196
197
198		:- use_module(btypechecker,[prime_identifiers/2,prime_identifier/2,prime_identifiers0/2]).
199
200		% add a prime (') to each typed identifier
201		prime_variables(V,PV) :- prime_identifiers(V,PV).
202		% add a prime (') to a typed identifier
203		prime_variable(V,P) :- prime_identifier(V,P).
204		% add (or remove) a prime (') to a plain identifier (without syntax structure)
205		prime_id(UnPrimed,Primed) :-
206		atom_concat(UnPrimed,'\'',Primed).
207
208		% unprime_id( ListoPrimedIds, CorrespondingIds, PossiblyPrimedID, UnprimedID)
209		unprime_id(AtomicIds0,AtomicIds,Id0,Id) :- nth1(N,AtomicIds0,Id0),!, nth1(N,AtomicIds,Id).
210		unprime_id(_,_,Id,Id).
211
212		check_for_errors(Errors) :-
213		% TO DO: extract and add warnings in list
214		Errors = [_|_],!,throw(typecheck_errors(Errors)).
215		check_for_errors([]).
216
217		typecheck_l(Untyped,Env,Type,Typed,Context) :-
218		all_same(Untyped,Type,Types),
219		btype_ground_dl(Untyped,Env,[],Types,Typed1,Errors,[]),
220		check_for_errors(Errors),
221		clean_up_l_with_optimizations(Typed1,[],Typed,Context),!.
222		typecheck_l(Untyped,Env,Type,Typed,Context) :-
223		add_failed_call_error(typecheck_l(Untyped,Env,Type,Typed,Context)),fail.
224		all_same([],_,[]).
225		all_same([_|R],E,[E|T]) :- all_same(R,E,T).
226
227		typecheck(Untyped,Env,Type,Typed) :-
228		typecheck_with_freevars(Untyped,Env,[],Type,Typed).
229		typecheck_with_freevars(Untyped,Env,Freevars,Type,Typed) :-
230		btype_ground_dl([Untyped],Env,Freevars,[Type],[Typed1],Errors,[]),
231		clean_up_pred_or_expr(Freevars,Typed1,Typed),
232		check_for_errors(Errors).
233
234
235
236
237
238		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
239		% models
240
241		check_models(InitEnv,RawModels,Contextes,Models) :-
242		debug_println(9,'CHECKING MODELS'),
243		topological_sort(RawModels,SortedModels),
244		check_models2(SortedModels,InitEnv,[],Contextes,Models).
245
246		check_models2([],_,_,_,[]).
247		check_models2([RawModel|RMrest],InitEnv,PrevModels,Contextes,[Model|Mrest]) :-
248		(check_model(RawModel,InitEnv,PrevModels,Contextes,Model) -> true
249		; add_failed_call_error(check_model(RawModel,InitEnv,PrevModels,Contextes,Model)),
250		fail),
251		check_models2(RMrest,InitEnv,[Model|PrevModels],Contextes,Mrest).
252
253		check_model(RawModel,InitEnv,PrevModels,Contextes,Model) :-
254		extract_model_sections(RawModel,Name,Refines,Sees,
255		RawVariables,RawInvariant,
256		RawTheorems,RawVariant,RawEvents),
257		Model = model(Name,Refines,Sees,ConcreteVariables,NewVariables,Invariant,Theorems,Events),
258		get_refined_model(Refines,PrevModels,RefinedModel),
259
260		get_all_abstract_variables(Refines,PrevModels,AbstractionVariables),
261		length(PrevModels,Level),
262		IdInfos = [loc(Name,variables),section(Name),level(Level)],
263		create_identifiers(RawVariables,IdInfos,ConcreteVariables),
264		split_abstract_vars(AbstractionVariables,ConcreteVariables,
265		NewVariables,DroppedAbstractVars),
266
267		create_ctx_env(Sees,Contextes,InitEnv,CtxEnv),
268		add_unique_variables(ConcreteVariables,CtxEnv,ModelEnv),
269		add_unique_variables(DroppedAbstractVars,ModelEnv,InvEnv),
270		% add primed versions of the concrete variables to
271		% permit before-after predicates in the witnesses
272		add_primed_variables(ConcreteVariables,InvEnv,BeforeAfterEnv),
273
274		typecheck_together([RawInvariant,RawTheorems],InvEnv,[Invariant,Theorems],invariant),
275
276		typecheck_variant(RawVariant,InvEnv,Variant),
277
278		get_abstract_events(RefinedModel,AbstractEvents),
279
280		check_events(RawEvents,Name,ModelEnv,BeforeAfterEnv,InvEnv,
281		DroppedAbstractVars,ConcreteVariables,AbstractEvents,
282		NewVariables,Variant,Events).
283
284		% Context is just an information term about the context (axioms, ...)
285		typecheck_together(Raws,Env,Typed,Context) :-
286		maplist(same_length, Raws, Typed),
287		append(Raws,RawL), append(Typed,TypedL),
288		typecheck_l(RawL,Env,pred,TypedL,Context).
289
290		typecheck_variant(-, _Env, -) :- !.
291		typecheck_variant(RawVariant, Env, Variant) :-
292		typecheck(RawVariant, Env, Type, Variant),
293		( Type==integer -> true
294		; functor(Type,set,1) -> true
295		; otherwise ->
296		add_error(bmachine_eventb,'Invalid type of variant ',Type),
297		fail).
298
299		remove_linking_parts([],_AnimationChain,[]).
300		remove_linking_parts([Inv|Irest],AnimationChain,Invariants) :-
301		( abstraction_var_occures(Inv,AnimationChain) ->
302		Invariants = RestInvariants
303		; otherwise ->
304		Invariants = [Inv|RestInvariants]),
305		remove_linking_parts(Irest,AnimationChain,RestInvariants).
306
307		abstraction_var_occures(TExpr,AnimationChain) :-
308		get_texpr_expr(TExpr,identifier(_)),!,
309		get_texpr_section(TExpr,Section),
310		\+ member(Section,AnimationChain).
311		abstraction_var_occures(TExpr,AnimationChain) :-
312		syntaxtraversion(TExpr,_,_,_,Subs,_),
313		abstraction_var_occures_l(Subs,AnimationChain).
314		abstraction_var_occures_l([Sub|_],AnimationChain) :-
315		abstraction_var_occures(Sub,AnimationChain),!.
316		abstraction_var_occures_l([_|Srest],AnimationChain) :-
317		abstraction_var_occures_l(Srest,AnimationChain).
318
319		get_texpr_section(TExpr,Section) :-
320		get_texpr_info(TExpr,Info),member(section(Section),Info),!.
321
322		extract_model_sections(RawModel,Name,Refines,Sees,Variables,Invariant,Theorems,Variant,Events) :-
323		RawModel = event_b_model(_Pos,Name,Sections),
324		optional_rawmachine_section(refines,Sections,-,Refines),
325		optional_rawmachine_section(sees,Sections,[],Sees),
326		optional_rawmachine_section(variables,Sections,[],Variables),
327		optional_rawmachine_section(invariant,Sections,[],Invariant),
328		optional_rawmachine_section(theorems,Sections,[],Theorems),
329		optional_rawmachine_section(variant,Sections,-,Variant),
330		optional_rawmachine_section(events,Sections,[],Events).
331
332		%get_abstraction_variables(-,[]).
333		%get_abstraction_variables(Model,Variables) :-
334		% internal_model_vars(Model,_Name,Variables).
335
336		get_abstract_events(-,[]).
337		get_abstract_events(Model,Events) :- internal_model_events(Model,_Name,Events).
338
339		get_refined_model(-,_Models,-) :- !.
340		get_refined_model(Name,Models,Model) :-
341		internal_model(M,Name),
342		( memberchk(M,Models) ->
343		M=Model
344		; otherwise ->
345		add_error(bmachine_eventb,'Unable to find refined model ',Name),
346		fail).
347
348		split_abstract_vars(AbstractVars,ConcreteVars,NewVars,DroppedVars) :-
349		split_abstract_vars2(AbstractVars,ConcreteVars,DroppedVars),
350		find_new_variables(ConcreteVars,AbstractVars,NewVars).
351		split_abstract_vars2([],_,[]).
352		split_abstract_vars2([AbstractVar|AVrest],ConcreteVars,Dropped) :-
353		( find_identifier_in_list(AbstractVar,ConcreteVars,ConcreteVar) ->
354		% Both variables have the same type
355		get_texpr_type(AbstractVar,Type),
356		get_texpr_type(ConcreteVar,Type),
357		Dropped = DroppedRest
358		; otherwise ->
359		Dropped = [AbstractVar|DroppedRest]),
360		split_abstract_vars2(AVrest,ConcreteVars,DroppedRest).
361		find_new_variables([],_,[]).
362		find_new_variables([ConcreteVar|CVrest],AbstractVars,NewVars) :-
363		( find_identifier_in_list(ConcreteVar,AbstractVars,_AbstractVar) -> NewVars = Nrest
364		; otherwise -> NewVars = [ConcreteVar|Nrest]),
365		find_new_variables(CVrest,AbstractVars,Nrest).
366
367		% find_identifier_in_list(TypedIdToFind,List,Elem):
368		% search for a typed identifier Elem in List wich
369		% has the same id as TypedIdToFind, but type and informations
370		% may be different
371		find_identifier_in_list(TypedIdToFind,List,Found) :-
372		def_get_texpr_id(TypedIdToFind,Id),
373		get_texpr_id(Found,Id),
374		member(Found,List).
375
376		get_all_abstract_variables(Refines,AbstractModels,AbstractVariables) :-
377		get_all_abstract_variables2(Refines,AbstractModels,_EncounteredIds,AbstractVariables,[]).
378		get_all_abstract_variables2(-,_AbstractModels,EncounteredIds) -->
379		{!,empty_avl(EncounteredIds)}.
380		get_all_abstract_variables2(Name,AbstractModels,EncounteredIds) -->
381		{get_refined_model(Name,AbstractModels,Model),
382		internal_model_refines(Model,_,Refines)},
383		get_all_abstract_variables2(Refines,AbstractModels,EncounteredIdsAbs),
384		get_all_abstract_variables3(Model,EncounteredIdsAbs,EncounteredIds).
385		get_all_abstract_variables3(Model,EncounteredIdsIn,EncounteredIdsOut,
386		FoundVarsIn,FoundVarsOut) :-
387		internal_model_vars(Model,_,Vars),
388		extract_new_variables(Vars,EncounteredIdsIn,NewVars),
389		get_texpr_ids(NewVars,NewIds),
390		add_all_to_avl(NewIds,EncounteredIdsIn,EncounteredIdsOut),
391		add_all(NewVars,FoundVarsIn,FoundVarsOut).
392		add_all_to_avl([],Avl,Avl).
393		add_all_to_avl([H|T],In,Out) :-
394		avl_store(H,In,1,Inter),
395		add_all_to_avl(T,Inter,Out).
396		add_all([],L,L).
397		add_all([H|T],[H|L1],L2) :- add_all(T,L1,L2).
398		extract_new_variables([],_EncounteredIdsIn,[]).
399		extract_new_variables([Var|Vrest],EncounteredIds,NewVars) :-
400		get_texpr_id(Var,Id),
401		( avl_fetch(Id,EncounteredIds) ->
402		NewVars = NewRest
403		; otherwise ->
404		NewVars = [Var|NewRest]),
405		extract_new_variables(Vrest,EncounteredIds,NewRest).
406
407
408
409
410
411		check_events([],_ModelName,_Env,_GEnv,_InvEnv,_Dropped,_ConcreteVars,_AbstractEvents,_NewVars,_Variant,[]).
412		check_events([RawEvent|RawRest],ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,[Event|Erest]) :-
413		(check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event)
414		-> true
415		; add_failed_call_error(check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event))),
416		check_events(RawRest,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Erest).
417
418
419		check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVariables,Variant,
420		event(EvName,ModelName,Status,TParameters,TGuard,TTheorems,MActions,TVarWitnesses,TParamWitnesses,Unmodifiables,Refines)) :-
421
422		raw_event(RawEvent,_,EvName,RawStatus,Refines,Params,Guards,Theorems,Actions,Witnesses),
423		check_status(RawStatus, Variant, Status, Refines, AbstractEvents, eventlocation(ModelName,EvName)),
424		get_abstract_parameters(Refines,AbstractEvents,AbstractParameters),
425		create_identifiers(Params,[loc(ModelName,event(EvName))],TParameters),
426		split_abstract_vars(AbstractParameters,TParameters,
427		_NewParameters,DroppedParameters1),
428		annotate_dropped_parameters(DroppedParameters1,Refines,AbstractEvents,DroppedParameters),
429		conjunct_guards(Guards,Guard),
430		maplist(adapt_becomes_such,Actions,Actions1),
431		% add new parameters to the typing environments:
432		add_identifiers_to_environment(TParameters,Env,Subenv),
433		add_identifiers_to_environment(TParameters,GEnv,SubGenv),
434		add_identifiers_to_environment(TParameters,InvEnv,SubTheoremsEnv), % theorems can access dropped abstract variables; just like the invariant
435		typecheck(Guard,Subenv,pred,TGuard),
436		typecheck_l(Theorems,SubTheoremsEnv,pred,TTheorems,theorems),
437		typecheck_l(Actions1,Subenv,subst,TActions,actions),
438		check_witnesses(Witnesses,SubGenv,DroppedParameters,DroppedVars,TVarWitnesses,TParamWitnesses),
439		% add checks that some variables may not be modified, e.g
440		% if skip is refined
441		get_abstract_actions(Refines,AbstractEvents,AbstractActions),
442		~~mnf( add_modified_vars_to_actions(TActions,MActions1) ),
443		add_unmodified_assignments(AbstractActions,MActions1,ConcreteVars,MActions),
444		add_equality_check(MActions,AbstractActions,NewVariables,ConcreteVars,Unmodifiables).
445
446		% add assignments of the form x:=x if a not dropped abstract variable
447		% is modified by the abstract event, but not the dropped event
448		add_unmodified_assignments(AbstractActions,ConcreteActions,ConcreteVars,NewActions) :-
449		get_modified_vars_of_actions(AbstractActions,AbstractModified),
450		get_modified_vars_of_actions(ConcreteActions,ConcreteModified),
451		remove_all(AbstractModified,ConcreteModified,OnlyAbstractModified),
452		findall( Var,
453		( member(Id,OnlyAbstractModified), get_texpr_id(Var,Id), memberchk(Var,ConcreteVars)),
454		ToKeep),
455		( ToKeep = [] -> NewActions = ConcreteActions
456		; ToKeep = [_|_] ->
457		create_texpr(assign(ToKeep,ToKeep),subst,[],Action1),
458		add_modified_vars_to_action(Action1,Action),
459		NewActions = [Action|ConcreteActions]).
460
461		check_status(RawStatus, Variant, TConv, Refines, AbstractEvents, Location) :-
462		remove_pos(RawStatus,Status),
463		check_status2(Status, Variant, Refines, AbstractEvents, Location, Conv, Infos),
464		create_texpr(Conv, status, Infos, TConv).
465		check_status2(ordinary, _Variant, _Refines, _AbstractEvents, _Location, ordinary, []).
466		check_status2(convergent, _Variant, Refines, AbstractEvents, _Location, ordinary, [convergence_proved]) :-
467		% if the refined event is also convergent, we can (or must because the
468		% variant may be missing in the refinement) omit the check for decreasing the
469		% variant. We do this by treating the event as ordinary.
470		convergence_ensured_by_abstract_event(Refines, AbstractEvents),!.
471		check_status2(convergent, Variant, _Refines, _AbstractEvents, Location, convergent(RVariant), [convergence_proved]) :-
472		variant_must_be_set(Variant,Location,RVariant).
473		check_status2(anticipated, Variant, _Refines, _AbstractEvents, _Location, anticipated(RVariant), []) :-
474		get_variant(Variant,RVariant).
475
476		:- use_module(tools_strings,[ajoin/2]).
477		variant_must_be_set(-,Location,RVariant) :- !,
478		Location = eventlocation(Model,Name),
479		ajoin(['No variant defined for ', Name, ' in model ', Model],Msg),
480		add_error(bmachine_eventb,Msg),
481		get_variant(-,RVariant).
482		% removed fail to allow animation
483		variant_must_be_set(V,_,V).
484
485		% get_variant(ModelVariant,Variant) checks profides a default variant (0) if
486		% the model does not have a variant
487		get_variant(-,V) :- !, create_texpr(integer(0),integer,[default_variant],V).
488		get_variant(V,V).
489
490		convergence_ensured_by_abstract_event(Refines, AbstractEvents) :-
491		% find a refined event which status is convergent
492		internal_event_status(Event,Ref,Status),
493		get_texpr_info(Status,StatusInfo),
494		member(Event, AbstractEvents),
495		member(Ref, Refines),
496		member(convergence_proved,StatusInfo),!.
497
498		annotate_dropped_parameters([],_,_,[]).
499		annotate_dropped_parameters([P|PRest],Refines,AbstractEvents,[A|ARest]) :-
500		def_get_texpr_id(P,Id),
501		add_texpr_infos(P,[droppedby(DropList)],A),
502		findall(Event, event_drops_param(Event,Refines,AbstractEvents,Id), DropList),
503		annotate_dropped_parameters(PRest,Refines,AbstractEvents,ARest).
504		event_drops_param(Event,Refines,AbstractEvents,Id) :-
505		get_texpr_id(Pattern,Id),
506		member(Event,Refines),
507		get_event_parameters(Event,AbstractEvents,AbParams),
508		member(Pattern,AbParams).
509
510		get_abstract_parameters([],_,R) :- !,R=[].
511		get_abstract_parameters([Refines|Rest],Events,Params) :- !,
512		get_event_parameters(Refines,Events,LocalParams),
513		append(LocalParams,RestParams,Params),
514		get_abstract_parameters(Rest,Events,RestParams).
515		get_abstract_parameters(Refines,_,Params) :- add_error(get_abstract_parameters,'Illegal Refines List: ',Refines),
516		Params=[].
517		get_event_parameters(Refines,Events,Params) :-
518		internal_event_params(Event,Refines,Params),
519		member(Event,Events),!.
520
521		get_abstract_actions([],_,[]).
522		get_abstract_actions([Refines|Rest],Events,Actions) :-
523		get_event_action(Refines,Events,LocalActions),
524		append(LocalActions,RestActions,Actions),
525		get_abstract_actions(Rest,Events,RestActions).
526		get_event_action(Refines,Events,Actions) :-
527		internal_event_actions(Event,Refines,Actions),
528		member(Event,Events),!.
529
530		check_witnesses([],_Env,_DroppedParams,_DroppedVars,[],[]).
531		check_witnesses([Witness|Rest],Env,DroppedParams,DroppedVars,TVarWitnesses,TParamWitnesses) :-
532		check_witness(Witness,Env,DroppedParams,DroppedVars,TWitness,WType),
533		( WType = droppedvar ->
534		TVarWitnesses = [TWitness|TWVRest],
535		TParamWitnesses = TWPRest
536		; WType = droppedparam(_DropList) ->
537		TVarWitnesses = TWVRest,
538		TParamWitnesses = [TWitness|TWPRest]),
539		check_witnesses(Rest,Env,DroppedParams,DroppedVars,TWVRest,TWPRest).
540		check_witness(witness(_Pos,RawId,Pred),Env,DroppedParams,DroppedVars,TWitness,WType) :-
541		RawId = identifier(_,WitnessId),
542		get_witness_identifier(WitnessId,DroppedParams,DroppedVars,TId,Info,WType),
543		get_texpr_type(TId,Type),
544		env_store(WitnessId,Type,Info,Env,Subenv),
545		typecheck(Pred,Subenv,pred,TPred),
546		create_texpr(witness(TId,TPred),witness,[],TWitness).
547		get_witness_identifier(PrimedId,_DroppedParams,DroppedVars,TPrimeId,[],droppedvar) :-
548		prime_id(Id,PrimedId),
549		get_texpr_id(TId,Id),
550		member(TId,DroppedVars),!,
551		prime_variables([TId],[TPrimeId]).
552		get_witness_identifier(Id,DroppedParams,_DroppedVars,TId,Info,droppedparam(DropList)) :-
553		get_texpr_id(TId,Id),
554		member(TId,DroppedParams),!,
555		get_texpr_info(TId,Info),
556		member(droppedby(DropList),Info),!.
557
558		conjunct_guards([],truth(none)).
559		conjunct_guards([H|T],Result) :- conjunct_guards2(T,H,Result).
560		conjunct_guards2([],G,G).
561		conjunct_guards2([H|T],G,Result) :- conjunct_guards2(T,conjunct(none,G,H),Result).
562
563		/*
564		parallel_actions(Actions,Pos,Action) :-
565		( Actions = [] -> Action = skip(Pos)
566		; Actions = [S] -> Action = S
567		; otherwise -> Action = parallel(Pos,Actions)).
568		*/
569
570		% eventb becomes_such uses primed identifiers: distinguish it from normal becomes_such
571		% ast_cleanup will translate it back to becomes_such, but with $0 instead of primes (so that it conforms to classical B)
572		adapt_becomes_such(becomes_such(Pos,Ids,Pred),evb2_becomes_such(Pos,Ids,Pred)) :- !.
573		adapt_becomes_such(Subst,Subst).
574
575		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
576		% convert B project to classical B machine
577
578		:- use_module(bmachine_structure,[create_machine/2]).
579
580		convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine) :-
581		debug_println(9,'Converting to classical B'),
582		select_models(AnimationChain,Models,AnimatedModels),
583		% todo: access to private elements of bmachine_construction
584		create_machine(Main,Empty),
585		convert_event_b2(Freetypes,Ops,AnimatedModels,Contextes,AnimationChain,
586		Empty,Machine),!.
587		convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine) :-
588		add_failed_call_error(convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine)),
589		fail.
590		convert_event_b2(Freetypes,Ops,AnimatedModels,Contextes,AnimationChain) -->
591		append_to_section(freetypes,Freetypes),
592		append_to_section(operators,Ops),
593		create_constants(AnimatedModels,Contextes,AnimatedContextNames),
594		{append(AnimatedContextNames,AnimationChain,AnimatedSectionNames)},
595		create_variables(AnimatedModels,AnimatedSectionNames),
596		create_events(AnimatedModels,AnimatedSectionNames),
597		create_animated_section_info(AnimatedContextNames,AnimationChain).
598
599		create_animated_section_info(Contextes,Models) -->
600		{reverse(Models,FromAbstractToConcrete),
601		maplist(mark_as_model,FromAbstractToConcrete,MarkedModels),
602		maplist(mark_as_context,Contextes,MarkedContextes),
603		append(MarkedContextes,MarkedModels,Sections)},
604		append_to_section(meta,[animated_sections(Sections)]).
605
606		mark_as_model(Name,model(Name)).
607		mark_as_context(Name,context(Name)).
608
609		/*
610		get_operation_identifiers([],[]).
611		get_operation_identifiers([TExpr|Rest],[Id|IdRest]) :-
612		get_texpr_expr(TExpr,operation(Id,_,_,_)),
613		get_operation_identifiers(Rest,IdRest).
614		*/
615
616		create_variables(Models,AnimatedSectionNames) -->
617		{collect_model_infos(Models,AnimatedSectionNames,Variables,Invariants,Theorems)},
618		append_to_section(abstract_variables,Variables),
619		conjunct_to_section(invariant,Invariants),
620		append_to_section(assertions,Theorems).
621
622		select_contexts([],_Contexts,[]).
623		select_contexts([Name|NRest],Contexts,[Context|CRest]) :-
624		internal_context(Context,Name),
625		memberchk(Context,Contexts),
626		select_contexts(NRest,Contexts,CRest).
627
628		select_models([],_Models,[]).
629		select_models([Name|NRest],Models,[Model|MRest]) :-
630		internal_model(Model,Name), memberchk(Model,Models),
631		select_models(NRest,Models,MRest).
632
633		% collect_model_infos(Models,Variables,Invariants,Theorems):
634		% collect all variables, invariants and theorems of the given models
635		collect_model_infos([],_,[],[],[]) :- !.
636		collect_model_infos(Models,AnimatedSectionNames,Vars,Invs,Thms) :-
637		collect_model_infos2(Models,AnimatedSectionNames,AllVars,Vars1,Invs,Thms),
638		% add to every variable the information in which models
639		% it is present
640		add_var_model_occurrences(Vars1,AllVars,Vars).
641		collect_model_infos2([],_,[],[],[],[]).
642		collect_model_infos2([Model|MRest],AnimatedSectionNames,Vars,NewVars,Invs,Thms) :-
643		internal_model_vars(Model,_,LVars), append(LVars,RVars,Vars),
644		% use only newly introduced variables of a model, to prevent
645		% double declarations
646		% in case of a limited animation chain, it is important to introduce
647		% all variables for the most abstract model
648		( MRest == [] -> LNewVars = LVars
649		; otherwise -> internal_model_newvars(Model,_,LNewVars)),
650		append(LNewVars,RNewVars,NewVars),
651		internal_model_invs(Model,_,LInvs1), append_stripped_predicates(LInvs1,AnimatedSectionNames,RInvs,Invs),
652		internal_model_thms(Model,_,LThms1), append_stripped_predicates(LThms1,AnimatedSectionNames,RThms,Thms),
653		collect_model_infos2(MRest,AnimatedSectionNames,RVars,RNewVars,RInvs,RThms).
654		add_var_model_occurrences([],_,[]).
655		add_var_model_occurrences([Var|Vrest],AllVars,[MVar|Mrest]) :-
656		add_var_model_occurrence(Var,AllVars,MVar),
657		add_var_model_occurrences(Vrest,AllVars,Mrest).
658		add_var_model_occurrence(Var,AllVars,MVar) :-
659		findall(Section,
660		( find_identifier_in_list(Var,AllVars,M),
661		get_texpr_info(M,Infos),
662		member(section(Section),Infos)),
663		Sections),
664		reverse(Sections,FromAbstractToConcrete),
665		add_texpr_infos(Var,[occurrences(FromAbstractToConcrete)],MVar).
666		append_stripped_predicates(PredsIn,AnimatedSectionNames,RestPreds,Preds) :-
667		remove_linking_parts(PredsIn,AnimatedSectionNames,LPreds),
668		append(LPreds,RestPreds,Preds).
669
670		all_used_contextes(AnimatedModels,Contextes,Sees) :-
671		( AnimatedModels = [] ->
672		all_context_names(Contextes,Sees)
673		; otherwise ->
674		collect_sees(AnimatedModels,Sees)).
675		all_context_names([],[]).
676		all_context_names([Context|Crest],[Name|Nrest]) :-
677		internal_context(Context,Name),
678		all_context_names(Crest,Nrest).
679		collect_sees([],[]).
680		collect_sees([Model|MRest],Sees) :-
681		internal_model_sees(Model,_,LocalSees), append(LocalSees,RestSees,Sees),
682		collect_sees(MRest,RestSees).
683
684		create_constants(AnimatedModels,Contextes,AnimatedContextNames) -->
685		{all_used_contextes(AnimatedModels,Contextes,Sees),
686		get_constants(Sees,Contextes,DefSets,EnumSets,EnumElems,Constants,AbstractConstants,Axioms,Theorems,AnimatedContextNames)},
687		append_to_section(deferred_sets,DefSets),
688		append_to_section(enumerated_sets,EnumSets),
689		append_to_section(enumerated_elements,EnumElems),
690		append_to_section(concrete_constants,Constants),
691		append_to_section(abstract_constants,AbstractConstants),
692		conjunct_to_section(properties,Axioms),
693		append_to_section(assertions,Theorems).
694
695		get_constants(Sees,Contextes,DefSets,EnumSets,EnumElems,Constants,AbstractConstants,Axioms,Theorems,AllContextNames) :-
696		transitive_contextes(Sees,Contextes,AllContextNames),
697		select_contexts(AllContextNames,Contextes,AllContextes),
698		collect_context_infos(AllContextes,Sets,Constants1,AbstractConstants,Axioms1,Theorems),
699		enumerated_deferred_sets(Sets,Constants1,Axioms1,DefSets,Constants,Axioms,
700		EnumSets,EnumElems).
701
702		collect_context_infos([],[],[],[],[],[]).
703		collect_context_infos([context(Name,_Ex,LSets1,LCsts1,LAbsCsts1,LAxms,LThms)|Rest],Sets,Constants,AbstractConstants,Axioms,Theorems) :-
704		add_context_occurrences(LSets1,Name,LSets),
705		add_context_occurrences(LCsts1,Name,LCsts),
706		add_context_occurrences(LAbsCsts1,Name,LAbsCsts),
707		append(LSets,RSets,Sets),
708		append(LCsts,RCsts,Constants),
709		append(LAbsCsts,RAbsCsts,AbstractConstants),
710		append(LAxms,RAxms,Axioms),
711		append(LThms,RThms,Theorems),
712		collect_context_infos(Rest,RSets,RCsts,RAbsCsts,RAxms,RThms).
713		add_context_occurrences([],_,[]).
714		add_context_occurrences([Constant|Crest],Name,[CC|CCrest]) :-
715		add_texpr_infos(Constant,[occurrences([Name])],CC),
716		add_context_occurrences(Crest,Name,CCrest).
717
718
719		% merge the events and write them to a machine
720		create_events(AnimatedModels,AnimatedSectionNames) -->
721		{get_events(AnimatedModels,AnimatedSectionNames,Events,Initialisation,Promoted)},
722		append_to_section(operation_bodies,Events),
723		bmachine_construction:write_section(initialisation,Initialisation),
724		append_to_section(promoted,Promoted).
725
726		% merge the events of multiple refinement levels
727		get_events([],_,[],Initialisation,[]) :- !,
728		create_texpr(skip,subst,[],Initialisation).
729		get_events(AnimatedModels,AnimatedSectionNames,Events,Initialisation,Promoted) :-
730		get_events_to_animate(AnimatedModels,AnimEvents),
731		merge_refinement_levels(AnimEvents,AnimatedModels,AnimatedSectionNames,MergedEvents,Promoted1),
732		remove_initialisation(Promoted1,Promoted2),
733		add_op_parenthesis(Promoted2,Promoted),
734		select_initialisation(MergedEvents,PreOps,Initialisation),
735		create_operations(PreOps,Events).
736		remove_initialisation(In,Out) :-
737		get_texpr_id(Expr,'INITIALISATION'),
738		select(Expr,In,Out),!.
739		remove_initialisation(In,Out) :-
740		% add_error(check_event_b_project,'Model has no INITIALISATION'), %err msg already generated below
741		Out=In.
742		add_op_parenthesis([],[]).
743		add_op_parenthesis([Old|ORest],[New|NRest]) :-
744		def_get_texpr_id(Old,Id),
745		rename_bt(Old,[rename(Id,op(Id))],New),
746		add_op_parenthesis(ORest,NRest).
747
748		select_initialisation(In,Ops,Init) :-
749		select(eventop('INITIALISATION',Section,[],Init1,op([],[]),_),In,Ops),!,
750		add_texpr_infos(Init1,[eventb(Section)],Init).
751		select_initialisation(In,Ops,Init) :-
752		add_error(select_initialisation,'Model has no INITIALISATION'),
753		Init = b(skip,subst,[]), % replace skip by non-det assign
754		Ops=In.
755		create_operations([],[]).
756		create_operations([E|ERest],[O|ORest]) :-
757		create_operation(E,O),
758		create_operations(ERest,ORest).
759		create_operation(eventop(Name,Section,Parameters,Subst,Type,Refines),Operation) :-
760		create_texpr(identifier(op(Name)),Type,[],Id),
761		get_texpr_info(Subst,SubstInfo),
762		Mod=modifies(_),memberchk(Mod,SubstInfo),
763		Reads=reads(_),memberchk(Reads,SubstInfo),
764		( Refines == [] -> RefInfo = []
765		; otherwise -> RefInfo = [refines(Refines)]),
766		create_texpr(operation(Id,[],Parameters,Subst),Type,[eventb(Section),Mod,Reads|RefInfo],Operation).
767
768		get_events_to_animate([Model|_],Events) :- internal_model_events(Model,_,Events).
769
770		merge_refinement_levels([],_,_,[],[]).
771		merge_refinement_levels([Event|ERest],AnimModels,AnimatedSectionNames,[Merged|MRest],[Prom|PRest]) :-
772		merge_refinement_levels2(Event,AnimModels,AnimatedSectionNames,Merged,Prom),
773		merge_refinement_levels(ERest,AnimModels,AnimatedSectionNames,MRest,PRest).
774
775		merge_refinement_levels2(Event,AnimatedLevels,AnimatedSectionNames,
776		eventop(Name,Section,Parameters,Subst,OpType,Refines),Prom) :-
777		AnimatedLevels = [CurrentLevel|_Abstractions],
778		internal_model(CurrentLevel,Section),
779		internal_event_params(Event,Name,Parameters),
780		internal_event_refined(Event,Name,Refines),
781		%merge_parameters(Refines,Parameters,_Abstractions,MergedParameters),
782		merge_events_to_subst(Name,AnimatedLevels,AnimatedSectionNames,[],Subst1),
783		optimise_events(Subst1,Subst),
784		get_texpr_types(Parameters,Types),OpType = op(Types,[]),
785		create_texpr(identifier(Name),OpType,[],Prom).
786		merge_events_to_subst(Name,[CurrentLevel|Abstractions],AnimatedSectionNames,RefinedParameters,TEvent) :-
787		create_texpr(RefLevelEvent,subst,[modifies(Vars),reads(Reads)],TEvent),
788		RefLevelEvent = rlevent(Name,Section,Status,Params,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents),
789		InternalEvent = event(Name,Section,Status,AllParams,Guard,Theorems,Actions,VWitnesses1,PWitnesses1,Unmodifiables,Refines),
790		get_event_from_model(Name,CurrentLevel,InternalEvent),
791		strip_witnesses(VWitnesses1,AnimatedSectionNames,VWitnesses),
792		strip_witnesses(PWitnesses1,AnimatedSectionNames,PWitnesses),
793		remove_refined_parameters(AllParams,RefinedParameters,Params),
794		( Abstractions = [] ->
795		AbstractEvents = []
796		; otherwise ->
797		append(RefinedParameters,Params,NewRefinedParameters),
798		merge_events_to_subst_l(Refines,Abstractions,AnimatedSectionNames,NewRefinedParameters,AbstractEvents1),
799		normalise_merged_events(AbstractEvents1,AbstractEvents)),
800		collect_modified_vars(Actions,AbstractEvents,Vars),
801		collect_read_vars(AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,AbstractEvents,Reads).
802		merge_events_to_subst_l([],_,_,_,[]).
803		merge_events_to_subst_l([Name|NRest],Abstractions,AnimatedSectionNames,RefinedParameters,[TEvent|TRest]) :-
804		merge_events_to_subst(Name,Abstractions,AnimatedSectionNames,RefinedParameters,TEvent),
805		merge_events_to_subst_l(NRest,Abstractions,AnimatedSectionNames,RefinedParameters,TRest).
806
807		% removes a witness completely if the witnessed variable belongs
808		% to a refinement level that is not animated or removes part of the
809		% witness-predicate if references to not animated levels are made.
810		strip_witnesses([],_AnimatedSectionNames,[]).
811		strip_witnesses([Witness|WRest],AnimatedSectionNames,Result) :-
812		strip_witness(Witness,AnimatedSectionNames,StrippedWitness),
813		append(StrippedWitness,SWRest,Result),
814		strip_witnesses(WRest,AnimatedSectionNames,SWRest).
815		strip_witness(Witness,AnimatedSectionNames,StrippedWitness) :-
816		get_texpr_expr(Witness,witness(W,P)),
817		( abstraction_var_occures(W,AnimatedSectionNames) ->
818		% The abstract variable is not animated, skip the complete witness
819		StrippedWitness = []
820		; otherwise ->
821		conjunction_to_list(P,Preds),
822		remove_linking_parts(Preds,AnimatedSectionNames,SPreds),
823		conjunct_predicates(SPreds,SP),
824		get_texpr_type(Witness,Type),
825		get_texpr_info(Witness,Info),
826		create_texpr(witness(W,SP),Type,Info,TWitness),
827		StrippedWitness = [TWitness]).
828
829		remove_refined_parameters([],_RefinedParameters,[]).
830		remove_refined_parameters([Param|APRest],RefinedParameters,Parameters) :-
831		( find_identifier_in_list(Param,RefinedParameters,_RefParam) ->
832		Parameters = PRest
833		; otherwise ->
834		Parameters = [Param|PRest]),
835		remove_refined_parameters(APRest,RefinedParameters,PRest).
836
837		/* currently commented out :
838		merge_parameters([],Parameters,_Abstractions,Parameters).
839		merge_parameters([_|_],Parameters,[],Parameters) :- !.
840		merge_parameters([Refines|Rest],OldParameters,Abstractions,Parameters) :-
841		Abstractions = [Abstract|FurtherAbstractions],
842		get_event_from_model(Refines,Abstract,Event),
843		internal_event_params(Event,_,NewParameters),
844		internal_event_refined(Event,_,NewRefines),
845		add_unique_parameters(NewParameters,OldParameters,Parameters2),
846		merge_parameters(NewRefines,Parameters2,FurtherAbstractions,Parameters3),
847		merge_parameters(Rest,Parameters3,Abstractions,Parameters).
848		add_unique_parameters([],Parameters,Parameters).
849		add_unique_parameters([P|PRest],InParameters,OutParameters) :-
850		( find_identifier_in_list(P,InParameters,_) ->
851		!,Parameters = InParameters
852		; otherwise ->
853		Parameters = [P|InParameters]),
854		add_unique_parameters(PRest,Parameters,OutParameters).
855		*/
856
857		get_event_from_model(Name,Model,Event) :-
858		internal_model_events(Model,_,Events),
859		internal_event(Event,Name),
860		member(Event,Events),!.
861
862		collect_modified_vars(Actions,Events,Vars) :-
863		~~mnf( get_modified_vars_of_actions(Actions,M1) ),
864		append_modified_vars_of_events(Events,M2),
865		append(M1,M2,M3),sort(M3,Vars).
866		get_modified_vars_of_actions([],[]).
867		get_modified_vars_of_actions([Action|Arest],Vars) :-
868		get_modified_vars_of_action(Action,Vlocal),
869		append(Vlocal,Vrest,Vars),
870		get_modified_vars_of_actions(Arest,Vrest).
871		get_modified_vars_of_action(Action,Vars) :-
872		get_texpr_info(Action,Infos),
873		member(modifies(Vars), Infos),!.
874
875		add_modified_vars_to_actions([],[]).
876		%add_modified_vars_to_actions([TAction|ARest],MRest) :-
877		% get_texpr_expr(TAction,skip),!, % remove skip actions % for Daniel: is this better than keeping them ??
878		% add_modified_vars_to_actions(ARest,MRest).
879		add_modified_vars_to_actions([TAction|ARest],[MAction|MRest]) :-
880		(add_modified_vars_to_action(TAction,MAction) ->true
881		; add_internal_error('Call failed: ',add_modified_vars_to_action(TAction,MAction)),
882		MAction = TAction),
883		add_modified_vars_to_actions(ARest,MRest).
884		add_modified_vars_to_action(TAction,MAction) :-
885		get_lhs_ids(TAction,Vars),
886		maplist(prime_id,Vars,Primed),
887		add_texpr_infos(TAction,[assigned_after(Primed),modifies(Vars)],MAction).
888
889		get_lhs_ids(TAction,Ids) :-
890		get_lhs_tids(TAction,Vars),
891		get_texpr_ids(Vars,Ids).
892		get_lhs_tids(TAction,Vars) :-
893		get_texpr_expr(TAction,Action),
894		split_lhs_rhs(Action,Lhs,_),
895		extract_lhs_ids(Lhs,Vars).
896
897		split_lhs_rhs(skip,[],[]). % not needed as skip removed above
898		split_lhs_rhs(assign(Ids,Exprs),Ids,Exprs).
899		split_lhs_rhs(assign_single_id(Id,Expr),[Id],[Expr]).
900		split_lhs_rhs(becomes_element_of(Ids,Expr),Ids,[Expr]).
901		split_lhs_rhs(becomes_such(Ids,Pred),Ids,[Pred]).
902		split_lhs_rhs(evb2_becomes_such(Ids,Pred),Ids,[Pred]).
903		extract_lhs_ids([],[]).
904		extract_lhs_ids([TId|TRest],[Var|VRest]) :-
905		extract_lhs_id(TId,Var),
906		extract_lhs_ids(TRest,VRest).
907		extract_lhs_id(Id,Var) :-
908		get_texpr_id(Id,_),!,Var=Id.
909		extract_lhs_id(Func,Var) :-
910		get_texpr_expr(Func,function(Id,_)),
911		get_texpr_id(Id,Var).
912
913		append_modified_vars_of_events(Events,Vars) :-
914		append_modified_vars_of_events2(Events,Unsorted),
915		sort(Unsorted,Vars).
916		append_modified_vars_of_events2([],[]).
917		append_modified_vars_of_events2([TEvent|ERest],Vars) :-
918		get_modified_vars_of_event(TEvent,Local),
919		append(Local,VRest,Vars),
920		append_modified_vars_of_events2(ERest,VRest).
921		get_modified_vars_of_event(TEvent,Local) :-
922		get_texpr_info(TEvent,Info),
923		memberchk(modifies(Local),Info).
924
925		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
926		% get all the variables that are accessed in an event
927		collect_read_vars(AllParams,Guard,Theorems,Actions,VWitnesses,PWitnesses,AbstractEvents,Reads) :-
928		get_texpr_ids(AllParams,Params), % access to parameters is not reading a variable
929		find_identifier_uses(Guard,Params,GrdVars),
930		find_identifier_uses_l(Theorems,Params,ThmVars),
931		maplist(find_all_action_reads(Params),Actions,ActVars0), ord_union(ActVars0, ActVars),
932		maplist(find_all_witness_reads(Params),VWitnesses,VWitVars0), ord_union(VWitVars0,VWitVars),
933		maplist(find_all_witness_reads(Params),PWitnesses,PWitVars0), ord_union(PWitVars0,PWitVars),
934		join_abstract_reads(AbstractEvents,AbstrVars),
935		ord_union([GrdVars,ThmVars,ActVars,VWitVars,PWitVars,AbstrVars],Reads).
936		%find_all_identifiers(Ignore,Expr,Vars) :-
937		% find_identifier_uses(Expr,Ignore,Vars). % Just switch arguments to allow the use of maplist
938		find_all_action_reads(Ignore,TAction,Res) :-
939		get_texpr_expr(TAction,Action),
940		(find_action_reads2(Action,Ignore,Vars) -> Res=Vars
941		; add_internal_error('Illegal action: ',find_action_reads2(Action,Ignore,_)),Res=[]).
942		find_action_reads2(skip,_,Vars) :- Vars=[].
943		find_action_reads2(assign(_,Exprs),Ignore,Vars) :- find_identifier_uses_l(Exprs,Ignore,Vars).
944		find_action_reads2(assign_single_id(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars).
945		find_action_reads2(becomes_element_of(_,Expr),Ignore,Vars) :- find_identifier_uses(Expr,Ignore,Vars).
946		find_action_reads2(becomes_such(Ids,Pred),Ignore,Vars1) :-
947		% all references to Ids are to the state after: not a read
948		get_texpr_ids(Ids,AtomicIds),
949		append(AtomicIds,Ignore,Ignore0),sort(Ignore0,Ignore1),
950		find_identifier_uses(Pred,Ignore1,Vars),
951		prime_identifiers0(Ids,Ids0), % Ids with $0 afterwards
952		get_texpr_ids(Ids0,AtomicIds0),
953		maplist(unprime_id(AtomicIds0,AtomicIds),Vars,Vars1).
954		%find_action_reads2(evb2_becomes_such(Ids,Pred),Ignore,Vars) :-
955		% prime_variables(Ids,PIds),get_texpr_ids(PIds,Primes),
956		% append(Primes,Ignore,Ignore0),sort(Ignore0,Ignore1),
957		% find_identifier_uses(Pred,Ignore1,Vars).
958		find_all_witness_reads(Ignore,Witness,Vars) :-
959		get_texpr_expr(Witness,witness(I,P)),
960		get_texpr_id(I,Id),
961		sort([Id|Ignore],Ignore2),
962		find_identifier_uses(P,Ignore2,Vars1),
963		% a small hack to remove the primed variables that refer to the after-state
964		% without the need to put all variables in the Ingore list:
965		exclude(is_primed_id,Vars1,Vars).
966		is_primed_id(Id) :- atom_codes(Id,Codes),[Prime]="'",last(Codes,Prime).
967		join_abstract_reads([],[]) :- !.
968		join_abstract_reads(AbstractEvents,Reads) :-
969		maplist(get_read_from_info,AbstractEvents,AbsReads),
970		ord_union(AbsReads,ReadBySome),
971		maplist(get_modifies_from_info,AbstractEvents,AbsModifies),
972		ord_union(AbsModifies,ModifiedBySome),
973		ord_intersection(AbsModifies,ModifiedByAll),
974		ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll),
975		ord_union(ReadBySome,ModifiedByNotAll,Reads).
976		get_read_from_info(AbstrEvents,Reads) :-
977		get_texpr_info(AbstrEvents,Info),memberchk(reads(Reads),Info).
978		get_modifies_from_info(AbstrEvents,Modifies) :-
979		get_texpr_info(AbstrEvents,Info),memberchk(modifies(Modifies),Info).
980
981		add_equality_check(Actions,AbstractActions,NewVars,Variables,Unmodifiables) :-
982		get_modified_vars_of_actions(Actions,Modified),
983		get_modified_vars_of_actions(AbstractActions,AbstractModified),
984		unmodifiables(Modified,AbstractModified,NewVars,Variables,Unmodifiables).
985		unmodifiables([],_AbstractModified,_NewVars,_Variables,[]).
986		unmodifiables([UM|Modified],AbstractModified,NewVars,Variables,Unmodifiables) :-
987		( is_modifiable(UM,AbstractModified,NewVars) ->
988		Unmodifiables = UMrest
989		; otherwise ->
990		get_texpr_id(TUM,UM),
991		member(TUM,Variables),!,
992		Unmodifiables = [TUM|UMrest]),
993		unmodifiables(Modified,AbstractModified,NewVars,Variables,UMrest).
994		% the abstract event modifies it, so we can do it, too
995		is_modifiable(UM,AbstractModified,_NewVars) :- member(UM,AbstractModified),!.
996		% the variables is newly introduced, so we can modifiy it
997		is_modifiable(UM,_AbstractModified,NewVars) :-
998		get_texpr_id(TUM,UM), member(TUM,NewVars).
999
1000		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1001		% normalising merged events means that if two refined events A and B
1002		% change a different set of variables then the event A gets an additional
1003		% assignment of the form x:=x with x as a variable that is changed in B
1004		% but not in A.
1005		% This can happen even though merged events have the same assignments because
1006		% they again can refine events that have different assignments.
1007
1008		% None or one refined event do not have to be normalised
1009		normalise_merged_events([],[]) :- !.
1010		normalise_merged_events([E],[E]) :- !.
1011		normalise_merged_events(Events,Normalised) :-
1012		append_modified_vars_of_events(Events,AllModifiedVars),
1013		find_typed_version_in_events(AllModifiedVars,Events,TypedVars),
1014		normalise_merged_events2(Events,AllModifiedVars,TypedVars,Normalised).
1015		normalise_merged_events2([],_AllModifiedVars,_TypedVars,[]).
1016		normalise_merged_events2([Event|Erest],AllModifiedVars,TypedVars,[Normalised|Nrest]) :-
1017		normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised),
1018		normalise_merged_events2(Erest,AllModifiedVars,TypedVars,Nrest).
1019		normalise_merged_event(Event,AllModifiedVars,TypedVars,Normalised) :-
1020		get_modified_vars_of_event(Event,Modified),
1021		remove_all(AllModifiedVars,Modified,MissingVars),
1022		add_missing_assignments(MissingVars,Event,AllModifiedVars,TypedVars,Normalised).
1023		add_missing_assignments([],Event,_,_,Event) :- !.
1024		add_missing_assignments(MissingVars,TEvent,AllModifiedVars,TypedVars,Normalised) :-
1025		get_texpr_expr(TEvent,Event),
1026		get_texpr_type(TEvent,Type),
1027		get_texpr_info(TEvent,Infos),
1028		selectchk(modifies(_),Infos,RestInfos), % TO DO: also add reads Information
1029		create_texpr(NewEvent,Type,[modifies(AllModifiedVars)|RestInfos],Normalised),
1030		Event = rlevent(Name,Sec,St,Prm,Grd,Thm,Actions,VWit,PWit,Unmod,AbsEvents),
1031		NewEvent = rlevent(Name,Sec,St,Prm,Grd,Thm,NewActions,VWit,PWit,Unmod,AbsEvents),
1032		append(Actions,NewAssignments,NewActions),
1033		create_missing_assignments(MissingVars,TypedVars,NewAssignments).
1034		create_missing_assignments([],_TypedVars,[]).
1035		create_missing_assignments([MissingVar|Mrest],TypedVars,[Assign|Arest]) :-
1036		create_missing_assignment(MissingVar,TypedVars,Assign),
1037		create_missing_assignments(Mrest,TypedVars,Arest).
1038		create_missing_assignment(Var,TypedVars,Assignment) :-
1039		get_texpr_id(TId,Var),
1040		memberchk(TId,TypedVars),
1041		prime_id(Var,Primed),
1042		create_texpr(assign([TId],[TId]),subst,[assigned_after(Primed),modifies(Var)],Assignment).
1043
1044		find_typed_version_in_events([],_Events,[]).
1045		find_typed_version_in_events([Name|Nrest],Events,[Typed|Trest]) :-
1046		find_typed_version_in_events2(Name,Events,Typed),
1047		find_typed_version_in_events(Nrest,Events,Trest).
1048		find_typed_version_in_events2(Name,Events,Typed) :-
1049		get_texpr_id(Typed,Name),
1050		member(Event,Events),
1051		get_texpr_expr(Event,rlevent(_Name,_Sec,_St,_Prm,_Grd,_Thm,Actions,_VWit,_PWit,_Unmod,AbsEvents)),
1052		find_typed_version_in_events3(Name,Actions,AbsEvents,Typed),!.
1053		find_typed_version_in_events3(_Name,Actions,_AbsEvents,Typed) :-
1054		member(Action,Actions),
1055		get_lhs_tids(Action,Vars),
1056		member(Typed,Vars),!.
1057		find_typed_version_in_events3(Name,_Actions,AbsEvents,Typed) :-
1058		find_typed_version_in_events2(Name,AbsEvents,Typed).
1059
1060		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1061		% optimisation of guards:
1062		% A guard in a refinement does not need to be evaluated in in an abstract event
1063		% again. This happens quiet frequently, especially if "extends" is used.
1064		% The same applies for assignments: If in a refinement an action is performed,
1065		% we do not have to check if the same action can be performed in a more abstract
1066		% level.
1067		optimise_events(TEvent,NTEvent) :-
1068		empty_avl(Empty),
1069		optimise_events2(Empty,TEvent,NTEvent).
1070		optimise_events2(KnownElements,TEvent,NTEvent) :-
1071		create_texpr(Event,Type,Infos,TEvent),
1072		create_texpr(NewEvent,Type,Infos,NTEvent),
1073		Event = rlevent(Name,Section,Status,Params,OldGuard,OldTheorems,OldActions,
1074		VWitnesses,PWitnesses,Unmodifiables,OldAbstractEvents),
1075		NewEvent = rlevent(Name,Section,Status,Params,NewGuard,NewTheorems,NewActions,
1076		VWitnesses,PWitnesses,Unmodifiables,NewAbstractEvents),
1077		optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,KnownElements1),
1078		optimise_formulas(OldActions,KnownElements1,NewActions,NewKnownElements),
1079		maplist(optimise_events2(NewKnownElements),OldAbstractEvents,NewAbstractEvents).
1080		optimise_guards(OldGuard,OldTheorems,KnownElements,NewGuard,NewTheorems,NewKnownElements) :-
1081		conjunction_to_list(OldGuard,OldGuards),
1082		optimise_formulas(OldGuards,KnownElements,NewGuards,KnownElements1),
1083		% If no elements were removed, we just use the old guard
1084		( OldGuards=NewGuards -> OldGuard=NewGuard
1085		; otherwise -> conjunct_predicates(NewGuards,NewGuard)
1086		),
1087		optimise_formulas(OldTheorems,KnownElements1,NewTheorems,NewKnownElements).
1088		% optimise_formulas(+AllFormulas,+KnownElements,-NewFormulas,-NewNormed)
1089		% AllFormulas: A list of formulas
1090		% KnownElementes: A list of normed versions of already encountered elements
1091		% NewFormulas: A sub-list of AllFormulas which are new (not in KnownElements)
1092		% NewKnownElements: The updated list of already encountered elements
1093		% If no formulas are removed, it is guaranteed that NewFormulas=AllFormulas
1094		optimise_formulas(AllFormulas,KnownElements,NewFormulas,NewKnownElements) :-
1095		% convert formulas to a list: Formula/Normed where Normed is a normalised form
1096		maplist(add_stripped_ast,AllFormulas,AllFormNormed),
1097		% remove the already known formulas
1098		exclude(is_duplicate_formula(KnownElements),AllFormNormed,NewFormNormed),
1099		% split the list [Form/Normed] into [Form] and [Normed]
1100		maplist(unzipslash,NewFormNormed,NewFormulas1,NewNormed),
1101		( AllFormNormed = NewFormNormed -> % No formulas removed, keep everything as it is
1102		NewFormulas = AllFormulas
1103		; otherwise ->
1104		NewFormulas = NewFormulas1
1105		),
1106		foldl(add_to_known_elements,NewNormed,KnownElements,NewKnownElements).
1107		add_stripped_ast(Formula,Formula/Stripped) :-
1108		strip_and_norm_ast(Formula,Stripped).
1109		is_duplicate_formula(KnownElements,_Formula/Stripped) :-
1110		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 !
1111		unzipslash(A/B,A,B).
1112		add_to_known_elements(New,In,Out) :-
1113		avl_store(New,In,true,Out).
1114
1115		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1116		% internal event handling (just data structure)
1117		internal_event(event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref),Name).
1118		internal_event_status(event(Name,_Section,Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref),Name,Status).
1119		internal_event_params(event(Name,_Section,_Status,Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_Ref),Name,Params).
1120		internal_event_actions(event(Name,_Section,_Status,_Params,_Grd,_Thm,Act,_VWit,_PWit,_Unmod,_Ref),Name,Act).
1121		internal_event_refined(event(Name,_Section,_Status,_Params,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,Ref),Name,Ref).
1122
1123		internal_context(context(Name,_Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name).
1124		internal_context_extends(context(Name,Extends,_Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Extends).
1125		internal_context_sets(context(Name,_Extends,Sets,_Constants,_AbstractConstants,_Axioms,_Theorems),Name,Sets).
1126		internal_context_constants(context(Name,_Extends,_Sets,Constants,_AbstractConstants,_Axioms,_Theorems),Name,Constants).
1127		internal_context_abstract_constants(context(Name,_Extends,_Sets,_Constants,AbstractConstants,_Axioms,_Theorems),Name,AbstractConstants).
1128
1129		internal_model(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name).
1130		internal_model_refines(model(Name,Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Refines).
1131		internal_model_sees(model(Name,_Refines,Sees,_Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Sees).
1132		internal_model_vars(model(Name,_Refines,_Sees,Variables,_NewVariables,_Invariants,_Theorems,_Events),Name,Variables).
1133		internal_model_newvars(model(Name,_Refines,_Sees,_Variables,NewVariables,_Invariants,_Theorems,_Events),Name,NewVariables).
1134		internal_model_invs(model(Name,_Refines,_Sees,_Variables,_NewVariables,Invariants,_Theorems,_Events),Name,Invariants).
1135		internal_model_thms(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,Theorems,_Events),Name,Theorems).
1136		internal_model_events(model(Name,_Refines,_Sees,_Variables,_NewVariables,_Invariants,_Theorems,Events),Name,Events).
1137
1138		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1139		% analyse deferred sets and generate enumerated sets if possible
1140
1141
1142
1143
1144		%% :- include(bmachine_eventb_common).
1145		%% code below used to be in separate file, as there was the single-level and multi-level mode:
1146
1147
1148
1149		extract_name(event_b_model(_,Name,_Sections),Res) :- !, Res=Name.
1150		extract_name(event_b_context(_,Name,_Sections),Res) :- !, Res=Name.
1151		extract_name(MODEL,_) :- add_error(extract_name,'Could not extract model name: ',MODEL),fail.
1152
1153		extract_sections(event_b_model(_,_Name,Sections),Sections).
1154		extract_sections(event_b_context(_,_Name,Sections),Sections).
1155
1156		% topological sort
1157
1158		topological_sort(List,Sorted) :-
1159		get_dependencies(List,Dependencies),
1160		topolsort(Dependencies,[],SortedNames),
1161		get_sorted(SortedNames,List,Sorted),!.
1162		topological_sort(List,Sorted) :- add_failed_call_error(topological_sort(List,Sorted)),fail.
1163
1164		get_dependencies([],[]).
1165		get_dependencies([E|Rest],[dep(Name,Deps)|Drest]) :-
1166		extract_name(E,Name),
1167		findall(D,dependency(E,D),Deps1),
1168		sort(Deps1,Deps),
1169		get_dependencies(Rest,Drest).
1170
1171		dependency(Elem,Dependend) :-
1172		extract_sections(Elem,Sections),
1173		( rawmachine_section(extends,Sections,Extends),
1174		member(Dependend,Extends)
1175		; rawmachine_section(refines,Sections,Dependend)).
1176
1177		topolsort([],_,[]) :- !.
1178		topolsort(Deps,Fulfilled,[First|Rest]) :-
1179		select(dep(First,Before),Deps,Drest),
1180		is_sublist(Before,Fulfilled),!,
1181		sort([First|Fulfilled],NewFulfilled),
1182		topolsort(Drest,NewFulfilled,Rest).
1183		is_sublist([],_).
1184		is_sublist([H|T],[F|R]) :-
1185		( H=F -> is_sublist(T,R)
1186		; otherwise -> is_sublist([H|T],R)).
1187
1188		get_sorted([],_,[]).
1189		get_sorted([Name|Nrest],Elems,[First|Srest]) :-
1190		member(First,Elems),
1191		extract_name(First,Name),!,
1192		get_sorted(Nrest,Elems,Srest).
1193
1194		% copy&paste from bmachine_construction
1195		rawmachine_section(Elem,List,Result) :-
1196		functor(Pattern,Elem,2),
1197		arg(2,Pattern,Result),
1198		member(Pattern,List),!.
1199
1200		optional_rawmachine_section(Elem,List,Default,Result) :-
1201		( rawmachine_section(Elem,List,Result1) -> true
1202		; Result1=Default),
1203		Result1=Result.
1204
1205		% ----------------------------------------
1206
1207
1208		% older versions of the .eventb files do not have a status included
1209		raw_event(event(Pos,Name,RawRefines,Params,Guards,Actions,Witnesses),
1210		Pos,Name,ordinary(none),Refines,Params,Guards,[],Actions,Witnesses) :-
1211		(\+((RawRefines==[] ; RawRefines=[_|_]))
1212		-> add_error(b_machine_eventb,'Outdated .eventb format, ignoring refines:',RawRefines),
1213		Refines = []
1214		; Refines=RawRefines).
1215		raw_event(event(Pos,Name,Status,Refines,Params,Guards,Actions,Witnesses),
1216		Pos,Name,Status,Refines,Params,Guards,[],Actions,Witnesses).
1217		raw_event(event(Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses),
1218		Pos,Name,Status,Refines,Params,Guards,Theorems,Actions,Witnesses).
1219
1220		% code common to bmachine_eventb.pl and bmachine_eventb_ml.pl
1221
1222		:- use_module(bmachine_structure,[select_section/5]).
1223		append_to_section(Section,List,Old,New) :-
1224		% todo: access to private elements of bmachine_construction
1225		select_section(Section,OldList,NewList,Old,New),
1226		append(OldList,List,NewList).
1227		conjunct_to_section(Section,Preds,Old,New) :-
1228		% todo: access to private elements of bmachine_construction
1229		select_section(Section,OldPred,NewPred,Old,New),
1230		conjunct_predicates([OldPred|Preds],NewPred).
1231
1232		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1233		% analyse Event-B deferred sets and generate enumerated sets if possible
1234
1235		enumerated_deferred_sets(Sets,Constants,Axioms,NewSets,NewConstants,NewAxioms,TSet,TElements) :-
1236		conjunct_predicates(Axioms,Axiom),
1237		conjunction_to_list(Axiom,Axiom2),
1238		enumerated_deferred_sets2(Sets,Constants,Axiom2,NewSets,NewConstants,NewAxioms,TSet,TElements).
1239
1240		enumerated_deferred_sets2([],Csts,Axioms,[],Csts,Axioms,[],[]).
1241		enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,NewSets,NewCsts,NewAxioms,[TSet|TSetRest],TElementsAll) :-
1242		% case 1: the set is an enumerated set
1243		enumerated_deferred_set(Set,Csts,Axioms,ICsts,IAxioms,TSet,TElements),!,
1244		append(TElements,TElementsRest,TElementsAll),
1245		enumerated_deferred_sets2(SetRest,ICsts,IAxioms,NewSets,NewCsts,NewAxioms,TSetRest,TElementsRest).
1246		enumerated_deferred_sets2([Set|SetRest],Csts,Axioms,[Set|NewSets],NewCsts,NewAxioms,TSets,TElements) :-
1247		% case 2: the set is a normal deferred set
1248		enumerated_deferred_sets2(SetRest,Csts,Axioms,NewSets,NewCsts,NewAxioms,TSets,TElements).
1249
1250		enumerated_deferred_set(Set,Constants,Axioms,NewConstants,NewAxioms,Set,TElements) :-
1251		%% print(checking_for_enumerated_deferred_sets(Axioms)),nl,
1252		has_enumeration_axioms(Set,Elements,Axioms,NewAxioms),
1253		%% print(found_enumerated_set(Set)),nl, %%
1254		% remove Elem1,...,ElemN from the constants
1255		remove_constants(Elements,Constants,NewConstants),
1256		% add enumerated set information to the elements
1257		get_texpr_type(Set,SType),
1258		(SType=set(global(Type)) -> true
1259		; add_error_and_fail(enumerated_deferred_set,'Unexpected Set: ',(Set:SType))),
1260		(typeset_enumerated(Elements,Type,TElements) -> true
1261		; add_error_and_fail(enumerated_deferred_set,'Could not typeset: ',(Type,Elements))).
1262
1263
1264		has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :-
1265		has_partition_axioms(Set,Elements,AxiomsIn,AxiomsOut),!.
1266		has_enumeration_axioms(Set,Elements,AxiomsIn,AxiomsOut) :-
1267		% there in an axiom Set = {Elem1,...,ElemN}
1268		select_equal_extension_set_of_ids(Set,AxiomsIn,Axioms1,ExtSet,Elements),
1269		% check if all axioms needed for an enumeration are
1270		% present, and remove them
1271		% second case: All elements of the set are mutually unequal
1272
1273		% generate the unequalities we have to check for
1274		generate_unequals(Elements,Unequals),
1275		% check if they are all in the axioms, and remove them from the axioms
1276		(all_unequals_present(Unequals,Axioms1,AxiomsOut) -> true
1277		; assert(deferred_set_eq_wo_enumeration_axioms(Set,ExtSet)),
1278		print('Deferred set with equality but *not* recognized as enumerated set: '),
1279		translate:print_bexpr(Set), print(' = '), translate:print_bexpr(ExtSet),nl,
1280		fail
1281		).
1282
1283		has_partition_axioms(Set,PartitionElements,AxiomsIn,AxiomsOut) :-
1284		% print(checking_for_enumeration_axioms(Set)),nl,
1285		% first case: A partion predicate is present with
1286		% all elements of the set as its arguments
1287		% ( e.g. partition(S,{a},{b},...) )
1288
1289		% create a pattern for the partition:
1290		get_texpr_id(Set,SetId),get_texpr_id(SetRef,SetId),
1291		create_texpr(partition(SetRef,Singletons),pred,_,Partition),
1292		% remove the partition from the axioms
1293		% print(looking_for_partition(SetId,Partition)),nl,nl,
1294		select(Partition,AxiomsIn,AxiomsOut1),
1295		%%print(found_partition(SetID,Partition)),nl,
1296		% check if all arguments are singletons and get the
1297		% singleton elements
1298		all_singletons(Singletons,PartitionElements,AxiomsOut1,AxiomsOut2,Recursive),
1299		(Recursive==true
1300		-> AxiomsOut=AxiomsIn /* then we still need the partition axioms */
1301		; AxiomsOut=AxiomsOut2).
1302		%% ,print(all_singletons(Singletons)),nl.
1303		%% print(singletons(PartitionElements)),nl,
1304		% check if all arguments and the identifiers
1305		% of the set are the same
1306		% same_elements(Elements,PartitionElements).
1307
1308
1309		% all elements of a list are singletons, the second argument
1310		% returns the list of elements without the set around it
1311		all_singletons([],[],Ax,Ax,_).
1312		all_singletons([Set|SRest],[Expr|ERest],AxiomsIn,AxiomsOut,Recursive) :-
1313		get_texpr_expr(Set,set_extension([Expr])),!,
1314		all_singletons(SRest,ERest,AxiomsIn,AxiomsOut,Recursive).
1315		all_singletons([ID1|SRest],Result,AxiomsIn,AxiomsOut,Recursive) :-
1316		ID1 = b(identifier(_ID),set(global(_)),_Info),
1317		Recursive=true,
1318		% print(trying_to_look_for_recursive_partition(_ID)),nl, %%
1319		has_enumeration_axioms(ID1,PartitionElements,AxiomsIn,AxiomsOut1),
1320		% print(recursive_partition(ID,PartitionElements)),nl,
1321		append(PartitionElements,ERest,Result),
1322		all_singletons(SRest,ERest,AxiomsOut1,AxiomsOut,_).
1323
1324		% the two lists of typed identifiers have the same identifiers
1325		%same_elements(ElemsA,ElemsB) :-
1326		% get_texpr_ids(ElemsA,IdsA),sort(IdsA,A),
1327		% get_texpr_ids(ElemsB,IdsB),sort(IdsB,B),
1328		% A=B.
1329
1330		typeset_enumerated([],_Type,[]).
1331		typeset_enumerated([Elem|Erest],Type,[TElem|Trest]) :-
1332		create_texpr(identifier(Id),global(Type),Infos,Elem),
1333		create_texpr(identifier(Id),global(Type),[enumerated_set_element|Infos],TElem),
1334		typeset_enumerated(Erest,Type,Trest).
1335
1336		remove_constants([],Cst,Cst).
1337		remove_constants([TId|Erest],In,Out) :-
1338		get_texpr_id(TId,Id),
1339		get_texpr_id(Pattern,Id),
1340		select(Pattern,In,Env),
1341		remove_constants(Erest,Env,Out).
1342
1343		% find an equality Set = {id1,...,idk}
1344		select_equal_extension_set_of_ids(Set,In,Out,Ext,Elements) :-
1345		get_texpr_id(Set,SetId),
1346		get_texpr_id(Expr,SetId),
1347		create_texpr(set_extension(Elements),_,_,Ext),
1348		create_texpr(Equal,_,_,TEqual),
1349		( Equal = equal(Expr,Ext); Equal = equal(Ext,Expr) ),
1350		select(TEqual,In,Out),!.
1351
1352		generate_unequals(Elements,Unequals) :-
1353		get_texpr_ids(Elements,Ids),
1354		findall(unequal(A,B),two_ids(Ids,A,B),Unequals).
1355		two_ids([A|Rest],A,B) :- member(B,Rest).
1356		two_ids([_|Rest],A,B) :- two_ids(Rest,A,B).
1357
1358		all_unequals_present([],Axioms,Axioms).
1359		all_unequals_present([unequal(A,B)|Rest],InAxioms,OutAxioms) :-
1360		remove_unequalities(InAxioms,A,B,IntAxioms,0,N), N>0,!, % at least one occurrence
1361		all_unequals_present(Rest,IntAxioms,OutAxioms).
1362
1363		remove_unequalities([],_,_,[],N,N).
1364		remove_unequalities([TAxiom|T],A,B,Rest,NrRemoved,R) :-
1365		get_texpr_id(AExpr,A), get_texpr_id(BExpr,B),
1366		get_texpr_expr(TAxiom,Axiom),
1367		is_unequality(Axiom,AExpr,BExpr),!, N1 is NrRemoved+1,
1368		remove_unequalities(T,A,B,Rest,N1,R).
1369		remove_unequalities([Axiom|T],A,B,[Axiom|TR],N,R) :- % not an unequality between A and B
1370		remove_unequalities(T,A,B,TR,N,R).
1371
1372		is_unequality(not_equal(A,B),A,B) :- !.
1373		is_unequality(not_equal(B,A),A,B) :- !.
1374		is_unequality(negation(TEqual),A,B) :-
1375		get_texpr_expr(TEqual,Equal),
1376		is_equality(Equal,A,B).
1377		is_equality(equal(A,B),A,B) :- !.
1378		is_equality(equal(B,A),A,B) :- !.
1379
1380		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1381		% creating a type environment with information about theories inside
1382
1383		check_extensions(Infos,Freetypes,Ops,TheoryEnv) :-
1384		findall( T, (member(T,Infos),is_eventb_additional_info(T)), Theories),
1385		default_theory_ops(InitialEnv),
1386		foldl(check_theory,Theories,FreetypesL,OpsL,InitialEnv,TheoryEnv),
1387		append(FreetypesL,Freetypes),append(OpsL,Ops).
1388		is_eventb_additional_info(Term) :-
1389		nonvar(Term),functor(Term,theory,Arity),
1390		memberchk(Arity,[3,4,5,7]).
1391		default_theory_ops(Env) :-
1392		env_empty(Empty),
1393		cond_operator(Id,Op),
1394		env_store_operator(Id,Op,Empty,Env).
1395		cond_operator('COND',bmachine_eventb:direct_definition(Params,DirectDef,[PT])) :-
1396		PT = '__IFTHENELSETYPE',
1397		TypeExpr = identifier(none,PT),
1398		Params = [argument('THEN',TypeExpr),
1399		argument('ELSE',TypeExpr),
1400		argument('IF',set_extension(none,[truth(none)]))],
1401		DirectDef = if_then_else(none,identifier(none,'IF'),
1402		identifier(none,'THEN'),identifier(none,'ELSE')).
1403		check_theory(Theory,Freetypes,Ops,Env,OutEnv) :-
1404		(check_theory2(Theory,Env,Freetypes,Ops) -> true
1405		; add_internal_error('Theory check failed:',Theory),fail),
1406		store_operator_list(Ops,Env,OutEnv).
1407		store_operator_list(Ops,Env,OutEnv) :-
1408		keys_and_values(Ops,Ids,Operators),
1409		foldl(env_store_operator,Ids,Operators,Env,OutEnv).
1410		check_theory2(theory(PT,Datatypes,OP),Env,Freetypes,Ops) :-
1411		% just to be backward-compatible to a version without axiomatic definitions
1412		check_theory2(theory(PT,Datatypes,OP,[]),Env,Freetypes,Ops).
1413		check_theory2(theory(PT,Datatypes,OP,AxDefs),Env,Freetypes,Ops) :-
1414		% just to be backward-compatible to a version without operator mapping
1415		% definitions
1416		check_theory2(theory(PT,Datatypes,OP,AxDefs,[]),Env,Freetypes,Ops).
1417		check_theory2(theory(PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,Ops) :-
1418		check_theory2(theory(unknown,unknown,PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,Ops).
1419		check_theory2(theory(_Id,_Imported,PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,AllOps) :-
1420		extract_freetypes(Env,Datatypes,Freetypes,FreetypeOps),
1421		(Mappings=none -> ML=[] ; ML=Mappings), % some older .eventb files seem to have none here, e.g., Theory/SumProduct_m1_mch.eventb
1422		foldl(handle_mappings(PT),ML,MappedOpsL,OP/AxDefs,OP1/AxDefs1),
1423		append(MappedOpsL,MappedOps),
1424		maplist(store_operator(PT),OP1,DefinedOps),
1425		maplist(store_axiomatic_operator(PT),AxDefs1,AxOpsL),
1426		append(AxOpsL,AxOps),
1427		append([FreetypeOps,MappedOps,DefinedOps,AxOps],AllOps1),
1428		% The operators are used for call-backs, a module prefix is mandatory
1429		maplist(prefix_with_module,AllOps1,AllOps).
1430		prefix_with_module(Id-Op,Id-(bmachine_eventb:Op)).
1431
1432		store_operator(PT,operator(Id,Parameters,_WD,DirectDef,RecursiveDef),Id-Op) :-
1433		store_operator2(DirectDef,RecursiveDef,Parameters,PT,Op).
1434		store_operator2(_,RecursiveDef,Parameters,PT,Op) :-
1435		RecursiveDef=[_|_],!,Op=recursive_operator(Parameters,RecursiveDef,PT).
1436		store_operator2([Def],_,Parameters,PT,Op) :- !,
1437		Op=direct_definition(Parameters,Def,PT).
1438		store_operator2(_,_,_,_,Op) :-
1439		Op = unsupported_operator('Operators without direct definition are currently unsupported').
1440
1441		extract_freetypes(ParamEnv,DataTypes,Freetypes,FreetypeOps) :-
1442		maplist(extract_freetype(DataTypes,ParamEnv),DataTypes,Freetypes,FreetypeOpsL),
1443		append(FreetypeOpsL,FreetypeOps).
1444		extract_freetype(AllDataTypes,Env,
1445		datatype(Id,TypeParams,Constructors),
1446		freetype(FreetypeId,Cases),
1447		[Id-freetype_operator(FreetypeId,Types,TypeParams,Usage)|CaseOps]) :-
1448		foldl(add_datatype_to_env,AllDataTypes,Env,Env1),
1449		foldl(add_type_parameter,TypeParams,Types,Env1,ParamEnv),
1450		create_freetype_typeid(Id,Types,FreetypeId),
1451		Type = freetype(FreetypeId),
1452		extract_used_type_parameters(Constructors,TypeParams,Usage),
1453		store_eventb_operator(Id,freetype_operator_as_identifier(Id),ParamEnv,ParamEnv2),
1454		maplist(extract_case(ParamEnv2,Type,Types),Constructors,Cases,CaseOpsL),
1455		append(CaseOpsL,CaseOps).
1456		add_datatype_to_env(datatype(Id,Params,_),In,Out) :-
1457		length(Params,NumberOfParams),
1458		functor(FreetypeId,Id,NumberOfParams),
1459		env_store(Id,set(freetype(FreetypeId)),[],In,Out).
1460		add_type_parameter(TypeParam,Type,In,Out) :-
1461		extract_id(TypeParam,ParameterId),
1462		env_store(ParameterId,set(Type),[],In,Out).
1463		extract_id(identifier(_,Id),Id).
1464		% constructor without parameters
1465		extract_case(_ParamEnv,freetype(TypeId),_Types, constructor(Id,[]),
1466		case(Id,constant([Id])),Ops) :- !,
1467		Ops=[Id-constructor_operator(TypeId,[])].
1468		% constructor with parameters
1469		extract_case(ParamEnv,Freetype,ParamTypes,constructor(Id,Destructors),
1470		case(Id,Type),
1471		[Id-constructor_operator(FreetypeId,Types)|DestructOps]) :-
1472		maplist(extract_destructor(ParamEnv,Freetype,ParamTypes,Id,Type),
1473		Destructors,Projections,TypesAndOps),
1474		maplist(split_type_and_op,TypesAndOps,Types,DestructOps),
1475		Freetype=freetype(FreetypeId),
1476		combine_typelist_with_prj(Types,Type,Projections).
1477		extract_destructor(Env,freetype(FreetypeId),ParamTypes,Case,CType,
1478		destructor(Name,TypeExpr),Projection,Type-Name-Op) :-
1479		typecheck_with_freevars(TypeExpr,Env,ParamTypes,set(Type),_),
1480		Op = destructor_operator(FreetypeId,Projection,Case,CType).
1481		split_type_and_op(Type-Name-Op,Type,Name-Op).
1482
1483		create_freetype_typeid(Id,Types,FreetypeId) :-
1484		FreetypeId =.. [Id|Types].
1485
1486		:- assert_must_succeed(( combine_typelist_with_prj([a,b],T,P),
1487		T == couple(a,b), P == [[prj1],[prj2]] )).
1488		:- assert_must_succeed(( combine_typelist_with_prj([a,b,c],T,P),
1489		T == couple(a,couple(b,c)),
1490		P == [[prj1],[prj2,prj1],[prj2,prj2]] )).
1491		:- assert_must_succeed(( combine_typelist_with_prj([a,b,c,d],T,P),
1492		T == couple(couple(a,b),couple(c,d)),
1493		P == [[prj1,prj1],[prj1,prj2],[prj2,prj1],[prj2,prj2]] )).
1494		combine_typelist_with_prj([T],R,Projections) :- !,R=T,Projections=[[]].
1495		combine_typelist_with_prj(Types,couple(TypeL,TypeR),Projections) :-
1496		split_list_in_middle(Types,TypesLeft,TypesRight),
1497		same_length(TypesLeft,PrjLeft),same_length(TypesRight,PrjRight),
1498		append(PrjLeft,PrjRight,Projections),
1499		maplist(cons(prj1),PrjLeft1,PrjLeft),
1500		maplist(cons(prj2),PrjRight1,PrjRight),
1501		combine_typelist_with_prj(TypesLeft,TypeL,PrjLeft1),
1502		combine_typelist_with_prj(TypesRight,TypeR,PrjRight1).
1503		split_list_in_middle(List,Left,Right) :-
1504		length(List,N),
1505		Half is floor(N / 2),
1506		append_length(Left,Right,List,Half).
1507
1508		combine_exprlist_to_couple([T],R) :- !,T=R.
1509		combine_exprlist_to_couple(Exprs,R) :-
1510		split_list_in_middle(Exprs,ExprsLeft,ExprsRight),
1511		combine_exprlist_to_couple(ExprsLeft,TL),
1512		combine_exprlist_to_couple(ExprsRight,TR),
1513		get_texpr_types([TL,TR],[TypeL,TypeR]),
1514		create_texpr(couple(TL,TR),couple(TypeL,TypeR),[],R).
1515
1516		combine_exprlist_to_cprod([T],R) :- !,T=R.
1517		combine_exprlist_to_cprod(Exprs,R) :-
1518		split_list_in_middle(Exprs,ExprsLeft,ExprsRight),
1519		combine_exprlist_to_cprod(ExprsLeft,TL),
1520		combine_exprlist_to_cprod(ExprsRight,TR),
1521		get_texpr_types([TL,TR],[set(TypeL),set(TypeR)]),
1522		create_texpr(cartesian_product(TL,TR),set(couple(TypeL,TypeR)),[],R).
1523
1524		extract_used_type_parameters(Constructors,TypeParams,Usages) :-
1525		maplist(extract_id,TypeParams,TypeParamIds),
1526		convlist(used_type_parameters_of_constructor(TypeParamIds),Constructors,Usages).
1527		used_type_parameters_of_constructor(TypeParamIds,constructor(Id,Destructors),
1528		used_param_types(Id,UsedParamTypes,DestructorExprs)) :-
1529		maplist(destructor_expr,Destructors,DestructorExprs),
1530		maplist(used_type_parameters_of_destructor(TypeParamIds),
1531		DestructorExprs,UsedParamTypeL),
1532		UsedParamTypeL = [_|_], % store the information only for constructors that actually use
1533		% type parameters
1534		ord_union(UsedParamTypeL,UsedParamTypes).
1535		used_type_parameters_of_destructor(TypeParamIds,TypeExpr,UsedTypes) :-
1536		extract_raw_identifiers(TypeExpr,UsedIds),
1537		findall( N, (nth1(N,TypeParamIds,T),memberchk(T,UsedIds)), UsedTypes1),
1538		sort(UsedTypes1,UsedTypes).
1539		destructor_expr(destructor(_,Expr),Expr).
1540		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1541		% callback predicates for operators
1542
1543		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1544
1545		:- public unsupported_operator/9.
1546		unsupported_operator(Msg,Id,_Args,Pos,_Env,ExPr,Result,TRin,TRout) :-
1547		store_typecheck_error(Msg,Pos,TRin,TRout),
1548		failure_syntax_element(ExPr,Id,F,Type), % just to make sure that the result
1549		create_texpr(F,Type,[],Result). % is nonvar, to prevent later errors
1550		failure_syntax_element(expr,Id,identifier(Id),_).
1551		failure_syntax_element(pred,_Id,falsity,pred).
1552
1553		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1554
1555		:- use_module(prozsrc(z_tools),[create_z_let/6]).
1556
1557		% Theory plug-in: direct definitions
1558		:- public direct_definition/11.
1559		direct_definition(Params, % e.g. [argument(a,bool_set(none))]
1560		DirectDef, % Raw AST of DirectDefinition Body, e.g., convert_bool(none,negation(none,equal(none,identifier(none,a),boolean_true(none))))
1561		PT, _Id, TArgs, Pos,
1562		Env, % environment of operators
1563		ExPr,Result,TRin,TRout) :-
1564		(Params,DirectDef) = (NewParams,NewDirectDefBody), %gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody),
1565		apply_direct_definition(TArgs,NewParams,NewDirectDefBody,PT,Env,Pos,TLetIds,TLetValues,TDef,TRin,TRout),
1566		create_z_let(ExPr,TLetIds,TLetValues,TDef,[],Result).
1567
1568		% Example: ddef([argument(R,pow_subset(none,identifier(none,T)))],seq(none,identifier(none,R)),[T],seq)
1569
1570		% this code not needed as we now systematically rename in create_z_let
1571		%:- use_module(input_syntax_tree,[raw_replace/3]).
1572		%gen_fresh_params(Params,DirectDef,NewParams,NewDirectDefBody) :-
1573		% maplist(alpha_rename,Params,NewParams,RenameList), %print(replaces(RenameList)),nl,
1574		% raw_replace(DirectDef,RenameList,NewDirectDefBody).
1575		%:- use_module(gensym,[gensym/2]).
1576		%alpha_rename(argument(OldID,Type),argument(FreshID,Type),replace(OldID,identifier(none,FreshID))) :-
1577		% gensym(OldID,FreshID).
1578
1579		% Args are the arguments of the operator where it is used
1580		% Params are the parameters in the operator definition
1581		:- public apply_direct_definition/11.
1582		apply_direct_definition(TArgs,Params,DirectDef,PT,Env,_Pos,
1583		TLetIds,TLetValues,TDef,TRin,TRout) :-
1584		same_length(TArgs,Params),!,
1585		maplist(create_typed_id,PT,ParametricTypes,TPT),
1586		add_identifiers_to_environment(TPT,Env,SubEnv),
1587		% type check the arguments given in the operator usage
1588		get_texpr_types(TArgs,ArgTypes),
1589		typecheck_arguments(Params,SubEnv,ArgTypes,TParams,TRin,TR2),
1590		% type check the direct definition of the operator. To do this we need the parameters of the operators
1591		% in the type environment. Their type is determined by the arguments of the operator call.
1592		add_identifiers_to_environment(TParams,SubEnv,DefEnv),
1593		btype(apply_direct_definition,DirectDef,DefEnv,_Type,TDef,TR2,TRout),
1594		append(TParams,TPT,TLetIds),
1595		maplist(create_typeset,ParametricTypes,TypeValues),
1596		append(TArgs,TypeValues,TLetValues).
1597		apply_direct_definition(_TArgs,_Arguments,_DirectDef,_PT,_Env,Pos,
1598		_TParams,_,_TDef,TRin,TRout) :-
1599		store_typecheck_error('Wrong number of operator arguments',Pos,TRin,TRout).
1600
1601		split_arg_and_typedef(argument(Id,TypeExpr),Id,TypeExpr).
1602		map_to_set_type(Type,set(Type)).
1603		typecheck_arguments(Params,Env,ArgTypes,TParams,TRin,TRout) :-
1604		% type check the parameters' type expressions of the operator definition, they should have the same type
1605		% as the arguments (except being a set)
1606		% E.g. an operator "o" has one argument "arg" and type expression "T**BOOL" (with T being a parameter type of the theory),
1607		% then for "o(5|->TRUE)" we have "couple(integer,boolean)" as the argument's type,
1608		% we add "T" to the type environment (with type set(_)),
1609		% then we type check the parameter expression "T**BOOL", expecting the type set(coule(integer,boolean)),
1610		% the type check results in T being of type set(integer).
1611		maplist(split_arg_and_typedef,Params,ParamIds,ParamTypeExprs),
1612		same_length(Params,ArgTypes),
1613		maplist(map_to_set_type,ArgTypes,SetArgTypes),
1614		btype_l(ParamTypeExprs,Env,SetArgTypes,_TParamTypeExprs,TRin,TRout),
1615		maplist(create_typed_id,ParamIds,ArgTypes,TParams).
1616		create_typeset(Type,TExpr) :- create_texpr(typeset,Type,[],TExpr).
1617
1618
1619
1620		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1621		:- public choose_operator/8.
1622		% Theory plug-in: CHOOSE operator
1623		% Maybe the use of the direct_definition operator would be possible but it turned out
1624		% that constructing the necessary parameters was quite tricky.
1625		choose_operator(Id,[TArg],Pos,_Env,ExPr,Result,TRin,TRout) :- !,
1626		( get_texpr_type(TArg,set(Type)) ->
1627		create_texpr(external_function_call('CHOOSE',[TArg]),Type,[],Result),
1628		TRin = TRout
1629		; otherwise ->
1630		failure_syntax_element(ExPr,Id,Expression,Type),
1631		create_texpr(Expression,Type,[],Result), % just to avoid free variables in the AST
1632		store_typecheck_error('Expected set for choose operator argument',Pos,TRin,TRout)
1633		).
1634		choose_operator(_Id,_TArgs,Pos,_Env,_ExPr,_Result,TRin,TRout) :-
1635		store_typecheck_error('Wrong number of operator arguments',Pos,TRin,TRout).
1636
1637
1638		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1639		% Theory plug-in: Recursive operators
1640		:- public recursive_operator/11.
1641		recursive_operator(Arguments,Cases,PT,
1642		Id,TArgs,_Pos,Env,ExPr,Result,TRin,TRout) :-
1643		% parameter types
1644		maplist(create_typed_id,PT,ParametricTypes,TPT),
1645		add_identifiers_to_environment(TPT,Env,Env1),
1646		maplist(create_typeset,ParametricTypes,LetValues), % needed for the LET
1647		typecheck_arguments(Arguments,Env1,ArgTypes,TParamIds,TRin,TR1),
1648		% TArgs: A,B,Cf
1649		% TArg: A|->B|->C
1650		get_texpr_types(TArgs,ArgTypes),
1651		create_couple(TArgs,TArg),
1652		length(TArgs,NumberOfArgs),OpInfo = [theory_operator(Id,NumberOfArgs)],
1653		unique_id("opresult.",ResultId),create_typed_id(ResultId,Type,TResultId),
1654		( ExPr=expr -> % Result: Comp(x|->y|->z)
1655		% we need to append a result parameter in the comprehension set
1656		create_texpr(function(TCompSet,TArg),Type,OpInfo,InnerResult),
1657		append(TParamIds,[TResultId],CompSetIds),append(ArgTypes,[Type],CompSetTypes),
1658		% make sure that we do not run into an infinite loop
1659		store_eventb_operator(Id,freetype_operator_as_function(RecId,Type),Env1,Env2)
1660		; ExPr=pred -> % Result: x|->y|->z : Comp
1661		create_texpr(member(TArg,TCompSet),pred,OpInfo,InnerResult),
1662		CompSetIds = TParamIds,ArgTypes=CompSetTypes,
1663		% make sure that we do not run into an infinite loop
1664		store_eventb_operator(Id,freetype_operator_as_set(RecId),Env1,Env2)
1665		),
1666		couplise_list(CompSetTypes,CompSetType),
1667		% Comp: {i,r| Cond}
1668		create_recursive_compset(CompSetIds,Cond,set(CompSetType),[],RecId,TCompSet),
1669		% Params: a,b,c
1670		% i = a|->b|->c
1671		add_identifiers_to_environment(TParamIds,Env2,Subenv),
1672		foldl(recursive_operator_case(Subenv,TResultId),Cases,TCases,TR1,TRout),
1673		conjunct_predicates(TCases,Cond),
1674		create_z_let(ExPr,TPT,LetValues,InnerResult,OpInfo,Result).
1675
1676
1677		recursive_operator_case(Env,TResultId,case(ParamId,_,Expression,Formula),Cond,TRin,TRout) :-
1678		% Add free identifiers of case to environment
1679		extract_free_identifiers(Expression,TFreeIdentifiers,Env,Subenv),
1680		% IsCase => CaseCheck
1681		create_texpr(implication(IsCase,TCaseCheck),pred,[],Cond),
1682		% IsCase: ParamId = constructor(x,y,z)
1683		typecheck_parameter(ParamId,Env,TParamId),
1684		recop_create_is_case(Expression,Subenv,IsCase,TParamId,FT,Case,TRin,TR1),
1685		% CaseCheck: #x,y,z | Destruction & Predicate
1686		recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,TCaseCheck,TR1,TRout).
1687		extract_free_identifiers(typeof(_Pos,ExtExpr,_TypeExpr),TIds,In,Out) :-
1688		extract_free_identifiers(ExtExpr,TIds,In,Out).
1689		extract_free_identifiers(extended_expr(_Pos,_Case,Exprs,Preds),TIds,In,Out) :-
1690		append(Exprs,Preds,Ids),
1691		maplist(extract_free_identifier,Ids,TIds),
1692		add_identifiers_to_environment(TIds,In,Out).
1693		extract_free_identifier(identifier(_Pos,Id),TId) :-
1694		create_typed_id(Id,_,TId).
1695		typecheck_parameter(ParamId,Env,TParamId) :-
1696		env_lookup_type(ParamId,Env,ParamType),
1697		create_typed_id(ParamId,ParamType,TParamId).
1698		%env_store_type(Id,Type,In,Out) :-
1699		% % Version without Info field
1700		% env_store(Id,Type,[],In,Out).
1701		recop_create_is_case(typeof(_,Expr,_TypeExpr),Env,IsCase,TParamId,FT,Case,TRin,TRout) :-
1702		recop_create_is_case(Expr,Env,IsCase,TParamId,FT,Case,TRin,TRout).
1703		recop_create_is_case(Expression,Env,IsCase,TParamId,FT,Case,TRin,TRout) :-
1704		Expression = extended_expr(_,Case,_,_),
1705		get_texpr_type(TParamId,freetype(FT)),
1706		btype(recop_create_is_case,Expression,Env,freetype(FT),_TCons,TRin,TRout),
1707		create_texpr(freetype_case(FT,Case,TParamId),pred,[],IsCase).
1708		recop_create_in_case(Formula,TParamId,TResultId,Subenv,TFreeIdentifiers,FT,Case,Cond,TRin,TRout) :-
1709		% Predicate
1710		btype(recop_create_in_case,Formula,Subenv,Type,TFormula,TRin,TRout),
1711		( Type=pred -> Predicate = TFormula
1712		; otherwise ->
1713		get_texpr_types([TResultId,TFormula],[TypeA,TypeB]),
1714		unify_types_strict(TypeA,TypeB),
1715		create_texpr(equal(TResultId,TFormula),pred,[],Predicate)),
1716		% Destruction: x->y|->z = destructor(ParamId)
1717		( TFreeIdentifiers = [] ->
1718		Cond = Predicate
1719		; TFreeIdentifiers = [_|_] ->
1720		get_texpr_types(TFreeIdentifiers,FTypes),
1721		combine_typelist_with_prj(FTypes,FType,Projections),
1722		unique_id("destructed",DId),create_typed_id(DId,FType,TDId),
1723		create_texpr(freetype_destructor(FT,Case,TParamId),FType,[],Destructor),
1724		maplist(create_inner_let(TDId),Projections,TLetExpressions),
1725		create_z_let(pred,TFreeIdentifiers,TLetExpressions,Predicate,[],InnerLets),
1726		create_z_let(pred,[TDId], [Destructor], InnerLets,[],Cond)
1727		).
1728
1729		create_inner_let(TOrig,Projections,TExpr) :-
1730		apply_projections(Projections,TOrig,TExpr).
1731
1732		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1733		% Theory plug-in: datatype sets
1734		:- public freetype_operator/12.
1735		freetype_operator(FreetypeId1,Types1,TypeParams1,Usage1,
1736		Id,TArgs,_Pos,Env,_ExPr,Result,TR,TR) :-
1737		% make a fresh copy to prevent that several instances of the freetype propagate
1738		% their types to each other (resulting in spurious typing errors)
1739		copy_term(freetype(FreetypeId1,Types1,TypeParams1,Usage1),
1740		freetype(FreetypeId, Types, TypeParams, Usage)),
1741		maplist(map_to_set_type,Types,SetTypes),
1742		get_texpr_types(TArgs,SetTypes),
1743		create_freetype_compset(TArgs,Id,FreetypeId,TypeParams,Usage,Env,Result).
1744		create_freetype_compset(TArgs,SetId,FreetypeId,TypeParams,Usage,Env,Result) :-
1745		find_constructors_with_complex_types(TArgs,Usage,Constructors),
1746		( Constructors = [] ->
1747		create_texpr(freetype_set(FreetypeId),set(freetype(FreetypeId)),[],Result)
1748		; otherwise ->
1749		create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result)).
1750		create_freetype_compset2(TArgs,SetId,Constructors,FreetypeId,TypeParams,Env,Result) :-
1751		btypechecker:add_ext_variables(TypeParams,Env,TParams,Subenv,TRin,TRout),
1752		get_texpr_types(TParams,Types),get_texpr_types(TArgs,Types),
1753		Type=freetype(FreetypeId),
1754		create_texpr(identifier(freetype_element),Type,[],TId),
1755		do_prettyprint_freetype(FreetypeId,TArgs,PP),
1756		create_recursive_compset([TId],Let,set(Type),[freetype(PP)],RecId,Result),
1757		store_eventb_operator(SetId,freetype_operator_as_identifier(RecId),Subenv,Subenv2),
1758		foldl(create_cons_check(FreetypeId,Subenv2,TId),Constructors,Checks,TRin,TRout),
1759		conjunct_predicates(Checks,Cond),
1760		create_z_let(pred,TParams,TArgs,Cond,[],Let).
1761		create_cons_check(FreetypeId,Env,TId,cons(Case,Exprs),Check,TRin,TRout) :-
1762		btype_l(Exprs,Env,_Types,TExprs,TRin,TRout),
1763		combine_exprlist_to_cprod(TExprs,Set),
1764		get_texpr_type(Set,set(Type)),
1765		create_texpr(freetype_case(FreetypeId,Case,TId),pred,[],CheckCase),
1766		create_texpr(freetype_destructor(FreetypeId,Case,TId),Type,[],Value),
1767		create_texpr(member(Value,Set),pred,[],Membercheck),
1768		create_texpr(implication(CheckCase,Membercheck),pred,[],Check).
1769		% this is used to pretty-print the resulting comprehension set
1770		do_prettyprint_freetype(Id,Params,R) :-
1771		maplist(translate_bexpression,Params,Strs),
1772		ajoin_with_sep(Strs,',',S),
1773		functor(Id,I,_),
1774		ajoin([I,'(',S,')'],R).
1775
1776		find_constructors_with_complex_types(TArgs,Usage,Constructors) :-
1777		find_complex_type_params(TArgs,ComplexTP),
1778		findall(cons(Id,DestructorExprs),
1779		( member(used_param_types(Id,UsedParamTypes,DestructorExprs),Usage),
1780		ord_intersect(UsedParamTypes,ComplexTP)),
1781		Constructors).
1782		% returns the indeces of the type arguments that are not only types
1783		find_complex_type_params(TArgs,ComplexTP) :-
1784		findall(N,(nth1(N,TArgs,TArg),\+ is_just_type(TArg)),ComplexTP1),
1785		sort(ComplexTP1,ComplexTP).
1786
1787		:- public freetype_operator_as_identifier/9.
1788		freetype_operator_as_identifier(RecId,Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
1789		get_texpr_types(TArgs,SetTypes),
1790		maplist(map_to_set_type,Types,SetTypes),
1791		create_freetype_typeid(Id,Types,FreetypeId),
1792		create_recursion_ref(RecId,set(freetype(FreetypeId)),Result).
1793
1794		:- public freetype_operator_as_function/10.
1795		freetype_operator_as_function(RecId,RType,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
1796		create_couple(TArgs,TArg), get_texpr_type(TArg,Type),
1797		create_recursion_ref(RecId,set(couple(Type,RType)),TFunction),
1798		create_texpr(function(TFunction,TArg),RType,[],Result).
1799
1800		:- public freetype_operator_as_set/9.
1801		freetype_operator_as_set(RecId,_Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
1802		create_couple(TArgs,TArg), get_texpr_type(TArg,Type),
1803		create_recursion_ref(RecId,set(Type),TSet),
1804		create_texpr(member(TArg,TSet),pred,[],Result).
1805
1806		create_recursion_ref(RecId,Type,TId) :-
1807		create_texpr(identifier(RecId),Type,[for_recursion],TId).
1808
1809		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1810		% Theory plug-in: datatype constructors
1811		:- public constructor_operator/10. % TO DO: ensure by another mechanism that Spider detects that this is called
1812		constructor_operator(FreetypeId1,[],Id,[],_Pos,_Env,_ExPr,Result,TRin,TRout) :-
1813		!, copy_term(FreetypeId1,FreetypeId),
1814		create_texpr(value(freeval(FreetypeId,Id,term(Id))),
1815		freetype(FreetypeId),[],Result),
1816		TRin = TRout.
1817		constructor_operator(FreetypeId1,ParamTypes1,
1818		Id,TArgs,_Pos,_Env,_ExPr,Result,TR,TR) :-
1819		copy_term(constructor(FreetypeId1,ParamTypes1),constructor(FreetypeId,ParamTypes)),
1820		get_texpr_types(TArgs,ParamTypes),
1821		combine_exprlist_to_couple(TArgs,TArg),
1822		create_texpr(freetype_constructor(FreetypeId,Id,TArg),freetype(FreetypeId),[],Result).
1823
1824		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1825		% Theory plug-in: datatype destructors
1826		:- public destructor_operator/12. % TO DO: ensure by another mechanism that Spider detects that this is called
1827		destructor_operator(FreetypeId1,Projections,Case,CType1,
1828		_Id,[TArg],_Pos,_Env,_ExPr,Result,TR,TR) :-
1829		copy_term(destructor(FreetypeId1,CType1),destructor(FreetypeId,CType)),
1830		get_texpr_type(TArg,freetype(FreetypeId)),
1831		create_texpr(freetype_destructor(FreetypeId,Case,TArg),CType,[],Destructed),
1832		apply_projections(Projections,Destructed,Result).
1833
1834		% create an projection expression (or a combination of arbitrary many) to
1835		% access a part of a couple. The input is a list of prj1/prj2 atoms,
1836		% e.g. [prj1,prj1,prj2]: Take the first of the first of the second element.
1837		apply_projections(Projections,Expr,Result) :-
1838		reverse(Projections,Prjs),
1839		apply_projections1(Prjs,Expr,Result).
1840		apply_projections1([],Expr,Expr).
1841		apply_projections1([P|Rest],Expr,Result) :-
1842		get_texpr_type(Inner,couple(A,B)),
1843		apply_projections2(P,A,B,Result,Inner),
1844		apply_projections1(Rest,Expr,Inner).
1845		apply_projections2(prj1,A,_B,Result,Inner) :-
1846		create_texpr(first_of_pair(Inner),A,[],Result).
1847		apply_projections2(prj2,_A,B,Result,Inner) :-
1848		create_texpr(second_of_pair(Inner),B,[],Result).
1849
1850		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1851		% Theory plug-in: axiomatic definitions of operators
1852		store_axiomatic_operator(_PT,axiomatic_def_block(_Id,_Types,OpDefs,_Axioms),Ops) :-
1853		% in case we do not recognize the operator, we store an error message
1854		% that is shown as soon the operator is used somewhere
1855		maplist(store_axdef_error,OpDefs,Ops).
1856		store_axdef_error(opdef(Id,_Arguments,_WD),Id-unsupported_operator(Msg)) :-
1857		ajoin(['Axiomatic defined operator \"',Id,'\" not recognized. Be sure to add a .ptm file to your Theory project.'],Msg).
1858
1859
1860		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1861		% Theory plug-in: Tagged operators that can be replaced by internal constructs
1862		handle_mappings(PT,tag(Opname,Tag),Ops,OPin/AxDefsin,OPout/AxDefsOut) :- !,
1863		( extract_operator(Opname,Operator,OPin/AxDefsin,OPout/AxDefsOut) ->
1864		(debug:debug_mode(on) -> format("Mapping Theory Operator ~s -> ~w~n",[Tag,Opname]) ; true),
1865		(store_operator_by_tag(Tag,Opname,Operator,PT,Ops) -> true
1866		; add_internal_error('Error mapping Theory Operator (the *.ptm file maybe incorrect or you need a newer version of ProB): ',Tag:Opname))
1867		; otherwise ->
1868		ajoin(['ProB theory mapping: operator ',Opname,' not found, mapping entry ignored.'],Msg),
1869		add_error(bmachine_eventb,Msg),
1870		OPin/AxDefsin=OPout/AxDefsOut,Ops=[]
1871		).
1872		handle_mappings(_PT,Mapping,[],X,X) :-
1873		functor(Mapping,Functor,Arity),
1874		ajoin(['ProB theory mapping: unexpected entry of type ',Functor,'/',Arity,', entry ignored.'],Msg),
1875		add_error(bmachine_eventb,Msg).
1876
1877		extract_operator(Opname,Operator,OPin/AxDefs,OPout/AxDefs) :-
1878		Operator = operator(Opname,_Parameters,_WD,_DirectDef,_RecursiveDef),
1879		selectchk(Operator,OPin,OPout),!.
1880		extract_operator(Opname,Operator,OP/AxDefsIn,OP/AxDefsOut) :-
1881		Operator = axdef(Opname,Parameters,WD,block(Id,Types,Axioms)),
1882		select(axiomatic_def_block(Id,Types,OpDefsIn,Axioms),AxDefsIn,axiomatic_def_block(Id,Types,OpDefsOut,Axioms),AxDefsOut),
1883		select(opdef(Opname,Parameters,WD),OpDefsIn,OpDefsOut),!.
1884
1885		% two versions are supported: The older one expects an atom Tag, the new one a string
1886		% The string version is then parsed as a Prolog term.
1887		store_operator_by_tag(Tag,Opname,Operator,PT,Ops) :-
1888		is_list(Tag),!, % A string
1889		append(Tag,".",Tag1), % read_from_codes/2 needs a full-stop at the end
1890		read_from_codes(Tag1,Term),
1891		store_operator_by_tag(Term,Opname,Operator,PT,Ops).
1892		store_operator_by_tag(Tag,Opname,Operator,PT,Ops) :-
1893		store_operator_by_tag1(Tag,Opname,Operator,PT,Ops).
1894		store_operator_by_tag1(Tag,Opname,Operator,PT,Ops) :-
1895		% SIGMA or PI
1896		aggregation_operator(Tag,Functor),!,
1897		get_operator_parameters(Operator,Parameters),
1898		( Parameters = [Arg] ->
1899		create_raw_aggregation_op(Functor,Arg,ClassicalBOp),
1900		Ops=[Opname-direct_definition([Arg],ClassicalBOp,PT)]
1901		; otherwise ->
1902		parameter_error(Parameters,1,Opname),Ops=[]
1903		).
1904		store_operator_by_tag1(mkinat,OpName,Operator,PT,Ops) :- !,
1905		store_operator_by_tag1(mkinat(iZero,iSucc),OpName,Operator,PT,Ops).
1906		store_operator_by_tag1(mkinat(ZeroOp,SuccOp),OpName,Operator,_PT,Ops) :- !,
1907		get_operator_parameters(Operator,Parameters),
1908		( Parameters = [argument(Arg,_ArgType)] ->
1909		Ops=[OpName-make_inductive_natural(Arg,ZeroOp,SuccOp)]
1910		; otherwise ->
1911		parameter_error(Parameters,1,OpName),Ops=[]
1912		).
1913		store_operator_by_tag1(choose,OpName,Operator,_PT,Ops) :- !,
1914		get_operator_parameters(Operator,Parameters),
1915		( Parameters = [argument(_Arg,_ArgType)] ->
1916		Ops=[OpName-choose_operator]
1917		; otherwise ->
1918		parameter_error(Parameters,1,OpName),Ops=[]
1919		).
1920		store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :- unary_operator_raw_term(BOperator,Arg,Expr), !,
1921		get_operator_parameters(Operator,Parameters),
1922		( Parameters = [argument(Arg,_ArgType)] ->
1923		Ops=[Opname-direct_definition(Parameters,Expr,PT)]
1924		; otherwise ->
1925		parameter_error(Parameters,1,Opname),Ops=[]
1926		).
1927		store_operator_by_tag1(BOperator,Opname,Operator,PT,Ops) :- %print(try(BOperator,Opname,Operator,PT,Ops)),nl,
1928		binary_operator_raw_term(BOperator,Arg1,Arg2,Expr), !,
1929		get_operator_parameters(Operator,Parameters),
1930		( Parameters = [argument(Arg1,_ArgType1), argument(Arg2,_ArgType2)] ->
1931		Ops=[Opname-direct_definition(Parameters,Expr,PT)]
1932		; otherwise ->
1933		parameter_error(Parameters,1,Opname),Ops=[]
1934		).
1935
1936		% TO DO ternary operator ?? son/3
1937
1938		% construct a raw term with arguments for replacement in AST
1939		% first argument is functor name as it appears in the theory mapping file *.ptm
1940		binary_operator_raw_term(Functor,Arg1,Arg2,Term) :- binary_operator_to_ast(Functor,ASTFunctor),
1941		Term =.. [ASTFunctor,none,identifier(none,Arg1),identifier(none,Arg2)].
1942		binary_operator_to_ast('^',concat).
1943		binary_operator_to_ast(concat,concat).
1944		binary_operator_to_ast(div,floored_div).
1945		binary_operator_to_ast(restrict_front,restrict_front).
1946		binary_operator_to_ast(restrict_tail,restrict_tail).
1947		% binary tree operators
1948		binary_operator_to_ast(arity,arity).
1949		binary_operator_to_ast(bin,bin).
1950		binary_operator_to_ast(const,const).
1951		binary_operator_to_ast(father,father).
1952		binary_operator_to_ast(rank,rank).
1953		binary_operator_to_ast(subtree,subtree).
1954
1955		% construct a raw term with argument for replacement in AST
1956		% first argument is functor name as it appears in the theory mapping file *.ptm
1957		unary_operator_raw_term(Functor,Arg,Term) :- unary_operator_to_ast(Functor,ASTFunctor),
1958		Term =.. [ASTFunctor,none,identifier(none,Arg)].
1959		unary_operator_to_ast(closure,reflexive_closure). % reflexive_closure corresponds to closure B operator !
1960		unary_operator_to_ast(closure1,closure).
1961		unary_operator_to_ast(conc,general_concat).
1962		unary_operator_to_ast(fnc,trans_function).
1963		unary_operator_to_ast(rel,trans_relation).
1964		unary_operator_to_ast(succ,successor). % also exist in Event-B
1965		unary_operator_to_ast(pred,predecessor). % also exist in Event-B
1966		unary_operator_to_ast(bool,convert_bool). % also exist in Event-B
1967		unary_operator_to_ast(id,identity). % exists in similar way in Event-B
1968		unary_operator_to_ast(union,general_union).
1969		unary_operator_to_ast(inter,general_intersection).
1970		unary_operator_to_ast(F,F) :- unary_operator(F). % operators that have same name in B and AST
1971
1972		% sequence operators
1973		unary_operator(seq).
1974		unary_operator(seq1).
1975		unary_operator(iseq).
1976		unary_operator(iseq1).
1977		unary_operator(perm).
1978		unary_operator(first).
1979		unary_operator(size).
1980		unary_operator(front).
1981		unary_operator(tail).
1982		unary_operator(rev).
1983		unary_operator(last).
1984		unary_operator(mu).
1985		% tree operators
1986		unary_operator(tree).
1987		unary_operator(btree).
1988		unary_operator(top).
1989		unary_operator(sons).
1990		unary_operator(bin).
1991		unary_operator(left).
1992		unary_operator(right).
1993		unary_operator(sizet).
1994		unary_operator(prefix).
1995		unary_operator(postfix).
1996		%unary_operator(infix). % not yet supported
1997		%unary_operator(mirror). % not yet supported
1998		% general operators
1999		unary_operator(min). % also exist in Event-B
2000		unary_operator(max). % also exist in Event-B
2001		unary_operator(domain).
2002		unary_operator(range).
2003		% z operators
2004		unary_operator(compaction).
2005		unary_operator(bag_items).
2006
2007		aggregation_operator('SIGMA',general_sum).
2008		aggregation_operator('PI',general_product).
2009
2010		create_raw_aggregation_op(Op,argument(Arg,_ArgType),Result) :-
2011		% this construction will immediately wrap _agg_op1/2 inside Sigma or Pi, and thus _agg_op1/2 will not be visibile outside
2012		A = identifier(none,Arg), % User-given argument
2013		create_fresh_identifier('_agg_op1',[A],I1), % starting with _ ensures user cannot create such an id
2014		create_fresh_identifier('_agg_op2',[A],I2),
2015		I = identifier(none,I1), % I is the (not used) index variable
2016		N = identifier(none,I2), % N is the integer to sum or multiply
2017		Pred = member(none,couple(none,I,N),A), % I|->N : Arg
2018		Result =.. [Op,none,[I,N],Pred,N]. % SIGMA(I,N . I|->N:Arg | N) (or PI)
2019
2020		parameter_error(Parameters,Expected,Opname) :-
2021		length(Parameters,N),
2022		ajoin(['ProB theory mapping: Expected ',Expected,' parameter for operator ',
2023		Opname,' but found ',N],Msg),
2024		add_error(bmachine_eventb,Msg).
2025
2026		get_operator_parameters(operator(_Opname,Parameters,_WD,_DirectDef,_RecursiveDef),Parameters).
2027		get_operator_parameters(axdef(_Opname,Parameters,_WD,_Block),Parameters).
2028
2029		store_eventb_operator(Id,Op,Ein,Eout) :-
2030		env_store_operator(Id,bmachine_eventb:Op,Ein,Eout).
2031
2032
2033		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2034		% Operator for constructing inductive natural numbers
2035		:- public make_inductive_natural/11.
2036		make_inductive_natural(ArgId,ZeroOp,SuccOp,
2037		Id,[TParam],_Pos,Env,expr,Result,TRin,TRout) :-
2038		unique_id("opresult.",ResultId),
2039		create_typed_id(ResultId,NatType,TResult),
2040		create_typed_id(ArgId,integer,TArgId),
2041		% prepare environment:
2042		add_identifiers_to_environment([TArgId,TResult],Env,Env1),
2043		% we create a recursive function by using a (as recursive annotated) comprehension
2044		% set. We can refer to the compset with RecId.
2045		create_recursive_compset([TArgId,TResult],Cond,set(couple(integer,NatType)),[],RecId,TCompSet),
2046		% used for recursive call:
2047		env_store(RecId,set(couple(integer,NatType)),[],Env1,SubEnv),
2048		% just type iZero to retrieve its type:
2049		IZero=extended_expr(none,ZeroOp,[],[]),
2050		btype(make_inductive_natural,IZero,SubEnv,NatType,_,TRin,TR1),
2051		% Arg=0 => Result=iZero
2052		RawCase1=implication(none,
2053		equal(none,identifier(none,ArgId),integer(none,0)),
2054		equal(none,identifier(none,ResultId),IZero)),
2055		btype(make_inductive_natural,RawCase1,SubEnv,pred,Case1,TR1,TR2),
2056		% Arg>0 => Result=iSucc( recursive_call(Arg-1) )
2057		RawCase2=implication(none,
2058		greater(none,identifier(none,ArgId),integer(none,0)),
2059		equal(none,identifier(none,ResultId),extended_expr(none,SuccOp,[Minus1],[]))),
2060		Minus1=function(none,identifier(none,RecId),minus(none,identifier(none,ArgId),integer(none,1))),
2061		btype(make_inductive_natural,RawCase2,SubEnv,pred,Case2,TR2,TRout),
2062		% {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )}
2063		conjunct_predicates([Case1,Case2],Cond),
2064		% {Arg,Result | Arg=0=>Result=iZero & Arg>0=>Result=iSucc( RC(Arg-1) )}(TParam)
2065		create_texpr(function(TCompSet,TParam),NatType,[theory_operator(Id,1)],Result).