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, '% ~w:~d~n', [File, Line]).
  159print_location(_).
  160
  161clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, Subst, State) :-
  162    State.get(factorize) == true, !,
  163    clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, Subst).
  164clause_factorized(Path, Goal, Children, FPath, FGoal, FChildren, [], _) :-
  165    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.

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

 nav_action(+Dict0, -Dict) is det

Read a command and return a new state.

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

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

Find a goal in the proof tree that matches Target.

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

 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.

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

 read_key(+Prompt, -Key) is det

Read the first character for the command.

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

 br_line

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

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