b_machine_identifier_normalization

adapt_machinevar_name_info(Name, Info, NewInfo) :-
    select(synthesis(machinevar,_), Info, TempInfo),
    NewInfo = [synthesis(machinevar,Name)|TempInfo],
    !.

adapt_machinevar_name_info(_, Info, Info).

adapt_synthesis_ast_info(Env, Info, NInfo) :-
    Env = [_,NormalizedSets,NormalizedIds,_,_],
    member(synthesis(machinevar,Name), Info),
    ( member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedSets)
    ; member((b(identifier(Name),_,_),b(identifier(NName),_,_)), NormalizedIds)
    ),
    !,
    adapt_machinevar_name_info(NName, Info, NInfo).

adapt_synthesis_ast_info(Env, Info, Info) :-
    % info already normalized
    Env = [_,NormalizedSets,NormalizedIds,_,_],
    member(synthesis(machinevar,NName), Info),
    ( member((_,b(identifier(NName),_,_)), NormalizedSets)
    ; member((_,b(identifier(NName),_,_)), NormalizedIds)
    ),
    !.

adapt_synthesis_ast_info(_, Info, Info).

b_component(precondition).

b_component(select).

b_component(select_when).

b_component(parameter).

b_component(function).

b_component(partial_function).

b_component(total_function).

b_component(partial_injection).

b_component(total_injection).

b_component(partial_surjection).

b_component(total_surjection).

b_component(total_bijection).

b_component(partial_bijection).

b_component(total_relation).

b_component(surjection_relation).

b_component(total_surjection_relation).

b_component(exists).

b_component(comprehension_set).

b_component(forall).

b_component(constant).

b_component(first_of_pair).

b_component(second_of_pair).

b_component(event_b_identity).

b_component(identity).

b_component(relations).

b_component(domain).

b_component(image).

b_component(range).

b_component(domain_restriction).

b_component(domain_subtraction).

b_component(range_restriction).

b_component(range_subtraction).

b_component(reflexive_closure).

b_component(closure).

b_component(conjunct).

b_component(disjunct).

b_component(implication).

b_component(equivalence).

b_component(negation).

b_component(equal).

b_component(not_equal).

b_component(convert_bool).

b_component(if_then_else).

b_component(if_elsif).

b_component(member).

b_component(not_member).

b_component(union).

b_component(intersection).

b_component(set_subtraction).

b_component(cartesian_product).

b_component(direct_product).

b_component(card).

b_component(subset).

b_component(not_subset).

b_component(subset_strict).

b_component(not_subset_strict).

b_component(pow_subset).

b_component(pow1_subset).

b_component(fin_subset).

b_component(fin1_subset).

b_component(finite).

b_component(general_union).

b_component(general_intersection).

b_component(composition).

b_component(integer_set_natural).

b_component(integer_set_natural1).

b_component(implementable_natural).

b_component(implementable_natural1).

b_component(integer_set).

b_component(integer_set_min_max).

b_component(min).

b_component(max).

b_component(add).

b_component(minus).

b_component(multiplication).

b_component(div).

b_component(modulo).

b_component(greater).

b_component(less).

b_component(greater_equal).

b_component(less_equal).

b_component(interval).

b_component(power_of).

b_component(unary_minus).

b_component(seq).

b_component(seq1).

b_component(iseq).

b_component(iseq1).

b_component(perm).

b_component(concat).

b_component(size).

b_component(rev).

b_component(reverse).

b_component(first).

b_component(last).

b_component(tail).

b_component(front).

b_component(insert_front).

b_component(insert_tail).

b_component(restrict_front).

b_component(restrict_tail).

b_component(overwrite).

b_component(general_concat).

b_component(skip).

b_component(assign).

b_component(parallel).

b_component(parallel_product).

b_component(sequence).

b_component(assertion).

enumerate_deferred_sets([], Acc, Acc).

enumerate_deferred_sets([Ast|T], Acc, EIDs) :-
    get_enumerated_name('s', UniqueId),
    Ast = b(_,_,Info),
    adapt_machinevar_name_info(UniqueId, Info, NewInfo),
    NId = b(identifier(UniqueId),set(global(UniqueId)),NewInfo),
    enumerate_deferred_sets(T, [(Ast,NId)|Acc], EIDs).

enumerate_enum_elements(NormalizedSets, Elements, EElements) :-
    group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements),
    % enum elements from 1 to n (reminder: fd(1,Name))
    maplist(enumerate_enum_elements_aux(NormalizedSets, 1, []), GroupedElements, TempEElements),
    append(TempEElements, EElements).

enumerate_enum_elements_aux(_, _, Acc, _-[], Acc).

enumerate_enum_elements_aux(NormalizedSets, C, Acc, NormalizedIdName-[Element|T], NormalizedIds) :-
    % enum elements are normalized as follows: NormSetName+'e'+Id
    atom_concat(NormalizedIdName, e, TempName),
    Element = b(identifier(_),Type,Info),
    number_codes(C, CC),
    atom_codes(AC, CC),
    atom_concat(TempName, AC, NormalizedName),
    C1 is C+1,
    normalize_id_type(NormalizedSets, Type, NType),
    NElement = b(identifier(NormalizedName),NType,Info),
    enumerate_enum_elements_aux(NormalizedSets, C1, [(Element,NElement)|Acc], NormalizedIdName-T, NormalizedIds).

