b_machine_hierarchy

all_definition_ids(Body,Ids) :-
    get_opt_section(definitions,Body,Definitions),
    convlist(get_definition_name,Definitions,Ids1),
    sort(Ids1,Ids).

analyse_eventb_context(Context) :-
    event_b_context(Context,Name,Sections),
    get_identifiers([constants],Sections,ConcreteConstants),
    get_identifiers([abstract_constants],Sections,AbstractConstants),
    append([ConcreteConstants,AbstractConstants],AllConstants),
    get_sets(Sections,Sets),
    get_extends_refs(Sections,Refs),
    store_eventb_hash(Name,Context),
    assertz(machine_type(Name,context)),
    assertz(machine_identifiers(Name,[],Sets,[],[],[],AllConstants)),
    assertz(machine_references(Name,Refs)),
    assertz(machine_operations(Name,[])),
    assertz(machine_operation_calls(Name,[])),
    maplist(assert_raw_id_with_position(concrete_constant),ConcreteConstants),
    maplist(assert_raw_id_with_position(abstract_constant),AbstractConstants),
    assert_if_has_theorems(Name,Sections).

analyse_eventb_hierarchy(Machines,Contextes) :-
    reset_hierarchy,
    get_eventb_name(Machines,Contextes,MainName),
    assertz(main_machine_name(MainName)),
    maplist(analyse_eventb_machine,Machines),
    analyse_eventb_refinement_types(Machines),
    maplist(analyse_eventb_context,Contextes),!.

analyse_eventb_hierarchy(Machines,Contextes) :-
    add_internal_error('Analyzing Event-B Hierarchy Failed: ',analyse_eventb_hierarchy(Machines,Contextes)).

analyse_eventb_machine(Machine) :-
    event_b_model(Machine,Name,Sections),
    % print(analyzing(Name)),nl,
    ( memberchk(refines(_,RName),Sections) -> Type=refinement, RRefs=[ref(refines,RName,'')]
    ; Type=abstract_model, RRefs=[], RName='$none'),
    get_identifiers([variables],Sections,Vars),
    get_sees_context_refs(Sections,SRefs),
    append(RRefs,SRefs,Refs),
    get_events(Name,Sections,Events,RName),
    store_eventb_hash(Name,Machine),
    assertz(machine_type(Name,Type)),
    assertz(machine_identifiers(Name,[],[],Vars,[],[],[])),
    assertz(machine_references(Name,Refs)),
    assertz(machine_operations(Name,Events)),
    assertz(machine_operation_calls(Name,[])), % Event-B events cannot call other events
    assert_if_has_theorems(Name,Sections).

analyse_eventb_refinement_types([]).

analyse_eventb_refinement_types([RefMachine,AbsMachine|_]) :-
    event_b_model(RefMachine,RefName,RefSections),
    memberchk(refines(_,AbsName),RefSections),
    event_b_model(AbsMachine,AbsName,AbsSections),
    get_opt_section(events,RefSections,RawEvents),
    get_opt_section(events,AbsSections,AbsRawEvents),
    member(RawEvent,RawEvents),
    bmachine_eventb:raw_event(RawEvent,_,RefEvName,_St1,Ref,_Prm1,RefGrd,_Thm1,RefAct,_Wit1),
    Ref = [AbsEvName],
    member(AbsRawEvent,AbsRawEvents),
    bmachine_eventb:raw_event(AbsRawEvent,_,AbsEvName,_St2,_,_Prm2,AbsGrd,_Thm2,AbsAct,_Wit2),
    check_raw_prefix(AbsGrd,RefGrd,SameGuard),
    check_raw_prefix(AbsAct,RefAct,SameAct),
    %% format('~nEvent refinement change ~w (~w) -> ~w (~w) guard: ~w, action: ~w~n',[RefEvName,RefName,AbsEvName,AbsName,SameGuard,SameAct]),
    %print(rawgrd(RefGrd,AbsGrd)), nl, print(rawact(RefAct,AbsAct)),nl,
    assertz(event_refinement_change(RefName,RefEvName,AbsName,AbsEvName,SameGuard,SameAct)),
    fail.

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

analyse_hierarchy(Main,Machines) :- (var(Main) ; var(Machines)),!,
    add_internal_error('Illegal call:',analyse_hierarchy(Main,Machines)).

