bmachine_construction

add_arrows([E],[E]) :- !.

add_arrows([E|Erest],[E,'->'|Arest]) :- add_arrows(Erest,Arest).

add_def_dep(DN,In,Out) :-
    analyse_definition_dependencies(In,DN,Deps),
    In = definition_decl(Name,DefType,Pos,Args,RawExpr),
    Out = definition_decl(Name,DefType,Pos,Args,RawExpr,Deps).

add_def_dependency_information(DefsIn,DefsOut,Ein,Eout) :-
    extract_def_name_set(DefsIn,DefNames,DN),
    maplist(add_def_dep(DN),DefsIn,Defs1),
    check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,Ein,Eout).

add_infos_to_identifier(NewInfos,In,Out) :-
    add_texpr_infos(In,NewInfos,Out).

add_link_constraints(Includes,MType,Parameters,RefMachines,Old,New,Ein,Eout) :-
    AllRefMachines = [ref(local,Old)|RefMachines],
    extract_parameter_types(RefMachines,NonGroundExceptions),
    foldl(add_link_section(MType,Parameters,AllRefMachines,NonGroundExceptions),
    Includes,Links/Ein,[]/Eout), % TO DO: Daniel check if [] is correct here
    %print(conjunct_predicates(Links,Link)),nl,
    conjunct_predicates(Links,Link),
    select_section(constraints,OConstraints,NConstraints,Old,New),
    conjunct_predicates([Link,OConstraints],NConstraints).

add_link_section(MType,Parameters,RefMachines,NonGroundExceptions,
    machine_reference(Pos,Ref,Args),Links/Ein,RLinks/Eout) :-
    visible_env(MType,includes,RefMachines,Env,Ein,E1),
    memberchk(parameters(Ref,TParameters),Parameters),
    ( same_length(TParameters, Args) ->
    get_texpr_types(TParameters,Types),
    btype_ground_dl(Args,Env,NonGroundExceptions,Types,TArgs,E1,Eout),
    maplist(create_plink_equality,TParameters,TArgs,LLinks)
    ;
    E1 = [error('wrong number of machine arguments',Pos)|Eout],
    LLinks = []),
    append(LLinks,RLinks,Links).

add_machine_infos(MainName,Machines,CheckedMachines,Old,New) :-
    get_raw_model_type(MainName,Machines,RawModelType), functor(RawModelType,ModelType,_), % argument is position
    % model type could be machine or system (or model ?)
    append_to_section(meta,[model_type/ModelType,hierarchy/Hierarchy,header_pos/HeaderPosList],Old,NewT),
    get_refinement_hierarchy(MainName,Machines,Hierarchy),
    find_machine_header_positions(Machines,HeaderPosList),
    add_refined_machine(Hierarchy,CheckedMachines,NewT,New).

add_nonpos(TId,identifier(none,Id)) :-
    get_texpr_id(TId,op(Id)).

add_precondition(b(truth,_,_),Old,New) :- !, Old=New.

add_precondition(Pre,b(Old,T,I),b(New,T,I2)) :-
    Old=operation(Id,Res,Params,Subst),
    New=operation(Id,Res,Params,NewSubst),
    extract_preconditions(Subst,OldPres,Inner),
    conjunct_predicates([Pre|OldPres],NewPre),
    create_texpr(precondition(NewPre,Inner),subst,[],NewSubst),
    (select(reads(OldReads),I,I1) % we do not have to update modifies(.), non_det_modifies(.), reads_locals(.),...
    -> I2=[reads(NewReads)|I1],
    get_texpr_ids(Params,Ignore),
    find_identifier_uses(Pre,Ignore,PreUsedIds),
    ord_union(PreUsedIds,OldReads,NewReads)
    ; add_internal_error('No reads info for operation: ',add_precondition(Pre,b(Old,T,I),b(New,T,I2))),
    I2=I).

add_promotes_not_found_error(identifier(Pos,Id),[error(Msg,Pos)|E],E) :-
    ajoin(['Promoted operation ',Id,' not found'],Msg).