enumerate_ids(NormalizedSets, Prefix, IDs, EIDs) :-
    atom(Prefix),
    !,
    enumerate_ids_acc(NormalizedSets, Prefix, IDs, [], EIDs).

enumerate_ids(_, _, _, _) :-
    add_error(enumerate_ids, 'Error: Prefix has to be an atom.', []).

enumerate_ids_acc(_, _, [], Acc, Acc).

enumerate_ids_acc(NormalizedSets, Prefix, [b(identifier(op(Name)),Type,Info)|T], Acc, EIDs) :-
    (normalization_inline_defs_only(true)
    -> NId = b(identifier(op(Name)),Type,Info)
    ; get_enumerated_name(Prefix, NewName),
    NId = b(identifier(op(NewName)),Type,Info)
    ),
    enumerate_ids_acc(NormalizedSets, Prefix, T, [(b(identifier(op(Name)),Type,Info),NId)|Acc], EIDs).

enumerate_ids_acc(NormalizedSets, Prefix, [Ast|T], Acc, EIDs) :-
    ( Ast = b(identifier(Name),Type,Info)
    ; ( Ast = b(_,Type,Info),
    member(synthesis(machinevar,Name), Info)
    )
    ),
    normalize_id_type(NormalizedSets, Type, NewType),
    (normalization_inline_defs_only(true)
    -> NId = b(identifier(op(Name)),Type,Info)
    ; get_enumerated_name(Prefix, NewName),
    adapt_machinevar_name_info(NewName, Info, NewInfo),
    NId = b(identifier(op(NewName)),NewType,NewInfo)
    ),
    enumerate_ids_acc(NormalizedSets, Prefix, T, [(b(identifier(Name),Type,Info),NId)|Acc], EIDs).

enumerate_record_fields([], NewC, Acc, NewC, Acc).

enumerate_record_fields([field(Name,_Type)|T], C, Acc, NewC, NewAcc) :-
    \+ member((Name,_), Acc),
    !,
    C1 is C+1,
    number_codes(C1, NC1),
    atom_codes(AC1, NC1),
    atom_concat('f', AC1, NName),
    enumerate_record_fields(T, C1, [(Name,NName)|Acc], NewC, NewAcc).

enumerate_record_fields([_|T], C, Acc, NewC, NewAcc) :-
    enumerate_record_fields(T, C, Acc, NewC, NewAcc).

enumerate_record_fields_from_types(CstsOrVars, Acc, NRecordFieldNames) :-
    length(Acc, C),
    enumerate_record_fields_from_types(CstsOrVars, C, Acc, NRecordFieldNames).

enumerate_record_fields_from_types([], _, Acc, Acc).

enumerate_record_fields_from_types([CstOrVar|T], C, Acc, NRecordFieldNames) :-
    CstOrVar = b(_,Type,_),
    get_record_fields_from_type([Type], [], RecordFields),
    !,
    enumerate_record_fields(RecordFields, C, Acc, NewC, NewAcc),
    enumerate_record_fields_from_types(T, NewC, NewAcc, NRecordFieldNames).

enumerate_record_fields_from_types([_|T], C, Acc, NRecordFieldNames) :-
    enumerate_record_fields_from_types(T, C, Acc, NRecordFieldNames).

get_b_and_eventb_machine_paths(Directory, FileList) :-
    directory_exists(Directory),
    directory_members_of_directory(Directory, SubDirectories),
    get_b_and_eventb_machine_paths_aux(SubDirectories, [], SubdirFileList), % Does not include toplevel machines.
    get_b_machines_in_dir(Directory, TopLevelMachines),
    append(TopLevelMachines, SubdirFileList, FileList).

get_b_and_eventb_machine_paths(Directory, []) :-
    \+ directory_exists(Directory).

get_b_and_eventb_machine_paths_aux([], Acc, Acc).

get_b_and_eventb_machine_paths_aux([_-AbsoluteSubDirectoryPath|T], Acc, FileList) :-
    get_b_machines_in_dir(AbsoluteSubDirectoryPath, BMachines),
    get_b_and_eventb_machine_paths(AbsoluteSubDirectoryPath, RecursiveFileList1),
    remove_normalized_machines(RecursiveFileList1, RecursiveFileList1, [], RecursiveFileList),
    append([BMachines,RecursiveFileList,Acc], NewAcc),
    get_b_and_eventb_machine_paths_aux(T, NewAcc, FileList).

get_b_machines_in_dir(Directory, BMachines) :-
    file_members_of_directory(Directory, '*.mch', BMachines1),
    % file_members_of_directory(Directory, '*.eventb', EventBMachines1),
    remove_normalized_machines(BMachines1, BMachines1, [], BMachines).

get_enumerated_name(Prefix, UniqueId) :-
    ( is_list(Prefix)
    ->
    CPrefix = Prefix
    ; atom_codes(Prefix, CPrefix)
    ),
    unique_id(CPrefix, UniqueId).

