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