1:- module(scasp_stack,
    2          [ justification_tree/3,		% :Stack, -JustTree, +Options
    3            print_justification_tree/1,         % :JustTree
    4            print_justification_tree/2,         % :JustTree, +Options
    5            unqualify_justitication_tree/3      % +TreeIn, +Module, -TreeOut
    6          ]).    7:- use_module(predicates).    8:- use_module(common).    9:- use_module(modules).   10:- use_module(output).   11
   12:- autoload(library(apply), [maplist/3]).   13:- autoload(library(lists), [reverse/2, append/3]).   14:- autoload(library(option),
   15            [option/2, merge_options/3, option/3, select_option/3]).   16
   17:- meta_predicate
   18    justification_tree(:, -, +),
   19    print_justification_tree(:),
   20    print_justification_tree(:, +).   21
   22:- multifile
   23    justification_tree_hook/2.   24
   25%!  justification_tree(:Stack, -JustificationTree, +Options)
   26%
   27%   Process Stack as produced by solve/4 into a justification tree.
   28%   Options include:
   29%
   30%      <none yet>
   31%
   32%   The `tree` format is defined as follows.
   33%
   34%     - The tree as a whole is module-qualified with the same
   35%       module as the input Stack.
   36%     - Each node takes the shape `Node-Children`, where `Node`
   37%       is an _atom_ (in the logical sense) and `Children` is
   38%       a (possibly empty) list of sub-trees that justify the
   39%       `Node`.
   40%     - Nodes (_atom_) may be wrapped in one or more of
   41%       - not(Node)
   42%         NAF negation
   43%       - -(Node)
   44%         Classical negation
   45%       - chs(Node)
   46%         Node was proven by co-induction ("it is assumed that ...")
   47%       - proved(Node)
   48%         Node was proven before ("justified above")
   49%       - assume(Node)
   50%         Node was assumed (matching chs(Node)).
   51%
   52%   The root node has the atom `query`  and has two children: the actual
   53%   query  and  the  atom  `o_nmr_check`  which  represents  the  global
   54%   constraints.
   55
   56:- det(justification_tree/3).   57
   58justification_tree(M:Stack, M:JustificationTree, Options) :-
   59    reverse(Stack, RevStack),
   60    stack_tree([query|RevStack], Trees),
   61    filter_tree(Trees, M, [JustificationTree], Options).
   62
   63%!  stack_tree(+Stack, -Tree) is det.
   64%
   65%   Translate the solver  Stack  into  a   tree.  The  solver  stack  is
   66%   represented as a flat list  of   proved  goals  where `[]` indicates
   67%   _this branch is complete_.  Here are some examples
   68%
   69%     [p, []]				p-[]
   70%     [p, q, [], []]			p-[q-[]]
   71%     [p, q, [], r, [], []]		p-[q-[],r-[]]
   72%
   73%     We maintain a stack of  difference  lists   in  the  4th  argument.
   74%     On encountering a `[]` we pop this stack.
   75
   76stack_tree(Stack, Tree) :-
   77    stack_tree(Stack, Tree, [], []).
   78
   79stack_tree([], Children0, Children, []) =>
   80    Children = Children0.
   81stack_tree([[]|Stack], Children0, Children, [T0/T|Parents]) =>
   82    Children = Children0,
   83    stack_tree(Stack, T0, T, Parents).
   84stack_tree([H|Stack], Tree, T, Parents) =>
   85    Tree = [H-Children|T0],
   86    stack_tree(Stack, Children, [], [T0/T|Parents]).
   87
   88
   89%!  filter_tree(+Children, +Module, -FilteredChildren, +Options)
   90%
   91%   Clean the tree from less  interesting   details.  By default removes
   92%   auxiliary nodes created as part of the compilation and the NMR proof
   93%   if this is empty. Additional filtering is based on Options:
   94%
   95%      - pos(true)
   96%        Remove all not(_) nodes from the tree.
   97
   98filter_tree([],_,[], _) :- !.
   99filter_tree([goal_origin(_,_)-[_,goal_origin(Abd, O)-_]|Cs],
  100            M,
  101            [goal_origin(abduced(Atom), O)-[]|Fs], Options) :-
  102    abduction_justification(Abd, Atom),
  103    !,
  104    filter_tree(Cs, M, Fs, Options).
  105filter_tree([proved(Abd)-[]|Cs],
  106            M,
  107            [proved(Atom)-[]|Fs], Options) :-
  108    abduction_justification(Abd, Atom),
  109    !,
  110    filter_tree(Cs, M, Fs, Options).
  111filter_tree([goal_origin(Term0,O)-Children|Cs], M, Tree, Options) :-
  112    filter_pos(Term0, Options),
  113    raise_negation(Term0, Term),
  114    selected(Term, M), !,
  115    filter_tree(Children, M, FChildren, Options),
  116    Tree = [goal_origin(Term, O)-FChildren|Fs],
  117    filter_tree(Cs, M, Fs, Options).
  118filter_tree([Term0-Children|Cs], M, Tree, Options) :-
  119    filter_pos(Term0, Options),
  120    raise_negation(Term0, Term),
  121    selected(Term, M), !,
  122    filter_tree(Children, M, FChildren, Options),
  123    (   Term == o_nmr_check, FChildren == []
  124    ->  Tree = Fs
  125    ;   Tree = [Term-FChildren|Fs]
  126    ),
  127    filter_tree(Cs, M, Fs, Options).
  128filter_tree([_-Childs|Cs], M, FilterChildren, Options) :-
  129    append(Childs, Cs, AllCs),
  130    filter_tree(AllCs, M, FilterChildren, Options).
  131
  132%!  filter_pos(+Node, +Options) is semidet.
  133%
  134%   Filter negated nodes when  ``--pos``  is   active.  We  should _not_
  135%   filter the global constraint nodes.
  136
  137filter_pos(not(GC), _Options), is_global_constraint(GC) =>
  138    true.
  139filter_pos(not(_), Options) =>
  140    \+ option(pos(true), Options).
  141filter_pos(_, _) =>
  142    true.
  143
  144selected(query, _) => true.
  145selected(proved(_), _) => true.
  146selected(chs(_), _) => true.
  147selected(assume(_), _) => true.
  148selected(not(-Goal), _) =>
  149    \+ aux_predicate(Goal).
  150selected(not(Goal), _) =>
  151    \+ aux_predicate(Goal).
  152selected(-(Goal), M) =>
  153    selected(Goal, M).
  154selected(findall(_,_,_), _) => true.
  155selected(is(_,_), _) => true.
  156selected(_>_, _) => true.
  157selected(_>=_, _) => true.
  158selected(_<_, _) => true.
  159selected(_=<_, _) => true.
  160selected(Goal, M) =>
  161    (   aux_predicate(Goal)
  162    ->  fail
  163    ;   (   current_predicate(M:pr_user_predicate/1)
  164        ->  user_predicate(M:Goal)
  165        ;   true
  166        )
  167    ->  true
  168    ;   is_global_constraint(Goal)
  169    ).
  170
  171aux_predicate(-(o_,_)) :- !.                    % copied from io.pl
  172aux_predicate(A) :-
  173    functor(A, Name, _Arity),
  174    sub_atom(Name, 0, _, _, o_),
  175    \+ is_global_constraint(Name).
  176
  177is_global_constraint(o_nmr_check) :-
  178    !.
  179is_global_constraint(Atom) :-
  180    atom(Atom),
  181    atom_concat(o_chk_, NA, Atom),
  182    atom_number(NA, _).
  183
  184
  185abduction_justification(Abd, Atom) :-
  186    Abd =.. [F, Atom],
  187    abduction_justification_(F).
  188
  189abduction_justification_(F) :-
  190    sub_atom(F, _, _, 0, 'abducible$'),
  191    !.
  192abduction_justification_(abducible).
  193
  194
  195%!  print_justification_tree(:Tree) is det.
  196%!  print_justification_tree(:Tree, +Options) is det.
  197%
  198%   Print the justification tree as  returned by justification_tree/3 or
  199%   scasp_justification/2. The tree is  printed   to  the current output
  200%   stream. Options:
  201%
  202%     - format(+Format)
  203%       One of `unicode` (default) or `ascii`.
  204%     - depth(+Integer)
  205%       Initial indentation (0)
  206%     - indent(+Integer)
  207%       Indent increment per level (3).
  208%     - full_stop(+Bool)
  209%       End the tree with a full stop and newline.  If `false`,
  210%       it ends with the last atom.
  211
  212print_justification_tree(Tree) :-
  213    print_justification_tree(Tree, []).
  214
  215:- det(print_justification_tree/2).  216
  217print_justification_tree(Tree, Options) :-
  218    justification_tree_hook(Tree, Options),
  219    !.
  220print_justification_tree(M:Tree, Options) :-
  221    merge_options(Options, [depth(0),module(M)], Options1),
  222    plain_output(Tree, Options1),
  223    (   option(full_stop(true), Options, true)
  224    ->  format(".~n", [])
  225    ;   true
  226    ).
  227
  228%!  plain_output(+FilterChildren, +Options)
  229
  230plain_output(goal_origin(Term, _)-Children, Options) :-
  231    !,
  232    plain_output(Term-Children, Options).
  233plain_output(Term-[], Options) :-
  234    !,
  235    option(depth(D), Options),
  236    Indent is D*3,
  237    nl_indent(Indent),
  238    term(Term, Options).
  239plain_output(Term-Children, Options) :-
  240    !,
  241    select_option(depth(D), Options, Options1),
  242    option(indent(Width), Options1, 3),
  243    Indent is D*Width,
  244    connector(implies, Conn, Options),
  245    nl_indent(Indent), term(Term, Options), format(" ~w",[Conn]),
  246    D1 is D+1,
  247    plain_output_children(Children, [depth(D1)|Options1]).
  248
  249nl_indent(Indent) :-
  250    format('~N~t~*|', [Indent]).
  251
  252plain_output_children([A,B|Rs], Options) :-
  253    !,
  254    plain_output(A, Options),
  255    connector(and, Conn, Options),
  256    format("~w",[Conn]),
  257    plain_output_children([B|Rs], Options).
  258plain_output_children([A], Options) :-
  259    !,
  260    plain_output(A, Options).
  261
  262%!  term(+Node, +Options) is det.
  263%
  264%   Print a, possibly annotated, stack atom.
  265
  266term(proved(Term), Options) =>
  267    term1(proved, Term, Options).
  268term(assume(Term), Options) =>
  269    term1(assume, Term, Options).
  270term(chs(Term), Options) =>
  271    term1(chs, Term, Options).
  272term(Term, Options) =>
  273    print_model_term(Term, Options).
  274
  275term1(Functor, Arg, Options) :-
  276    print_connector(Functor, Options),
  277    format('(', []),
  278    print_model_term(Arg, Options),
  279    format(')', []).
  280
  281%!  unqualify_justitication_tree(:TreeIn, +Module, -TreeOut) is det.
  282%
  283%   Unqualify the nodes in TreeIn, turning the nodes qualified to module
  284%   Module into plain nodes.
  285
  286:- det(unqualify_justitication_tree/3).  287
  288unqualify_justitication_tree(_:Tree0, Module, Tree) :-
  289    is_list(Tree0),
  290    !,
  291    maplist(unqualify_just(Module), Tree0, Tree).
  292unqualify_justitication_tree(_:Tree0, Module, Tree) :-
  293    unqualify_just(Module, Tree0, Tree).
  294
  295unqualify_just(M, Node0-Children0, Node-Children) :-
  296    unqualify_model_term(M, Node0, Node),
  297    maplist(unqualify_just(M), Children0, Children)