1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(record_detection,[replace_sets_by_records/2]). | |
6 | ||
7 | ||
8 | :- use_module(tools). | |
9 | :- use_module(self_check). | |
10 | ||
11 | :- use_module(module_information,[module_info/2]). | |
12 | :- module_info(group,typechecker). | |
13 | :- module_info(description,'This module detects bijections between deferred sets and cartesian products, and compiles them away.'). | |
14 | ||
15 | ||
16 | :- use_module(library(lists)). | |
17 | :- use_module(library(ordsets)). | |
18 | ||
19 | :- use_module(bmachine_structure). | |
20 | :- use_module(bsyntaxtree). | |
21 | :- use_module(btypechecker,[couplise_list/2]). | |
22 | :- use_module(preferences,[get_preference/2]). | |
23 | :- use_module(b_ast_cleanup,[clean_up/3]). | |
24 | ||
25 | replace_sets_by_records(Machine,ResultMachine) :- | |
26 | % replace until a fixpoint is reached | |
27 | replace_sets_by_records2(Machine,RMachine),!, | |
28 | replace_sets_by_records(RMachine,ResultMachine). | |
29 | /* we could do something like this for the values clause for deferred sets mapped to integer intervals: | |
30 | it would have to be done for all deferred sets + the problem is that the type checker runs before this code ! | |
31 | replace_sets_by_records(Machine,ResultMachine) :- | |
32 | bmachine:get_section(values,Machine,Values), | |
33 | member(b(values_entry(TID,TVal),_,Info),Values), | |
34 | get_texpr_id(TID,Set), | |
35 | bmachine:get_section(deferred_sets,Machine,Sets), | |
36 | get_texpr_id(TExpr,Set),member(TExpr,Sets), | |
37 | get_texpr_type(TVal,Type), | |
38 | !, | |
39 | Domain = TVal, | |
40 | replace_type_in_machine(GlobalSet,Type,Domain,Machine,ResultMachine). | |
41 | */ | |
42 | replace_sets_by_records(Machine,Machine). | |
43 | ||
44 | replace_sets_by_records2(Machine,ResultMachine) :- | |
45 | get_preference(use_record_construction,true), | |
46 | has_deferred_sets(Machine), | |
47 | get_section(deferred_sets,Machine,DeferredSets), | |
48 | select_section(properties,Properties,NewProperties,Machine,ConsMachine), | |
49 | select_constructor_axiom(Properties,DeferredSets,Set,Constructor,Cons,Domain,RestList1), | |
50 | (debug:debug_mode(on) -> format('Record detected for deferred set ~w~n',[Set]) ; true), | |
51 | % now we know that we have detected a record | |
52 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine). | |
53 | ||
54 | :- use_module(error_manager,[add_internal_error/2]). | |
55 | :- use_module(translate,[print_bexpr/1]). | |
56 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor1,Cons,Domain,RestList1,ResultMachine) :- | |
57 | Cons = constructor(ConstructorDomain,RecDomainType,_), | |
58 | add_texpr_infos(Constructor1,[record_detection(constructor)],Constructor), | |
59 | create_constructor_definition(Constructor,ConstructorDomain,ConsDef), | |
60 | (debug:debug_mode(on) -> print_bexpr(ConsDef),nl ; true), %% | |
61 | create_recordset_definition(Set,Domain,SetDef), | |
62 | (debug:debug_mode(on) -> print_bexpr(SetDef),nl ; true), %% | |
63 | create_optional_field_access(Set,Domain,Constructor,RecordFunIds,RestList1,RestList), | |
64 | conjunct_predicates([ConsDef,SetDef|RestList],NewProperties), | |
65 | move_deferred_set(Set,ConsMachine,SetMachine), | |
66 | % replace the constants (constructor,accessors,update functions) by versions that | |
67 | % have an info field that indicate their function (needed later to exclude them when | |
68 | % adding additional constraints): | |
69 | foldl(replace_constant,[Constructor|RecordFunIds],SetMachine,M2), | |
70 | %% print(replacing(Set,RecDomainType)),nl, %% | |
71 | replace_type_in_machine(Set,RecDomainType,Domain,M2,ResultMachine), | |
72 | !. | |
73 | replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine) :- | |
74 | add_internal_error('Replacing record failed ',replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine)),fail. | |
75 | ||
76 | has_deferred_sets(Machine) :- | |
77 | get_section(deferred_sets,Machine,DefSets), | |
78 | DefSets = [_|_]. | |
79 | ||
80 | % replace_constant(+NewConstant,+In,-Out): | |
81 | % replace a constant by a new one of the same name | |
82 | replace_constant(NewConstant,In,Out) :- | |
83 | % try the replacement in abstract and concrete constants: | |
84 | ( replace_id_in_section(NewConstant,abstract_constants,In,Out) -> true | |
85 | ; replace_id_in_section(NewConstant,concrete_constants,In,Out) -> true | |
86 | ; otherwise -> fail). | |
87 | replace_id_in_section(NewId,Section,In,Out) :- | |
88 | get_texpr_id(NewId,Id), get_texpr_id(OldId,Id), | |
89 | select_section(Section,OldIds,NewIds,In,Out), | |
90 | selectchk(OldId,OldIds,NewId,NewIds). | |
91 | ||
92 | % select_constructor_axiom(+Properties,+Sets,-Set,-Constructor,-Cons,-Domain,-RestList) | |
93 | % Chooses a constructor axiom if any exists | |
94 | % Properties: The properties (a typed predicate) of the machine | |
95 | % Sets: The list of deferred sets (a list of typed identifiers) | |
96 | % Set,Constructor,Cons,Domain: see is_constructor_axiom/6 below | |
97 | % RestList: A list of remaining predicates after removing the constructor axiom | |
98 | select_constructor_axiom(Properties,Sets,Set,Constructor,Cons,Domain,RestList) :- | |
99 | conjunction_to_list(Properties,PList), | |
100 | ? | select(Prop,PList,RestList), |
101 | is_constructor_axiom(Prop,Sets,Set,Constructor,Cons,Domain). | |
102 | ||
103 | create_constructor_definition(Constructor,Domain,ConsDef) :- | |
104 | create_texpr(equal(Constructor,Identity),pred,[],ConsDef), | |
105 | get_texpr_type(Constructor,Type), | |
106 | create_texpr(identity(Domain),Type,[],Identity). | |
107 | ||
108 | create_recordset_definition(SetName,Domain,SetDef) :- | |
109 | create_texpr(equal(Set,Domain),pred,[],SetDef), | |
110 | get_texpr_type(Domain,Type), | |
111 | create_texpr(identifier(SetName),Type,[],Set). | |
112 | ||
113 | % move_deferred_set(Set+,OldMachine+,NewMachine-) :- | |
114 | % Moves a deferred set to the concrete_constants section | |
115 | % Set: The (untyped) id of the set | |
116 | % OldMachine: The complete B machine where the set is a deferred set | |
117 | % NewMachine: The same B machine, but the deferred set is now a constant | |
118 | move_deferred_set(Set,OldMachine,NewMachine) :- | |
119 | select_section(deferred_sets,Sets,NewSets,OldMachine,Machine1), | |
120 | get_texpr_id(TSet,Set), | |
121 | selectchk(TSet,Sets,NewSets), | |
122 | select_section(concrete_constants,Constants,[TSet|Constants],Machine1,NewMachine). | |
123 | ||
124 | % is_constructor_axiom(+TAxiom,+Sets,-GType,-TConstructor,-Cons,-TDom) | |
125 | % TAxiom: A typed predicate | |
126 | % Sets: A list of typed identifiers, the deferred sets | |
127 | % GType: The (untyped) ID of the set that represents the record | |
128 | % TConstructor: The constructor function (a bijection from a domain to the record type) | |
129 | % Cons: a term of the form constructor(Domain,DomainType,Kind) where Kind is either constructor or destructor | |
130 | % TDom: The domain of the constructor | |
131 | % The constructor can actually be a destructor, i.e. a bijection from the record to the domain. | |
132 | % The third argument in the Cons term indicates which case has been encountered | |
133 | is_constructor_axiom(TAxiom,Sets,GType,TConstructor,Cons,TDom) :- | |
134 | % The axiom has the form c : Dom >->> Set, where | |
135 | % c and Set are identifiers | |
136 | get_texpr_expr(TAxiom,member(TConstructor,TBijection)), | |
137 | get_texpr_type(TConstructor,set(couple(FromType,ToType))), | |
138 | get_texpr_id(TConstructor,_), % just make sure that TConstructor is an identifer | |
139 | FromType \= ToType, % otherwise bijection maps to itself | |
140 | ? | (get_texpr_expr(TBijection,total_bijection(TDom,TSet)), |
141 | Cons=constructor(TDom,FromType,constructor) | |
142 | ; get_texpr_expr(TBijection,total_bijection(TSet,TDom)), | |
143 | % we have the bijection the other way; does not really matter for a bijection anyway | |
144 | Cons = constructor(TSet,ToType,destructor)), | |
145 | get_texpr_type(TSet,set(global(GType))), | |
146 | get_texpr_id(TSet,GType), | |
147 | % check if the set is a deferred set, not an enumerated set | |
148 | get_texpr_id(SetTest,GType), | |
149 | memberchk(SetTest,Sets), | |
150 | % in Dom, there should be no reference to Set | |
151 | no_reference(TDom,GType). | |
152 | ||
153 | ||
154 | no_reference(TExpr,Type) :- | |
155 | syntaxtraversion(TExpr,Expr,_,_,Subs,_), | |
156 | no_reference2(Expr,Type), | |
157 | no_reference_l(Subs,Type). | |
158 | no_reference2(identifier(Type),Type) :- !,fail. | |
159 | no_reference2(_,_). | |
160 | no_reference_l([],_). | |
161 | no_reference_l([Expr|Rest],Type) :- | |
162 | no_reference(Expr,Type), | |
163 | no_reference_l(Rest,Type). | |
164 | ||
165 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
166 | create_optional_field_access(SetName,Domain,Constructor,UpAc,Properties,RestList) :- | |
167 | get_texpr_id(Set,SetName), | |
168 | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Properties,P4), | |
169 | !, | |
170 | replace_update_definitions(Fields,Set,Constructor,Updates,P4,P5), | |
171 | maplist(create_field_definition(Domain),Fields,Accessors,FieldDefs), | |
172 | append(FieldDefs,P5,RestList), | |
173 | % A list of identifiers that are used at update and accessor functions: | |
174 | append(Updates,Accessors,UpAc). | |
175 | create_optional_field_access(_Set,_Domain,_Constructor,[],Properties,Properties). | |
176 | ||
177 | find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Pin,Pout) :- | |
178 | % F1 >< ... >< Fn : Set -->> Domain | |
179 | bsyntax_pattern(member(FieldProduct,total_surjection(-Set,-Domain)), SurjMemb), | |
180 | selectchk(SurjMemb,Pin,P1), | |
181 | % the injection is only defined for closed records | |
182 | % F1 >< ... >< Fn : Set >-> Domain | |
183 | bsyntax_pattern(member(-FieldProduct,total_injection(-Set,-Domain)), InjMemb), | |
184 | selectchk(InjMemb,P1,P2), | |
185 | access_locations(FieldProduct,Domain,Fields), | |
186 | % for each field accessor fx, there should be a declaration | |
187 | % fx : Record --> Domain, remove them | |
188 | remove_field_declarations(Fields,Set,P2,P3), | |
189 | % for each field accessor fx, there should be a predicate | |
190 | % !(v1,...,...), remove it | |
191 | remove_field_quantifiers(Fields,Constructor,P3,Pout). | |
192 | ||
193 | % find the field accessor functions | |
194 | access_locations(TExpr,TDomain,Fields) :- | |
195 | access_locations1(TExpr,TDomain,[],Fields). | |
196 | access_locations1(TExpr,TDomain,Path,Fields) :- | |
197 | get_texpr_expr(TExpr,Expr), | |
198 | access_locations2(Expr,TExpr,TDomain,Path,Fields). | |
199 | access_locations2(identifier(_Id),TExpr,TDomain,Path,[fieldloc(TExpr,TDomain,RPath)]) :- rev(Path,RPath). | |
200 | access_locations2(direct_product(F1,F2),_TExpr,TCart,Path,Fields) :- | |
201 | get_texpr_expr(TCart,cartesian_product(D1,D2)), | |
202 | access_locations1(F1,D1,[left |Path],Fields1), | |
203 | access_locations1(F2,D2,[right|Path],Fields2), | |
204 | append(Fields1,Fields2,Fields). | |
205 | ||
206 | create_field_definition(RecordDomain,fieldloc(AccessorId1,Domain,Path),AccessorId,Equal) :- | |
207 | add_texpr_infos(AccessorId1,[record_detection(accessor)],AccessorId), | |
208 | create_texpr(equal(AccessorId,AccessorDef),pred,[],Equal), | |
209 | % the accessor function maps a record to the domain | |
210 | get_texpr_type(RecordDomain,set(RecordTupleType)), | |
211 | create_accessor_function(Domain,Path,RecordTupleType,AccessorDef). | |
212 | ||
213 | create_accessor_function(Domain,Path,RecordTupleType,AccessDefinition) :- | |
214 | % fieldAccess = {r,v | v = prj...(r)} | |
215 | create_texpr(identifier(r),RecordTupleType,[],RecordVar), | |
216 | get_texpr_type(Domain,set(FieldType)), | |
217 | create_texpr(identifier(v),FieldType,[],ValueVar), | |
218 | create_texpr(equal(ValueVar,Projection),pred,[],Equals), | |
219 | create_projection(Path,RecordVar,Projection), | |
220 | %translate:print_bexpr(Projection),nl, | |
221 | create_symbolic_comprehension_set([RecordVar,ValueVar],Equals, | |
222 | [record_detection(accessor)],AccessDefinition). | |
223 | ||
224 | create_symbolic_comprehension_set(Ids,Pred,Info,Result) :- | |
225 | get_texpr_types(Ids,Types), | |
226 | couplise_list(Types,ElementType), | |
227 | create_texpr(comprehension_set(Ids,Pred),set(ElementType),Info,CompSet), | |
228 | mark_bexpr_as_symbolic(CompSet,Result). | |
229 | ||
230 | create_projection(Path,RecordVar,ProjectionResult) :- | |
231 | get_texpr_type(RecordVar,InnerType), | |
232 | create_projection_aux(Path,InnerType,RecordVar,ProjectionResult). | |
233 | ||
234 | create_projection_aux([],_InnerType,SubExpression,SubExpression). % return record as is | |
235 | create_projection_aux([Loc|Path],couple(A,B),SubExpression,ProjectionResult) :- | |
236 | ( Loc==left -> Expr=first_of_pair(SubExpression), InnerType=A | |
237 | ; Loc==right -> Expr=second_of_pair(SubExpression),InnerType=B), | |
238 | create_texpr(Expr,InnerType,[],NewSubExpression), | |
239 | create_projection_aux(Path,InnerType,NewSubExpression,ProjectionResult). | |
240 | ||
241 | ||
242 | % remove fieldx : RecSet --> Domx | |
243 | remove_field_declarations([],_RecSet,Predicates,Predicates). | |
244 | remove_field_declarations([fieldloc(AccessorId,Domain,_Path)|Frest],RecSet,Pin,Pout) :- | |
245 | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pinter), | |
246 | remove_field_declarations(Frest,RecSet,Pinter,Pout). | |
247 | remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pout) :- | |
248 | bsyntax_pattern(member(-AccessorId,total_function(-RecSet,-Domain)),Pattern), | |
249 | selectchk(Pattern,Pin,Pout). | |
250 | ||
251 | % remove !(f1,...,fn). ( f1:T1 & ... & fn:Tn => fieldx(make_rec(f1|->f2|->f3)) = fx) | |
252 | remove_field_quantifiers(Fields,Constructor,Pin,Pout) :- | |
253 | remove_field_quantifiers2(Fields,0,Constructor,Pin,Pout). | |
254 | ||
255 | remove_field_quantifiers2(Fields,N,Constructor,Pin,Pout) :- | |
256 | ( nth0(N,Fields,fieldloc(Field,_Dom,_Path)) -> | |
257 | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pinter), | |
258 | N2 is N+1, | |
259 | remove_field_quantifiers2(Fields,N2,Constructor,Pinter,Pout) | |
260 | ; otherwise -> | |
261 | Pin=Pout). | |
262 | remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pout) :- | |
263 | make_field_identifiers(Fields,FSkels), | |
264 | get_texpr_ids(FSkels,Ids), | |
265 | nth0(N,FSkels,Ref), | |
266 | bsyntax_pattern(forall(FSkels,_,equal(function(-Field,function(-Constructor,ConstArg)),-Ref)),ForAll), | |
267 | select(ForAll,Pin,Pout), | |
268 | are_mappings(ConstArg,Ids),!. | |
269 | are_mappings(TExpr,Ids) :- | |
270 | are_mappings2(TExpr,Ids,[]). | |
271 | are_mappings2(TExpr) --> | |
272 | {get_texpr_expr(TExpr,Expr)}, | |
273 | are_mappings3(Expr). | |
274 | are_mappings3(identifier(Id)) --> [Id]. | |
275 | are_mappings3(couple(A,B)) --> | |
276 | are_mappings2(A), | |
277 | are_mappings2(B). | |
278 | ||
279 | make_field_identifiers([],[]). | |
280 | make_field_identifiers([FieldAcc|FRest],[Id|Irest]) :- | |
281 | make_field_identifier(FieldAcc,Id), | |
282 | make_field_identifiers(FRest,Irest). | |
283 | make_field_identifier(fieldloc(FieldAcc,_,_),Id) :- | |
284 | get_texpr_type(FieldAcc,set(couple(_,FType))), | |
285 | create_texpr(identifier(_),FType,_,Id). | |
286 | ||
287 | replace_update_definitions(Fields,RecSet,Constructor,Updates,Pin,Pout) :- | |
288 | replace_update_definitions2(Fields,Fields,RecSet,Constructor,Updates,Pin,Pout). | |
289 | replace_update_definitions2([],_Fields,_RecSet,_Constructor,[],Predicates,Predicates). | |
290 | replace_update_definitions2([fieldloc(AccessorId,FDomain,Path)|Frest],Fields,RecSet, | |
291 | Constructor,[UpdateId|URest],Pin,Pout) :- | |
292 | replace_update_definition(AccessorId,FDomain,Path,Fields,RecSet,Constructor,UpdateId,Pin,Pinter), | |
293 | replace_update_definitions2(Frest,Fields,RecSet,Constructor,URest,Pinter,Pout). | |
294 | ||
295 | % Identify two predicates of the form | |
296 | % updatex : Record ** Domain --> Record | |
297 | % !(Rec,New).(_ => updatex(Rec,New) = Constructor(..)) | |
298 | % and replace them by | |
299 | % updatex = {i,o | #(n,f1,...,fn).(i=(f1,...,fn)|->n & o=(f1,...,n,..,fn))} | |
300 | replace_update_definition(FieldAccessorId,FieldDomain,Path,Fields, | |
301 | RecSet,Constructor,Update,Pin,[Equal|Pout]) :- | |
302 | % Updatex : Record ** Domain --> Record | |
303 | bsyntax_pattern(member(Update1,total_function(cartesian_product(-RecSet,-FieldDomain),-RecSet)),Memb), | |
304 | select(Memb,Pin,P1), | |
305 | % !(Rec,New).(_ => Updatex(Rec,New) = Constructor(..)) | |
306 | % TODO: Implication and constructor arguments are missing | |
307 | bsyntax_pattern(forall([Rec,New],_,equal(function(-Update1,couple(-Rec,-New)), | |
308 | function(-Constructor,_))), ForAll), | |
309 | select(ForAll,P1,Pout), | |
310 | !, | |
311 | add_texpr_infos(Update1,[record_detection(update)],Update), | |
312 | % Updatex = {i,o | #(i,r,f1,...,fn).(i=r|->n & ) } | |
313 | create_texpr(equal(Update,Function),pred,[],Equal), | |
314 | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function). | |
315 | ||
316 | create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function) :- | |
317 | % {i,o | #n,f1,...,fn. ( i=( (f1,...,fn) |-> n ) ) & o=(f1,...,n,...,fn) } | |
318 | get_texpr_type(FieldAccessorId,set(couple(RecType,FieldType))), | |
319 | InType = couple(RecType,FieldType), | |
320 | create_texpr(identifier(update__in),InType,[],In), | |
321 | create_texpr(identifier(update__out),RecType,[],Out), | |
322 | create_symbolic_comprehension_set([In,Out],Pred,[record_detection(update)],CompSet), | |
323 | ||
324 | % #(n,f1,...,fn).(...&...) | |
325 | %create_exists([NewValue|FieldVars],ExistsPred,Pred), % moved below; see comment | |
326 | create_var_for_field(FieldAccessorId,FieldDomain,'f$n__',NewValue), | |
327 | maplist(create_field_var,Fields,FieldVars), | |
328 | create_texpr(conjunct(InEqual,OutEqual),pred,[],ExistsPred), | |
329 | ||
330 | % i = ( (f1,...,fn) |-> n ) | |
331 | create_texpr(equal(In,InPair),pred,[],InEqual), | |
332 | create_texpr(couple(OldFields,NewValue),InType,[],InPair), | |
333 | create_record_tuple(Fields,FieldVars,OldFields), | |
334 | ||
335 | % o = (f1,...,n,...,fn) | |
336 | create_texpr(equal(Out,NewFields),pred,[],OutEqual), | |
337 | update_record_tuple(Path,NewValue,OldFields,NewFields), | |
338 | ||
339 | % the creation of the exists has to be deferred until here as used identifiers are computed: | |
340 | create_exists([NewValue|FieldVars],ExistsPred,Pred), | |
341 | %translate:print_bexpr(CompSet),nl, | |
342 | ||
343 | % we need to call the clean-up functions because exists(...) needs more | |
344 | % information about which identifier are used and that information | |
345 | % is added by clean_up/3. | |
346 | clean_up(CompSet,[],Function). | |
347 | ||
348 | % for a fields, create an identifier with the corresponding type | |
349 | create_field_var(fieldloc(AccessorId,Domain,_Path),TId) :- | |
350 | create_var_for_field(AccessorId,Domain,'f$__',TId). | |
351 | create_var_for_field(AccessorId,Domain,Prefix,TId) :- | |
352 | get_texpr_id(AccessorId,FId), | |
353 | get_texpr_type(Domain,set(Type)), | |
354 | atom_concat(Prefix,FId,VId), | |
355 | create_texpr(identifier(VId),Type,[],TId). | |
356 | ||
357 | % for a list of fields and identifiers f1,...,fn, create a tuple (f1,...,fn) | |
358 | create_record_tuple([],[],_). | |
359 | create_record_tuple([fieldloc(_,_,Path)|Frest],[FieldVar|Vrest],Tuple) :- | |
360 | create_record_tuple2(Path,FieldVar,Tuple), | |
361 | create_record_tuple(Frest,Vrest,Tuple). | |
362 | create_record_tuple2([],Expr,Expr). | |
363 | create_record_tuple2([Loc|Path],Expr,Tuple) :- | |
364 | ( Loc==left -> create_texpr(couple(Sub,_),couple(SubType,_),[],Tuple) | |
365 | ; Loc==right -> create_texpr(couple(_,Sub),couple(_,SubType),[],Tuple)), | |
366 | get_texpr_type(Sub,SubType), | |
367 | create_record_tuple2(Path,Expr,Sub). | |
368 | ||
369 | % in a tuple representing a record, replace one field | |
370 | update_record_tuple([],NewValue,_OldFields,NewValue). | |
371 | update_record_tuple([Loc|Path],NewValue,OldFields,NewFields) :- | |
372 | get_texpr_expr(OldFields,couple(A,B)), | |
373 | get_texpr_type(OldFields,Type), | |
374 | create_texpr(couple(X,Y),Type,[],NewFields), | |
375 | ( Loc==left -> X=NewSub,A=OldSub,Y=B | |
376 | ; Loc==right -> Y=NewSub,B=OldSub,X=A), | |
377 | update_record_tuple(Path,NewValue,OldSub,NewSub). | |
378 | ||
379 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
380 | % replace_type_in_machine(+T1,+T2,+Domain,+OldMachine,-NewMachine): | |
381 | % T1: The name of the global set that refers to the old type | |
382 | % T2: The new type that should replace global(T1) | |
383 | % Domain: A B expression that describes the domain of the record, used to | |
384 | % constrain introduced identifiers | |
385 | % OldMachine: The B machine before replacement | |
386 | % NewMachine: The resulting B machine | |
387 | replace_type_in_machine(T1,T2,Domain,OldMachine,NewMachine) :- | |
388 | extract_constants_that_are_types(OldMachine,RTT), | |
389 | ( is_just_type(Domain,RTT) -> Domain2 = simple | |
390 | ; otherwise -> Domain2 = Domain), | |
391 | % add predicates to constrain variables or constants, if needed | |
392 | foldl(add_type_constraint_to_section(T1,Domain2), | |
393 | [decl([abstract_constants,concrete_constants],properties), | |
394 | decl([abstract_variables,concrete_variables],invariant)], | |
395 | OldMachine,Machine1), | |
396 | % replace the type in the expressions of the machine (identifier declarations | |
397 | % can be treated as expressions, too) | |
398 | foldl(replace_type_in_machine2(T1,T2,Domain2), | |
399 | [abstract_constants,concrete_constants, | |
400 | abstract_variables,concrete_variables, | |
401 | promoted, unpromoted, | |
402 | constraints, properties, invariant, assertions, | |
403 | initialisation, operation_bodies], | |
404 | Machine1,NewMachine). | |
405 | replace_type_in_machine2(T1,T2,Domain,Sec,In,Out) :- | |
406 | select_section_texprs(Sec,Old,New,In,Out), | |
407 | replace_type_in_exprs(Old,T1,T2,Domain,New). | |
408 | replace_type_in_expr(TExpr,T1,T2,Domain,New) :- | |
409 | % if identifiers (e.g. i) are declared in an expression (like in forall), we may have | |
410 | % to add an predicate (e.g. i:1..4) | |
411 | ( Domain=simple -> % the domain is a whole type, no additional constraint needed | |
412 | TExpr2 = TExpr | |
413 | ; has_declared_identifier(TExpr,Ids),contains_identifier_with_type(Ids,T1) -> | |
414 | % identifiers are introduced and one of them contains the record type | |
415 | add_type_declarations(TExpr,global(T1),Domain,Ids,TExpr2) | |
416 | ; otherwise -> % no identifiers introduced that use the record type | |
417 | TExpr = TExpr2 | |
418 | ), | |
419 | create_texpr(Expr,EType,Info,TExpr2), % de-assemble old expression | |
420 | replace_type(EType,T1,T2,NType), % replace type global(T1) by T2 in Type | |
421 | create_texpr(NExpr,NType,Info,New), % assemble new expression with new type | |
422 | syntaxtransformation(Expr,Subs,_Names,NSubs,NExpr), % continue with sub-expressions | |
423 | replace_type_in_exprs(Subs,T1,T2,Domain,NSubs). | |
424 | replace_type_in_exprs([],_T1,_T2,_Domain,[]). | |
425 | replace_type_in_exprs([Sub|Irest],T1,T2,Domain,[NSub|Orest]) :- | |
426 | replace_type_in_expr(Sub,T1,T2,Domain,NSub), | |
427 | replace_type_in_exprs(Irest,T1,T2,Domain,Orest). | |
428 | ||
429 | contains_identifier_with_type(Ids,T1) :- | |
430 | get_texpr_type(TId,Type), | |
431 | member(TId,Ids), | |
432 | contains_type(global(T1),Type). | |
433 | ||
434 | add_type_constraint_to_section(_ToReplace,simple,_Decl,In,Out) :- | |
435 | !,In=Out. | |
436 | add_type_constraint_to_section(ToReplace,Domain,decl(IdSecs,PredSec),In,Out) :- | |
437 | maplist(aux_get_section(In),IdSecs,IdsL),append(IdsL,Ids1), | |
438 | % do not add constraints for accessor and update functions for records: | |
439 | exclude(is_record_detection_expr,Ids1,Ids), | |
440 | ( contains_identifier_with_type(Ids,ToReplace) -> | |
441 | create_type_predicate(global(ToReplace),Domain,Ids,P), | |
442 | ( is_truth(P) -> In=Out % Trivial, nothing to do | |
443 | ; otherwise -> % Add the type constraint to the relevant predicate section | |
444 | select_section(PredSec,OldPred,NewPred,In,Out), | |
445 | conjunct_predicates([P,OldPred],NewPred) | |
446 | ) | |
447 | ; otherwise -> % Not applicable, nothing to do | |
448 | In=Out). | |
449 | aux_get_section(Machine,Sec,Content) :- % just to rearrange the parameters | |
450 | get_section(Sec,Machine,Content). | |
451 | ||
452 | is_record_detection_expr(Expr) :- | |
453 | get_texpr_info(Expr,Info),memberchk(record_detection(_),Info). | |
454 | ||
455 | replace_type(global(Type),Type,NewType,Result) :- !, NewType=Result. | |
456 | replace_type(couple(A,B),T1,T2,couple(RA,RB)) :- | |
457 | !, replace_type(A,T1,T2,RA), replace_type(B,T1,T2,RB). | |
458 | replace_type(set(A),T1,T2,set(RA)) :- | |
459 | !, replace_type(A,T1,T2,RA). | |
460 | replace_type(seq(A),T1,T2,seq(RA)) :- | |
461 | !, replace_type(A,T1,T2,RA). | |
462 | replace_type(T,_,_,T). % just skip types like integer, string, etc. | |
463 | ||
464 | contains_type(Type,couple(A,_)) :- contains_type(Type,A). | |
465 | contains_type(Type,couple(_,B)) :- contains_type(Type,B). | |
466 | contains_type(Type,set(A)) :- contains_type(Type,A). | |
467 | contains_type(Type,seq(A)) :- contains_type(Type,A). | |
468 | contains_type(Type,Type). | |
469 | ||
470 | add_type_declarations(TExpr,ToReplace,Set,Ids,Result) :- | |
471 | create_type_predicate(ToReplace,Set,Ids,P), | |
472 | ( is_truth(P) -> Result = TExpr % Nothing to do | |
473 | ; otherwise -> | |
474 | add_declaration_for_identifier(TExpr,P,Result)). | |
475 | ||
476 | create_type_predicate(ToReplace,Set,Ids,P) :- | |
477 | include(expr_contains_type(ToReplace),Ids,RelevantIds), | |
478 | maplist(create_type_membership(ToReplace,Set),RelevantIds,Preds), | |
479 | conjunct_predicates(Preds,P1), | |
480 | clean_up(P1,[],P). | |
481 | ||
482 | expr_contains_type(ToReplace,TExpr) :- | |
483 | get_texpr_type(TExpr,Type), | |
484 | contains_type(ToReplace,Type). | |
485 | ||
486 | create_type_membership(ToReplace,Set,TId,Membership) :- | |
487 | get_texpr_type(TId,Type), | |
488 | create_set_for_type(Type,ToReplace,Set,GenSet), | |
489 | create_texpr(member(TId,GenSet),pred,[],Membership). | |
490 | ||
491 | create_set_for_type(T,ToReplace,Set,R) :- | |
492 | T=ToReplace,!,R=Set. | |
493 | create_set_for_type(couple(A,B),ToReplace,Set,R) :- !, | |
494 | create_set_for_type(A,ToReplace,Set,SA), | |
495 | create_set_for_type(B,ToReplace,Set,SB), | |
496 | ( is_typeset(SA),is_typeset(SB) -> create_typeset(couple(A,B),R) | |
497 | ; create_texpr(cartesian_product(SA,SB),set(couple(A,B)),[],R)). | |
498 | create_set_for_type(set(A),ToReplace,Set,R) :- !, | |
499 | create_set_for_type(A,ToReplace,Set,SA), | |
500 | ( is_typeset(SA) -> create_typeset(set(A),R) | |
501 | ; create_texpr(pow_subset(SA),set(set(A)),[],R)). | |
502 | create_set_for_type(seq(A),ToReplace,Set,R) :- !, | |
503 | % for our purpose, we can ignore other constraints on sequences | |
504 | create_set_for_type(set(couple(integer,A)),ToReplace,Set,R). | |
505 | create_set_for_type(Type,_ToReplace,_Set,R) :- create_typeset(Type,R). | |
506 | is_typeset(Expr) :- get_texpr_expr(Expr,typeset). | |
507 | ||
508 | create_typeset(Type,Set) :- | |
509 | create_texpr(typeset,set(Type),[],Set). | |
510 | ||
511 | % extract_constants_that_are_types(+Machine,-RTT): | |
512 | % gives a list of identifiers of those constants that are defined to be the whole type. | |
513 | % This works only for constants that are defined with an equality, e.g. | |
514 | % c = BOOL**BOOL | |
515 | extract_constants_that_are_types(Machine,RTT) :- | |
516 | get_all_equalities_from_machine(Machine,Equalities), | |
517 | extract_type_references(Equalities,[],RTT). | |
518 | % get_all_equalities_from_properties(+Machine,-Equalities): | |
519 | % extract all equalities from the properties. | |
520 | % Equalities is a list of terms equal(Id,Expr) where Id denotes a | |
521 | % constant and Expr the expr on the other side of the equation. | |
522 | get_all_equalities_from_machine(Machine,Equalities) :- | |
523 | get_all_constants_from_machine(Machine,Constants), | |
524 | get_section(properties,Machine,Properties), | |
525 | conjunction_to_list(Properties,PList), | |
526 | convlist(is_equality_left(Constants), PList,LEqualities), | |
527 | convlist(is_equality_right(Constants),PList,REqualities), | |
528 | append(LEqualities,REqualities,Equalities). | |
529 | get_all_constants_from_machine(Machine,Constants) :- | |
530 | get_section(abstract_constants,Machine,AC), | |
531 | get_section(concrete_constants,Machine,CC), | |
532 | append(AC,CC,Constants). | |
533 | % extract_type_references(+Equalities,+RTT,-Result): | |
534 | % Equalities: A list of term of the form equal(Id,Expr), see get_all_equalities_from_properties/2 | |
535 | % RTT: An ordered list of already known constants that refer to types | |
536 | % Result: A ordered list of constants (their id, no types) that refer to types | |
537 | % The predicate works recursively because a definition like a = B**INTEGER can denote a | |
538 | % type if B also denotes a type which must be detected first. | |
539 | extract_type_references(Equalities,RTT,Result) :- | |
540 | convlist(equality_is_typedef(RTT),Equalities,ReferencesToTypes), | |
541 | list_to_ord_set(ReferencesToTypes,Sorted), | |
542 | ord_subtract(Sorted,RTT,Unique), | |
543 | ( Unique = [] -> Result=RTT % no new definitions found | |
544 | ; otherwise -> % new definitions found, continue recursively | |
545 | ord_union(Unique,RTT,NewRTT), | |
546 | extract_type_references(Equalities,NewRTT,Result) | |
547 | ). | |
548 | % Pred is of form Id=Expr where Id is a constant | |
549 | is_equality_left(Constants,Pred,equal(Id,Expr)) :- | |
550 | get_texpr_expr(Pred,equal(TId,Expr)), is_equality_aux(TId,Constants,Id). | |
551 | % Pred is of form Expr=Id where Id is a constant | |
552 | is_equality_right(Constants,Pred,equal(Id,Expr)) :- | |
553 | get_texpr_expr(Pred,equal(Expr,TId)), is_equality_aux(TId,Constants,Id). | |
554 | is_equality_aux(TId,Constants,Id) :- | |
555 | get_texpr_id(TId,Id),get_texpr_id(Constant,Id),memberchk(Constant,Constants). | |
556 | equality_is_typedef(RTT,equal(Id,Expr),Id) :- | |
557 | is_just_type(Expr,RTT). |