record_detection

access_locations(TExpr,TDomain,Fields) :-
    access_locations1(TExpr,TDomain,[],Fields).

access_locations1(TExpr,TDomain,Path,Fields) :-
    get_texpr_expr(TExpr,Expr),
    access_locations2(Expr,TExpr,TDomain,Path,Fields).

access_locations2(identifier(_Id),TExpr,TDomain,Path,[fieldloc(TExpr,TDomain,RPath)]) :- reverse(Path,RPath).

access_locations2(direct_product(F1,F2),_TExpr,TCart,Path,Fields) :-
    get_texpr_expr(TCart,cartesian_product(D1,D2)),
    access_locations1(F1,D1,[left |Path],Fields1),
    access_locations1(F2,D2,[right|Path],Fields2),
    append(Fields1,Fields2,Fields).

add_type_constraint_to_section(_ToReplace,simple,_Decl,In,Out) :-
    !,In=Out.

add_type_constraint_to_section(ToReplace,Domain,decl(IdSecs,PredSec),In,Out) :-
    maplist(aux_get_section(In),IdSecs,IdsL),append(IdsL,Ids1),
    % do not add constraints for accessor and update functions for records:
    exclude(is_record_detection_expr,Ids1,Ids),
    ( contains_identifier_with_type(Ids,ToReplace) ->
    create_type_predicate(global(ToReplace),Domain,Ids,P),
    ( is_truth(P) -> In=Out % Trivial, nothing to do
    ; % Add the type constraint to the relevant predicate section
    select_section(PredSec,OldPred,NewPred,In,Out),
    conjunct_predicates([P,OldPred],NewPred)
    )
    ; % Not applicable, nothing to do
    In=Out).

add_type_declarations(TExpr,ToReplace,Set,Ids,Result) :-
    create_type_predicate(ToReplace,Set,Ids,P),
    ( is_truth(P) -> Result = TExpr % Nothing to do
    ; add_declaration_for_identifier(TExpr,P,Result)).

are_mappings(TExpr,Ids) :-
    are_mappings2(TExpr,Ids,[]).

are_mappings2(TExpr) -->
    {get_texpr_expr(TExpr,Expr)},
    are_mappings3(Expr).

are_mappings3(identifier(Id)) --> [Id].

are_mappings3(couple(A,B)) -->
    are_mappings2(A),
    are_mappings2(B).

aux_get_section(Machine,Sec,Content) :- % just to rearrange the parameters
    get_section(Sec,Machine,Content).

check_record_construction_ok(Set,Domain) :-
    classical_b_mode, % classical B
    get_texpr_type(Domain,Type),
    is_infinite_type(Type),
    % now we know that we have detected a record
    % Section 5.2.6 of \cite{Abrial:BBook} (page 281) and Section 7.13 of \atelierb{} handbook says that given sets are finite
    !,
    get_preference(disprover_mode,false), % fail in disprover mode for classical B
    ajoin(['Translating deferred set ',Set,' to possibly infinite set (set USE_RECORD_CONSTRUCTION to FALSE to prevent this) : '],Msg),
    add_message(record_detection,Msg,Domain,Domain).

check_record_construction_ok(_,_).

contains_identifier_with_type(Ids,T1) :-
    get_texpr_type(TId,Type),
    member(TId,Ids),
    contains_type(global(T1),Type).

contains_type(Type,couple(A,_)) :- contains_type(Type,A).

contains_type(Type,couple(_,B)) :- contains_type(Type,B).

contains_type(Type,set(A)) :- contains_type(Type,A).

contains_type(Type,seq(A)) :- contains_type(Type,A).

contains_type(Type,freetype(A)) :- get_freetype_type_parameters(A,_,TypeParas),
    member(TP,TypeParas), contains_type(Type,TP).

contains_type(Type,Type).

