1/*  Part of SWI-Prolog
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        jan@swi-prolog.org
    5    WWW:           http://www.swi-prolog.org
    6    Copyright (c)  2023, SWI-Prolog Solutions b.v.
    7    All rights reserved.
    8
    9    Redistribution and use in source and binary forms, with or without
   10    modification, are permitted provided that the following conditions
   11    are met:
   12
   13    1. Redistributions of source code must retain the above copyright
   14       notice, this list of conditions and the following disclaimer.
   15
   16    2. Redistributions in binary form must reproduce the above copyright
   17       notice, this list of conditions and the following disclaimer in
   18       the documentation and/or other materials provided with the
   19       distribution.
   20
   21    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   22    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   23    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   24    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   25    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   26    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   27    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   28    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   29    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   30    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   31    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   32    POSSIBILITY OF SUCH DAMAGE.
   33*/
   34
   35:- module(dd_navigate,
   36          [ navigate/1        % +Tree
   37          ]).   38:- use_module(prooftree).   39:- autoload(library(ansi_term), [ansi_format/3]).   40:- autoload(library(apply), [foldl/4]).   41:- autoload(library(edit), [edit/1]).   42:- autoload(library(lists), [nth1/3, append/3]).

 navigate(+Tree) is semidet

Navigate a proof tree as produced by proof_tree/2. This is an interactive process. This predicate succeeds if the user hits q (quit) and fails to re-satisfy proof_tree/2 if the user hits n (next).

   54navigate(Tree) :-
   55    nav(#{tree:Tree, path:[], factorize:true}).
   56
   57nav(State) :-
   58    path_goals(State.path, State.tree, Path),
   59    sub_tree(State.path, State.tree, SubTree),
   60    print_node(Path, SubTree, State),
   61    nav_action(State, State1),
   62    (   State1.get(done) == true
   63    ->  true
   64    ;   State1.get(next) == true
   65    ->  fail
   66    ;   nav(State1)
   67    ).
   68
   69print_path([]) =>
   70    ansi_format(comment, '<root>~n', []).
   71print_path(Path) =>
   72    ansi_format(comment, 'Callers: ', []),
   73    print_path_(Path),
   74    nl(user_output).
   75
   76print_path_([]) =>
   77    true.
   78print_path_([n(I,N,G)|T]) =>
   79    ansi_format(code, '~p', [G]),
   80    (   N == 1
   81    ->  ansi_format(comment, ' <- ', [])
   82    ;   ansi_format(comment, ' [~d/~d] <- ', [I,N])
   83    ),
   84    print_path_(T).
   85
   86path_goals([], _, []).
   87path_goals([H|T], Tree, [n(H,NCh,G)|GT]) :-
   88    pt_goal(Tree, G),
   89    pt_children(Tree, Children),
   90    length(Children, NCh),
   91    nth1(H, Children, SubTree),
   92    path_goals(T, SubTree, GT).

 sub_tree(?Path, +Tree, -SubTree)

True when SubTree is a sub tree of Tree at the location defined by Path. Path is a list of integers, where each integer is an index into the list of children.

  100sub_tree([], Tree, Tree).
  101sub_tree([H|T], Tree, SubTree) :-
  102    pt_children(Tree, Children),
  103    nth1(H, Children, SubTree0),
  104    sub_tree(T, SubTree0, SubTree).

 print_node(+Path, +Tree, +State) is det

Print a location in the proof tree. The goal is the goal associated with Tree, which is a sub-tree of the entire tree. State is passed for settings.

  112print_node(Path, Tree, State) :-
  113    pt_goal(Tree, Goal),
  114    pt_children(Tree, Children0),
  115    maplist(pt_goal, Children0, Children),
  116    clause_factorized(Path, Goal,  Children,
  117                      FPath, FGoal, FChildren,
  118                      Subst, State),
  119    numbervars(v(FGoal,FChildren,FPath,Subst), 0, _,
  120               [singletons(true)]),
  121    br_line,
  122    print_path(FPath),
  123    print_location(Tree),
  124    (   Children == []
  125    ->  ansi_format(bold, '~p.~n', [FGoal])
  126    ;   ansi_format(bold, '~p :-~n', [FGoal]),
  127        length(Children, Count),
  128        foldl(print_body_goal(Count), FChildren, 1, _)
  129    ),
  130    (   Subst == []
  131    ->  true
  132    ;   ansi_format(comment, '% where~n', []),
  133        sort(Subst, Subst1),
  134        forall(member(Var = Value, Subst1),
  135               ansi_format(code, '~t~p = ~10|~p~n',
  136                           [Var,Value]))
  137    ).
  138
  139print_body_goal(Count, Goal, Nth, Nth1) =>
  140    Nth1 is Nth+1,
  141    ansi_format(comment, '~t[~d] ~8|', [Nth]),
  142    (   Nth == Count
  143    ->  Sep = '.'
  144    ;   Sep = ','
  145    ),
  146    ansi_format(code, '~p~w~n', [Goal, Sep]).

 print_location(+Tree)

If the goal associated to Tree is a Prolog predicate, print the clause location that resulted in this answer.

  153print_location(Tree) :-
  154    pt_clause(Tree, CRef),
  155    clause_property(CRef, file(File)),
  156    clause_property(CRef, line_count(Line)),
  157    !,
  158    ansi_format(comment, '% ', []),
  159    ansi_hyperlink(user_output, File:Line),
  160    nl(user_output).
  161print_location(_).
  162
  163clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, Subst, State) :-
  164    State.get(factorize) == true, !,
  165    clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, Subst).
  166clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, [], _) :-
  167    v(Path, Goal, Children) = v(FPath, FGoal, FChildren).

 clause_factorized(+Path, +Goal, +Children, -FPath, -FGoal, -FChildren, -Subst) is det