add_refined_machine([_Main,Refined|_],Machines,Old,New) :-
    member(machine(Refined,Body),Machines),
    append_to_section(meta,[refined_machine/Body],Old,New).

add_refined_machine(_,_,M,M). % not refining

add_theory_operators(Machine,Ein,Eout) :-
    get_section(operators,Machine,Operators),
    keys_and_values(Operators,Ids,Ops),
    foldl(env_store_operator,Ids,Ops,Ein,Eout).

add_unique_variable(Var1,Old/Err_in,New/Err_out) :-
    optionally_rewrite_id(Var1,Var),
    get_texpr_id(Var,Id),
    get_texpr_type(Var,Type),
    get_texpr_info(Var,InfosOfNew),!,
    ( env_lookup_type(Id,Old,_) ->
    % we have a collision of two identifiers
    handle_collision(Var,Id,Type,Old,InfosOfNew,New,Err_in,Err_out)
    ;
    % no collision, just introduce the new identifier
    env_store(Id,Type,InfosOfNew,Old,New),
    %btypechecker:portray_env(New),nl,
    Err_in=Err_out
).

add_unique_variable(Var,Env/Err,Env/Err) :- print(Var),nl,
    ( Var = b(definition(DEFNAME,_),_,INFO) ->
    add_error(add_unique_variable,'DEFINITION used in place of Identifier: ',DEFNAME,INFO)
    ; Var = b(description(Txt,_),_,INFO) ->
    add_error(add_unique_variable,'Unsupported @desc pragma: ',Txt,INFO)
    ;
    add_error(add_unique_variable,'Expected Identifier, but got: ',Var,Var)
).

add_unknown_identifier_error(TId,[error(Msg,Pos)|E],E) :-
    get_texpr_id(TId,Id),
    ajoin(['Unknown identifier ',Id,'.'],Msg),
    % TO DO: generate fuzzy match and possible completions message
    get_texpr_pos(TId,Pos).

add_use_info_to_identifier(Mode,Name,TExpr,New) :-
    get_texpr_id(TExpr,PId), get_texpr_type(TExpr,Type),
    get_texpr_id(New,PId), get_texpr_type(New,Type),
    split_prefix(PId,_Prefix,Id),
    get_texpr_info(TExpr,Info),
    get_texpr_info(New,[usesee(Name,Id,Mode)|Info]).

add_use_param(identifier(_,Param),identifier(none,Name)) :-
    ( is_upper_case(Param) ->
    ajoin(['Useparam(',Param,')'],Name)
    ;
    ajoin(['useparam(',Param,')'],Name)).

add_warning_with_info(Msg1,Msg2,P,Info) :-
    (contains_info_pos(Info) -> Pos=Info ; Pos=P),
    add_warning(bmachine_construction,Msg1,Msg2,Pos).

all_deps_known(K,dep(_Name,Deps)) :- sort(Deps,DS),sort(K,KS),subseq0(KS,DS),!.

allow_local_or_expr_op_calls :-
    (get_preference(allow_local_operation_calls,true) -> true
    ; get_preference(allow_operation_calls_in_expr,true)).

analyse_definition_dependencies(Expr,DN,Deps) :-
    analyse_definition_dependencies2(Expr,DN,Unsorted,[]),
    sort(Unsorted,Deps).

analyse_definition_dependencies2(VAR,_DN) --> {var(VAR)},!,
    {add_internal_error('Variable DEFINITION expression in',analyse_definition_dependencies)}.

analyse_definition_dependencies2([Expr|Rest],DN) -->
    !, analyse_definition_dependencies2(Expr,DN),
    analyse_definition_dependencies2(Rest,DN).

analyse_definition_dependencies2(definition(_Pos,Name,Args),DN) -->
    !,[Name],analyse_definition_dependencies2(Args,DN).

analyse_definition_dependencies2(identifier(_Pos,Name),DN) -->
    {avl_fetch(Name,DN),!},[Name].

analyse_definition_dependencies2(Expr,DN) -->
    { compound(Expr),functor(Expr,_Functor,Arity),!},
    analyse_definition_dependencies_arg(2,Arity,Expr,DN).