create_accessor_function(Domain,Path,RecordTupleType,AccessDefinition) :-
    % fieldAccess = {r,v | v = prj...(r)}
    create_texpr(identifier(r),RecordTupleType,[],RecordVar),
    get_texpr_type(Domain,set(FieldType)),
    create_texpr(identifier(v),FieldType,[],ValueVar),
    create_texpr(equal(ValueVar,Projection),pred,[],Equals),
    create_projection(Path,RecordVar,Projection),
    %translate:print_bexpr(Projection),nl,
    create_symbolic_comprehension_set([RecordVar,ValueVar],Equals,
    [record_detection(accessor)],AccessDefinition).

create_constructor_definition(Constructor,Domain,ConsDef) :-
    create_texpr(equal(Constructor,Identity),pred,[],ConsDef),
    get_texpr_type(Constructor,Type),
    create_texpr(identity(Domain),Type,[],Identity).

create_field_definition(RecordDomain,fieldloc(AccessorId1,Domain,Path),AccessorId,Equal) :-
    add_texpr_infos(AccessorId1,[record_detection(accessor)],AccessorId),
    create_texpr(equal(AccessorId,AccessorDef),pred,[],Equal),
    % the accessor function maps a record to the domain
    get_texpr_type(RecordDomain,set(RecordTupleType)),
    create_accessor_function(Domain,Path,RecordTupleType,AccessorDef).

create_field_var(fieldloc(AccessorId,Domain,_Path),TId) :-
    create_var_for_field(AccessorId,Domain,'f$__',TId).

create_optional_field_access(SetName,Domain,Constructor,UpAc,Properties,RestList) :-
    get_texpr_id(Set,SetName),
    find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Properties,P4),
    !,
    replace_update_definitions(Fields,Set,Constructor,Updates,P4,P5),
    maplist(create_field_definition(Domain),Fields,Accessors,FieldDefs),
    append(FieldDefs,P5,RestList),
    % A list of identifiers that are used at update and accessor functions:
    append(Updates,Accessors,UpAc).

create_optional_field_access(_Set,_Domain,_Constructor,[],Properties,Properties).

create_projection(Path,RecordVar,ProjectionResult) :-
    get_texpr_type(RecordVar,InnerType),
    create_projection_aux(Path,InnerType,RecordVar,ProjectionResult).

create_projection_aux([],_InnerType,SubExpression,SubExpression). % return record as is

create_projection_aux([Loc|Path],couple(A,B),SubExpression,ProjectionResult) :-
    ( Loc==left -> Expr=first_of_pair(SubExpression), InnerType=A
    ; Loc==right -> Expr=second_of_pair(SubExpression),InnerType=B),
    create_texpr(Expr,InnerType,[],NewSubExpression),
    create_projection_aux(Path,InnerType,NewSubExpression,ProjectionResult).

create_record_tuple([],[],_).

create_record_tuple([fieldloc(_,_,Path)|Frest],[FieldVar|Vrest],Tuple) :-
    create_record_tuple2(Path,FieldVar,Tuple),
    create_record_tuple(Frest,Vrest,Tuple).

create_record_tuple2([],Expr,Expr).

create_record_tuple2([Loc|Path],Expr,Tuple) :-
    ( Loc==left -> create_texpr(couple(Sub,_),couple(SubType,_),[],Tuple)
    ; Loc==right -> create_texpr(couple(_,Sub),couple(_,SubType),[],Tuple)),
    get_texpr_type(Sub,SubType),
    create_record_tuple2(Path,Expr,Sub).

create_recordset_definition(SetName,Domain,SetDef) :-
    create_texpr(equal(Set,Domain),pred,[],SetDef),
    get_texpr_type(Domain,Type),
    create_texpr(identifier(SetName),Type,[],Set).

create_set_for_type(T,ToReplace,Set,R) :-
    T=ToReplace,!,R=Set.

create_set_for_type(couple(A,B),ToReplace,Set,R) :- !,
    create_set_for_type(A,ToReplace,Set,SA),
    create_set_for_type(B,ToReplace,Set,SB),
    ( is_typeset(SA),is_typeset(SB) -> create_typeset(couple(A,B),R)
    ; create_texpr(cartesian_product(SA,SB),set(couple(A,B)),[],R)).

