bmachine_eventb

abstraction_var_occures(TExpr,AnimationChain) :-
    get_texpr_expr(TExpr,identifier(_)),!,
    get_texpr_section(TExpr,Section),
    \+ member(Section,AnimationChain).

abstraction_var_occures(TExpr,AnimationChain) :-
    syntaxtraversion(TExpr,_,_,_,Subs,_),
    abstraction_var_occures_l(Subs,AnimationChain).

abstraction_var_occures_l([Sub|_],AnimationChain) :-
    abstraction_var_occures(Sub,AnimationChain),!.

abstraction_var_occures_l([_|Srest],AnimationChain) :-
    abstraction_var_occures_l(Srest,AnimationChain).

adapt_becomes_such(becomes_such(Pos,Ids,Pred),evb2_becomes_such(Pos,Ids,Pred)) :- !.

adapt_becomes_such(Subst,Subst).

add_all([],L,L).

add_all([H|T],[H|L1],L2) :- add_all(T,L1,L2).

add_all_to_avl([],Avl,Avl).

add_all_to_avl([H|T],In,Out) :-
    avl_store(H,In,1,Inter),
    add_all_to_avl(T,Inter,Out).

add_context_occurrences([],_,[]).

add_context_occurrences([Constant|Crest],Name,[CC|CCrest]) :-
    add_texpr_infos(Constant,[occurrences([Name])],CC),
    add_context_occurrences(Crest,Name,CCrest).

add_datatype_to_env(datatype(Id,Params,_),In,Out) :-
    length(Params,NumberOfParams),
    functor(FreetypeId,Id,NumberOfParams),
    env_store(Id,set(freetype(FreetypeId)),[],In,Out).

add_env_vars_for_extended2([],_,Env,Env).

add_env_vars_for_extended2([Name|Erest],Contextes,Old,New) :-
    internal_context_sets(Context,Name,Sets),
    internal_context_constants(Context,Name,Constants),
    internal_context_abstract_constants(Context,Name,AbstractConstants),
    member(Context,Contextes),!,
    add_unique_variables(Sets,Old,Env1),
    add_unique_variables(Constants,Env1,Env2),
    add_unique_variables(AbstractConstants,Env2,Env),
    add_env_vars_for_extended2(Erest,Contextes,Env,New).

add_equality_check(Actions,AbstractActions,NewVars,Variables,Unmodifiables) :-
    get_modified_vars_of_actions(Actions,Modified),
    get_modified_vars_of_actions(AbstractActions,AbstractModified),
    unmodifiables(Modified,AbstractModified,NewVars,Variables,Unmodifiables).

add_eventb_pos_aux(Model,LabelName,Context,b(E,T,I),b(E,T,NewInfo)) :-
    nonmember(nodeid(_),I),
    NewInfo = [nodeid(rodin_derived_context_pos(Model,Context,LabelName))|I].

add_missing_assignments([],Event,_,_,Event) :- !.

add_missing_assignments(MissingVars,TEvent,AllModifiedVars,TypedVars,Normalised) :-
    get_texpr_expr(TEvent,Event),
    get_texpr_type(TEvent,Type),
    get_texpr_info(TEvent,Infos),
    selectchk(modifies(_),Infos,RestInfos), % TO DO: also add reads Information
    create_texpr(NewEvent,Type,[modifies(AllModifiedVars)|RestInfos],Normalised),
    Event = rlevent(Name,Sec,St,Prm,Grd,Thm,Actions,VWit,PWit,Unmod,AbsEvents),
    NewEvent = rlevent(Name,Sec,St,Prm,Grd,Thm,NewActions,VWit,PWit,Unmod,AbsEvents),
    append(Actions,NewAssignments,NewActions),
    create_missing_assignments(MissingVars,TypedVars,NewAssignments).

add_modified_vars_to_action(TAction,MAction) :-
    get_lhs_ids(TAction,Vars),
    maplist(prime_id,Vars,Primed),
    add_texpr_infos(TAction,[assigned_after(Primed),modifies(Vars)],MAction).

add_modified_vars_to_actions([],[]).