get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames, NRecordFieldNames) :-
    full_b_machine(Machine),
    Machine = machine(_,SectionList),
    member('deferred_sets'/DSets, SectionList),
    member('enumerated_sets'/ESets, SectionList),
    member('enumerated_elements'/Elements, SectionList),
    member('operation_bodies'/OperationBodies, SectionList),
    findall(OpNameId, member(b(operation(OpNameId,_,_,_),_,_), OperationBodies), OperationNames),
    findall(ReturnIds, member(b(operation(_,ReturnIds,_,_),_,_), OperationBodies), TempReturnIds),
    findall(Params, member(b(operation(_,_,Params,_),_,_), OperationBodies), TempParams),
    tools:flatten(TempParams, Params),
    tools:flatten(TempReturnIds, ReturnIds),
    enumerate_ids([], 'p', Params, NParams),
    enumerate_ids([], 'r', ReturnIds, NReturnIds),
    enumerate_ids([], 'o', OperationNames, NOperationNames),
    b_get_machine_all_constants(MachineConstants),
    b_get_machine_variables(MachineVars),
    random_permutation(ESets, RESets),
    random_permutation(DSets, RDSets),
    append(RESets, RDSets, RSets),
    random_permutation(MachineVars, RMachineVars),
    enumerate_record_fields_from_types(MachineConstants, [], NRecordFieldNames1),
    enumerate_record_fields_from_types(MachineVars, NRecordFieldNames1, NRecordFieldNames),
    enumerate_deferred_sets(RSets, [], NormalizedSets),
    % pass the new set names to adapt the types of identifiers too
    enumerate_ids(NormalizedSets, 'v', RMachineVars, EMachineVars),
    enumerate_ids(NormalizedSets, 'c', MachineConstants, EMachineConstants),
    enumerate_enum_elements(NormalizedSets, Elements, EElements),
    append([EMachineConstants,EElements,EMachineVars,NParams,NReturnIds], NormalizedIds),
    !.

get_record_fields_from_type([], Acc, RecordFields) :-
    !,
    RecordFields = Acc.

get_record_fields_from_type([record(Fields)|T], Acc, RecordFields) :-
    !,
    append(Fields, Acc, NewAcc),
    get_record_fields_from_type(T, NewAcc, RecordFields).

get_record_fields_from_type([Type|T], Acc, RecordFields) :-
    Type =.. [_|InnerT],
    get_record_fields_from_type(InnerT, Acc, Acc1),
    get_record_fields_from_type(T, Acc1, RecordFields).

group_enumerated_elements_by_set(NormalizedSets, Elements, GroupedElements) :-
    group_enumerated_elements_by_set(NormalizedSets, Elements, [], GroupedElements).

group_enumerated_elements_by_set([], _, Acc, Acc).

group_enumerated_elements_by_set([(RealId,NormalizedId)|T], Elements, Acc, GroupedElements) :-
    RealId = b(_,set(Type),_),
    findall(E, ( member(E, Elements),
    E = b(_,Type,_)
    ), Group),
    NormalizedId = b(identifier(NormalizedIdName),_,_),
    group_enumerated_elements_by_set(T, Elements, [NormalizedIdName-Group|Acc], GroupedElements).

inline_defs_only(Value) :-
    retractall(normalization_inline_defs_only(_)),
    assertz(normalization_inline_defs_only(Value)).

is_b_machine_file(FilePath, _, _) :-
    \+ atom(FilePath),
    !,
    add_error(normalize_b_machine, 'Prolog atom expected.', []),
    fail.

is_b_machine_file(FilePath, Prefix, Ext) :-
    member(Ext, ['.mch','.eventb','.prob']),
    atom_concat(Prefix, Ext, FilePath),
    !.

is_b_machine_file(FilePath, _, _) :-
    add_error(normalize_b_machine, 'Wrong file format. B/Event-B machine with extension .mch, .eventb or .prob expected:', FilePath),
    fail.

is_classical_b_machine_path(Path) :-
    atom(Path),
    atom_concat(_, Ext, Path),
    Ext == '.mch'.

load_b_or_eventb_machine(AbsoluteFilePath) :-
    is_classical_b_machine_path(AbsoluteFilePath),
    !,
    b_load_machine_from_file(AbsoluteFilePath),
    b_machine_precompile.

load_b_or_eventb_machine(AbsoluteFilePath) :-
    b_load_eventb_project(AbsoluteFilePath),
    b_machine_precompile.

machine_exists(FilePath) :-
    file_exists(FilePath),
    !.

machine_exists(FilePath) :-
    add_error(normalize_b_machine, 'File does not exist:', FilePath),
    fail.

map_normalize_ids_in_b_ast(Env, Ast, Ast, Env) :-
    normalization_inline_defs_only(true), !.

map_normalize_ids_in_b_ast(Env, Ast, NewAst, NewEnv) :-
    map_normalize_ids_in_b_ast_(Env, Ast, NewAst, NewEnv).

map_normalize_ids_in_b_ast_(Env, [], [], Env).

map_normalize_ids_in_b_ast_(Env, [Ast|T], [NAst|NT], NewEnv) :-
    normalize_ids_in_b_ast(Env, Ast, NAst, Env1),
    map_normalize_ids_in_b_ast_(Env1, T, NT, NewEnv).