create_set_for_type(set(A),ToReplace,Set,R) :- !,
    create_set_for_type(A,ToReplace,Set,SA),
    ( is_typeset(SA) -> create_typeset(set(A),R)
    ; create_texpr(pow_subset(SA),set(set(A)),[],R)).

create_set_for_type(seq(A),ToReplace,Set,R) :- !,
    % for our purpose, we can ignore other constraints on sequences
    create_set_for_type(set(couple(integer,A)),ToReplace,Set,R).

create_set_for_type(Type,_ToReplace,_Set,R) :- create_typeset(Type,R).

create_symbolic_comprehension_set(Ids,Pred,Info,Result) :-
    create_comprehension_set(Ids,Pred,Info,CompSet),
    mark_bexpr_as_symbolic(CompSet,Result).

create_type_membership(ToReplace,Set,TId,Membership) :-
    get_texpr_type(TId,Type),
    create_set_for_type(Type,ToReplace,Set,GenSet),
    create_texpr(member(TId,GenSet),pred,[],Membership).

create_type_predicate(ToReplace,Set,Ids,P) :-
    include(expr_contains_type(ToReplace),Ids,RelevantIds),
    maplist(create_type_membership(ToReplace,Set),RelevantIds,Preds),
    conjunct_predicates(Preds,P1),
    clean_up(P1,[],P).

create_typeset(Type,Set) :-
    create_texpr(typeset,set(Type),[],Set).

