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