normalize_b_machine(InputFilePath) :-
    retractall(tools:id_counter(_)),
    is_b_machine_file(InputFilePath, Prefix, Ext),
    (normalization_inline_defs_only(true)
    -> atom_concat(Prefix, '_inlinedef', OutputFilePath1)
    ; atom_concat(Prefix, '_normalized', OutputFilePath1)
    ),
    atom_concat(OutputFilePath1, Ext, OutputFilePath),
    normalize_b_machine(InputFilePath, OutputFilePath).

normalize_b_machine(InputFilePath, OutputFilePath) :-
    ground(OutputFilePath),
    error_manager:reset_errors,
    machine_exists(InputFilePath),
    format("Normalize machine: ~w~n", [InputFilePath]),
    load_b_or_eventb_machine(InputFilePath),
    b_machine_precompile,
    !,
    preferences:set_preference(use_solver_on_load, prob),
    get_normalized_id_name_mapping(NormalizedSets, NormalizedIds, NOperationNames, NRecordFieldNames),
    Env = [[],NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    full_b_machine(Machine),
    Machine = machine(MachineName,SectionList),
    subtract(SectionList, ['definitions'/_,'linking_invariant'/LinkingInvariant,'enumerated_elements'/EnumeratedElements,'enumerated_sets'/EnumeratedSets,'deferred_sets'/DeferredSets,'abstract_constants'/_,'concrete_constants'/_,'abstract_variables'/_,'concrete_variables'/_,'properties'/_,'invariant'/_,'linking_invariant'/_,'assertions'/_,'initialisation'/_,'operation_bodies'/OperationBodies,'definitions'/_], MachineMeta),
    % definitions are inlined and removed
    map_normalize_ids_in_b_ast(Env, DeferredSets, NDeferredSets, _),
    map_normalize_ids_in_b_ast(Env, EnumeratedSets, NEnumeratedSets, _),
    map_normalize_ids_in_b_ast(Env, EnumeratedElements, NEnumeratedElements, _),
    map_normalize_ids_in_b_ast(Env, OperationBodies, NOperationBodies, _),
    b_get_machine_variables(MachineVars),
    map_normalize_ids_in_b_ast(Env, MachineVars, NVariables, _),
    b_get_machine_all_constants(MachineConstants),
    map_normalize_ids_in_b_ast(Env, MachineConstants, NConstants, _),
    normalize_ids_in_b_ast(Env, LinkingInvariant, NLinkingInvariant, Env1),
    b_get_invariant_from_machine(MachineInvariant),
    normalize_ids_in_b_ast(Env1, MachineInvariant, NInvariant, Env2),
    b_get_properties_from_machine(MachineProperties),
    normalize_ids_in_b_ast(Env2, MachineProperties, NProperties, Env3),
    b_get_initialisation_from_machine(MachineInitialisation, _),
    normalize_ids_in_b_ast(Env3, MachineInitialisation, NInitialisation, Env4),
    get_all_assertions_from_machine(MachineAssertions),
    map_normalize_ids_in_b_ast(Env4, MachineAssertions, NAssertions, _),
    !,
    % unchanged: 'used'/_,'freetypes'/_,'operators'/_,'values'/_,'meta'/_,'constraints'/_,'promoted'/_,'unpromoted'/_,'internal_parameters'/_,'parameters'/_
    NMachine = machine(MachineName,['deferred_sets'/NDeferredSets,'enumerated_sets'/NEnumeratedSets,'enumerated_elements'/NEnumeratedElements,'concrete_constants'/NConstants,'abstract_variables'/NVariables,'properties'/NProperties,'invariant'/NInvariant,'linking_invariant'/NLinkingInvariant,'assertions'/NAssertions,'initialisation'/NInitialisation,'operation_bodies'/NOperationBodies|MachineMeta]),
    b_set_typed_machine(NMachine,InputFilePath),
   
    % atom_concat('/home/joshua/STUPS/prob_examples/public_examples', Rest, OutputFilePath),
    % atom_concat('/home/joshua/STUPS/prob_examples/public_examples_normalized', Rest, NOutputFilePath),
   
    b_write_machine_representation_to_file(none, OutputFilePath),
    format("Done.~n", []).

normalize_b_machine(InputFilePath, _) :-
    add_error(normalize_b_machine, 'Skip machine normalization due to errorneous B machine:', InputFilePath),
    fail.

normalize_b_machines([]).

normalize_b_machines([_MachineName-FilePath|T]) :-
    normalize_b_machine(FilePath),
    !,
    normalize_b_machines(T).

normalize_b_machines([_|T]) :-
    normalize_b_machines(T).

normalize_b_machines_in_dir(Directory) :-
    preferences:temporary_set_preference(use_common_subexpression_elimination, false),
    preferences:temporary_set_preference(optimize_ast, false),
    get_b_and_eventb_machine_paths(Directory, FileList),
    normalize_b_machines(FileList),
    preferences:reset_temporary_preference(use_common_subexpression_elimination),
    preferences:reset_temporary_preference(optimize_ast).

normalize_id_type(NormalizedAny, Name, NormalizedName) :-
    member((b(identifier(Name),_,_),b(identifier(NormalizedName),_,_)), NormalizedAny),
    !.

normalize_id_type(NormalizedRecFields, Name, NormalizedName) :-
    member((Name,NormalizedName), NormalizedRecFields),
    !.

normalize_id_type(NormalizedAny, Type, NType) :-
    Type =.. [Functor|Args],
    Args \== [],
    !,
    maplist(normalize_id_type(NormalizedAny), Args, NArgs),
    NType =.. [Functor|NArgs].

normalize_id_type(_, Type, Type).

normalize_ids_in_b_ast(Env, b(truth,pred,Info), NAst, NewEnv) :-
    !,
    NAst = b(truth,pred,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(falsity,pred,Info), NAst, NewEnv) :-
    !,
    NAst = b(falsity,pred,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, pred_true, NAst, NewEnv) :-
    !,
    NAst = b(value(pred_true),boolean,[]),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, pred_false, NAst, NewEnv) :-
    !,
    NAst = b(value(pred_false),boolean,[]),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(integer(Value),integer,Info), NAst, NewEnv) :-
    !,
    NAst = b(integer(Value),integer,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(identifier(op(Name)),_,_), NOperationName, NewEnv) :-
    !,
    Env = [_,_,_,NOperationNames,_],
    member((b(identifier(op(Name)),_,_),NOperationName), NOperationNames),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NId, NewEnv) :-
    Node =.. [function|Args],
    !,
    map_normalize_ids_in_b_ast(Env, Args, NArgs, NewEnv),
    NNode =.. [function|NArgs],
    NId = b(NNode,Type,Info).