analyse_definition_dependencies2(_Expr,_DN) --> [].

analyse_definition_dependencies_arg(I,Arity,Expr,DN) -->
    { I =< Arity,!,arg(I,Expr,Arg),I2 is I+1 },
    analyse_definition_dependencies2(Arg,DN),
    analyse_definition_dependencies_arg(I2,Arity,Expr,DN).

analyse_definition_dependencies_arg(_I,_Arity,_Expr,_DN) --> [].

append_if_new(Section,Machine,In,Out) :-
    get_section(Section,Machine,Content),
    select_section(Section,Old,New,In,Out),
    get_texpr_ids(Old,ExistingIds),
    exclude(is_in_existing_ids(ExistingIds),Content,NewElements),
    append(Old,NewElements,New).

append_sections(Sections,AbsMachine,Old,New) :-
    expand_shortcuts(Sections,AllSections),
    append_sections2(AllSections,AbsMachine,Old,New).

append_sections2([],_,M,M).

append_sections2([Section|Rest],AbsMachine,Old,New) :-
    get_section(Section,AbsMachine,Content),
    append_to_section3(Section,Content,Old,Inter),
    append_sections2(Rest,AbsMachine,Inter,New).

append_to_section3(Section,Content,Old,Inter) :- section_can_have_duplicates(Section),!,
    append_to_section_and_remove_dups(Section,Content,Old,Inter).

append_to_section3(Section,Content,Old,Inter) :- append_to_section(Section,Content,Old,Inter).

assert_external_procedure_used(FunName) :-
    (external_procedure_used(FunName) -> true ; assertz(external_procedure_used(FunName))).

assert_machine_order(Order) :-
    retractall(machine_global_order(_)),
    debug_print(9,machine_global_order(Order)),
    assertz(machine_global_order(Order)).

better_pos(Pos,_) :- get_position_filenumber(Pos,Filenumber),
    b_get_main_filenumber(Filenumber).

better_pos(_,none).

change_definition_style(DefsIn,DefsOut) :-
    maplist(change_definition_style2,DefsIn,DefsOut).

change_definition_style2(conversion(Pos,InnerDef),definition_decl(Name,DefType,InnerPos,Args,conversion(Pos,RawExpr))) :-
    change_definition_style2(InnerDef,definition_decl(Name,DefType,InnerPos,Args,RawExpr)).

change_definition_style2(Def,definition_decl(Name,DefType,Pos,Args,RawExpr)) :-
    Def =.. [Functor,Pos,Name,Args,RawExpr],
    maplist(check_def_argument(Name,Pos),Args),
    map_def_functor(Functor,DefType).

change_info_of_expression_or_init(init(A,OExpr),Old,New,init(A,NExpr)) :-
    !,change_info_of_expression_or_init(OExpr,Old,New,NExpr).

change_info_of_expression_or_init(includeduse(A,B,C),[],_,includeduse(A,B,C)) :- !.

change_info_of_expression_or_init(freetype(FTypeId,Cases),[],_,freetype(FTypeId,Cases)) :- !.

change_info_of_expression_or_init(OExpr,Old,New,NExpr) :-
    create_texpr(Expr,Type,Old,OExpr),!,
    create_texpr(Expr,Type,New,NExpr).

change_info_of_expression_or_init(OExpr,Old,New,NExpr) :-
    add_internal_error('Illegal typed expression:',change_info_of_expression_or_init(OExpr,Old,New,NExpr)),
    Old=[], NExpr=OExpr.

change_operation(TId,OldOp,NewOp,OldBodies,[NewOp|NewBodies]) :-
    select_operation(TId,OldBodies,OldOp,NewBodies).

