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