analyse_hierarchy(Main,Machines) :-
    reset_hierarchy,
    assertz(main_machine_name(Main)),
    analyse_machine(Main,Machines,main).

analyse_machine(Name,_Machines,_) :-
    % machine already analysed
    machine_type(Name,_),!.

analyse_machine(Name,Machines,_) :-
    debug:debug_println(19,analysing_machine(Name)),
    get_machine(Name,Machines,Type,Header,Refines,Body),
    !,
    ( cache_is_activated -> % we need the machines stored for later analysis
    assert_all_machines(Machines)
    ; true),
    assertz(machine_type(Name,Type)),
    (get_machine_parent_directory(Name,Dir) -> assertz(machine_package_directory(Name,Dir)) ; true),
    ( get_raw_section(assertions,Body,_) ->
    assertz(machine_has_assertions(Name))
    ; true),
    store_identifiers(Name,Header,Body),
    store_operations(Name,Body),
    store_values(Name,Body),
    store_references(Name,Refines,Body,Machines).

analyse_machine(Name,Machines,RefType) :-
    get_machine_file_number(Name,_Ext,Nr,File),
    get_ref_type_name(RefType,Clause),
    !,
    ( member(M,Machines),get_constructed_machine_name_and_filenumber(M,OtherName,Nr)
    -> ajoin(['Cannot use B machine "',Name,'" within ', Clause,
    ' clause. Rename machine "', OtherName,'" to "', Name, '" in file: '],Msg)
    ; ajoin(['Cannot find B machine "',Name,'" within ', Clause,
    ' clause. Check that machine name matches filename in: '],Msg)
    ),
    add_error_fail(invalid_machine_reference,Msg,File).

analyse_machine(Name,_Machines,_) :-
    add_error_fail(invalid_machine_reference,
    'Could not find machine in parsed machine list (check that your machine names match your filenames): ',Name).

analyze_extends_relation :-
    retractall(event_info(_,_,_)),
    bmachine:b_get_machine_operation(_Name,_Results,_RealParameters,TBody,_OType,_OpPos),
    treat_event_body(TBody),fail.

analyze_extends_relation.

arrow_style(unchanged,unchanged,Style,ColPref) :- !,
    Style=arrowhead(none,solid), ColPref=dot_event_hierarchy_extends_colour.