check_copied_operation(OpRef,Op,RefMachines,Ein,Eout) :-
    % todo: check the "refinement" parameter
    visible_env(refinement,operation_bodies,RefMachines,Env1,_Errors,[]),
    get_texpr_id(OpRef,OpId),get_texpr_type(OpRef,OpType),
    env_store(OpId,OpType,[],Env1,Env),
    findall(U, find_unknown_identifier(Op,Env,U), Unknown1),
    ( Unknown1=[] -> Ein=Eout
    ;
    sort(Unknown1,Unknown),
    op(OpName) = OpId,
    join_ids(Unknown,IdList),
    (Unknown = [_] -> Plural=[]; Plural=['s']),
    append([['Operation ',OpName,
    ' was copied from abstract machine but the identifier'],
    Plural,
    [' '],
    IdList,
    [' cannot be seen anymore']],Msgs),
    ajoin(Msgs,Msg), Ein = [error(Msg,none)|Eout]
).

check_def_argument(_,_,identifier(_,_)) :- !.

check_def_argument(DefName,DefPos,definition(_,ID,_)) :- !,
    tools:ajoin(['Formal parameter ', ID, ' is a definition call in Definition: '],Msg),
    add_error(bmachine_construction,Msg,DefName,DefPos).

check_def_argument(DefName,DefPos,FP) :- !,
    tools:ajoin(['Formal parameter ', FP, ' is not an identifier in Definition: '],Msg),
    add_error(bmachine_construction,Msg,DefName,DefPos).

check_for_cyclic_def_dependency(Defs,DefNames,DefsOut,Ein,Eout) :-
    % check if we have a cyclic definition:
    create_definitions_avl(Defs,DefsAvl),
    search_for_cyclic_definition(DefNames,DefsAvl,[],Pos,RCycle),!,
    % if we have found a cyclic definition, generate an error message, ...
    reverse(RCycle,Cycle),add_arrows(Cycle,Msg0),
    ajoin(['Found cyclic definitions: '|Msg0],Msg),
    Ein = [error(Msg,Pos)|E1],
    % ... remove the definitions in the cycle (to prevent later infinite loops) ...
    exclude(definition_in_list(Cycle),Defs,Defs1),
    % ... and check the remaining definitions.
    check_for_cyclic_def_dependency(Defs1,DefNames,DefsOut,E1,Eout).

check_for_cyclic_def_dependency(Defs,_DefNames,Defs,E,E).

check_if_all_ids_are_typed([],_RefMachines,_NonGroundExceptions,Ein,Eout) :- !,Ein=Eout.

check_if_all_ids_are_typed(SectionsToType,RefMachines,NonGroundExceptions,Ein,Eout) :-
    memberchk(ref(local,Local),RefMachines),
    get_all_identifiers(SectionsToType,Local,IdentifiersToType),
    check_ground_types_dl(IdentifiersToType, NonGroundExceptions, Ein, Eout).

check_if_equal_identifiers(Local,Abstract,Ein,Eout,LocalMachine) :-
    ( same_length(Local,Abstract) ->
    foldl(check_if_equal_identifiers2,Local,Abstract,Ein,Eout)
    ;
    get_texpr_ids(Abstract,AIDs),
    get_machine_name(LocalMachine,MachName),
    ajoin(['Refinement ',MachName,' must have same Parameters ', AIDs,' as abstract Machine'],Msg),
    Ein = [error(Msg,none)|Eout]
).

check_if_equal_identifiers2(LParam,AParam,Ein,Eout) :-
    get_texpr_id(LParam,LName),
    get_texpr_id(AParam,AName),
    ( LName = AName ->
    % type in refinement is the same as in the abstraction
    get_texpr_type(LParam,Type),
    get_texpr_type(AParam,Type),
    Ein=Eout
    ;
    get_texpr_pos(LParam,Pos),
    ajoin(['Parameter ',LName,' of refinement machine must be ',
    AName,' like in the abstract machine'],Msg),
    Ein = [error(Msg,Pos)|Eout]
).

check_important_annotions_from_machine(RawMachine) :-
    member(definitions(_Pos,Defs),RawMachine),
    member(expression_definition(DPOS,'PROB_REQUIRED_VERSION',[],RawValue),Defs),!,
    (RawValue = string(VPos,Version)
    -> add_message(bmachine_construction,'Checking PROB_REQUIRED_VERSION: ',Version,VPos),
    (check_version(Version,VPos) -> true ; true)
    ; add_warning(bmachine_construction,'PROB_REQUIRED_VERSION must provide a version number string.','',DPOS)
).