add_modified_vars_to_actions([TAction|ARest],[MAction|MRest]) :-
    (add_modified_vars_to_action(TAction,MAction) ->true
    ; add_internal_error('Call failed: ',add_modified_vars_to_action(TAction,MAction)),
    MAction = TAction),
    add_modified_vars_to_actions(ARest,MRest).

add_op_parenthesis([],[]).

add_op_parenthesis([Old|ORest],[New|NRest]) :-
    def_get_texpr_id(Old,Id),
    rename_bt(Old,[rename(Id,op(Id))],New),
    add_op_parenthesis(ORest,NRest).

add_primed_variables(Variables,OrigEnv,NewEnv) :-
    prime_variables(Variables,Primed),
    add_unique_variables(Primed,OrigEnv,NewEnv).

add_stripped_ast(Formula,Formula/Stripped) :-
    strip_and_norm_ast(Formula,Stripped).

add_to_known_elements(New,In,Out) :-
    avl_store(New,In,true,Out).

add_type_parameter(TypeParam,Type,In,Out) :-
    extract_id(TypeParam,ParameterId),
    env_store(ParameterId,set(Type),[],In,Out).

add_unique_variables([],Env,Env).

add_unique_variables([Var|Rest],Old,New) :-
    def_get_texpr_id(Var,Name),
    get_texpr_type(Var,Type),
    get_texpr_info(Var,Infos),
    ( env_lookup_type(Name,Old,_) ->
    add_error(bmachine_eventb,'Identifier declared twice',Name),
    fail
    ; true),
    env_store(Name,Type,Infos,Old,Env),
    add_unique_variables(Rest,Env,New).

add_unmodified_assignments(AbstractActions,ConcreteActions,ConcreteVars,NewActions) :-
    get_modified_vars_of_actions(AbstractActions,AbstractModified),
    get_modified_vars_of_actions(ConcreteActions,ConcreteModified),
    remove_all(AbstractModified,ConcreteModified,OnlyAbstractModified),
    findall( Var,
    ( member(Id,OnlyAbstractModified), get_texpr_id(Var,Id), memberchk(Var,ConcreteVars)),
    ToKeep),
    ( ToKeep = [] -> NewActions = ConcreteActions
    ; ToKeep = [_|_] ->
    create_texpr(assign(ToKeep,ToKeep),subst,[],Action1),
    add_modified_vars_to_action(Action1,Action),
    NewActions = [Action|ConcreteActions]).

add_var_model_occurrence(Var,AllVars,MVar) :-
    findall(Section,
    ( find_identifier_in_list(Var,AllVars,M),
    get_texpr_info(M,Infos),
    member(section(Section),Infos)),
    Sections),
    reverse(Sections,FromAbstractToConcrete),
    add_texpr_infos(Var,[occurrences(FromAbstractToConcrete)],MVar).

add_var_model_occurrences([],_,[]).

add_var_model_occurrences([Var|Vrest],AllVars,[MVar|Mrest]) :-
    add_var_model_occurrence(Var,AllVars,MVar),
    add_var_model_occurrences(Vrest,AllVars,Mrest).

aggregation_operator('SIGMA',general_sum).

aggregation_operator('PI',general_product).

all_context_names([],[]).

all_context_names([Context|Crest],[Name|Nrest]) :-
    internal_context(Context,Name),
    all_context_names(Crest,Nrest).

all_same([],_,[]).

all_same([_|R],E,[E|T]) :- all_same(R,E,T).

all_singletons([],[],Ax,Ax,_).

all_singletons([Set|SRest],[Expr|ERest],AxiomsIn,AxiomsOut,Recursive) :-
    get_texpr_expr(Set,set_extension([Expr])),!,
    all_singletons(SRest,ERest,AxiomsIn,AxiomsOut,Recursive).

all_singletons([ID1|SRest],Result,AxiomsIn,AxiomsOut,Recursive) :-
    ID1 = b(identifier(_ID),set(global(_)),_Info),
    Recursive=true,
    % print(trying_to_look_for_recursive_partition(_ID)),nl,
    has_enumeration_axioms(ID1,PartitionElements,AxiomsIn,AxiomsOut1),
    % print(recursive_partition(ID,PartitionElements)),nl,
    append(PartitionElements,ERest,Result),
    all_singletons(SRest,ERest,AxiomsOut1,AxiomsOut,_).