normalize_ids_in_b_ast(Env, b(operation(OperationName,ReturnIds,Params,Body),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, OperationName, NOperationName, _),
    map_normalize_ids_in_b_ast(Env, ReturnIds, NReturnIds, _),
    map_normalize_ids_in_b_ast(Env, Params, NParams, _),
    normalize_ids_in_b_ast(Env, Body, NBody, NewEnv),
    NNode = operation(NOperationName,NReturnIds,NParams,NBody),
    NAst = b(NNode,Type,Info).

normalize_ids_in_b_ast(Env, b(Node,subst,Info), NAst, NewEnv) :-
    Node =.. [Functor,Assignments],
    ( Functor = select
    ; Functor = parallel
    ; Functor = sequence
    ),
    !,
    map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv),
    NNode =.. [Functor,NAssignments],
    NAst = b(NNode,subst,Info).

normalize_ids_in_b_ast(Env, b(struct(Record),Type,Info), b(struct(NRecord),NType,NInfo), NewEnv) :-
    normalize_ids_in_b_ast(Env, Record, NRecord, NewEnv),
    NewEnv = [_,_,NormalizedIds,_,_],
    normalize_id_type(NormalizedIds, Type, NType),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo).

normalize_ids_in_b_ast(Env, b(rec(Fields),Type,Info), b(rec(NFields),NType,NInfo), NewEnv) :-
    normalize_record_fields(Env, Fields, NFields, NewEnv),
    NewEnv = [_,_,NormalizedIds,_,_],
    normalize_id_type(NormalizedIds, Type, NType),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo).

normalize_ids_in_b_ast(Env, b(record_field(Id,Field),Type,Info), b(record_field(NId,NField),NType,NInfo), NewEnv) :-
    normalize_ids_in_b_ast(Env, Id, NId, Env1),
    normalize_ids_in_b_ast(Env1, Field, NField, NewEnv),
    NewEnv = [_,_,NormalizedIds,_,_],
    normalize_id_type(NormalizedIds, Type, NType),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo).

normalize_ids_in_b_ast(Env, b(assign(Ids,Assignments),subst,Info), b(assign(NIds,NAssignments),subst,Info), NewEnv) :-
    map_normalize_ids_in_b_ast(Env, Ids, NIds, _),
    map_normalize_ids_in_b_ast(Env, Assignments, NAssignments, NewEnv).

normalize_ids_in_b_ast(Env, b(assign_single_id(Id,Assignment),subst,Info), b(assign_single_id(NId,NAssignment),subst,Info), NewEnv) :-
    normalize_ids_in_b_ast(Env, Id, NId, _),
    normalize_ids_in_b_ast(Env, Assignment, NAssignment, NewEnv).

normalize_ids_in_b_ast(Env, b(value(global_set(SetName)),_,_), NId, NewEnv) :-
    !,
    Env = [_,NormalizedSets,_,_,_],
    member((b(identifier(SetName),_,_),NId), NormalizedSets),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, In, NewId, NewEnv) :-
    ( In = string(String), Info = []
    ; In = b(string(String),string,Info)),
    normalize_strings,
    !,
    NewId = b(string(NString),string,NInfo),
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    normalize_string(NormalizedStrings, String, NString, NewNormalizedStrings),
    NewEnv = [NewNormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    adapt_synthesis_ast_info(NewEnv, Info, NInfo).

normalize_ids_in_b_ast(Env, b(string(String),string,Info), Out, NewEnv) :-
    !,
    Out = b(string(String),string,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, string(String), Out, NewEnv) :-
    !,
    Out = b(string(String),string,[]),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(EmptySet,set(Type),Info), b(empty_set,set(NType),NInfo), Env) :-
    (EmptySet = set_extension([]); EmptySet = empty_set),
    adapt_synthesis_ast_info(Env, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType).

normalize_ids_in_b_ast(Env, b(EmptySeq,Type,Info), b(empty_sequence,NType,NInfo), Env) :-
    (EmptySeq = sequence_extension([]); EmptySeq = empty_sequence),
    adapt_synthesis_ast_info(Env, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType).