check_important_annotions_from_machine(_).

check_include_use([],_,[],Errors,Errors).

check_include_use([U|Rest],Machines,NotIncluded,Ein,Eout) :-
    findall(I,include_usage(Machines,U,I),Inc),
    ( Inc=[] -> NotIncluded = [U|RestNotIncluded], Ein=E1
    ; Inc=[_] -> NotIncluded = RestNotIncluded, Ein=E1
    ;
    NotIncluded = RestNotIncluded,
    use_usage(Machines,Pos,U),
    Ein = [error('used machine is included more than once',Pos)|E1]
    ),
    check_include_use(Rest,Machines,RestNotIncluded,E1,Eout).

check_machine(MainName,MachinesMayContainGenerated,Result,FinalErrors) :-
    clear_warnings,
    debug_println(9,checking_machine(MainName)),
    temporary_set_preference(perform_stricter_static_checks,true,CHNG),
    strip_global_pragmas(MachinesMayContainGenerated,Machines,_WasGenerated), % TODO: is generated still used?
    set_important_prefs_from_machine(MainName,Machines), % set important prefs before type-checking,...
    check_main_machine_file_origin(MainName,Machines),
    % we need to find all SEES/USES declarations, because all references
    % refer to the same machine and that has to be included exactly once.
    find_uses(Machines,Uses,NotIncluded,Errors,E1),
    % if a seen/used machine was not included, we include it by constructing
    % a dummy machine that extends the seen/used machine and the origional
    % main machine
    extend_not_included_uses(NotIncluded,MainName,NewMainName,Machines,IMachines),
    % figure out the right order of machines, so that each machine is
    % type-checked before a dependend machine is loaded
    machine_order(IMachines,Order),
    assert_machine_order(Order),
    % expand (= type-check + includes) machines in the given order
    expand_machines(Order,IMachines,Uses,[],Results1,E1,E2),
    % until now, the initialisation section consists of a list of init(MachineName,Substitution)
    % fold_initialisation merges those to one substitution, respecting the dependencies
    % between the machines
    maplist(fold_initialisation(Order),Results1,Results),
    % find main machine
    memberchk(machine(NewMainName,MainMachine),Results), %nl,print('MAIN:'),nl,print_machine(MainMachine),
    % if the main machine has parameters, we convert them to global sets resp. constants
    convert_parameters_to_global_sets(E2,[],MainMachine,Result1),
    % add some additional informations about the machine
    add_machine_infos(MainName,Machines,Results,Result1,Result),
    ( debug_machine -> print_machine(Result); true),
    %% comment in to pretty print all machines:
    %( member(machine(Name,Mchx),Results), format('~n*** Machine ~w~n',[Name]), print_machine(Mchx),nl,fail ; true),
    % finalize the list of errors, remove duplicates
    sort(Errors,FinalErrors),
    % output warnings
    show_warnings,
    % run static checks on the resulting machine
    static_check_main_machine(Result),
    reset_temporary_preference(perform_stricter_static_checks,CHNG).

check_machine(Main,_,Result,FinalErrors) :-
    add_internal_error('Internal error: Checking the machine failed: ',
    check_machine(Main,_,Result,FinalErrors)),
    fail.

check_main_machine_file_origin(MainName,Machines) :-
    member(M,Machines), get_machine_parameters(M,MainName,_,Position),
    !,
    (Position = none -> true
    ; get_nr_name(Position,Number,Name)
    -> (Number=1 -> true
    ; ajoin(['Main machine name ',MainName,' overriden by machine in file ',Number,' :'],Msg),
    add_error(bmachine_construction,Msg,Name,Position))
    ; add_error(bmachine_construction,'Could not extract file number and name:',Position)
).

check_main_machine_file_origin(MainName,_) :-
    add_error(bmachine_construction,'Could not extract file number and name for main machine:',MainName).

