34
35:- module(dd_navigate,
36 [ navigate/1 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]).
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).
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).
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]).
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).
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).
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).
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
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"). 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]))).
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`).
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)
Interactively navigate a proof tree
*/