create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function) :-
    % {i,o | #n,f1,...,fn. ( i=( (f1,...,fn) |-> n ) ) & o=(f1,...,n,...,fn) }
    get_texpr_type(FieldAccessorId,set(couple(RecType,FieldType))),
    InType = couple(RecType,FieldType),
    create_texpr(identifier(update__in),InType,[],In),
    create_texpr(identifier(update__out),RecType,[],Out),
    create_symbolic_comprehension_set([In,Out],Pred,[record_detection(update)],CompSet),
   
    % #(n,f1,...,fn).(...&...)
    %create_exists([NewValue|FieldVars],ExistsPred,Pred), % moved below; see comment
    create_var_for_field(FieldAccessorId,FieldDomain,'f$n__',NewValue),
    maplist(create_field_var,Fields,FieldVars),
    create_texpr(conjunct(InEqual,OutEqual),pred,[],ExistsPred),
   
    % i = ( (f1,...,fn) |-> n )
    create_texpr(equal(In,InPair),pred,[],InEqual),
    create_texpr(couple(OldFields,NewValue),InType,[],InPair),
    create_record_tuple(Fields,FieldVars,OldFields),
   
    % o = (f1,...,n,...,fn)
    create_texpr(equal(Out,NewFields),pred,[],OutEqual),
    update_record_tuple(Path,NewValue,OldFields,NewFields),
   
    % the creation of the exists has to be deferred until here as used identifiers are computed:
    create_exists([NewValue|FieldVars],ExistsPred,Pred),
    %translate:print_bexpr(CompSet),nl,
   
    % we need to call the clean-up functions because exists(...) needs more
    % information about which identifier are used and that information
    % is added by clean_up/3.
    clean_up(CompSet,[],Function).

create_var_for_field(AccessorId,Domain,Prefix,TId) :-
    get_texpr_id(AccessorId,FId),
    get_texpr_type(Domain,set(Type)),
    atom_concat(Prefix,FId,VId),
    create_texpr(identifier(VId),Type,[],TId).

equality_is_typedef(RTT,equal(Id,Expr),Id) :-
    is_just_type(Expr,RTT).

expr_contains_type(ToReplace,TExpr) :-
    get_texpr_type(TExpr,Type),
    contains_type(ToReplace,Type).

extract_constants_that_are_types(Machine,RTT) :-
    get_all_equalities_from_machine(Machine,Equalities),
    extract_type_references(Equalities,[],RTT).

extract_type_references(Equalities,RTT,Result) :-
    convlist(equality_is_typedef(RTT),Equalities,ReferencesToTypes),
    list_to_ord_set(ReferencesToTypes,Sorted),
    ord_subtract(Sorted,RTT,Unique),
    ( Unique = [] -> Result=RTT % no new definitions found
    ; % new definitions found, continue recursively
    ord_union(Unique,RTT,NewRTT),
    extract_type_references(Equalities,NewRTT,Result)
).

find_and_remove_field_declaration(Set,Domain,Constructor,Fields,Pin,Pout) :-
    % F1 >< ... >< Fn : Set -->> Domain
    bsyntax_pattern(member(FieldProduct,total_surjection(-Set,-Domain)), SurjMemb),
    selectchk(SurjMemb,Pin,P1),
    % the injection is only defined for closed records
    % (F1 >< ...) >< Fn : Set >-> Domain
    bsyntax_pattern(member(-FieldProduct,total_injection(-Set,-Domain)), InjMemb),
    selectchk(InjMemb,P1,P2),
    access_locations(FieldProduct,Domain,Fields),
    % for each field accessor fx, there should be a declaration
    % fx : Record --> Domain, remove them
    remove_field_declarations(Fields,Set,P2,P3),
    % for each field accessor fx, there should be a predicate
    % !(v1,...,...), remove it
    remove_field_quantifiers(Fields,Constructor,P3,Pout).

get_all_constants_from_machine(Machine,Constants) :-
    get_section(abstract_constants,Machine,AC),
    get_section(concrete_constants,Machine,CC),
    append(AC,CC,Constants).

get_all_equalities_from_machine(Machine,Equalities) :-
    get_all_constants_from_machine(Machine,Constants),
    get_section(properties,Machine,Properties),
    conjunction_to_list(Properties,PList),
    convlist(is_equality_left(Constants), PList,LEqualities),
    convlist(is_equality_right(Constants),PList,REqualities),
    append(LEqualities,REqualities,Equalities).

has_deferred_sets(Machine) :-
    get_section(deferred_sets,Machine,DefSets),
    DefSets = [_|_].

is_constructor_axiom(TAxiom,Sets,GType,TConstructor,Cons,TDom) :-
    % The axiom has the form c : Dom >->> Set, where
    % c and Set are identifiers
    get_texpr_expr(TAxiom,member(TConstructor,TBijection)),
    get_texpr_type(TConstructor,set(couple(FromType,ToType))),
    get_texpr_id(TConstructor,_), % just make sure that TConstructor is an identifer
    FromType \= ToType, % otherwise bijection maps to itself
    (get_texpr_expr(TBijection,total_bijection(TDom,TSet)),
    Cons=constructor(TDom,FromType,constructor)
    ; get_texpr_expr(TBijection,total_bijection(TSet,TDom)),
    % we have the bijection the other way; does not really matter for a bijection anyway
    Cons = constructor(TSet,ToType,destructor)),
    get_texpr_type(TSet,set(global(GType))),
    get_texpr_id(TSet,GType),
    % check if the set is a deferred set, not an enumerated set
    get_texpr_id(SetTest,GType),
    memberchk(SetTest,Sets),
    % in Dom, there should be no reference to Set
    no_reference(TDom,GType).

is_equality_aux(TId,Constants,Id) :-
    get_texpr_id(TId,Id),get_texpr_id(Constant,Id),memberchk(Constant,Constants).

is_equality_left(Constants,Pred,equal(Id,Expr)) :-
    get_texpr_expr(Pred,equal(TId,Expr)), is_equality_aux(TId,Constants,Id).

is_equality_right(Constants,Pred,equal(Id,Expr)) :-
    get_texpr_expr(Pred,equal(Expr,TId)), is_equality_aux(TId,Constants,Id).

is_record_detection_expr(Expr) :-
    get_texpr_info(Expr,Info),memberchk(record_detection(_),Info).

is_typeset(Expr) :- get_texpr_expr(Expr,typeset).

make_field_identifier(fieldloc(FieldAcc,_,_),Id) :-
    get_texpr_type(FieldAcc,set(couple(_,FType))),
    create_texpr(identifier(_),FType,_,Id).

make_field_identifiers([],[]).

make_field_identifiers([FieldAcc|FRest],[Id|Irest]) :-
    make_field_identifier(FieldAcc,Id),
    make_field_identifiers(FRest,Irest).

move_deferred_set(Set,OldMachine,NewMachine) :-
    select_section(deferred_sets,Sets,NewSets,OldMachine,Machine1),
    get_texpr_id(TSet,Set),
    selectchk(TSet,Sets,NewSets),
    select_section(concrete_constants,Constants,[TSet|Constants],Machine1,NewMachine).

mreplace(T1,T2,Type,ReplacedType) :- replace_type(Type,T1,T2,ReplacedType).

no_reference(TExpr,Type) :-
    syntaxtraversion(TExpr,Expr,_,_,Subs,_),
    no_reference2(Expr,Type),
    no_reference_l(Subs,Type).

no_reference2(identifier(Type),Type) :- !,fail.

no_reference2(_,_).

no_reference_l([],_).

no_reference_l([Expr|Rest],Type) :-
    no_reference(Expr,Type),
    no_reference_l(Rest,Type).

remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pout) :-
    bsyntax_pattern(member(-AccessorId,total_function(-RecSet,-Domain)),Pattern),
    selectchk(Pattern,Pin,Pout).