check_version(VersAtom,DPOS) :- atom_codes(VersAtom,Codes),
    split_chars(Codes,".",VCNrs),
    maplist(codes_to_number(DPOS),VCNrs,VNrs),
    compare_against_current_version(VNrs,Result),
    (Result = current_older
    -> full_version_str(Cur),
    ajoin(['This model requires at newer version of ProB than ',Cur,'. Download at least version: '],Msg),
    add_warning(prob_too_old,Msg,VersAtom,DPOS)
    ; true).

clean_up_machine(In,RefMachines,Out) :-
    extract_parameter_types([ref(local,In)|RefMachines],NonGroundExceptions),
    clean_up_machine2(NonGroundExceptions,In,Out).

clean_up_machine2(NonGroundExceptions) -->
    get_section_content(enumerated_sets,Enum),
    get_section_content(enumerated_elements,Elems),
    {register_enumerated_sets(Enum,Elems)}, % register name of enumerated sets, e.g., to detect finite in ast_cleanup
    get_section_content(freetypes,Freetypes),
    {register_freetypes(Freetypes)}, % so that info is available in ast_cleanup for eval_set_extension
    clean_up_section(constraints,NonGroundExceptions),
    clean_up_section(properties,NonGroundExceptions),
    clean_up_section(invariant,NonGroundExceptions),
    clean_up_section(initialisation,NonGroundExceptions),
    clean_up_section(assertions,NonGroundExceptions),
    clean_up_section(operation_bodies,NonGroundExceptions).

clean_up_section(Section,NonGroundExceptions,In,Out) :-
    % debug_stats(cleaning_up(Section)),
    select_section_texprs(Section,Old,New,In,Out),
    clean_up_l_with_optimizations(Old,NonGroundExceptions,New,Section).

clear_warnings :-
    retractall( warnings(_,_) ).

codes_to_number(DPOS,C,A) :-
    catch(number_codes(A,C), error(syntax_error(_N),_),
    (atom_codes(AA,C),
    add_warning(bmachine_construction,'Illegal part of version number (use only numbers separated by dots): ',AA,DPOS),fail)).

collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :-
    % in case of a re-introduced variable from the abstraction,
    % we prefer the concrete variable to the abstract one.
    is_abstraction(DroppedVarInfos,PreferredVarInfos),!.

collision_precedence(_Name,PreferredVarInfos,DroppedVarInfos) :-
    % We are checking an Event-B model with multi-level support
    % and have the same variable in two different refinement levels.
    % Then the one in the more refined module takes precedence
    member(level(L1),PreferredVarInfos),
    member(level(L2),DroppedVarInfos),
    % Level 0 is the abstract level, level 1 the first refinement, etc.
    L1 > L2,!.

collision_precedence(Name,PreferredVarInfos,DroppedVarInfos) :-
    % A local definition takes precedence over a non-local identifier
    % TODO:
    member(loc(local,_DefMachine,definitions),PreferredVarInfos),
    member(loc(_,_VarMachine,Section),DroppedVarInfos),
    Section \= definitions,!,
    (preferences:get_preference(warn_if_definition_hides_variable,true)
    % default is true; we could also check clash_strict_checks
    -> get_id_kind(Section,HiddenIdKind),
    (get_info_pos(PreferredVarInfos,Pos1), Pos1 \= none,
    get_info_pos(DroppedVarInfos,Pos2), Pos2 \= none
    -> translate:translate_span(Pos1,Pos1Str), translate:translate_span(Pos2,Pos2Str),
    ajoin(['Warning: DEFINITION of ', Name, ' at ', Pos1Str,
    ' hides ',HiddenIdKind,' with same name at ', Pos2Str, '.'], Msg)
    ; ajoin(['Warning: DEFINITION of ', Name, ' hides ',HiddenIdKind,' with same name.'], Msg),
    Pos1 = unknown
    ),
    store_warning(Msg,Pos1) % TO DO: add position info
    ; true
).