all_unequals_present([],Axioms,Axioms).

all_unequals_present([unequal(A,B)|Rest],InAxioms,OutAxioms) :-
    remove_unequalities(InAxioms,A,B,IntAxioms,0,N), N>0,!, % at least one occurrence
    all_unequals_present(Rest,IntAxioms,OutAxioms).

all_used_contextes(AnimatedModels,Contextes,Sees) :-
    ( AnimatedModels = [] ->
    all_context_names(Contextes,Sees)
    ;
    collect_sees(AnimatedModels,Sees)).

annotate_dropped_parameters([],_,_,[]).

annotate_dropped_parameters([P|PRest],Refines,AbstractEvents,[A|ARest]) :-
    def_get_texpr_id(P,Id),
    add_texpr_infos(P,[droppedby(DropList)],A),
    findall(Event, event_drops_param(Event,Refines,AbstractEvents,Id), DropList),
    annotate_dropped_parameters(PRest,Refines,AbstractEvents,ARest).

append_modified_vars_of_events(Events,Vars) :-
    append_modified_vars_of_events2(Events,Unsorted),
    sort(Unsorted,Vars).

append_modified_vars_of_events2([],[]).

append_modified_vars_of_events2([TEvent|ERest],Vars) :-
    get_modified_vars_of_event(TEvent,Local),
    append(Local,VRest,Vars),
    append_modified_vars_of_events2(ERest,VRest).

append_stripped_predicates(PredsIn,AnimatedSectionNames,RestPreds,Preds) :-
    remove_linking_parts(PredsIn,AnimatedSectionNames,LPreds),
    append(LPreds,RestPreds,Preds).

append_to_section(Section,List,Old,New) :-
    % todo: access to private elements of bmachine_construction
    select_section(Section,OldList,NewList,Old,New),
    append(OldList,List,NewList).

apply_direct_definition(TArgs,Params,DirectDef,PT,Env,_Pos,
    TLetIds,TLetValues,TDef,TRin,TRout) :-
    same_length(TArgs,Params),!,
    maplist(create_typed_id,PT,ParametricTypes,TPT),
    add_identifiers_to_environment(TPT,Env,SubEnv),
    % type check the arguments given in the operator usage
    get_texpr_types(TArgs,ArgTypes),
    typecheck_arguments(Params,SubEnv,ArgTypes,TParams,TRin,TR2),
    % type check the direct definition of the operator. To do this we need the parameters of the operators
    % in the type environment. Their type is determined by the arguments of the operator call.
    add_identifiers_to_environment(TParams,SubEnv,DefEnv),
    btype(apply_direct_definition,DirectDef,DefEnv,_Type,TDef,TR2,TRout),
    append(TParams,TPT,TLetIds),
    maplist(create_typeset,ParametricTypes,TypeValues),
    append(TArgs,TypeValues,TLetValues).

apply_direct_definition(_TArgs,_Arguments,_DirectDef,_PT,_Env,Pos,
    _TParams,_,_TDef,TRin,TRout) :-
    store_typecheck_error('Wrong number of operator arguments',Pos,TRin,TRout).

apply_projections(Projections,Expr,Result) :-
    reverse(Projections,Prjs),
    apply_projections1(Prjs,Expr,Result).

apply_projections1([],Expr,Expr).

apply_projections1([P|Rest],Expr,Result) :-
    get_texpr_type(Inner,couple(A,B)),
    apply_projections2(P,A,B,Result,Inner),
    apply_projections1(Rest,Expr,Inner).

apply_projections2(prj1,A,_B,Result,Inner) :-
    create_texpr(first_of_pair(Inner),A,[],Result).

apply_projections2(prj2,_A,B,Result,Inner) :-
    create_texpr(second_of_pair(Inner),B,[],Result).

binary_external_function(FUN,FUN) :- visible_external_function(FUN,2).

binary_operator_raw_term(Functor,Arg1,Arg2,Term) :-
    binary_operator_to_ast(Functor,ASTFunctor),
    Term =.. [ASTFunctor,none,identifier(none,Arg1),identifier(none,Arg2)].

