1 % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(bmachine_construction,[reset_bmachine_construction/0,
6 check_machine/4,
7 type_in_machine_l/6,
8 type_open_predicate_with_quantifier/6,
9 get_constructed_machine_name/2, get_constructed_machine_name_and_filenumber/3,
10 type_open_formula/8,
11 filter_linking_invariant/3,
12 machine_promotes_operations/2,
13 external_procedure_used/1,
14 dummy_machine_name/2]).
15
16 :- use_module(module_information,[module_info/2]).
17 :- module_info(group,typechecker).
18 :- module_info(description,'This module contains the rules for loading, including, seeing, etc. B machines, scope of constants, variables, parameters, etc.').
19
20 :- use_module(library(lists)).
21 :- use_module(library(avl)).
22
23 :- use_module(self_check).
24 :- use_module(tools).
25 :- use_module(error_manager).
26 :- use_module(debug).
27 :- use_module(preferences).
28
29 :- use_module(btypechecker).
30 :- use_module(b_ast_cleanup).
31 :- use_module(bsyntaxtree).
32 :- use_module(bmachine_structure).
33 :- use_module(pragmas).
34 :- use_module(b_global_sets,[register_enumerated_sets/2]).
35
36 :- use_module(bmachine_static_checks).
37 :- use_module(tools_lists,[ord_member_nonvar_chk/2, remove_dups_keep_order/2]).
38
39 :- use_module(translate,[print_machine/1]).
40
41
42 :- set_prolog_flag(double_quotes, codes).
43
44 %maximum_type_errors(100).
45
46 :- dynamic debug_machine/0.
47
48 :- use_module(pref_definitions,[b_get_important_preferences_from_raw_machine/2]).
49 set_important_prefs_from_machine(Main,Machines) :-
50 find_machine(Main,Machines,_MType,_Header,RawMachine),
51 ? get_raw_model_type(Main,Machines,RawModelType),
52 b_get_important_preferences_from_raw_machine(RawMachine,RawModelType),
53 check_important_annotions_from_machine(RawMachine).
54
55 check_important_annotions_from_machine(RawMachine) :-
56 ? member(definitions(_Pos,Defs),RawMachine),
57 member(expression_definition(DPOS,'PROB_REQUIRED_VERSION',[],RawValue),Defs),!,
58 (RawValue = string(VPos,Version)
59 -> add_message(bmachine_construction,'Checking PROB_REQUIRED_VERSION: ',Version,VPos),
60 (check_version(Version,VPos) -> true ; true)
61 ; add_warning(bmachine_construction,'PROB_REQUIRED_VERSION must provide a version number string.','',DPOS)
62 ).
63 check_important_annotions_from_machine(_).
64
65 :- use_module(version,[compare_against_current_version/2,full_version_str/1]).
66 check_version(VersAtom,DPOS) :- atom_codes(VersAtom,Codes),
67 split_chars(Codes,".",VCNrs),
68 maplist(codes_to_number(DPOS),VCNrs,VNrs),
69 compare_against_current_version(VNrs,Result),
70 (Result = current_older
71 -> full_version_str(Cur),
72 ajoin(['This model requires at newer version of ProB than ',Cur,'. Download at least version: '],Msg),
73 add_warning(prob_too_old,Msg,VersAtom,DPOS)
74 ; true).
75
76 codes_to_number(DPOS,C,A) :-
77 catch(number_codes(A,C), error(syntax_error(_N),_),
78 (atom_codes(AA,C),
79 add_warning(bmachine_construction,'Illegal part of version number (use only numbers separated by dots): ',AA,DPOS),fail)).
80
81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
82
83 :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
84
85 % typecheck complete machines (incl. includes)
86 check_machine(MainName,MachinesMayContainGenerated,Result,FinalErrors) :-
87 clear_warnings,
88 debug_println(9,checking_machine(MainName)),
89 temporary_set_preference(perform_stricter_static_checks,true,CHNG),
90 strip_global_pragmas(MachinesMayContainGenerated,Machines,_WasGenerated), % TODO: is generated still used?
91 ? set_important_prefs_from_machine(MainName,Machines), % set important prefs before type-checking,...
92 check_main_machine_file_origin(MainName,Machines),
93 % we need to find all SEES/USES declarations, because all references
94 % refer to the same machine and that has to be included exactly once.
95 find_uses(Machines,Uses,NotIncluded,Errors,E1),
96 % if a seen/used machine was not included, we include it by constructing
97 % a dummy machine that extends the seen/used machine and the origional
98 % main machine
99 extend_not_included_uses(NotIncluded,MainName,NewMainName,Machines,IMachines),
100 % figure out the right order of machines, so that each machine is
101 % type-checked before a dependend machine is loaded
102 machine_order(IMachines,Order),
103 assert_machine_order(Order),
104 % expand (= type-check + includes) machines in the given order
105 expand_machines(Order,IMachines,Uses,[],Results1,E1,E2),
106 % until now, the initialisation section consists of a list of init(MachineName,Substitution)
107 % fold_initialisation merges those to one substitution, respecting the dependencies
108 % between the machines
109 ? maplist(fold_initialisation(Order),Results1,Results),
110 % find main machine
111 memberchk(machine(NewMainName,MainMachine),Results), %nl,print('MAIN:'),nl,print_machine(MainMachine),
112 % if the main machine has parameters, we convert them to global sets resp. constants
113 convert_parameters_to_global_sets(E2,[],MainMachine,Result1),
114 % add some additional informations about the machine
115 ? add_machine_infos(MainName,Machines,Results,Result1,Result),
116 ( debug_machine -> print_machine(Result); true),
117 %% comment in to pretty print all machines:
118 %( member(machine(Name,Mchx),Results), format('~n*** Machine ~w~n',[Name]), print_machine(Mchx),nl,fail ; true),
119 % finalize the list of errors, remove duplicates
120 sort(Errors,FinalErrors),
121 % output warnings
122 show_warnings,
123 % run static checks on the resulting machine
124 static_check_main_machine(Result),
125 reset_temporary_preference(perform_stricter_static_checks,CHNG).
126 check_machine(Main,_,Result,FinalErrors) :-
127 add_internal_error('Internal error: Checking the machine failed: ',
128 check_machine(Main,_,Result,FinalErrors)),
129 fail.
130
131 strip_global_pragmas([],[],false).
132 strip_global_pragmas([generated(POS,M)|Ms],MachinesOut,true) :- !, % @generated pragma used at top of file
133 assertz(pragmas:global_pragma(generated,POS)),
134 strip_global_pragmas([M|Ms],MachinesOut,_).
135 strip_global_pragmas([unit_alias(_,Alias,Content,M)|Ms],MachinesOut,true) :- !,
136 assertz(pragmas:global_pragma(unit_alias,[Alias|Content])),
137 strip_global_pragmas([M|Ms],MachinesOut,_).
138 strip_global_pragmas([M|Ms],[M|SMs],WasGenerated) :-
139 strip_global_pragmas(Ms,SMs,WasGenerated).
140
141 fold_initialisation(Order,machine(Name,Sections),machine(Name,NewSections)) :-
142 select_section(initialisation,List,Subst,Sections,NewSections),
143 maplist(extract_init_substitutions(List),Order,LSubstitutions),
144 append(LSubstitutions,Substitutions),
145 ? create_init_sequence(Substitutions,Subst).
146 extract_init_substitutions(Unsorted,Name,Substitutions) :-
147 convlist(unzip_init(Name),Unsorted,Substitutions). % keep inits for Name
148 unzip_init(Name,init(Name,Subst),Subst).
149 create_init_sequence([],Subst) :- create_texpr(skip,subst,[generated],Subst).
150 create_init_sequence([I],I) :- !.
151 create_init_sequence(L,Sequence) :-
152 (L = [First|_], get_texpr_info(First,AllInfos), extract_pos_infos(AllInfos,Pos) -> true ; Pos=[]),
153 % TODO: try and merge first and last position info
154 (get_preference(allow_overriding_initialisation,true),
155 override_initialisation_sequence(L,NL)
156 -> NewList=NL ; NewList=L),
157 create_texpr(sequence(NewList),subst,[initial_sequence|Pos],Sequence).
158
159 :- use_module(b_read_write_info,[get_accessed_vars/4]).
160 % override initialisation sequence, remove unnecessary earlier assignments (which may time-out, ...)
161 % in future we may inline equalities into becomes_such that, e.g., x :: S ; x := 1 --> x :: X /\ {1}
162 % currently x :: S ; x := 1 gets simplified to skip ; x := 1
163 override_initialisation_sequence(List,NewList) :-
164 append(Prefix,[Last],List),
165 Prefix = [_|_], % there are some earlier initialisation statements to simplify
166 get_accessed_vars(Last,[],LIds,Read),
167 ord_intersection(LIds,Read,RWIds),
168 (RWIds = []
169 -> true
170 ; add_warning(b_machine_construction,'Initialisation (override) statement reads written variables:',RWIds,Last)
171 ),
172 process_override(Last,Prefix, NewLast, SPrefix),
173 append(SPrefix,[NewLast],NewList).
174
175
176 process_override(b(parallel(List),subst,Info), Prefix,
177 b(parallel(NewList),subst,Info), NewPrefix) :- !,
178 l_process_override(List,Prefix,NewList,NewPrefix).
179 process_override(Subst, Prefix, NewSubst, NewPrefix) :-
180 create_after_pred(Subst,AfterPred),
181 get_accessed_vars(Subst,[],Ids,Read),
182 % write(after_pred(Ids, read(Read))),nl, translate:print_bexpr(AfterPred),nl,
183 ord_intersection(Read,Ids,RWIds),
184 (RWIds=[]
185 -> maplist(try_simplify_init_stmt(Ids,AfterPred,Keep),Prefix,NewPrefix),
186 !,
187 (Keep==merged_override_stmt
188 -> NewSubst = b(skip,subst,[was(Subst)])
189 ; NewSubst = Subst
190 )
191 ; add_warning(b_machine_construction,'Initialisation statement reads written variables:',RWIds,Subst),
192 fail % we actually have a before after predicate which may modify RWIds
193 ).
194 process_override(Subst, Prefix , Subst, Prefix) :- add_message(b_machine_construction,'Keeping: ',Subst,Subst).
195
196 l_process_override([],Prefix,[],Prefix).
197 l_process_override([H|List],Prefix,[H1|NewList],NewPrefix) :-
198 process_override(H,Prefix,H1,Prefix1),
199 l_process_override(List,Prefix1,NewList,NewPrefix).
200
201 :- use_module(library(ordsets)).
202 simplify_init_stmt(b(parallel(List),subst,I),OverrideIds,AfterPred,Keep,b(parallel(SList),subst,I)) :- !,
203 maplist(try_simplify_init_stmt(OverrideIds,AfterPred,Keep),List,SList).
204 simplify_init_stmt(Assign,OverrideIds,AfterPred,Keep,NewSubst) :-
205 get_accessed_vars(Assign,[],AssignIds,_Read),
206 (ord_subset(OverrideIds,AssignIds),
207 merge_statement(Assign,AssignIds,AfterPred,NewSubst),
208 Keep = merged_override_stmt
209 -> % we need to remove the override assign, if it is non-det.
210 add_message(b_machine_construction,'Adapting initialisation due to override: ',NewSubst,Assign)
211 ; ord_subset(AssignIds,OverrideIds)
212 % The assignment is useless, will be completely overriden
213 -> NewSubst = b(skip,subst,[was(Assign)]),
214 add_message(b_machine_construction,'Removing initialisation due to override: ',Assign,Assign),
215 Keep = keep_override_stmt
216 ).
217 % TODO: we could simplify IF-THEN-ELSE, ... and other constructs
218
219 % Note: the merging assumes the initialisation before the override assigns each overriden variable only once
220 try_simplify_init_stmt(OverrideIds,AfterPred,Keep,Stmt,NewStmt) :-
221 (simplify_init_stmt(Stmt,OverrideIds,AfterPred,Keep,N)
222 -> NewStmt=N ; NewStmt=Stmt).
223
224 merge_statement(b(Subst,subst,Info),AssignIds,AfterPred,b(NewSubst,subst,Info)) :-
225 merge_stmt_aux(Subst,AssignIds,AfterPred,NewSubst).
226
227 merge_stmt_aux(becomes_such(Ids,Pred),_AssignIds,AfterPred,becomes_such(Ids,NewPred)) :-
228 conjunct_predicates([AfterPred,Pred],NewPred).
229 merge_stmt_aux(becomes_element_of(Ids,Set),_,AfterPred2,becomes_such(Ids,NewPred)) :-
230 create_couple(Ids,Couple),
231 safe_create_texpr(member(Couple,Set),pred,AfterPred1),
232 conjunct_predicates([AfterPred1,AfterPred2],NewPred).
233
234 create_after_pred(b(Subst,subst,Info),Pred) :- create_after_pred_aux(Subst,Info,Pred).
235
236 create_after_pred_aux(assign_single_id(Id,RHS),Info,b(equal(Id,RHS),pred,Info)).
237 create_after_pred_aux(assign(LHS,RHS),_Info,Conj) :- % TODO: split assignments so that we can individually apply preds
238 maplist(create_equality,LHS,RHS,Eqs),
239 conjunct_predicates(Eqs,Conj).
240 % the following two are non-deterministic; hence we need to remove the substitutions
241 % in case we have managed to merge them into an earlier becomes_such,... (otherwise we may do a second non-det incompatible choice)
242 create_after_pred_aux(becomes_element_of(Id,Set),Info,b(member(Couple,Set),pred,Info)) :-
243 create_couple(Id,Couple).
244 create_after_pred_aux(becomes_such(_,Pred),_Info,Pred).
245
246
247 % -------------------------
248
249 add_machine_infos(MainName,Machines,CheckedMachines,Old,New) :-
250 ? get_raw_model_type(MainName,Machines,RawModelType), functor(RawModelType,ModelType,_), % argument is position
251 % model type could be machine or system (or model ?)
252 append_to_section(meta,[model_type/ModelType,hierarchy/Hierarchy,header_pos/HeaderPosList],Old,NewT),
253 get_refinement_hierarchy(MainName,Machines,Hierarchy),
254 find_machine_header_positions(Machines,HeaderPosList),
255 ? add_refined_machine(Hierarchy,CheckedMachines,NewT,New).
256 get_refinement_hierarchy(Main,Machines,[Main|Abstractions]) :-
257 ( find_refinement(Machines,Main,Abstract) ->
258 get_refinement_hierarchy(Abstract,Machines,Abstractions)
259 ;
260 Abstractions = []).
261 find_refinement([M|Rest],Name,Abstract) :-
262 ( get_constructed_machine_name(M,Name) ->
263 refines(M,Abstract)
264 ;
265 find_refinement(Rest,Name,Abstract)).
266
267 find_machine_header_positions(Machines,SRes) :-
268 Header = machine_header(Pos,_Nm,_Paras),
269 findall(Name/Pos,find_machine(Name,Machines,_Type,Header,_Sections),Res),
270 sort(Res,SRes).
271
272 :- use_module(specfile,[animation_minor_mode/1]).
273 % check whether the main machine has filenumber 1; if not something strange is going on.
274 % an example can be found in prob_examples/public_examples/B/ErrorMachines/IllegalSeesIncludes/WrongNameM1.mch
275 check_main_machine_file_origin(MainName,Machines) :-
276 ? member(M,Machines), get_machine_parameters(M,MainName,_,Position),
277 !,
278 (Position = none -> true
279 ; get_nr_name(Position,Number,Name)
280 -> (Number=1 -> true
281 ; ajoin(['Main machine name ',MainName,' overriden by machine in file ',Number,' :'],Msg),
282 add_error(bmachine_construction,Msg,Name,Position))
283 ; add_error(bmachine_construction,'Could not extract file number and name:',Position)
284 ).
285 check_main_machine_file_origin(MainName,_) :-
286 add_error(bmachine_construction,'Could not extract file number and name for main machine:',MainName).
287 get_nr_name(none,Nr,Name) :- !, Nr=1,Name=none.
288 get_nr_name(1,Nr,Name) :- !, Nr=1,Name=none. % TLA mode, animation_minor_mode(tla) not yet set and positions are numbers
289 get_nr_name(Position,Number,Name) :- extract_file_number_and_name(Position,Number,Name).
290
291 add_refined_machine([_Main,Refined|_],Machines,Old,New) :-
292 member(machine(Refined,Body),Machines),
293 append_to_section(meta,[refined_machine/Body],Old,New).
294 add_refined_machine(_,_,M,M). % not refining
295
296 convert_parameters_to_global_sets(Ein,Eout) -->
297 % extract and remove parameters and constraints
298 select_section(parameters,PP,[]),
299 select_section(internal_parameters,IP,[]),
300 {create_texpr(truth,pred,[],Truth)},
301 select_section(constraints,C,Truth),
302 % split parameters into sets and scalars
303 { split_list(is_set_parameter,PP,Sets,Scalars),
304 foldl(type_set_parameter,Sets,Ein,Eout) },
305 % put the sets to the deferred sets
306 append_to_section(deferred_sets,Sets),
307 % and the scalars to the constants
308 append_to_section(concrete_constants,Scalars),
309 append_to_section(concrete_constants,IP),
310 % the scalars should be typed by constraints,
311 % so move the constraints to the properties
312 select_section(properties,OldProps,NewProps),
313 {conjunct_predicates([C,OldProps],NewProps)}.
314 is_set_parameter(TExpr) :-
315 % upper case identifiers denote set parameters, otherwise scalars
316 get_texpr_id(TExpr,Name),is_upper_case(Name).
317 type_set_parameter(TExpr,Ein,Eout) :-
318 get_texpr_id(TExpr,Name),
319 get_texpr_type(TExpr,Type),
320 get_texpr_pos(TExpr,Pos),
321 % we directly type the deferred set
322 unify_types_werrors(set(global(Name)),Type,Pos,'PARAMETER',Ein,Eout).
323
324
325 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
326 % included machines
327
328 expand_machines([],_,_,M,M,Errors,Errors).
329 expand_machines([M|Rest],Machines,Uses,Typed,Result,Ein,Eout) :-
330 ? ( expand_machine(M,Machines,Uses,Typed,New,Ein,E1) -> true
331 ; add_error(bmachine_construction,'Expansion of machine failed:',M),fail),
332 expand_machines(Rest,Machines,Uses,[machine(M,New)|Typed],Result,E1,Eout).
333
334 % resolve all includes and typecheck the machine
335 % expand_machine(Name,Machines,TypeChecked,Expanded) :
336 % Name of the Machine to expand
337 % Machines contains the list of all loaded machines
338 % TypeChecked contains the list of all expanded machines so far
339 % Expanded is the resulting machine
340 expand_machine(Name,Machines,GlobalUses,TypeChecked,Expanded,Ein,Eout) :-
341 debug_format(9,'~nExpanding machine ~w~n',[Name]),
342 % find the machine in the list
343 find_machine(Name,Machines,MType,Header,RawMachineWithPragmas),
344 % remove pragmas for later reattachment
345 strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,_Pragmas),
346 % look for abstract machine
347 get_abstractions(Name,Machines,TypeChecked,Abstractions),
348 % merge all used and seen machines
349 ? use_and_see_machines(RawMachine,TypeChecked,SeenRefs),
350 % merge all included machines into one machine
351 include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes),
352 % Parameters contains now a list of parameters for each included machine
353 % Included contains now a machine that represents all included machines
354 % their parameters are renamed to internal_parameters
355 append([Abstractions,Included,SeenRefs],RefMachines),
356 % typecheck this machine
357 debug_stats(type_machine(Name)),
358 type_machine(Header,Name,MType,RawMachine,RefMachines,TypedLocal,RefMachines2,Ein,Err1),
359 % merge included and including machine
360 debug_stats(merge_included_machines(Name)),
361 merge_included_machines(Name,TypedLocal,Included,Promotes,Expanded2,Err1,Err2),
362 % add some predicates that state the equivalence between arguments
363 % in the include statement and the parameters of the included machine
364 add_link_constraints(Includes,MType,Parameters,RefMachines2,Expanded2,Expanded3,Err2,Err3),
365 % put together refinement and abstraction.
366 ? merge_refinement_and_abstraction(Expanded3,[ref(local,TypedLocal)|RefMachines2],Expanded4,Err3,Eout),
367 % merge used machines, will also prefix
368 debug_stats(merge_used_machines(Name)),
369 merge_used_machines(Included,Expanded4,Expanded5),
370 % clean up the syntax tree
371 debug_stats(clean_up_machine(Name)),
372 clean_up_machine(Expanded5,RefMachines2,Expanded),
373 debug_stats(finished_clean_up_and_expand_machine(Name)).
374
375 strip_machine_section_pragmas(RawMachineWithPragmas,RawMachine,Pragmas) :-
376 selectchk(units(_Pos,RealVariables,Pragmas),RawMachineWithPragmas,TRawMachine), !,
377 RawMachine = [RealVariables|TRawMachine].
378 strip_machine_section_pragmas(Machine,Machine,[]).
379
380 merge_included_machines(Name, TypedLocal, RefMachines, Promotes, Merged, Ein, Eout) :-
381 (Promotes=[] -> true ; assertz(machine_promotes_operations(Name,Promotes))),
382 include(is_included_ref,RefMachines,Included),
383 create_machine(Name,Empty),
384 % move the included operations into the promoted or unpromoted section
385 move_operations(Included,Promotes,Included2,Ein,Eout),
386 LocalAndIncluded = [ref(local,TypedLocal)|Included2],
387 % TODO: make sure that the constants of two instances of the same machine do not repeat (check what should be done for distinct machines with same identifiers)
388 concat_sections_of_refs([identifiers,initialisation,operation_bodies,
389 assertions,used,values],LocalAndIncluded,Empty,Merged1),
390 conjunct_sections_of_refs([constraints,properties,invariant],LocalAndIncluded,Merged1,Merged2),
391 concat_section_of_simple_lists(freetypes,LocalAndIncluded,Merged2,Merged3),
392 get_section(definitions,TypedLocal,Defs),
393 write_section(definitions,Defs,Merged3,Merged).
394 is_included_ref(ref(included,_)).
395
396 concat_section_of_simple_lists(Sec,References,In,Out) :-
397 maplist(extract_machine_from_ref,References,Machines),
398 sort_machines_by_global_order(Machines,OMachines),
399 foldl(concat_section_of_simple_lists2(Sec),OMachines,In,Out).
400 concat_section_of_simple_lists2(Sec,Machine,In,Out) :-
401 get_section(Sec,In,Orig),
402 get_section(Sec,Machine,List),
403 append(Orig,List,NewList),
404 write_section(Sec,NewList,In,Out).
405
406 merge_used_machines(RefMachines,Old,New) :-
407 % get all included machines from the references
408 convlist(ref_to_included_machine,RefMachines,Included),
409 foldl(merge_used_machines2,Included,Old,New).
410 merge_used_machines2(Included,Old,New) :-
411 get_section(used,Included,IncludedUse),
412 (IncludedUse = [] -> New = Old ; rename_used(IncludedUse,Old,New)).
413 ref_to_included_machine(ref(included,Inc),Inc).
414
415 % will add prefixes to identifiers
416 rename_used(IncludedUse,Old,New) :-
417 %print(renaming(IncludedUse)),nl,
418 expand_shortcuts([properties,invariant, assertions,
419 initialisation,operation_bodies],Sections), % TO DO: also traverse GOAL ? should we later apply this at the REPL level as well ? should we apply it to other DEFINITIONS ?
420 foldl(rename_used_sec(IncludedUse),Sections,Old,New).
421 rename_used_sec(IncludedUse,Sec,Old,New) :-
422 select_section_texprs(Sec,TExprs,NewTExprs,Old,New),
423 rename_used2_l(TExprs,IncludedUse,NewTExprs).
424
425 rename_used2(TExpr,IncludedUse,NewTExpr) :-
426 get_texpr_expr(TExpr,operation(Id,Params,Results,Subst)),!,
427 rename_used2_l(Params,IncludedUse,NParams),
428 rename_used2_l(Results,IncludedUse,NResults),
429 rename_used2(Subst,IncludedUse,NSubst),
430 get_texpr_type(TExpr,Type),
431 get_texpr_info(TExpr,Info),
432 selectchk(modifies(MIn),Info,Info1),selectchk(reads(RIn),Info1,RestInfo),
433 rename_used_ids(MIn,IncludedUse,MOut),
434 rename_used_ids(RIn,IncludedUse,ROut),
435 create_texpr(operation(Id,NParams,NResults,NSubst),Type,[modifies(MOut),reads(ROut)|RestInfo],
436 NewTExpr).
437 rename_used2(TExpr,IncludedUse,NewTExpr) :-
438 % rename identifier by adding machine prefix M.id
439 get_texpr_id(TExpr,_), % result is also Id (always ??)
440 get_texpr_info(TExpr,Info),
441 ? member(usesee(Name,Id,_Mode),Info),
442 ? member(includeduse(Name,Id,NewTExpr),IncludedUse), % This seems to reuse position information from includeduse list for all identifiers !! TO DO: check this
443 % we now rename Id to Name.Id
444 !. %, print(ren_id(Name,Id)),nl.
445 rename_used2(TExpr,IncludedUse,NTExpr1) :-
446 remove_bt(TExpr,Expr,NExpr,NTExpr),
447 syntaxtransformation(Expr,Subs,_,NSubs,NExpr),!,
448 rename_used2_l(Subs,IncludedUse,NSubs),
449 rename_infos(NTExpr,IncludedUse,NTExpr1).
450 rename_used2(TExpr,IncludedUse,NTExpr) :-
451 add_internal_error('Rename failed: ',rename_used2(TExpr,IncludedUse,NTExpr)),
452 NTExpr = TExpr.
453
454 % update infos, e.g., read/modifies for while loops
455 rename_infos(b(E,T,I),List,b(E,T,NI)) :- maplist(rename_info(List),I,NI).
456
457 rename_info(IncludeUseList,Info,NewInfo) :- info_field_contains_ids(Info,I,NewInfo,SNI),!,
458 maplist(rename_usage_info(IncludeUseList),I,NI), sort(NI,SNI).
459 rename_info(_,I,I).
460
461 info_field_contains_ids(reads(I),I,reads(SNI),SNI).
462 info_field_contains_ids(modifies(I),I,modifies(SNI),SNI).
463 info_field_contains_ids(non_det_modifies(I),I,non_det_modifies(SNI),SNI).
464 info_field_contains_ids(modifies_locals(I),I,modifies_locals(SNI),SNI).
465 info_field_contains_ids(reads_locals(I),I,reads_locals(SNI),SNI).
466 info_field_contains_ids(used_ids(I),I,used_ids(SNI),SNI).
467
468 rename_usage_info(IncludeUseList,ID,NewID) :-
469 (member(includeduse(_,ID,NewTExpr),IncludeUseList) -> get_texpr_id(NewTExpr,NewID) ; NewID = ID).
470
471
472 rename_used2_l([],_,R) :- !, R=[].
473 rename_used2_l([T|Rest],IncludedUse,[NT|NRest]) :-
474 rename_used2(T,IncludedUse,NT), !,
475 rename_used2_l(Rest,IncludedUse,NRest).
476 rename_used2_l(X,Y,Z) :- add_internal_error('Rename failed: ', rename_used2_l(X,Y,Z)),Z=X.
477
478 rename_used_ids(InIds,IncludedUse,OutIds) :-
479 maplist(rename_used_ids2(IncludedUse),InIds,OutIds).
480 rename_used_ids2(IncludedUse,InId,OutId) :-
481 memberchk(includeduse(_,InId,TOutId),IncludedUse),!,
482 get_texpr_id(TOutId,OutId).
483 rename_used_ids2(_IncludedUse,Id,Id).
484
485 get_abstractions(CName,Machines,TypedMachines,[ref(abstraction,Abstraction)]) :-
486 ? refines(M,AName),
487 get_constructed_machine_name(M,CName),
488 memberchk(M,Machines),!,
489 memberchk(machine(AName,Abstraction),TypedMachines).
490 get_abstractions(_,_,_,[]).
491
492 get_includes_and_promotes(Sections,M,Includes,Promotes) :-
493 optional_rawmachine_section(includes,Sections,[],Includes1),
494 optional_rawmachine_section(imports,Sections,[],Imports),
495 optional_rawmachine_section(extends,Sections,[],Extends),
496 optional_rawmachine_section(promotes,Sections,[],Promotes1),
497 append([Includes1,Extends,Imports],Includes),
498 maplist(expand_extends(M),Extends,Promotes2),
499 append([Promotes1|Promotes2],Promotes).
500 expand_extends(Machines,machine_reference(_,Ref,_),Promotes) :-
501 split_prefix(Ref,Prefix,Name),
502 memberchk(machine(Name,Body),Machines),
503 get_section(promoted,Body,Promoted),
504 prefix_identifiers(Promoted,Prefix,Renamings),
505 rename_bt_l(Promoted,Renamings,TPromotes),
506 maplist(add_nonpos,TPromotes,Promotes).
507 add_nonpos(TId,identifier(none,Id)) :-
508 get_texpr_id(TId,op(Id)).
509
510 move_operations([],Promotes,[],Ein,Eout) :-
511 foldl(add_promotes_not_found_error,Promotes,Ein,Eout).
512 move_operations([ref(_,IncMachine)|IncRest],Promotes,[ref(included,NewIncMachine)|RefRest],Ein,Eout) :-
513 move_operations2(IncMachine,Promotes,NewIncMachine,RestPromotes),
514 move_operations(IncRest,RestPromotes,RefRest,Ein,Eout).
515 move_operations2(Included,Promotes,Result,RestPromotes) :-
516 select_section(promoted,IncOperations,Promoted,Included,Included1),
517 select_section(unpromoted,OldUnpromoted,Unpromoted,Included1,Result),
518 filter_promoted(IncOperations,Promotes,Promoted,NewUnpromoted,RestPromotes),
519 append(OldUnpromoted,NewUnpromoted,Unpromoted).
520 filter_promoted([],Promotes,[],[],Promotes).
521 filter_promoted([TExpr|OpsRest],Promotes,Promoted,Unpromoted,RestPromotes) :-
522 get_texpr_id(TExpr,op(P)),
523 ? ( select(identifier(_,P),Promotes,RestPromotes1) ->
524 !,Promoted = [TExpr|RestPromoted],
525 Unpromoted = RestUnpromoted
526 ;
527 RestPromotes1 = Promotes,
528 Promoted = RestPromoted,
529 Unpromoted = [TExpr|RestUnpromoted]),
530 filter_promoted(OpsRest,RestPromotes1,RestPromoted,RestUnpromoted,RestPromotes).
531 add_promotes_not_found_error(identifier(Pos,Id),[error(Msg,Pos)|E],E) :-
532 ajoin(['Promoted operation ',Id,' not found'],Msg).
533
534 find_machine(Name,Machines,Type,Header,Sections) :-
535 Header = machine_header(_,Name,_),
536 ? ( (member(abstract_machine(_,_ModelType,Header,Sections),Machines),
537 Type=machine)
538 ; (member(refinement_machine(_,Header,_Abstract,Sections),Machines),
539 Type=refinement)
540 ; (member(implementation_machine(_,Header,_Abstract,Sections),Machines),
541 Type=implementation)),
542 !.
543
544 include_machines(RawMachine, TypeChecked, GlobalUses, Includes, Parameters, Included, Promotes) :-
545 get_includes_and_promotes(RawMachine,TypeChecked,Includes,Promotes),
546 maplist(include_machine(TypeChecked, GlobalUses), Includes, Parameters, Singles),
547 remove_duplicate_set_inclusions(Singles,Singles1),
548 % duplicate constants inclusion is handled currently in concat_section_contents via section_can_have_duplicates
549 % create refs
550 maplist(create_ref,Singles1,Included).
551 create_ref(IncMachine,ref(included,IncMachine)).
552
553 % it is possible that a deferred or enumerated set is declared in an included machine
554 % that is included more than once. We remove all but one occurrences.
555 remove_duplicate_set_inclusions([],[]).
556 remove_duplicate_set_inclusions([M],[M]) :- !.
557 remove_duplicate_set_inclusions([M|Rest],[M|CleanedRest]) :-
558 get_section(deferred_sets,M,DSets),
559 get_section(enumerated_sets,M,ESets),
560 get_section(enumerated_elements,M,EElements),
561 append([DSets,ESets,EElements],Identifiers),
562 sort(Identifiers,SortedIds),
563 maplist(remove_duplicate_sets2(SortedIds),Rest,Rest2),
564 remove_duplicate_set_inclusions(Rest2,CleanedRest).
565 remove_duplicate_sets2(Identifiers,M,Cleaned) :-
566 remove_duplicate_sets_section(deferred_sets,Identifiers,M,M1),
567 remove_duplicate_sets_section(enumerated_sets,Identifiers,M1,M2),
568 remove_duplicate_sets_section(enumerated_elements,Identifiers,M2,Cleaned).
569 remove_duplicate_sets_section(Section,Identifiers,In,Out) :-
570 select_section(Section,Old,New,In,Out),
571 %get_texpr_ids(Identifiers,II),format('Removing duplicates ~w = ~w~n',[Section,II]),
572 exclude(element_is_duplicate(Identifiers),Old,New).
573
574 element_is_duplicate(Identifiers,TId) :-
575 get_texpr_id(TId,Name),
576 get_texpr_type(TId,Type),
577 get_texpr_id(ToRemove,Name),
578 get_texpr_type(ToRemove,Type),
579 ord_member_nonvar_chk(ToRemove,Identifiers),
580 get_texpr_info(TId,InfosA),
581 get_texpr_info(ToRemove,InfosB),
582 member(def(Sec,File),InfosA),
583 member(def(Sec,File),InfosB),
584 debug_format(5,'Removed duplicate included identifier: ~w~n',[Name]),
585 !.
586
587 include_machine(TypeChecked,Used,machine_reference(_Pos,FullRef,_Args),
588 parameters(FullRef,Parameters), TM) :-
589 split_prefix(FullRef,Prefix,Name),
590 % TM1 is the already typechecked included machine:
591 ? member(machine(Name,TM1),TypeChecked),!,
592 debug_println(9,including_machine(Name)),
593 % TM2 is a fresh copy, so we prevent unification of the parameter types:
594 (get_section(parameters,TM1,[]) -> TM2=TM1
595 ; copy_term(TM1,TM2) % this can be expensive; only copy if there are parameters
596 ),
597 % If the included machine is used somewhere, we store the identifiers
598 % to enable joining the different references later:
599 include_usings(Name,Used,TM2,TM3),
600 % TM3 is typechecked and all internal variables are renamed with a prefix
601 hide_private_information(FullRef,TM3,TM4),
602 % TM4 is typechecked, and if it was referenced with a prefix (e.g. INCLUDES p.M2)
603 % all variables are prefixed
604 %print(prefixing(Prefix)),nl,
605 prefix_machine(Prefix,TM4,TM5),
606 % We need the parameters later to state their equivilance to the arguments
607 get_section(parameters,TM5,Parameters),
608 % We move the parameters to the internal parameters, because the resulting
609 % machine has only the parameters of the including machine.
610 parameters_to_internal(TM5,TM).
611
612 include_usings(Name,Uses,Old,New) :-
613 ( member(Name,Uses) ->
614 store_usage_info(Old,Name,UsedInfo),
615 append_to_section(used,UsedInfo,Old,New)
616 ;
617 Old = New).
618 % returns a list of which identifiers are used in the machine
619 % for each identifier, we have a trible includeuse(Name,Id,TExpr)
620 % where Name is the name of the used machine, Id is the
621 % original ID and TExpr is the currently used reference to this
622 % identifier
623 store_usage_info(Machine,Name,UsedInfo) :-
624 expand_shortcuts([identifiers],IdSections),
625 foldl(store_usage_info2(Machine,Name),IdSections,UsedInfo,[]).
626 store_usage_info2(Machine,Name,Sec,I,O) :-
627 get_section(Sec,Machine,Content),
628 foldl(store_usage_info3(Name),Content,I,O).
629 store_usage_info3(Name,TId,[includeduse(Name,Id,TId)|L],L) :-
630 get_texpr_id(TId,Id).
631
632 % conjunct sections that contain predicates (CONSTRAINTS, PROPERTIES, INVARIANT)
633 conjunct_sections_of_refs(Sections1,References,Old,New) :-
634 expand_shortcuts(Sections1,Sections),
635 maplist(extract_machine_from_ref,References,Machines),
636 sort_machines_by_global_order(Machines,OMachines),
637 foldl(conjunct_sections2(OMachines),Sections,Old,New).
638 conjunct_sections2(Machines,Section,Old,New) :-
639 % Section is constraints,properties,invariant, ...
640 write_section(Section,NewContent,Old,New), % prepare new section
641 get_section_of_machines(Machines,Section,Preds),
642 %maplist(get_machine_name,Machines,Ns),print(got_sections(Section,Ns)),nl,
643 %translate:l_print_bexpr_or_subst(Preds),nl,
644 conjunct_predicates(Preds,NewContent).
645
646
647 % merge sections that contain a list of expressions/formulas like identifiers, assertions, ...
648 concat_sections_of_refs(Sections1,References,Old,New) :-
649 maplist(extract_machine_from_ref,References,Machines),
650 maplist(create_tag_by_reference,References,Tags),
651 sort_machines_by_global_order(Machines,Tags,OMachines,STags),
652 % should we only sort for some sections, e.g., assertions
653 % for each machine, create a tag where the expression comes from
654 concat_sections(Sections1,OMachines,STags,Old,New).
655
656 extract_machine_from_ref(ref(_,M),M).
657
658 create_tag_by_reference(ref(local,_Machine),[]) :- !.
659 create_tag_by_reference(ref(RefType,Machine),[RefType/Name]) :-
660 get_machine_name(Machine,Name).
661
662 concat_sections(Sections1,Machines,Tags,Old,New) :-
663 expand_shortcuts(Sections1,Sections),
664 foldl(concat_section2(Machines,Tags),Sections,Old,New).
665 concat_section2(Machines,Tags,Section,Old,New) :-
666 write_section(Section,NewContent,Old,New),
667 maplist(get_tagged_lsection_of_machine(Section),Machines,Tags,Contents),
668 concat_section_contents(Section,Contents,NewContent).
669
670 concat_section_contents(_,[SingleContent],Res) :- !, Res=SingleContent. % no need to remove_dups
671 concat_section_contents(Section,Contents,NewContent) :-
672 append(Contents,ConcContents),
673 (section_can_have_duplicates(Section)
674 -> remove_dups_keep_order(ConcContents,NewContent)
675 ; NewContent=ConcContents).
676
677 % see issue PROB-403
678 section_can_have_duplicates(X) :- section_can_be_included_multiple_times_nonprefixed(X).
679 % should we also remove duplicates in PROPERTIES section ? cf. machines used in test 1857
680
681
682 get_tagged_lsection_of_machine(Section,Machine,Tags,TaggedContent) :-
683 get_section(Section,Machine,Content),
684 (Tags=[] -> TaggedContent=Content ; maplist(tag_with_origin(Tags),Content,TaggedContent)).
685
686 tag_with_origin(Origins,TExpr,TaggedExpr) :-
687 change_info_of_expression_or_init(TExpr,Info,TaggedInfo,TaggedExpr),
688 % add a new origin to the old tag or if not existent, add a new info field
689 ( Origins = [] -> TaggedInfo = Info
690 ; selectchk(origin(Orest),Info,origin(Onew),TaggedInfo) -> append(Origins,Orest,Onew)
691 ; TaggedInfo = [origin(Origins)|Info]).
692 % the substitutions in the initialisation are additionally wrapped by an init/2 term
693 % a small hack to work with those too.
694 % TODO: this became a very ugly hack -- redo!
695 change_info_of_expression_or_init(init(A,OExpr),Old,New,init(A,NExpr)) :-
696 !,change_info_of_expression_or_init(OExpr,Old,New,NExpr).
697 % ignore the info for includeduse/3 completely
698 change_info_of_expression_or_init(includeduse(A,B,C),[],_,includeduse(A,B,C)) :- !.
699 change_info_of_expression_or_init(freetype(FTypeId,Cases),[],_,freetype(FTypeId,Cases)) :- !.
700 change_info_of_expression_or_init(OExpr,Old,New,NExpr) :-
701 create_texpr(Expr,Type,Old,OExpr),!,
702 create_texpr(Expr,Type,New,NExpr).
703 change_info_of_expression_or_init(OExpr,Old,New,NExpr) :-
704 add_internal_error('Illegal typed expression:',change_info_of_expression_or_init(OExpr,Old,New,NExpr)),
705 Old=[], NExpr=OExpr.
706
707 % adds a prefix to all variables and promoted operations
708 prefix_machine('',TM,TM) :- !.
709 prefix_machine(Prefix,Old,New) :-
710 debug_println(5,prefixing_machine(Prefix)),
711 expand_shortcuts([variables,promoted], RenamedIdentiferSections),
712 get_all_identifiers(RenamedIdentiferSections,Old,Identifiers),
713 prefix_identifiers(Identifiers,Prefix,Renamings),
714 find_relevant_sections(RenamedIdentiferSections,[machine],Sections1),
715 append(RenamedIdentiferSections,Sections1,Sections),
716 rename_in_sections(Sections,Renamings,Old,M),
717 rename_includeduse(M,Renamings,New).
718 rename_includeduse(Old,Renamings,New) :-
719 select_section(used,OldContent,NewContent,Old,New),
720 maplist(rename_includeduse2(Renamings),OldContent,NewContent).
721 rename_includeduse2(Renamings,includeduse(M,N,TExpr),includeduse(M,N,NExpr)) :-
722 rename_bt(TExpr,Renamings,NExpr).
723
724 get_all_identifiers(Sections1,M,Identifiers) :-
725 expand_shortcuts(Sections1,Sections),
726 maplist(get_all_identifiers2(M),Sections,LIdentifiers),
727 append(LIdentifiers,Identifiers).
728 get_all_identifiers2(M,Sec,Identifiers) :-
729 get_section(Sec,M,Identifiers).
730
731 % hide all parameters and unpromoted operations
732 hide_private_information(Prefix,Machine,NewMachine) :-
733 get_section(parameters,Machine,Params),
734 get_section(unpromoted,Machine,UnPromoted),
735 append(Params,UnPromoted,ToHide),
736 %debug_println(9,hide_private(Prefix,ToHide)),
737 ( ToHide = [] -> NewMachine=Machine
738 ;
739 prefix_identifiers(ToHide,Prefix,Renamings),
740 % we have to do the renaming in promoted operations, too, because
741 % those operations might use the renamed parameters and their reads/modifies
742 % info must be updated
743 rename_in_sections([parameters,promoted,unpromoted],Renamings,Machine,Machine1),
744 rename_includeduse(Machine1,Renamings,Machine2),
745 rename_relevant_sections([parameters,operations],Renamings,Machine2,NewMachine)).
746
747 prefix_identifiers(Identifiers,'',Identifiers) :- !.
748 prefix_identifiers(Old,Prefix,New) :-
749 maplist(prefix_identifier(Prefix),Old,New).
750 prefix_identifier(Prefix,TExpr,rename(Old,New)) :-
751 get_texpr_expr(TExpr,identifier(Old)),
752 (Old=op(OI) -> New=op(NI) ; OI=Old,NI=New),
753 ajoin([Prefix,'.',OI],NI). % , print(rename(Old,New)),nl.
754
755 parameters_to_internal(M1,M2) :-
756 select_section(internal_parameters,OldParams,Params,M1,M3),
757 select_section(parameters,NewParams,[],M3,M2),
758 append(OldParams,NewParams,Params).
759
760 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
761 % uses and sees relations
762 find_uses(Machines,Uses,NotIncluded,Ein,Eout) :-
763 findall(U, use_usage(Machines,_,U), UnsortedUses),
764 sort(UnsortedUses,Uses),
765 check_include_use(Uses,Machines,NotIncluded,Ein,Eout).
766
767 % check_include_use/5 checks if the used machines are included in any machine
768 % check_include_use(+Uses,+Machines,-NotIncluded,Ein,Eout)
769 % Uses: The list of machine names that are used
770 % Machines: The list of machines
771 % NotIncluded: The list of used machines (their names) that are not included
772 % Ein/Eout: The errors (as difference-list)
773 check_include_use([],_,[],Errors,Errors).
774 check_include_use([U|Rest],Machines,NotIncluded,Ein,Eout) :-
775 findall(I,include_usage(Machines,U,I),Inc),
776 ( Inc=[] -> NotIncluded = [U|RestNotIncluded], Ein=E1
777 ; Inc=[_] -> NotIncluded = RestNotIncluded, Ein=E1
778 ;
779 NotIncluded = RestNotIncluded,
780 use_usage(Machines,Pos,U),
781 Ein = [error('used machine is included more than once',Pos)|E1]
782 ),
783 check_include_use(Rest,Machines,RestNotIncluded,E1,Eout).
784 % extend_not_included_uses(+Uses,+Main,-Name,+Machines,-AllMachines):
785 % Create a dummy machine that extends the main machine and extends or includes
786 % all seen/used machines that are not included if such machines exist.
787 % In case of refinement this is done for the whole refinement chain.
788 % Uses: List of machine names of the machines that are used/seen but not included
789 % Main: The name of the main machine
790 % Name: The name of the generated dummy machine (or Main if no dummy machine is generated)
791 % Machines: List of all specified Machines
792 % AllMachines: List of all Machines + the new dummy machine(s)
793 extend_not_included_uses([],Main,Main,Machines,Machines) :- !.
794 extend_not_included_uses(Uses,Main,NewMainName,Machines,AllMachines) :-
795 get_refinement_hierarchy(Main,Machines,RefChain),
796 maplist(extend_not_included_uses2(Uses,Machines),RefChain,NewMachines),
797 append(NewMachines,Machines,AllMachines),
798 dummy_machine_name(Main,NewMainName),
799 debug_format(19,'Creating dummy machine called ~w for main machine~n',[NewMainName]).
800 extend_not_included_uses2(Uses,Machines,Name,DummyMachine) :-
801 debug_format(19,'Creating dummy subsidiary machine for refined machine ~w~n',[Name]),
802 create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine),
803 IncludeMain = machine_reference(none,Name,Parameters),
804 ( get_preference(seen_machines_included,true) ->
805 % extend just the main machine, include the used/seen machines
806 References = [extends(none,[IncludeMain]),includes(none,UReferences)]
807 ;
808 % extends the main machine and all used/seen machines
809 References = [extends(none,[IncludeMain|UReferences])]),
810 maplist(find_using(Machines),Uses,UReferences,LUParameters),
811 append([Parameters|LUParameters],DummyParameters),
812 copy_raw_definitions(Name,Machines,OptDefs),
813 % we store a flag "is_dummy" in the machine because we have a special case
814 % later, see type_constraints/7.
815 append([References,[is_dummy],OptDefs],Sections).
816 create_dummy_machine(Name,Machines,Parameters,DummyParameters,Sections,DummyMachine) :-
817 dummy_machine_name(Name,DummyName),
818 ? get_raw_model_type(Name,Machines,ModelType),
819 Header = machine_header(_,Name,Parameters),
820 DummyHeader = machine_header(none,DummyName,DummyParameters),
821 ? member(Machine,Machines),
822 ? generate_raw_machine(Header,DummyHeader,ModelType,Sections,Machine,DummyMachine),!.
823
824 generate_raw_machine(OldHeader,NewHeader,_,NewSections,
825 abstract_machine(_, ModelType,OldHeader,_),
826 abstract_machine(none,ModelType,NewHeader,NewSections)).
827 generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections,
828 refinement_machine(_, OldHeader,_Abstract, _),
829 abstract_machine(none,ModelType,NewHeader,NewSections)).
830 generate_raw_machine(OldHeader,NewHeader,ModelType,NewSections,
831 implementation_machine(_, OldHeader,_Abstract, _),
832 abstract_machine(none,ModelType,NewHeader,NewSections)).
833
834 dummy_machine_name(Name,DummyName) :-
835 atom_concat('MAIN_MACHINE_FOR_',Name,DummyName).
836
837 find_using(Machines,U,machine_reference(none,Name,Arguments),Arguments) :-
838 % was using(U).U
839 ajoin([U,'.',U],Name),
840 ? member(M,Machines), get_machine_parameters(M,U,Params,_),!,
841 maplist(add_use_param,Params,Arguments).
842 add_use_param(identifier(_,Param),identifier(none,Name)) :-
843 ( is_upper_case(Param) ->
844 ajoin(['Useparam(',Param,')'],Name)
845 ;
846 ajoin(['useparam(',Param,')'],Name)).
847
848 % copy_raw_definitions(+Name,+Machines,-OptDefs):
849 % Get the definitions section from a raw (untyped) machine
850 % Name: Name of the machine
851 % Machines: List of Machines
852 % OptDefs: [] if no definitions are present or [Def] if a definition section Def is present
853 copy_raw_definitions(Name,Machines,OptDefs) :-
854 ? get_constructed_machine_name_and_body(M,Name,_,Sections),
855 memberchk(M,Machines),!,
856 Def = definitions(_,_),
857 ( memberchk(Def,Sections) ->
858 OptDefs = [Def]
859 ;
860 OptDefs = []).
861
862 add_def_dependency_information(DefsIn,DefsOut,Ein,Eout) :-
863 extract_def_name_set(DefsIn,DefNames,DN),
864 maplist(add_def_dep(DN),DefsIn,Defs1),
865 check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,Ein,Eout).
866
867 extract_def_name_set(Defs,DefNames,DN) :-
868 maplist(get_def_name,Defs,DefNames),
869 maplist(to_mapset_entry,DefNames,DN1),
870 list_to_avl(DN1,DN).
871
872 get_def_name(Def,Name) :- arg(1,Def,Name).
873 get_def_pos(Def,Pos) :- arg(3,Def,Pos).
874 get_def_dependencies(Def,Dependencies) :- arg(6,Def,Dependencies).
875 to_mapset_entry(Name,Name-true).
876
877 add_def_dep(DN,In,Out) :-
878 analyse_definition_dependencies(In,DN,Deps),
879 In = definition_decl(Name,DefType,Pos,Args,RawExpr),
880 Out = definition_decl(Name,DefType,Pos,Args,RawExpr,Deps).
881
882 check_for_cyclic_def_dependency(Defs,DefNames,DefsOut,Ein,Eout) :-
883 % check if we have a cyclic definition:
884 create_definitions_avl(Defs,DefsAvl),
885 search_for_cyclic_definition(DefNames,DefsAvl,[],Pos,RCycle),!,
886 % if we have found a cyclic definition, generate an error message, ...
887 reverse(RCycle,Cycle),add_arrows(Cycle,Msg0),
888 ajoin(['Found cyclic definitions: '|Msg0],Msg),
889 Ein = [error(Msg,Pos)|E1],
890 % ... remove the definitions in the cycle (to prevent later infinite loops) ...
891 exclude(definition_in_list(Cycle),Defs,Defs1),
892 % ... and check the remaining definitions.
893 check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,E1,Eout).
894 check_for_cyclic_def_dependency(Defs,_DefNames,Defs,E,E).
895 add_arrows([E],[E]) :- !.
896 add_arrows([E|Erest],[E,'->'|Arest]) :- add_arrows(Erest,Arest).
897 definition_in_list(List,Def) :-
898 get_def_name(Def,Name),memberchk(Name,List).
899
900 create_definitions_avl(Defs,DefsAvl) :-
901 maplist(split_def_name,Defs,Entries),
902 list_to_avl(Entries,DefsAvl).
903 split_def_name(Def,Name-Def) :- get_def_name(Def,Name).
904
905
906 % just a depth-first search to find a cycle
907 search_for_cyclic_definition(DefNames,Definitions,Visited,Pos,Cycle) :-
908 ? member(Name,DefNames),avl_fetch(Name,Definitions,Definition),
909 get_def_pos(Definition,Pos),
910 ( memberchk(Name,Visited) ->
911 Cycle = [Name|Visited]
912 ;
913 get_def_dependencies(Definition,Dependencies),
914 search_for_cyclic_definition(Dependencies,Definitions,[Name|Visited],_,Cycle)
915 ).
916
917 :- assert_must_succeed((
918 list_to_avl([def1-true,def2-true,def3-true,def4-true],DefNames),
919 analyse_definition_dependencies(
920 conjunct(none,
921 equals(none,
922 identifier(none,x),
923 identifier(none,def1)),
924 equals(none,
925 definition(none,def4,
926 [function(none,
927 identifier(none,def3),
928 integer(none,5))]),
929 identifier(y))),DefNames,Defs),
930 Defs==[def1,def3,def4]
931 )).
932 % analyse_definition_dependencies(+Expr,+DefinitionNames,Deps):
933 % Expr: raw (i.e. untyped) expression to analyse
934 % DN: AVL set (i.e. mapping from elements to 'true') of the names of the definitions
935 % This is needed to decide if an identifier is a reference to a definition
936 % Deps: A list of used definitions (a list of their names)
937 analyse_definition_dependencies(Expr,DN,Deps) :-
938 analyse_definition_dependencies2(Expr,DN,Unsorted,[]),
939 sort(Unsorted,Deps).
940 analyse_definition_dependencies2(VAR,_DN) --> {var(VAR)},!,
941 {add_internal_error('Variable DEFINITION expression in',analyse_definition_dependencies)}.
942 analyse_definition_dependencies2([Expr|Rest],DN) -->
943 !, analyse_definition_dependencies2(Expr,DN),
944 analyse_definition_dependencies2(Rest,DN).
945 analyse_definition_dependencies2(definition(_Pos,Name,Args),DN) -->
946 !,[Name],analyse_definition_dependencies2(Args,DN).
947 analyse_definition_dependencies2(identifier(_Pos,Name),DN) -->
948 {avl_fetch(Name,DN),!},[Name].
949 analyse_definition_dependencies2(Expr,DN) -->
950 { compound(Expr),functor(Expr,_Functor,Arity),!},
951 analyse_definition_dependencies_arg(2,Arity,Expr,DN).
952 analyse_definition_dependencies2(_Expr,_DN) --> [].
953
954 analyse_definition_dependencies_arg(I,Arity,Expr,DN) -->
955 { I =< Arity,!,arg(I,Expr,Arg),I2 is I+1 },
956 analyse_definition_dependencies2(Arg,DN),
957 analyse_definition_dependencies_arg(I2,Arity,Expr,DN).
958 analyse_definition_dependencies_arg(_I,_Arity,_Expr,_DN) --> [].
959
960
961 :- use_module(tools_positions, [get_position_filenumber/2]).
962
963 get_constructed_machine_name(MachineTerm,Name) :- get_constructed_machine_name_and_body(MachineTerm,Name,_Pos,_).
964 % name and pos; pos can be used for filenumber
965 get_constructed_machine_name_and_filenumber(MachineTerm,Name,Filenumber) :-
966 get_constructed_machine_name_and_body(MachineTerm,Name,Pos,_),
967 (get_position_filenumber(Pos,FN) -> Filenumber=FN ; Filenumber=unknown).
968 get_constructed_machine_name_and_body(abstract_machine(_,_ModelType,machine_header(Pos,Name,_),Body),Name,Pos,Body).
969 get_constructed_machine_name_and_body(refinement_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body).
970 get_constructed_machine_name_and_body(implementation_machine(_,machine_header(Pos,Name,_),_Abstract,Body),Name,Pos,Body).
971
972 refines(refinement_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract).
973 refines(implementation_machine(_,machine_header(_,_Name,_),Abstract,_Body),Abstract).
974
975 get_machine_parameters(abstract_machine(Pos,_ModelType,machine_header(_,Name,Parameters),_),Name,Parameters,Pos).
976 get_machine_parameters(refinement_machine(Pos,machine_header(_,Name,Parameters),_,_),Name,Parameters,Pos).
977 get_machine_parameters(implementation_machine(Pos,machine_header(_,Name,Parameters),_,_),Name,Parameters,Pos).
978
979 get_raw_model_type(Main,Machines,ModelType) :-
980 ? get_constructed_machine_name_and_body(M,Main,_,_),
981 memberchk(M,Machines),
982 ( refines(M,RefName) ->
983 ? get_raw_model_type(RefName,Machines,ModelType)
984 ;
985 M = abstract_machine(_,ModelType,_,_)).
986
987 some_machine_name_body(Machines,M,Name,Body) :-
988 ? member(M,Machines),
989 get_constructed_machine_name_and_body(M,Name,_,Body).
990
991 use_usage(Machines,Pos,Use) :-
992 ? some_machine_name_body(Machines,_,_,Body),
993 ? ( member(sees(Pos,R),Body)
994 ; member(uses(Pos,R),Body)),
995 member(identifier(_,PrefixUse),R),
996 split_prefix(PrefixUse,_,Use).
997 % include_usage/3 checks if there is any machine in Machines that
998 % includes/extends/imports the used machine
999 % include_usage(+Machines,+Use,-Name):
1000 % Machines: The list of machines
1001 % Use: The name of the used machine
1002 % Name: The name of the machine that imports the used machine
1003 % include_usage/3 fails if there is not such an import
1004 include_usage(Machines,Use,Name) :-
1005 ? some_machine_name_body(Machines,_,Name,Body),
1006 ? ( member(includes(_,R),Body)
1007 ; member(extends(_,R), Body)
1008 ; member(imports(_,R), Body)),
1009 ? member(machine_reference(_Pos,PrefixRef,_),R),
1010 % The name could be prefixed, we need it without prefix:
1011 split_prefix(PrefixRef,_,Use).
1012
1013 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1014 % uses and sees clauses
1015
1016 % returns a list of references to used and seen machines
1017 % the machines contain only identifier sections and
1018 % the identifier are prefixed accordingly
1019 % all identifier are marked as coming from a seen/used machine
1020 use_and_see_machines(Sections,Machines,References) :-
1021 get_uses_and_sees(Sections,Uses,Sees),
1022 maplist(use_or_see_machine(used,Machines),Uses,Used),
1023 ? maplist(use_or_see_machine(seen,Machines),Sees,Seen),
1024 append(Used,Seen,References).
1025
1026 % get uses and sees sections from the untyped machines
1027 get_uses_and_sees(Sections,Uses,Sees) :-
1028 get_uses_or_sees2(sees,Sections,Sees),
1029 get_uses_or_sees2(uses,Sections,Uses).
1030 get_uses_or_sees2(Mode,Sections,US) :-
1031 optional_rawmachine_section(Mode,Sections,[],US1),
1032 findall(I,member(identifier(_,I),US1),US).
1033
1034 use_or_see_machine(Mode,TypedMachines,Ref,ref(Mode,Result)) :-
1035 split_prefix(Ref,Prefix,Name),
1036 memberchk(machine(Name,Typed),TypedMachines),
1037 create_machine(Name,Empty),
1038 ? use_sections([sets],Mode,'',Name,Typed,Empty,M1),
1039 ? use_sections([constants,variables,promoted],Mode,Prefix,Name,Typed,M1,Result).
1040 use_sections(Sections,Mode,Prefix,MName,Typed,Old,New) :-
1041 expand_shortcuts(Sections,AllSections),
1042 ? foldl(use_section(Mode,Prefix,MName,Typed),AllSections,Old,New).
1043 use_section(Mode,Prefix,MName,Machine,Section,OldM,NewM) :-
1044 ? get_section_texprs(Section,Machine,Identifiers),
1045 write_section(Section,NewIds,OldM,NewM),
1046 ( Prefix='' ->
1047 Ids1=Identifiers
1048 ;
1049 prefix_identifiers(Identifiers,Prefix,Renamings),
1050 rename_bt_l(Identifiers,Renamings,Ids1)),
1051 maplist(add_use_info_to_identifier(Mode,MName),Ids1,NewIds).
1052 add_use_info_to_identifier(Mode,Name,TExpr,New) :-
1053 get_texpr_id(TExpr,PId), get_texpr_type(TExpr,Type),
1054 get_texpr_id(New,PId), get_texpr_type(New,Type),
1055 split_prefix(PId,_Prefix,Id),
1056 get_texpr_info(TExpr,Info),
1057 get_texpr_info(New,[usesee(Name,Id,Mode)|Info]).
1058
1059
1060 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1061 % add a section to the machine that describes the linking of
1062 % parameters and arguments
1063 add_link_constraints(Includes,MType,Parameters,RefMachines,Old,New,Ein,Eout) :-
1064 AllRefMachines = [ref(local,Old)|RefMachines],
1065 extract_parameter_types(RefMachines,NonGroundExceptions),
1066 foldl(add_link_section(MType,Parameters,AllRefMachines,NonGroundExceptions),
1067 Includes,Links/Ein,[]/Eout), % TO DO: Daniel check if [] is correct here
1068 %print(conjunct_predicates(Links,Link)),nl,
1069 conjunct_predicates(Links,Link),
1070 select_section(constraints,OConstraints,NConstraints,Old,New),
1071 conjunct_predicates([Link,OConstraints],NConstraints).
1072 add_link_section(MType,Parameters,RefMachines,NonGroundExceptions,
1073 machine_reference(Pos,Ref,Args),Links/Ein,RLinks/Eout) :-
1074 visible_env(MType,includes,RefMachines,Env,Ein,E1),
1075 memberchk(parameters(Ref,TParameters),Parameters),
1076 ( same_length(TParameters, Args) ->
1077 get_texpr_types(TParameters,Types),
1078 btype_ground_dl(Args,Env,NonGroundExceptions,Types,TArgs,E1,Eout),
1079 maplist(create_plink_equality,TParameters,TArgs,LLinks)
1080 ;
1081 E1 = [error('wrong number of machine arguments',Pos)|Eout],
1082 LLinks = []),
1083 append(LLinks,RLinks,Links).
1084 create_plink_equality(P,A,E) :-
1085 create_texpr(equal(P,A),pred,[parameterlink],E).
1086
1087 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1088 % type machines
1089
1090 type_machine(Header,Name,MType,RawMachine,RefMachines,TypedMachine,NewRefMachines,Ein,Eout) :-
1091 Header = machine_header(_,Name,_),
1092 create_machine(Name,Empty),
1093 % (optional) definitions
1094 extract_definitions(RawMachine,Empty,DefsOnly,Ein,E0),
1095 debug_stats(extracted_definitions(Name)),
1096 % create the identifiers that will be typed,
1097 % Local will contain the identifier sections
1098 create_id_sections(Header,RawMachine,Name,DefsOnly,Local),
1099 debug_stats(created_identifier_sections(Name)),
1100 create_freetypes(RawMachine,MType,RefMachines,Local,Local1,E0,E1),
1101 % in case of a refinement, check if all newly defined operations are refinements
1102 link_to_refinement(MType,Name,RawMachine,RefMachines,Local1,Local2,E1,E2),
1103 % extract types that can be variables
1104 debug_stats(created_link_to_refinement(Name)),
1105 extract_parameter_types([ref(local,Local2)|RefMachines],NonGroundExceptions),
1106 % check for a VALUES clause. They are a little bit tricky because they can replace
1107 % already defined deferred sets by integers or other deferred sets
1108 process_values_section(MType,RawMachine,NonGroundExceptions,
1109 Local2/E2/RefMachines,Local3/E3/NewRefMachines),
1110 % type-check the other sections (properties, invariant, operation_bodies, etc)
1111 type_sections(RawMachine,MType,[ref(local,Local3)|NewRefMachines],NonGroundExceptions,
1112 Name,E3,Eout,Local3,TypedMachine).
1113
1114 % extract definitions from a definition file
1115 extract_only_definitions(MainName,RawMachine,DefsOnlyMachine,FinalErrors) :-
1116 create_machine(MainName,Empty),
1117 extract_definitions(RawMachine,Empty,DefsOnlyMachine,Errors,[]),
1118 sort(Errors,FinalErrors),
1119 add_all_perrors(FinalErrors).
1120
1121 extract_definitions(RawMachine,In,Out,Ein,Eout) :-
1122 optional_rawmachine_section(definitions,RawMachine,[],AllDefinitions),
1123 write_section(definitions,Definitions,In,Out),
1124 % remove all references to definition files from definitions
1125 exclude(is_file_definition,AllDefinitions,Definitions1),
1126 % replace expression_definition(...) by defintion(expression,...), etc.
1127 change_definition_style(Definitions1,Definitions2),
1128 % analyse dependencies
1129 add_def_dependency_information(Definitions2,Definitions3,Ein,Eout),
1130 % replace external function definitions by calls to the external function
1131 replace_external_declarations(Definitions3,Definitions).
1132
1133 is_file_definition(file_definition(_Pos,_Filename)).
1134
1135 change_definition_style(DefsIn,DefsOut) :-
1136 maplist(change_definition_style2,DefsIn,DefsOut).
1137 change_definition_style2(conversion(Pos,InnerDef),definition_decl(Name,DefType,InnerPos,Args,conversion(Pos,RawExpr))) :-
1138 change_definition_style2(InnerDef,definition_decl(Name,DefType,InnerPos,Args,RawExpr)).
1139 change_definition_style2(Def,definition_decl(Name,DefType,Pos,Args,RawExpr)) :-
1140 Def =.. [Functor,Pos,Name,Args,RawExpr],
1141 maplist(check_def_argument(Name,Pos),Args),
1142 map_def_functor(Functor,DefType).
1143 map_def_functor(expression_definition,expression).
1144 map_def_functor(substitution_definition,substitution).
1145 map_def_functor(predicate_definition,predicate).
1146
1147 % check formal arguments of definitions , e.g., here xx in square2 is not an identifier: xx == 20; square2(xx) == xx*xx
1148 check_def_argument(_,_,identifier(_,_)) :- !.
1149 check_def_argument(DefName,DefPos,definition(_,ID,_)) :- !,
1150 tools:ajoin(['Formal parameter ', ID, ' is a definition call in Definition: '],Msg),
1151 add_error(bmachine_construction,Msg,DefName,DefPos).
1152 check_def_argument(DefName,DefPos,FP) :- !,
1153 tools:ajoin(['Formal parameter ', FP, ' is not an identifier in Definition: '],Msg),
1154 add_error(bmachine_construction,Msg,DefName,DefPos).
1155
1156 replace_external_declarations(Definitions,NewDefs) :-
1157 split_list(is_external_declaration,Definitions,ExtFunctionDecls,RestDefs),
1158 foldl(replace_external_declaration,ExtFunctionDecls,RestDefs,NewDefs).
1159 is_external_declaration(definition_decl(DefName,expression,_Pos,_Params,_Def,_Dependencies)) :-
1160 external_name(DefName,ExtType,_ExpectedDefType,_ExtCall,FunName),
1161 debug_format(4,'external ~w declared: ~w~n', [ExtType,FunName]).
1162 external_name(DefName,_,_,_,_) :-
1163 \+ atom(DefName),!,
1164 add_internal_error('Non-atomic DEFINITION id:',DefName),fail.
1165 external_name(DefName,function,expression,external_function_call,FunName) :-
1166 atom_concat('EXTERNAL_FUNCTION_',FunName,DefName).
1167 external_name(DefName,predicate,predicate,external_pred_call,FunName) :-
1168 atom_concat('EXTERNAL_PREDICATE_',FunName,DefName).
1169 external_name(DefName,substitution,substitution,external_subst_call,FunName) :-
1170 atom_concat('EXTERNAL_SUBSTITUTION_',FunName,DefName).
1171
1172 replace_external_declaration(definition_decl(DefName,expression,DefPos,TypeParams,Decl,_Deps),In,Out) :-
1173 OldDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,FunDef,Deps),
1174 NewDefinition = definition_decl(FunName,ExpectedDefType,Pos,FunParams,ExtCall,Deps),
1175 ( external_name(DefName,_ExtType,ExpectedDefType,ExtCallFunctor,FunName),
1176 ExtCall =.. [ExtCallFunctor,Pos,FunName,FunParams,FunDef,
1177 rewrite_protected(TypeParams),rewrite_protected(Decl)],
1178 selectchk(OldDefinition,In,NewDefinition,Out) ->
1179 assert_external_procedure_used(FunName)
1180 ; external_name(DefName,ExpectedKind,_,_,FunName),
1181 selectchk(definition_decl(FunName,OtherDefType,_OtherPos,_,_,_),In,_,_),!,
1182 % definition found for different type of external function
1183 ajoin(['No DEFINITION associated with external ',ExpectedKind,
1184 ' (but definition as ',OtherDefType,' exists):'],Msg),
1185 add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In
1186 ; external_name(DefName,ExpectedKind,_,_,FunName) ->
1187 % no definition found for external function
1188 ajoin(['No DEFINITION associated with external ',ExpectedKind,':'],Msg),
1189 add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In
1190 ; % no definition found for external function
1191 ajoin(['No DEFINITION associated with:'],Msg),
1192 add_error(replace_external_declaration,Msg,DefName,DefPos), Out=In
1193 ).
1194
1195 :- use_module(external_function_declarations,
1196 [external_function_library/2, safe_external_function_library/2,
1197 get_external_function_definition/3]).
1198 % store external definitions of a given library in the type environment, e.g. for debugging in Repl or VisB
1199 % Library could be "LibraryStrings.def"
1200
1201 store_ext_defs(Library,In,Out) :-
1202 (Library = all_available_libraries
1203 -> findall(extfun(Id,Lib),external_function_library(Id,Lib),Ids)
1204 ; Library = safe_available_libraries
1205 -> findall(extfun(Id,Lib),safe_external_function_library(Id,Lib),Ids)
1206 ; findall(extfun(Id,Library),external_function_library(Id,Library),Ids)
1207 ),
1208 (Ids=[] -> add_warning(store_ext_defs,'No external functions found for library: ',Library) ; true),
1209 foldl(store_ext_def,Ids,In,Out).
1210
1211 store_ext_def(extfun(Id,Library),In,Out) :- env_lookup_type(Id,In,_),!,
1212 debug_println(4,not_storing_ext_def(Id,Library)), % already imported from stdlib or user has other definition
1213 Out=In.
1214 store_ext_def(extfun(FunName,Library),In,Out) :-
1215 ? get_external_function_definition(FunName,Library,DEFINITION),!,
1216 debug_println(4,storing_ext_def(FunName,Library)),
1217 env_store(FunName,DEFINITION,[loc('automatically included',Library,definitions)],In,Out).
1218 store_ext_def(extfun(Id,_),In,Out) :-
1219 add_internal_error('Cannot add external definition: ',Id),
1220 Out=In.
1221
1222
1223 % store which machine promotes which operations
1224 :- dynamic machine_promotes_operations/2, machine_global_order/1.
1225
1226 reset_bmachine_construction :-
1227 retractall(machine_promotes_operations(_,_)),
1228 retractall(machine_global_order(_)),
1229 reset_external_procedure_used.
1230
1231
1232 % maybe this information should be stored somewhere else ??
1233 :- dynamic external_procedure_used/1.
1234 reset_external_procedure_used :- retractall(external_procedure_used(_)).
1235 assert_external_procedure_used(FunName) :-
1236 (external_procedure_used(FunName) -> true ; assertz(external_procedure_used(FunName))).
1237
1238 link_to_refinement(machine,_,_RawMachine,_RefMachines,Local,Local,Errors,Errors).
1239 link_to_refinement(refinement,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :-
1240 link_to_refinement(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout).
1241 link_to_refinement(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :-
1242 link_to_refinement2(implementation,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout).
1243 link_to_refinement2(_MType,Name,RawMachine,RefMachines,Local,NewLocal,Ein,Eout) :-
1244 memberchk(ref(abstraction,AbstractMachine),RefMachines),
1245 copy_constraints(Local,AbstractMachine,NewLocal,Ein,E1),
1246 type_vars_in_refinement(AbstractMachine,NewLocal),
1247 type_refinement_operations(Name,RawMachine,AbstractMachine,NewLocal,E1,Eout).
1248
1249 copy_constraints(Local,AbstractMachine,NewLocal,Ein,Eout) :-
1250 get_section(parameters,Local,LocalParameters),
1251 get_section(parameters,AbstractMachine,AbstractParameters),
1252 check_if_equal_identifiers(LocalParameters,AbstractParameters,Ein,Eout,Local),
1253 get_section(constraints,AbstractMachine,Constraints),
1254 write_section(constraints,Constraints,Local,NewLocal).
1255 check_if_equal_identifiers(Local,Abstract,Ein,Eout,LocalMachine) :-
1256 ( same_length(Local,Abstract) ->
1257 foldl(check_if_equal_identifiers2,Local,Abstract,Ein,Eout)
1258 ;
1259 get_texpr_ids(Abstract,AIDs),
1260 get_machine_name(LocalMachine,MachName),
1261 ajoin(['Refinement ',MachName,' must have same Parameters ', AIDs,' as abstract Machine'],Msg),
1262 Ein = [error(Msg,none)|Eout]
1263 ).
1264 check_if_equal_identifiers2(LParam,AParam,Ein,Eout) :-
1265 get_texpr_id(LParam,LName),
1266 get_texpr_id(AParam,AName),
1267 ( LName = AName ->
1268 % type in refinement is the same as in the abstraction
1269 get_texpr_type(LParam,Type),
1270 get_texpr_type(AParam,Type),
1271 Ein=Eout
1272 ;
1273 get_texpr_pos(LParam,Pos),
1274 ajoin(['Parameter ',LName,' of refinement machine must be ',
1275 AName,' like in the abstract machine'],Msg),
1276 Ein = [error(Msg,Pos)|Eout]
1277 ).
1278
1279 % in case of a refinement, give variables the same type as in the abstract machine
1280 % the same for constants
1281 type_vars_in_refinement(AbstractMachine,ConcreteMachine) :-
1282 pass_type(AbstractMachine,[abstract_variables,concrete_variables],
1283 ConcreteMachine,[abstract_variables,concrete_variables]),
1284 pass_type(AbstractMachine,[abstract_constants,concrete_constants],
1285 ConcreteMachine,[abstract_constants,concrete_constants]).
1286
1287 % pass the type from variables in Sections1 of Machine1 to
1288 % the variables of the same name in Sections2 of Machine2
1289 % Machine1,Machine2: a machine
1290 % Sections1, Sections2: a list of section names
1291 pass_type(Machine1,Sections1,Machine2,Sections2) :-
1292 get_sections_and_append(Sections1,Machine1,Vars1),
1293 get_sections_and_append(Sections2,Machine2,Vars2),
1294 maplist(pass_type2(Vars2),Vars1).
1295 get_sections_and_append([],_M,[]).
1296 get_sections_and_append([Sec|RestSections],M,R) :-
1297 get_section(Sec,M,L), append(L,Rest,R),
1298 get_sections_and_append(RestSections,M,Rest).
1299 pass_type2(DstVariables,SrcVariable) :-
1300 get_texpr_id(SrcVariable,Id),
1301 get_texpr_id(DstVariable,Id),
1302 ( memberchk(DstVariable,DstVariables) ->
1303 get_texpr_type(DstVariable,Type),
1304 get_texpr_type(SrcVariable,Type)
1305 ;
1306 true).
1307
1308
1309 % in case of a refinement, check if the defined operations are already defined
1310 % in the abstract machine and copy that type.
1311 type_refinement_operations(MName,RawMachine,AbstractMachine,Local,Ein,Eout) :-
1312 get_operation_identifiers(RawMachine,Operations),
1313 type_refinement_operations2(Operations,MName,Local,AbstractMachine,Ein,Eout).
1314 type_refinement_operations2([],_,_,_AbstractMachine,Errors,Errors).
1315 type_refinement_operations2([Op|Rest],MName,M,AbstractMachine,Ein,Eout) :-
1316 get_abstract_operation_name_wo_infos(Op,AOp),
1317 %print(treating_refines_operation(Op,AOp)),nl,
1318 get_texpr_pos(Op,Pos),
1319 % look up the abstract definition
1320 get_abstract_op(AOp,MName,AbstractMachine,Pos,Ein,E1),
1321 % store the type in the identifier section
1322 copy_texpr_wo_info(Op,SOp),
1323 get_section(promoted,M,Operations),
1324 memberchk(SOp, Operations),
1325 % do the rest
1326 type_refinement_operations2(Rest,MName,M,AbstractMachine,E1,Eout).
1327 % looks up the type of the operator in an abstract machine
1328 get_abstract_op(Op,_,Abstraction,_,Errors,Errors) :-
1329 % look for the operation in promoted and unpromoted
1330 ? ( get_section(promoted,Abstraction,AbstractOps), member(Op,AbstractOps)
1331 ; get_section(unpromoted,Abstraction,AbstractOps), member(Op,AbstractOps) ),
1332 % forget alternatives
1333 !.
1334 get_abstract_op(Op,_,_Abstraction,_Pos,Errors,Errors) :-
1335 % we might allow new operations
1336 get_preference(allow_new_ops_in_refinement,true),!, % ALLOW_NEW_OPERATIONS_IN_REFINEMENT
1337 get_texpr_type(Op,op(_,_)).
1338 get_abstract_op(Op,MName,AbstractMachine,Pos,[warning(Msg,Pos)|Eout],Eout) :-
1339 % in case we do not find the operation, store an error
1340 get_texpr_id(Op,op(Id)),
1341 get_machine_name(AbstractMachine,Name),
1342 ajoin(['operation ', Id, ' from ', MName, ' is not defined in the abstract machine ',Name,
1343 ' (set ALLOW_NEW_OPERATIONS_IN_REFINEMENT to TRUE to allow this)'], Msg).
1344 % copy a typed expression without the additional information (just expression and type)
1345 copy_texpr_wo_info(A,B) :-
1346 % copy the expression and type, the additional information may be different
1347 get_texpr_expr(A,Expr),get_texpr_expr(B,Expr),
1348 get_texpr_type(A,Type),get_texpr_type(B,Type).
1349
1350 get_abstract_operation_name_wo_infos(b(_,Type,Infos),Res) :-
1351 memberchk(refines_operation(RefID),Infos),!, % renaming occurs:
1352 Res = b(identifier(op(RefID)),Type,_).
1353 get_abstract_operation_name_wo_infos(ID,Copy) :- copy_texpr_wo_info(ID,Copy).
1354
1355 create_id_sections(Header,RawMachine,Name) -->
1356 create_id_sections_header(Header),
1357 %{print(created_header(Name)),nl},
1358 create_set_sections(RawMachine,Name),
1359 %{print(created_set(Name)),nl},
1360 create_constants_sections(RawMachine),
1361 %{print(created_constants(Name)),nl},
1362 create_variables_sections(RawMachine),
1363 %{print(created_variables(Name)),nl},
1364 create_operations_sections(RawMachine).
1365
1366 extract_parameter_types(MachineRefs,ParameterTypes) :-
1367 maplist(extract_parameter_types2,MachineRefs,ParameterTypesL),
1368 append(ParameterTypesL,ParameterTypes).
1369 extract_parameter_types2(ref(_,Machine),ParameterTypes) :-
1370 get_section(parameters,Machine,VisibleParams),
1371 get_section(internal_parameters,Machine,InternalParams),
1372 append(VisibleParams,InternalParams,Params),
1373 include(is_a_parameter_set,Params,ParameterSets),
1374 maplist(get_texpr_set_type,ParameterSets,ParameterTypes).
1375 is_a_parameter_set(TExpr) :-
1376 get_texpr_info(TExpr,Info),
1377 memberchk(parameter_set,Info).
1378
1379 type_sections(RawMachine,MachineType,RefMachines,NonGroundExceptions,Name,Ein,Eout) -->
1380 {debug_stats('TYPING CONSTRAINTS'(Name))},
1381 type_constraints(MachineType,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,E1),
1382 % Maybe the VALUES section must be moved up later because it may be used to
1383 % substitute types (e.g. deferred sets to integers) for later use
1384 {debug_stats('TYPING PROPERTIES'(Name))},
1385 type_section_with_single_predicate(properties,Name,[constants],MachineType,RawMachine,RefMachines,NonGroundExceptions,E1,E2),
1386 {debug_stats('TYPING INVARIANT'(Name))},
1387 type_section_with_single_predicate(invariant,Name,[variables],MachineType,RawMachine,RefMachines,NonGroundExceptions,E2,E3),
1388 {debug_stats('TYPING ASSERTIONS'(Name))},
1389 type_section_with_predicate_list(assertions,[],MachineType,RawMachine,RefMachines,NonGroundExceptions,E3,E4),
1390 {debug_stats('TYPING INITIALISATION'(Name))},
1391 type_initialisation_section(RawMachine,Name,MachineType,RefMachines,NonGroundExceptions,E4,E5),
1392 {debug_stats('TYPING OPERATIONS'(Name))},
1393 type_operations_section(RawMachine,MachineType,RefMachines,NonGroundExceptions,E5,Eout),
1394 {debug_stats('FINISHED TYPING SECTIONS'(Name))}.
1395
1396 % skip this section, it is copied from the abstract machine and
1397 % does not need to be typed again
1398 type_constraints(refinement,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !.
1399 type_constraints(implementation,_,_RawMachine,_RefMachines,_NonGroundExceptions,Errors,Errors) --> !.
1400 type_constraints(machine,Name,RawMachine,RefMachines,NonGroundExceptions,Ein,Eout) -->
1401 % if the machine is a dummy machine (in presence of a not included seen or used
1402 % machine), we must omit the check that the (lower case) parameters are all typed.
1403 % We can assume that they are properly typed by the included machine.
1404 {(is_dummy_machine(RawMachine) -> IdsToType = [] ; IdsToType = [parameters])},
1405 type_section_with_single_predicate(constraints,Name,IdsToType,machine,
1406 RawMachine,RefMachines,NonGroundExceptions,Ein,Eout).
1407
1408 ?is_dummy_machine(RawMachine) :- member(is_dummy,RawMachine),!.
1409
1410 % Header: Parameters
1411 create_id_sections_header(machine_header(_,_,Parameters),Old,New) :-
1412 write_section(parameters,TParams,Old,New),
1413 maplist(create_id_section_parameter,Parameters,TParams).
1414 create_id_section_parameter(Param,TParam) :-
1415 Expr=identifier(Name),
1416 ext2int_with_pragma(Param,Expr,_,Type,Expr,[ParameterType],TParam),
1417 ( is_upper_case(Name) ->
1418 ParameterType = parameter_set,
1419 Type = set(_)
1420 ;
1421 ParameterType = parameter_scalar).
1422 is_upper_case(Name) :- \+ atom(Name),!, add_internal_error('Illegal call:', is_upper_case(Name)),fail.
1423 is_upper_case(Name) :- atom_codes(Name,[C|_]),
1424 memberchk(C,"ABCDEFGHIJKLMNOPQRSTUVWXYZ").
1425
1426 % Body: Sets
1427 create_set_sections(Sections,MachineName) -->
1428 write_section(deferred_sets,DeferredSets),
1429 write_section(enumerated_sets,EnumeratedSets),
1430 write_section(enumerated_elements,EnumeratedElements),
1431 {optional_rawmachine_section(sets,Sections,[],Sets),
1432 split_list(is_deferred_set_element,Sets,RawDeferredSets,RawEnumeratedSets),
1433 maplist(create_deferred_set_section(MachineName),RawDeferredSets,DeferredSets),
1434 maplist(create_enumerated_set_section(Sections,MachineName),
1435 RawEnumeratedSets,EnumeratedSets,LEnumeratedElements),
1436 append(LEnumeratedElements,EnumeratedElements)}.
1437 is_deferred_set_element(AstElem) :- has_functor(AstElem,deferred_set,_).
1438 create_deferred_set_section(MachineName,DS,TExpr) :-
1439 unwrap_opt_description(DS,deferred_set(Pos,I),TInfos),
1440 Infos = [given_set,def(deferred_set,MachineName)|TInfos],
1441 create_global_id(I,Pos,Infos,TExpr).
1442 create_enumerated_set_section(Sections,MachineName,ES,TExpr,Elements) :-
1443 unwrap_opt_description(ES,EnumSetList,TInfos),
1444 create_enum_set_aux(EnumSetList,Sections,MachineName,TInfos,TExpr,Elements).
1445
1446 create_global_id(identifier(_,Id),Pos,Infos,TExpr) :- !,
1447 add_warning(bmachine_construction,'Identifier unexpectedly not atomic: ',Id,Pos), % happened e.g. in ANTLR parser
1448 create_identifier(Id,Pos,set(global(Id)),Infos,TExpr).
1449 create_global_id(Id,Pos,Infos,TExpr) :- !,
1450 create_identifier(Id,Pos,set(global(Id)),Infos,TExpr).
1451
1452 create_enum_set_aux(enumerated_set(Pos,I,Elems),_,MachineName,TInfos,TExpr,Elements) :- !,
1453 % regular case I = {Elems1, ...}
1454 Infos = [given_set,def(enumerated_set,MachineName)|TInfos],
1455 create_global_id(I,Pos,Infos,TExpr),
1456 maplist(create_enum_set_element(I,MachineName),Elems,Elements).
1457 create_enum_set_aux(enumerated_set_via_def(Pos,I,ElemsDEF),Sections,MachineName,TInfos,TExpr,Elements) :- !,
1458 % we have the case I = ElemsDEF and DEFINITIONS ElemsDEF == {Elems1, ...}
1459 Infos = [given_set,def(enumerated_set,MachineName)|TInfos],
1460 create_global_id(I,Pos,Infos,TExpr),
1461 (optional_rawmachine_section(definitions,Sections,[],Defs),
1462 member(expression_definition(DPos,ElemsDEF,Paras,DefBody),Defs)
1463 -> (Paras \= []
1464 -> add_error(bmachine_construction,
1465 'DEFINITION for enumerated set elements must not have parameters:',ElemsDEF,DPos),
1466 Elements=[]
1467 ; DefBody = set_extension(_,Elems),
1468 maplist(create_enum_set_element(I,MachineName),Elems,Elements)
1469 -> true
1470 ; add_error(bmachine_construction,
1471 'DEFINITION for enumerated set elements must be of the form {El1,El2,...}:',ElemsDEF,DPos),
1472 Elements=[]
1473 )
1474 ; add_error(bmachine_construction,'No DEFINITION for enumerated set elements found:',ElemsDEF,Pos),
1475 Elements=[]
1476 ).
1477 create_enum_set_aux(E,_,_,_,_,_) :- add_internal_error('Illegal enumerated set:',E),fail.
1478
1479
1480 % deal with optional description(Pos,Desc,A) wrapper
1481 has_functor(description(_,_Desc,A),Functor,Arity) :- !, functor(A,Functor,Arity).
1482 has_functor(A,Functor,Arity) :- functor(A,Functor,Arity).
1483
1484 % remove description wrapper and generate info field
1485 unwrap_opt_description(Pragma,Res,Infos) :-
1486 unwrap_pragma(Pragma,Expr,I),!, Res=Expr,Infos=I.
1487 unwrap_opt_description(A,A,[]).
1488
1489 % new parser now has specific position info here:
1490 unwrap_desc_pragma(description_text(_Pos,Desc),Res) :- !, Res=Desc.
1491 unwrap_desc_pragma(D,D).
1492
1493
1494 create_enum_set_element(Id,MachineName,Ext,Elem) :-
1495 (Id=identifier(none,RID)
1496 -> Type=global(RID), add_warning(bmachine_construction,'Unexpected non-atomic global set id: ',RID)
1497 ; Type=global(Id)),
1498 ext2int_with_pragma(Ext,Expr,_Pos,Type,Expr,[enumerated_set_element,def(enumerated_element,MachineName)],Elem).
1499
1500 create_identifier(Id,Pos,Type,Infos,TExpr) :-
1501 create_texpr(identifier(Id),Type,[nodeid(Pos)|Infos],TExpr).
1502
1503 % Constants
1504 create_constants_sections(RawMachine) -->
1505 create_section_identifiers(constants,concrete_constants,RawMachine),
1506 create_section_identifiers(abstract_constants,abstract_constants,RawMachine).
1507 % Variables
1508 create_variables_sections(RawMachine) -->
1509 create_section_identifiers(concrete_variables,concrete_variables,RawMachine),
1510 create_section_identifiers(variables,abstract_variables,RawMachine).
1511
1512 % Freetypes: Treat them as additional constants, plus add entries in the "freetypes"
1513 % section of the resulting machine
1514 create_freetypes(RawMachine,MType,RefMachines,Old,New,Ein,Eout) :-
1515 optional_rawmachine_section(freetypes,RawMachine,[],RawFreetypes),
1516 create_freetypes2(RawFreetypes,MType,[ref(local,Old)|RefMachines],Old,New,Ein,Eout).
1517 create_freetypes2([],_MType,_RefMachines,M,M,E,E) :- !.
1518 create_freetypes2(RawFreetypes,MType,RefMachines,Old,New,Ein,Eout) :-
1519 % we need the NonGroundExceptions for type checking
1520 extract_parameter_types(RefMachines,NonGroundExceptions),
1521 % create identifiers in the constants section
1522 maplist(create_ids_for_freetype,RawFreetypes,IdsFreetypes),
1523 % we just combined the results to keep the numbers of arguments low (too much for maplist)
1524 maplist(split_ft,IdsFreetypes,IdentifiersL,Freetypes),
1525 append(IdentifiersL,Identifiers),
1526 % create properties for each freetype
1527 foldl(create_properties_for_freetype(MType,RefMachines,NonGroundExceptions,Identifiers),
1528 RawFreetypes,IdsFreetypes,PropertiesL,Ein,Eout),
1529 conjunct_predicates(PropertiesL,Properties),
1530 (debug_mode(off) -> true
1531 ; format('Created PROPERTIES for FREETYPES:~n',[]), translate:nested_print_bexpr(Properties),nl),
1532 append_to_section(abstract_constants,Identifiers,Old,Inter),
1533 conjunct_to_section(properties,Properties,Inter,Inter2),
1534 write_section(freetypes,Freetypes,Inter2,New).
1535
1536 split_ft(ft(Ids,Freetype),Ids,Freetype).
1537
1538
1539 create_ids_for_freetype(FT,ft([TId|TCons],freetype(Id,Cases))) :-
1540 is_freetype_declaration(FT,_Pos,Id,_TypeParams,Constructors),
1541 !,
1542 create_typed_id_with_given_set_info(Id,set(freetype(Id)),TId),
1543 maplist(create_ids_for_constructor(Id),Constructors,TCons,Cases).
1544 create_ids_for_freetype(FT,_) :-
1545 add_internal_error('Illegal freetype term:',create_ids_for_freetype(FT,_)),fail.
1546
1547 % add given_set info so that is_just_type3 can detect this as a type
1548 create_typed_id_with_given_set_info(IDName,Type,b(identifier(IDName),Type,[given_set])).
1549
1550 % deconstruct a .prob Prolog encoding of a freetype declaration
1551 % new versions of parser generate freetype parameters
1552 is_freetype_declaration(freetype(Pos,Id,Constructors),Pos,Id,[],Constructors).
1553 is_freetype_declaration(freetype(Pos,Id,TypeParams,Constructors),Pos,Id,TypeParams,Constructors) :-
1554 (TypeParams=[] -> true ; add_warning(bmachine_construction,'Not yet supporting freetype parameters:',Id,Pos)).
1555
1556 create_ids_for_constructor(Id,constructor(_Pos,Name,_Arg),TCons,case(Name,Type)) :-
1557 create_typed_id(Name,set(couple(Type,freetype(Id))),TCons).
1558 create_ids_for_constructor(Id,element(_Pos,Name),TCons,case(Name,constant([Name]))) :-
1559 create_typed_id(Name,freetype(Id),TCons).
1560
1561 create_properties_for_freetype(MType,RefMachines,NonGroundExceptions, AllFTIdentifiers,
1562 FREETYPE,ft(Ids,_Freetypes),Properties,Ein,Eout) :-
1563 is_freetype_declaration(FREETYPE,_Pos,Id,_TypeParams,Constructors),
1564 debug_format(9,'Processing freetype ~w (one of ~w)~n',[Id,AllFTIdentifiers]),
1565 % The freetype type
1566 FType = freetype(Id),
1567 % We use the standard type environment of properties...
1568 visible_env(MType,properties,RefMachines,CEnv,Ein,E1),
1569 % ...plus the identifiers of the free type (type name and constructor names)
1570 add_identifiers_to_environment(Ids,CEnv,FEnv0),
1571 % ...plus the identifiers of all free type names (will overwrite Id, but not a problem)
1572 % Note: instead of adding all freetype ids, we could just add the ones preceding Id
1573 add_identifiers_to_environment(AllFTIdentifiers,FEnv0,FEnv),
1574 % We generate a comprehension set for all elements
1575 create_typed_id(Id,set(FType),TId),
1576 create_texpr(equal(TId,TComp),pred,[],FDef),
1577 unique_typed_id("_freetype_arg",FType,Element),
1578 create_recursive_compset([Element],ECond,set(FType),[],RecId,TComp),
1579 create_typed_id(RecId,set(FType),TRecId),
1580 % For each constructor, we generate a definition and a condition for the
1581 % comprehension set above
1582 foldl(create_properties_for_constructor(Id,FEnv,Element,TRecId,NonGroundExceptions),
1583 Constructors,Defs,Conds,E1,Eout),
1584 conjunct_predicates(Conds,ECond),
1585 conjunct_predicates([FDef|Defs],Properties).
1586
1587 /* create_properties_for_constructor(+Env,+Element,+RecId,+NGE,+Constructor,-Def,-Cond,Ein,Eout)
1588 Env: Type environment
1589 Element: A typed identifier "e" that is used in the definition of the freetype set:
1590 ft = {e | e has_freetype_constructor x => e:...}
1591 RecId: The typed identifier that can be used to refer to the freetype set (ft in the
1592 example above
1593 NGE: "Non ground exceptions", needed for type checking when having a parametrized machine
1594 Constructor: The constructor expression as it comes from the parser
1595 (constructor(Pos,Name,ArgSet) or element(Pos,Name))
1596 Def: The predicate that defines the constant for the constructor,
1597 e.g. "cons = {i,o | i:NAT & o = freetype(cons,i)}"
1598 Cond: The predicate that checks the argument of a freetype in the freetype set
1599 (That would be the part "e:..." in the example above.
1600 Ein,Eout: Used for type checker errors
1601 */
1602 create_properties_for_constructor(FID,Env,Element,RecId,NonGroundExceptions,
1603 Constructor,Def,Cond,Ein,Eout) :-
1604 constructor_name(Constructor,Name),
1605 env_lookup_type(Name,Env,CType),
1606 create_properties_for_constructor2(Constructor,Env,NonGroundExceptions,FID,
1607 Element,RecId,CDef,Cond,Ein,Eout),
1608 get_texpr_type(CDef,CType),
1609 create_typed_id(Name,CType,CId),
1610 create_texpr(equal(CId,CDef),pred,[],Def).
1611 constructor_name(element(_Pos,Name),Name).
1612 constructor_name(constructor(_Pos,Name,_Domain),Name).
1613 create_properties_for_constructor2(element(_Pos,Name),_Env,_NonGroundExceptions,FID,
1614 _Element,_RecId,CDef,Cond,Ein,Ein) :-
1615 create_texpr(value(freeval(FID,Name,term(Name))),freetype(FID),[],CDef),
1616 create_texpr(truth,pred,[],Cond).
1617 create_properties_for_constructor2(constructor(_Pos,Name,RArg),Env,NonGroundExceptions,
1618 FID,Element,RecId,CDef,Cond,Ein,Eout) :-
1619 % First, type check the given set of the domain:
1620 btype_ground_dl([RArg],Env,NonGroundExceptions,[set(DType)],[TDomain],Ein,Eout),
1621 % then create the RHS of "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}"
1622 create_definition_for_constructor(Name,TDomain,FID,CDef),
1623 % The check in the freetype comprehension set is of the form
1624 % e "of_freetype_case" Name => "content_of"(e) : Domain
1625 create_texpr(implication(IsCase,DomainTest),pred,[],Cond),
1626 create_texpr(freetype_case(FID,Name,Element),pred,[],IsCase),
1627 create_texpr(freetype_destructor(FID,Name,Element),DType,[],Content),
1628 % all references to the freetype itself are replaced by the recursive reference
1629 replace_id_by_expr(TDomain,FID,RecId,TDomain2),
1630 create_texpr(member(Content,TDomain2),pred,[],DomainTest).
1631
1632 :- use_module(bsyntaxtree,[get_texpr_set_type/2]).
1633
1634 /* The constructor is a function to the freetype, defined with a comprehension set:
1635 The general form is "c = {i,o | i:Domain & o=freetype_constructor(Name,i)}"
1636 create_definition_for_constructor(+Name,+DType,+FID,-CType,-CDef) :-
1637 Name: Name of the constructor
1638 TDomain: The user-specified domain
1639 FID: The name of the free type
1640 CDef: The RHS of the definition "Name = CDef"
1641 */
1642 create_definition_for_constructor(Name,TDomain,FID,CDef) :-
1643 % get the type of the domain:
1644 get_texpr_set_type(TDomain,DType),
1645 % create argument and result identifiers:
1646 unique_typed_id("_constr_arg",DType,TArgId), % was constructor_arg and constructor_res
1647 unique_typed_id("_constr_res",freetype(FID),TResId),
1648 % The comprehension set as a whole
1649 CType = set(couple(DType,freetype(FID))),
1650 create_texpr(comprehension_set([TArgId,TResId],Pred),CType,
1651 [prob_annotation('SYMBOLIC')],CDef),
1652 create_texpr(conjunct(DomainCheck,Construction),pred,[],Pred),
1653 % "i:Domain"
1654 create_texpr(member(TArgId,TDomain),pred,[],DomainCheck),
1655 % "o=freetype_constructor(i)
1656 create_texpr(freetype_constructor(FID,Name,TArgId),freetype(FID),[],FreetypeCons),
1657 create_texpr(equal(TResId,FreetypeCons),pred,[],Construction).
1658
1659 % Operations
1660 create_operations_sections(RawMachine,Old,New) :-
1661 write_section(promoted,OperationIdentifiers,Old,New0),
1662 get_operation_identifiers(RawMachine,operations,OperationIdentifiers),
1663 (allow_local_or_expr_op_calls,
1664 get_operation_identifiers(RawMachine,local_operations,LocOpIDs),
1665 LocOpIDs \= []
1666 -> append_to_section(unpromoted,LocOpIDs,New0,New) % TODO: check that it does not yet exist
1667 ; New = New0
1668 ).
1669
1670 get_operation_identifiers(RawMachine,OperationIdentifiers) :-
1671 get_operation_identifiers(RawMachine,operations,OperationIdentifiers).
1672 get_operation_identifiers(RawMachine,SECTION,OperationIdentifiers) :-
1673 optional_rawmachine_section(SECTION,RawMachine,[],Ops),
1674 maplist(extract_operation_identifier,Ops,OperationIdentifiers).
1675 extract_operation_identifier(Ext,TId) :-
1676 remove_pos(Ext, operation(ExtId,_,_,_)),!,
1677 ext2int_with_pragma(ExtId,identifier(I),_,op(_,_),identifier(op(I)),Infos,TId),
1678 operation_infos(Infos).
1679 extract_operation_identifier(Ext,TId) :-
1680 remove_pos(Ext, refined_operation(ExtId,_,_,RefinesOp,_)),!,
1681 ext2int_with_pragma(ExtId,identifier(I),_,op(_,_),identifier(op(I)),[refines_operation(RefinesOp)|Infos],TId),
1682 operation_infos(Infos).
1683 extract_operation_identifier(Ext,TId) :-
1684 remove_pos(Ext, description_operation(_Desc,RealOp)),!,
1685 extract_operation_identifier(RealOp,TId).
1686 extract_operation_identifier(Ext,_) :- add_internal_error('Unknown operation node:',Ext),fail.
1687
1688 % VALUES section:
1689 % process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut):
1690 % Type-check the VALUES section and change the type of valuated deferred sets, if necessary
1691 % MachineType, RawMachine, NonGroundExceptions: as usual, see other comments
1692 % Min/Mout: The currently constructed machine
1693 % Ein/Eout: The difference list of errors
1694 % RefMin/RefMout: The list of already typechecked machines. These typechecked machines can be
1695 % altered by this predicate because if a deferred set is valuated by an integer set or
1696 % other deferred set, all occurrences of the original type are replaced by the new type,
1697 % even for the already typed machines.
1698 process_values_section(MachineType,RawMachine,NonGroundExceptions,Min/Ein/RefMIn,Mout/Eout/RefMOut) :-
1699 optional_rawmachine_section(values,RawMachine,[],RawValues),
1700 process_values_section_aux(RawValues,MachineType,NonGroundExceptions,
1701 Min/Ein/RefMIn,Mout/Eout/RefMOut).
1702 process_values_section_aux([],_MachineType,_NonGroundExceptions,In,Out) :- !,In=Out.
1703 process_values_section_aux(RawValues,MachineType,NonGroundExceptions,
1704 Min/Ein/RefMin,Mout/Eout/RefMout) :-
1705 debug_stats('TYPING VALUES'),
1706 type_values_section(MachineType,RawValues,RefMin,NonGroundExceptions,Min/Ein,Mout/Eout),
1707 % will be added as additional_property in bmachine
1708 RefMin=RefMout.
1709
1710 type_values_section(MachineType,RawValues,RefMachines,NonGroundExceptions,Min/Ein,Mout/Eout) :-
1711 write_section(values,Values,Min,Mout),
1712 visible_env(MachineType,values_expression,RefMachines,Env,Ein,E1),
1713 % We have to pass an environment that can be modified because in each
1714 % valuation the previously valuated constants can be used.
1715 foldl(extract_values_entry(NonGroundExceptions),RawValues,Values,Env/E1,_ResultingEnv/Eout).
1716
1717 extract_values_entry(NonGroundExceptions, values_entry(POS,ValueID,ValueExpr), Entry,
1718 EnvIn/Ein,EnvOut/Eout) :-
1719 % TODO: There seem to be a lot of additional constraints for valuations in VALUES that are not
1720 % yet handled here
1721 btype_ground_dl([ValueExpr],EnvIn,NonGroundExceptions,[Type],[TExpr],Ein,Eout),
1722 clean_up(TExpr,[],CTExpr), % ensure we remove things like mult_or_cart/2
1723 create_identifier(ValueID,POS,Type,[valuated_constant],TypedID),
1724 create_texpr(values_entry(TypedID,CTExpr),values_entry,[nodeid(POS)],Entry),
1725 debug_println(9,valued_constant(ValueID)),
1726 EnvOut=EnvIn.
1727 %add_identifiers_to_environment([TypedID],EnvIn,EnvOut). % ideally we should register the new type of TypedID
1728 % However: ProB can currently only process VALUES clauses where the type does not change
1729
1730 % type_section_with_single_predicate(+Sec,+Name,+SectionsToType,+MachineType,+Sections,
1731 % +RefMachines,+NonGroundExceptions,+Ein,-Eout,+Old,-New):
1732 % Type a section such as INVARIANT, PROPERTIES, CONSTRAINTS with a single predicate
1733 % Sec: section name in the raw (untyped) machine (e.g. invariant)
1734 % Name: name of machine from which this section comes
1735 % SectionsToType: list of section names that contain identifiers that must be typed
1736 % by this predicate (e.g. all variables must be typed by the invariant)
1737 % MachineType: machine type (machine, refinement, ...)
1738 % Sections: list of sections representing the raw (untyped) machine
1739 % RefMachines: list of already typed machines
1740 % NonGroundExceptions: list of types that may be not ground because the concrete type
1741 % is determinded by machine parameter
1742 % Ein/Eout: difference list of errors
1743 % Old/New: the new typed section is added (by conjunction) to the machine
1744 type_section_with_single_predicate(Sec,Name,SectionsToType,MachineType,Sections,
1745 RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :-
1746 optional_rawmachine_section(Sec,Sections,truth(none),Predicate),
1747 ( Predicate = truth(_) ->
1748 % even if there is no content, we must check if all identifiers are typed
1749 check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout),
1750 Old=New
1751 ;
1752 get_machine_infos(Sections,Infos),
1753 toplevel_raw_predicate_sanity_check(Sec,Name,Predicate,Infos),
1754 type_predicates(Sec,SectionsToType,MachineType,[Predicate],RefMachines,NonGroundExceptions,
1755 [Typed],Ein,Eout),
1756 conjunct_to_section(Sec,Typed,Old,New)
1757 ),
1758 !.
1759 type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_) :-
1760 add_internal_error('type_section_with_single_predicate failed',
1761 type_section_with_single_predicate(Sec,Name,SectsToType,MchType,_,_,_,_,_,_,_)),
1762 fail.
1763
1764 % get some infos relevant for sanity check:
1765 get_machine_infos(Sections,Infos) :-
1766 ((rawmachine_section_exists(concrete_variables,Sections) ; rawmachine_section_exists(abstract_variables,Sections))
1767 -> Infos = [has_variables|I1] ; Infos = I1),
1768 ((rawmachine_section_exists(concrete_constants,Sections) ; rawmachine_section_exists(abstract_constants,Sections))
1769 -> I1 = [has_constants] ; I1 = []).
1770
1771 % Type a section with multiple predicates, such as ASSERTIONS
1772 type_section_with_predicate_list(Sec,SectionsToType,MachineType,Sections,
1773 RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :-
1774 write_section(Sec,Typed,Old,New),
1775 optional_rawmachine_section(Sec,Sections,[],Predicates),
1776 type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout),
1777 !.
1778 type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New) :-
1779 add_internal_error('type_section_with_predicate_list failed',
1780 type_section_with_predicate_list(Sec,SectsToType,MchType,Sects,RefMchs,NonGrndExc,Ein,Eout,Old,New)),
1781 fail.
1782
1783
1784 type_predicates(_Sec,SectionsToType,_MachineType,[],RefMachines,NonGroundExceptions,Typed,Ein,Eout) :-
1785 !,Typed=[],
1786 check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout).
1787 type_predicates(Sec,SectionsToType,MachineType,Predicates,RefMachines,NonGroundExceptions,Typed,Ein,Eout) :-
1788 visible_env(MachineType, Sec, RefMachines, Env, Ein, E1),
1789 same_length(Predicates,Types),maplist(is_pred_type,Types),
1790 btype_ground_dl_in_section(Sec,Predicates,Env,NonGroundExceptions,Types,Typed1,E1,E2),
1791 mark_with_section(Sec,Typed1,Typed),
1792 check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,E2,Eout),
1793 (no_perrors_occured(Ein,Eout)
1794 -> perform_post_static_check(Typed) % only run if no type errors, it makes use of find_typed_identifier_uses
1795 ; true
1796 ).
1797
1798 no_perrors_occured(Ein,Eout) :- Ein==Eout,!.
1799 no_perrors_occured([H|T],Eout) :- nonvar(H),not_a_perror(H),no_perrors_occured(T,Eout).
1800
1801 not_a_perror(warning(_,_)).
1802 % other possible values: error(Msg,Pos), internal_error(Msg,Pos); see get_perror/2
1803
1804 % check if the identifiers that should be typed by this section are completly typed
1805 check_if_all_ids_are_typed([],_RefMachines,_NonGroundExceptions,Ein,Eout) :- !,Ein=Eout.
1806 check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout) :-
1807 memberchk(ref(local,Local),RefMachines),
1808 get_all_identifiers(SectionsToType,Local,IdentifiersToType),
1809 check_ground_types_dl(IdentifiersToType, NonGroundExceptions, Ein, Eout).
1810
1811
1812 mark_with_section(Sec,In,Out) :-
1813 maplist(mark_with_section2(Sec),In,Out).
1814 mark_with_section2(Sec,In,Out) :-
1815 remove_bt(In,conjunct(A,B),conjunct(NA,NB),Out),!,
1816 mark_with_section2(Sec,A,NA), mark_with_section2(Sec,B,NB).
1817 mark_with_section2(Sec,In,Out) :-
1818 add_texpr_infos(In,[section(Sec)],Out).
1819
1820 type_initialisation_section(Sections,Name,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :-
1821 write_section(initialisation,Initialisation,Old,New),
1822 ( rawmachine_section(initialisation,Sections,Init) ->
1823 visible_env(MType, initialisation, RefMachines, InitEnv, Ein, E1),
1824 btype_ground_dl([Init],InitEnv,NonGroundExceptions,[subst],[TypedInit],E1,Eout),
1825 Initialisation=[init(Name,TypedInit)]
1826 ;
1827 Ein=Eout,
1828 Initialisation=[]).
1829
1830 :- use_module(library(ugraphs)).
1831
1832 type_operations_section(Sections,MType,RefMachines,NonGroundExceptions,Ein,Eout,Old,New) :-
1833 write_section(operation_bodies,Operations,Old,New),
1834 visible_env(MType, operation_bodies, RefMachines, Env, Ein, E1),
1835 optional_rawmachine_section(operations,Sections,[],Ops1),
1836 optional_rawmachine_section(local_operations,Sections,[], Ops2),
1837 append(Ops2,Ops1,Ops),
1838 topological_sort(Ops,Env,SOps),
1839 (debug_mode(off) -> true ; length(SOps,NrOps),debug_stats(finished_topological_sorting(NrOps))),
1840 same_length(SOps,Types), maplist(is_op_type,Types),
1841 btype_ground_dl(SOps,Env,NonGroundExceptions,Types,Operations,E1,Eout),!.
1842
1843 allow_local_or_expr_op_calls :-
1844 (get_preference(allow_local_operation_calls,true) -> true
1845 ; get_preference(allow_operation_calls_in_expr,true)).
1846 % at the moment ProB allows local calls inside expressions, independently of the allow_local_operation_calls preference
1847
1848 % perform a topological sort of the operations: treat called operation before calling operation
1849 % only relevant when allow_local_operation_calls is set to true
1850 topological_sort(Ops,Env,SortedOps) :-
1851 allow_local_or_expr_op_calls,
1852 findall(OtherID-ID, (member(Op,Ops),op_calls_op(Op,Env,ID,OtherID)),Edges),
1853 % print(edges(Edges)),nl,
1854 % TO DO: maybe only store edges where OtherID also appears in Ops (i.e., call within same machine)
1855 Edges \= [],
1856 !,
1857 findall(ID,(member(operation(_,RawID,_,_,_),Ops),raw_id(RawID,ID)),Vertices), %print(vertices(Vertices)),nl,
1858 vertices_edges_to_ugraph(Vertices,Edges,Graph),
1859 (top_sort(Graph,Sorted)
1860 -> sort_ops(Sorted,Ops,SortedOps)
1861 ; get_preference(allow_operation_calls_in_expr,true) ->
1862 add_warning(topological_sort,'Mutual recursion or cycle in the (local) operation call graph, this may cause problems computing reads information: ',Edges),
1863 SortedOps=Ops
1864 % not necessarily a problem, because operations called in expressions are not allowed to modify the state
1865 % TODO: however, we may have an issue with computing reads information correctly for mutual recursion !?
1866 % direct recursion should be ok
1867 ; add_error(topological_sort,'Cycle in the (local) operation call graph: ',Edges),
1868 SortedOps=Ops).
1869 topological_sort(Ops,_,Ops).
1870
1871 sort_ops([],Ops,Ops). % Ops should be []
1872 sort_ops([OpID|T],Ops,Res) :-
1873 raw_op_id(Op1,OpID),
1874 (select(Op1,Ops,TOps)
1875 -> Res = [Op1|TSOps], sort_ops(T,TOps,TSOps)
1876 ; % operation from another machine
1877 % print(could_not_find(OpID,Ops)),nl,
1878 sort_ops(T,Ops,Res)
1879 ).
1880
1881 is_op_type(op(_,_)).
1882 is_pred_type(pred).
1883
1884 % compute which other operations are directly called
1885 op_calls_op(operation(_,RawID,_,_,RawBody),Env,ID,OtherID) :- raw_id(RawID,ID),
1886 raw_body_calls_operation(RawBody,ID,Env,OtherID).
1887
1888 raw_body_calls_operation(RawBody,ID,Env,OtherID) :-
1889 raw_member(OpCall,RawBody),
1890 raw_op_call(OpCall,ID,Env,RawOtherID), raw_id(RawOtherID,OtherID).
1891
1892 raw_op_call(operation_call(_,RawOtherID,_,_),_,_, RawOtherID).
1893 raw_op_call(operation_call_in_expr(_,RawOtherID,_),ID,_, RawOtherID) :-
1894 \+ raw_id(RawOtherID,ID). % we do not look at direct recursion: it poses no problem for computing reads/writes info
1895 raw_op_call(function(_,RawOtherID,_), ID, Env, RawOtherID) :- % function calls possibly not yet translated to operation_call_in_expr
1896 get_preference(allow_operation_calls_in_expr,true),
1897 \+ raw_id(RawOtherID,ID), % direct recursion ok
1898 btypechecker:is_operation_call(RawOtherID,Env).
1899 raw_op_call(identifier(Pos,OtherID), ID, Env, RawOtherID) :- % possible operation call in expr without arguments
1900 OtherID \= ID, % direct recursion ok
1901 get_preference(allow_operation_calls_in_expr,true),
1902 RawOtherID = identifier(Pos,OtherID),
1903 btypechecker:is_operation_call(RawOtherID,Env).
1904
1905
1906 raw_op_id(operation(_,RawID,_,_,_RawBody),ID) :- raw_id(RawID,ID).
1907 raw_id(identifier(_,ID),ID).
1908
1909 % a utility function to work on the raw AST Functor(POS,Arg1,...,Argn)
1910 % this will not be able to look inside DEFINITIONS !
1911 % TO DO: deal with more raw substitutions which have list arguments
1912 raw_member(X,X).
1913 raw_member(X,parallel(_,List)) :- !, member(Term,List), raw_member(X,Term).
1914 raw_member(X,sequence(_,List)) :- !, member(Term,List), raw_member(X,Term).
1915 raw_member(X,[H|T]) :- !, (raw_member(X,H) ; raw_member(X,T)).
1916 raw_member(X,Term) :- compound(Term), Term =.. [_Functor,_Pos|Args],
1917 member(A,Args), raw_member(X,A).
1918
1919
1920 create_section_identifiers(Section,DestSection,RawMachine,Old,New) :-
1921 write_section(DestSection,Vars,Old,New),
1922 optional_rawmachine_section(Section,RawMachine,[],Identifiers),
1923 create_section_ids2(Identifiers,[],Vars,DestSection,New).
1924
1925 create_section_ids2([],_,[],_,_).
1926 create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :-
1927 expand_definition_to_variable_list(Ext,MachSections,List),!,
1928 append(List,Rest,NewList),
1929 create_section_ids2(NewList,Infos,Res,DestSection,MachSections).
1930 create_section_ids2([Ext|Rest],Infos,Res,DestSection,MachSections) :-
1931 create_section_id(Ext,Infos,DestSection,TId),
1932 ( TId = error(Msg,Term,Pos) ->
1933 Res = TRest, add_error(bmachine_construction,Msg,Term,Pos)
1934 ;
1935 Res = [TId|TRest]),
1936 create_section_ids2(Rest,Infos,TRest,DestSection,MachSections).
1937 create_section_id(Ext,Infos,DestSection,TId) :-
1938 (unwrap_pragma(Ext,Ext2,PragmaInfos) -> append(PragmaInfos,Infos,FullInfos)
1939 ; Ext2=Ext, FullInfos=Infos),
1940 I=identifier(_),
1941 ( ext2int(Ext2,I,_Pos,_Type,I,FullInfos,TId) ->
1942 true
1943 ; Ext2 = definition(POSINFO,ID,_) ->
1944 TId = error('Trying to use DEFINITION name as identifier: ',
1945 (ID,within(DestSection)), POSINFO)
1946 ;
1947 TId = error('Illegal identifier: ',
1948 (Ext2,within(DestSection)), Ext2)
1949 ).
1950
1951 % support using DEFINITIONS which are variable lists;
1952 % currently for ProB parser you need to write VARS == (x,y,..) for Atelier-B: VARS == x,y,..
1953 expand_definition_to_variable_list(definition(_POSINFO,ID,_),MachSections,List) :-
1954 get_section(definitions,MachSections,Defs),
1955 member(definition_decl(ID,expression,_InnerPos,[],RawExpr,_Deps),Defs),
1956 extract_identifier_list(RawExpr,List,[]).
1957
1958 % convert a raw tuple into a raw identifier list:
1959 extract_identifier_list(identifier(Pos,ID)) --> [identifier(Pos,ID)].
1960 extract_identifier_list(couple(_,List)) -->
1961 extract_identifier_list(List).
1962 extract_identifier_list([]) --> [].
1963 extract_identifier_list([H|T]) --> extract_identifier_list(H), extract_identifier_list(T).
1964
1965
1966 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1967 % sort the machines topologically
1968
1969 % can be used to store the result:
1970 assert_machine_order(Order) :-
1971 retractall(machine_global_order(_)),
1972 debug_print(9,machine_global_order(Order)),
1973 assertz(machine_global_order(Order)).
1974
1975 get_mach_position(Order,M,Ref,Pos-mch(M,Ref)) :-
1976 get_machine_name(M,Name),
1977 ? (nth1(Pos,Order,Name) -> true
1978 ; add_internal_error('Unknown machine:',Name:Order),
1979 Pos=0).
1980 get_machine(_-mch(M,_),M). % re-extract info after sorting
1981 get_reference(_-mch(_,R),R).
1982
1983 :- use_module(library(samsort),[samkeysort/2]).
1984 sort_machines_by_global_order(Machines,SortedMachines) :-
1985 sort_machines_by_global_order(Machines,_,SortedMachines,_).
1986 sort_machines_by_global_order(Machines,Refs,SortedMachines,SortedRefs) :-
1987 machine_global_order(Order),
1988 maplist(get_mach_position(Order),Machines,Refs,KM), % add position so that sorting works
1989 samkeysort(KM,SKM), % for test 925 it is important to keep duplicates and not use sort/2
1990 maplist(get_machine,SKM,SortedMachines),
1991 maplist(get_reference,SKM,SortedRefs),!.
1992 %maplist(get_machine_name,Sorted,SNs),print(sorted(SNs)),nl.
1993 sort_machines_by_global_order(M,R,M,R) :-
1994 add_internal_error('Sorting machines failed:',M).
1995
1996 % perform the actual computation:
1997 machine_order(Machines,Order) :-
1998 machine_dependencies(Machines,Dependencies),
1999 topsort(Dependencies,Order).
2000
2001 % sort the machines topologically
2002 topsort(Deps,Sorted) :-
2003 topsort2(Deps,[],Sorted).
2004 topsort2([],_,[]) :- !.
2005 topsort2(Deps,Known,Sorted) :-
2006 split_list(all_deps_known(Known),Deps,DAvailable,DNotAvailable),
2007 DAvailable = [_|_], % we have new machines available whose dependencies are all known
2008 !,
2009 maplist(dep_name,DAvailable,Available),
2010 append(Available,Known,NewKnown),
2011 append(Available,Rest,Sorted),
2012 topsort2(DNotAvailable,NewKnown,Rest).
2013 topsort2(Deps,_Known,_) :-
2014 member(dep(Name,NameDeps),Deps),
2015 add_error(bmachine_construction,'Could not resolve machine dependencies for: ',Name:depends_on(NameDeps)),
2016 fail.
2017
2018 ?all_deps_known(K,dep(_Name,Deps)) :- sort(Deps,DS),sort(K,KS),subseq0(KS,DS),!.
2019 dep_name(dep(Name,_Deps),Name).
2020
2021 % find dependencies between machines
2022 machine_dependencies(Machines,Dependencies) :-
2023 maplist(machine_dependencies2,Machines,Deps),
2024 sort(Deps,Dependencies).
2025 machine_dependencies2(M,dep(Name,Deps)) :-
2026 get_constructed_machine_name_and_body(M,Name,_,Body),
2027 findall(Ref,
2028 (refines(M,Ref);machine_reference(Body,Ref)),
2029 Deps).
2030
2031 machine_reference(MachineBody,Ref) :-
2032 ? ( member(sees(_,R),MachineBody)
2033 ; member(uses(_,R),MachineBody) ),
2034 member(identifier(_,PrefixRef),R),
2035 split_prefix(PrefixRef,_,Ref).
2036 machine_reference(MachineBody,Ref) :-
2037 ? ( member(includes(_,R),MachineBody)
2038 ? ; member(extends(_,R),MachineBody)
2039 ; member(imports(_,R),MachineBody) ),
2040 ? member(machine_reference(_,PrefixRef,_),R),
2041 split_prefix(PrefixRef,_,Ref).
2042
2043 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2044 % refinements
2045 merge_refinement_and_abstraction(Concrete,RefMachines,Result,Ein,Eout) :-
2046 memberchk(ref(abstraction,Abstraction),RefMachines),
2047 append_sections([sets,concrete_constants,concrete_variables],Abstraction,Concrete,M1),
2048 append_if_new(abstract_constants,Abstraction,M1,M2),
2049 get_section(properties,Abstraction,AbstractProperties),
2050 conjunct_to_section(properties,AbstractProperties,M2,M3),
2051 % now get current invariant Invariant and filter out gluing/linking invariant
2052 % (the linking invariant talks about variables which no longer exist; hence we cannot check it anymore)
2053 select_section(invariant,Invariant,FullConcreteInvariant,M3,M4),
2054 write_section(linking_invariant,LinkingInvariant,M4,Merged),
2055 % we now also copy from the abstraction those invariants which are still valid
2056 get_section(invariant,Abstraction,AbstractInvariant),
2057 filter_abstract_invariant(AbstractInvariant,Concrete,AbsInvariantStillValid),
2058 filter_linking_invariant(Invariant,LinkingInvariant,ConcreteInvariant),
2059 conjunct_predicates([AbsInvariantStillValid,ConcreteInvariant],FullConcreteInvariant),
2060 propagate_abstract_operations(Abstraction,Merged,RefMachines,Result,Ein,Eout).
2061 merge_refinement_and_abstraction(Machine,_,Machine,Errors,Errors).
2062
2063 % append sections from abstract machine to concrete machine:
2064 append_sections(Sections,AbsMachine,Old,New) :-
2065 expand_shortcuts(Sections,AllSections),
2066 append_sections2(AllSections,AbsMachine,Old,New).
2067 append_sections2([],_,M,M).
2068 append_sections2([Section|Rest],AbsMachine,Old,New) :-
2069 get_section(Section,AbsMachine,Content),
2070 append_to_section3(Section,Content,Old,Inter),
2071 append_sections2(Rest,AbsMachine,Inter,New).
2072
2073 append_to_section3(Section,Content,Old,Inter) :- section_can_have_duplicates(Section),!,
2074 append_to_section_and_remove_dups(Section,Content,Old,Inter).
2075 append_to_section3(Section,Content,Old,Inter) :- append_to_section(Section,Content,Old,Inter).
2076
2077 :- assert_must_succeed((create_machine(abs,EA), create_machine(conc,EB),
2078 write_section(abstract_constants,[b(identifier(x),integer,[some_info])],EA,A),
2079 write_section(abstract_constants,[b(identifier(x),integer,[other_info]),
2080 b(identifier(y),integer,[info])],EB,B),
2081 append_if_new(abstract_constants,A,B,ResultM),
2082 get_section(abstract_constants,ResultM,ResultConst),
2083 ResultConst==[b(identifier(x),integer,[other_info]),
2084 b(identifier(y),integer,[info])]
2085 )).
2086
2087 append_if_new(Section,Machine,In,Out) :-
2088 get_section(Section,Machine,Content),
2089 select_section(Section,Old,New,In,Out),
2090 get_texpr_ids(Old,ExistingIds),
2091 exclude(is_in_existing_ids(ExistingIds),Content,NewElements),
2092 append(Old,NewElements,New).
2093 is_in_existing_ids(ExistingIds,TId) :-
2094 get_texpr_id(TId,Id),
2095 memberchk(Id,ExistingIds).
2096
2097 % filter linking and concrete invariant
2098 filter_linking_invariant(Invariant,Linking,Concrete) :-
2099 split_conjuncts(Invariant,Predicates),
2100 split_list(contains_abstraction_refs,Predicates,Linkings,Concretes),
2101 conjunct_predicates(Linkings,Linking),
2102 conjunct_predicates(Concretes,Concrete).
2103
2104
2105 % contains_abstraction_refs can be used on predicates of the current machine: the abstraction info field has been computed for this machine
2106 contains_abstraction_refs(TExpr) :-
2107 syntaxtraversion(TExpr,_,_,Infos,Subs,_),
2108 ( memberchk(abstraction,Infos) % This info field comes from the last argument of visibility/6
2109 -> true
2110 ? ; member(Sub,Subs),
2111 contains_abstraction_refs(Sub)).
2112
2113 % Determine which part of the abstract invariant can be imported into the refinement machine
2114 % TODO: should this be applied to WHILE loop INVARIANTS?
2115 filter_abstract_invariant(AbsInvariant,ConcreteMachine,ConcreteInv) :-
2116 split_conjuncts(AbsInvariant,Predicates),
2117 get_machine_sorted_variables(ConcreteMachine,SortedConcrVars),
2118 filter_abs_invs(Predicates,SortedConcrVars,Concretes),
2119 conjunct_predicates(Concretes,ConcreteInv). %, print('COPY: '), translate:print_bexpr(Concrete),nl.
2120 :- use_module(translate,[translate_bexpression/2]).
2121
2122 filter_abs_invs([],_,[]).
2123 filter_abs_invs([TExpr|TInv],SortedConcrVars,Res) :-
2124 ? contains_abstract_variables2(SortedConcrVars,TExpr,Cause),!,
2125 (silent_mode(on) -> true
2126 ; translate_bexpression(Cause,ID),
2127 ajoin(['Discarding abstract INVARIANT (requires variable "',ID,'"): '],Msg),
2128 add_message(bmachine_construction,Msg,TExpr,Cause)
2129 ),
2130 (adapt_invariant(SortedConcrVars,TExpr,NewTExpr)
2131 -> Res = [NewTExpr|TRes],
2132 add_message(bmachine_construction,'Replaced abstract INVARIANT by: ',NewTExpr,Cause)
2133 ; Res=TRes
2134 ),
2135 filter_abs_invs(TInv,SortedConcrVars,TRes).
2136 filter_abs_invs([TExpr|TInv],SortedConcrVars,[TExpr|TRes]) :-
2137 filter_abs_invs(TInv,SortedConcrVars,TRes).
2138
2139 contains_abstract_variables2(SortedConcrVars,TExpr,Cause) :-
2140 syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_),
2141 ( memberchk(loc(_,_Mch,abstract_variables),Infos) % are there other things that pose problems: abstract_constants ?
2142 -> %print('Abs: '),translate:print_bexpr(TExpr),nl, print(SortedConcrVars),nl,
2143 Cause=TExpr,
2144 \+ ord_member_nonvar_chk(b(Expr,Type,_),SortedConcrVars) % otherwise variable is re-introduced with same type
2145 % in some Event-B models: VARIABLES keyword is used and in refinement VARIABLES are re-listed
2146 % TO DO: check what happens when variable not immediately re-introduced
2147 ? ; member(Sub,Subs),
2148 contains_abstract_variables2(SortedConcrVars,Sub,Cause)
2149 ).
2150
2151 % try and keep part of invariant, e.g., if f:ABS-->Ran translate to f: TYPE +-> Ran
2152 adapt_invariant(SortedConcrVars,b(member(LHS,RHS),pred,I),b(member(LHS,NewRHS),pred,I)) :-
2153 \+ contains_abstract_variables2(SortedConcrVars,LHS,_),
2154 adapt_to_concrete_superset(RHS,SortedConcrVars,NewRHS),
2155 \+ get_texpr_expr(NewRHS,typeset). % not really useful
2156
2157 adapt_to_concrete_superset(b(E,Type,Info),SortedConcrVars,b(NewE,Type,Info)) :-
2158 adapt_super2(E,SortedConcrVars,NewE). % TODO: adapt info fields?
2159 adapt_to_concrete_superset(b(_E,Type,_Info),_SortedConcrVars,b(typeset,Type,[])).
2160 % Range of function remains concrete, Domain is abstract and no longer available:
2161 adapt_super2(PFUN,SortedConcrVars,partial_function(NewDom,RAN)) :-
2162 is_fun(PFUN,partial,DOM,RAN),
2163 \+ contains_abstract_variables2(SortedConcrVars,RAN,_),
2164 adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom).
2165 adapt_super2(TFUN,SortedConcrVars,partial_function(NewDom,RAN)) :-
2166 is_fun(TFUN,total,DOM,RAN),
2167 \+ contains_abstract_variables2(SortedConcrVars,RAN,_),
2168 adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom).
2169 % Domain of function remains concrete, Range is abstract and no longer available:
2170 adapt_super2(PFUN,SortedConcrVars,partial_function(DOM,NewRan)) :-
2171 is_fun(PFUN,partial,DOM,RAN),
2172 \+ contains_abstract_variables2(SortedConcrVars,DOM,_),
2173 adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan).
2174 adapt_super2(TFUN,SortedConcrVars,total_function(DOM,NewRan)) :-
2175 is_fun(TFUN,total,DOM,RAN),
2176 \+ contains_abstract_variables2(SortedConcrVars,DOM,_),
2177 adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan).
2178 adapt_super2(FUN,SortedConcrVars,partial_function(NewDom,NewRan)) :-
2179 is_fun(FUN,_,DOM,RAN),
2180 adapt_to_concrete_superset(DOM,SortedConcrVars,NewDom),
2181 adapt_to_concrete_superset(RAN,SortedConcrVars,NewRan).
2182 % TODO: more cases, intersection(ABS,CONCR) -> CONCR, cartesian_product
2183
2184 is_fun(partial_function(DOM,RAN),partial,DOM,RAN).
2185 is_fun(partial_injection(DOM,RAN),partial,DOM,RAN).
2186 is_fun(partial_surjection(DOM,RAN),partial,DOM,RAN).
2187 is_fun(partial_bijection(DOM,RAN),partial,DOM,RAN).
2188 is_fun(total_function(DOM,RAN),total,DOM,RAN).
2189 is_fun(total_injection(DOM,RAN),total,DOM,RAN).
2190 is_fun(total_surjection(DOM,RAN),total,DOM,RAN).
2191 is_fun(total_bijection(DOM,RAN),total,DOM,RAN).
2192
2193 % ---------------------
2194
2195 get_machine_sorted_variables(Machine,SortedAllVars) :-
2196 get_section(abstract_variables,Machine,AbsVars),
2197 get_section(concrete_variables,Machine,ConcVars),
2198 append(ConcVars,AbsVars,AllVars),
2199 sort(AllVars,SortedAllVars).
2200
2201 split_conjuncts(Expr,List) :-
2202 split_conjuncts2(Expr,List,[]).
2203 split_conjuncts2(Expr) -->
2204 {get_texpr_expr(Expr,conjunct(A,B)),!},
2205 split_conjuncts2(A),
2206 split_conjuncts2(B).
2207 split_conjuncts2(Expr) --> [Expr].
2208
2209 % copy the abstract operations or re-use their preconditions
2210 % TODO: think about copying Initialisation?
2211 propagate_abstract_operations(Abstract,Concrete,RefMachines,Result,Ein,Eout) :-
2212 get_section(promoted,Abstract,APromoted),
2213 get_section(operation_bodies,Abstract,ABodies),
2214 % signature: select_section(SecName,OldContent,NewContent,OldMachine,NewMachine)
2215 select_section(promoted,CPromotedIn,CPromotedOut,Concrete,Concrete2),
2216 select_section(operation_bodies,CBodiesIn,CBodiesOut,Concrete2,Result),
2217 propagate_aops(APromoted,ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout).
2218 propagate_aops([],_ABodies,_RefMachines,CPromoted,CBodies,CPromoted,CBodies,Errors,Errors).
2219 propagate_aops([APromoted|ApRest],ABodies,RefMachines,CPromotedIn,CBodiesIn,CPromotedOut,CBodiesOut,Ein,Eout) :-
2220 get_operation(APromoted,ABodies,AbstractOp),
2221 def_get_texpr_id(APromoted,op(APromotedOpName)),
2222 copy_texpr_wo_info(APromoted,CProm),
2223 ? ( member(CProm,CPromotedIn) ->
2224 debug_format(19,'Refining promoted abstract operation ~w to refinement machine.~n',[APromotedOpName]),
2225 extract_concrete_preconditions(AbstractOp,RefMachines,Pre),
2226 change_operation(APromoted,ConcreteOpOld,ConcreteOpNew,CBodiesIn,CBodiesRest),
2227 add_precondition(Pre,ConcreteOpOld,ConcreteOpNew), % propagate PRE down to concrete operation
2228 CPromotedIn = CPromotedRest,
2229 Ein = E1
2230 % TO DO: do not copy if event is refined at least once with renaming !
2231 ; is_refined_by_some_event(APromotedOpName,CPromotedIn,ConcreteOpName) ->
2232 debug_format(19,'Not copying abstract operation ~w to refinement machine, as it is refined by ~w.~n',[APromotedOpName,ConcreteOpName]),
2233 CPromotedRest=CPromotedIn, CBodiesRest=CBodiesIn,
2234 E1=Ein
2235 ;
2236 debug_format(19,'Copying abstract operation ~w to refinement machine, as it is not refined.~n',[APromotedOpName]),
2237 % TO DO: check that this is also the right thing to do for Atelier-B Event-B
2238 % TO DO: check that the variables are also still there
2239 check_copied_operation(APromoted,AbstractOp,RefMachines,Ein,E1),
2240 append(CPromotedIn,[APromoted],CPromotedRest),
2241 append(CBodiesIn,[AbstractOp],CBodiesRest)
2242 ),
2243 propagate_aops(ApRest,ABodies,RefMachines,CPromotedRest,CBodiesRest,CPromotedOut,CBodiesOut,E1,Eout).
2244
2245 is_refined_by_some_event(AbstractName,CPromotedList,ConcreteName) :-
2246 ? member(TID,CPromotedList),
2247 get_texpr_info(TID,Infos),
2248 memberchk(refines_operation(AbstractName),Infos),
2249 def_get_texpr_id(TID,ConcreteName).
2250
2251 get_operation(TId,Bodies,Operation) :-
2252 select_operation(TId,Bodies,Operation,_BodiesRest).
2253 change_operation(TId,OldOp,NewOp,OldBodies,[NewOp|NewBodies]) :-
2254 select_operation(TId,OldBodies,OldOp,NewBodies).
2255 select_operation(TId,Bodies,Operation,BodiesRest) :-
2256 copy_texpr_wo_info(TId,OpId),
2257 get_texpr_expr(Operation,operation(OpId,_,_,_)),
2258 ? select(Operation,Bodies,BodiesRest),!.
2259
2260 extract_concrete_preconditions(Op,RefMachines,FPre) :-
2261 extract_preconditions_op(Op,Pre),
2262 extract_op_arguments(Op,Args),
2263 conjunction_to_list(Pre,Pres),
2264 % todo: check the "machine" parameter
2265 visible_env(machine,operation_bodies,RefMachines,Env1,_Errors,[]),
2266 store_variables(Args,Env1,Env),
2267 filter_predicates_with_unknown_identifiers(Pres,Env,FPres),
2268 conjunct_predicates(FPres,FPre).
2269
2270 extract_op_arguments(Op,Params) :-
2271 get_texpr_expr(Op,operation(_,_,Params,_)).
2272
2273 extract_preconditions_op(OpExpr,Pre) :-
2274 get_texpr_expr(OpExpr,operation(_,_,_,Subst)),
2275 extract_preconditions(Subst,Pres,_),
2276 conjunct_predicates(Pres,Pre).
2277 extract_preconditions(TExpr,Pres,Inner) :-
2278 get_texpr_expr(TExpr,Expr),
2279 extract_preconditions2(Expr,TExpr,Pres,Inner).
2280 extract_preconditions2(precondition(Pre,Subst),_,[Pre|Pres],Inner) :- !,
2281 extract_preconditions(Subst,Pres,Inner).
2282 extract_preconditions2(block(Subst),_,Pres,Inner) :- !,
2283 extract_preconditions(Subst,Pres,Inner).
2284 extract_preconditions2(_,Inner,[],Inner).
2285
2286 :- use_module(btypechecker,[prime_atom0/2]).
2287 filter_predicates_with_unknown_identifiers([],_Env,[]).
2288 filter_predicates_with_unknown_identifiers([Pred|Prest],Env,Result) :-
2289 ( find_unknown_identifier(Pred,Env,_Id) ->
2290 !,Result = Rrest
2291 ;
2292 Result = [Pred|Rrest]),
2293 filter_predicates_with_unknown_identifiers(Prest,Env,Rrest).
2294 find_unknown_identifier(Pred,Env,Id) :-
2295 get_texpr_id(Pred,Id),!,
2296 \+ env_lookup_type(Id,Env,_),
2297 (prime_atom0(UnprimedId,Id)
2298 -> % we have an identifier with $0 at end
2299 \+ env_lookup_type(UnprimedId,Env,_) % check unprimed identifier also unknown
2300 ; true).
2301 find_unknown_identifier(Pred,Env,Id) :-
2302 syntaxtraversion(Pred,_,_,_,Subs,Names),
2303 store_variables(Names,Env,Subenv),
2304 find_unknown_identifier_l(Subs,Subenv,Id).
2305 find_unknown_identifier_l([S|_],Env,Id) :-
2306 find_unknown_identifier(S,Env,Id),!.
2307 find_unknown_identifier_l([_|Rest],Env,Id) :-
2308 find_unknown_identifier_l(Rest,Env,Id).
2309
2310 :- use_module(library(ordsets),[ord_union/3]).
2311 % we add a precondition to an existing operation
2312 % Note: we need to update the reads info computed by the type checker (compute_accessed_vars_infos_for_operation)
2313 add_precondition(b(truth,_,_),Old,New) :- !, Old=New.
2314 add_precondition(Pre,b(Old,T,I),b(New,T,I2)) :-
2315 Old=operation(Id,Res,Params,Subst),
2316 New=operation(Id,Res,Params,NewSubst),
2317 extract_preconditions(Subst,OldPres,Inner),
2318 conjunct_predicates([Pre|OldPres],NewPre),
2319 create_texpr(precondition(NewPre,Inner),subst,[],NewSubst),
2320 ? (select(reads(OldReads),I,I1) % we do not have to update modifies(.), non_det_modifies(.), reads_locals(.),...
2321 -> I2=[reads(NewReads)|I1],
2322 get_texpr_ids(Params,Ignore),
2323 find_identifier_uses(Pre,Ignore,PreUsedIds),
2324 ord_union(PreUsedIds,OldReads,NewReads)
2325 ; add_internal_error('No reads info for operation: ',add_precondition(Pre,b(Old,T,I),b(New,T,I2))),
2326 I2=I).
2327
2328
2329
2330 check_copied_operation(OpRef,Op,RefMachines,Ein,Eout) :-
2331 % todo: check the "refinement" parameter
2332 visible_env(refinement,operation_bodies,RefMachines,Env1,_Errors,[]),
2333 get_texpr_id(OpRef,OpId),get_texpr_type(OpRef,OpType),
2334 env_store(OpId,OpType,[],Env1,Env),
2335 findall(U, find_unknown_identifier(Op,Env,U), Unknown1),
2336 ( Unknown1=[] -> Ein=Eout
2337 ;
2338 sort(Unknown1,Unknown),
2339 op(OpName) = OpId,
2340 join_ids(Unknown,IdList),
2341 (Unknown = [_] -> Plural=[]; Plural=['s']),
2342 append([['Operation ',OpName,
2343 ' was copied from abstract machine but the identifier'],
2344 Plural,
2345 [' '],
2346 IdList,
2347 [' cannot be seen anymore']],Msgs),
2348 ajoin(Msgs,Msg), Ein = [error(Msg,none)|Eout]
2349 ).
2350 join_ids([I],[Msg]) :- !,opname(I,Msg).
2351 join_ids([A|Rest],[Msg,','|Mrest]) :- opname(A,Msg),join_ids(Rest,Mrest).
2352 opname(op(Id),Id) :- !.
2353 opname(Id,Id).
2354
2355 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2356 % split an identifier into a (possible empty) prefix and the name itself
2357 % e.g. split_prefix('path.to.machine', 'path.to', 'machine').
2358 split_prefix(Term,Prefix,Main) :-
2359 one_arg_term(Functor,Arg,Term),!,
2360 one_arg_term(Functor,MArg,Main),
2361 split_prefix(Arg,Prefix,MArg).
2362 split_prefix(PR,Prefix,Main) :- %print(split_prefix(PR,Prefix,Main)),nl,trace,
2363 safe_atom_chars(PR,Chars,split_prefix1),
2364 split_prefix2(Chars,Chars,[],CPrefix,CMain),
2365 safe_atom_chars(Main,CMain,split_prefix2),
2366 safe_atom_chars(Prefix,CPrefix,split_prefix3).
2367 split_prefix2([],Main,_,[],Main).
2368 split_prefix2([C|Rest],Previous,PrefBefore,Prefix,Main) :-
2369 ( C='.' ->
2370 append(PrefBefore,RestPrefix,Prefix),
2371 split_prefix2(Rest,Rest,[C],RestPrefix,Main)
2372 ;
2373 append(PrefBefore,[C],NextPref),
2374 split_prefix2(Rest,Previous,NextPref,Prefix,Main)).
2375
2376 rawmachine_section(Elem,List,Result) :- %
2377 functor(Pattern,Elem,2),
2378 arg(2,Pattern,Result),
2379 ? select(Pattern,List,Rest),!,
2380 (functor(Pattern2,Elem,2),member(Pattern2,Rest)
2381 -> arg(1,Pattern2,Pos),
2382 add_error(bmachine_construction,'Multiple sections for: ',Elem,Pos)
2383 ; true).
2384
2385 optional_rawmachine_section(Elem,List,Default,Result) :-
2386 ( rawmachine_section(Elem,List,Result1) -> true
2387 ; Result1=Default),
2388 Result1=Result.
2389
2390 one_arg_term(Functor,Arg,Term) :- %print(one_arg_term(Functor,Arg,Term)),nl,
2391 functor(Term,Functor,1),arg(1,Term,Arg).
2392
2393 % check if a rawmachine section list has a given section
2394 rawmachine_section_exists(Elem,List) :- %
2395 functor(Pattern,Elem,2),
2396 (member(Pattern,List) -> true).
2397
2398 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2399 % visibility rules
2400
2401 % the visibility/5 predicate declares what a part of a machine can see
2402 % visibility(MType, Scope, Section, Access, Info) means:
2403 % In a machine of type MType (machine, refinement, implementation),
2404 % an expression in a Section (like invariant) can see
2405 % the identifiers in the Access sections. Access is a list of
2406 % sections, where shortcuts are allowed (see shortcut/2, e.g., shortcut(operations,[unpromoted,promoted]).).
2407 % Scope defines where (in relation to the Section)
2408 % the section in Access are (local: same machine, included: in an
2409 % included machine, etc.)
2410 % Info is a list of additional information that is added to each
2411 % identifier in the environment to build up. E.g. in an operation
2412 % definition, constants are marked readonly.
2413 visibility(machine, local, constraints, [parameters],[]).
2414 visibility(machine, local, includes, [parameters,sets,constants],[]).
2415 visibility(machine, local, properties, [sets,constants],[]).
2416 visibility(machine, local, invariant, [parameters,sets,constants,variables],[]).
2417 visibility(machine, local, operation_bodies, [parameters,sets,constants],[readonly]).
2418 visibility(machine, local, operation_bodies, [operations],Info) :- Info =[readonly,dontcall].
2419 % an operation to be readonly: means we cannot assign to it; but the operation itself can change variables
2420 % for allow_operation_calls_in_expr=true we check that operation is inquiry in type checker
2421 % (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry]
2422 % ; Info =[readonly,dontcall] ). % we check in btype(operation_call_in_expr)
2423 visibility(machine, local, operation_bodies, [variables],[]).
2424 ?visibility(machine, local, initialisation, Access,[not_initialised|Info]) :- visibility(machine,local,operation_bodies,Access,Info).
2425
2426 visibility(machine, Scope, assertions, [Allow],[inquiry|DC]) :-
2427 (Scope = local -> Allow=operations, DC=[dontcall] ; Allow=promoted, DC=[]),
2428 get_preference(allow_operation_calls_in_expr,true). % if we allow calling operations in expressions
2429 visibility(machine, Scope, invariant, [promoted],[inquiry]) :-
2430 Scope \= local, % do not allow calling local operations in invariant; their correctness relies on the invariant
2431 get_preference(allow_operation_calls_in_expr,true).
2432
2433 visibility(machine, included, properties, [sets,constants],[]).
2434 visibility(machine, included, invariant, [sets,constants,variables],[]).
2435 visibility(machine, included, operation_bodies, [sets,constants,variables],[readonly]).
2436 visibility(machine, included, operation_bodies, [promoted],Info) :- Info = [readonly].
2437 % for allow_operation_calls_in_expr=true we check that operation is inquiry in type checker
2438 % (get_preference(allow_operation_calls_in_expr,true) -> Info = [inquiry] ; Info=[readonly]).
2439 %visibility(machine, included, initialisation, [sets,constants,variables,promoted],[readonly]).
2440 visibility(machine, included, initialisation, [sets,constants,promoted],[readonly]).
2441 visibility(machine, included, initialisation, [variables],Info) :-
2442 (get_preference(allow_overriding_initialisation,true)
2443 -> Info = [] % allow overriding INITIALISATION / making it more concrete
2444 ; Info = [readonly]). % default Atelier-B semantics
2445
2446 visibility(machine, used, properties, [sets,constants],[]).
2447 visibility(machine, used, invariant, [parameters,sets,constants,variables],[]).
2448 visibility(machine, used, operation_bodies, [parameters,sets,constants,variables],[readonly]).
2449 visibility(machine, used, initialisation, [parameters,sets,constants,variables],[readonly]).
2450 visibility(machine, used, operation_bodies, [operations],[inquiry]) :-
2451 get_preference(allow_operation_calls_for_uses,true). %% added by leuschel, allowed in Schneider Book
2452 % but not allowed by Atelier-B; see test 2135
2453
2454 visibility(machine, seen, includes, [sets,constants],[]).
2455 visibility(machine, seen, properties, [sets,constants],[]).
2456 visibility(machine, seen, invariant, [sets,constants],[]).
2457 visibility(machine, seen, operation_bodies, [sets,constants,variables],[readonly]).
2458 visibility(machine, seen, initialisation, [sets,constants,variables],[readonly]).
2459 visibility(machine, seen, operation_bodies, [operations],[inquiry]). %% added by leuschel, allow query operation
2460
2461 visibility(refinement, local, Section, Access, Info) :-
2462 Section \= assertions, % assertions are handled below
2463 ? visibility(machine, local, Section, Access, Info).
2464
2465 visibility(refinement, abstraction, includes, [sets,concrete_constants],[]).
2466 visibility(refinement, abstraction, properties, [sets,constants],[]).
2467 visibility(refinement, abstraction, invariant, [sets,constants,concrete_variables],[]).
2468 visibility(refinement, abstraction, invariant, [abstract_variables],[abstraction]).
2469 visibility(refinement, abstraction, operation_bodies, [sets,concrete_constants],[readonly]).
2470 visibility(refinement, abstraction, operation_bodies, [concrete_variables],[]).
2471
2472 visibility(refinement, included, properties, [sets,constants],[]).
2473 visibility(refinement, included, invariant, [sets,constants,variables],[]).
2474 visibility(refinement, included, operation_bodies, [sets,constants,variables,promoted],[re]). % What is re ??? TO DO: investigate
2475
2476 visibility(refinement, seen, includes, [sets,constants],[]).
2477 visibility(refinement, seen, properties, [sets,constants],[]).
2478 visibility(refinement, seen, invariant, [sets,constants],[]).
2479 visibility(refinement, seen, operation_bodies, [sets,constants,variables],[readonly]).
2480 visibility(refinement, seen, operation_bodies, [operations],[inquiry]).
2481
2482 visibility(refinement, Ref, initialisation, Access, [not_initialised|Info]) :-
2483 ? visibility(refinement,Ref,operation_bodies,Access,Info).
2484
2485 % assertions have same visibility as invariant
2486 visibility(MType, Ref, assertions, Part, Access) :-
2487 ? visibility(MType,Ref,invariant,Part,Access).
2488
2489 visibility(implementation, Ref, Section, Part, Access) :-
2490 visibility(refinement, Ref, Section, Part, Access).
2491 visibility(implementation, local, values_expression, [concrete_constants,sets],[]). % seems to have no effect (yet); see ArrayValuationAImp
2492 visibility(implementation, included, values_expression, [concrete_constants,sets],[]).
2493 visibility(implementation, seen, values_expression, [concrete_constants,sets],[]).
2494 visibility(implementation, abstraction,values_expression, [concrete_constants,sets],[]).
2495
2496 % For predicates over pre- and post-states
2497 visibility(MType, Rev, prepost, Access, Info) :-
2498 ? visibility(MType, Rev, invariant, Access, Info).
2499 visibility(MType, Rev, prepost, Access, [primed,poststate|Info]) :-
2500 ? visibility(MType, Rev, invariant, Access, Info).
2501
2502 % add error messages for some common mistakes (access to parameters in the properties)
2503 visibility(machine, local, properties, [parameters], [error('a parameter cannot be accessed in the PROPERTIES section')]).
2504 % the following rule should be helpful for the user, but additionally it also
2505 % provides a mechanism to re-introduce abstract variables in the INVARIANT
2506 % section of a while loop (to enable this, an identifier is also marked with "abstraction")
2507 % in the predicate allow_access_to_abstract_var
2508 visibility(refinement, abstraction, operation_bodies, [abstract_variables],
2509 [error('illegal access to an abstract variable in an operation'),abstraction]).
2510 visibility(refinement, abstraction, operation_bodies, [abstract_constants],
2511 [error('illegal access to an abstract constant in an operation (only allowed in WHILE INVARIANT or ASSERT)'),abstraction]).
2512
2513
2514 % lookups up all identifier sections that are accessible from
2515 % the given section, removes all shortcuts and removes
2516 % duplicate entries
2517 %
2518 % Returns a list of vis(Section,Info) where Section is the
2519 % identifier section that can be seen with Info as a list
2520 % of additional information
2521 expanded_visibility(MType, Ref, Part, Access) :-
2522 findall(vis(Section,Infos),
2523 ( visibility(MType,Ref,Part,Sections1,Infos),
2524 expand_shortcuts(Sections1,Sections),
2525 member(Section,Sections)),
2526 Access1),
2527 sort(Access1,Access).
2528 %format('MType=~w, Ref=~w, Part=~w~n Vis=~w~n',[MType,Ref,Part,Access]).
2529
2530 % visible_env/6 creates a type environment for a certain
2531 % part of a machine by looking up which identifier should
2532 % be visible from there and what additional information should
2533 % be added (e.g. to restrict access to read-only)
2534 %
2535 % The visibility/6 facts are used to define which identifier are visible
2536 %
2537 % MType: machine type (machine, refinement, ...)
2538 % Part: part of the machine for which the environment should be created
2539 % RefMachines: referred machines that are already typed
2540 % Env: The created environment
2541 % Errors: errors might be added if multiple variables with the same identifier
2542 % are declared
2543 visible_env(MType, Part, RefMachines, Env, Err_in, Err_out) :-
2544 env_empty(Init),
2545 visible_env(MType, Part, RefMachines, Init, Env, Err_in, Err_out).
2546 % visible_env/7 is like visible_env/6, but an initial environment
2547 % can be given in "In"
2548 visible_env(MType, Part, RefMachines, In, Out, Err_in, Err_out) :-
2549 foldl(visible_env2(MType,Part),RefMachines,In/Err_in,Out/Err_out).
2550 visible_env2(MType,Part,extended_local_ref(Machine),InEnvErr,OutEnvErr) :- !,
2551 Scope=local,
2552 get_machine_name(Machine,MName),
2553 %format('adding identifiers from machine ~w for scope ~w~n',[MName,Scope]),
2554 get_section(definitions,Machine,Defs),
2555 foldl(env_add_def(MName),Defs,InEnvErr,InEnvErr2),
2556 (bmachine:additional_configuration_machine(_MchName,AddMachine),
2557 get_section(definitions,AddMachine,AdditionalDefs)
2558 -> foldl(env_add_def(MName),AdditionalDefs,InEnvErr2,InterEnvErr)
2559 ; InterEnvErr = InEnvErr2
2560 ),
2561 expanded_visibility(MType, Scope, Part, Access),
2562 foldl(create_vis_env(Scope,MName,Machine),Access,InterEnvErr,OutEnvErr).
2563 visible_env2(MType,Part,ref(Scope,Machine),InEnvErr,OutEnvErr) :-
2564 get_machine_name(Machine,MName),
2565 %format('adding identifiers from machine ~w for scope ~w~n',[MName,Scope]),
2566 ( Scope == local ->
2567 get_section(definitions,Machine,Defs),
2568 %nl,print(adding_defs(Defs)),nl,nl,
2569 foldl(env_add_def(MName),Defs,InEnvErr,InterEnvErr)
2570 ;
2571 InEnvErr=InterEnvErr),
2572 expanded_visibility(MType, Scope, Part, Access),
2573 foldl(create_vis_env(Scope,MName,Machine),Access,InterEnvErr,OutEnvErr).
2574 env_add_def(MName,definition_decl(Name,PType,Pos,Params,Body,_Deps),InEnvErr,OutEnvErr) :-
2575 Type = definition(PType,Params,Body),
2576 Info = [nodeid(Pos),loc(local,MName,definitions)],
2577 create_texpr(identifier(Name),Type,Info,TExpr),
2578 add_unique_variable(TExpr,InEnvErr,OutEnvErr),!.
2579 env_add_def(MName,Def,EnvErr,EnvErr) :-
2580 add_internal_error('Cannot deal with DEFINITION: ',env_add_def(MName,Def)).
2581
2582 create_vis_env(Scope,MName,IDS,vis(Section,Infos),InEnvErr,OutEnvErr) :-
2583 get_section(Section,IDS,Identifiers1),
2584 %get_texpr_ids(Identifiers2,II),format('Got identifiers for ~w:~w = ~w~n',[MName,Section,II]),
2585 (Section=freetypes
2586 -> generate_free_type_ids(Identifiers1,Identifiers2)
2587 ; Identifiers2=Identifiers1),
2588 maplist(add_infos_to_identifier([loc(Scope,MName,Section)|Infos]),Identifiers2,Identifiers),
2589 foldl(add_unique_variable,Identifiers,InEnvErr,OutEnvErr).
2590
2591 % freetypes: generate IDs for Z freetype section
2592 % The classical B FREETYPE section is dealt with in another place (TODO: unify this)
2593 generate_free_type_ids([freetype(FTypeId,Cases)|T],[b(identifier(FTypeId),set(freetype(FTypeId)),[])|FT]) :- !,
2594 findall(b(identifier(CaseID),CaseType,[]),
2595 (member(case(CaseID,ArgType),Cases), gen_freecase_type(ArgType,FTypeId,CaseType)),
2596 FT, FT2),
2597 %write(generated_freetype_cases(FT)),nl,
2598 generate_free_type_ids(T,FT2).
2599 generate_free_type_ids(T,T).
2600
2601 gen_freecase_type(ArgType,FTypeId,Type) :- nonvar(ArgType), ArgType=constant(_),!, Type = freetype(FTypeId).
2602 gen_freecase_type(ArgType,FTypeId,set(couple(ArgType,freetype(FTypeId)))).
2603
2604 add_unique_variable(Var1,Old/Err_in,New/Err_out) :-
2605 optionally_rewrite_id(Var1,Var),
2606 get_texpr_id(Var,Id),
2607 get_texpr_type(Var,Type),
2608 get_texpr_info(Var,InfosOfNew),!,
2609 ( env_lookup_type(Id,Old,_) ->
2610 % we have a collision of two identifiers
2611 handle_collision(Var,Id,Type,Old,InfosOfNew,New,Err_in,Err_out)
2612 ;
2613 % no collision, just introduce the new identifier
2614 env_store(Id,Type,InfosOfNew,Old,New),
2615 %btypechecker:portray_env(New),nl,
2616 Err_in=Err_out
2617 ).
2618 add_unique_variable(Var,Env/Err,Env/Err) :- print(Var),nl,
2619 ( Var = b(definition(DEFNAME,_),_,INFO) ->
2620 add_error(add_unique_variable,'DEFINITION used in place of Identifier: ',DEFNAME,INFO)
2621 ; Var = b(description(Txt,_),_,INFO) ->
2622 add_error(add_unique_variable,'Unsupported @desc pragma: ',Txt,INFO)
2623 ;
2624 add_error(add_unique_variable,'Expected Identifier, but got: ',Var,Var)
2625 ).
2626
2627 add_infos_to_identifier(NewInfos,In,Out) :-
2628 add_texpr_infos(In,NewInfos,Out).
2629
2630 % get the ID of the variable, prime it if the infos contain "primed"
2631 optionally_rewrite_id(Var,NewVar) :-
2632 get_texpr_info(Var,InfosIn),
2633 ( selectchk(primed,InfosIn,InfosOut) ->
2634 get_texpr_id(Var,Id1),
2635 get_texpr_type(Var,Type),
2636 atom_concat(Id1,'\'',Id),
2637 create_texpr(identifier(Id),Type,InfosOut,NewVar)
2638 ;
2639 Var = NewVar).
2640
2641 :- use_module(translate,[translate_span/2]).
2642 % in case of a collision, we have three options:
2643 % - overwrite the old identifier,
2644 % - ignore the new identifier or
2645 % - generate an error message
2646 handle_collision(Var,Name,Type,OldEnv,InfosOfNew,NewEnv,Ein,Eout) :-
2647 env_lookup_infos(Name,OldEnv,InfosOfExisting),
2648 %btypechecker:portray_env(OldEnv),nl,
2649 ( collision_precedence(Name,InfosOfExisting,InfosOfNew) ->
2650 % this identifier should be ignored
2651 OldEnv = NewEnv,
2652 Ein = Eout
2653 ; collision_precedence(Name,InfosOfNew,InfosOfExisting) ->
2654 % the existing should be overwritten
2655 env_store(Name,Type,InfosOfNew,OldEnv,NewEnv),
2656 Ein = Eout
2657 ;
2658 % generate error and let the environment unchanged
2659 (Name = op(IName) -> Kind='Operation identifier'; Name=IName, Kind='Identifier'),
2660 get_texpr_pos(Var,Pos1),
2661 safe_get_info_pos(InfosOfExisting,Pos2),
2662 ( double_inclusion_allowed(Name,Pos1,Pos2,InfosOfExisting)
2663 -> %print(double_inclusion_of_id_allowed(Name,Type,Pos1,OldEnv,InfosOfExisting)),nl,
2664 OldEnv=NewEnv,
2665 Ein=Eout
2666 ; (better_pos(Pos2,Pos1), \+ better_pos(Pos1,Pos2)
2667 -> Pos = Pos2, translate_span(Pos1,PS1)
2668 ; Pos = Pos1,
2669 PS1='' % Pos1 is already part of error span
2670 ),
2671 translate_span(Pos2,PS2),
2672 translate_inclusion_path(InfosOfExisting,Path2),
2673 get_texpr_info(Var,Info1), translate_inclusion_path(Info1,Path1),
2674 %ajoin(['Identifier \'', IName, '\' declared twice at (Line:Col[:File]) ', PS1, Path1, ' and ', PS2, Path2],Msg),
2675 ajoin([Kind,' \'', IName, '\'', PS1, Path1, ' already declared at ', PS2, Path2],Msg),
2676 %format(user_error,'*** ~w~n',[Msg]),trace,
2677 Ein = [error(Msg,Pos)|Eout],
2678 OldEnv = NewEnv
2679 )
2680 ).
2681
2682
2683 % example identifier: %b(identifier(aa),integer,[loc(seen,M2,concrete_constants),readonly,usesee(M2,aa,seen),origin([included/M1]),nodeid(pos(18,2,2,11,2,13))])
2684
2685 % try and infer inclusion path of identifier from Infos
2686 translate_inclusion_path(Infos,Str) :- member(loc(How,Machine,_Section),Infos),!,
2687 (member(origin(Path),Infos) -> get_origin_path(Path,T) ; T=[')']),
2688 ajoin([' (', How,' from ', Machine|T],Str).
2689 translate_inclusion_path(_,'').
2690
2691 get_origin_path([How/Machine|T],[', ', How,' from ',Machine|TRes]) :- !,
2692 get_origin_path(T,TRes).
2693 get_origin_path(_,[')']).
2694
2695
2696 % SEE ISSUE PROB-403, test 1857
2697 % Correct behaviour related to multiple instantiation is specified in
2698 % B Reference Manual (AtelierB 4.2.1), 8.3 B Project/Instantiating and renaming.
2699 % => Constants and Sets defined in machines instantiated multiple times CAN be used in the including machine with their original (non-prefixed names).
2700 % Note: this code did lead to the constants being added multiple times; this has been fixed in concat_section_contents
2701 double_inclusion_allowed(Name,Pos1,Pos2,InfosOfExisting) :-
2702 %print(check_double_inclusion(Name,Pos1,Pos2,InfosOfExisting)),nl,
2703 Pos1==Pos2,
2704 %print(chk(InfosOfExisting)),nl,
2705 member(loc(LOC,_,Section),InfosOfExisting),
2706 %print(try(LOC,Section)),nl,
2707 section_can_be_included_multiple_times_nonprefixed(Section),
2708 % check that we are in a context of an included machine identifier:
2709 (inclusion_directive(LOC,Name,Pos2)
2710 -> true
2711 ; %LOC is probably local
2712 member(origin([INCL/_MACHINE|_]),InfosOfExisting),
2713 inclusion_directive(INCL,Name,Pos2)
2714 ).
2715
2716 inclusion_directive(included,_,_).
2717 inclusion_directive(used,_,_).
2718 inclusion_directive(seen,_,_). % imports ??
2719 inclusion_directive(abstraction,Name,Pos) :- % probably not allowed by Atelier-B
2720 (debug_mode(off) -> true
2721 ; add_message(bmachine_construction,'Allowing double inclusion from abstraction of: ',Name,Pos)).
2722
2723 section_can_be_included_multiple_times_nonprefixed(abstract_constants).
2724 section_can_be_included_multiple_times_nonprefixed(concrete_constants).
2725 section_can_be_included_multiple_times_nonprefixed(sets).
2726 section_can_be_included_multiple_times_nonprefixed(enumerated_sets).
2727 section_can_be_included_multiple_times_nonprefixed(enumerated_elements).
2728 section_can_be_included_multiple_times_nonprefixed(deferred_sets). % added 2.12.2022
2729 section_can_be_included_multiple_times_nonprefixed(constants). % shortcut
2730
2731
2732 % decide which position info is better: prefer info in main file (highlighting)
2733 :- use_module(bmachine,[b_get_main_filenumber/1]).
2734 better_pos(Pos,_) :- get_position_filenumber(Pos,Filenumber),
2735 b_get_main_filenumber(Filenumber).
2736 better_pos(_,none).
2737
2738 safe_get_info_pos(Info,Pos) :- (get_info_pos(Info,Pos) -> true ; Pos=none).
2739
2740 % collision_precedence/3 decides if the first variable takes
2741 % precedence over the second in case of a collision
2742 % the decision is made by the additional information of both
2743 % variables
2744 collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :-
2745 % in case of a re-introduced variable from the abstraction,
2746 % we prefer the concrete variable to the abstract one.
2747 ? is_abstraction(DroppedVarInfos,PreferredVarInfos),!.
2748 collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :-
2749 % We are checking an Event-B model with multi-level support
2750 % and have the same variable in two different refinement levels.
2751 % Then the one in the more refined module takes precedence
2752 member(level(L1),PreferredVarInfos),
2753 member(level(L2),DroppedVarInfos),
2754 % Level 0 is the abstract level, level 1 the first refinement, etc.
2755 L1 > L2,!.
2756 collision_precedence(Name,PreferredVarInfos,DroppedVarInfos) :-
2757 % A local definition takes precedence over a non-local identifier
2758 % TODO:
2759 member(loc(local,_DefMachine,definitions),PreferredVarInfos),
2760 member(loc(_,_VarMachine,Section),DroppedVarInfos),
2761 Section \= definitions,!,
2762 (preferences:get_preference(warn_if_definition_hides_variable,true)
2763 % default is true; we could also check clash_strict_checks
2764 -> get_id_kind(Section,HiddenIdKind),
2765 (get_info_pos(PreferredVarInfos,Pos1), Pos1 \= none,
2766 get_info_pos(DroppedVarInfos,Pos2), Pos2 \= none
2767 -> translate:translate_span(Pos1,Pos1Str), translate:translate_span(Pos2,Pos2Str),
2768 ajoin(['Warning: DEFINITION of ', Name, ' at ', Pos1Str,
2769 ' hides ',HiddenIdKind,' with same name at ', Pos2Str, '.'], Msg)
2770 ; ajoin(['Warning: DEFINITION of ', Name, ' hides ',HiddenIdKind,' with same name.'], Msg),
2771 Pos1 = unknown
2772 ),
2773 store_warning(Msg,Pos1) % TO DO: add position info
2774 ; true
2775 ).
2776 % TO DO: allow identical DEFINITIONS ?
2777
2778 % translate section name into a name for the identifier
2779 get_id_kind(abstract_constants,'constant').
2780 get_id_kind(concrete_constants,'constant').
2781 get_id_kind(parameters,'parameter').
2782 get_id_kind(deferred_sets,'deferred set').
2783 get_id_kind(enumerated_sets,'enumerated set').
2784 get_id_kind(enumerated_elements,'enumerated set element').
2785 get_id_kind(freetypes,'freetype').
2786 get_id_kind(promoted,'operation').
2787 % TODO: complete and use in other places
2788 get_id_kind(_SectionName,'variable').
2789
2790
2791 % is_abstraction/2 tries to find out if (in case of a name clash of
2792 % two variables) the second variable is just the re-introduced abstract
2793 % variable in a refinement.
2794 % InfosAbs is the list of information about the abstract variable
2795 % InfosConc is the list of information about the concrete variable
2796 is_abstraction(InfosAbs,InfosConc) :-
2797 % one variable is an abstract variable, introduced in the abstraction
2798 ? member(loc(abstraction,_,abstract_variables),InfosAbs),
2799 % the other is either an abstract or concrete variable,
2800 ? member(VarType,[abstract_variables,concrete_variables]),
2801 % introduced either locally or in an included machine
2802 ? member(Scope,[local,included]),
2803 ? member(loc(Scope,_,VarType),InfosConc).
2804 % and the same for constants:
2805 is_abstraction(InfosAbs,InfosConc) :-
2806 % one variable is an abstract variable, introduced in the abstraction
2807 member(loc(abstraction,_,abstract_constants),InfosAbs),
2808 % the other is either an abstract or concrete variable,
2809 member(VarType,[abstract_constants,concrete_constants]),
2810 % introduced either locally or in an included machine
2811 member(Scope,[local,included]),
2812 member(loc(Scope,_,VarType),InfosConc).
2813
2814 % shortcuts for sections, to ease the use of typical combinations of
2815 % sections
2816 shortcut(all_parameters,[parameters,internal_parameters]).
2817 shortcut(sets,[deferred_sets,enumerated_sets,enumerated_elements|T]) :-
2818 (animation_minor_mode(M), (M=z ; M=eventb)
2819 -> T = [freetypes]
2820 ; T = []). % The FREETYPES section in classical B is unfortunately dealt with differently and
2821 % we currently have errors if add the freetypes section here
2822 shortcut(constants,[abstract_constants,concrete_constants]).
2823 shortcut(variables,[abstract_variables,concrete_variables]).
2824 shortcut(operations,[unpromoted,promoted]).
2825 shortcut(identifiers,[all_parameters,sets,constants,variables,operations]).
2826
2827 expand_shortcuts(Sections,Expanded) :-
2828 foldl(expand_shortcut,Sections,Expanded,[]).
2829 expand_shortcut(Section,Sections,RSections) :-
2830 ( shortcut(Section,Expanded) ->
2831 foldl(expand_shortcut,Expanded,Sections,RSections)
2832 ; valid_section(Section) ->
2833 Sections = [Section|RSections]
2834 ;
2835 add_internal_error('invalid section',expand_shortcut(Section,Sections,RSections)),fail).
2836
2837 % find sections that can see given sections
2838 find_relevant_sections(RSecs,MTypes,Result) :-
2839 expand_shortcuts(RSecs,Sections),
2840 findall(R,
2841 ( member(MType,MTypes),
2842 visibility(MType,local,R,SAccess,_),
2843 expand_shortcuts(SAccess,Access),
2844 member(S,Sections),
2845 member(S,Access),
2846 valid_section(R)),
2847 Result1),
2848 sort(Result1,Result).
2849
2850
2851 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2852 % renaming
2853
2854 rename_relevant_sections(DefSecs,Renamings,Machine,New) :-
2855 find_relevant_sections(DefSecs,[machine],Relevant),
2856 rename_in_sections(Relevant,Renamings,Machine,New).
2857 rename_in_sections([],_,M,M).
2858 rename_in_sections([Section|Rest],Renamings,Old,New) :-
2859 select_section_texprs(Section,OTExprs,NTExprs,Old,Inter),
2860 rename_bt_l(OTExprs,Renamings,NTExprs),
2861 rename_in_sections(Rest,Renamings,Inter,New).
2862
2863 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2864 :- use_module(kernel_freetypes,[register_freetypes/1]).
2865 % cleaning up machine
2866 clean_up_machine(In,RefMachines,Out) :-
2867 extract_parameter_types([ref(local,In)|RefMachines],NonGroundExceptions),
2868 clean_up_machine2(NonGroundExceptions,In,Out).
2869 clean_up_machine2(NonGroundExceptions) -->
2870 get_section_content(enumerated_sets,Enum),
2871 get_section_content(enumerated_elements,Elems),
2872 {register_enumerated_sets(Enum,Elems)}, % register name of enumerated sets, e.g., to detect finite in ast_cleanup
2873 get_section_content(freetypes,Freetypes),
2874 {register_freetypes(Freetypes)}, % so that info is available in ast_cleanup for eval_set_extension
2875 clean_up_section(constraints,NonGroundExceptions),
2876 clean_up_section(properties,NonGroundExceptions),
2877 clean_up_section(invariant,NonGroundExceptions),
2878 clean_up_section(initialisation,NonGroundExceptions),
2879 clean_up_section(assertions,NonGroundExceptions),
2880 clean_up_section(operation_bodies,NonGroundExceptions).
2881 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
2882 :- if(environ(prob_safe_mode,true)).
2883 clean_up_section(Section,NonGroundExceptions,In,Out) :-
2884 select_section_texprs(Section,Old,New,In,Out),
2885 %format('Cleaning up and optimizing section ~w~n',[Section]), %maplist(check_ast,Old), % this will raise errors
2886 clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section),
2887 %format('Checking result of clean_up section ~w~n',[Section]),
2888 maplist(check_ast(true),New),
2889 formatsilent('Finished checking section ~w~n',[Section]).
2890 :- else.
2891 clean_up_section(Section,NonGroundExceptions,In,Out) :-
2892 % debug_stats(cleaning_up(Section)),
2893 select_section_texprs(Section,Old,New,In,Out),
2894 clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section).
2895 :- endif.
2896
2897 get_section_content(SecName,SectionContent,Mch,Mch) :- get_section(SecName,Mch,SectionContent).
2898
2899 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2900 % type expressions in context of an already type-checked machine
2901 % TO DO: maybe do some performance optimisations for identifiers, values, ... to avoid creating scope, see formula_typecheck2_for_eval optimisation
2902 % b_type_literal does it in bmachine before calling type_in_machine_l
2903 type_in_machine_l(Exprs,Scope,Machine,Types,TExprs,Errors) :-
2904 MType = machine,
2905 create_scope_if_necessary(Exprs,Scope,MType,Machine,Env,Errors,E1), % this can be expensive for big B machines
2906 %runtime_profiler:profile_single_call(create_scope,unknown,
2907 % bmachine_construction:create_scope(Scope,MType,Machine,Env,Errors,E1)),
2908 btype_ground_dl(Exprs,Env,[],Types,TExprUncleans,E1,[]),
2909 perform_post_static_check(TExprUncleans),
2910 maplist(clean_up_pred_or_expr([]),TExprUncleans,TExprs).
2911
2912 % detect a few common expressions which do not require creating a scope of all the identifiers
2913 create_scope_if_necessary([E],_Scope,MType,Machine,Env,Ein,Eout) :- raw_expr_wo_ids(E),!,
2914 create_scope([],MType,Machine,Env,Ein,Eout).
2915 create_scope_if_necessary(_Exprs,Scope,MType,Machine,Env,Ein,Eout) :-
2916 create_scope(Scope,MType,Machine,Env,Ein,Eout).
2917
2918 % a few common raw ASTs which do not refer to identifiers
2919 raw_expr_wo_ids(falsity(_)).
2920 raw_expr_wo_ids(truth(_)).
2921 raw_expr_wo_ids(empty_set(_)).
2922 raw_expr_wo_ids(equal(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2923 raw_expr_wo_ids(not_equal(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2924 raw_expr_wo_ids(interval(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2925 raw_expr_wo_ids(add(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2926 raw_expr_wo_ids(minus_or_set_subtract(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2927 raw_expr_wo_ids(mult_or_cart(_,A,B)) :- raw_expr_wo_ids(A), raw_expr_wo_ids(B).
2928 raw_expr_wo_ids(unary_minus(_,A)) :- raw_expr_wo_ids(A).
2929 raw_expr_wo_ids(boolean_true(_)).
2930 raw_expr_wo_ids(boolean_false(_)).
2931 raw_expr_wo_ids(bool_set(_)).
2932 raw_expr_wo_ids(integer(_,_)).
2933 raw_expr_wo_ids(real(_,_)).
2934 raw_expr_wo_ids(string(_,_)).
2935
2936 % note prob_ids(visible), external_library(all_available_libraries) scope is expanded somewhere else
2937 create_scope(Scope,MType,Machine,Env,Ein,Eout) :-
2938 env_empty(Init),
2939 add_theory_operators(Machine,Init,WithOperators),
2940 foldl(create_scope2(MType,Machine),Scope,WithOperators/Ein,Env/Eout).
2941 add_theory_operators(Machine,Ein,Eout) :-
2942 get_section(operators,Machine,Operators),
2943 keys_and_values(Operators,Ids,Ops),
2944 foldl(env_store_operator,Ids,Ops,Ein,Eout).
2945 create_scope2(MType,Machine,Scope,In/Ein,Out/Eout) :-
2946 ( Scope = constants ->
2947 visible_env(MType,properties,[ref(local,Machine)],In,Out,Ein,Eout)
2948 ; Scope = variables ->
2949 visible_env(MType,invariant,[ref(local,Machine)],In,Out,Ein,Eout)
2950 ; Scope = variables_and_additional_defs ->
2951 visible_env(MType,invariant,[extended_local_ref(Machine)],In,Out,Ein,Eout)
2952 ; Scope = assertions_scope_and_additional_defs ->
2953 visible_env(MType,assertions,[extended_local_ref(Machine)],In,Out,Ein,Eout)
2954 ; Scope = prepost ->
2955 visible_env(MType,prepost,[ref(local,Machine)],In,Out,Ein,Eout)
2956 ; Scope = operation_bodies ->
2957 visible_env(MType,operation_bodies,[ref(local,Machine)],In,Out,Ein,Eout)
2958 ; Scope = operation(Op) ->
2959 create_operation_scope(Op,Machine,In,Out), Ein=Eout
2960 ; Scope = env(ExplicitEnv) ->
2961 ExplicitEnv = Out, Ein=Eout
2962 ; Scope = identifier(Ids) ->
2963 store_variables(Ids,In,Out), Ein=Eout
2964 ; Scope = external_library(LibName) % be sure to make these last to avoid duplication errors
2965 -> store_ext_defs(LibName,In,Out), Ein=Eout
2966 ;
2967 add_error(bmachine_construction, 'invalid scope', Scope),fail).
2968 create_operation_scope(Op,Machine,In,Out) :-
2969 get_section(operation_bodies,Machine,OpBodies),
2970 get_texpr_id(OpId,op(Op)),
2971 get_texpr_expr(TOp,operation(OpId,Results,Params,_)),
2972 ( member(TOp,OpBodies) ->
2973 append(Results,Params,LocalVariables),
2974 store_variables(LocalVariables,In,Out)
2975 ;
2976 ajoin(['operation \'',Op,'\' not found for building scope'], Msg),
2977 add_error(bmachine_construction,Msg),fail).
2978 store_variables(Ids,In,Out) :- foldl(store_variable,Ids,In,Out).
2979 store_variable(Id,In,Out) :-
2980 get_texpr_id(Id,Name),get_texpr_type(Id,Type),
2981 env_store(Name,Type,[],In,Out).
2982
2983 type_open_predicate_with_quantifier(OptionalOuterQuantifier,Predicate,Scope,Machine,TResult,Errors) :-
2984 type_open_formula(Predicate,Scope,false,Machine,pred,Identifiers,TPred,Errors),
2985 ( Identifiers = [] ->
2986 TResult = TPred
2987 ; OptionalOuterQuantifier=forall ->
2988 create_forall(Identifiers,TPred,TResult)
2989 ; OptionalOuterQuantifier=no_quantifier ->
2990 TResult = TPred
2991 ; % OptionalOuterQuantifier=exists
2992 %perform_do_not_enumerate_analysis(Identifiers,TPred,'EXISTS',Span,TPred2), % now done by apply_kodkod_or_other_optimisations
2993 create_exists(Identifiers,TPred,TResult)
2994 ).
2995
2996 type_open_formula(Raw,Scope,AllowOpenIdsinExpressions,Machine,Type,Identifiers,Result,Errors) :-
2997 create_scope_if_necessary([Raw],Scope,machine,Machine,Env1,Errors,E1),
2998 ( Identifiers==[] -> Mode=closed, Env1=Env
2999 ; Mode=open, openenv(Env1,Env)),
3000 btype_ground_dl([Raw],Env,[],[Type],[TExprUnclean],E1,E2),
3001 ( Mode=closed -> true
3002 ;
3003 openenv_identifiers(Env,Identifiers), % TODO: treat theory operators ?
3004 check_ground_types_dl(Identifiers,[],E2,E3)
3005 ),
3006 %print(type_open_formula(Identifiers,TExprUnclean)),nl,
3007 mark_outer_quantifier_ids(TExprUnclean,TExprUnclean2),
3008 perform_post_static_check([TExprUnclean2]),
3009 clean_up_pred_or_expr([],TExprUnclean2,TResult), % TODO: only run if requested
3010 ( Identifiers = [] -> % no newly introduced identifiers, no problem
3011 E3 = []
3012 ; Type = pred -> % newly introduced identifiers in a predicate - ok
3013 E3 = []
3014 ; AllowOpenIdsinExpressions=true -> % we explicitly allow open ids in expressions
3015 E3 = []
3016 ; % newly introduced identifiers in expression make no sense
3017 % (is that so?)
3018 foldl(add_unknown_identifier_error,Identifiers,E3,[])
3019 ),
3020 Result = TResult.
3021 add_unknown_identifier_error(TId,[error(Msg,Pos)|E],E) :-
3022 get_texpr_id(TId,Id),
3023 ajoin(['Unknown identifier ',Id,'.'],Msg),
3024 % TO DO: generate fuzzy match and possible completions message
3025 get_texpr_pos(TId,Pos).
3026
3027 % mark outermost identfiers so that they don't get optimized away
3028 % e.g., ensure that we print the solution for something like #(y2,x2).(x2 : 0..10 & y2 : 0..10 & x2 = 10 & y2 = 10)
3029 mark_outer_quantifier_ids(b(exists(IDS,Pred),pred,Info),Res) :-
3030 maplist(mark_id,IDS,MIDS),!,
3031 Res = b(exists(MIDS,Pred),pred,Info).
3032 mark_outer_quantifier_ids(b(let_predicate(IDS,Exprs,Pred),pred,Info),Res) :-
3033 maplist(mark_id,IDS,MIDS),!,
3034 Res = b(let_predicate(MIDS,Exprs,Pred),pred,Info).
3035 mark_outer_quantifier_ids(b(forall(IDS,LHS,RHS),pred,Info),Res) :-
3036 maplist(mark_id,IDS,MIDS),!,
3037 Res = b(forall(MIDS,LHS,RHS),pred,Info).
3038 mark_outer_quantifier_ids(X,X).
3039
3040 mark_id(b(identifier(ID),TYPE,INFO),b(identifier(ID),TYPE,[do_not_optimize_away|INFO])).
3041
3042 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3043
3044 % some additional static checks; they should be run only once before ast_cleanup runs
3045 % TO DO: move maybe some of the exists/forall checks here; would be simpler and not require removed_typing inspection
3046
3047 :- use_module(bsyntaxtree,[map_over_typed_bexpr/2]).
3048 perform_post_static_check([Typed|_]) :- %print(t(Typed)),nl,
3049 preferences:get_preference(disprover_mode,false),
3050 map_over_typed_bexpr(post_static_check,Typed),
3051 fail.
3052 perform_post_static_check([_|T]) :- !, perform_post_static_check(T).
3053 perform_post_static_check(_).
3054
3055 post_static_check(b(E,T,I)) :-
3056 %bsyntaxtree:check_infos(I,post_static_check),
3057 post_static_check_aux(E,T,I).
3058
3059 :- use_module(bsyntaxtree,[find_identifier_uses/3, is_a_disjunct_or_implication/4]).
3060 :- use_module(library(ordsets),[ord_subtract/3]).
3061 % should detect patterns like { zz | # r__1, q__1, zz . ( ...)}
3062 % {x,z|z=1}[{TRUE}] = {1}
3063 % %x.(1=1|1)(TRUE) = 1
3064 post_static_check_aux(lambda(Ids,Body,Expr),_T,Info) :-
3065 get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds),
3066 find_identifier_uses(Body,[],UsedIds1),
3067 find_identifier_uses(Expr,[],UsedIds2), % relevant for tests 1106, 1264, 1372, 1622 to also look at Expr
3068 ord_subtract(SortedIds,UsedIds1,S2),
3069 ord_subtract(S2,UsedIds2,UnusedIds), UnusedIds \= [],
3070 add_warning_with_info('Condition of lambda does not use these identifiers: ',UnusedIds,Body,Info).
3071 post_static_check_aux(comprehension_set(Ids,Body),_T,Info) :-
3072 get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds),
3073 find_identifier_uses(Body,[],UsedIds),
3074 ord_subtract(SortedIds,UsedIds,UnusedIds), UnusedIds \= [],
3075 add_warning_with_info('Body of comprehension set does not use these identifiers: ',UnusedIds,Body,Info).
3076 post_static_check_aux(exists(_,P),_T,Info) :-
3077 is_a_disjunct_or_implication(P,Type,_Q,_R),
3078 exists_body_warning(P,Info,Type).
3079
3080
3081 exists_body_warning(_,_,_) :- animation_minor_mode(X),(X=eventb ; X=tla),!.
3082 exists_body_warning(P,I,Type) :-
3083 translate_bexpression(P,PS),
3084 ajoin(['Warning: body of existential quantifier is a ',Type,
3085 ' (not allowed by Atelier-B): '],Msg),
3086 add_warning_with_info(Msg,PS,P,I).
3087
3088
3089
3090 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3091 % Warnings
3092
3093 :- use_module(bsyntaxtree,[contains_info_pos/1]).
3094 add_warning_with_info(Msg1,Msg2,P,Info) :-
3095 (contains_info_pos(Info) -> Pos=Info ; Pos=P),
3096 add_warning(bmachine_construction,Msg1,Msg2,Pos).
3097
3098 :- dynamic warnings/2.
3099 clear_warnings :-
3100 retractall( warnings(_,_) ).
3101 show_warnings :-
3102 warnings(Warning,Span),
3103 add_warning(bmachine_construction, Warning,'',Span),
3104 fail.
3105 show_warnings.
3106
3107
3108 store_warning(Warning,Span) :-
3109 (warnings(Warning,Span) -> true ; assertz(warnings(Warning,Span))).