concat_section2(Machines,Tags,Section,Old,New) :-
    write_section(Section,NewContent,Old,New),
    maplist(get_tagged_lsection_of_machine(Section),Machines,Tags,Contents),
    concat_section_contents(Section,Contents,NewContent).

concat_section_contents(_,[SingleContent],Res) :- !, Res=SingleContent. % no need to remove_dups

concat_section_contents(Section,Contents,NewContent) :-
    append(Contents,ConcContents),
    (section_can_have_duplicates(Section)
    -> remove_dups_keep_order(ConcContents,NewContent)
    ; NewContent=ConcContents).

concat_section_of_simple_lists(Sec,References,In,Out) :-
    maplist(extract_machine_from_ref,References,Machines),
    sort_machines_by_global_order(Machines,OMachines),
    foldl(concat_section_of_simple_lists2(Sec),OMachines,In,Out).

concat_section_of_simple_lists2(Sec,Machine,In,Out) :-
    get_section(Sec,In,Orig),
    get_section(Sec,Machine,List),
    append(Orig,List,NewList),
    write_section(Sec,NewList,In,Out).

concat_sections(Sections1,Machines,Tags,Old,New) :-
    expand_shortcuts(Sections1,Sections),
    foldl(concat_section2(Machines,Tags),Sections,Old,New).

concat_sections_of_refs(Sections1,References,Old,New) :-
    maplist(extract_machine_from_ref,References,Machines),
    maplist(create_tag_by_reference,References,Tags),
    sort_machines_by_global_order(Machines,Tags,OMachines,STags),
    % should we only sort for some sections, e.g., assertions
    % for each machine, create a tag where the expression comes from
    concat_sections(Sections1,OMachines,STags,Old,New).

conjunct_sections2(Machines,Section,Old,New) :-
    % Section is constraints,properties,invariant, ...
    write_section(Section,NewContent,Old,New), % prepare new section
    get_section_of_machines(Machines,Section,Preds),
    %maplist(get_machine_name,Machines,Ns),print(got_sections(Section,Ns)),nl,
    %translate:l_print_bexpr_or_subst(Preds),nl,
    conjunct_predicates(Preds,NewContent).

conjunct_sections_of_refs(Sections1,References,Old,New) :-
    expand_shortcuts(Sections1,Sections),
    maplist(extract_machine_from_ref,References,Machines),
    sort_machines_by_global_order(Machines,OMachines),
    foldl(conjunct_sections2(OMachines),Sections,Old,New).

constructor_name(element(_Pos,Name),Name).

constructor_name(constructor(_Pos,Name,_Domain),Name).

contains_abstract_variables(SortedConcrVars,TExpr) :-
    contains_abstract_variables2(SortedConcrVars,TExpr,Cause),
    (silent_mode(on) -> true
    ; translate_bexpression(Cause,ID),
    ajoin(['Discarding abstract INVARIANT (requires variable "',ID,'"): '],Msg),
    add_message(bmachine_construction,Msg,TExpr,Cause)
).

contains_abstract_variables2(SortedConcrVars,TExpr,Cause) :-
    syntaxtraversion(TExpr,Expr,Type,Infos,Subs,_),
    ( memberchk(loc(_,_Mch,abstract_variables),Infos) % are there other things that pose problems: abstract_constants ?
    -> %print('Abs: '),translate:print_bexpr(TExpr),nl, print(SortedConcrVars),nl,
    Cause=TExpr,
    \+ ord_member_nonvar_chk(b(Expr,Type,_),SortedConcrVars) % otherwise variable is re-introduced with same type
    % in some Event-B models: VARIABLES keyword is used and in refinement VARIABLES are re-listed
    % TO DO: check what happens when variable not immediately re-introduced
    ; member(Sub,Subs),
    contains_abstract_variables2(SortedConcrVars,Sub,Cause)
).

contains_abstraction_refs(TExpr) :-
    syntaxtraversion(TExpr,_,_,Infos,Subs,_),
    ( memberchk(abstraction,Infos) % This info field comes from the last argument of visibility/6
    -> true
    ; member(Sub,Subs),
    contains_abstraction_refs(Sub)).