Factorize Goal and Children. We do not factorize goals or terms that are considered too small to be worth factorizing.

  175clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, Subst) :-
  176    term_factorized(v(Goal,Children,Path),
  177                    v(FGoal,FChildren,FPath), Subst0),
  178    rebind_small(Subst0, Subst1),
  179    rebind_goals([FGoal|FChildren], Subst1, Subst).
  180
  181rebind_small([], []).
  182rebind_small([Var=Value|T0], T) :-
  183    term_size(Value, Size),
  184    Size < 4,
  185    !,
  186    Var = Value,
  187    rebind_small(T0, T).
  188rebind_small([H|T0], [H|T]) :-
  189    rebind_small(T0, T).
  190
  191rebind_goals([], Subst, Subst).
  192rebind_goals([H0|T], Subst0, Subst) :-
  193    strip_module(H0, _, H),
  194    select(X=Value, Subst0, Subst1),
  195    X == H,
  196    !,
  197    H = Value,
  198    rebind_goals(T, Subst1, Subst).
  199rebind_goals([_|T], Subst0, Subst) :-
  200    rebind_goals(T, Subst0, Subst).

 nav_action(+Dict0, -Dict) is det

Read a command and return a new state.

  206nav_action(Dict0, Dict) :-
  207    read_command('Ddebug? ', Command),
  208    nav_action(Command, Dict0, Dict).
  209
  210nav_action(Command, Dict0, Dict),
  211    clause(path_op(Command, _, _), _) =>
  212    (   path_op(Command, Dict0.path, NewPath),
  213        Dict1 = Dict0.put(path, NewPath),
  214        sub_tree(Dict1.path, Dict1.tree, _)
  215    ->  Dict = Dict1
  216    ;   ansi_format(warning, 'No more (~w)~n', [Command]),
  217        nav_action(Dict0,Dict)
  218    ).
  219nav_action(find(Term), Dict0, Dict) =>
  220    find_goal(Term, Dict0, Dict).
  221nav_action(top, Dict0, Dict) =>
  222    Dict = Dict0.put(path, []).
  223nav_action(abort, _, _) =>
  224    abort.
  225nav_action(break, Dict0, Dict) =>
  226    break,
  227    nav_action(Dict0,Dict).
  228nav_action(quit, Dict0, Dict) =>
  229    Dict = Dict0.put(done, true).
  230nav_action(next, Dict0, Dict) =>
  231    Dict = Dict0.put(next, true).
  232nav_action(help, Dict0, Dict) =>
  233    help,
  234    nav_action(Dict0,Dict).
  235nav_action(edit, Dict0, Dict) =>
  236    sub_tree(Dict0.path, Dict0.tree, Tree),
  237    pt_clause(Tree, Clause),
  238    clause_property(Clause, file(File)),
  239    clause_property(Clause, line_count(Line)),
  240    edit(File:Line),
  241    nav_action(Dict0,Dict).
  242nav_action(listing, Dict0, Dict) =>
  243    sub_tree(Dict0.path, Dict0.tree, Tree),
  244    pt_clause(Tree, Clause),
  245    br_line,
  246    listing(Clause, [source(true)]),
  247    br_line,
  248    nav_action(Dict0,Dict).
  249nav_action(factorize, Dict0, Dict) =>
  250    negate(Dict0.factorize, New),
  251    Dict = Dict0.put(factorize, New),
  252    nav(Dict).
  253
  254negate(true, false).
  255negate(false, true).
  256
  257path_op(up, Path0, Path) :-
  258    append(Path, [_], Path0).
  259path_op(down, Path0, Path) :-
  260    append(Path0, [1], Path).
  261path_op(down(N), Path0, Path) :-
  262    append(Path0, [N], Path).
  263path_op(left, Path0, Path) :-
  264    append(Path1, [Here], Path0),
  265    Here1 is Here-1,
  266    append(Path1, [Here1], Path).
  267path_op(right, Path0, Path) :-
  268    append(Path1, [Here], Path0),
  269    Here1 is Here+1,
  270    append(Path1, [Here1], Path).

 find_goal(+Target:term, +State0, -State) is det

