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