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).