state_graph_canon

emptyset([]).

expand_data_value(DataValue,S1) :-
    (is_custom_explicit_set(DataValue,expand_data_value)
    -> try_expand_custom_set_with_catch(DataValue,S1,expand_data_value)
    ; DataValue=S1
).

gen_relation(S1,VariableName,NewTransitions) :-
    (S1=[H|_],is_pair_to_pair(H) -> MatchTriples=false ; MatchTriples=true),
    grelation(S1,MatchTriples,sg_root,VariableName,[],NewTransitions).

get_abstract_node_type_colour([],C) :- !,C=1.

get_abstract_node_type_colour([H|_],C) :- !, get_abstract_node_type_colour(H,CH),
    C is CH+1.

get_abstract_node_type_colour((A,_),C) :- !, get_abstract_node_type_colour(A,CH),
    C is CH+1.

get_abstract_node_type_colour(_,0).

grelation([],_,_,_,F,F).

grelation([(E0,E1,E2)|T],true,Parent,VariableName,F,Fi) :-
    % interpret E0 as label for string; note: (E0,E1,E2) matches ((A,B),(C,D))
    generate_state_for_dot,
    simple_value(E0),
    !,
    translate_inner_node(E1,C1,E1_NewTransitions),
    translate_inner_node(E2,C2,E2_NewTransitions),
    translate_bvalue_for_dot(E0,E0String),
    Label =.. [VariableName,E0String],
    append([E2_NewTransitions,[(C1,Label,C2)|E1_NewTransitions],F],F6),
    grelation(T,true,Parent,VariableName,F6,Fi).

grelation([(E1,E2)|T],MatchTriples,Parent,VariableName,F,Fi) :-
    translate_inner_node(E1,C1,E1_NewTransitions),
    translate_inner_node(E2,C2,E2_NewTransitions),
    append([E2_NewTransitions,[(C1,VariableName,C2)|E1_NewTransitions],F],F6),
    grelation(T,MatchTriples,Parent,VariableName,F6,Fi).

gset([],_,_,F,F).

gset([S1|T],Parent,TransitionLabel,F,Fi) :-
    translate_inner_node(S1,C1,S1_NewTransitions),
    append([(C1,TransitionLabel,Parent)|S1_NewTransitions],F,F4),
    gset(T,Parent,TransitionLabel,F4,Fi).

is_pair_to_pair(((A,B),(C,D))) :-
    infer_value_type(A,T1), infer_value_type(C,T1),
    infer_value_type(B,T2), infer_value_type(D,T2).

list_set([]).

list_set([_|_]).

new_sg_node(Value,abs_cn(J,NestingCol)) :- retract(cn(I)), J is I+1,
    asserta(cn(J)),
    get_abstract_node_type_colour(Value,NestingCol),
    assertz(cn_value(Value,abs_cn(J,NestingCol))).

relation([(_,_)|_]).

relation([(X,_,_)|_]) :- generate_state_for_dot, simple_value(X). % TO DO: check if it is a function ?; maybe also support other nested ternary relations

reset_n :-
    retractall(cn(_)),retractall(cn_value(_,_)),asserta(cn(0)).

simple_pair_value((A,B)) :- !,simple_pair_value(A), simple_pair_value(B).

simple_pair_value(X) :- simple_value(X).

simple_value(X) :- atomic(X).

simple_value(int(_)).

simple_value(fd(_,_)).

simple_value(string(_)).

simple_value(pred_false).

simple_value(pred_true).

state_graph(root,R) :- !,R=[].

state_graph(concrete_constants(C),SG) :- !, state_graph(C,SG).

state_graph(const_and_vars(ConstID,S),SG) :- !,
    expand_const_and_vars(ConstID,S,Full),
    reset_n,
    state_graph(Full,[],SG).

state_graph(S,SG) :-
    reset_n,
    state_graph(S,[],SG).

state_graph([],Final,Final).

state_graph([bind(VarName,Value)|T],C,F) :-
    tools:string_escape(VarName,EscVarName),
    (top_level_translate_node(Value,EscVarName,PG) -> true
    %print(translate(Value,VarName,PG)),nl
    ; add_error(state_graph,'Call failed: ',top_level_translate_node(Value,VarName,PG))),
    append(PG,C,C2),
    state_graph(T,C2,F).

state_graph_for_dot(State,R) :-
    assertz(generate_state_for_dot),
    call_cleanup(state_graph(State,R), retract(generate_state_for_dot)).

top_level_translate_node(DataValue,VariableName,NewTransitions) :-
    % Input: DataValue
    % Output: NewTransitions required to represent the structure
    % In contrast to translate_inner_node, we do not generate new inner artificial nodes;
    % VariableName is used as an arc-label to encode the top-level information
    expand_data_value(DataValue,S1),
    % check whether S1 is a relation/atom/set
    ( relation(S1) -> gen_relation(S1,VariableName,NewTransitions)
    ; emptyset(S1) -> NewTransitions = [(sg_root,VariableName,sg_root)]
    %% [('$Empty_Set',VariableName,sg_root)] has problems as we cannot distinguish between v={} and v={{}}
    %% [] has problems when we have set_up_constants and variables which are all initialised with
    %% the empty set: then we get confused between set_up_constants & initialise_machine
    ; list_set(S1) -> gset(S1,sg_root,VariableName,[],NewTransitions)
    ; S1=(P1,P2) -> % a pair
    translate_inner_node(P1,Node1,NewTrans1),
    translate_inner_node(P2,Node2,NewTrans2),
    append([(Node1,VariableName,Node2)|NewTrans1],NewTrans2,NewTransitions)
    ; % an atom
    NewTransitions = [(DataValue,VariableName,sg_root)]
).

translate_inner_node(DataValue,NodeinGraph,NewTransitions) :- %% print(trans(DataValue)),nl,
    % Input: DataValue
    % Output: NodeinGraph representing DataValue + NewTransitions required to represent the structure
    (get_preference(dot_state_graph_decompose,false) -> % treat as an atom
    NewTransitions = [], NodeinGraph = DataValue
    ; expand_data_value(DataValue,S1),
    % check whether S1 is a atom/set
    ( emptyset(S1) -> NodeinGraph = [], %'$Empty_Set',
    NewTransitions=[]
    ; cn_value(S1,NodeinGraph) -> NewTransitions=[]
    ; simple_pair_value(S1),generate_state_for_dot -> NodeinGraph=S1, NewTransitions=[]
    ; list_set(S1) ->
    new_sg_node(S1,NodeinGraph),
    gset(S1,NodeinGraph,'$to_el',[],NewTransitions) % use the $to_el label to encode membership, using ':' would be more readable; but less efficient for symmetry (extra layers required)
    ; S1=(P1,P2)
    -> % a complex pair
    translate_inner_node(P1,Node1,NewTrans1),
    translate_inner_node(P2,Node2,NewTrans2),
    new_sg_node(S1,NodeinGraph),
    append([(NodeinGraph,'$from',Node1),
    (NodeinGraph,'$to_el',Node2)|NewTrans1],NewTrans2,NewTransitions)
    ; % an atom
    NewTransitions = [],
    NodeinGraph = S1
)
).