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