remove_field_declarations([],_RecSet,Predicates,Predicates).

remove_field_declarations([fieldloc(AccessorId,Domain,_Path)|Frest],RecSet,Pin,Pout) :-
    remove_field_declaration(AccessorId,Domain,RecSet,Pin,Pinter),
    remove_field_declarations(Frest,RecSet,Pinter,Pout).

remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pout) :-
    make_field_identifiers(Fields,FSkels),
    get_texpr_ids(FSkels,Ids),
    nth0(N,FSkels,Ref),
    bsyntax_pattern(forall(FSkels,_,equal(function(-Field,function(-Constructor,ConstArg)),-Ref)),ForAll),
    select(ForAll,Pin,Pout),
    are_mappings(ConstArg,Ids),!.

remove_field_quantifiers(Fields,Constructor,Pin,Pout) :-
    remove_field_quantifiers2(Fields,0,Constructor,Pin,Pout).

remove_field_quantifiers2(Fields,N,Constructor,Pin,Pout) :-
    ( nth0(N,Fields,fieldloc(Field,_Dom,_Path)) ->
    remove_field_quantifier(Field,N,Fields,Constructor,Pin,Pinter),
    N2 is N+1,
    remove_field_quantifiers2(Fields,N2,Constructor,Pinter,Pout)
    ;
    Pin=Pout).

replace_constant(NewConstant,In,Out) :-
    % try the replacement in abstract and concrete constants:
    ( replace_id_in_section(NewConstant,abstract_constants,In,Out) -> true
    ; replace_id_in_section(NewConstant,concrete_constants,In,Out) -> true
    ; add_error(record_detection,'Could not replace constant: ',NewConstant,NewConstant),
    fail
).

replace_freetype_paras(A,T1,T2,RA) :-
    get_freetype_type_parameters(A,Func,TypeParas),
    maplist(mreplace(T1,T2),TypeParas,NewTypeParas),
    get_freetype_type_parameters(RA,Func,NewTypeParas).

replace_hidden_type_paras(freetype_constructor(A,Case,Expr),T1,T2,freetype_constructor(RA,Case,Expr)) :- !,
    replace_freetype_paras(A,T1,T2,RA).

replace_hidden_type_paras(freetype_destructor(A,Case,Expr),T1,T2,freetype_destructor(RA,Case,Expr)) :- !,
    replace_freetype_paras(A,T1,T2,RA).

replace_hidden_type_paras(E,_,_,E).

replace_id_in_section(NewId,Section,In,Out) :-
    get_texpr_id(NewId,Id), get_texpr_id(OldId,Id),
    select_section(Section,OldIds,NewIds,In,Out),
    selectchk(OldId,OldIds,NewId,NewIds).

replace_sets_by_records(Machine,ResultMachine) :-
    % replace until a fixpoint is reached
    replace_sets_by_records2(Machine,RMachine),!,
    replace_sets_by_records(RMachine,ResultMachine).