normalize_ids_in_b_ast(Env, List, NAst, NewEnv) :-
    List \= [],
    is_list(List),
    !,
    map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
    NewList = [b(_,Type,_)|_],
    NAst = b(set_extension(NewList),set(Type),[]).

normalize_ids_in_b_ast(Env, Ast, NewSetNode, NewEnv) :-
    ( Ast = b(value(avl_set(Avl)),set(Type),Info)
    ; Ast = avl_set(Avl),
    Type = set(any),
    Info = []
    ),
    !,
    avl_to_list(Avl, TList),
    findall(L, member(L-_, TList), List),
    map_normalize_ids_in_b_ast(Env, List, NewList, NewEnv),
    NewSetNode = b(set_extension(NewList),set(NType),NInfo),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType).

normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
    Env = [_,NormalizedSets,_,_,_],
    member((b(identifier(Name),_,_),NId), NormalizedSets),
    !,
    NewEnv = Env.

normalize_ids_in_b_ast(Env, Name, NewName, NewEnv) :-
    Env = [_,_,_,_,NRecordFieldNames],
    member((Name,NName), NRecordFieldNames),
    !,
    NewName = NName,
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(identifier(Name),Type,Info), NId, NewEnv) :-
    Env = [_,_,_,_,NRecordFieldNames],
    member((Name,NName), NRecordFieldNames),
    !,
    normalize_id_type(NRecordFieldNames, Type, NType),
    NId = b(identifier(NName),NType,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NId, NewEnv) :-
    Env = [_,_,NormalizedIds,_,_],
    member((b(identifier(Name),_,_),NId), NormalizedIds),
    !,
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
    Env = [_,NormalizedSets,_,_,_],
    atom_concat(SetName, Nr, Name),
    member((b(identifier(SetName),_,_),NId), NormalizedSets),
    !,
    NId = b(identifier(NSetName),NType,NInfo),
    atom_concat(NSetName, e, NNSetName),
    atom_concat(NNSetName, Nr, NName),
    NAst = b(identifier(NName),NType,NInfo),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, (A1,A2), NAst, NewEnv) :-
    !,
    % value couple
    normalize_ids_in_b_ast(Env, A1, NA1, Env1),
    normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
    NA1 = b(_,T1,_),
    NA2 = b(_,T2,_),
    NAst = b(couple(NA1,NA2),couple(T1,T2),[]).

normalize_ids_in_b_ast(Env, b(couple(A1,A2),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, A1, NA1, Env1),
    normalize_ids_in_b_ast(Env1, A2, NA2, NewEnv),
    adapt_synthesis_ast_info(Env, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType),
    NAst = b(couple(NA1,NA2),NType,NInfo).

normalize_ids_in_b_ast(Env, b(value(fd(Nr,SetName)),_,Info), b(Node,Type,NInfo), NewEnv) :-
    normalize_ids_in_b_ast(Env, fd(Nr,SetName), TAst, NewEnv),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    TAst = b(Node,Type,_).

normalize_ids_in_b_ast(Env, fd(Nr,SetName), NAst, NewEnv) :-
    Env = [_,NormalizedSets,_,_,_],
    member((b(identifier(SetName),_,_),NId), NormalizedSets),
    !,
    NId = b(identifier(NSetName),set(NType),_),
    atom_concat(NSetName, e, TempName),
    number_codes(Nr, NC),
    atom_codes(AN, NC),
    atom_concat(TempName, AN, NName),
    NAst = b(identifier(NName),NType,[]),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(identifier(Name),_,_), NAst, NewEnv) :-
    Env = [_,NormalizedSets,NormalizedIds,_,_],
    atom(Name),
    atom_concat(NameP, Prime, Name),
    ( Prime == '__prime'
    ; Prime == '\''
    ),
    ( member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedSets)
    ;
    member((b(identifier(NameP),_,_),b(identifier(TName),NType,NInfo)), NormalizedIds)
    ),
    !,
    atom_concat(TName, Prime, NName),
    NAst = b(identifier(NName),NType,NInfo),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor,Ids,Pred],
    ( Functor == exists
    ; Functor == comprehension_set
    ),
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
    adapt_synthesis_ast_info(Env1, Info, NInfo),
    NNode =.. [Functor,NIds,NPred],
    NAst = b(NNode,Type,NInfo),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(forall(Ids,LHS,RHS),Type,Info), NAst, NewEnv) :-
    !,
    % TO DO: refactor creation of local ids
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], LHS, NLHS, Env1),
    normalize_ids_in_b_ast(Env1, RHS, NRHS, Env2),
    adapt_synthesis_ast_info(Env2, Info, NInfo),
    NAst = b(forall(NIds,NLHS,NRHS),Type,NInfo),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor,Ids,Pred,Int],
    ( Functor == general_sum
    ; Functor == general_product
    ),
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
    normalize_ids_in_b_ast(Env1, Int, NInt, _),
    NNode =.. [Functor,NIds,NPred,NInt],
    NewEnv = Env,
    NAst = b(NNode,Type,Info).

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor,Ids,PredOrExpr],
    ( Functor == becomes_such
    ; Functor == becomes_element_of
    ),
    !,
    map_normalize_ids_in_b_ast(Env, Ids, NIds, Env1),
    normalize_ids_in_b_ast(Env1, PredOrExpr, NPredOrExpr, NewEnv),
    NNode =.. [Functor,NIds,NPredOrExpr],
    NAst = b(NNode,Type,Info).

