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%      - long(true)
   98%        Keep the full tree, including forall() and intermediate nodes.
   99
  100filter_tree(Tree, _, Tree, Options) :-
  101    option(long(true), Options), !.
  102filter_tree([],_,[], _) :- !.
  103filter_tree([goal_origin(Atom0,_)-[goal_origin(Abd, O)-_]|Cs],
  104            M,
  105            [goal_origin(abduced(Atom), O)-[]|Fs], Options) :-
  106    abduction_justification(Abd),
  107    !,
  108    raise_negation(Atom0, Atom),
  109    filter_tree(Cs, M, Fs, Options).
  110filter_tree([ proved(Atom0)-[],
  111              not(_Neg)-[ not(_) - [proved(not(Abd))-[]]]],
  112            _M,
  113            [abduced(Atom)-[]], _Options) :-
  114    abduction_justification(Abd),
  115    !,
  116    raise_negation(Atom0, Atom).
  117filter_tree([ not(Atom0)-[not(_Neg)-[proved(not(Abd))-[]]]],
  118            _M,
  119            [abduced(Atom)-[]], _Options) :-
  120    raise_negation(Atom0, Atom1),
  121    neg(Atom1, Atom),
  122    abduction_justification(Abd),
  123    !.
  124filter_tree([goal_origin(Term0,O)-Children|Cs], M, Tree, Options) :-
  125    filter_pos(Term0, Options),
  126    raise_negation(Term0, Term),
  127    selected(Term, M), !,
  128    filter_tree(Children, M, FChildren, Options),
  129    Tree = [goal_origin(Term, O)-FChildren|Fs],
  130    filter_tree(Cs, M, Fs, Options).
  131filter_tree([Term0-Children|Cs], M, Tree, Options) :-
  132    filter_pos(Term0, Options),
  133    raise_negation(Term0, Term),
  134    selected(Term, M), !,
  135    filter_tree(Children, M, FChildren, Options),
  136    (   Term == o_nmr_check, FChildren == []
  137    ->  Tree = Fs
  138    ;   Tree = [Term-FChildren|Fs]
  139    ),
  140    filter_tree(Cs, M, Fs, Options).
  141filter_tree([_-Childs|Cs], M, FilterChildren, Options) :-
  142    append(Childs, Cs, AllCs),
  143    filter_tree(AllCs, M, FilterChildren, Options).
  144
  145neg(-A, Neg) => Neg = A.
  146neg(A, Neg) => Neg = -A.
  147
  148%!  filter_pos(+Node, +Options) is semidet.
  149%
  150%   Filter negated nodes when  ``--pos``  is   active.  We  should _not_
  151%   filter the global constraint nodes.
  152
  153filter_pos(not(GC), _Options), is_global_constraint(GC) =>
  154    true.
  155filter_pos(not(_), Options) =>
  156    \+ option(pos(true), Options).
  157filter_pos(_, _) =>
  158    true.
  159
  160selected(query, _) => true.
  161selected(proved(_), _) => true.
  162selected(chs(_), _) => true.
  163selected(assume(_), _) => true.
  164selected(not(-Goal), _) =>
  165    \+ aux_predicate(Goal).
  166selected(not(Goal), _) =>
  167    \+ aux_predicate(Goal).
  168selected(-(Goal), M) =>
  169    selected(Goal, M).
  170selected(findall(_,_,_), _) => true.
  171selected(is(_,_), _) => true.
  172selected(_>_, _) => true.
  173selected(_>=_, _) => true.
  174selected(_<_, _) => true.
  175selected(_=<_, _) => true.
  176selected(Goal, M) =>
  177    (   aux_predicate(Goal)
  178    ->  fail
  179    ;   (   current_predicate(M:pr_user_predicate/1)
  180        ->  user_predicate(M:Goal)
  181        ;   true
  182        )
  183    ->  true
  184    ;   is_global_constraint(Goal)
  185    ).
  186
  187aux_predicate(-(o_,_)) :- !.                    % copied from io.pl
  188aux_predicate(A) :-
  189    functor(A, Name, _Arity),
  190    sub_atom(Name, 0, _, _, o_),
  191    \+ is_global_constraint(Name).
  192
  193is_global_constraint(o_nmr_check) :-
  194    !.
  195is_global_constraint(Atom) :-
  196    atom(Atom),
  197    atom_concat(o_chk_, NA, Atom),
  198    atom_number(NA, _).
  199
  200
  201abduction_justification(Abd) :-
  202    atom(Abd),
  203    sub_atom(Abd, _, _, _, ':abducible$'),
  204    !.
  205
  206
  207%!  print_justification_tree(:Tree) is det.
  208%!  print_justification_tree(:Tree, +Options) is det.
  209%
  210%   Print the justification tree as  returned by justification_tree/3 or
  211%   scasp_justification/2. The tree is  printed   to  the current output
  212%   stream. Options:
  213%
  214%     - format(+Format)
  215%       One of `unicode` (default) or `ascii`.
  216%     - depth(+Integer)
  217%       Initial indentation (0)
  218%     - indent(+Integer)
  219%       Indent increment per level (3).
  220%     - full_stop(+Bool)
  221%       End the tree with a full stop and newline.  If `false`,
  222%       it ends with the last atom.
  223
  224print_justification_tree(Tree) :-
  225    print_justification_tree(Tree, []).
  226
  227:- det(print_justification_tree/2).  228
  229print_justification_tree(Tree, Options) :-
  230    justification_tree_hook(Tree, Options),
  231    !.
  232print_justification_tree(M:Tree, Options) :-
  233    merge_options(Options, [depth(0),module(M)], Options1),
  234    plain_output(Tree, Options1),
  235    (   option(full_stop(true), Options, true)
  236    ->  format(".~n", [])
  237    ;   true
  238    ).
  239
  240%!  plain_output(+FilterChildren, +Options)
  241
  242plain_output(goal_origin(Term, _)-Children, Options) :-
  243    !,
  244    plain_output(Term-Children, Options).
  245plain_output(Term-[], Options) :-
  246    !,
  247    option(depth(D), Options),
  248    Indent is D*3,
  249    nl_indent(Indent),
  250    term(Term, Options).
  251plain_output(Term-Children, Options) :-
  252    !,
  253    select_option(depth(D), Options, Options1),
  254    option(indent(Width), Options1, 3),
  255    Indent is D*Width,
  256    connector(implies, Conn, Options),
  257    nl_indent(Indent), term(Term, Options), format(" ~w",[Conn]),
  258    D1 is D+1,
  259    plain_output_children(Children, [depth(D1)|Options1]).
  260
  261nl_indent(Indent) :-
  262    format('~N~t~*|', [Indent]).
  263
  264plain_output_children([A,B|Rs], Options) :-
  265    !,
  266    plain_output(A, Options),
  267    connector(and, Conn, Options),
  268    format("~w",[Conn]),
  269    plain_output_children([B|Rs], Options).
  270plain_output_children([A], Options) :-
  271    !,
  272    plain_output(A, Options).
  273
  274%!  term(+Node, +Options) is det.
  275%
  276%   Print a, possibly annotated, stack atom.
  277
  278term(proved(Term), Options) =>
  279    term1(proved, Term, Options).
  280term(assume(Term), Options) =>
  281    term1(assume, Term, Options).
  282term(chs(Term), Options) =>
  283    term1(chs, Term, Options).
  284term(Term, Options) =>
  285    print_model_term(Term, Options).
  286
  287term1(Functor, Arg, Options) :-
  288    print_connector(Functor, Options),
  289    format('(', []),
  290    print_model_term(Arg, Options),
  291    format(')', []).
  292
  293%!  unqualify_justitication_tree(:TreeIn, +Module, -TreeOut) is det.
  294%
  295%   Unqualify the nodes in TreeIn, turning the nodes qualified to module
  296%   Module into plain nodes.
  297
  298:- det(unqualify_justitication_tree/3).  299
  300unqualify_justitication_tree(_:Tree0, Module, Tree) :-
  301    is_list(Tree0),
  302    !,
  303    maplist(unqualify_just(Module), Tree0, Tree).
  304unqualify_justitication_tree(_:Tree0, Module, Tree) :-
  305    unqualify_just(Module, Tree0, Tree).
  306
  307unqualify_just(M, Node0-Children0, Node-Children) :-
  308    unqualify_model_term(M, Node0, Node),
  309    maplist(unqualify_just(M), Children0, Children)