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