replace_sets_by_records(Machine,Machine).

replace_sets_by_records2(Machine,ResultMachine) :-
    get_preference(use_record_construction,true),
    has_deferred_sets(Machine),
    get_section(deferred_sets,Machine,DeferredSets),
    select_section(properties,Properties,NewProperties,Machine,ConsMachine),
    select_constructor_axiom(Properties,DeferredSets,Set,Constructor,Cons,Domain,RestList1),
    (debug:debug_mode(on) -> format('Record detected for deferred set ~w~n',[Set]) ; true),
    check_record_construction_ok(Set,Domain),
    replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine).

replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor1,Cons,Domain,RestList1,ResultMachine) :-
    Cons = constructor(ConstructorDomain,RecDomainType,_),
    add_texpr_infos(Constructor1,[record_detection(constructor)],Constructor),
    create_constructor_definition(Constructor,ConstructorDomain,ConsDef),
    (debug:debug_mode(on) -> format(' Constructor for ~w: ',[Set]),print_bexpr(ConsDef),nl ; true),
    create_recordset_definition(Set,Domain,SetDef),
    (debug:debug_mode(on) -> format(' New definition for ~w: ',[Set]),print_bexpr(SetDef),nl ; true),
    create_optional_field_access(Set,Domain,Constructor,RecordFunIds,RestList1,RestList),
    conjunct_predicates([ConsDef,SetDef|RestList],NewProperties),
    move_deferred_set(Set,ConsMachine,SetMachine),
    % replace the constants (constructor,accessors,update functions) by versions that
    % have an info field that indicate their function (needed later to exclude them when
    % adding additional constraints):
    foldl(replace_constant,[Constructor|RecordFunIds],SetMachine,M2),
    %% print(replacing(Set,RecDomainType)),nl,
    replace_type_in_machine(Set,RecDomainType,Domain,M2,ResultMachine),
    !,
    register_replaced_global_set(Set,Domain).

replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine) :-
    add_internal_error('Replacing record failed ',replace_sets_by_records3(NewProperties,ConsMachine,Set,Constructor,Cons,Domain,RestList1,ResultMachine)),fail.

replace_type(global(Type),Type,NewType,Result) :- !, NewType=Result.

replace_type(couple(A,B),T1,T2,couple(RA,RB)) :-
    !, replace_type(A,T1,T2,RA), replace_type(B,T1,T2,RB).

replace_type(set(A),T1,T2,set(RA)) :-
    !, replace_type(A,T1,T2,RA).

replace_type(seq(A),T1,T2,seq(RA)) :-
    !, replace_type(A,T1,T2,RA).

replace_type(freetype(A),T1,T2,freetype(RA)) :-
    !, replace_freetype_paras(A,T1,T2,RA).

replace_type(T,_,_,T). % just skip types like integer, string, etc.

replace_type_in_expr(TExpr,T1,T2,Domain,New) :-
    % if identifiers (e.g. i) are declared in an expression (like in forall), we may have
    % to add an predicate (e.g. i:1..4)
    ( Domain=simple -> % the domain is a whole type, no additional constraint needed
    TExpr2 = TExpr
    ; has_declared_identifier(TExpr,Ids),contains_identifier_with_type(Ids,T1) ->
    % identifiers are introduced and one of them contains the record type
    add_type_declarations(TExpr,global(T1),Domain,Ids,TExpr2)
    ; % no identifiers introduced that use the record type
    TExpr = TExpr2
    ),
    create_texpr(Expr,EType,Info,TExpr2), % de-assemble old expression
    replace_type(EType,T1,T2,NType), % replace type global(T1) by T2 in Type
    create_texpr(NExpr2,NType,Info,New), % assemble new expression with new type
    syntaxtransformation(Expr,Subs,_Names,NSubs,NExpr1), % continue with sub-expressions
    replace_type_in_exprs(Subs,T1,T2,Domain,NSubs),
    replace_hidden_type_paras(NExpr1,T1,T2,NExpr2).