Find a goal in the proof tree that matches Target.

  276find_goal(Term, State0, State) :-
  277    sub_tree(State0.path, State0.tree, SubTree),
  278    findall(Path-Goal,
  279            (   sub_tree(Path, SubTree, Hit),
  280                pt_goal(Hit, Goal),
  281                goal_matches(Term, Goal)
  282            ), Pairs),
  283    (   Pairs == []
  284    ->  ansi_format(warning, 'No matching goals~n', []),
  285        nav_action(State0, State)
  286    ;   Pairs = [Path-_]
  287    ->  State = State0.put(path, Path)
  288    ;   sort(2, @>, Pairs, Sorted),
  289        length(Sorted, Hits),
  290        ansi_format(comment, 'Found ~D hits~n', [Hits]),
  291        forall(nth1(N, Sorted, Path-Goal),
  292               ( ansi_format(comment, '~t[~d]~8| ', [N]),
  293                 numbervars(Goal, 0, _, [singletons(true)]),
  294                 ansi_format(code, '~p~n', [Goal]))),
  295        (   ask_integer('Please select 1-~d? '-[Hits], 1-Hits, I)
  296        ->  nth1(I, Sorted, Path-_),
  297            State = State0.put(path, Path)
  298        ;   nav_action(State0, State)
  299        )
  300    ).
  301
  302goal_matches(Term, Goal) :-
  303    Term = Goal,
  304    !.
  305goal_matches(Atom, Goal0) :-
  306    strip_module(Goal0, _, Goal),
  307    atom(Atom),
  308    compound(Goal),
  309    compound_name_arity(Goal, Atom, _).
  310
  311
  312		 /*******************************
  313		 *         READ COMMANDS	*
  314		 *******************************/

 read_command(+Prompt, -Command) is det

Get a new command from the user.

bug