binary_operator_raw_term(Functor,Arg1,Arg2,Term) :-
    binary_external_function(Functor,ASTFunctor),
    Term = external_function_call_auto(none, ASTFunctor, [identifier(none,Arg1),identifier(none,Arg2)]).

binary_operator_to_ast('^',concat).

binary_operator_to_ast(concat,concat).

binary_operator_to_ast(div,floored_div).

binary_operator_to_ast(restrict_front,restrict_front).

binary_operator_to_ast(restrict_tail,restrict_tail).

binary_operator_to_ast(arity,arity).

binary_operator_to_ast(bin,bin).

binary_operator_to_ast(const,const).

binary_operator_to_ast(father,father).

binary_operator_to_ast(rank,rank).

binary_operator_to_ast(subtree,subtree).

binary_operator_to_ast(rdiv,div_real).

binary_operator_to_ast(plus,add_real).

binary_operator_to_ast(power_of,power_of_real).

binary_operator_to_ast(minus,minus_real).

binary_operator_to_ast(mul,multiplication_real).

check_context(RawContext,InitEnv,PrevContextes,Context) :-
    extract_ctx_sections(RawContext,Name,Extends,
    RawSets,RawConstants,RawAbstractConstants,RawAxioms,RawTheorems),
    Context = context(Name,Extends,Sets,Constants,AbstractConstants,Axioms,Theorems),
   
    % create deferred sets
    create_sets(RawSets,Name,Sets),
    % and constants
    IdInfos = [loc(Name,constants),section(Name)],
    create_identifiers(RawConstants,IdInfos,Constants),
    create_identifiers(RawAbstractConstants,IdInfos,AbstractConstants),
   
    % with the constants and set of seen contextes,
    create_ctx_env(Extends,PrevContextes,InitEnv,PrevEnv),
    % and the sets and constants
    add_unique_variables(Sets,PrevEnv,SetEnv),
    add_unique_variables(Constants,SetEnv,EnvT),
    add_unique_variables(AbstractConstants,EnvT,Env),
   
    % now typecheck the axioms and theorems,
    % this should determine the constant's types
    typecheck_together([RawAxioms,RawTheorems],Env,[Axioms,Theorems],axioms).

check_contextes(InitEnv,RawContextes,Contextes) :-
    debug_println(9,'Checking Contextes'),
    % make sure that a extended context is treated before
    % the extending context
    topological_sort(RawContextes,SortedContextes),
    check_contextes2(SortedContextes,InitEnv,[],Contextes).

check_contextes2([],_,_,[]).

check_contextes2([RawContext|Rrest],InitEnv,PrevContextes,[Context|Crest]) :-
    check_context(RawContext,InitEnv,PrevContextes,Context),
    check_contextes2(Rrest,InitEnv,[Context|PrevContextes],Crest).

check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVariables,Variant,
    event(EvName,ModelName,Status,TParameters,TGuard,TTheorems,MActions,
    TVarWitnesses,TParamWitnesses,Unmodifiables,Refines)) :-
    raw_event(RawEvent,_,EvName,RawStatus,Refines,Params,Guards,Theorems,Actions,Witnesses),
    check_status(RawStatus, Variant, Status, Refines, AbstractEvents, eventlocation(ModelName,EvName)),
    get_abstract_parameters(Refines,AbstractEvents,AbstractParameters),
    create_identifiers(Params,[loc(ModelName,event(EvName))],TParameters),
    split_abstract_vars(AbstractParameters,TParameters,
    _NewParameters,DroppedParameters1),
    annotate_dropped_parameters(DroppedParameters1,Refines,AbstractEvents,DroppedParameters),
    conjunct_guards(Guards,Guard),
    maplist(adapt_becomes_such,Actions,Actions1),
    % add new parameters to the typing environments:
    add_identifiers_to_environment(TParameters,Env,Subenv),
    add_identifiers_to_environment(TParameters,GEnv,SubGenv),
    add_identifiers_to_environment(TParameters,InvEnv,SubTheoremsEnv), % theorems can access dropped abstract variables; just like the invariant
    typecheck(Guard,Subenv,pred,TGuard,event(EvName,guard)),
    typecheck_l(Theorems,SubTheoremsEnv,pred,TTheorems,event(EvName,theorems)),
    typecheck_l(Actions1,Subenv,subst,TActions,event(EvName,actions)),
    check_witnesses(Witnesses,SubGenv,DroppedParameters,DroppedVars,TVarWitnesses,TParamWitnesses),
    % add checks that some variables may not be modified, e.g
    % if skip is refined
    get_abstract_actions(Refines,AbstractEvents,AbstractActions),
    add_modified_vars_to_actions(TActions,MActions1),
    add_unmodified_assignments(AbstractActions,MActions1,ConcreteVars,MActions),
    add_equality_check(MActions,AbstractActions,NewVariables,ConcreteVars,Unmodifiables).

