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