normalize_ids_in_b_ast(Env, b(iteration(Id,Int),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Id, NId, NewEnv),
    NAst = b(iteration(NId,Int),Type,Info).

normalize_ids_in_b_ast(Env, b(choice(Substs),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, Substs, NSubsts, NewEnv),
    NAst = b(choice(NSubsts),Type,Info).

normalize_ids_in_b_ast(Env, b(kodkod(Int,List),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
    NAst = b(kodkod(Int,NList),Type,Info).

normalize_ids_in_b_ast(Env, b(assertion_expression(Expr1,Msg,Expr2),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Expr1, NExpr1, Env1),
    normalize_ids_in_b_ast(Env1, Expr2, NExpr2, NewEnv),
    NAst = b(assertion_expression(NExpr1,Msg,NExpr2),Type,Info).

normalize_ids_in_b_ast(Env, b(external_function_call(FuncName,Exprs),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, Exprs, NExprs, NewEnv),
    NAst = b(external_function_call(FuncName,NExprs),Type,Info).

normalize_ids_in_b_ast(Env, b(operation_call(Id,L1,L2),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Id, NId, Env1),
    map_normalize_ids_in_b_ast(Env1, L1, NL1, Env2),
    map_normalize_ids_in_b_ast(Env2, L2, NL2, NewEnv),
    NAst = b(operation_call(NId,NL1,NL2),Type,Info).

normalize_ids_in_b_ast(Env, b(while(Cond,Subst,Invariant,Variant),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Cond, NCond, Env1),
    normalize_ids_in_b_ast(Env1, Subst, NSubst, Env2),
    normalize_ids_in_b_ast(Env2, Invariant, NInvariant, Env3),
    normalize_ids_in_b_ast(Env3, Variant, NVariant, NewEnv),
    NAst = b(while(NCond,NSubst,NInvariant,NVariant),Type,Info).

normalize_ids_in_b_ast(Env, b(partition(Id,List),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Id, NId, Env1),
    map_normalize_ids_in_b_ast(Env1, List, NList, NewEnv),
    NAst = b(partition(NId,NList),Type,Info).

normalize_ids_in_b_ast(Env, b(if(IfElsifs),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, IfElsifs, NIfElsifs, NewEnv),
    NAst = b(if(NIfElsifs),Type,Info).

normalize_ids_in_b_ast(Env, b(var(Ids,Subst),Type,Info), NAst, NewEnv) :-
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    Env1 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
    normalize_ids_in_b_ast(Env1, Subst, NSubst, _),
    NAst = b(var(NIds,NSubst),Type,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(any(Ids,Pred,Subst),Type,Info), NAst, NewEnv) :-
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    normalize_ids_in_b_ast([NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames], Pred, NPred, Env1),
    normalize_ids_in_b_ast(Env1, Subst, NSubst, _),
    NAst = b(any(NIds,NPred,NSubst),Type,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(lazy_lookup_expr(RawIdName),Type,Info), NAst, NewEnv) :-
    atom(RawIdName),
    !,
    Env = [_,_,NormalizedIds,_,_],
    member((b(identifier(RawIdName),_,_),b(identifier(NRawIdName),_,_)), NormalizedIds),
    NAst = b(lazy_lookup_expr(NRawIdName),Type,Info),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, b(recursive_let(Id,Expr),Type,Info), NAst, NewEnv) :-
    !,
    normalize_ids_in_b_ast(Env, Id, NId, Env1),
    normalize_ids_in_b_ast(Env1, Expr, NExpr, _),
    NewEnv = Env,
    NAst = b(recursive_let(NId,NExpr),Type,Info).

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor,Ids,PredOrExprs,Sub],
    ( Functor == let_expression
    ; Functor == let_predicate
    ; Functor == let
    ),
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    append(EIds, NormalizedIds, NNormalizedIds),
    Env0 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
    ( is_list(PredOrExprs)
    ->
    map_normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
    ; normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
    ),
    normalize_ids_in_b_ast(Env1, Sub, NSub, _),
    NNode =.. [Functor,NIds,NExprs,NSub],
    NAst = b(NNode,Type,Info),
    NewEnv = Env. % normalized ids are local

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor,Id,PredOrExprs,Sub],
    ( Functor == lazy_let_pred
    ; Functor == lazy_let_expr
    ; Functor == reorder_lazy_let_pred
    ; Functor == reorder_lazy_let_expr
    ),
    !,
    Env = [NormalizedStrings,NormalizedSets,NormalizedIds,NOperationNames,NRecordFieldNames],
    Ids = [Id],
    enumerate_ids(NormalizedSets, 'l', Ids, EIds),
    findall(NId, member((_,NId), EIds), NIds),
    NIds = [NId],
    append(EIds, NormalizedIds, NNormalizedIds),
    Env0 = [NormalizedStrings,NormalizedSets,NNormalizedIds,NOperationNames,NRecordFieldNames],
    ( is_list(PredOrExprs)
    ->
    map_normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
    ; normalize_ids_in_b_ast(Env0, PredOrExprs, NExprs, Env1)
    ),
    normalize_ids_in_b_ast(Env1, Sub, NSub, _),
    NNode =.. [Functor,NId,NExprs,NSub],
    NAst = b(NNode,Type,Info),
    NewEnv = Env. % normalized ids are local

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node = value(Arg),
    is_list(Arg),
    !,
    map_normalize_ids_in_b_ast(Env, Arg, NArg, NewEnv),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType),
    NNode = set_extension(NArg),
    NAst = b(NNode,NType,NInfo).

normalize_ids_in_b_ast(Env, b(value(Value),_Type,Info), b(Node,NType,NInfo), Env) :-
    normalize_ids_in_b_ast(Env, Value, NAst, NewEnv),
    NAst = b(Node,NType,_),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo).

normalize_ids_in_b_ast(Env, b(set_extension(List),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType),
    NAst = b(set_extension(NList),NType,NInfo).

normalize_ids_in_b_ast(Env, b(sequence_extension(List),Type,Info), NAst, NewEnv) :-
    !,
    map_normalize_ids_in_b_ast(Env, List, NList, NewEnv),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType),
    NAst = b(sequence_extension(NList),NType,NInfo).

normalize_ids_in_b_ast(Env, b(Node,Type,Info), NAst, NewEnv) :-
    Node =.. [Functor|Args],
    b_component(Functor),
    !,
    map_normalize_ids_in_b_ast(Env, Args, NArgs, NewEnv),
    adapt_synthesis_ast_info(NewEnv, Info, NInfo),
    NNode =.. [Functor|NArgs],
    Env = [_,NormalizedSets,_,_,_],
    normalize_id_type(NormalizedSets, Type, NType),
    NAst = b(NNode,NType,NInfo).

normalize_ids_in_b_ast(Env, [], NAst, NewEnv) :-
    !,
    NAst = b(empty_set,set(any),[]),
    NewEnv = Env.

normalize_ids_in_b_ast(Env, Value, Ast, NewEnv) :-
    value_to_ast(Value, Ast),
    !,
    Env = NewEnv.

normalize_ids_in_b_ast(Env, Ast, NAst, NewEnv) :-
    whitelist(Ast),
    !,
    NAst = Ast,
    NewEnv = Env.

normalize_ids_in_b_ast(Env, Ast, Ast, Env) :-
    nl,
    print(Ast),
    nl,
    add_warning(normalize_ids_in_b_ast, 'Skipped AST for normalization:', Ast).

normalize_record_fields(Env, [], [], Env).

normalize_record_fields(Env, [Field|T], [NField|NT], NewEnv) :-
    Env = [_,_,_,_,NRecordFieldNames],
    Field = field(Name,Value),
    ( member((Name,NName), NRecordFieldNames),
    Env1 = Env
    ; Env = [A,B,C,D,NRecordFieldNames],
    length(NRecordFieldNames, L),
    L1 is L+1,
    number_codes(L1, NL1),
    atom_codes(AL1, NL1),
    atom_concat('f', AL1, NName),
    Env1 = [A,B,C,D,[(Name,NName)|NRecordFieldNames]]
    ),
    normalize_ids_in_b_ast(Env1, Value, NValue, Env2),
    NField = field(NName,NValue),
    normalize_record_fields(Env2, T, NT, NewEnv).

normalize_string(NormalizedStrings, String, NString, NormalizedStrings) :-
    % string has already been seen
    member((NString,String), NormalizedStrings),
    !.

normalize_string(NormalizedStrings, String, NString, [(NString,String)|NormalizedStrings]) :-
    length(NormalizedStrings, AmountOfStrings),
    AmountOfStrings1 is AmountOfStrings+1,
    number_codes(AmountOfStrings1, CIndex),
    append([83], CIndex, CString),
    atom_codes(NString, CString),
    !.

remove_file_extension(Path, Prefix, Ext) :-
    atom_concat(Prefix, '.mch', Path),
    Ext = '.mch'.

remove_file_extension(Path, Prefix, Ext) :-
    atom_concat(Prefix, '.eventb', Path),
    Ext = '.eventb'.

remove_normalized_machines(_, [], Acc, Acc).

remove_normalized_machines(All, [Name-Path|T], Acc, Filtered) :-
    \+ atom_concat(_, '_normalized.mch', Path),
    \+ atom_concat(_, '_normalized.eventb', Path),
    \+ atom_concat(_, '_inlinedef.mch', Path),
    \+ atom_concat(_, '_inlinedef.eventb', Path),
    remove_file_extension(Path, PrefixPath, Ext),
    (normalization_inline_defs_only(true)
    -> atom_concat(PrefixPath, '_inlinedef', TNPath)
    ; atom_concat(PrefixPath, '_normalized', TNPath)
    ),
    atom_concat(TNPath, Ext, NPath),
    \+ member(_-NPath, All),
    !,
    remove_normalized_machines(All, T, [Name-Path|Acc], Filtered).

remove_normalized_machines(All, [_|T], Acc, Filtered) :-
    remove_normalized_machines(All, T, Acc, Filtered).

value_to_ast(Value, b(value(Value),Type,[])) :-
    kernel_objects:infer_value_type(Value, Type).