1		% (c) 2020-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		:- module(b_machine_identifier_normalization, [normalize_b_machine/1,
5		normalize_b_machine/2,
6		normalize_b_machines_in_dir/1,
7		map_normalize_ids_in_b_ast/4,
8		normalize_ids_in_b_ast/4,
9		get_normalized_id_name_mapping/4,
10		enumerate_ids/4,
11		normalize_id_type/3,
12		b_component/1]).
13
14		:- use_module(library(lists)).
15		:- use_module(library(sets), [subtract/3]).
16		:- use_module(library(avl), [avl_to_list/2]).
17		:- use_module(library(random), [random_permutation/2]).
18		:- use_module(library(file_systems)).
19
20		:- use_module(probsrc(preferences)).
21		:- use_module(probsrc(bmachine)).
22		:- use_module(probsrc(error_manager)).
23		:- use_module(probsrc(tools), [unique_id/2]).
24		:- use_module(probsrc(module_information), [module_info/2]).
25
26		:- module_info(group, synthesis).
27		:- module_info(description, 'Normalize all identifiers and strings in the currently loaded B machine. Patterns are preserved using specific prefixes: variables (v), constants (c), deferred sets (s), enumerated elements (e), record fields (f), operation parameters (p), operation return ids (r), operation names (o), local ids (l) e.g. in quantifiers or comprehension sets. Intended to be used for deep learning tasks on B/Event-B machines.').
28
29		% NOTE: if directly using any exported predicate other than normalize_b_machine*/[1,2],
30		% consider retracting tools:id_counter/1 before normalizing a single dataset
31		% NOTE: assertz(normalization_inline_defs_only(true)) to skip normalization of
32		% identifiers and only create machines with inlined definitions.
33
34		:- dynamic normalization_inline_defs_only/1.
35		inline_defs_only(Value) :-
36		retractall(normalization_inline_defs_only(_)),
37		assertz(normalization_inline_defs_only(Value)).
38
39		% Currently only classical B machines (.mch) are normalized.
40		% TO DO: consider Event-B machines
41		% TO DO: check if structs are normalized correctly (see /home/joshua/STUPS/prob_examples/public_examples/VDM/Airport/Airport.mch)
42		normalize_b_machines_in_dir(Directory) :-
43		preferences:temporary_set_preference(use_common_subexpression_elimination, false),
44		preferences:temporary_set_preference(optimize_ast, false),
45		get_b_and_eventb_machine_paths(Directory, FileList),
46		normalize_b_machines(FileList),
47		preferences:reset_temporary_preference(use_common_subexpression_elimination),
48		preferences:reset_temporary_preference(optimize_ast).
49
50		normalize_b_machines([]).
51		normalize_b_machines([_MachineName-FilePath|T]) :-
52		normalize_b_machine(FilePath),
53		!,
54		normalize_b_machines(T).
55		normalize_b_machines([_|T]) :-
56		normalize_b_machines(T).
57
58		get_b_and_eventb_machine_paths(Directory, FileList) :-
59		directory_exists(Directory),
60		directory_members_of_directory(Directory, SubDirectories),
61		get_b_and_eventb_machine_paths_aux(SubDirectories, [], SubdirFileList), % Does not include toplevel machines.
62		get_b_machines_in_dir(Directory, TopLevelMachines),
63		append(TopLevelMachines, SubdirFileList, FileList).
64		get_b_and_eventb_machine_paths(Directory, []) :-
65		\+ directory_exists(Directory).
66
67		% Get a list of file paths from the list of directories and recursively crawl each sub directory.
68		get_b_and_eventb_machine_paths_aux([], Acc, Acc).
69		get_b_and_eventb_machine_paths_aux([_-AbsoluteSubDirectoryPath|T], Acc, FileList) :-
70		get_b_machines_in_dir(AbsoluteSubDirectoryPath, BMachines),
71		get_b_and_eventb_machine_paths(AbsoluteSubDirectoryPath, RecursiveFileList1),
72		remove_normalized_machines(RecursiveFileList1, RecursiveFileList1, [], RecursiveFileList),
73		append([BMachines,RecursiveFileList,Acc], NewAcc),
74		get_b_and_eventb_machine_paths_aux(T, NewAcc, FileList).
75
76		% Lists all toplevel B Machines of the given directory (i.e. non-recursively).
77		get_b_machines_in_dir(Directory, BMachines) :-
78		file_members_of_directory(Directory, '*.mch', BMachines1),
79		% file_members_of_directory(Directory, '*.eventb', EventBMachines1),
80		remove_normalized_machines(BMachines1, BMachines1, [], BMachines).
81
82		remove_file_extension(Path, Prefix, Ext) :-
83		atom_concat(Prefix, '.mch', Path),
84		Ext = '.mch'.
85		remove_file_extension(Path, Prefix, Ext) :-
86		atom_concat(Prefix, '.eventb', Path),
87		Ext = '.eventb'.
88
89		remove_normalized_machines(_, [], Acc, Acc).
90		remove_normalized_machines(All, [Name-Path|T], Acc, Filtered) :-
91		\+ atom_concat(_, '_normalized.mch', Path),
92		\+ atom_concat(_, '_normalized.eventb', Path),
93		\+ atom_concat(_, '_inlinedef.mch', Path),
94		\+ atom_concat(_, '_inlinedef.eventb', Path),
95		remove_file_extension(Path, PrefixPath, Ext),
96		(normalization_inline_defs_only(true)
97		-> atom_concat(PrefixPath, '_inlinedef', TNPath)
98		; atom_concat(PrefixPath, '_normalized', TNPath)
99		),
100		atom_concat(TNPath, Ext, NPath),
101		\+ member(_-NPath, All),
102		!,
103		remove_normalized_machines(All, T, [Name-Path|Acc], Filtered).
104		remove_normalized_machines(All, [_|T], Acc, Filtered) :-
105		remove_normalized_machines(All, T, Acc, Filtered).
106
107		load_b_or_eventb_machine(AbsoluteFilePath) :-
108		is_classical_b_machine_path(AbsoluteFilePath),
109		!,
110		b_load_machine_from_file(AbsoluteFilePath),
111		b_machine_precompile.
112		load_b_or_eventb_machine(AbsoluteFilePath) :-
113		b_load_eventb_project(AbsoluteFilePath),
114		b_machine_precompile.
115		% TO DO: set desired timeout from java
116		is_classical_b_machine_path(Path) :-
117		atom(Path),
118		atom_concat(_, Ext, Path),
119		Ext == '.mch'.
120
121		:- dynamic normalize_strings/0. % strings are normalized if asserted
122		:- volatile normalize_strings/0.
123
124		%% normalize_b_machine(+InputFilePath).
125		%
126		% Normalise all identifier in a B machine, load the normalised machine, and save the new machine file.
127		normalize_b_machine(InputFilePath) :-
128		retractall(tools:id_counter(_)),
129		is_b_machine_file(InputFilePath, Prefix, Ext),
130		(normalization_inline_defs_only(true)
131		-> atom_concat(Prefix, '_inlinedef', OutputFilePath1)
132		; atom_concat(Prefix, '_normalized', OutputFilePath1)
133		),
134		atom_concat(OutputFilePath1, Ext, OutputFilePath),
135		normalize_b_machine(InputFilePath, OutputFilePath).
136
137		%% normalize_b_machine(+InputFilePath,+OutputFilePath).
138		normalize_b_machine(InputFilePath, OutputFilePath) :-
139		ground(OutputFilePath),
140		error_manager:reset_errors,
141		machine_exists(InputFilePath),
142		format("Normalize machine: ~w~n", [InputFilePath]),
143		load_b_or_eventb_machine(InputFilePath),
144		b_machine_precompile,
145		!,
146		preferences:set_preference(use_solver_on_load, prob),
147		get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames, NRecordFieldNames),
148		Env = [[],NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
149		full_b_machine(Machine),
150		Machine = machine(MachineName,SectionList),
151		subtract(SectionList, ['definitions'/_,'linking_invariant'/LinkingInvariant,'enumerated_elements'/EnumeratedElements,'enumerated_sets'/EnumeratedSets,'deferred_sets'/DeferredSets,'abstract_constants'/_,'concrete_constants'/_,'abstract_variables'/_,'concrete_variables'/_,'properties'/_,'invariant'/_,'linking_invariant'/_,'assertions'/_,'initialisation'/_,'operation_bodies'/OperationBodies,'definitions'/_], MachineMeta),
152		% definitions are inlined and removed
153		map_normalize_ids_in_b_ast(Env, DeferredSets, NDeferredSets, _),
154		map_normalize_ids_in_b_ast(Env, EnumeratedSets, NEnumeratedSets, _),
155		map_normalize_ids_in_b_ast(Env, EnumeratedElements, NEnumeratedElements, _),
156		map_normalize_ids_in_b_ast(Env, OperationBodies, NOperationBodies, _),
157		b_get_machine_variables(MachineVars),
158		map_normalize_ids_in_b_ast(Env, MachineVars, NVariables, _),
159		b_get_machine_all_constants(MachineConstants),
160		map_normalize_ids_in_b_ast(Env, MachineConstants, NConstants, _),
161		normalize_ids_in_b_ast(Env, LinkingInvariant, NLinkingInvariant, Env1),
162		b_get_invariant_from_machine(MachineInvariant),
163		normalize_ids_in_b_ast(Env1, MachineInvariant, NInvariant, Env2),
164		b_get_properties_from_machine(MachineProperties),
165		normalize_ids_in_b_ast(Env2, MachineProperties, NProperties, Env3),
166		b_safe_get_initialisation_from_machine(MachineInitialisation, _),
167		normalize_ids_in_b_ast(Env3, MachineInitialisation, NInitialisation, Env4),
168		get_all_assertions_from_machine(MachineAssertions),
169		map_normalize_ids_in_b_ast(Env4, MachineAssertions, NAssertions, _),
170		!,
171		% unchanged: 'used'/_,'freetypes'/_,'operators'/_,'values'/_,'meta'/_,'constraints'/_,'promoted'/_,'unpromoted'/_,'internal_parameters'/_,'parameters'/_
172		NMachine = machine(MachineName,['deferred_sets'/NDeferredSets,'enumerated_sets'/NEnumeratedSets,'enumerated_elements'/NEnumeratedElements,'concrete_constants'/NConstants,'abstract_variables'/NVariables,'properties'/NProperties,'invariant'/NInvariant,'linking_invariant'/NLinkingInvariant,'assertions'/NAssertions,'initialisation'/NInitialisation,'operation_bodies'/NOperationBodies|MachineMeta]),
173		b_set_typed_machine(NMachine,InputFilePath),
174		%%
175		% atom_concat('/home/joshua/STUPS/prob_examples/public_examples', Rest, OutputFilePath),
176		% atom_concat('/home/joshua/STUPS/prob_examples/public_examples_normalized', Rest, NOutputFilePath),
177		%%
178		b_write_machine_representation_to_file(none, OutputFilePath),
179		format("Done.~n", []).
180		normalize_b_machine(InputFilePath, _) :-
181		add_error(normalize_b_machine, 'Skip machine normalization due to errorneous B machine:', InputFilePath),
182		fail.
183
184		machine_exists(FilePath) :-
185		file_exists(FilePath),
186		!.
187		machine_exists(FilePath) :-
188		add_error(normalize_b_machine, 'File does not exist:', FilePath),
189		fail.
190
191		is_b_machine_file(FilePath, _, _) :-
192		\+ atom(FilePath),
193		!,
194		add_error(normalize_b_machine, 'Prolog atom expected.', []),
195		fail.
196		is_b_machine_file(FilePath, Prefix, Ext) :-
197		member(Ext, ['.mch','.eventb','.prob']),
198		atom_concat(Prefix, Ext, FilePath),
199		!.
200		is_b_machine_file(FilePath, _, _) :-
201		add_error(normalize_b_machine, 'Wrong file format. B/Event-B machine with extension .mch, .eventb or .prob expected:', FilePath),
202		fail.
203
204		normalize_id_type(NormalizedAny, Name, NormalizedName) :-
205		member((b(identifier(Name),_,_),b(identifier(NormalizedName),_,_)), NormalizedAny),
206		!.
207		normalize_id_type(NormalizedRecFields, Name, NormalizedName) :-
208		member((Name,NormalizedName), NormalizedRecFields),
209		!.
210		normalize_id_type(NormalizedAny, Type, NType) :-
211		Type =.. [Functor|Args],
212		Args \== [],
213		!,
214		maplist(normalize_id_type(NormalizedAny), Args, NArgs),
215		NType =.. [Functor|NArgs].
216		normalize_id_type(_, Type, Type).
217
218		enumerate_ids(NormalizedSets, Prefix, IDs, EIDs) :-
219		atom(Prefix),
220		!,
221		enumerate_ids_acc(NormalizedSets, Prefix, IDs, [], EIDs).
222		enumerate_ids(_, _, _, _) :-
223		add_error(enumerate_ids, 'Error: Prefix has to be an atom.', []).
224
225		enumerate_ids_acc(_, _, [], Acc, Acc).
226		enumerate_ids_acc(NormalizedSets, Prefix, [b(identifier(op(Name)),Type,Info)|T], Acc, EIDs) :-
227		(normalization_inline_defs_only(true)
228		-> NId = b(identifier(op(Name)),Type,Info)
229		; get_enumerated_name(Prefix, NewName),
230		NId = b(identifier(op(NewName)),Type,Info)
231		),
232		enumerate_ids_acc(NormalizedSets, Prefix, T, [(b(identifier(op(Name)),Type,Info),NId)|Acc], EIDs).
233		enumerate_ids_acc(NormalizedSets, Prefix, [Ast|T], Acc, EIDs) :-
234		( Ast = b(identifier(Name),Type,Info)
235		; ( Ast = b(_,Type,Info),
236		member(synthesis(machinevar,Name), Info)
237		)
238		),
239		normalize_id_type(NormalizedSets, Type, NewType),
240		(normalization_inline_defs_only(true)
241		-> NId = b(identifier(op(Name)),Type,Info)
242		; get_enumerated_name(Prefix, NewName),
243		adapt_machinevar_name_info(NewName, Info, NewInfo),
244		NId = b(identifier(op(NewName)),NewType,NewInfo)
245		),
246		enumerate_ids_acc(NormalizedSets, Prefix, T, [(b(identifier(Name),Type,Info),NId)|Acc], EIDs).
247
248		get_enumerated_name(Prefix, UniqueId) :-
249		( is_list(Prefix)
250		->
251		CPrefix = Prefix
252		; atom_codes(Prefix, CPrefix)
253		),
254		unique_id(CPrefix, UniqueId).
255
256		enumerate_deferred_sets([], Acc, Acc).
257		enumerate_deferred_sets([Ast|T], Acc, EIDs) :-
258		get_enumerated_name('s', UniqueId),
259		Ast = b(_,_,Info),
260		adapt_machinevar_name_info(UniqueId, Info, NewInfo),
261		NId = b(identifier(UniqueId),set(global(UniqueId)),NewInfo),
262		enumerate_deferred_sets(T, [(Ast,NId)|Acc], EIDs).
263
264		group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements) :-
265		group_enumerated_elements_by_set(NormalizedSets, Elements, [], GroupedElements).
266
267		group_enumerated_elements_by_set([], _, Acc, Acc).
268		group_enumerated_elements_by_set([(RealId,NormalizedId)|T], Elements, Acc, GroupedElements) :-
269		RealId = b(_,set(Type),_),
270		findall(E, ( member(E, Elements),
271		E = b(_,Type,_)
272		), Group),
273		NormalizedId = b(identifier(NormalizedIdName),_,_),
274		group_enumerated_elements_by_set(T, Elements, [NormalizedIdName-Group|Acc], GroupedElements).
275
276		enumerate_enum_elements(NormalizedSets, Elements, EElements) :-
277		group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements),
278		% enum elements from 1 to n (reminder: fd(1,Name))
279		maplist(enumerate_enum_elements_aux(NormalizedSets, 1, []), GroupedElements, TempEElements),
280		append(TempEElements, EElements).
281
282		enumerate_enum_elements_aux(_, _, Acc, _-[], Acc).
283		enumerate_enum_elements_aux(NormalizedSets, C, Acc, NormalizedIdName-[Element|T], NormalizedIds) :-
284		% enum elements are normalized as follows: NormSetName+'e'+Id
285		atom_concat(NormalizedIdName, e, TempName),
286		Element = b(identifier(_),Type,Info),
287		number_codes(C, CC),
288		atom_codes(AC, CC),
289		atom_concat(TempName, AC, NormalizedName),
290		C1 is C+1,
291		normalize_id_type(NormalizedSets, Type, NType),
292		NElement = b(identifier(NormalizedName),NType,Info),
293		enumerate_enum_elements_aux(NormalizedSets, C1, [(Element,NElement)|Acc], NormalizedIdName-T, NormalizedIds).
294
295		adapt_machinevar_name_info(Name, Info, NewInfo) :-
296		select(synthesis(machinevar,_), Info, TempInfo),
297		NewInfo = [synthesis(machinevar,Name)|TempInfo],
298		!.
299		adapt_machinevar_name_info(_, Info, Info).
300
301		% create a list of tuples (OldId,NewId)
302		get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames, NRecordFieldNames) :-
303		full_b_machine(Machine),
304		Machine = machine(_,SectionList),
305		member('deferred_sets'/DSets, SectionList),
306		member('enumerated_sets'/ESets, SectionList),
307		member('enumerated_elements'/Elements, SectionList),
308		member('operation_bodies'/OperationBodies, SectionList),
309		findall(OpNameId, member(b(operation(OpNameId,_,_,_),_,_), OperationBodies), OperationNames),
310		findall(ReturnIds, member(b(operation(_,ReturnIds,_,_),_,_), OperationBodies), TempReturnIds),
311		findall(Params, member(b(operation(_,_,Params,_),_,_), OperationBodies), TempParams),
312		tools:flatten(TempParams, Params),
313		tools:flatten(TempReturnIds, ReturnIds),
314		enumerate_ids([], 'p', Params, NParams),
315		enumerate_ids([], 'r', ReturnIds, NReturnIds),
316		enumerate_ids([], 'o', OperationNames, NOperationNames),
317		b_get_machine_all_constants(MachineConstants),
318		b_get_machine_variables(MachineVars),
319		random_permutation(ESets, RESets),
320		random_permutation(DSets, RDSets),
321		append(RESets, RDSets, RSets),
322		random_permutation(MachineVars, RMachineVars),
323		enumerate_record_fields_from_types(MachineConstants, [], NRecordFieldNames1),
324		enumerate_record_fields_from_types(MachineVars, NRecordFieldNames1, NRecordFieldNames),
325		enumerate_deferred_sets(RSets, [], NormalizedSets),
326		% pass the new set names to adapt the types of identifiers too
327		enumerate_ids(NormalizedSets, 'v', RMachineVars, EMachineVars),
328		enumerate_ids(NormalizedSets, 'c', MachineConstants, EMachineConstants),
329		enumerate_enum_elements(NormalizedSets, Elements, EElements),
330		append([EMachineConstants,EElements,EMachineVars,NParams,NReturnIds], NormalizedIds),
331		!.
332
333		value_to_ast(Value, b(value(Value),Type,[])) :-
334		kernel_objects:infer_value_type(Value, Type).
335
336		normalize_string(NormalizedStrings, String, NString, NormalizedStrings) :-
337		% string has already been seen
338		member((NString,String), NormalizedStrings),
339		!.
340		normalize_string(NormalizedStrings, String, NString, [(NString,String)|NormalizedStrings]) :-
341		length(NormalizedStrings, AmountOfStrings),
342		AmountOfStrings1 is AmountOfStrings+1,
343		number_codes(AmountOfStrings1, CIndex),
344		append([83], CIndex, CString),
345		atom_codes(NString, CString),
346		!.
347
348		map_normalize_ids_in_b_ast(Env, Ast, Ast, Env) :-
349		normalization_inline_defs_only(true), !.
350		map_normalize_ids_in_b_ast(Env, Ast, NewAst, NewEnv) :-
351		map_normalize_ids_in_b_ast_(Env, Ast, NewAst, NewEnv).
352
353		map_normalize_ids_in_b_ast_(Env, [], [], Env).
354		map_normalize_ids_in_b_ast_(Env, [Ast|T], [NAst|NT], NewEnv) :-
355		normalize_ids_in_b_ast(Env, Ast, NAst, Env1),
356		map_normalize_ids_in_b_ast_(Env1, T, NT, NewEnv).
357
358		% TO DO: environment
359		% Note: always returns a typed B AST
360		normalize_ids_in_b_ast(Env, b(truth,pred,Info), NAst, NewEnv) :-
361		!,
362		NAst = b(truth,pred,Info),
363		NewEnv = Env.
364		normalize_ids_in_b_ast(Env, b(falsity,pred,Info), NAst, NewEnv) :-
365		!,
366		NAst = b(falsity,pred,Info),
367		NewEnv = Env.
368		normalize_ids_in_b_ast(Env, pred_true, NAst, NewEnv) :-
369		!,
370		NAst = b(value(pred_true),boolean,[]),
371		NewEnv = Env.
372		normalize_ids_in_b_ast(Env, pred_false, NAst, NewEnv) :-
373		!,
374		NAst = b(value(pred_false),boolean,[]),
375		NewEnv = Env.
376		normalize_ids_in_b_ast(Env, b(integer(Value),integer,Info), NAst, NewEnv) :-
377		!,
378		NAst = b(integer(Value),integer,Info),
379		NewEnv = Env.
380		normalize_ids_in_b_ast(Env, b(identifier(op(Name)),_,_), NOperationName, NewEnv) :-
381		!,
382		Env = [_,_,_,NOperationNames,_],
383		member((b(identifier(op(Name)),_,_),NOperationName), NOperationNames),
384		NewEnv = Env.
385		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NId, NewEnv) :-
386		Node =.. [function|Args],
387		!,
388		map_normalize_ids_in_b_ast(Env, Args, NArgs, NewEnv),
389		NNode =.. [function|NArgs],
390		NId = b(NNode,Type,Info).
391		/* normalize_ids_in_b_ast(Env, b(rlevent(EventName,Section,Status,Params,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmod,AbstractEvents),Type,Info), NAst, NewEnv) :-
392		!,
393		normalize_ids_in_b_ast(Env, EventName, NEventName, _),
394		map_normalize_ids_in_b_ast(Env, Params, NParams, _),
395		normalize_ids_in_b_ast(Env, Guard, NGuard, Env1),
396		map_normalize_ids_in_b_ast(Env1, Theorems, NTheorems, Env2),
397		map_normalize_ids_in_b_ast(Env2, Actions, NActions, Env3),
398		map_normalize_ids_in_b_ast(Env3, VWitnesses, NVWitnesses, Env4),
399		map_normalize_ids_in_b_ast(Env4, PWitnesses, NPWitnesses, Env5),
400		normalize_ids_in_b_ast(Env5, Unmod, NUnmod, Env6),
401		map_normalize_ids_in_b_ast(Env6, AbstractEvents, NAbstractEvents, NewEnv),
402		NNode = rlevent(NEventName,Section,Status,NParams,NGuard,NTheorems,NActions,NVWitnesses,NPWitnesses,NUnmod,NAbstractEvents),
403		NAst = b(NNode,Type,Info). */
404		normalize_ids_in_b_ast(Env, b(operation(OperationName,ReturnIds,Params,Body),Type,Info), NAst, NewEnv) :-
405		!,
406		normalize_ids_in_b_ast(Env, OperationName, NOperationName, _),
407		map_normalize_ids_in_b_ast(Env, ReturnIds, NReturnIds, _),
408		map_normalize_ids_in_b_ast(Env, Params, NParams, _),
409		normalize_ids_in_b_ast(Env, Body, NBody, NewEnv),
410		NNode = operation(NOperationName,NReturnIds,NParams,NBody),
411		NAst = b(NNode,Type,Info).
412		normalize_ids_in_b_ast(Env, b(Node,subst,Info), NAst, NewEnv) :-
413		Node =.. [Functor,Assignments],
414		( Functor = select
415		; Functor = parallel
416		; Functor = sequence
417		),
418		!,
419		map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv),
420		NNode =.. [Functor,NAssignments],
421		NAst = b(NNode,subst,Info).
422		normalize_ids_in_b_ast(Env, b(struct(Record),Type,Info), b(struct(NRecord),NType,NInfo), NewEnv) :-
423		normalize_ids_in_b_ast(Env, Record, NRecord, NewEnv),
424		NewEnv = [_,_,NormalizedIds,_,_],
425		normalize_id_type(NormalizedIds, Type, NType),
426		adapt_synthesis_ast_info(NewEnv, Info, NInfo).
427		normalize_ids_in_b_ast(Env, b(rec(Fields),Type,Info), b(rec(NFields),NType,NInfo), NewEnv) :-
428		normalize_record_fields(Env, Fields, NFields, NewEnv),
429		NewEnv = [_,_,NormalizedIds,_,_],
430		normalize_id_type(NormalizedIds, Type, NType),
431		adapt_synthesis_ast_info(NewEnv, Info, NInfo).
432		normalize_ids_in_b_ast(Env, b(record_field(Id,Field),Type,Info), b(record_field(NId,NField),NType,NInfo), NewEnv) :-
433		normalize_ids_in_b_ast(Env, Id, NId, Env1),
434		normalize_ids_in_b_ast(Env1, Field, NField, NewEnv),
435		NewEnv = [_,_,NormalizedIds,_,_],
436		normalize_id_type(NormalizedIds, Type, NType),
437		adapt_synthesis_ast_info(NewEnv, Info, NInfo).
438		normalize_ids_in_b_ast(Env, b(assign(Ids,Assignments),subst,Info), b(assign(NIds,NAssignments),subst,Info), NewEnv) :-
439		map_normalize_ids_in_b_ast(Env, Ids, NIds, _),
440		map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv).
441		normalize_ids_in_b_ast(Env, b(assign_single_id(Id,Assignment),subst,Info), b(assign_single_id(NId,NAssignment),subst,Info), NewEnv) :-
442		normalize_ids_in_b_ast(Env, Id, NId, _),
443		normalize_ids_in_b_ast(Env, Assignment, NAssignment, NewEnv).
444		normalize_ids_in_b_ast(Env, b(value(global_set(SetName)),_,_), NId, NewEnv) :-
445		!,
446		Env = [_,NormalizedSets,_,_,_],
447		member((b(identifier(SetName),_,_),NId), NormalizedSets),
448		NewEnv = Env.
449		normalize_ids_in_b_ast(Env, In, NewId, NewEnv) :-
450		( In = string(String), Info = []
451		; In = b(string(String),string,Info)),
452		normalize_strings,
453		!,
454		NewId = b(string(NString),string,NInfo),
455		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
456		normalize_string(NormalizedStrings, String, NString, NewNormalizedStrings),
457		NewEnv = [NewNormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
458		adapt_synthesis_ast_info(NewEnv, Info, NInfo).
459		normalize_ids_in_b_ast(Env, b(string(String),string,Info), Out, NewEnv) :-
460		!,
461		Out = b(string(String),string,Info),
462		NewEnv = Env.
463		normalize_ids_in_b_ast(Env, string(String), Out, NewEnv) :-
464		!,
465		Out = b(string(String),string,[]),
466		NewEnv = Env.
467		normalize_ids_in_b_ast(Env, b(EmptySet,set(Type),Info), b(empty_set,set(NType),NInfo), Env) :-
468		(EmptySet = set_extension([]); EmptySet = empty_set),
469		adapt_synthesis_ast_info(Env, Info, NInfo),
470		Env = [_,NormalizedSets,_,_,_],
471		normalize_id_type(NormalizedSets, Type, NType).
472		normalize_ids_in_b_ast(Env, b(EmptySeq,Type,Info), b(empty_sequence,NType,NInfo), Env) :-
473		(EmptySeq = sequence_extension([]); EmptySeq = empty_sequence),
474		adapt_synthesis_ast_info(Env, Info, NInfo),
475		Env = [_,NormalizedSets,_,_,_],
476		normalize_id_type(NormalizedSets, Type, NType).
477		normalize_ids_in_b_ast(Env, List, NAst, NewEnv) :-
478		List \= [],
479		is_list(List),
480		!,
481		map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
482		NewList = [b(_,Type,_)|_],
483		NAst = b(set_extension(NewList),set(Type),[]).
484		normalize_ids_in_b_ast(Env, Ast, NewSetNode, NewEnv) :-
485		( Ast = b(value(avl_set(Avl)),set(Type),Info)
486		; Ast = avl_set(Avl),
487		Type = set(any),
488		Info = []
489		),
490		!,
491		avl_to_list(Avl, TList),
492		findall(L, member(L-_, TList), List),
493		map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
494		NewSetNode = b(set_extension(NewList),set(NType),NInfo),
495		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
496		Env = [_,NormalizedSets,_,_,_],
497		normalize_id_type(NormalizedSets, Type, NType).
498		normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
499		Env = [_,NormalizedSets,_,_,_],
500		member((b(identifier(Name),_,_),NId), NormalizedSets),
501		!,
502		NewEnv = Env.
503		normalize_ids_in_b_ast(Env, Name, NewName, NewEnv) :-
504		Env = [_,_,_,_,NRecordFieldNames],
505		member((Name,NName), NRecordFieldNames),
506		!,
507		NewName = NName,
508		NewEnv = Env.
509		normalize_ids_in_b_ast(Env, b(identifier(Name),Type,Info), NId, NewEnv) :-
510		Env = [_,_,_,_,NRecordFieldNames],
511		member((Name,NName), NRecordFieldNames),
512		!,
513		normalize_id_type(NRecordFieldNames, Type, NType),
514		NId = b(identifier(NName),NType,Info),
515		NewEnv = Env.
516		normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
517		Env = [_,_,NormalizedIds,_,_],
518		member((b(identifier(Name),_,_),NId), NormalizedIds),
519		!,
520		NewEnv = Env.
521		normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
522		Env = [_,NormalizedSets,_,_,_],
523		atom_concat(SetName, Nr, Name),
524		member((b(identifier(SetName),_,_),NId), NormalizedSets),
525		!,
526		NId = b(identifier(NSetName),NType,NInfo),
527		atom_concat(NSetName, e, NNSetName),
528		atom_concat(NNSetName, Nr, NName),
529		NAst = b(identifier(NName),NType,NInfo),
530		NewEnv = Env.
531		normalize_ids_in_b_ast(Env, (A1,A2), NAst, NewEnv) :-
532		!,
533		% value couple
534		normalize_ids_in_b_ast(Env, A1, NA1, Env1),
535		normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
536		NA1 = b(_,T1,_),
537		NA2 = b(_,T2,_),
538		NAst = b(couple(NA1,NA2),couple(T1,T2),[]).
539		normalize_ids_in_b_ast(Env, b(couple(A1,A2),Type,Info), NAst, NewEnv) :-
540		!,
541		normalize_ids_in_b_ast(Env, A1, NA1, Env1),
542		normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
543		adapt_synthesis_ast_info(Env, Info, NInfo),
544		Env = [_,NormalizedSets,_,_,_],
545		normalize_id_type(NormalizedSets, Type, NType),
546		NAst = b(couple(NA1,NA2),NType,NInfo).
547		normalize_ids_in_b_ast(Env, b(value(fd(Nr,SetName)),_,Info), b(Node,Type,NInfo), NewEnv) :-
548		normalize_ids_in_b_ast(Env, fd(Nr,SetName), TAst, NewEnv),
549		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
550		TAst = b(Node,Type,_).
551		normalize_ids_in_b_ast(Env, fd(Nr,SetName), NAst, NewEnv) :-
552		Env = [_,NormalizedSets,_,_,_],
553		member((b(identifier(SetName),_,_),NId), NormalizedSets),
554		!,
555		NId = b(identifier(NSetName),set(NType),_),
556		atom_concat(NSetName, e, TempName),
557		number_codes(Nr, NC),
558		atom_codes(AN, NC),
559		atom_concat(TempName, AN, NName),
560		NAst = b(identifier(NName),NType,[]),
561		NewEnv = Env.
562		normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
563		Env = [_,NormalizedSets,NormalizedIds,_,_],
564		atom(Name),
565		atom_concat(NameP, Prime, Name),
566		( Prime == '__prime'
567		; Prime == '\''
568		),
569		( member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedSets)
570		;
571		member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedIds)
572		),
573		!,
574		atom_concat(TName, Prime, NName),
575		NAst = b(identifier(NName),NType,NInfo),
576		NewEnv = Env.
577		%% local environment
578		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
579		Node =.. [Functor,Ids,Pred],
580		( Functor == exists
581		; Functor == comprehension_set
582		),
583		!,
584		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
585		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
586		findall(NId, member((_,NId), EIds), NIds),
587		append(EIds, NormalizedIds, NNormalizedIds),
588		normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
589		adapt_synthesis_ast_info(Env1, Info, NInfo),
590		NNode =.. [Functor,NIds,NPred],
591		NAst = b(NNode,Type,NInfo),
592		NewEnv = Env.
593		normalize_ids_in_b_ast(Env, b(forall(Ids,LHS,RHS),Type,Info), NAst, NewEnv) :-
594		!,
595		% TO DO: refactor creation of local ids
596		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
597		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
598		findall(NId, member((_,NId), EIds), NIds),
599		append(EIds, NormalizedIds, NNormalizedIds),
600		normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], LHS, NLHS, Env1),
601		normalize_ids_in_b_ast(Env1, RHS, NRHS, Env2),
602		adapt_synthesis_ast_info(Env2, Info, NInfo),
603		NAst = b(forall(NIds,NLHS,NRHS),Type,NInfo),
604		NewEnv = Env.
605		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
606		Node =.. [Functor,Ids,Pred,Int],
607		( Functor == general_sum
608		; Functor == general_product
609		),
610		!,
611		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
612		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
613		findall(NId, member((_,NId), EIds), NIds),
614		append(EIds, NormalizedIds, NNormalizedIds),
615		normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
616		normalize_ids_in_b_ast(Env1, Int, NInt, _),
617		NNode =.. [Functor,NIds,NPred,NInt],
618		NewEnv = Env,
619		NAst = b(NNode,Type,Info).
620		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
621		Node =.. [Functor,Ids,PredOrExpr],
622		( Functor == becomes_such
623		; Functor == becomes_element_of
624		),
625		!,
626		map_normalize_ids_in_b_ast(Env, Ids, NIds, Env1),
627		normalize_ids_in_b_ast(Env1, PredOrExpr, NPredOrExpr, NewEnv),
628		NNode =.. [Functor,NIds,NPredOrExpr],
629		NAst = b(NNode,Type,Info).
630		normalize_ids_in_b_ast(Env, b(iteration(Id,Int),Type,Info), NAst, NewEnv) :-
631		!,
632		normalize_ids_in_b_ast(Env, Id, NId, NewEnv),
633		NAst = b(iteration(NId,Int),Type,Info).
634		normalize_ids_in_b_ast(Env, b(choice(Substs),Type,Info), NAst, NewEnv) :-
635		!,
636		map_normalize_ids_in_b_ast(Env, Substs, NSubsts, NewEnv),
637		NAst = b(choice(NSubsts),Type,Info).
638		normalize_ids_in_b_ast(Env, b(kodkod(Int,List),Type,Info), NAst, NewEnv) :-
639		!,
640		map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
641		NAst = b(kodkod(Int,NList),Type,Info).
642		normalize_ids_in_b_ast(Env, b(assertion_expression(Expr1,Msg,Expr2),Type,Info), NAst, NewEnv) :-
643		!,
644		normalize_ids_in_b_ast(Env, Expr1, NExpr1, Env1),
645		normalize_ids_in_b_ast(Env1, Expr2, NExpr2, NewEnv),
646		NAst = b(assertion_expression(NExpr1,Msg,NExpr2),Type,Info).
647		normalize_ids_in_b_ast(Env, b(external_function_call(FuncName,Exprs),Type,Info), NAst, NewEnv) :-
648		!,
649		map_normalize_ids_in_b_ast(Env, Exprs, NExprs, NewEnv),
650		NAst = b(external_function_call(FuncName,NExprs),Type,Info).
651		normalize_ids_in_b_ast(Env, b(operation_call(Id,L1,L2),Type,Info), NAst, NewEnv) :-
652		!,
653		normalize_ids_in_b_ast(Env, Id, NId, Env1),
654		map_normalize_ids_in_b_ast(Env1, L1, NL1, Env2),
655		map_normalize_ids_in_b_ast(Env2, L2, NL2, NewEnv),
656		NAst = b(operation_call(NId,NL1,NL2),Type,Info).
657		normalize_ids_in_b_ast(Env, b(while(Cond,Subst,Invariant,Variant),Type,Info), NAst, NewEnv) :-
658		!,
659		normalize_ids_in_b_ast(Env, Cond, NCond, Env1),
660		normalize_ids_in_b_ast(Env1, Subst, NSubst, Env2),
661		normalize_ids_in_b_ast(Env2, Invariant, NInvariant, Env3),
662		normalize_ids_in_b_ast(Env3, Variant, NVariant, NewEnv),
663		NAst = b(while(NCond,NSubst,NInvariant,NVariant),Type,Info).
664		normalize_ids_in_b_ast(Env, b(partition(Id,List),Type,Info), NAst, NewEnv) :-
665		!,
666		normalize_ids_in_b_ast(Env, Id, NId, Env1),
667		map_normalize_ids_in_b_ast(Env1, List, NList, NewEnv),
668		NAst = b(partition(NId,NList),Type,Info).
669		normalize_ids_in_b_ast(Env, b(if(IfElsifs),Type,Info), NAst, NewEnv) :-
670		!,
671		map_normalize_ids_in_b_ast(Env, IfElsifs, NIfElsifs, NewEnv),
672		NAst = b(if(NIfElsifs),Type,Info).
673		normalize_ids_in_b_ast(Env, b(var(Ids,Subst),Type,Info), NAst, NewEnv) :-
674		!,
675		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
676		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
677		findall(NId, member((_,NId), EIds), NIds),
678		append(EIds, NormalizedIds, NNormalizedIds),
679		Env1 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
680		normalize_ids_in_b_ast(Env1, Subst, NSubst, _),
681		NAst = b(var(NIds,NSubst),Type,Info),
682		NewEnv = Env.
683		normalize_ids_in_b_ast(Env, b(any(Ids,Pred,Subst),Type,Info), NAst, NewEnv) :-
684		!,
685		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
686		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
687		findall(NId, member((_,NId), EIds), NIds),
688		append(EIds, NormalizedIds, NNormalizedIds),
689		normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
690		normalize_ids_in_b_ast(Env1, Subst, NSubst, _),
691		NAst = b(any(NIds,NPred,NSubst),Type,Info),
692		NewEnv = Env.
693		normalize_ids_in_b_ast(Env, b(lazy_lookup_expr(RawIdName),Type,Info), NAst, NewEnv) :-
694		atom(RawIdName),
695		!,
696		Env = [_,_,NormalizedIds,_,_],
697		member((b(identifier(RawIdName),_,_),b(identifier(NRawIdName),_,_)), NormalizedIds),
698		NAst = b(lazy_lookup_expr(NRawIdName),Type,Info),
699		NewEnv = Env.
700		normalize_ids_in_b_ast(Env, b(recursive_let(Id,Expr),Type,Info), NAst, NewEnv) :-
701		!,
702		normalize_ids_in_b_ast(Env, Id, NId, Env1),
703		normalize_ids_in_b_ast(Env1, Expr, NExpr, _),
704		NewEnv = Env,
705		NAst = b(recursive_let(NId,NExpr),Type,Info).
706		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
707		Node =.. [Functor,Ids,PredOrExprs,Sub],
708		( Functor == let_expression
709		; Functor == let_predicate
710		; Functor == let
711		),
712		!,
713		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
714		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
715		findall(NId, member((_,NId), EIds), NIds),
716		append(EIds, NormalizedIds, NNormalizedIds),
717		Env0 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
718		( is_list(PredOrExprs)
719		->
720		map_normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
721		; normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
722		),
723		normalize_ids_in_b_ast(Env1, Sub, NSub, _),
724		NNode =.. [Functor,NIds,NExprs,NSub],
725		NAst = b(NNode,Type,Info),
726		NewEnv = Env. % normalized ids are local
727		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
728		Node =.. [Functor,Id,PredOrExprs,Sub],
729		( Functor == lazy_let_pred
730		; Functor == lazy_let_expr
731		; Functor == reorder_lazy_let_pred
732		; Functor == reorder_lazy_let_expr
733		),
734		!,
735		Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
736		Ids = [Id],
737		enumerate_ids(NormalizedSets, 'l', Ids, EIds),
738		findall(NId, member((_,NId), EIds), NIds),
739		NIds = [NId],
740		append(EIds, NormalizedIds, NNormalizedIds),
741		Env0 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
742		( is_list(PredOrExprs)
743		->
744		map_normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
745		; normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
746		),
747		normalize_ids_in_b_ast(Env1, Sub, NSub, _),
748		NNode =.. [Functor,NId,NExprs,NSub],
749		NAst = b(NNode,Type,Info),
750		NewEnv = Env. % normalized ids are local
751		%%
752		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
753		Node = value(Arg),
754		is_list(Arg),
755		!,
756		map_normalize_ids_in_b_ast(Env, Arg, NArg, NewEnv),
757		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
758		Env = [_,NormalizedSets,_,_,_],
759		normalize_id_type(NormalizedSets, Type, NType),
760		NNode = set_extension(NArg),
761		NAst = b(NNode,NType,NInfo).
762		normalize_ids_in_b_ast(Env, b(value(Value),_Type,Info), b(Node,NType,NInfo), Env) :-
763		normalize_ids_in_b_ast(Env, Value, NAst, NewEnv),
764		NAst = b(Node,NType,_),
765		adapt_synthesis_ast_info(NewEnv, Info, NInfo).
766		normalize_ids_in_b_ast(Env, b(set_extension(List),Type,Info), NAst, NewEnv) :-
767		!,
768		map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
769		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
770		Env = [_,NormalizedSets,_,_,_],
771		normalize_id_type(NormalizedSets, Type, NType),
772		NAst = b(set_extension(NList),NType,NInfo).
773		normalize_ids_in_b_ast(Env, b(sequence_extension(List),Type,Info), NAst, NewEnv) :-
774		!,
775		map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
776		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
777		Env = [_,NormalizedSets,_,_,_],
778		normalize_id_type(NormalizedSets, Type, NType),
779		NAst = b(sequence_extension(NList),NType,NInfo).
780		normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
781		Node =.. [Functor|Args],
782		b_component(Functor),
783		!,
784		map_normalize_ids_in_b_ast(Env, Args, NArgs, NewEnv),
785		adapt_synthesis_ast_info(NewEnv, Info, NInfo),
786		NNode =.. [Functor|NArgs],
787		Env = [_,NormalizedSets,_,_,_],
788		normalize_id_type(NormalizedSets, Type, NType),
789		NAst = b(NNode,NType,NInfo).
790		normalize_ids_in_b_ast(Env, [], NAst, NewEnv) :-
791		!,
792		NAst = b(empty_set,set(any),[]),
793		NewEnv = Env.
794		normalize_ids_in_b_ast(Env, Value, Ast, NewEnv) :-
795		value_to_ast(Value, Ast),
796		!,
797		Env = NewEnv.
798		normalize_ids_in_b_ast(Env, Ast, NAst, NewEnv) :-
799		whitelist(Ast),
800		!,
801		NAst = Ast,
802		NewEnv = Env.
803		normalize_ids_in_b_ast(Env, Ast, Ast, Env) :-
804		nl,
805		print(Ast),
806		nl,
807		add_warning(normalize_ids_in_b_ast, 'Skipped AST for normalization:', Ast).
808
809		whitelist('NATURAL').
810		whitelist('NATURAL1').
811		whitelist('NAT').
812		whitelist('NAT1').
813		whitelist('INTEGER').
814		whitelist('INT').
815		whitelist('BOOL').
816		whitelist('STRING').
817		whitelist('TRUE').
818		whitelist('FALSE').
819		whitelist(b(empty_sequence,_,_)).
820		whitelist(b(string_set,_,_)).
821		whitelist(b(empty_set,_,_)).
822		whitelist(b(bool_set,_,_)).
823		whitelist(b(boolean_true,_,_)).
824		whitelist(b(boolean_false,_,_)).
825		whitelist(b(max_int,_,_)).
826		whitelist(b(min_int,_,_)).
827		whitelist(b(external_pred_call(_,_),_,_)).
828
829		enumerate_record_fields_from_types(CstsOrVars, Acc, NRecordFieldNames) :-
830		length(Acc, C),
831		enumerate_record_fields_from_types(CstsOrVars, C, Acc, NRecordFieldNames).
832
833		enumerate_record_fields_from_types([], _, Acc, Acc).
834		enumerate_record_fields_from_types([CstOrVar|T], C, Acc, NRecordFieldNames) :-
835		CstOrVar = b(_,Type,_),
836		get_record_fields_from_type([Type], [], RecordFields),
837		!,
838		enumerate_record_fields(RecordFields, C, Acc, NewC, NewAcc),
839		enumerate_record_fields_from_types(T, NewC, NewAcc, NRecordFieldNames).
840		enumerate_record_fields_from_types([_|T], C, Acc, NRecordFieldNames) :-
841		enumerate_record_fields_from_types(T, C, Acc, NRecordFieldNames).
842
843		enumerate_record_fields([], NewC, Acc, NewC, Acc).
844		enumerate_record_fields([field(Name,_Type)|T], C, Acc, NewC, NewAcc) :-
845		\+ member((Name,_), Acc),
846		!,
847		C1 is C+1,
848		number_codes(C1, NC1),
849		atom_codes(AC1, NC1),
850		atom_concat('f', AC1, NName),
851		enumerate_record_fields(T, C1, [(Name,NName)|Acc], NewC, NewAcc).
852		enumerate_record_fields([_|T], C, Acc, NewC, NewAcc) :-
853		enumerate_record_fields(T, C, Acc, NewC, NewAcc).
854
855		get_record_fields_from_type([], Acc, RecordFields) :-
856		!,
857		RecordFields = Acc.
858		get_record_fields_from_type([record(Fields)|T], Acc, RecordFields) :-
859		!,
860		append(Fields, Acc, NewAcc),
861		get_record_fields_from_type(T, NewAcc, RecordFields).
862		get_record_fields_from_type([Type|T], Acc, RecordFields) :-
863		Type =.. [_|InnerT],
864		get_record_fields_from_type(InnerT, Acc, Acc1),
865		get_record_fields_from_type(T, Acc1, RecordFields).
866
867		normalize_record_fields(Env, [], [], Env).
868		normalize_record_fields(Env, [Field|T], [NField|NT], NewEnv) :-
869		Env = [_,_,_,_,NRecordFieldNames],
870		Field = field(Name,Value),
871		( member((Name,NName), NRecordFieldNames),
872		Env1 = Env
873		; Env = [A,B,C,D,NRecordFieldNames],
874		length(NRecordFieldNames, L),
875		L1 is L+1,
876		number_codes(L1, NL1),
877		atom_codes(AL1, NL1),
878		atom_concat('f', AL1, NName),
879		Env1 = [A,B,C,D,[(Name,NName)|NRecordFieldNames]]
880		),
881		normalize_ids_in_b_ast(Env1, Value, NValue, Env2),
882		NField = field(NName,NValue),
883		normalize_record_fields(Env2, T, NT, NewEnv).
884
885		adapt_synthesis_ast_info(Env, Info, NInfo) :-
886		Env = [_,NormalizedSets,NormalizedIds,_,_],
887		member(synthesis(machinevar,Name), Info),
888		( member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedSets)
889		; member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedIds)
890		),
891		!,
892		adapt_machinevar_name_info(NName, Info, NInfo).
893		adapt_synthesis_ast_info(Env, Info, Info) :-
894		% info already normalized
895		Env = [_,NormalizedSets,NormalizedIds,_,_],
896		member(synthesis(machinevar,NName), Info),
897		( member((_,b(identifier(NName),_,_)), NormalizedSets)
898		; member((_,b(identifier(NName),_,_)), NormalizedIds)
899		),
900		!.
901		adapt_synthesis_ast_info(_, Info, Info).
902
903		%% internal B/Event-B component names
904		b_component(precondition).
905		b_component(select).
906		b_component(select_when).
907		b_component(parameter).
908		b_component(function).
909		b_component(partial_function).
910		b_component(total_function).
911		b_component(partial_injection).
912		b_component(total_injection).
913		b_component(partial_surjection).
914		b_component(total_surjection).
915		b_component(total_bijection).
916		b_component(partial_bijection).
917		b_component(total_relation).
918		b_component(surjection_relation).
919		b_component(total_surjection_relation).
920		b_component(exists).
921		b_component(comprehension_set).
922		b_component(forall).
923		b_component(constant).
924		% relations
925		b_component(first_of_pair).
926		b_component(second_of_pair).
927		b_component(event_b_identity).
928		b_component(identity).
929		b_component(relations).
930		b_component(domain).
931		b_component(image).
932		b_component(range).
933		b_component(domain_restriction).
934		b_component(domain_subtraction).
935		b_component(range_restriction).
936		b_component(range_subtraction).
937		b_component(reflexive_closure).
938		b_component(closure).
939		% predicates
940		b_component(conjunct).
941		b_component(disjunct).
942		b_component(implication).
943		b_component(equivalence).
944		b_component(negation).
945		b_component(equal).
946		b_component(not_equal).
947		b_component(convert_bool).
948		b_component(if_then_else).
949		b_component(if_elsif).
950		% special case in normalize_ids_in_b_ast/4 for if([...])
951		% sets
952		b_component(member).
953		b_component(not_member).
954		b_component(union).
955		b_component(intersection).
956		b_component(set_subtraction).
957		b_component(cartesian_product).
958		b_component(direct_product).
959		b_component(card).
960		b_component(subset).
961		b_component(not_subset).
962		b_component(subset_strict).
963		b_component(not_subset_strict).
964		b_component(pow_subset).
965		b_component(pow1_subset).
966		b_component(fin_subset).
967		b_component(fin1_subset).
968		b_component(finite).
969		b_component(general_union).
970		b_component(general_intersection).
971		b_component(composition).
972		% b_component(general_sum).
973		% b_component(general_product).
974		% numbers
975		b_component(integer_set_natural).
976		b_component(integer_set_natural1).
977		b_component(implementable_natural).
978		b_component(implementable_natural1).
979		b_component(integer_set).
980		b_component(integer_set_min_max).
981		b_component(min).
982		b_component(max).
983		b_component(add).
984		b_component(minus).
985		b_component(multiplication).
986		b_component(div).
987		b_component(modulo).
988		b_component(greater).
989		b_component(less).
990		b_component(greater_equal).
991		b_component(less_equal).
992		b_component(interval).
993		b_component(power_of).
994		b_component(unary_minus).
995		% sequences
996		b_component(seq).
997		b_component(seq1).
998		b_component(iseq).
999		b_component(iseq1).
1000		b_component(perm).
1001		b_component(concat).
1002		b_component(size).
1003		b_component(rev).
1004		b_component(reverse).
1005		b_component(first).
1006		b_component(last).
1007		b_component(tail).
1008		b_component(front).
1009		b_component(insert_front).
1010		b_component(insert_tail).
1011		b_component(restrict_front).
1012		b_component(restrict_tail).
1013		b_component(overwrite).
1014		b_component(general_concat).
1015		% substitutions
1016		b_component(skip).
1017		b_component(assign).
1018		b_component(parallel).
1019		b_component(parallel_product).
1020		b_component(sequence).
1021		b_component(assertion).
1022		% following are B components but handled as special cases for local identifier normalization in normalize_ids_in_b_ast/4
1023		% b_component(becomes_such).
1024		% b_component(becomes_element_of).
1025		% b_component(let).
1026		% b_component(let_predicate).
1027		% b_component(let_expression).
1028		% b_component(any).