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