- Reading a line works poorly if with the prompt. Probably we should use prompt1/1.

  323read_command(Prompt, Command) :-
  324    read_key(Prompt, Key),
  325    (   key_command(Key, Command0, _Comment)
  326    ->  command_args(Command0, Command)
  327    ;   char_type(Key, digit(D))
  328    ->  Command = down(D),
  329        ansi_format(comment, '[~w]~n', [Command])
  330    ;   ansi_format(warning,
  331                    'Unknown command (? for help)~n', []),
  332        read_command(Prompt, Command)
  333    ).
  334
  335command_args(Command, Command) :-
  336    atom(Command), !,
  337    ansi_format(comment, '[~w]~n', [Command]).
  338command_args(Command0, Command) :-
  339    Command0 =.. [Name|Args0],
  340    ansi_format(code, '~w ~w? ', [Name, Args0]),
  341    flush_output(user_output),
  342    read_line_to_string(user_input, Line),
  343    split_string(Line, " \t", " \t", Args1),
  344    (   catch(maplist(convert_arg, Args0, Args1, Args), _, fail)
  345    ->  Command =.. [Name|Args]
  346    ;   ansi_format(warning, '~NInvalid arguments~n', []),
  347        command_args(Command0, Command)
  348    ).
  349
  350convert_arg(int, String, Int) =>
  351    number_string(Int, String).
  352convert_arg(term, String, Term) =>
  353    term_string(Term, String).
  354
  355key_command('?',   help,       "Help").
  356key_command(up,    up,         "Parent goal").
  357key_command(down,  down,       "First child").
  358key_command(left,  left,       "Previous sibling").
  359key_command(right, right,      "Next sibling").
  360key_command(k,     up,         "Parent goal"). % vi compatible bindings
  361key_command(j,     down,       "First child").
  362key_command(h,     left,       "Previous sibling").
  363key_command(l,     right,      "Next sibling").
  364key_command(d,     down(int),  "Down to Nth child").
  365key_command('1-9', down(int),  "Down to Nth child").
  366key_command(t,     top,        "Go to the top").
  367key_command('/',   find(term), "Find goal (below current)").
  368key_command(e,     edit,       "Edit").
  369key_command('L',   listing,    "Listing").
  370key_command('F',   factorize,  "Toggle factorization").
  371key_command(q,     quit,       "Quit").
  372key_command(a,     abort,      "Abort").
  373key_command(b,     break,      "Run nested toplevel").
  374key_command(n,     next,       "Next answer").
  375
  376ask_integer(Fmt-Args, Low-High, Int) :-
  377    High =< 9,
  378    !,
  379    ansi_format(bold, Fmt, Args),
  380    flush_output(user_output),
  381    get_single_char(X),
  382    code_type(X, digit(Int)),
  383    between(Low, High, Int).
  384ask_integer(Fmt-Args, Low-High, Int) :-
  385    ansi_format(bold, Fmt, Args),
  386    flush_output(user_output),
  387    read_line_to_string(user_input, Line),
  388    number_string(Int, Line),
  389    between(Low, High, Int).
  390
  391help :-
  392    findall(Command, key_command(_, Command, _Comment), Commands0),
  393    list_to_set(Commands0, Commands),
  394    forall((   member(Command, Commands),
  395               once(key_command(_, Command, Comment)),
  396               findall(Key, key_command(Key, Command, _), Keys)
  397           ),
  398           (   atomics_to_string(Keys, ',', KeysS),
  399               ansi_format(comment, '% ~w~t~20|~w~n',
  400                           [KeysS, Comment]))).

 read_key(+Prompt, -Key) is det

Read the first character for the command.

  406read_key(Prompt, Key) :-
  407    ansi_format(bold, '~w', [Prompt]),
  408    flush_output(user_output),
  409    with_tty_raw(read_key_(Key, [])).
  410
  411read_key_(Key, Sofar) :-
  412    get_code(Code),
  413    append(Sofar, [Code|T], Codes),
  414    (   key_code(Key0, Codes)
  415    ->  (   T == []
  416        ->  Key = Key0
  417        ;   append(Sofar, [Code], Sofar1),
  418            read_key_(Key, Sofar1)
  419        )
  420    ;   char_code(Key, Code)
  421    ).
  422
  423key_code(up,    `\e[A`).
  424key_code(down,  `\e[B`).
  425key_code(left,  `\e[D`).
  426key_code(right, `\e[C`).

 br_line

Print a line (`<br>`) accross the screen using Unicode.

  432br_line :-
  433    tty_width(Width),
  434    format('~N~`\u2015t~*|~n', [Width]).
  435
  436tty_width(W) :-
  437    catch(tty_size(_, TtyW), _, fail),
  438    !,
  439    W is max(60, TtyW - 8).
  440tty_width(60)