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