check_event_b_project(RawModels,RawContextes,Extensions,MachineWithPragmas) :-
    retractall(deferred_set_eq_wo_enumeration_axioms(_,_)),
    catch( check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas),
    typecheck_errors(Errors),
    ( add_all_perrors(Errors), NoError=false )), % a cut here does not work !
    !, NoError=true.

check_event_b_project(_,_,_,_) :-
    add_internal_error('Checking Event-B Model failed; Please submit bug report.',check_event_b_project(_,_,_,_)),
    fail.

check_event_b_project1([],RawContextes,Extensions,MachineWithPragmas) :-
    !,
    check_extensions(Extensions,Freetypes,Ops,InitEnv), % Theories
    check_contextes(InitEnv,RawContextes,Contextes),
    convert_event_b(context,Freetypes,Ops,Contextes,[],[],Machine),
    extract_pragmas_from_event_b_extensions(Extensions,Pragmas),
    apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas).

check_event_b_project1(RawModels,RawContextes,Extensions,MachineWithPragmas) :-
    compute_animation_chain(RawModels,AnimationChain),
    check_event_b_project2(RawModels,RawContextes,Extensions,
    AnimationChain,Machine),
    extract_pragmas_from_event_b_extensions(Extensions,Pragmas),
    apply_pragmas_to_event_b_machine(Pragmas,Machine,MachineWithPragmas).

check_event_b_project2(RawModels,RawContextes,Extensions,AnimationChain,Machine) :-
    RawModels=[event_b_model(_,Main,_)|_],
    check_extensions(Extensions,Freetypes,Ops,InitEnv), % related to Theory plugin
    % generate type-checked contextes
    check_contextes(InitEnv,RawContextes,Contextes),
    % generate type-checked models
    check_models(InitEnv,RawModels,Contextes,Models),
    % merge all the constants/vars/predicates and events into one machine
    convert_event_b(Main,Freetypes,Ops,Contextes,Models,AnimationChain,Machine).

check_events([],_ModelName,_Env,_GEnv,_InvEnv,_Dropped,_ConcreteVars,_AbstractEvents,_NewVars,_Variant,[]).

check_events([RawEvent|RawRest],ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,[Event|Erest]) :-
    (check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event)
    -> true
    ; add_failed_call_error(check_event(RawEvent,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Event))),
    check_events(RawRest,ModelName,Env,GEnv,InvEnv,DroppedVars,ConcreteVars,AbstractEvents,NewVars,Variant,Erest).

check_extensions(Infos,Freetypes,Ops,TheoryEnv) :-
    findall( T, (member(T,Infos),is_eventb_additional_info(T)), Theories),
    default_theory_ops(InitialEnv),
    foldl(check_theory,Theories,FreetypesL,OpsL,InitialEnv,TheoryEnv),
    append(FreetypesL,Freetypes),append(OpsL,Ops).

check_for_errors(Errors) :-
    % TO DO: extract and add warnings in list
    Errors = [_|_],!,throw(typecheck_errors(Errors)).

check_for_errors([]).