replace_type_in_exprs([],_T1,_T2,_Domain,[]).

replace_type_in_exprs([Sub|Irest],T1,T2,Domain,[NSub|Orest]) :-
    replace_type_in_expr(Sub,T1,T2,Domain,NSub),
    replace_type_in_exprs(Irest,T1,T2,Domain,Orest).

replace_type_in_machine(T1,T2,Domain,OldMachine,NewMachine) :-
    extract_constants_that_are_types(OldMachine,RTT),
    (is_just_type(Domain,RTT) -> Domain2 = simple ; Domain2 = Domain),
    % add predicates to constrain variables or constants, if needed
    foldl(add_type_constraint_to_section(T1,Domain2),
    [decl([abstract_constants,concrete_constants],properties),
    decl([abstract_variables,concrete_variables],invariant)],
    OldMachine,Machine1),
    % replace the type in the expressions of the machine (identifier declarations
    % can be treated as expressions, too)
    foldl(replace_type_in_machine2(T1,T2,Domain2),
    [abstract_constants,concrete_constants,
    abstract_variables,concrete_variables,
    promoted, unpromoted,
    constraints, properties, invariant, assertions,
    initialisation, operation_bodies],
    Machine1,NewMachine).

replace_type_in_machine2(T1,T2,Domain,Sec,In,Out) :-
    select_section_texprs(Sec,Old,New,In,Out),
    replace_type_in_exprs(Old,T1,T2,Domain,New).

replace_update_definition(FieldAccessorId,FieldDomain,Path,Fields,
    RecSet,Constructor,Update,Pin,[Equal|Pout]) :-
    % Updatex : Record ** Domain --> Record
    bsyntax_pattern(member(Update1,total_function(cartesian_product(-RecSet,-FieldDomain),-RecSet)),Memb),
    select(Memb,Pin,P1),
    % !(Rec,New).(_ => Updatex(Rec,New) = Constructor(..))
    % TODO: Implication and constructor arguments are missing
    bsyntax_pattern(forall([Rec,New],_,equal(function(-Update1,couple(-Rec,-New)),
    function(-Constructor,_))), ForAll),
    select(ForAll,P1,Pout),
    !,
    add_texpr_infos(Update1,[record_detection(update)],Update),
    % Updatex = {i,o | #(i,r,f1,...,fn).(i=r|->n & ) }
    create_texpr(equal(Update,Function),pred,[],Equal),
    create_update_function(FieldAccessorId,FieldDomain,Path,Fields,Function).

replace_update_definitions(Fields,RecSet,Constructor,Updates,Pin,Pout) :-
    replace_update_definitions2(Fields,Fields,RecSet,Constructor,Updates,Pin,Pout).

replace_update_definitions2([],_Fields,_RecSet,_Constructor,[],Predicates,Predicates).

replace_update_definitions2([fieldloc(AccessorId,FDomain,Path)|Frest],Fields,RecSet,
    Constructor,[UpdateId|URest],Pin,Pout) :-
    replace_update_definition(AccessorId,FDomain,Path,Fields,RecSet,Constructor,UpdateId,Pin,Pinter),
    replace_update_definitions2(Frest,Fields,RecSet,Constructor,URest,Pinter,Pout).

select_constructor_axiom(Properties,Sets,Set,Constructor,Cons,Domain,RestList) :-
    conjunction_to_list(Properties,PList),
    select(Prop,PList,RestList),
    is_constructor_axiom(Prop,Sets,Set,Constructor,Cons,Domain).

update_record_tuple([],NewValue,_OldFields,NewValue).

update_record_tuple([Loc|Path],NewValue,OldFields,NewFields) :-
    get_texpr_expr(OldFields,couple(A,B)),
    get_texpr_type(OldFields,Type),
    create_texpr(couple(X,Y),Type,[],NewFields),
    ( Loc==left -> X=NewSub,A=OldSub,Y=B
    ; Loc==right -> Y=NewSub,B=OldSub,X=A),
    update_record_tuple(Path,NewValue,OldSub,NewSub).