1 :- module(b_machine_identifier_normalization, [normalize_b_machine/1,
2 normalize_b_machine/2,
3 map_normalize_ids_in_b_ast/4,
4 normalize_ids_in_b_ast/4,
5 get_normalized_id_name_mapping/3,
6 enumerate_ids/4,
7 normalize_id_type/3,
8 b_component/1]).
9
10 :- use_module(library(lists)).
11 :- use_module(library(sets), [subtract/3]).
12 :- use_module(library(avl), [avl_to_list/2]).
13 :- use_module(library(random), [random_permutation/2]).
14 :- use_module(library(file_systems), [file_exists/1]).
15
16 :- use_module(probsrc(bmachine)).
17 :- use_module(probsrc(error_manager)).
18 :- use_module(probsrc(module_information), [module_info/2]).
19
20 :- module_info(group, synthesis).
21 :- module_info(description, 'Normalize all identifiers and strings in the currently loaded B machine. Patterns like variables, deferred sets, or enumerated elements are preserved using specific prefixes.').
22
23 %% normalize_b_machine(+InputFilePath).
24 %
25 % Normalise all identifier in a B machine, load the normalised machine, and save the new machine file.
26 normalize_b_machine(InputFilePath) :-
27 is_b_machine_file(InputFilePath, Prefix),
28 atom_concat(Prefix, '_normalized.mch', OutputFilePath),
29 normalize_b_machine(InputFilePath, OutputFilePath).
30
31 %% normalize_b_machine(+InputFilePath,+OutputFilePath).
32 normalize_b_machine(InputFilePath, OutputFilePath) :-
33 machine_exists(InputFilePath),
34 b_load_machine_from_file(InputFilePath),
35 b_machine_precompile,
36 !,
37 get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames),
38 Env = [[],NormalizedSets,NormalizedIds,NOperationNames],
39 full_b_machine(Machine),
40 Machine = machine(MachineName,SectionList),
41 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),
42 % definitions are inlined and removed
43 map_normalize_ids_in_b_ast(Env, DeferredSets, NDeferredSets, _),
44 map_normalize_ids_in_b_ast(Env, EnumeratedSets, NEnumeratedSets, _),
45 map_normalize_ids_in_b_ast(Env, EnumeratedElements, NEnumeratedElements, _),
46 map_normalize_ids_in_b_ast(Env, OperationBodies, NOperationBodies, _),
47 b_get_machine_variables(MachineVars),
48 map_normalize_ids_in_b_ast(Env, MachineVars, NVariables, _),
49 b_get_machine_all_constants(MachineConstants),
50 map_normalize_ids_in_b_ast(Env, MachineConstants, NConstants, _),
51 normalize_ids_in_b_ast(Env, LinkingInvariant, NLinkingInvariant, Env1),
52 b_get_invariant_from_machine(MachineInvariant),
53 normalize_ids_in_b_ast(Env1, MachineInvariant, NInvariant, Env2),
54 b_get_properties_from_machine(MachineProperties),
55 normalize_ids_in_b_ast(Env2, MachineProperties, NProperties, Env3),
56 b_get_initialisation_from_machine(MachineInitialisation, _),
57 normalize_ids_in_b_ast(Env3, MachineInitialisation, NInitialisation, Env4),
58 get_all_assertions_from_machine(MachineAssertions),
59 map_normalize_ids_in_b_ast(Env4, MachineAssertions, NAssertions, _),
60 % unchanged: 'used'/_,'freetypes'/_,'operators'/_,'values'/_,'meta'/_,'constraints'/_,'promoted'/_,'unpromoted'/_,'internal_parameters'/_,'parameters'/_
61 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]),
62 b_set_typed_machine(NMachine),
63 b_write_machine_representation_to_file(none, OutputFilePath).
64 normalize_b_machine(InputFilePath, _) :-
65 add_error(normalize_b_machine, 'Error in B machine:', InputFilePath),
66 fail.
67
68 machine_exists(FilePath) :-
69 file_exists(FilePath),
70 !.
71 machine_exists(FilePath) :-
72 add_error(normalize_b_machine, 'File does not exist:', FilePath),
73 fail.
74
75 is_b_machine_file(FilePath, _) :-
76 \+ atom(FilePath),
77 !,
78 add_error(normalize_b_machine, 'Prolog atom expected.', []),
79 fail.
80 is_b_machine_file(FilePath, Prefix) :-
81 member(Ext, ['.mch','.eventb','.prob']),
82 atom_concat(Prefix, Ext, FilePath),
83 !.
84 is_b_machine_file(FilePath, _) :-
85 add_error(normalize_b_machine, 'Wrong file format. B/Event-B machine with extension .mch, .eventb or .prob expected:', FilePath),
86 fail.
87
88 normalize_id_type(NormalizedSets, Name, NormalizedName) :-
89 member((b(identifier(Name),_,_),b(identifier(NormalizedName),_,_)), NormalizedSets),
90 !.
91 normalize_id_type(NormalizedSets, Type, NType) :-
92 Type =.. [Functor|Args],
93 Args \== [],
94 !,
95 maplist(normalize_id_type(NormalizedSets), Args, NArgs),
96 NType =.. [Functor|NArgs].
97 normalize_id_type(_, Type, Type).
98
99 enumerate_ids(NormalizedSets, Prefix, IDs, EIDs) :-
100 atom(Prefix),
101 !,
102 enumerate_ids_acc(NormalizedSets, Prefix, IDs, 0, [], EIDs).
103 enumerate_ids(_, _, _, _) :-
104 add_error(enumerate_ids, 'Error: Prefix has to be an atom.', []).
105
106 enumerate_ids_acc(_, _, [], _, Acc, Acc).
107 enumerate_ids_acc(NormalizedSets, Prefix, [b(identifier(op(Name)),Type,Info)|T], C, Acc, EIDs) :-
108 get_enumerated_name(Prefix, C, NewName, C1),
109 NId = b(identifier(op(NewName)),Type,Info),
110 enumerate_ids_acc(NormalizedSets, Prefix, T, C1, [(b(identifier(op(Name)),Type,Info),NId)|Acc], EIDs).
111 enumerate_ids_acc(NormalizedSets, Prefix, [Ast|T], C, Acc, EIDs) :-
112 ( Ast = b(identifier(Name),Type,Info)
113 ; ( Ast = b(_,Type,Info),
114 member(synthesis(machinevar,Name), Info)
115 )
116 ),
117 normalize_id_type(NormalizedSets, Type, NewType),
118 get_enumerated_name(Prefix, C, NewName, C1),
119 adapt_machinevar_name_info(NewName, Info, NewInfo),
120 NId = b(identifier(NewName),NewType,NewInfo),
121 enumerate_ids_acc(NormalizedSets, Prefix, T, C1, [(b(identifier(Name),Type,Info),NId)|Acc], EIDs).
122
123 get_enumerated_name(Prefix, C, NewName, C1) :-
124 number_codes(C, NC),
125 atom_codes(AC, NC),
126 atom_concat(Prefix, AC, NewName),
127 C1 is C+1.
128
129 enumerate_deferred_sets([], _, Acc, Acc).
130 enumerate_deferred_sets([Ast|T], C, Acc, EIDs) :-
131 number_codes(C, NC),
132 atom_codes(AC, NC),
133 atom_concat('s', AC, NewName),
134 C1 is C+1,
135 Ast = b(_,_,Info),
136 adapt_machinevar_name_info(NewName, Info, NewInfo),
137 NId = b(identifier(NewName),set(global(NewName)),NewInfo),
138 enumerate_deferred_sets(T, C1, [(Ast,NId)|Acc], EIDs).
139
140 group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements) :-
141 group_enumerated_elements_by_set(NormalizedSets, Elements, [], GroupedElements).
142
143 group_enumerated_elements_by_set([], _, Acc, Acc).
144 group_enumerated_elements_by_set([(RealId,NormalizedId)|T], Elements, Acc, GroupedElements) :-
145 RealId = b(_,set(Type),_),
146 findall(E, ( member(E, Elements),
147 E = b(_,Type,_)
148 ), Group),
149 NormalizedId = b(identifier(NormalizedIdName),_,_),
150 group_enumerated_elements_by_set(T, Elements, [NormalizedIdName-Group|Acc], GroupedElements).
151
152 enumerate_enum_elements(NormalizedSets, Elements, EElements) :-
153 group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements),
154 % enum elements from 1 to n (reminder: fd(1,Name))
155 maplist(enumerate_enum_elements_aux(NormalizedSets, 1, []), GroupedElements, TempEElements),
156 append(TempEElements, EElements).
157
158 enumerate_enum_elements_aux(_, _, Acc, _-[], Acc).
159 enumerate_enum_elements_aux(NormalizedSets, C, Acc, NormalizedIdName-[Element|T], NormalizedIds) :-
160 % enum elements are normalized as follows: NormSetName+'e'+Id
161 atom_concat(NormalizedIdName, e, TempName),
162 Element = b(identifier(_),Type,Info),
163 number_codes(C, CC),
164 atom_codes(AC, CC),
165 atom_concat(TempName, AC, NormalizedName),
166 C1 is C+1,
167 normalize_id_type(NormalizedSets, Type, NType),
168 NElement = b(identifier(NormalizedName),NType,Info),
169 enumerate_enum_elements_aux(NormalizedSets, C1, [(Element,NElement)|Acc], NormalizedIdName-T, NormalizedIds).
170
171 adapt_machinevar_name_info(Name, Info, NewInfo) :-
172 select(synthesis(machinevar,_), Info, TempInfo),
173 NewInfo = [synthesis(machinevar,Name)|TempInfo],
174 !.
175 adapt_machinevar_name_info(_, Info, Info).
176
177 % create a list of tuples (OldId,NewId)
178 get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames) :-
179 full_b_machine(Machine),
180 Machine = machine(_,SectionList),
181 member('deferred_sets'/DSets, SectionList),
182 member('enumerated_sets'/ESets, SectionList),
183 member('enumerated_elements'/Elements, SectionList),
184 member('operation_bodies'/OperationBodies, SectionList),
185 findall(OpNameId, member(b(operation(OpNameId,_,_,_),_,_), OperationBodies), OperationNames),
186 findall(ReturnIds, member(b(operation(_,ReturnIds,_,_),_,_), OperationBodies), TempReturnIds),
187 findall(Params, member(b(operation(_,_,Params,_),_,_), OperationBodies), TempParams),
188 tools:flatten(TempParams, Params),
189 tools:flatten(TempReturnIds, ReturnIds),
190 enumerate_ids([], 'p', Params, NParams),
191 enumerate_ids([], 'r', ReturnIds, NReturnIds),
192 enumerate_ids([], 'o', OperationNames, NOperationNames),
193 b_get_machine_all_constants(MachineConstants),
194 b_get_machine_variables(MachineVars),
195 random_permutation(ESets, RESets),
196 random_permutation(DSets, RDSets),
197 append(RESets, RDSets, RSets),
198 random_permutation(MachineVars, RMachineVars),
199 enumerate_deferred_sets(RSets, 0, [], NormalizedSets),
200 % pass the new set names to adapt the types of identifiers too
201 enumerate_ids(NormalizedSets, 'v', RMachineVars, EMachineVars),
202 enumerate_ids(NormalizedSets, 'c', MachineConstants, EMachineConstants),
203 enumerate_enum_elements(NormalizedSets, Elements, EElements),
204 append([EMachineConstants,EElements,EMachineVars,NParams,NReturnIds], NormalizedIds),
205 !.
206
207 value_to_ast(Value, b(value(Value),Type,[])) :-
208 kernel_objects:infer_value_type(Value, Type).
209
210 normalize_string(NormalizedStrings, String, NString, NormalizedStrings) :-
211 % string has already been seen
212 member((NString,String), NormalizedStrings),
213 !.
214 normalize_string(NormalizedStrings, String, NString, [(NString,String)|NormalizedStrings]) :-
215 length(NormalizedStrings, AmountOfStrings),
216 AmountOfStrings1 is AmountOfStrings+1,
217 number_codes(AmountOfStrings1, CIndex),
218 append([83], CIndex, CString),
219 atom_codes(NString, CString),
220 !.
221
222 map_normalize_ids_in_b_ast(Env, [], [], Env).
223 map_normalize_ids_in_b_ast(Env, [Ast|T], [NAst|NT], NewEnv) :-
224 normalize_ids_in_b_ast(Env, Ast, NAst, Env1),
225 map_normalize_ids_in_b_ast(Env1, T, NT, NewEnv).
226
227 % TODO: environment
228 normalize_ids_in_b_ast(Env, b(truth,pred,Info), NAst, NewEnv) :-
229 !,
230 NAst = b(truth,pred,Info),
231 NewEnv = Env.
232 normalize_ids_in_b_ast(Env, b(falsity,pred,Info), NAst, NewEnv) :-
233 !,
234 NAst = b(falsity,pred,Info),
235 NewEnv = Env.
236 normalize_ids_in_b_ast(Env, pred_true, NAst, NewEnv) :-
237 !,
238 NAst = b(value(pred_true),boolean,[]),
239 NewEnv = Env.
240 normalize_ids_in_b_ast(Env, pred_false, NAst, NewEnv) :-
241 !,
242 NAst = b(value(pred_false),boolean,[]),
243 NewEnv = Env.
244 normalize_ids_in_b_ast(Env, b(integer(Value),integer,Info), NAst, NewEnv) :-
245 !,
246 NAst = b(integer(Value),integer,Info),
247 NewEnv = Env.
248 normalize_ids_in_b_ast(Env, b(identifier(op(Name)),_,_), NOperationName, NewEnv) :-
249 !,
250 Env = [_,_,_,NOperationNames],
251 member((b(identifier(op(Name)),_,_),NOperationName), NOperationNames),
252 NewEnv = Env.
253 normalize_ids_in_b_ast(Env, b(operation(OperationName,ReturnIds,Params,Body),Type,Info), NAst, NewEnv) :-
254 !,
255 normalize_ids_in_b_ast(Env, OperationName, NOperationName, _),
256 map_normalize_ids_in_b_ast(Env, ReturnIds, NReturnIds, _),
257 map_normalize_ids_in_b_ast(Env, Params, NParams, _),
258 normalize_ids_in_b_ast(Env, Body, NBody, NewEnv),
259 NNode = operation(NOperationName,NReturnIds,NParams,NBody),
260 NAst = b(NNode,Type,Info).
261 normalize_ids_in_b_ast(Env, b(Node,subst,Info), NAst, NewEnv) :-
262 Node =.. [Functor,Assignments],
263 ( Functor = select
264 ; Functor = parallel
265 ; Functor = sequence
266 ),
267 !,
268 map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv),
269 NNode =.. [Functor,NAssignments],
270 NAst = b(NNode,subst,Info).
271 normalize_ids_in_b_ast(Env, b(assign(Ids,Assignments),subst,Info), b(assign(NIds,NAssignments),subst,Info), NewEnv) :-
272 map_normalize_ids_in_b_ast(Env, Ids, NIds, _),
273 map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv).
274 normalize_ids_in_b_ast(Env, b(assign_single_id(Id,Assignment),subst,Info), b(assign_single_id(NId,NAssignment),subst,Info), NewEnv) :-
275 normalize_ids_in_b_ast(Env, Id, NId, _),
276 normalize_ids_in_b_ast(Env, Assignment, NAssignment, NewEnv).
277 normalize_ids_in_b_ast(Env, b(value(global_set(SetName)),_,_), NId, NewEnv) :-
278 !,
279 Env = [_,NormalizedSets,_,_],
280 member((b(identifier(SetName),_,_),NId), NormalizedSets),
281 NewEnv = Env.
282 normalize_ids_in_b_ast(Env, string(String), b(string(NString),string,[]), NewEnv) :-
283 Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames],
284 normalize_string(NormalizedStrings, String, NString, NewNormalizedStrings),
285 NewEnv = [NewNormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames].
286 normalize_ids_in_b_ast(Env, b(set_extension([]),set(Type),Info), b(set_extension([]),set(NType),NInfo), Env) :-
287 adapt_synthesis_ast_info(Env, Info, NInfo),
288 Env = [_,NormalizedSets,_,_],
289 normalize_id_type(NormalizedSets, Type, NType).
290 normalize_ids_in_b_ast(Env, b(sequence_extension([]),Type,Info), b(sequence_extension([]),NType,NInfo), Env) :-
291 adapt_synthesis_ast_info(Env, Info, NInfo),
292 Env = [_,NormalizedSets,_,_],
293 normalize_id_type(NormalizedSets, Type, NType).
294 normalize_ids_in_b_ast(Env, List, NAst, NewEnv) :-
295 List \= [],
296 is_list(List),
297 !,
298 map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
299 NewList = [b(_,Type,_)|_],
300 NAst = b(set_extension(NewList),set(Type),[]).
301 normalize_ids_in_b_ast(Env, Ast, NewSetNode, NewEnv) :-
302 ( Ast = b(value(avl_set(Avl)),set(Type),Info)
303 ; Ast = avl_set(Avl),
304 Type = set(any),
305 Info = []
306 ),
307 !,
308 avl_to_list(Avl, TList),
309 findall(L, member(L-_, TList), List),
310 map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
311 NewSetNode = b(set_extension(NewList),set(NType),NInfo),
312 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
313 Env = [_,NormalizedSets,_,_],
314 normalize_id_type(NormalizedSets, Type, NType).
315 normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
316 Env = [_,NormalizedSets,_,_],
317 member((b(identifier(Name),_,_),NId), NormalizedSets),
318 !,
319 NewEnv = Env.
320 normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
321 Env = [_,_,NormalizedIds,_],
322 member((b(identifier(Name),_,_),NId), NormalizedIds),
323 !,
324 NewEnv = Env.
325 normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
326 Env = [_,NormalizedSets,_,_],
327 atom_concat(SetName, Nr, Name),
328 member((b(identifier(SetName),_,_),NId), NormalizedSets),
329 !,
330 NId = b(identifier(NSetName),NType,NInfo),
331 atom_concat(NSetName, e, NNSetName),
332 atom_concat(NNSetName, Nr, NName),
333 NAst = b(identifier(NName),NType,NInfo),
334 NewEnv = Env.
335 normalize_ids_in_b_ast(Env, (A1,A2), NAst, NewEnv) :-
336 !,
337 % value couple
338 normalize_ids_in_b_ast(Env, A1, NA1, Env1),
339 normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
340 NA1 = b(_,T1,_),
341 NA2 = b(_,T2,_),
342 NAst = b(couple(NA1,NA2),couple(T1,T2),[]).
343 normalize_ids_in_b_ast(Env, b(couple(A1,A2),Type,Info), NAst, NewEnv) :-
344 !,
345 normalize_ids_in_b_ast(Env, A1, NA1, Env1),
346 normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
347 adapt_synthesis_ast_info(Env, Info, NInfo),
348 Env = [_,NormalizedSets,_,_],
349 normalize_id_type(NormalizedSets, Type, NType),
350 NAst = b(couple(NA1,NA2),NType,NInfo).
351 normalize_ids_in_b_ast(Env, b(value(fd(Nr,SetName)),_,Info), b(Node,Type,NInfo), NewEnv) :-
352 normalize_ids_in_b_ast(Env, fd(Nr,SetName), TAst, NewEnv),
353 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
354 TAst = b(Node,Type,_).
355 normalize_ids_in_b_ast(Env, fd(Nr,SetName), NAst, NewEnv) :-
356 Env = [_,NormalizedSets,_,_],
357 member((b(identifier(SetName),_,_),NId), NormalizedSets),
358 !,
359 NId = b(identifier(NSetName),set(NType),_),
360 atom_concat(NSetName, e, TempName),
361 number_codes(Nr, NC),
362 atom_codes(AN, NC),
363 atom_concat(TempName, AN, NName),
364 NAst = b(identifier(NName),NType,[]),
365 NewEnv = Env.
366 normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
367 Env = [_,NormalizedSets,NormalizedIds,_],
368 atom(Name),
369 atom_concat(NameP, Prime, Name),
370 ( Prime == '__prime'
371 ; Prime == '\''
372 ),
373 ( member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedSets)
374 ;
375 member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedIds)
376 ),
377 !,
378 atom_concat(TName, Prime, NName),
379 NAst = b(identifier(NName),NType,NInfo),
380 NewEnv = Env.
381 %% local environment
382 normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
383 Node =.. [Functor,Ids,Pred],
384 ( Functor == exists
385 ; Functor == comprehension_set
386 ),
387 !,
388 Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames],
389 enumerate_ids(NormalizedSets, 'l', Ids, EIds),
390 findall(NId, member((_,NId), EIds), NIds),
391 append(EIds, NormalizedIds, NNormalizedIds),
392 normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames], Pred, NPred, Env1),
393 adapt_synthesis_ast_info(Env1, Info, NInfo),
394 NNode =.. [Functor,NIds,NPred],
395 NAst = b(NNode,Type,NInfo),
396 NewEnv = Env.
397 normalize_ids_in_b_ast(Env, b(forall(Ids,LHS,RHS),Type,Info), NAst, NewEnv) :-
398 !,
399 Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames],
400 enumerate_ids(NormalizedSets, 'l', Ids, EIds),
401 findall(NId, member((_,NId), EIds), NIds),
402 append(EIds, NormalizedIds, NNormalizedIds),
403 normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames], LHS, NLHS, Env1),
404 normalize_ids_in_b_ast(Env1, RHS, NRHS, Env2),
405 adapt_synthesis_ast_info(Env2, Info, NInfo),
406 NAst = b(forall(NIds,NLHS,NRHS),Type,NInfo),
407 NewEnv = Env.
408 normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
409 Node =.. [Functor,Ids,Expr,Sub],
410 ( Functor == let_expression
411 ; Functor = let_predicate
412 ),
413 !,
414 Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames],
415 enumerate_ids(NormalizedSets, 'l', Ids, EIds),
416 findall(NId, member((_,NId), EIds), NIds),
417 append(EIds, NormalizedIds, NNormalizedIds),
418 normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames], Expr, NExpr, Env1),
419 normalize_ids_in_b_ast(Env1, Sub, NSub, Env2),
420 adapt_synthesis_ast_info(Env2, Info, NInfo),
421 NNode =.. [Functor,NIds,NExpr,NSub],
422 NAst = b(NNode,Type,NInfo),
423 NewEnv = Env.
424 %%
425 normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
426 Node =.. [value,Arg],
427 is_list(Arg),
428 !,
429 map_normalize_ids_in_b_ast(Env, Arg, NArg, NewEnv),
430 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
431 Env = [_,NormalizedSets,_,_],
432 normalize_id_type(NormalizedSets, Type, NType),
433 NNode = set_extension(NArg),
434 NAst = b(NNode,NType,NInfo).
435 normalize_ids_in_b_ast(Env, b(value(Value),_Type,Info), b(Node,NType,NInfo), Env) :-
436 normalize_ids_in_b_ast(Env, Value, NAst, NewEnv),
437 NAst = b(Node,NType,_),
438 adapt_synthesis_ast_info(NewEnv, Info, NInfo).
439 normalize_ids_in_b_ast(Env, b(set_extension(List),Type,Info), NAst, NewEnv) :-
440 !,
441 map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
442 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
443 Env = [_,NormalizedSets,_,_],
444 normalize_id_type(NormalizedSets, Type, NType),
445 NAst = b(set_extension(NList),NType,NInfo).
446 normalize_ids_in_b_ast(Env, b(sequence_extension(List),Type,Info), NAst, NewEnv) :-
447 !,
448 map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
449 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
450 Env = [_,NormalizedSets,_,_],
451 normalize_id_type(NormalizedSets, Type, NType),
452 NAst = b(sequence_extension(NList),NType,NInfo).
453 normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
454 Node =.. [Functor|Args],
455 b_component(Functor),
456 !,
457 map_normalize_ids_in_b_ast(Env, Args, NArgs, NewEnv),
458 adapt_synthesis_ast_info(NewEnv, Info, NInfo),
459 NNode =.. [Functor|NArgs],
460 Env = [_,NormalizedSets,_,_],
461 normalize_id_type(NormalizedSets, Type, NType),
462 NAst = b(NNode,NType,NInfo).
463 normalize_ids_in_b_ast(Env, [], NAst, NewEnv) :-
464 !,
465 NAst = b(set_extension([]),set(any),[]),
466 NewEnv = Env.
467 normalize_ids_in_b_ast(Env, Value, Ast, NewEnv) :-
468 value_to_ast(Value, Ast),
469 !,
470 Env = NewEnv.
471 normalize_ids_in_b_ast(Env, Ast, Ast, Env) :-
472 add_warning(normalize_ids_in_b_ast, 'Skipped AST for normalization:', Ast).
473
474 adapt_synthesis_ast_info(Env, Info, NInfo) :-
475 Env = [_,NormalizedSets,NormalizedIds,_],
476 member(synthesis(machinevar,Name), Info),
477 ( member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedSets)
478 ; member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedIds)
479 ),
480 !,
481 adapt_machinevar_name_info(NName, Info, NInfo).
482 adapt_synthesis_ast_info(Env, Info, Info) :-
483 % info already normalized
484 Env = [_,NormalizedSets,NormalizedIds,_],
485 member(synthesis(machinevar,NName), Info),
486 ( member((_,b(identifier(NName),_,_)), NormalizedSets)
487 ; member((_,b(identifier(NName),_,_)), NormalizedIds)
488 ),
489 !.
490 adapt_synthesis_ast_info(_, Info, Info).
491
492 b_component(precondition).
493 b_component(select).
494 b_component(select_when).
495 b_component(parameter).
496 b_component(function).
497 b_component(partial_function).
498 b_component(total_function).
499 b_component(partial_injection).
500 b_component(total_injection).
501 b_component(partial_surjection).
502 b_component(total_surjection).
503 b_component(total_bijection).
504 b_component(partial_bijection).
505 b_component(total_relation).
506 b_component(surjection_relation).
507 b_component(total_surjection_relation).
508 b_component(exists).
509 b_component(comprehension_set).
510 b_component(forall).
511 b_component(constant).
512 % relations
513 b_component(relations).
514 b_component(domain).
515 b_component(image).
516 b_component(range).
517 b_component(domain_restriction).
518 b_component(domain_subtraction).
519 b_component(range_restriction).
520 b_component(range_subtraction).
521 b_component(reflexive_closure).
522 b_component(closure).
523 % predicates
524 b_component(conjunct).
525 b_component(disjunct).
526 b_component(implication).
527 b_component(equivalence).
528 b_component(negation).
529 b_component(equal).
530 b_component(not_equal).
531 b_component(convert_bool).
532 b_component(if_then_else).
533 b_component(if_elsif).
534 % sets
535 b_component(member).
536 b_component(not_member).
537 b_component(union).
538 b_component(intersection).
539 b_component(set_subtraction).
540 b_component(cartesian_product).
541 b_component(card).
542 b_component(subset).
543 b_component(not_subset).
544 b_component(subset_strict).
545 b_component(not_subset_strict).
546 b_component(pow_subset).
547 b_component(pow1_subset).
548 b_component(fin_subset).
549 b_component(fin_subset1).
550 b_component(finite).
551 b_component(general_union).
552 b_component(general_intersection).
553 b_component(composition).
554 b_component(general_sum).
555 % numbers
556 b_component(integer_set_natural).
557 b_component(integer_set_natural1).
558 b_component(implementable_natural).
559 b_component(implementable_natural1).
560 b_component(integer_set).
561 b_component(integer_set_min_max).
562 b_component(min).
563 b_component(max).
564 b_component(add).
565 b_component(minus).
566 b_component(multiplication).
567 b_component(div).
568 b_component(modulo).
569 b_component(greater).
570 b_component(less).
571 b_component(greater_equal).
572 b_component(less_equal).
573 b_component(interval).
574 b_component(power_of).
575 b_component(unary_minus).
576 % sequences
577 b_component(seq).
578 b_component(seq1).
579 b_component(iseq).
580 b_component(perm).
581 b_component(concat).
582 b_component(size).
583 b_component(rev).
584 b_component(reverse).
585 b_component(first).
586 b_component(last).
587 b_component(tail).
588 b_component(front).
589 b_component(insert_front).
590 b_component(insert_tail).
591 b_component(restrict_front).
592 b_component(restrict_tail).
593 b_component(overwrite).
594 b_component(general_concat).
595 % substitutions
596 b_component(skip).
597 b_component(becomes_such).
598 b_component(becomes_element_of).
599 b_component(assign).
600 b_component(let).
601 b_component(any).
602 b_component(parallel).
603 b_component(sequence).