check_model(RawModel,InitEnv,PrevModels,Contextes,Model) :-
    extract_model_sections(RawModel,Name,Refines,Sees,
    RawVariables,RawInvariant,
    RawTheorems,RawVariant,RawEvents),
    Model = model(Name,Refines,Sees,ConcreteVariables,NewVariables,Invariant,Theorems,Events),
    get_refined_model(Refines,PrevModels,RefinedModel),
   
    get_all_abstract_variables(Refines,PrevModels,AbstractionVariables),
    length(PrevModels,Level),
    IdInfos = [loc(Name,variables),section(Name),level(Level)],
    create_identifiers(RawVariables,IdInfos,ConcreteVariables),
    split_abstract_vars(AbstractionVariables,ConcreteVariables,
    NewVariables,DroppedAbstractVars),
   
    create_ctx_env(Sees,Contextes,InitEnv,CtxEnv),
    add_unique_variables(ConcreteVariables,CtxEnv,ModelEnv),
    add_unique_variables(DroppedAbstractVars,ModelEnv,InvEnv),
    % add primed versions of the concrete variables to
    % permit before-after predicates in the witnesses
    add_primed_variables(ConcreteVariables,InvEnv,BeforeAfterEnv),
   
    typecheck_together([RawInvariant,RawTheorems],InvEnv,[Invariant,Theorems],invariant),
   
    typecheck_variant(RawVariant,InvEnv,Variant),
   
    get_abstract_events(RefinedModel,AbstractEvents),
   
    check_events(RawEvents,Name,ModelEnv,BeforeAfterEnv,InvEnv,
    DroppedAbstractVars,ConcreteVariables,AbstractEvents,
    NewVariables,Variant,Events).

check_models(InitEnv,RawModels,Contextes,Models) :-
    debug_println(9,'CHECKING MODELS'),
    topological_sort(RawModels,SortedModels),
    check_models2(SortedModels,InitEnv,[],Contextes,Models).

check_models2([],_,_,_,[]).

check_models2([RawModel|RMrest],InitEnv,PrevModels,Contextes,[Model|Mrest]) :-
    (check_model(RawModel,InitEnv,PrevModels,Contextes,Model) -> true
    ; add_failed_call_error(check_model(RawModel,InitEnv,PrevModels,Contextes,Model)),
    fail),
    check_models2(RMrest,InitEnv,[Model|PrevModels],Contextes,Mrest).

check_status(RawStatus, Variant, TConv, Refines, AbstractEvents, Location) :-
    remove_pos(RawStatus,Status),
    check_status2(Status, Variant, Refines, AbstractEvents, Location, Conv, Infos),
    create_texpr(Conv, status, Infos, TConv).

check_status2(ordinary, _Variant, _Refines, _AbstractEvents, _Location, ordinary, []).

check_status2(convergent, _Variant, Refines, AbstractEvents, _Location, ordinary, [convergence_proved]) :-
    % if the refined event is also convergent, we can (or must because the
    % variant may be missing in the refinement) omit the check for decreasing the
    % variant. We do this by treating the event as ordinary.
    convergence_ensured_by_abstract_event(Refines, AbstractEvents),!.

check_status2(convergent, Variant, _Refines, _AbstractEvents, Location, convergent(RVariant), [convergence_proved]) :-
    variant_must_be_set(Variant,Location,RVariant).

check_status2(anticipated, Variant, _Refines, _AbstractEvents, _Location, anticipated(RVariant), []) :-
    get_variant(Variant,RVariant).

check_theory(Theory,Freetypes,Ops,Env,OutEnv) :-
    %print(Theory),nl,
    (check_theory2(Theory,Env,Freetypes,Ops) -> true
    ; add_internal_error('Theory check failed:',Theory),fail),
    store_operator_list(Ops,Env,OutEnv).

check_theory2(theory(PT,Datatypes,OP),Env,Freetypes,Ops) :-
    % just to be backward-compatible to a version without axiomatic definitions
    check_theory2(theory(PT,Datatypes,OP,[]),Env,Freetypes,Ops).

check_theory2(theory(PT,Datatypes,OP,AxDefs),Env,Freetypes,Ops) :-
    % just to be backward-compatible to a version without operator mapping
    % definitions
    check_theory2(theory(PT,Datatypes,OP,AxDefs,[]),Env,Freetypes,Ops).

