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). |