| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2025-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(sequent_prover_exports,[generate_proof_tree_graph/1, generate_proof_tree_graph/3, | |
| 6 | generate_proof_html_export/2]). | |
| 7 | ||
| 8 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 9 | :- module_info(group,sequent_prover). | |
| 10 | :- module_info(description,'This module provides export functionality for traces created by the sequent_prover.'). | |
| 11 | ||
| 12 | :- use_module(library(lists)). | |
| 13 | :- use_module(library(aggregate),[forall/2]). | |
| 14 | ||
| 15 | :- use_module(probsrc(error_manager)). | |
| 16 | :- use_module(probsrc(gensym),[gensym/2]). | |
| 17 | :- use_module(probsrc(specfile), [animation_minor_mode/1,get_operation_description_for_transition_id/3]). | |
| 18 | :- use_module(probsrc(state_space),[get_state_id_trace/1,history/1,op_trace_ids/1,transition/4,visited_expression/2]). | |
| 19 | :- use_module(probsrc(tools), [ajoin/2,ajoin_with_sep/3,read_string_from_file/2]). | |
| 20 | ||
| 21 | :- use_module(sequent_prover, [cont_length/2,get_continuations/2,translate_term/2]). | |
| 22 | ||
| 23 | ||
| 24 | %%%%%%%%% BUILD THE PROOF TREE %%%%%%%%% | |
| 25 | :- dynamic proof_node/3, proof_edge/4, proof_tree/2. | |
| 26 | % proof_node(ContinuationId,sequent(Hyps,Goal),DotAttrList). | |
| 27 | % proof_edge(PrevId,DestId,TransId,Label). | |
| 28 | :- dynamic current_node/1, continuation/2. % auxiliary predicates used during proof tree generation | |
| 29 | % continuation(ContinuationSequent,IdWhereThisContinuationWasAdded). | |
| 30 | ||
| 31 | build_proof_tree(StateIds,TransIds) :- proof_tree(StateIds,TransIds), !. % proof tree already created | |
| 32 | build_proof_tree(StateIds,TransIds) :- | |
| 33 | retractall(proof_node(_,_,_)), | |
| 34 | retractall(proof_edge(_,_,_,_)), | |
| 35 | retractall(proof_tree(_,_)), | |
| 36 | retractall(continuation(_,_)), | |
| 37 | retractall(current_node(_)), | |
| 38 | build_proof_tree_aux(StateIds,TransIds), | |
| 39 | assertz(proof_tree(StateIds,TransIds)). | |
| 40 | ||
| 41 | build_proof_tree_aux([],_). | |
| 42 | build_proof_tree_aux([_StateId],_). | |
| 43 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 44 | transition(PrevId,Act,TransId,StateId), | |
| 45 | Act=skip_to_cont, !, % ignore skips (just a reordering of continuations, not visible in the proof tree) | |
| 46 | build_proof_tree_aux([StateId|ST],TT). | |
| 47 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 48 | transition(PrevId,Act,TransId,StateId), | |
| 49 | visited_expression(StateId,State), | |
| 50 | State=state(success(SNr),_), !, % proof succeeded | |
| 51 | (current_node(PrevNode) -> true ; PrevNode=root), | |
| 52 | (get_operation_description_for_transition_id(PrevId,TransId,EdgeLabel) -> true ; EdgeLabel=Act), | |
| 53 | assert_node_with_edge(PrevNode,success(SNr),TransId,[shape/triangle,style/filled,fillcolor/'#99BF38'],EdgeLabel,GenID), | |
| 54 | set_current_node(GenID), | |
| 55 | build_proof_tree_aux([StateId|ST],TT). | |
| 56 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 57 | transition(PrevId,Act,TransId,StateId), % TODO: is there a way to obtain this directly from the history? | |
| 58 | visited_expression(PrevId,PrevState), visited_expression(StateId,state(Sequent,_)), | |
| 59 | (PrevState=state(PrevSequent,_) | |
| 60 | -> PrevSequent=sequent(PVHyps,PVGoal,_), cont_length(PrevSequent,PrevLen) | |
| 61 | ; PrevState=root, PrevLen=0), | |
| 62 | Sequent=sequent(Hyps,Goal,_), | |
| 63 | ||
| 64 | (retract(continuation(sequent(PVHyps,PVGoal),ContID)) % previous sequent has been registered as continuation before | |
| 65 | -> PrevNode=ContID | |
| 66 | ; (current_node(PrevNode) -> true ; PrevNode=root)), | |
| 67 | ||
| 68 | (get_operation_description_for_transition_id(PrevId,TransId,EdgeLabel) -> true ; EdgeLabel=Act), | |
| 69 | ||
| 70 | cont_length(Sequent,Len), | |
| 71 | (PrevLen>Len % sequent has been proven by the current transition and disappeared | |
| 72 | -> assert_node_with_edge(PrevNode,success(-1),TransId,[shape/triangle,style/filled,fillcolor/'#99BF38'],EdgeLabel,_GenID) | |
| 73 | ; assert_node_with_edge(PrevNode,sequent(Hyps,Goal),TransId,[shape/box],EdgeLabel,GenID), | |
| 74 | assertz(continuation(sequent(Hyps,Goal),GenID)), % store position of current node | |
| 75 | set_current_node(GenID) | |
| 76 | ), | |
| 77 | ||
| 78 | get_continuations(Sequent,Conts), | |
| 79 | forall(member(Cont,Conts),assert_new_continuation(Cont,PrevNode,TransId,EdgeLabel)), | |
| 80 | build_proof_tree_aux([StateId|ST],TT). | |
| 81 | ||
| 82 | assert_node_with_edge(PrevNode,Sequent,TransId,NodeAttr,EdgeLabel,GenID) :- | |
| 83 | gensym('seq_prov_',GenID), | |
| 84 | assertz(proof_node(GenID,Sequent,NodeAttr)), | |
| 85 | assertz(proof_edge(PrevNode,GenID,TransId,EdgeLabel)). | |
| 86 | ||
| 87 | assert_new_continuation(Cont,_,_,_) :- | |
| 88 | continuation(Cont,_ID), !. % is already registered | |
| 89 | % TODO: what happens if the same continuation occurs more than once? | |
| 90 | assert_new_continuation(Cont,PrevNode,TransId,EdgeLabel) :- | |
| 91 | assert_node_with_edge(PrevNode,Cont,TransId,[shape/box],EdgeLabel,CID), | |
| 92 | assertz(continuation(Cont,CID)). | |
| 93 | ||
| 94 | set_current_node(ID) :- | |
| 95 | retractall(current_node(_)), | |
| 96 | assertz(current_node(ID)). | |
| 97 | ||
| 98 | %%%%%%%%% END BUILD THE PROOF TREE %%%%%%%%% | |
| 99 | ||
| 100 | %%%%%%%%% HELPER PREDICATES FOR SEQUENT_PROVER STATES %%%%%%%%% | |
| 101 | pretty_hyps(sequent(Hyps,_),PHyps) :- maplist(translate_term,Hyps,PHyps). | |
| 102 | pretty_goal(sequent(_,Goal),PGoal) :- translate_term(Goal,PGoal). | |
| 103 | ||
| 104 | ||
| 105 | %%%%%%%%% BEGIN PROOF TREE DOT GRAPH %%%%%%%%% | |
| 106 | :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3,use_new_dot_attr_pred/7]). | |
| 107 | generate_proof_tree_graph(File) :- | |
| 108 | get_state_id_trace(StateIds), | |
| 109 | op_trace_ids(TransIds), | |
| 110 | reverse(TransIds,RTransIds), | |
| 111 | generate_proof_tree_graph(File,StateIds,RTransIds). | |
| 112 | generate_proof_tree_graph(File,StateIds,TransIds) :- | |
| 113 | (animation_minor_mode(sequent_prover) -> true | |
| 114 | ; add_error_and_fail(sequent_prover_exports,'Cannot create proof tree visualisation, not in sequent prover mode (load a .pl PO file exported by the ProB Rodin Plugin)','')), | |
| 115 | build_proof_tree(StateIds,TransIds), | |
| 116 | gen_dot_graph(File, | |
| 117 | use_new_dot_attr_pred(sequent_prover_exports:proof_tree_graph_node_predicate), | |
| 118 | use_new_dot_attr_pred(sequent_prover_exports:proof_tree_graph_trans_predicate)). | |
| 119 | ||
| 120 | :- public proof_tree_graph_node_predicate/3. | |
| 121 | proof_tree_graph_node_predicate(root,none,[shape/invtriangle,label/'Select PO']). | |
| 122 | proof_tree_graph_node_predicate(NodeId,none,[id/NodeId,color/'#99BF38',label/'Proven.'|Attr]) :- | |
| 123 | proof_node(NodeId,success(_),Attr). | |
| 124 | proof_tree_graph_node_predicate(NodeId,none,[id/NodeId,color/'#99BF38',label/htmllabel(Label)|Attr]) :- | |
| 125 | proof_node(NodeId,Sequent,Attr), | |
| 126 | Sequent\=success(_), NodeId\=root, | |
| 127 | (proof_edge(PrevNode,NodeId,_,_), proof_node(PrevNode,PrevSequent,_) | |
| 128 | -> true | |
| 129 | ; PrevSequent=Sequent), % highlight no changes | |
| 130 | build_html_dot_label(PrevSequent,Sequent,Label). | |
| 131 | ||
| 132 | build_html_dot_label(PrevSequent,Sequent,Label) :- | |
| 133 | pretty_hyps(PrevSequent,PPrevHyps), pretty_hyps(Sequent,PHyps), | |
| 134 | pred_changed(PHyps,PPrevHyps,ChangedPHyps), | |
| 135 | (ChangedPHyps=[] | |
| 136 | -> HypLabel='<TR><TD><FONT COLOR="grey"><I>no hypotheses</I></FONT></TD></TR>' % no hyps | |
| 137 | ; maplist(label_for_pred,ChangedPHyps,HypLabels), | |
| 138 | ajoin(HypLabels,HypLabel)), | |
| 139 | pretty_goal(PrevSequent,PPrevGoal), pretty_goal(Sequent,PGoal), | |
| 140 | (PPrevGoal=PGoal -> Changed=not_changed; Changed=changed), | |
| 141 | label_for_pred(pred_line(PGoal,Changed),GoalLabel), | |
| 142 | ajoin(['<<TABLE BORDER="0" CELLBORDER="0" COLOR="black">', HypLabel, '<HR/>', GoalLabel, '</TABLE>>'],Label). | |
| 143 | ||
| 144 | label_for_pred(pred_line(Pred,Changed),PredLabel) :- | |
| 145 | tools:html_escape(Pred,EPred), | |
| 146 | (Changed=changed | |
| 147 | -> ajoin(['<TR><TD ALIGN="LEFT"><FONT COLOR="#de8000"><B>',EPred,'</B></FONT></TD></TR>'],PredLabel) | |
| 148 | ; ajoin(['<TR><TD ALIGN="LEFT"><FONT COLOR="black">',EPred,'</FONT></TD></TR>'],PredLabel) | |
| 149 | ). | |
| 150 | ||
| 151 | pred_changed([],_,[]). | |
| 152 | pred_changed([Hyp|HT],[],[pred_line(Hyp,not_changed)|RT]) :- pred_changed(HT,[],RT). | |
| 153 | pred_changed([Hyp|HT],PrevHyps,[pred_line(Hyp,Changed)|RT]) :- | |
| 154 | (selectchk(Hyp,PrevHyps,NPrevHyps) | |
| 155 | -> Changed=not_changed | |
| 156 | ; Changed=changed, NPrevHyps=PrevHyps), | |
| 157 | pred_changed(HT,NPrevHyps,RT). | |
| 158 | ||
| 159 | :- public proof_tree_graph_trans_predicate/3. | |
| 160 | proof_tree_graph_trans_predicate(PrevId,SuccId,[label/Label]) :- | |
| 161 | proof_edge(PrevId,SuccId,_TransId,Label). | |
| 162 | %%%%%%%%% END PROOF TREE DOT GRAPH %%%%%%%%% | |
| 163 | ||
| 164 | %%%%%%%%% BEGIN PROOF TREE HTML EXPORT %%%%%%%%% | |
| 165 | :- dynamic proof_html_export_template_file_codes/2. | |
| 166 | ||
| 167 | assert_from_template(Filename) :- | |
| 168 | absolute_file_name(seqproversrc(Filename), Absolute, []), | |
| 169 | read_string_from_file(Absolute,String), | |
| 170 | assertz(proof_html_export_template_file_codes(Filename,String)). | |
| 171 | ||
| 172 | write_proof_html_export_template(HtmlFile,Stream) :- | |
| 173 | proof_html_export_template_file_codes(HtmlFile,Codes), | |
| 174 | format(Stream,'~s~n',[Codes]). | |
| 175 | ||
| 176 | :- assert_from_template('proof_html_export_header.html'). | |
| 177 | :- assert_from_template('proof_html_export_footer.html'). | |
| 178 | ||
| 179 | % TODO: maybe highlight selected step in SVG; allow to select a step by clicking in the proof tree | |
| 180 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 181 | :- use_module(probsrc(xtl_interface),[xtl_main_file_name/1]). | |
| 182 | generate_proof_html_export(File) :- | |
| 183 | get_state_id_trace(StateIds), | |
| 184 | op_trace_ids(TransIds), | |
| 185 | reverse(TransIds,RTransIds), | |
| 186 | generate_proof_html_export(File,StateIds,RTransIds). | |
| 187 | generate_proof_html_export(File,StateIds,TransIds) :- | |
| 188 | (animation_minor_mode(sequent_prover) -> true | |
| 189 | ; add_error_and_fail(sequent_prover_exports,'Cannot create proof export, not in sequent prover mode (load a .pl PO file exported by the ProB Rodin Plugin)','')), | |
| 190 | build_proof_tree(StateIds,TransIds), % important for step_list | |
| 191 | retractall(trans_id_done(_)), | |
| 192 | retractall(html_step_nr(_)), | |
| 193 | assertz(html_step_nr(1)), | |
| 194 | ||
| 195 | tools_io:safe_open_file(File,write,Stream,[encoding(utf8)]), | |
| 196 | write_proof_html_export_template('proof_html_export_header.html',Stream), | |
| 197 | xtl_main_file_name(POFile), | |
| 198 | (proof_edge(root,_,_,POLabel) | |
| 199 | -> format(Stream,' <div>Proof Trace Export for <b>~w</b> from <pre>~w</pre></div>~n',[POLabel,POFile]) | |
| 200 | ; format(Stream,' <div>Proof Trace Export from ~w</div>~n',[POFile])), | |
| 201 | format(Stream,' <hr/>~n',[]), | |
| 202 | format(Stream,' <div id="boxContainer" style="display: flex; width: 100%; position:fixed;">~n',[]), | |
| 203 | format(Stream,' <div id="stepListBox" style="width: 30%;">~n',[]), | |
| 204 | gen_step_list(Stream,TransIds), | |
| 205 | format(Stream,' </div>~n',[]), | |
| 206 | format(Stream,' <div id="divider" class="divider"> </div>~n',[]), | |
| 207 | format(Stream,' <div id="treeBox" style="width: 66.5%; height: 87vh; margin-left: 31%; position: fixed;">~n',[]), | |
| 208 | format(Stream,' <div class="box-caption">Proof Tree</div>~n',[]), | |
| 209 | format(Stream,' <div text-align="left" id="proof_tree_svg_outer_container" class="svg-outer-container">~n',[]), | |
| 210 | format(Stream,' <div text-align="left" id="proof_tree_svg_inner_container" class="svg-inner-container">~n',[]), | |
| 211 | write_proof_tree_svg_to_stream(Stream,StateIds,TransIds), % generate proof tree dot graph (with ProB dot preferences) | |
| 212 | format(Stream,' </div>~n',[]), | |
| 213 | format(Stream,' </div>~n',[]), | |
| 214 | format(Stream,' <button id="btnResetScale" class="visualisation-button" onclick="resetScale()">Reset View</button>~n',[]), | |
| 215 | format(Stream,' </div>~n',[]), % close tree box | |
| 216 | format(Stream,' </div>~n',[]), % close box container | |
| 217 | write_proof_html_export_template('proof_html_export_footer.html',Stream), | |
| 218 | close(Stream). | |
| 219 | ||
| 220 | :- use_module(probsrc(system_call),[get_temporary_filename/2]). | |
| 221 | :- use_module(probsrc(tools_io),[write_file_to_stream/2]). | |
| 222 | write_proof_tree_svg_to_stream(Stream,StateIds,TransIds) :- | |
| 223 | get_temporary_filename('_dot_proof_tree.dot',DotFile), | |
| 224 | get_temporary_filename('_dot_proof_tree.svg',SvgFile), | |
| 225 | generate_proof_tree_graph(DotFile,StateIds,TransIds), | |
| 226 | tools_commands:gen_dot_output(DotFile,dot,svg,SvgFile), | |
| 227 | write_file_to_stream(SvgFile,Stream). | |
| 228 | ||
| 229 | :- dynamic trans_id_done/1, html_step_nr/1. | |
| 230 | gen_step_list(Stream,TransIds) :- | |
| 231 | format(Stream,' <div class="box-caption" style="display: flex; justify-content: space-between;">Proof Steps~n',[]), | |
| 232 | format(Stream,' <div>~n',[]), | |
| 233 | format(Stream,' <button class="step-button" onclick="selectPrevStep()">< Previous Step</button>~n',[]), | |
| 234 | format(Stream,' <button class="step-button" onclick="selectNextStep()">Next Step ></button>~n',[]), | |
| 235 | format(Stream,' <button class="step-button" onclick="runAll()">Run Steps</button>~n',[]), | |
| 236 | format(Stream,' </div>~n',[]), | |
| 237 | format(Stream,' </div>~n',[]), | |
| 238 | format(Stream,' <div class="step-list">~n',[]), | |
| 239 | gen_step_list_entry(Stream,TransIds), | |
| 240 | format(Stream,' </div>~n',[]). | |
| 241 | gen_step_list_entry(Stream,TransIds) :- | |
| 242 | member(TransId,TransIds), | |
| 243 | proof_edge(PrevId,_Id,TransId,Label), | |
| 244 | \+ PrevId=root, | |
| 245 | \+ trans_id_done(TransId), | |
| 246 | findall(Id,proof_edge(_,Id,TransId,_),SuccIds), | |
| 247 | ajoin_with_sep([PrevId|SuccIds],'\',\'',IDList), | |
| 248 | format(Stream,' <div class="step-header green" onclick="focusSequents(\'trans_~w\',[\'~w\'])">~n',[TransId,IDList]), | |
| 249 | retract(html_step_nr(SNr)), | |
| 250 | NSNr is SNr+1, | |
| 251 | assertz(html_step_nr(NSNr)), | |
| 252 | format(Stream,' <b>~w. ~w</b>~n',[SNr,Label]), | |
| 253 | format(Stream,' </div>~n',[]), | |
| 254 | % TODO: here we could display more proof step details in the table (then an icon for extended/not-extended would be nice): | |
| 255 | format(Stream,' <div class="step-content" id="trans_~w">~n',[TransId]), | |
| 256 | % format(Stream,' <b>_TODO_</b>~n',[]), | |
| 257 | format(Stream,' </div>~n',[]), | |
| 258 | assertz(trans_id_done(TransId)), | |
| 259 | fail. | |
| 260 | gen_step_list_entry(_,_). | |
| 261 | %%%%%%%%% END PROOF TREE HTML EXPORT %%%%%%%%% |