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(prolog_prooftree, 36 [ proof_tree/2, % :Goal,-Tree 37 pt_children/2, % +Tree,-Children 38 pt_goal/2, % +Tree,-Goal 39 pt_clause/2 % +Tree,-ClauseRef 40 ]). 41:- use_module(library(assoc)). 42:- use_module(library(debug)). 43:- use_module(library(edinburgh)). 44:- use_module(library(lists)).
49:- meta_predicate
50 proof_tree(, ).g(Frame, Level, Goal, CRef, Complete, Children)
Here, Frame is the reference to the Prolog stack frame that ran the goal. This has no meaning to the user. Level is the nesting depth of the call, Goal is the executed goal as it is after the entire derivation succeeded, CRef is the clause that produced this answer, Complete is internal (means we have seen the "exit" port) and Children is a list of children in reverse order.
Re-satisfying re-satisfies Goal and on success Tree reflects the proof tree of the new answer.
69proof_tree(Goal, Tree) :- 70 notrace, 71 nodebug, 72 empty_assoc(Nodes), 73 b_setval(nodes, Nodes), 74 setup_call_cleanup( 75 asserta((user:prolog_trace_interception(Port, Frame, Choice, Action) :- 76 prolog_prooftree:trace_interception(Port, Frame, Choice, Action)), Ref), 77 ( b_setval(collecting, true), 78 setup_call_cleanup( 79 trace, 80 call(Goal), 81 nodebug), 82 b_setval(collecting, false) 83 ), 84 erase(Ref)), 85 b_getval(root, Tree). 86 87:- public trace_interception/4. 88trace_interception(call, Frame, _Choice, Action), 89 nb_current(collecting, true) => 90 Action = continue, 91 prolog_frame_attribute(Frame, goal, Goal), 92 prolog_frame_attribute(Frame, level, Level), 93 Node = g(Frame, Level, Goal, _CRef, _Complete, []), 94 debug(tree, 'Adding node ~p', [Node]), 95 ( parent_node(Frame, PNode) 96 -> add_child(PNode, Node) 97 ; b_getval(nodes, Nodes), 98 empty_assoc(Nodes) 99 -> debug(tree, 'Starting with root', []), 100 add_node(Node), 101 b_setval(root, Node) 102 ; debug(tree, 'Cannot connect ~p', [Node]) 103 ). 104trace_interception(exit, Frame, _Choice, Action), 105 nb_current(collecting, true) => 106 Action = continue, 107 ( node(Frame, Node) 108 -> ignore(prolog_frame_attribute(Frame, clause, CRef)), 109 complete(Node, CRef) 110 ; true 111 ). 112trace_interception(_Port, _Frame, _Choice, Action) => 113 Action = continue.
119parent_node(Frame, PNode) :- 120 b_getval(nodes, Nodes), 121 parent_frame(Frame, Parent), 122 get_assoc(Parent, Nodes, PNode), 123 !, 124 debug(tree, 'Got parent ~p', [PNode]). 125 126parent_frame(Frame, Parent) :- 127 prolog_frame_attribute(Frame, parent, Parent0), 128 parent_frame_(Parent0, Parent). 129 130parent_frame_(Frame, Frame). 131parent_frame_(Frame, Parent) :- 132 prolog_frame_attribute(Frame, parent, Parent0), 133 parent_frame_(Parent0, Parent).
140add_node(Node) :- 141 arg(1, Node, Frame), 142 b_getval(nodes, Nodes), 143 put_assoc(Frame, Nodes, Node, Nodes2), 144 b_setval(nodes, Nodes2). 145 146node(Frame, Node) :- 147 b_getval(nodes, Nodes), 148 get_assoc(Frame, Nodes, Node). 149 150add_child(Node, Child) :- 151 add_node(Child), 152 arg(6, Node, Children), 153 setarg(6, Node, [Child|Children]). 154 155complete(Node, CRef) :- 156 arg(4, Node, CRef), 157 arg(5, Node, true).
166pt_children(Tree, Children) :- 167 arg(6, Tree, Children0), 168 reverse(Children0, Children). 169 170pt_goal(Tree, Goal) :- 171 arg(3, Tree, Goal). 172 173pt_clause(Tree, CRef) :- 174 arg(4, Tree, CRef), 175 blob(CRef, clause)
Run goal and extract a proof tree
*/