arrow_style(refines,_,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.

arrow_style(_,refines,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.

arrow_style(_,_,Style,dot_event_hierarchy_extends_colour) :- Style = arrowhead(vee,solid). % we have extends

assert_all_machines(Machines) :-
    (raw_machine(_,_)
    -> true % machines already asserted
    ; maplist(assert_raw_machine,Machines)).

assert_if_has_theorems(Name,Sections) :-
    get_opt_section(theorems,Sections,[_|_]),
    assertz(machine_has_assertions(Name)).

assert_if_has_theorems(_Name,_Sections).

assert_raw_id_with_position(PredFunctor,Rid) :-
    (raw_id_is_identifier(Rid,Pos,ID)
    -> true
    ; Rid = definition(Pos,ID,_)
    -> add_error(illegal_definition_use,'Definition cannot be used as identifier here: ',ID,Pos)
    ; add_error_fail(assert_raw_id_with_position,'Not identifier: ',Rid)
    ),
    Fact =.. [PredFunctor,ID,Pos],
    assertz(Fact), debug_println(9,Fact).

assert_raw_machine(Machine) :-
    get_raw_machine_name(Machine,Name),
    (raw_machine(Name,_) -> add_warning(b_machine_hierarchy,'Raw machine already exists: ',Name) ; true),
    assertz( raw_machine(Name,Machine) ).

check_raw_prefix([],[],Res) :- !, Res=unchanged.

check_raw_prefix([],[_|_],Res) :- !, Res=extends. % the refinement has some more actions/guards

check_raw_prefix([Abs|AT],[Ref|RT],Result) :- same_raw_expression(Abs,Ref),!,
    check_raw_prefix(AT,RT,Result).

check_raw_prefix(_,_,refines).

compute_event_refines(MachineName,RawEvents,AbsMachineName) :-
    member(RawEvent,RawEvents),
    bmachine_eventb:raw_event(RawEvent,_Pos,EvName,_St,Refines,_Prm,_Grd,_Thm,_Act,_Wit),
    member(RefEvent,Refines),
    % print(refines(MachineName,EvName,AbsMachineName,RefEvent)),nl,
    assertz(refines_event(MachineName,EvName,AbsMachineName,RefEvent)),
    fail.

compute_event_refines(_,_,_).

compute_machine_hash(Name,Digest) :-
    if(raw_machine(Name,Machine),
    raw_sha_hash(Machine,Digest),
    add_error_and_fail(compute_machine_hash,'Machine does not exist or has not been processed:',Name)
).

compute_properties_hash(Name,Hash) :-
    raw_machine(Name,Machine),
    get_machine(Name,[Machine],_Type,_Header,_Refines,Body),
    extract_sorted_np_sets(Body,Sets),
    extract_sorted_np_constants(Body,Constants),
    extract_np_properties(Body,Properties),
    extract_used_np_definitions_from_properties(Body,Definitions),
    ToHash = [Sets,Constants,Properties,Definitions],
    raw_sha_hash(ToHash,Hash).

computed_basic_operation_hashes :-
    basic_operation_hash(_,_,_,_),!. % already computed

computed_basic_operation_hashes :-
    get_raw_machine_operation_hash(MachName,OpName,Digest,OpCalls),
    (basic_operation_hash(OpName,_,_,_)
    -> add_warning(computed_basic_operation_hashes,'Multiple hashes for operation: ',OpName)
    ; true),
    assertz(basic_operation_hash(OpName,MachName,Digest,OpCalls)),
    get_hex_bytes(Digest,Hex),
    formatsilent('value caching: basic op hash ~w in ~w hash: ~s (calls ~w)~n',[OpName,MachName,Hex,OpCalls]),
    fail.

computed_basic_operation_hashes.

dec_atom_length(Prev,Atom,New) :- atom_length(Atom,Len),
    New is Prev-Len.

dot_event_node(M:Ev,M,Desc,Shape,Style,Color) :-
    findall(showev(M,Ev),event_to_show(M,Ev),List), sort(List,SList),
    member(showev(M,Ev),SList),
    (event_info(M,Ev,Status) -> true ; Status=unknown),
    (event_refinement_change(M,Ev,_,_,SameGuard,SameAction)
    -> true ; SameGuard=unknown, SameAction=unknown),
    (SameGuard=unchanged,SameAction=unchanged -> ajoin([Ev,'\\n(unchanged)'],Ev2)
    ; SameGuard=unchanged -> ajoin([Ev,'\\n(same grd)'],Ev2)
    ; SameAction=unchanged -> ajoin([Ev,'\\n(same act)'],Ev2)
    ; Ev2=Ev),
    (Status = convergent -> ajoin([Ev2,' (<)'],Desc)
    ; Status = anticipated -> ajoin([Ev2, '(<=)'],Desc)
    ; Desc=Ev2),
    dot_get_color_style(M,Ev,Status,SameGuard,SameAction,Shape,Color,Style).

dot_get_color_style(M,Ev,_Status,_,_,box,Color,Style) :- \+ refines_event(M,Ev,_,_),!,
    get_preference(dot_event_hierarchy_new_event_colour,Color), Style=none.

dot_get_color_style(M,Ev,_,SameGuard,SameAction,box,Color,Style) :-
    refines_event(M,Ev,_,Ev2), dif(Ev2,Ev),!, % changes name
    ((SameGuard,SameAction)=(unchanged,unchanged)
    -> get_preference(dot_event_hierarchy_rename_unchanged_event_colour,Color)
    ; get_preference(dot_event_hierarchy_rename_event_colour,Color)), Style=filled.

dot_get_color_style(_M,_Ev,_,unchanged,unchanged,box,Color,Style) :- % keeps name and adds no guard or action
    !,
    get_preference(dot_event_hierarchy_unchanged_event_colour,Color), Style=filled.

dot_get_color_style(_M,_Ev,_,_,unchanged,box,Color,Style) :- % keeps name and adds no action, but modifies guard
    !,
    get_preference(dot_event_hierarchy_grd_strengthening_event_colour,Color), Style=filled.

dot_get_color_style(_M,_Ev,_,unchanged,_,box,Color,Style) :- % keeps name and adds action but keeps guard
    !,
    get_preference(dot_event_hierarchy_grd_keeping_event_colour,Color), Style=filled.

dot_get_color_style(_M,_Ev,_,_,_,box,Color,Style) :- % keeps name but adds or modifies
    % TO DO: distinguish extends from refines
    get_preference(dot_event_hierarchy_refines_colour,Color), Style=filled.

dot_op_calls_op(Op1,Label,Op2,Color,Style) :- Style=solid, Color=steelblue,
    Label = '', % TO DO: different colors for local operation calls, detect op calls in expressions?
    machine_operation_calls(_,Operations),
    member(calls(Op1,Op2),Operations).

dot_operation_node(OpName,M,Desc,Shape,Style,Color) :-
    machine_operations(M,Operations),
    (machine_promotes_operations(M,Promotes) -> true ; Promotes=[]),
    raw_identifier_member(OpName,Operations),
    (b_top_level_feasible_operation(OpName) -> Color=lightgray
    ; b_top_level_operation(OpName) -> Color='OldLace' % commented out operation
    ; raw_identifier_member(OpName,Promotes) -> Color='gray98' % promoted but not to top_level
    ; Color=white),
    Desc=OpName, Shape=box, Style=filled.

dot_refines_event(M2:Ev2,Label,M1:Ev1,Color,Style) :-
    Label = '', % TO DO: detect refine, extends, identical
    refines_event(M1,Ev1,M2,Ev2),
    Ev1 \= 'INITIALISATION',
    (event_refinement_change(M1,Ev1,_,_,SameGuard,SameAct)
    -> arrow_style(SameGuard,SameAct,Style,ColPref), get_preference(ColPref,Color)
    ; Style=solid, Color=red % should not happen
).

dot_subgraph(M,filled,Colour) :- get_preference(dot_event_hierarchy_machine_colour,Colour),
    machine_operations(M,[_|_]).

event_b_context(event_b_context(_,Name,Sections),Name,Sections).

event_b_model(event_b_model(_,Name,Sections),Name,Sections).

event_to_show(M,Ev) :- machine_operations(M,Evs),
    raw_identifier_member(Ev,Evs), Ev \= 'INITIALISATION'.

event_to_show(M,Ev) :-
    event_refinement_change(M,Ev,_,_,_,_), % for events that disappear, i.e., are not refined until bottom level
    Ev \= 'INITIALISATION'.

extract_np_properties(Body,Properties) :-
    get_opt_section(properties,Body,PosProperties),
    remove_raw_position_info(PosProperties,Properties).

extract_sorted_np_constants(Body,Constants) :-
    get_opt_sections([constants,concrete_constants,abstract_constants],Body,PosConstants),
    remove_raw_position_info(PosConstants,UnsortedConstants),
    sort(UnsortedConstants,Constants).

extract_sorted_np_sets(Body,Sets) :-
    get_sets(Body,PosSets),
    remove_raw_position_info(PosSets,UnsortedSets),
    sort(UnsortedSets,Sets).

extract_used_np_definitions(RawSyntax,Body,Definitions,PosDefinitions) :-
    extract_raw_identifiers(RawSyntax,UsedIds),
    all_definition_ids(Body,AllDefs),
    ord_intersection(UsedIds,AllDefs,UsedDefNames),
    transitive_used_definitions(UsedDefNames,AllUsedDefs),
    findall( definition(none,Name,Args,DefBody),
    ( member(Name,AllUsedDefs),b_get_definition(Name,_DefType,Args,DefBody,_Deps)),
    PosDefinitions),
    maplist(remove_raw_position_info,PosDefinitions,Definitions).

extract_used_np_definitions_from_properties(Body,Definitions) :-
    get_opt_section(properties,Body,Properties),
    extract_used_np_definitions(Properties,Body,Definitions,_).

filter_redundant_refs([],_,[]).

filter_redundant_refs([ref(sees,Dest,_)|T],All,R) :-
    machine_type(Dest,context),
    member(ref(sees,Other,_),All),
    machine_references(Other,Refs),
    member(ref(extends,Dest,_),Refs), % Dest already seen by other seen context;
    % Note: Rodin export contains transitive sees relation;
    % if the user had included Dest in the sees clause we would have a warning "Redundant seen context"
    !,
    %format(user_output,'Redundant sees of ~w (~w)~n',[Dest,Other]),
    filter_redundant_refs(T,All,R).

filter_redundant_refs([H|T],All,[H|R]) :-
    filter_redundant_refs(T,All,R).

findrefs(Body,Type,Refs) :-
    get_opt_section(Type,Body,RawRefs),
    findrefs2(RawRefs,Type,Refs).

findrefs2([],_Type,[]).

findrefs2([machine_reference(_Pos,R,_Params)|MRest],Type,[ref(Type,Name,Prefix)|RRest]) :-
    bmachine_construction:split_prefix(R,Prefix,Name),
    findrefs2(MRest,Type,RRest).

findusessees(Body,Type,Refs) :-
    get_opt_section(Type,Body,RawRefs),
    findusessees2(RawRefs,Type,Refs).

findusessees2([],_Type,[]).

findusessees2([identifier(_Pos,Name)|MRest],Type,[ref(Type,Name,'')|RRest]) :-
    findusessees2(MRest,Type,RRest).

follow_refs([],_Machines).

follow_refs([ref(RefType,Name,_Prefix)|Rest],Machines) :-
    analyse_machine(Name,Machines,RefType),
    follow_refs(Rest,Machines).

get_abstract_machine_type(machine(_Pos2),R) :- !,R=abstract_machine.

get_abstract_machine_type(system(_Pos2),R) :- !,R=abstract_machine.

get_abstract_machine_type(model(_Pos2),R) :- !,R=abstract_model.

get_abstract_machine_type(X,R) :- atomic(X),!,
    add_error(get_abstract_machine_type,'Your parser seems out-dated. Assuming abstract_machine: ',X),
    R=abstract_machine.

get_basic_op_hash(OpName,Digest) :-
    basic_operation_hash(OpName,_MachName,Digest,_OpCalls).

get_def_body(Body,Defs) :- member(definition(_,_DefName,_,Body),Defs).

get_eventb_name([MainMachine|_AbstractMachines],_Contextes,Name) :-
    event_b_model(MainMachine,Name,_),!.

get_eventb_name(_Machines,[MainContext|_AbstractContextes],Name) :-
    event_b_context(MainContext,Name,_).

get_events(Name,Sections,Events,AbsMachineName) :-
    get_opt_section(events,Sections,RawEvents),
    compute_event_refines(Name,RawEvents,AbsMachineName),
    findall( identifier(Pos,EvName),
    ( member(RawEvent,RawEvents),
    raw_event(RawEvent,Pos,EvName,_St,_Rf,_Prm,_Grd,_Thm,_Act,_Wit) ),
    Events).

get_extends_refs(Sections,Refs) :-
    get_opt_section(extends,Sections,Extended),
    findall(ref(extends,E,''),member(E,Extended),Refs).

get_identifiers([],_Body,[]).

get_identifiers([Sec|Rest],Body,Ids) :-
    get_opt_section(Sec,Body,Ids1),
    append(Ids1,IRest,Ids),
    get_identifiers(Rest,Body,IRest).

get_machine(Name,Machines,Type,Header,Refines,Body) :-
    get_machine1(Name,Machines,_Machine,Type,Header,Refines,Body).

get_machine1(Name,Machines,Machine,Type,Header,Refines,Body) :-
    Header = machine_header(_Pos,Name,_Params),
    member(Machine,Machines),
    get_machine2(Machine,Type,Header,Refines,Body),!.

get_machine2(abstract_machine(_Pos,MS,Header,Body),TypeOfAbstractMachine,Header,[],Body) :-
    get_abstract_machine_type(MS,TypeOfAbstractMachine).

get_machine2(refinement_machine(_Pos,Header,Refines,Body),refinement,Header,[Refines],Body).

get_machine2(implementation_machine(_Pos,Header,Refines,Body),implementation,Header,[Refines],Body).

get_machine2(generated(_Pos,Machine),A,B,C,D) :- % @generated Pragma used at top of file
    get_machine2(Machine,A,B,C,D).

get_machine2(unit_alias(_Pos,_Name,_Alias,Machine),A,B,C,D) :-
    get_machine2(Machine,A,B,C,D).

get_machine_identifier_names(Name,Params,Sets,AVars,CVars,AConsts,CConsts) :-
    machine_identifiers(Name,RawParams,RawSets,RawAVars,RawCVars,RawAConsts,RawCConsts),
    maplist(raw_id_is_identifier2,RawParams,Params),
    maplist(raw_id_is_identifier2,RawSets,Sets),
    maplist(raw_id_is_identifier2,RawAVars,AVars),
    maplist(raw_id_is_identifier2,RawCVars,CVars),
    maplist(raw_id_is_identifier2,RawAConsts,AConsts),
    maplist(raw_id_is_identifier2,RawCConsts,CConsts).

get_machine_parent_directory(Name,DirName) :-
    % try and get parent directory name; useful to distinguish different packages when using package pragma
    get_machine_file_number(Name,_Ext,_Nr,File),
    get_parent_directory_name(File,DirName).

get_machine_type_keyw(abstract_machine,'MACHINE').

get_machine_type_keyw(abstract_model,'MODEL').

get_machine_type_keyw(refinement,'REFINEMENT').

get_machine_type_keyw(implementation,'IMPLEMENTATION').

get_machine_type_keyw(context,'CONTEXT').

get_opt_section(Sec,Body,Result) :-
    ( get_raw_section(Sec,Body,Content) -> Result=Content; Result=[]).

get_opt_sections([],_Body,[]).

get_opt_sections([S|Srest],Body,Contents) :-
    get_opt_section(S,Body,L),append(L,Rest,Contents),
    get_opt_sections(Srest,Body,Rest).

get_parameters(machine_header(_Pos,_Name,Params),Params).

get_raw_identifier(Raw,Res) :- raw_id_is_identifier(Raw,_Pos,Id),!, Res=Id.

get_raw_identifier(definition(_Pos,DID,[]),ID) :- % see also expand_definition_to_variable_list
    atom(DID),!,
    ajoin([DID,'(DEFINITION)'],ID).

get_raw_identifier(Raw,Res) :- add_internal_error('Cannot get identifier:',Raw),Res='???'.

get_raw_machine_name(Machine,Name) :-
    get_machine2(Machine,_,machine_header(_,Name,_),_,_).

get_raw_machine_operation_hash(MachName,OpName,Digest,SOpCalls) :-
    raw_machine(MachName,Machine),
    get_machine(MachName,[Machine],_Type,_Header,_Refines,MachBody),
    get_opt_section(operations,MachBody,Operations),
    Op = operation(_,identifier(_,OpName),_,_,_),
    member(Op,Operations),
    get_raw_operation_id_and_body(Op,identifier(_,OpName),OpBody),
    extract_used_np_definitions(Op,MachBody,UsedDefinitions,DefsWithPos),
    remove_raw_position_info(Op,RawOperation),
    raw_sha_hash(op(RawOperation,UsedDefinitions),Digest),
    findall(Id, (get_raw_operation_call_id(OpBody,Id) % extract op calls in body of operation
    ; get_def_body(Def,DefsWithPos), get_raw_operation_call_id(Def,Id) % extract op calls in definitions
    ),
    OpCalls),
    sort(OpCalls,SOpCalls).

get_raw_operation_call(block(_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(precondition(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(assertion(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(var(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(select_when(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(if_elsif(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(let(_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(any(_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(case(_,_,_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(while(_,_Cond,Body,_,_),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(parallel(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).

get_raw_operation_call(sequence(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).

get_raw_operation_call(if(_,_Test,Then,List,Else),ID) :- !,member(A,[Then,Else|List]), get_raw_operation_call(A,ID).

get_raw_operation_call(select(_,_Cond,Body,List),ID) :- !,member(A,[Body|List]), get_raw_operation_call(A,ID).

get_raw_operation_call(select(_,_Cond,Body,List,Else),ID) :- !,member(A,[Body,Else|List]), get_raw_operation_call(A,ID).

get_raw_operation_call(choice(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).

get_raw_operation_call(choice_or(_,Body),ID) :- !, get_raw_operation_call(Body,ID).

get_raw_operation_call(operation_call(_,ID,_,_),ID) :- !.

get_raw_operation_call(skip(_),_) :- !, fail.

get_raw_operation_call(assign(_,_,_),_) :- !, fail.

get_raw_operation_call(becomes_element_of(_,_,_),_) :- !, fail.

get_raw_operation_call(becomes_such(_,_,_),_) :- !, fail.

get_raw_operation_call(definition(_,Name,_),_) :- !, % TO DO: improve
    debug_format(19,'Ignoring operation calls in DEFINITION ~w for operation call diagram~n',[Name]),
    % b_get_definition(Name,_DefType,_Args,DefBody,_Deps), not yet precompiled !
    fail.

get_raw_operation_call(Subst,_) :- functor(Subst,F,N),print(uncovered_subst(F,N,Subst)),nl,fail.

get_raw_operation_call(Op,Id,CallsId) :-
    get_raw_operation_id_and_body(Op,identifier(_,Id),Body),
    get_raw_operation_call(Body,identifier(_,CallsId)).

get_raw_operation_call_id(OpBody,CalledId) :-
    try_get_raw_operation_call(OpBody,identifier(_,CalledId)).

get_raw_operation_id_and_body(operation(_Pos,Id,_,_,Body),Id,Body).

get_raw_operation_id_and_body(refined_operation(_Pos,Id,_Results,_Args,_RefinesID,Body),Id,Body).

get_raw_section(Sec,Body,Content) :- % look for Sec(_Pos,Content) in Body list
    functor(Pattern,Sec,2),arg(2,Pattern,Content),
    memberchk(Pattern,Body).

get_ref_type(includes,'[label=\"INCLUDES\",color=navyblue]',normal).

get_ref_type(imports,'[label=\"IMPORTS\",color=navyblue]',normal).

get_ref_type(extends,'[label=\"EXTENDS\",color=navyblue]',normal).

get_ref_type(uses,'[label=\"USES\",color=navyblue,style=dashed]',normal).

get_ref_type(sees,'[label=\"SEES\",color=navyblue,style=dashed]',normal).

get_ref_type(refines,'[label=\"REFINEMENT\",color=navyblue,style=bold]',reverse). % reverse so that abstract machines are shown on top

get_ref_type(UNKNOWN,'[label=\"UNKNOWN\",color=navyblue]',normal) :- add_internal_error('Unknown : ',get_ref_type(UNKNOWN,_,_)).

get_ref_type_name(includes,'INCLUDES').

get_ref_type_name(imports,'IMPORTS').

get_ref_type_name(extends,'EXTENDS').

get_ref_type_name(uses,'USES').

get_ref_type_name(sees,'SEES').

get_ref_type_name(refines,'REFINEMENT').

get_ref_type_name(main,'MACHINE').

get_ref_type_name(UNKNOWN,UNKNOWN).

get_references(Body,Refs) :-
    findrefs(Body,includes,Includes),
    findrefs(Body,extends,Extends),
    findrefs(Body,imports,Imports),
    findusessees(Body,uses,Uses),
    findusessees(Body,sees,Sees),
    append([Includes,Imports,Extends,Uses,Sees],Refs).

get_refinements([],[]).

get_refinements([Name|NRest],[ref(refines,Name,'')|RRest]) :-
    get_refinements(NRest,RRest).

get_sees_context_refs(Sections,SRefs) :-
    get_opt_section(sees,Sections,Seen),
    findall(ref(sees,I,''),member(I,Seen),SRefs).

get_sets(Body,Sets) :-
    get_opt_section(sets,Body,Sets).

get_values_id(values_entry(Pos,ID,_Val),identifier(Pos,ID)).

is_refinining_event(M,identifier(_,Event)) :- (refines_event(M,Event,_,_) -> true).

machine_has_constants(MachName) :-
    machine_identifiers(MachName,_,_,_,_,AConsts,CConsts),
    (AConsts=[] -> CConsts = [_|_] ; true).

machine_hash(Name,Hash) :-
    machine_hash_cached(Name,Hash1),!,Hash=Hash1.

machine_hash(Name,Hash) :-
    compute_machine_hash(Name,Hash1),
    assertz( machine_hash_cached(Name,Hash1) ),
    Hash=Hash1.

machine_name(Name) :- machine_type(Name,_).

maxlinelength(30).