check_theory2(theory(PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,Ops) :-
    check_theory2(theory(unknown,unknown,PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,Ops).

check_theory2(theory(Id,_Imported,PT,Datatypes,OP,AxDefs,Mappings),Env,Freetypes,AllOps) :-
    extract_freetypes(Env,Datatypes,Freetypes,FreetypeOps),
    (Mappings \= [_|_]
    -> generate_default_mappings(AxDefs,Id,ML)
    ; ML=Mappings), % some older .eventb files seem to have none here, e.g., Theory/SumProduct_m1_mch.eventb
    debug_println(9,operator_mappings(ML)),
    foldl(handle_mappings(PT),ML,MappedOpsL,OP/AxDefs,OP1/AxDefs1),
    append(MappedOpsL,MappedOps),
    maplist(store_operator(PT),OP1,DefinedOps),
    maplist(store_axiomatic_operator(Id),AxDefs1,AxOpsL),
    append(AxOpsL,AxOps),
    append([FreetypeOps,MappedOps,DefinedOps,AxOps],AllOps1),
    % The operators are used for call-backs, a module prefix is mandatory
    maplist(prefix_with_module,AllOps1,AllOps).

check_witness(witness(_Pos,RawId,Pred),Env,DroppedParams,DroppedVars,TWitness,WType) :-
    RawId = identifier(_,WitnessId),
    get_witness_identifier(WitnessId,DroppedParams,DroppedVars,TId,Info,WType),
    get_texpr_type(TId,Type),
    env_store(WitnessId,Type,Info,Env,Subenv),
    typecheck(Pred,Subenv,pred,TPred,witness),
    create_texpr(witness(TId,TPred),witness,[],TWitness).

check_witnesses([],_Env,_DroppedParams,_DroppedVars,[],[]).

check_witnesses([Witness|Rest],Env,DroppedParams,DroppedVars,TVarWitnesses,TParamWitnesses) :-
    check_witness(Witness,Env,DroppedParams,DroppedVars,TWitness,WType),
    ( WType = droppedvar ->
    TVarWitnesses = [TWitness|TWVRest],
    TParamWitnesses = TWPRest
    ; WType = droppedparam(_DropList) ->
    TVarWitnesses = TWVRest,
    TParamWitnesses = [TWitness|TWPRest]),
    check_witnesses(Rest,Env,DroppedParams,DroppedVars,TWVRest,TWPRest).

collect_context_infos([],[],[],[],[],[]).

collect_context_infos([context(Name,_Ex,LSets1,LCsts1,LAbsCsts1,LAxms,LThms)|Rest],Sets,Constants,AbstractConstants,Axioms,Theorems) :-
    add_context_occurrences(LSets1,Name,LSets),
    add_context_occurrences(LCsts1,Name,LCsts),
    add_context_occurrences(LAbsCsts1,Name,LAbsCsts),
    append(LSets,RSets,Sets),
    append(LCsts,RCsts,Constants),
    append(LAbsCsts,RAbsCsts,AbstractConstants),
    append(LAxms,RAxms,Axioms),
    append(LThms,RThms,Theorems),
    collect_context_infos(Rest,RSets,RCsts,RAbsCsts,RAxms,RThms).

collect_model_infos([],_,[],[],[]) :- !.

collect_model_infos(Models,AnimatedSectionNames,Vars,Invs,Thms) :-
    collect_model_infos2(Models,AnimatedSectionNames,AllVars,Vars1,Invs,Thms),
    % add to every variable the information in which models
    % it is present
    add_var_model_occurrences(Vars1,AllVars,Vars).

collect_model_infos2([],_,[],[],[],[]).

collect_model_infos2([Model|MRest],AnimatedSectionNames,Vars,NewVars,Invs,Thms) :-
    internal_model_vars(Model,_,LVars), append(LVars,RVars,Vars),
    % use only newly introduced variables of a model, to prevent
    % double declarations
    % in case of a limited animation chain, it is important to introduce
    % all variables for the most abstract model
    (MRest == [] -> LNewVars = LVars ; internal_model_newvars(Model,_,LNewVars)),
    append(LNewVars,RNewVars,NewVars),
    internal_model_invs(Model,_,LInvs1), append_stripped_predicates(LInvs1,AnimatedSectionNames,RInvs,Invs),
    internal_model_thms(Model,_,LThms1), append_stripped_predicates(LThms1,AnimatedSectionNames,RThms,Thms),
    collect_model_infos2(MRest,AnimatedSectionNames,RVars,RNewVars,RInvs,RThms).