| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2025-2026 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,[export_proof_for_current_state/2, export_proof/4, | |
| 6 | pretty_print_pos/1]). | |
| 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 | :- meta_predicate with_forced_rodin_mode(0). | |
| 16 | ||
| 17 | :- use_module(probsrc(error_manager)). | |
| 18 | :- use_module(probsrc(gensym),[gensym/2]). | |
| 19 | :- use_module(probsrc(specfile),[animation_minor_mode/1,get_operation_description_for_transition_id/3]). | |
| 20 | :- use_module(probsrc(state_space),[get_state_id_trace/1,history/1,op_trace_ids/1,transition/4,visited_expression/2]). | |
| 21 | :- use_module(probsrc(system_call),[get_temporary_filename/2]). | |
| 22 | :- use_module(probsrc(translate),[translate_bexpression_to_unicode/2,transform_raw/2,with_translation_mode/2]). | |
| 23 | :- use_module(probsrc(tools),[ajoin/2,ajoin_with_sep/3,get_filename_extension/2,list_difference/3,read_string_from_file/2]). | |
| 24 | :- use_module(probsrc(tools_commands),[gen_dot_output/4,valid_dot_output_format/1]). | |
| 25 | :- use_module(wdsrc(well_def_hyps),[normalize_expression/2,normalize_predicate/2]). | |
| 26 | ||
| 27 | :- use_module(sequent_prover,[cont_length/2,get_continuations/2,parse_input/3,used_identifiers/2]). | |
| 28 | :- use_module(prover_utils,[translate_norm_expr_term_no_limit/2,translate_norm_expr_term/2]). | |
| 29 | ||
| 30 | export_proof_for_current_state(Mode,File) :- | |
| 31 | get_state_id_trace(StateIds), | |
| 32 | op_trace_ids(TransIds), | |
| 33 | reverse(TransIds,RTransIds), | |
| 34 | export_proof(Mode,File,StateIds,RTransIds). | |
| 35 | ||
| 36 | export_proof(Mode,File,StateIds,TransIds) :- | |
| 37 | animation_minor_mode(sequent_prover), !, | |
| 38 | get_filename_extension(File,Ext), | |
| 39 | (Ext=Mode -> true | |
| 40 | ; ajoin(['file extension ',Ext,' does not match the proof export mode: '],Msg), | |
| 41 | add_warning(sequent_prover_exports,Msg,Mode)), | |
| 42 | export_proof2(Mode,File,StateIds,TransIds). | |
| 43 | export_proof(_,_,_,_) :- | |
| 44 | add_error(sequent_prover_exports,'Proof export is only available in sequent prover mode.'), fail. | |
| 45 | ||
| 46 | export_proof2(html,File,StateIds,TransIds) :- !, generate_proof_html_export(File,StateIds,TransIds). | |
| 47 | export_proof2(bpr, File,StateIds,TransIds) :- !, generate_proof_bpr_rodin_export(File,StateIds,TransIds). | |
| 48 | export_proof2(Mode,File,StateIds,TransIds) :- | |
| 49 | valid_dot_output_format(Mode), !, | |
| 50 | write_proof_tree_to_file(Mode,File,StateIds,TransIds). | |
| 51 | export_proof2(Mode,_,_,_) :- | |
| 52 | add_error(sequent_prover_exports,'unrecognised file extension for proof export: ',Mode), fail. | |
| 53 | ||
| 54 | %%%%%%%%% BUILD THE PROOF TREE %%%%%%%%% | |
| 55 | :- dynamic proof_node/4, proof_edge/5, proof_tree/2. | |
| 56 | % proof_node(ContinuationId,sequent(Hyps,Goal),Info,DotAttrList). | |
| 57 | % proof_edge(PrevId,DestId,TransId,ActTerm,Label). | |
| 58 | :- dynamic current_node/1, continuation/2. % auxiliary predicates used during proof tree generation | |
| 59 | % continuation(ContinuationSequent,IdWhereThisContinuationWasAdded). | |
| 60 | ||
| 61 | build_proof_tree(StateIds,TransIds) :- proof_tree(StateIds,TransIds), !. % proof tree already created | |
| 62 | build_proof_tree(StateIds,TransIds) :- | |
| 63 | retractall(proof_node(_,_,_,_)), | |
| 64 | retractall(proof_edge(_,_,_,_,_)), | |
| 65 | retractall(proof_tree(_,_)), | |
| 66 | retractall(continuation(_,_)), | |
| 67 | retractall(current_node(_)), | |
| 68 | build_proof_tree_aux(StateIds,TransIds), | |
| 69 | assertz(proof_tree(StateIds,TransIds)). | |
| 70 | ||
| 71 | :- use_module(library(codesio),[write_to_codes/2]). | |
| 72 | build_proof_tree_aux([],_). | |
| 73 | build_proof_tree_aux([_StateId],_). | |
| 74 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 75 | transition(PrevId,Act,TransId,StateId), | |
| 76 | Act=skip_to_cont, !, % ignore skips (just a reordering of continuations, not visible in the proof tree) | |
| 77 | build_proof_tree_aux([StateId|ST],TT). | |
| 78 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 79 | transition(PrevId,Act,TransId,StateId), | |
| 80 | visited_expression(StateId,State), | |
| 81 | State=state(success(SNr),_), !, % proof succeeded | |
| 82 | visited_expression(PrevId,PrevState), | |
| 83 | (PrevState=state(PrevSequent,_Info) | |
| 84 | -> PrevSequent=sequent(PVHyps,PVGoal,_) | |
| 85 | ; PrevState=root), | |
| 86 | (retract(continuation(sequent(PVHyps,PVGoal),ContID)) % previous sequent has been registered as continuation before | |
| 87 | -> PrevNode=ContID | |
| 88 | ; (current_node(PrevNode) -> true ; PrevNode=root)), | |
| 89 | (get_operation_description_for_transition_id(PrevId,TransId,EdgeLabel) -> true ; write_to_codes(Act,CAct), atom_codes(EdgeLabel,CAct)), | |
| 90 | assert_node_with_edge(PrevNode,success(SNr),[],TransId,[shape/triangle,style/filled,fillcolor/'#99BF38'],Act,EdgeLabel,GenID), | |
| 91 | set_current_node(GenID), | |
| 92 | build_proof_tree_aux([StateId|ST],TT). | |
| 93 | build_proof_tree_aux([PrevId,StateId|ST],[TransId|TT]) :- | |
| 94 | transition(PrevId,Act,TransId,StateId), % TODO: is there a way to obtain this directly from the history? | |
| 95 | visited_expression(PrevId,PrevState), visited_expression(StateId,state(Sequent,NxtInfo)), | |
| 96 | (PrevState=state(PrevSequent,Info) | |
| 97 | -> PrevSequent=sequent(PVHyps,PVGoal,_), cont_length(PrevSequent,PrevLen) | |
| 98 | ; PrevState=root, PrevLen=0, Info=NxtInfo), % for root use next info (important for des_hyps) | |
| 99 | Sequent=sequent(Hyps,Goal,_), | |
| 100 | ||
| 101 | (retract(continuation(sequent(PVHyps,PVGoal),ContID)) % previous sequent has been registered as continuation before | |
| 102 | -> PrevNode=ContID | |
| 103 | ; (current_node(PrevNode) -> true ; PrevNode=root)), | |
| 104 | ||
| 105 | (get_operation_description_for_transition_id(PrevId,TransId,EdgeLabel) -> true ; write_to_codes(Act,CAct), atom_codes(EdgeLabel,CAct)), | |
| 106 | ||
| 107 | cont_length(Sequent,Len), | |
| 108 | (PrevLen>Len % sequent has been proven by the current transition and disappeared | |
| 109 | -> assert_node_with_edge(PrevNode,success(-1),Info,TransId,[shape/triangle,style/filled,fillcolor/'#99BF38'],Act,EdgeLabel,_GenID) | |
| 110 | ; assert_node_with_edge(PrevNode,sequent(Hyps,Goal),Info,TransId,[shape/box],Act,EdgeLabel,GenID), | |
| 111 | assertz(continuation(sequent(Hyps,Goal),GenID)), % store position of current node | |
| 112 | set_current_node(GenID) | |
| 113 | ), | |
| 114 | ||
| 115 | get_continuations(Sequent,Conts), | |
| 116 | forall(member(Cont,Conts),assert_new_continuation(Cont,PrevNode,Info,TransId,Act,EdgeLabel)), | |
| 117 | build_proof_tree_aux([StateId|ST],TT). | |
| 118 | ||
| 119 | assert_node_with_edge(PrevNode,Sequent,Info,TransId,NodeAttr,Act,EdgeLabel,GenID) :- | |
| 120 | gensym('seq_prov_',GenID), | |
| 121 | assertz(proof_node(GenID,Sequent,Info,NodeAttr)), | |
| 122 | assertz(proof_edge(PrevNode,GenID,TransId,Act,EdgeLabel)). | |
| 123 | ||
| 124 | assert_new_continuation(Cont,_,_,_,_,_) :- | |
| 125 | continuation(Cont,_ID), !. % is already registered | |
| 126 | % TODO: what happens if the same continuation occurs more than once? | |
| 127 | assert_new_continuation(Cont,PrevNode,Info,TransId,Act,EdgeLabel) :- | |
| 128 | assert_node_with_edge(PrevNode,Cont,Info,TransId,[shape/box],Act,EdgeLabel,CID), | |
| 129 | assertz(continuation(Cont,CID)). | |
| 130 | ||
| 131 | set_current_node(ID) :- | |
| 132 | retractall(current_node(_)), | |
| 133 | assertz(current_node(ID)). | |
| 134 | ||
| 135 | %%%%%%%%% END BUILD THE PROOF TREE %%%%%%%%% | |
| 136 | ||
| 137 | %%%%%%%%% HELPER PREDICATES FOR SEQUENT_PROVER STATES %%%%%%%%% | |
| 138 | pretty_hyps(sequent(Hyps,_),PHyps) :- maplist(translate_norm_expr_term,Hyps,PHyps). | |
| 139 | pretty_goal(sequent(_,Goal),PGoal) :- translate_norm_expr_term(Goal,PGoal). | |
| 140 | ||
| 141 | ||
| 142 | %%%%%%%%% BEGIN PROOF TREE DOT GRAPH %%%%%%%%% | |
| 143 | :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3,use_new_dot_attr_pred/7]). | |
| 144 | generate_proof_tree_graph(File,StateIds,TransIds) :- | |
| 145 | (animation_minor_mode(sequent_prover) -> true | |
| 146 | ; 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)','')), | |
| 147 | build_proof_tree(StateIds,TransIds), | |
| 148 | gen_dot_graph(File, | |
| 149 | use_new_dot_attr_pred(sequent_prover_exports:proof_tree_graph_node_predicate), | |
| 150 | use_new_dot_attr_pred(sequent_prover_exports:proof_tree_graph_trans_predicate)). | |
| 151 | ||
| 152 | :- public proof_tree_graph_node_predicate/3. | |
| 153 | proof_tree_graph_node_predicate(root,none,[shape/invtriangle,label/'Select PO']). | |
| 154 | proof_tree_graph_node_predicate(NodeId,none,[id/NodeId,color/'#99BF38',label/'Proven.'|Attr]) :- | |
| 155 | proof_node(NodeId,success(_),_,Attr). | |
| 156 | proof_tree_graph_node_predicate(NodeId,none,[id/NodeId,color/'#99BF38',label/htmllabel(Label)|Attr]) :- | |
| 157 | proof_node(NodeId,Sequent,_,Attr), | |
| 158 | Sequent\=success(_), NodeId\=root, | |
| 159 | (proof_edge(PrevNode,NodeId,_,_,_), proof_node(PrevNode,PrevSequent,_,_) | |
| 160 | -> true | |
| 161 | ; PrevSequent=Sequent), % highlight no changes | |
| 162 | build_html_dot_label(PrevSequent,Sequent,Label). | |
| 163 | ||
| 164 | build_html_dot_label(PrevSequent,Sequent,Label) :- | |
| 165 | pretty_hyps(PrevSequent,PPrevHyps), pretty_hyps(Sequent,PHyps), | |
| 166 | pred_changed(PHyps,PPrevHyps,ChangedPHyps), | |
| 167 | (ChangedPHyps=[] | |
| 168 | -> HypLabel='<TR><TD><FONT COLOR="grey"><I>no hypotheses</I></FONT></TD></TR>' % no hyps | |
| 169 | ; maplist(label_for_pred,ChangedPHyps,HypLabels), | |
| 170 | ajoin(HypLabels,HypLabel)), | |
| 171 | pretty_goal(PrevSequent,PPrevGoal), pretty_goal(Sequent,PGoal), | |
| 172 | (PPrevGoal=PGoal -> Changed=not_changed; Changed=changed), | |
| 173 | label_for_pred(pred_line(PGoal,Changed),GoalLabel), | |
| 174 | ajoin(['<<TABLE BORDER="0" CELLBORDER="0" COLOR="black">', HypLabel, '<HR/>', GoalLabel, '</TABLE>>'],Label). | |
| 175 | ||
| 176 | label_for_pred(pred_line(Pred,Changed),PredLabel) :- | |
| 177 | tools:html_escape(Pred,EPred), | |
| 178 | (Changed=changed | |
| 179 | -> ajoin(['<TR><TD ALIGN="LEFT"><FONT COLOR="#de8000"><B>',EPred,'</B></FONT></TD></TR>'],PredLabel) | |
| 180 | ; ajoin(['<TR><TD ALIGN="LEFT"><FONT COLOR="black">',EPred,'</FONT></TD></TR>'],PredLabel) | |
| 181 | ). | |
| 182 | ||
| 183 | pred_changed([],_,[]). | |
| 184 | pred_changed([Hyp|HT],[],[pred_line(Hyp,not_changed)|RT]) :- pred_changed(HT,[],RT). | |
| 185 | pred_changed([Hyp|HT],PrevHyps,[pred_line(Hyp,Changed)|RT]) :- | |
| 186 | (selectchk(Hyp,PrevHyps,NPrevHyps) | |
| 187 | -> Changed=not_changed | |
| 188 | ; Changed=changed, NPrevHyps=PrevHyps), | |
| 189 | pred_changed(HT,NPrevHyps,RT). | |
| 190 | ||
| 191 | :- public proof_tree_graph_trans_predicate/3. | |
| 192 | proof_tree_graph_trans_predicate(PrevId,SuccId,[label/Label]) :- | |
| 193 | proof_edge(PrevId,SuccId,_TransId,_Act,Label). | |
| 194 | ||
| 195 | write_proof_tree_to_file(Mode,File,StateIds,TransIds) :- | |
| 196 | get_temporary_filename('_dot_proof_tree.dot',DotFile), | |
| 197 | generate_proof_tree_graph(DotFile,StateIds,TransIds), | |
| 198 | gen_dot_output(DotFile,dot,Mode,File). | |
| 199 | %%%%%%%%% END PROOF TREE DOT GRAPH %%%%%%%%% | |
| 200 | ||
| 201 | %%%%%%%%% BEGIN PROOF TREE HTML EXPORT %%%%%%%%% | |
| 202 | :- dynamic proof_html_export_template_file_codes/2. | |
| 203 | ||
| 204 | assert_from_template(Filename) :- | |
| 205 | absolute_file_name(seqproversrc(Filename), Absolute, []), | |
| 206 | read_string_from_file(Absolute,String), | |
| 207 | assertz(proof_html_export_template_file_codes(Filename,String)). | |
| 208 | ||
| 209 | write_proof_html_export_template(HtmlFile,Stream) :- | |
| 210 | proof_html_export_template_file_codes(HtmlFile,Codes), | |
| 211 | format(Stream,'~s~n',[Codes]). | |
| 212 | ||
| 213 | :- assert_from_template('proof_html_export_header.html'). | |
| 214 | :- assert_from_template('proof_html_export_footer.html'). | |
| 215 | ||
| 216 | % TODO: maybe highlight selected step in SVG; allow to select a step by clicking in the proof tree | |
| 217 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 218 | :- use_module(probsrc(xtl_interface),[xtl_main_file_name/1]). | |
| 219 | generate_proof_html_export(File,StateIds,TransIds) :- | |
| 220 | (animation_minor_mode(sequent_prover) -> true | |
| 221 | ; 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)','')), | |
| 222 | build_proof_tree(StateIds,TransIds), % important for step_list | |
| 223 | retractall(trans_id_done(_)), | |
| 224 | retractall(html_step_nr(_)), | |
| 225 | assertz(html_step_nr(1)), | |
| 226 | ||
| 227 | tools_io:safe_open_file(File,write,Stream,[encoding(utf8)]), | |
| 228 | write_proof_html_export_template('proof_html_export_header.html',Stream), | |
| 229 | xtl_main_file_name(POFile), | |
| 230 | (proof_edge(root,_,_,_,POLabel) | |
| 231 | -> format(Stream,' <div>Proof Trace Export for <b>~w</b> from <pre>~w</pre></div>~n',[POLabel,POFile]) | |
| 232 | ; format(Stream,' <div>Proof Trace Export from ~w</div>~n',[POFile])), | |
| 233 | format(Stream,' <hr/>~n',[]), | |
| 234 | format(Stream,' <div id="boxContainer" style="display: flex; width: 100%; position:fixed; height: 90vh;">~n',[]), | |
| 235 | format(Stream,' <div id="stepListBox" style="width: 30%; display: flex; flex-direction: column;">~n',[]), | |
| 236 | gen_step_list(Stream,TransIds), | |
| 237 | write_generation_info(Stream), | |
| 238 | format(Stream,' </div>~n',[]), | |
| 239 | format(Stream,' <div id="divider" class="divider"> </div>~n',[]), | |
| 240 | format(Stream,' <div id="treeBox" style="width: 66.5%; height: 97%; margin-left: 5px;">~n',[]), | |
| 241 | format(Stream,' <div class="box-caption">Proof Tree</div>~n',[]), | |
| 242 | format(Stream,' <div text-align="left" id="proof_tree_svg_outer_container" class="svg-outer-container">~n',[]), | |
| 243 | format(Stream,' <div text-align="left" id="proof_tree_svg_inner_container" class="svg-inner-container">~n',[]), | |
| 244 | write_proof_tree_svg_to_stream(Stream,StateIds,TransIds), % generate proof tree dot graph (with ProB dot preferences) | |
| 245 | format(Stream,' </div>~n',[]), | |
| 246 | format(Stream,' </div>~n',[]), | |
| 247 | format(Stream,' <button id="btnResetScale" class="visualisation-button" onclick="resetScale()">Reset View</button>~n',[]), | |
| 248 | format(Stream,' </div>~n',[]), % close tree box | |
| 249 | format(Stream,' </div>~n',[]), % close box container | |
| 250 | write_proof_html_export_template('proof_html_export_footer.html',Stream), | |
| 251 | close(Stream). | |
| 252 | ||
| 253 | :- use_module(probsrc(tools_io),[write_file_to_stream/2]). | |
| 254 | write_proof_tree_svg_to_stream(Stream,StateIds,TransIds) :- | |
| 255 | get_temporary_filename('_dot_proof_tree.svg',SvgFile), | |
| 256 | write_proof_tree_to_file(svg,SvgFile,StateIds,TransIds), | |
| 257 | write_file_to_stream(SvgFile,Stream). | |
| 258 | ||
| 259 | :- dynamic trans_id_done/1, html_step_nr/1. | |
| 260 | gen_step_list(Stream,TransIds) :- | |
| 261 | format(Stream,' <div class="box-caption" style="display: flex; justify-content: space-between;">Proof Steps~n',[]), | |
| 262 | format(Stream,' <div>~n',[]), | |
| 263 | format(Stream,' <button class="step-button" onclick="selectPrevStep()">< Previous Step</button>~n',[]), | |
| 264 | format(Stream,' <button class="step-button" onclick="selectNextStep()">Next Step ></button>~n',[]), | |
| 265 | format(Stream,' <button class="step-button" onclick="runAll()">Run Steps</button>~n',[]), | |
| 266 | format(Stream,' </div>~n',[]), | |
| 267 | format(Stream,' </div>~n',[]), | |
| 268 | format(Stream,' <div class="step-list">~n',[]), | |
| 269 | gen_step_list_entry(Stream,TransIds), | |
| 270 | format(Stream,' </div>~n',[]). | |
| 271 | gen_step_list_entry(Stream,TransIds) :- | |
| 272 | member(TransId,TransIds), | |
| 273 | proof_edge(PrevId,_Id,TransId,_,Label), | |
| 274 | \+ PrevId=root, | |
| 275 | \+ trans_id_done(TransId), | |
| 276 | findall(Id,proof_edge(_,Id,TransId,_,_),SuccIds), | |
| 277 | ajoin_with_sep([PrevId|SuccIds],'\',\'',IDList), | |
| 278 | format(Stream,' <div class="step-header green" onclick="focusSequents(\'trans_~w\',[\'~w\'])">~n',[TransId,IDList]), | |
| 279 | retract(html_step_nr(SNr)), | |
| 280 | NSNr is SNr+1, | |
| 281 | assertz(html_step_nr(NSNr)), | |
| 282 | format(Stream,' <b>~w. ~w</b>~n',[SNr,Label]), | |
| 283 | format(Stream,' </div>~n',[]), | |
| 284 | % TODO: here we could display more proof step details in the table (then an icon for extended/not-extended would be nice): | |
| 285 | format(Stream,' <div class="step-content" id="trans_~w">~n',[TransId]), | |
| 286 | % format(Stream,' <b>_TODO_</b>~n',[]), | |
| 287 | format(Stream,' </div>~n',[]), | |
| 288 | assertz(trans_id_done(TransId)), | |
| 289 | fail. | |
| 290 | gen_step_list_entry(_,_). | |
| 291 | ||
| 292 | :- use_module(library(system),[datime/1]). | |
| 293 | :- use_module(probsrc(tools_strings),[number_codes_min_length/3]). | |
| 294 | :- use_module(probsrc(version),[version_str/1,revision/1]). | |
| 295 | write_generation_info(Stream) :- | |
| 296 | version_str(VStr), revision(VRev), | |
| 297 | format(Stream,' <div style="color: grey; font-size: 0.7rem;"><br>ProB Version: ~w (~w)~n',[VStr,VRev]), | |
| 298 | datime(datime(Yr,Mon,Day,Hr,Min,_Sec)), | |
| 299 | number_codes_min_length(Mon,2,MonC), number_codes_min_length(Min,2,MinC), | |
| 300 | format(Stream,' <br>Generated on ~w/~s/~w at ~w:~s</div>~n',[Day,MonC,Yr,Hr,MinC]). | |
| 301 | %%%%%%%%% END PROOF TREE HTML EXPORT %%%%%%%%% | |
| 302 | ||
| 303 | % TODO: bpr_import? difficult as some details can be left out to the bpo file | |
| 304 | %%%%%%%%% BEGIN PROOF TREE RODIN BPR EXPORT %%%%%%%%% | |
| 305 | :- dynamic predicate_id_count/1, expression_id_count/1, rule_id_count/1. | |
| 306 | :- dynamic prPred/3, prExpr/3, prIdent/2, prReas/2. | |
| 307 | ||
| 308 | generate_proof_bpr_rodin_export(File,StateIds,TransIds) :- | |
| 309 | (animation_minor_mode(sequent_prover) | |
| 310 | -> add_message(sequent_prover_exports,'The BPR Rodin proof export is experimental and may contain errors!') | |
| 311 | ; 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)','')), | |
| 312 | build_proof_tree(StateIds,TransIds), | |
| 313 | retractall(prPred(_,_,_)), | |
| 314 | retractall(prExpr(_,_,_)), | |
| 315 | retractall(prIdent(_,_)), | |
| 316 | retractall(prReas(_,_)), | |
| 317 | retractall(predicate_id_count(_)), | |
| 318 | retractall(expression_id_count(_)), | |
| 319 | retractall(rule_id_count(_)), | |
| 320 | assertz(predicate_id_count(0)), | |
| 321 | assertz(expression_id_count(0)), | |
| 322 | assertz(rule_id_count(0)), | |
| 323 | tools_io:safe_open_file(File,write,Stream,[encoding(utf8)]), | |
| 324 | generate_bpr_to_stream(Stream,StateIds,TransIds), | |
| 325 | % TODO: handle existing BPR file: replace only one proof, add (one/multiple) proofs to the file, ... | |
| 326 | close(Stream). | |
| 327 | ||
| 328 | % general idea of the translation: each proof_edge becomes a prRule, with a prAnte for each proof_node (continuation) | |
| 329 | generate_bpr_to_stream(Stream,StateIds,TransIds) :- | |
| 330 | format(Stream,'<?xml version="1.0" encoding="UTF-8" standalone="no"?>~n',[]), | |
| 331 | format(Stream,'<org.eventb.core.prFile version="1">~n',[]), | |
| 332 | (TransIds\=[] -> generate_bpr_proof_tree(Stream,StateIds,TransIds) ; true), | |
| 333 | format(Stream,'</org.eventb.core.prFile>~n',[]), flush_output(Stream). | |
| 334 | ||
| 335 | :- use_module(sequent_prover,[get_scope/3,po_nr_label/2,normalised_hyps/3,normalised_goal/3]). | |
| 336 | generate_bpr_proof_tree(Stream,StateIds,TransIds) :- | |
| 337 | StateIds=[root,S1|_], TransIds=[T1|_], | |
| 338 | transition(root,start_xtl_system,T1,S1), % extract first state to determine selected PO | |
| 339 | visited_expression(S1,state(sequent(NormHyps,NormGoal,success(PONr)),Info)), | |
| 340 | ||
| 341 | member(des_hyps(DesHyps),Info), | |
| 342 | append(DesHyps,NormHyps,AllHyps), | |
| 343 | get_scope([NormGoal|AllHyps],Info,[identifier(Ids)]), | |
| 344 | forall(member(Id,Ids),assert_identifier(Id)), % register global IDs known in the initial step (including goal) | |
| 345 | ||
| 346 | po_nr_label(PONr,POLabel), | |
| 347 | normalised_hyps(POLabel,RawPreds,NormPreds), | |
| 348 | normalised_goal(POLabel,RawGoal,NormGoal), | |
| 349 | get_prob_normalisation_rewrites(RawPreds,NormPreds,HypRewrites), | |
| 350 | get_prob_normalisation_rewrites([RawGoal],[NormGoal],GoalRewr), | |
| 351 | (GoalRewr=[hyp_action(rewrite,G1,G2)] -> true ; assert_hyp_predicate(NormGoal,G1), G1=G2), % rewrite goal if necessary | |
| 352 | ||
| 353 | proof_edge(root,FirstNode,_,_,_), | |
| 354 | format_indent(Stream,'<org.eventb.core.prProof name="~w" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="" org.eventb.core.prHyps="" org.eventb.core.psManual="true">~n',[POLabel],1), | |
| 355 | format_indent(Stream,'<org.eventb.core.lang name="L"/>~n',[],2), | |
| 356 | (HypRewrites=[] | |
| 357 | -> write_proof_rule(Stream,FirstNode,2) % no ProB AST normalisation | |
| 358 | ; assert_rule_index('org.eventb.core.seqprover.review',RID), % TODO: disable normalisation/add as reasoner? | |
| 359 | format_indent(Stream,'<org.eventb.core.prRule name="~w" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ProB AST normalisation" org.eventb.core.prGoal="~w" org.eventb.core.prHyps="">~n',[RID,G1],2), | |
| 360 | get_next_rule_comment(FirstNode,CommentCodes), | |
| 361 | format_indent(Stream,'<org.eventb.core.prAnte name="\'" org.eventb.core.comment="~s" org.eventb.core.prGoal="~w">~n',[CommentCodes,G2],3), | |
| 362 | write_hyp_actions(Stream,HypRewrites,0,4), | |
| 363 | write_proof_rule(Stream,FirstNode,4), | |
| 364 | format_indent(Stream,'</org.eventb.core.prAnte>~n',[],3), | |
| 365 | format_indent(Stream,'</org.eventb.core.prRule>~n',[],2)), | |
| 366 | ||
| 367 | findall('$'(Id),member(b(identifier(Id),_,_),Ids),IdsOfFirstStep), | |
| 368 | write_identifiers(Stream,global,IdsOfFirstStep,2), | |
| 369 | write_predicate_mapping(Stream,2), | |
| 370 | write_expression_mapping(Stream,2), | |
| 371 | write_reasoner_mapping(Stream,2), | |
| 372 | format_indent(Stream,'</org.eventb.core.prProof>~n',[],1). | |
| 373 | ||
| 374 | write_proof_rule(Stream,FromNode,Indent) :- | |
| 375 | proof_edge(FromNode,_,_,Act,Desc), !, % generate only one prRule | |
| 376 | get_rule_reasoner(Act,ReasID,RID,Conf), % TODO: add option to use without Rodin reasoner IDs? | |
| 377 | proof_node(FromNode,sequent(Hyps,Goal),_,_), | |
| 378 | get_hyp_ids(Act,Hyps,HypIds), | |
| 379 | get_expr_ids(Act,ExprIds), | |
| 380 | get_pred_ids(Act,PredIds), | |
| 381 | % TODO: is it useful to print enum sets?, e.g. org.eventb.core.prSets="Beverages" (but works without) | |
| 382 | get_goal_id(Act,ReasID,Goal,GoalStr), | |
| 383 | xml_attribute_escape_atom(Desc,EDesc), | |
| 384 | format_indent(Stream,'<org.eventb.core.prRule name="~w" org.eventb.core.confidence="~w" org.eventb.core.prDisplay="~s" ~w org.eventb.core.prHyps="~w">~n',[RID,Conf,EDesc,GoalStr,HypIds],Indent), | |
| 385 | write_proof_rule2(Stream,FromNode,ReasID,ExprIds,PredIds,Indent). | |
| 386 | write_proof_rule(_,_,_). % write nothing, this is an open antecedent without rule | |
| 387 | write_proof_rule2(Stream,FromNode,_,_,_,Indent) :- | |
| 388 | proof_edge(FromNode,NextNode,_,Act,_Desc), | |
| 389 | proof_node(FromNode,sequent(Hyps,_Goal),FromInfo,_), | |
| 390 | (member(des_hyps(DesHyps),FromInfo) -> true ; DesHyps=[]), | |
| 391 | (proof_node(NextNode,sequent(NHyps,_NGoal),_,_) | |
| 392 | -> compute_hyp_actions_for_rule(DesHyps,Hyps,NHyps,HypActions0), | |
| 393 | adapt_hyp_actions_for_rule(Act,HypActions0,HypActions) | |
| 394 | ; HypActions=[]), % for success(_) | |
| 395 | AnteIndent is Indent+1, | |
| 396 | write_antecedant(Stream,FromNode,NextNode,HypActions,AnteIndent), | |
| 397 | fail. | |
| 398 | write_proof_rule2(Stream,_,_,prExprRef(RefType,ExprIds),_,Indent) :- % RefType can be exprs or subst, ... depending on the rule | |
| 399 | ExprIds \= [], | |
| 400 | ajoin_with_sep(ExprIds,',',SepExprIds), | |
| 401 | AnteIndent is Indent+1, | |
| 402 | format_indent(Stream,'<org.eventb.core.prExprRef name=".~w" org.eventb.core.prRef="~w"/>~n',[RefType,SepExprIds],AnteIndent), | |
| 403 | fail. | |
| 404 | write_proof_rule2(Stream,_,_,_,prPredRef(RefType,PredIds),Indent) :- | |
| 405 | PredIds \= [], | |
| 406 | ajoin_with_sep(PredIds,',',SepPredIds), | |
| 407 | AnteIndent is Indent+1, | |
| 408 | format_indent(Stream,'<org.eventb.core.prPredRef name=".~w" org.eventb.core.prRef="~w"/>~n',[RefType,SepPredIds],AnteIndent), | |
| 409 | fail. | |
| 410 | write_proof_rule2(Stream,_,ReasID,_,_,Indent) :- | |
| 411 | rule_requires_pos(ReasID,PosNr), | |
| 412 | AnteIndent is Indent+1, | |
| 413 | format_indent(Stream,'<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="~w"/>~n',[PosNr],AnteIndent), | |
| 414 | fail. | |
| 415 | write_proof_rule2(Stream,_,_,_,_,Indent) :- format_indent(Stream,'</org.eventb.core.prRule>~n',[],Indent). | |
| 416 | ||
| 417 | % prRule WITHOUT org.eventb.core.prHyps="" (null hyps) is not valid! | |
| 418 | get_hyp_ids(and_l(Pred),_,HypIds) :- !, assert_hyp_predicate(Pred,HypIds). % provide only the affected Hyp, then the rule expects a forward_inf as first rewrite | |
| 419 | get_hyp_ids(and_r,_,HypIds) :- !, HypIds=''. % AND_R expects null hyps | |
| 420 | get_hyp_ids(eq(_,L,R),_,HypIds) :- !, assert_hyp_predicate(equal(L,R),HypIds). % provide the exact hypId | |
| 421 | get_hyp_ids(imp_case(Pred),_,HypIds) :- !, assert_hyp_predicate(Pred,HypIds). % provide only the affected Hyp | |
| 422 | get_hyp_ids(simplify_goal(_),_,HypIds) :- !, HypIds=''. | |
| 423 | get_hyp_ids(simplify_hyp(_,Hyp),_,HypIds) :- !, assert_hyp_predicate(Hyp,HypIds). | |
| 424 | get_hyp_ids(Rule,Hyps,HypIds) :- | |
| 425 | rule_with_hyp_inst(Rule,HypNr,_), !, | |
| 426 | nth1(HypNr,Hyps,ForallHyp), | |
| 427 | assert_hyp_predicate(ForallHyp,HypIds). | |
| 428 | get_hyp_ids(_,Hyps,SepHypIds) :- | |
| 429 | maplist(assert_hyp_predicate,Hyps,HypIds), | |
| 430 | ajoin_with_sep(HypIds,',',SepHypIds). | |
| 431 | ||
| 432 | get_expr_ids(Rule,ExprIds) :- | |
| 433 | rule_with_expr(Rule,Expr,Kind), !, | |
| 434 | parse_input(Expr,Rule,TExpr), | |
| 435 | normalize_expression(TExpr,NormExpr), | |
| 436 | assert_expression(NormExpr,ExprId), | |
| 437 | ExprIds = prExprRef(Kind,[ExprId]). | |
| 438 | get_expr_ids(Rule,ExprIds) :- | |
| 439 | RName='DERIV_DOM_TOTALREL'(DomExpr), | |
| 440 | (Rule=simplify_hyp(RName,_) ; Rule=simplify_goal(RName)), !, | |
| 441 | assert_expression(DomExpr,ExprId), % value of the domain. | |
| 442 | ExprIds = prExprRef(subst,[ExprId]). | |
| 443 | get_expr_ids(_,prExprRef(none,[])). | |
| 444 | ||
| 445 | % TODO: add more rules with user input | |
| 446 | rule_with_expr(exists_inst(Inst),Expr,Kind) :- !, Expr=Inst, Kind=exprs. | |
| 447 | rule_with_expr(Rule,Expr,Kind) :- rule_with_hyp_inst(Rule,_,Inst), !, Expr=Inst, Kind=exprs. | |
| 448 | rule_with_expr(Rule,Expr,Kind) :- rule_with_pfun_input(Rule,PFun), !, Expr=PFun, Kind=expr. | |
| 449 | ||
| 450 | rule_with_hyp_inst(forall_inst(HypNr,Inst),HypNr,Inst). | |
| 451 | rule_with_hyp_inst(forall_inst_mp(HypNr,Inst),HypNr,Inst). | |
| 452 | rule_with_hyp_inst(forall_inst_mt(HypNr,Inst),HypNr,Inst). | |
| 453 | ||
| 454 | % extensions of the PFunSetInputReasoner | |
| 455 | rule_with_pfun_input(fin_fun_dom_r(PFun),PFun). | |
| 456 | rule_with_pfun_input(fin_fun_img_r(PFun),PFun). | |
| 457 | rule_with_pfun_input(fin_fun_ran_r(PFun),PFun). | |
| 458 | rule_with_pfun_input(fin_fun1_r(PFun),PFun). | |
| 459 | rule_with_pfun_input(fin_fun2_r(PFun),PFun). | |
| 460 | ||
| 461 | get_pred_ids(Rule,PredIds) :- | |
| 462 | rule_with_pred(Rule,Pred,Kind), !, | |
| 463 | parse_input(Pred,Rule,TPred), | |
| 464 | normalize_predicate(TPred,NormPred), | |
| 465 | sequent_prover:translate_finite_expr(NormPred,NewPred), | |
| 466 | assert_hyp_predicate(NewPred,PredId), | |
| 467 | PredIds = prPredRef(Kind,[PredId]). | |
| 468 | get_pred_ids(_,prPredRef(none,[])). | |
| 469 | ||
| 470 | rule_with_pred(add_hyp(Hyp),Pred,Kind) :- !, Pred=Hyp, Kind=pred. | |
| 471 | rule_with_pred(distinct_case(P),Pred,Kind) :- !, Pred=P, Kind=pred. | |
| 472 | ||
| 473 | % prRule WITH org.eventb.core.prGoal="" is not a valid null goal! | |
| 474 | get_goal_id(cntr,_,_,GoalStr) :- !, GoalStr=''. % CNTR produces null goal | |
| 475 | get_goal_id(imp_case(_),_,_,GoalStr) :- !, GoalStr=''. % is goal independent | |
| 476 | get_goal_id(simplify_hyp(_,_),ReasID,_,GoalStr) :- \+ rodin_review_reasoner(ReasID), !, GoalStr=''. % is goal independent if not reviewed | |
| 477 | get_goal_id(_,_,Goal,GoalStr) :- | |
| 478 | assert_hyp_predicate(Goal,GID), % should already be registered, get ID only | |
| 479 | ajoin(['org.eventb.core.prGoal="',GID,'"'],GoalStr). | |
| 480 | ||
| 481 | rodin_review_reasoner('org.eventb.core.seqprover.review'). | |
| 482 | ||
| 483 | rule_requires_pos('org.eventb.core.seqprover.ri',''). % TODO: extend list | |
| 484 | rule_requires_pos('org.eventb.core.seqprover.riUniversal',''). | |
| 485 | rule_requires_pos('org.eventb.core.seqprover.rmL2',''). | |
| 486 | rule_requires_pos('org.eventb.core.seqprover.rn',''). | |
| 487 | rule_requires_pos('org.eventb.core.seqprover.setEqlRewrites',''). | |
| 488 | rule_requires_pos('org.eventb.core.seqprover.totalDom:2','1'). % always 1? | |
| 489 | ||
| 490 | compute_hyp_actions_for_rule(_,[],[],Res) :- !, Res=[]. | |
| 491 | compute_hyp_actions_for_rule(DesHyps,[],[NewHyp|NT],Res) :- | |
| 492 | !, % there are new hyps after the existing ones -> SELECT or new_hyp | |
| 493 | select_hyp(DesHyps,NewHyp,Act), | |
| 494 | compute_hyp_actions_for_rule(DesHyps,[],NT,Acts), | |
| 495 | Res=[Act|Acts]. | |
| 496 | compute_hyp_actions_for_rule(_,PrevHyps,CurHyps,HypActs) :- | |
| 497 | select(DesHyp,PrevHyps,CurHyps), !, % one hypothesis has been removed -> DESELECT | |
| 498 | deselect_hyp(DesHyp,Act), | |
| 499 | HypActs=[Act]. | |
| 500 | compute_hyp_actions_for_rule(DesHyps,PrevHyps,CurHyps,HypActs) :- | |
| 501 | append(PrevHyps,AddHyps,CurHyps), !, % only new hypotheses have been added -> SELECT or new_hyp | |
| 502 | maplist(select_hyp(DesHyps),AddHyps,HypActs). | |
| 503 | compute_hyp_actions_for_rule(DesHyps,[PHyp|PT],[CHyp|CT],HypActs) :- | |
| 504 | PHyp\=CHyp, !, | |
| 505 | (PT=[NHyp|_], CT=[NHyp|_] % hyp has been rewritten; after that, the sequent is the same -> REWRITE | |
| 506 | -> rewrite_hyp(PHyp,CHyp,Act0), HypActs=[Act0|HypActs1], | |
| 507 | compute_hyp_actions_for_rule(DesHyps,PT,CT,HypActs1) | |
| 508 | ; (PT=[CHyp|_] % previous hyp has been deselected and replaced (next prev hyp is the current) -> DESELECT | |
| 509 | -> deselect_hyp(PHyp,Act1), HypActs=[Act1|HypActs1], | |
| 510 | compute_hyp_actions_for_rule(DesHyps,PT,[CHyp|CT],HypActs1) | |
| 511 | ; deselect_hyp(PHyp,Act2), select_hyp(DesHyps,CHyp,Act3), HypActs=[Act2,Act3|HypActs1], | |
| 512 | compute_hyp_actions_for_rule(DesHyps,PT,CT,HypActs1)) | |
| 513 | % last row changed: we cannot determine if the action is a REWRITE -> first DESELECT previous hyp, than SELECT (or new_hyp) the current hyp | |
| 514 | ). | |
| 515 | compute_hyp_actions_for_rule(DesHyps,[PHyp|PT],[CHyp|CT],Acts) :- | |
| 516 | PHyp=CHyp, % hyps are the same, no action | |
| 517 | compute_hyp_actions_for_rule(DesHyps,PT,CT,Acts). | |
| 518 | ||
| 519 | % Important: an action is only applicable if the EXACT hypothesis exists in the current step in Rodin! Otherwise, the action fails silently. | |
| 520 | deselect_hyp(Hyp,hyp_action(deselect,HypID,HypID)) :- assert_hyp_predicate(Hyp,HypID). % TODO check Hyp is member of selected Hyps? | |
| 521 | rewrite_hyp(Hyp1,Hyp2,hyp_action(rewrite,Hyp1ID,Hyp2ID)) :- % TODO check Hyp is member of de/selected Hyps? | |
| 522 | assert_hyp_predicate(Hyp1,Hyp1ID), | |
| 523 | assert_hyp_predicate(Hyp2,Hyp2ID). | |
| 524 | select_hyp(DesHyps,Hyp,hyp_action(Act,HypID,HypID)) :- | |
| 525 | (member(Hyp,DesHyps) -> Act=select ; Act=new_hyp), % check that hyp to be selected is in the set of deselected hyps, otherwise it must be added as a new hyp | |
| 526 | assert_hyp_predicate(Hyp,HypID). % SELECT can fail if hyp is not available, but new_hyp is always ok (but then Rodin does not display the selection in the proof step details) | |
| 527 | ||
| 528 | % adapt some hyp actions for rules that expect special actions: | |
| 529 | adapt_hyp_actions_for_rule(_,[],Res) :- !, Res=[]. | |
| 530 | adapt_hyp_actions_for_rule(and_l(_),OldActs,NewActs) :- !, % expects a rewrite as first action for the selected conjunction | |
| 531 | OldActs=[hyp_action(deselect,Des,Des),hyp_action(new_hyp,N1,N1),hyp_action(new_hyp,N2,N2)], | |
| 532 | ajoin([N1,',',N2],Rewr), | |
| 533 | NewActs=[hyp_action(rewrite,Des,Rewr),hyp_action(select,Rewr,Rewr)]. | |
| 534 | adapt_hyp_actions_for_rule(eq(_,_,_),OldActs,NewActs) :- !, % replace rewrites by forwards infs | |
| 535 | maplist(replace_rewrite_forward_inf,OldActs,NewActs). | |
| 536 | % TODO this does not cover the case if the rewritten hyps are at the end of the hyp list -> DESELECT + new_hyp (but this is also accepted by Rodin) | |
| 537 | adapt_hyp_actions_for_rule(simplify_hyp(Rule,Hyp),OldActs,NewActs) :- | |
| 538 | remove_membership_id(Rule), % expects a rewrite as first action | |
| 539 | OldActs\=[hyp_action(rewrite,_,_)|_], !, % no replacement required if the first hyp action is already a rewrite | |
| 540 | assert_hyp_predicate(Hyp,HypId), | |
| 541 | member(hyp_action(deselect,HypId,HypId),OldActs), % HypId is previous hyp | |
| 542 | findall(N,member(hyp_action(new_hyp,N,N),OldActs),InfHyps), % all new inferred hyps, may contain other new hyps (is ok) | |
| 543 | ajoin_with_sep(InfHyps,',',SepInfHyps), | |
| 544 | % replace new_hyp + deselect by rewrite + select | |
| 545 | NewActs=[hyp_action(rewrite,HypId,SepInfHyps),hyp_action(select,SepInfHyps,SepInfHyps)]. | |
| 546 | adapt_hyp_actions_for_rule(RuleTerm,[HypAct|HT],[HypAct|NH]) :- | |
| 547 | adapt_hyp_actions_for_rule(RuleTerm,HT,NH). | |
| 548 | ||
| 549 | replace_rewrite_forward_inf(hyp_action(rewrite,H1,H2),Res) :- !, Res=hyp_action(forward_inf,H1,H2). | |
| 550 | replace_rewrite_forward_inf(Act,Act). | |
| 551 | % in Java: if hideOriginal: rewrite, else: forward_inf | |
| 552 | ||
| 553 | write_antecedant(_,_,Node,_,_) :- proof_node(Node,success(_),_,_), !. | |
| 554 | write_antecedant(Stream,FromNode,Node,HypActions,Indent) :- | |
| 555 | proof_node(Node,sequent(Hyps,Goal),Info,_), | |
| 556 | get_scope([Goal|Hyps],Info,[identifier(Ids)]), | |
| 557 | (FromNode \= root | |
| 558 | -> proof_node(FromNode,sequent(FromHyps,FromGoal),FromInfo,_), | |
| 559 | get_scope([FromGoal|FromHyps],FromInfo,[identifier(FromIds)]), | |
| 560 | list_difference(Ids,FromIds,NewIds) % find new IDs in scope, e.g. after all_r (free a variable of forall) | |
| 561 | ; NewIds=[]), | |
| 562 | forall(member(Hyp,Hyps),assert_hyp_predicate(Hyp,_)), | |
| 563 | assert_hyp_predicate(Goal,GName), | |
| 564 | findall(NewHyp,member(hyp_action(new_hyp,NewHyp,_),HypActions),NewHypIds), | |
| 565 | ajoin_with_sep(NewHypIds,',',SepNewHypIds), | |
| 566 | get_next_rule_comment(Node,CommentCodes), | |
| 567 | format_indent(Stream,'<org.eventb.core.prAnte name="~w" org.eventb.core.comment="~s" org.eventb.core.prGoal="~w" org.eventb.core.prHyps="~w">~n',[Node,CommentCodes,GName,SepNewHypIds],Indent), | |
| 568 | % each prAnte of the same prRule must have a different name, TODO: check if prAnte name can really be arbitrary | |
| 569 | NIndent is Indent+1, | |
| 570 | write_hyp_actions(Stream,HypActions,0,NIndent), | |
| 571 | write_proof_rule(Stream,Node,NIndent), | |
| 572 | forall(member(Id,NewIds),assert_identifier(Id)), | |
| 573 | findall('$'(NewId),member(b(identifier(NewId),_,_),NewIds),NewIdsForPrint), | |
| 574 | write_identifiers(Stream,local,NewIdsForPrint,NIndent), % add new free identifiers in the corresponding prAnte, expected e.g. for all_r | |
| 575 | % TODO: check purpose of org.eventb.core.prFresh="" | |
| 576 | format_indent(Stream,'</org.eventb.core.prAnte>~n',[],Indent). | |
| 577 | ||
| 578 | get_next_rule_comment(FromNode,EDesc) :- | |
| 579 | proof_edge(FromNode,_,_,_,Desc), !, | |
| 580 | xml_attribute_escape_atom(Desc,EDesc). | |
| 581 | get_next_rule_comment(_,[]). | |
| 582 | ||
| 583 | write_hyp_actions(_,[],_,_). | |
| 584 | write_hyp_actions(Stream,[hyp_action(new_hyp,_,_)|T],Nr,Indent) :- !, write_hyp_actions(Stream,T,Nr,Indent). % ignore new_hyps, these are added as prHyps | |
| 585 | write_hyp_actions(Stream,[HypAct|T],Nr,Indent) :- | |
| 586 | write_hyp_action(Stream,HypAct,Nr,Indent), | |
| 587 | NNr is Nr+1, % number is important for the order of actions, e.g. REWRITE0, SELECT1, FORWARD_INF2, DESELECT3, ... | |
| 588 | write_hyp_actions(Stream,T,NNr,Indent). | |
| 589 | ||
| 590 | write_hyp_action(Stream,hyp_action(deselect,I1,_),Nr,Indent) :- !, | |
| 591 | format_indent(Stream,'<org.eventb.core.prHypAction name="DESELECT~w" org.eventb.core.prHyps="~w"/>~n',[Nr,I1],Indent). | |
| 592 | write_hyp_action(Stream,hyp_action(forward_inf,I1,I2),Nr,Indent) :- !, % TODO: clarify purpose | |
| 593 | format_indent(Stream,'<org.eventb.core.prHypAction name="FORWARD_INF~w" org.eventb.core.prHyps="~w" org.eventb.core.prInfHyps="~w"/>~n',[Nr,I1,I2],Indent). | |
| 594 | write_hyp_action(Stream,hyp_action(hide,I1,_),Nr,Indent) :- !, % TODO: difference to deselect? | |
| 595 | format_indent(Stream,'<org.eventb.core.prHypAction name="HIDE~w" org.eventb.core.prHyps="~w"/>~n',[Nr,I1],Indent). | |
| 596 | write_hyp_action(Stream,hyp_action(rewrite,I1,I2),Nr,Indent) :- !, | |
| 597 | format_indent(Stream,'<org.eventb.core.prHypAction name="REWRITE~w" org.eventb.core.prHidden="~w" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="~w"/>~n',[Nr,I1,I2],Indent). % !! fails without empty prHyps !! | |
| 598 | write_hyp_action(Stream,hyp_action(select,I1,_),Nr,Indent) :- !, | |
| 599 | format_indent(Stream,'<org.eventb.core.prHypAction name="SELECT~w" org.eventb.core.prHyps="~w"/>~n',[Nr,I1],Indent). | |
| 600 | write_hyp_action(Stream,hyp_action(show,I1,_),Nr,Indent) :- !, % TODO: difference to select? | |
| 601 | format_indent(Stream,'<org.eventb.core.prHypAction name="SHOW~w" org.eventb.core.prHyps="~w"/>~n',[Nr,I1],Indent). | |
| 602 | ||
| 603 | get_rule_reasoner(Act,ReasID,RID,Conf) :- | |
| 604 | rule_reasoner(Act,ReasID,Conf), | |
| 605 | assert_rule_index(ReasID,RID). | |
| 606 | ||
| 607 | rule_reasoner(Act,ReasID,Conf) :- | |
| 608 | rodin_rule_reasoner(Act,SeqProvID), !, | |
| 609 | ajoin(['org.eventb.core.seqprover.',SeqProvID],ReasID), | |
| 610 | Conf=100. % is UNCERTAIN_MAX, will trigger replay | |
| 611 | % TODO: same for ML/PP (but the call in Rodin differs from ours; all vs. selected hyps) | |
| 612 | rule_reasoner(ml,ReasID,Conf) :- !, ReasID='com.clearsy.atelierb.provers.core.externalML:1', Conf=100. | |
| 613 | rule_reasoner(prob_disprover,ReasID,Conf) :- !, ReasID='de.prob.eventb.disprover.core.disproverReasoner', Conf=100. | |
| 614 | rule_reasoner(_,'org.eventb.core.seqprover.review',1000). % review reasoner as fallback, TODO: should be confidence 500 | |
| 615 | ||
| 616 | % TODO complete list | |
| 617 | rodin_rule_reasoner(add_hyp(_),cut). | |
| 618 | rodin_rule_reasoner(all_r,allI). | |
| 619 | rodin_rule_reasoner(and_l(_),conjF). | |
| 620 | rodin_rule_reasoner(and_r,'conj:0'). | |
| 621 | rodin_rule_reasoner(auto_mh,autoImpF). | |
| 622 | rodin_rule_reasoner(card_empty_interv,cardUpTo). | |
| 623 | rodin_rule_reasoner(card_interv,cardUpTo). | |
| 624 | rodin_rule_reasoner(case(_),disjE). | |
| 625 | rodin_rule_reasoner(cntr,contrHyps). | |
| 626 | rodin_rule_reasoner(contradict_l(_),contrL1). | |
| 627 | rodin_rule_reasoner(contradict_r,contrL1). | |
| 628 | rodin_rule_reasoner(dbl_hyp,mngHyp). | |
| 629 | rodin_rule_reasoner(def_expn_step(_),exponentiationStep). | |
| 630 | rodin_rule_reasoner(deriv_equal_card,cardComparison). | |
| 631 | rodin_rule_reasoner(deriv_ge_card,cardComparison). | |
| 632 | rodin_rule_reasoner(deriv_gt_card,cardComparison). | |
| 633 | rodin_rule_reasoner(deriv_le_card,cardComparison). | |
| 634 | rodin_rule_reasoner(deriv_lt_card,cardComparison). | |
| 635 | rodin_rule_reasoner(deriv_equal_interv_l,derivEqualInterv). | |
| 636 | rodin_rule_reasoner(dis_binter_l,'funInterImg:1'). | |
| 637 | rodin_rule_reasoner(dis_binter_r,'funInterImg:1'). | |
| 638 | rodin_rule_reasoner(dis_setminus_l,'funSetMinusImg:1'). | |
| 639 | rodin_rule_reasoner(dis_setminus_r,'funSetMinusImg:1'). | |
| 640 | rodin_rule_reasoner(distinct_case,doCase). | |
| 641 | rodin_rule_reasoner(eq(lr,_,_),'eqL2:1'). | |
| 642 | rodin_rule_reasoner(eq(rl,_,_),'heL2:1'). | |
| 643 | rodin_rule_reasoner(eqv(lr,_,_),eqvLR). | |
| 644 | rodin_rule_reasoner(eqv(rl,_,_),eqvRL). | |
| 645 | rodin_rule_reasoner(exists_inst(_),exI). | |
| 646 | rodin_rule_reasoner(false_hyp,falseHyp). | |
| 647 | rodin_rule_reasoner(fin_binter_r,finiteInter). | |
| 648 | rodin_rule_reasoner(fin_bunion_r,finiteUnion). | |
| 649 | rodin_rule_reasoner(fin_compset_r,finiteCompset). | |
| 650 | rodin_rule_reasoner(fin_fun_dom_r(_),'finiteFunDom:0'). | |
| 651 | rodin_rule_reasoner(fin_fun_img_r(_),'finiteFunRelImg:0'). | |
| 652 | rodin_rule_reasoner(fin_fun_ran_r(_),'finiteFunRan:0'). | |
| 653 | rodin_rule_reasoner(fin_fun1_r(_),'finiteFunction:0'). | |
| 654 | rodin_rule_reasoner(fin_fun2_r(_),'finiteFunConv:0'). | |
| 655 | rodin_rule_reasoner(fin_ge_0,finitePositive). | |
| 656 | rodin_rule_reasoner(fin_kinter_r,finiteInter). | |
| 657 | rodin_rule_reasoner(fin_kunion_r,finiteUnion). | |
| 658 | rodin_rule_reasoner(fin_l_lower_bound,finiteHypBoundedGoal). % two rules in Rodin: L/R | |
| 659 | rodin_rule_reasoner(fin_l_upper_bound,finiteHypBoundedGoal). % two rules in Rodin: L/R | |
| 660 | rodin_rule_reasoner(fin_lt_0,finiteNegative). | |
| 661 | rodin_rule_reasoner(fin_qinter_r,finiteInter). | |
| 662 | rodin_rule_reasoner(fin_qunion_r,finiteUnion). | |
| 663 | rodin_rule_reasoner(fin_rel_img_r,finiteRelImg). | |
| 664 | rodin_rule_reasoner(fin_rel_r,'finiteRelation:0'). | |
| 665 | rodin_rule_reasoner(fin_rel_dom_r,finiteDom). | |
| 666 | rodin_rule_reasoner(fin_rel_ran_r,finiteRan). | |
| 667 | rodin_rule_reasoner(fin_setminus_r,finiteSetMinus). | |
| 668 | rodin_rule_reasoner(fin_subseteq_r(_),'finiteSet:0'). | |
| 669 | rodin_rule_reasoner(forall_inst(_,_),allD). | |
| 670 | rodin_rule_reasoner(forall_inst_mp(_,_),'allmpD:0'). | |
| 671 | rodin_rule_reasoner(forall_inst_mt(_,_),'allmtD:0'). | |
| 672 | rodin_rule_reasoner(fun_goal,isFunGoal). | |
| 673 | rodin_rule_reasoner(fun_image_goal,funImgGoal). | |
| 674 | rodin_rule_reasoner(hm(_),'mt:2'). | |
| 675 | rodin_rule_reasoner(hyp,hyp). | |
| 676 | rodin_rule_reasoner(hyp_or,hypOr). | |
| 677 | rodin_rule_reasoner(imp_and_l(_),impAndRewrites). | |
| 678 | rodin_rule_reasoner(imp_case(_),impCase). | |
| 679 | rodin_rule_reasoner(imp_or_l(_),impOrRewrites). | |
| 680 | rodin_rule_reasoner(imp_r,impI). | |
| 681 | rodin_rule_reasoner(lower_bound_l,finiteMin). | |
| 682 | rodin_rule_reasoner(lower_bound_r,finiteMin). | |
| 683 | rodin_rule_reasoner(mh(_),'impE:2'). | |
| 684 | rodin_rule_reasoner(mon_deselect(_),mngHyp). | |
| 685 | rodin_rule_reasoner(neg_in,'negEnum:0'). % two rules in Rodin: L/R | |
| 686 | rodin_rule_reasoner(one_point_l,'onePointRule:2'). | |
| 687 | rodin_rule_reasoner(one_point_r,'onePointRule:2'). | |
| 688 | rodin_rule_reasoner(ov_l,'funOvr:1'). | |
| 689 | rodin_rule_reasoner(ov_r,'funOvr:1'). | |
| 690 | rodin_rule_reasoner(ov_setenum_l,'funOvr:1'). | |
| 691 | rodin_rule_reasoner(ov_setenum_r,'funOvr:1'). | |
| 692 | rodin_rule_reasoner(reselect_hyp(_),mngHyp). | |
| 693 | rodin_rule_reasoner(sim_dprod_l,funDprodImg). | |
| 694 | rodin_rule_reasoner(sim_dprod_r,funDprodImg). | |
| 695 | rodin_rule_reasoner(sim_fcomp_l,funCompImg). | |
| 696 | rodin_rule_reasoner(sim_fcomp_r,funCompImg). | |
| 697 | rodin_rule_reasoner(sim_rel_image_l,funSingletonImg). | |
| 698 | rodin_rule_reasoner(sim_rel_image_r,funSingletonImg). | |
| 699 | rodin_rule_reasoner(sim_ov_pfun,mapOvrG). | |
| 700 | rodin_rule_reasoner(sim_ov_rel,mapOvrG). | |
| 701 | rodin_rule_reasoner(sim_ov_tfun,mapOvrG). | |
| 702 | rodin_rule_reasoner(sim_ov_trel,mapOvrG). | |
| 703 | rodin_rule_reasoner(simplify_goal(R),RID) :- rewrite_rule_id(R,RID). | |
| 704 | rodin_rule_reasoner(simplify_hyp(R,_),RID) :- rewrite_rule_id(R,RID). | |
| 705 | rodin_rule_reasoner(true_goal,trueGoal). | |
| 706 | rodin_rule_reasoner(upper_bound_l,finiteMax). | |
| 707 | rodin_rule_reasoner(upper_bound_r,finiteMax). | |
| 708 | rodin_rule_reasoner(xst_l,exF). | |
| 709 | ||
| 710 | rewrite_rule_id('DEF_BCOMP',bcompDefRewrites). | |
| 711 | rewrite_rule_id('DEF_EQUAL_CARD', cardDefRewrites). | |
| 712 | rewrite_rule_id('DEF_EQUAL_FUN_IMAGE', equalFunImgDefRewrites). | |
| 713 | rewrite_rule_id('DEF_EQUAL_MIN', minMaxDefRewrites). | |
| 714 | rewrite_rule_id('DEF_EQUAL_MAX', minMaxDefRewrites). | |
| 715 | rewrite_rule_id('DEF_EQV', eqvRewrites). | |
| 716 | rewrite_rule_id('DEF_FINITE', finiteDefRewrites). | |
| 717 | rewrite_rule_id('DEF_OR', disjToImplRewrites). | |
| 718 | rewrite_rule_id('DEF_OVERL', relOvrRewrites). | |
| 719 | rewrite_rule_id('DEF_PARTITION', partitionRewrites). | |
| 720 | rewrite_rule_id('DEF_SPECIAL_NOT_EQUAL', rn). | |
| 721 | rewrite_rule_id('DEF_SUBSET', sir). | |
| 722 | rewrite_rule_id('DEF_SUBSETEQ', ri). % removeInclusionRewriter | |
| 723 | rewrite_rule_id('DERIV_DOM_TOTALREL'(_), 'totalDom:2'). | |
| 724 | rewrite_rule_id('DERIV_EQUAL', setEqlRewrites). | |
| 725 | rewrite_rule_id('DERIV_FCOMP_DOMRES', domCompRewrites). | |
| 726 | rewrite_rule_id('DERIV_FCOMP_DOMSUB', domCompRewrites). | |
| 727 | rewrite_rule_id('DERIV_FCOMP_RANRES', ranCompRewrites). | |
| 728 | rewrite_rule_id('DERIV_FCOMP_RANSUB', ranCompRewrites). | |
| 729 | rewrite_rule_id('DERIV_IMP', doubleImplGoalRewrites). | |
| 730 | rewrite_rule_id('DERIV_IMP_IMP', doubleImplHypRewrites). | |
| 731 | rewrite_rule_id('DERIV_NOT_EXISTS', rn). | |
| 732 | rewrite_rule_id('DERIV_NOT_FORALL', rn). | |
| 733 | rewrite_rule_id('DERIV_NOT_IMP', rn). | |
| 734 | rewrite_rule_id('DERIV_RELIMAGE_FCOMP', compImgRewrites). | |
| 735 | rewrite_rule_id('DERIV_SUBSETEQ', riUniversal). | |
| 736 | rewrite_rule_id('DERIV_SUBSETEQ_SETMINUS_L', inclusionSetMinusLeftRewrites). | |
| 737 | rewrite_rule_id('DERIV_SUBSETEQ_SETMINUS_R', inclusionSetMinusRightRewrites). | |
| 738 | rewrite_rule_id('DERIV_TYPE_SETMINUS_BINTER', setMinusRewrites). | |
| 739 | rewrite_rule_id('DERIV_TYPE_SETMINUS_BUNION', setMinusRewrites). | |
| 740 | rewrite_rule_id('DERIV_TYPE_SETMINUS_SETMINUS', setMinusRewrites). | |
| 741 | rewrite_rule_id('DISTRI_AND_OR', andOrDistRewrites). | |
| 742 | rewrite_rule_id('DISTRI_BINTER_BUNION', unionInterDistRewrites). | |
| 743 | rewrite_rule_id('DISTRI_BUNION_BINTER', unionInterDistRewrites). | |
| 744 | rewrite_rule_id('DISTRI_CONVERSE_BUNION', convRewrites). | |
| 745 | rewrite_rule_id('DISTRI_DOMRES_BINTER', 'domDistLeftRewrites:0'). % TODO: split our rule in L/R, Rodin uses separate reasoner for right: domDistRightRewrites | |
| 746 | rewrite_rule_id('DISTRI_DOMRES_BUNION', 'domDistLeftRewrites:0'). % TODO: ditto, two rules in Rodin: L/R | |
| 747 | rewrite_rule_id('DISTRI_DOMSUB_BINTER_L', 'domDistLeftRewrites:0'). | |
| 748 | rewrite_rule_id('DISTRI_DOMSUB_BINTER_R', domDistRightRewrites). | |
| 749 | rewrite_rule_id('DISTRI_DOMSUB_BUNION_L', 'domDistLeftRewrites:0'). | |
| 750 | rewrite_rule_id('DISTRI_DOMSUB_BUNION_R', domDistRightRewrites). | |
| 751 | rewrite_rule_id('DISTRI_DOM_BUNION', domRanUnionDistRewrites). | |
| 752 | rewrite_rule_id('DISTRI_FCOMP_BUNION', compUnionDistRewrites). % two rules in Rodin: L/R | |
| 753 | rewrite_rule_id('DISTRI_NOT_AND', rn). | |
| 754 | rewrite_rule_id('DISTRI_NOT_OR', rn). | |
| 755 | rewrite_rule_id('DISTRI_IMP_AND', impAndRewrites). | |
| 756 | rewrite_rule_id('DISTRI_IMP_OR', impOrRewrites). | |
| 757 | rewrite_rule_id('DISTRI_OR_AND', andOrDistRewrites). | |
| 758 | rewrite_rule_id('DISTRI_RAN_BUNION', domRanUnionDistRewrites). | |
| 759 | rewrite_rule_id('DISTRI_RANSUB_BINTER_L', ranDistLeftRewrites). | |
| 760 | rewrite_rule_id('DISTRI_RANSUB_BINTER_R', 'ranDistRightRewrites:0'). | |
| 761 | rewrite_rule_id('DISTRI_RANSUB_BUNION_L', ranDistLeftRewrites). | |
| 762 | rewrite_rule_id('DISTRI_RANSUB_BUNION_R', 'ranDistRightRewrites:0'). | |
| 763 | rewrite_rule_id('DISTRI_RANRES_BINTER', ranDistLeftRewrites). % TODO: split our rule in L/R, Rodin uses separate reasoner for right: ranDistRightRewrites | |
| 764 | rewrite_rule_id('DISTRI_RANRES_BUNION', ranDistLeftRewrites). % TODO: ditto | |
| 765 | rewrite_rule_id('DISTRI_RELIMAGE_BUNION_L', relImgUnionLeftRewrites). | |
| 766 | rewrite_rule_id('DISTRI_RELIMAGE_BUNION_R', relImgUnionRightRewrites). | |
| 767 | rewrite_rule_id('SIMP_EQUAL_CARD', equalCardRewrites). | |
| 768 | rewrite_rule_id('SIMP_FUNIMAGE_DOMRES', 'funImgSimplifies:0'). | |
| 769 | rewrite_rule_id('SIMP_FUNIMAGE_DOMSUB', 'funImgSimplifies:0'). | |
| 770 | rewrite_rule_id('SIMP_FUNIMAGE_PPROD', funPprodImg). | |
| 771 | rewrite_rule_id('SIMP_FUNIMAGE_RANRES', 'funImgSimplifies:0'). | |
| 772 | rewrite_rule_id('SIMP_FUNIMAGE_RANSUB', 'funImgSimplifies:0'). | |
| 773 | rewrite_rule_id('SIMP_FUNIMAGE_SETMINUS', 'funImgSimplifies:0'). | |
| 774 | rewrite_rule_id('SIMP_LIT_CARD_UPTO', cardUpTo). | |
| 775 | rewrite_rule_id('SIMP_MINUS_UNMINUS', 'arithRewrites:1'). | |
| 776 | rewrite_rule_id('SIMP_MULTI_ARITHREL_PLUS_PLUS', 'arithRewrites:1'). | |
| 777 | rewrite_rule_id('SIMP_MULTI_ARITHREL_PLUS_L', 'arithRewrites:1'). | |
| 778 | rewrite_rule_id('SIMP_MULTI_ARITHREL_PLUS_R', 'arithRewrites:1'). | |
| 779 | rewrite_rule_id('SIMP_MULTI_ARITHREL_MINUS_MINUS_L', 'arithRewrites:1'). | |
| 780 | rewrite_rule_id('SIMP_MULTI_ARITHREL_MINUS_MINUS_R', 'arithRewrites:1'). | |
| 781 | rewrite_rule_id('SIMP_MULTI_MINUS_PLUS_L', 'arithRewrites:1'). | |
| 782 | rewrite_rule_id('SIMP_MULTI_MINUS_PLUS_PLUS', 'arithRewrites:1'). | |
| 783 | rewrite_rule_id('SIMP_MULTI_MINUS_PLUS_R', 'arithRewrites:1'). | |
| 784 | rewrite_rule_id('SIMP_MULTI_PLUS_MINUS', 'arithRewrites:1'). | |
| 785 | rewrite_rule_id('SIMP_NOT_NOT', rn). | |
| 786 | rewrite_rule_id('SIMP_TYPE_EQUAL_EMPTY', 'typeRewrites:1'). | |
| 787 | rewrite_rule_id('SIMP_TYPE_IN', 'typeRewrites:1'). | |
| 788 | rewrite_rule_id('SIMP_TYPE_SUBSETEQ', 'typeRewrites:1'). | |
| 789 | rewrite_rule_id('SIMP_TYPE_SUBSET_L', 'typeRewrites:1'). | |
| 790 | % TODO: PredicateSimplifier.java | |
| 791 | ||
| 792 | :- use_module(probsrc(bsyntaxtree),[flatten_conjunctions/2]). | |
| 793 | get_prob_normalisation_rewrites([],[],[]). | |
| 794 | get_prob_normalisation_rewrites([InitPred|IT],[NormPred|NT],Rewrites) :- | |
| 795 | % important: must use correctly nested conjuncts with parentheses (otherwise Rodin recognises them as a different predicate) | |
| 796 | transform_raw(InitPred,TInitPred), | |
| 797 | with_forced_rodin_mode(translate_bexpression_to_unicode(TInitPred,PInitPred)), | |
| 798 | translate_norm_expr_term_no_limit(NormPred,PNormPred), | |
| 799 | (PInitPred = PNormPred | |
| 800 | -> assert_hyp_predicate(NormPred,_), Rewrites=RT % predicate is the same after normalisation -> no rewrite | |
| 801 | ; assert_hyp_predicate_init_rewrite(IName,PInitPred), | |
| 802 | assert_hyp_predicate(NormPred,NName), | |
| 803 | Rewrites=[hyp_action(rewrite,IName,NName)|RT]), % register rewrite | |
| 804 | get_prob_normalisation_rewrites(IT,NT,RT). | |
| 805 | ||
| 806 | assert_hyp_predicate(Hyp,Name) :- with_forced_rodin_mode(translate_norm_expr_term_no_limit(Hyp,Pred)), prPred(_,Name,Pred), !. % predicate already exists | |
| 807 | assert_hyp_predicate(Hyp,Name) :- | |
| 808 | retract(predicate_id_count(C)), | |
| 809 | ajoin([p,C],Name), | |
| 810 | NextC is C+1, | |
| 811 | with_forced_rodin_mode(translate_norm_expr_term_no_limit(Hyp,Pred)), | |
| 812 | assertz(prPred(Hyp,Name,Pred)), | |
| 813 | assertz(predicate_id_count(NextC)). | |
| 814 | ||
| 815 | assert_expression(Expr,Name) :- with_forced_rodin_mode(translate_norm_expr_term_no_limit(Expr,PExpr)), prExpr(_,Name,PExpr), !. % expression already exists | |
| 816 | assert_expression(Expr,Name) :- | |
| 817 | retract(expression_id_count(C)), | |
| 818 | ajoin([e,C],Name), | |
| 819 | NextC is C+1, | |
| 820 | with_forced_rodin_mode(translate_norm_expr_term_no_limit(Expr,PExpr)), | |
| 821 | assertz(prExpr(Expr,Name,PExpr)), | |
| 822 | assertz(expression_id_count(NextC)). | |
| 823 | ||
| 824 | with_forced_rodin_mode(Call) :- | |
| 825 | translate:set_force_eventb_mode, % for printing special unicodes for <+, <<->>, <<->, <->>, which we do not want to appear in the state visualisation | |
| 826 | call_cleanup(Call, translate:unset_force_eventb_mode). | |
| 827 | ||
| 828 | assert_hyp_predicate_init_rewrite(Name,PHyp) :- prPred(_,Name,PHyp), !. % predicate already exists | |
| 829 | assert_hyp_predicate_init_rewrite(Name,PHyp) :- | |
| 830 | retract(predicate_id_count(C)), | |
| 831 | ajoin([p,C],Name), | |
| 832 | NextC is C+1, | |
| 833 | assertz(prPred(Name,Name,PHyp)), | |
| 834 | assertz(predicate_id_count(NextC)). | |
| 835 | ||
| 836 | assert_rule_index(ReasonerID,RuleIndex) :- prReas(RuleIndex,ReasonerID), !. | |
| 837 | assert_rule_index(ReasonerID,RuleIndex) :- | |
| 838 | retract(rule_id_count(C)), | |
| 839 | ajoin([r,C],RuleIndex), | |
| 840 | NextC is C+1, | |
| 841 | assertz(prReas(RuleIndex,ReasonerID)), | |
| 842 | assertz(rule_id_count(NextC)). | |
| 843 | ||
| 844 | assert_identifier(b(identifier(Id),Type,_)) :- | |
| 845 | prIdent(Id,Type), !, | |
| 846 | findall(Type1,(prIdent(Id,Type1),Type1\=any),Types), | |
| 847 | (Types=[Type] -> true | |
| 848 | ; add_error(generate_proof_bpr_rodin_export,type_mismatch_for_prIdent(Id,Types,Type)), fail). | |
| 849 | assert_identifier(b(identifier(Id),Type,_)) :- | |
| 850 | assertz(prIdent(Id,Type)). | |
| 851 | ||
| 852 | % Global=global: retract globalIDs after print to avoid printing them for all predicates/expressions | |
| 853 | write_identifiers(Stream,Global,Ids,Indent) :- | |
| 854 | member('$'(Id),Ids), | |
| 855 | (Global=global -> retract(prIdent(Id,Type)) ; prIdent(Id,Type)), | |
| 856 | Type\=any, % TODO: get rid of any types here (that's because the type check failed, e.g. for x : {}) | |
| 857 | with_translation_mode(unicode,translate:pretty_normalized_type(Type,PType)), | |
| 858 | xml_attribute_escape_atom(PType,EType), | |
| 859 | format_indent(Stream,'<org.eventb.core.prIdent name="~w" org.eventb.core.type="~s"/>~n',[Id,EType],Indent), | |
| 860 | fail. | |
| 861 | write_identifiers(_,_,_,_). | |
| 862 | ||
| 863 | write_predicate_mapping(Stream,Indent) :- | |
| 864 | prPred(Hyp,Name,Pred), | |
| 865 | used_identifiers(Hyp,Ids), sort(Ids,SIds), | |
| 866 | xml_attribute_escape_atom(Pred,EPred), | |
| 867 | format_indent(Stream,'<org.eventb.core.prPred name="~w" org.eventb.core.predicate="~s">~n',[Name,EPred],Indent), | |
| 868 | NIndent is Indent+1, | |
| 869 | write_identifiers(Stream,local,SIds,NIndent), | |
| 870 | format_indent(Stream,'</org.eventb.core.prPred>~n',[],Indent), | |
| 871 | fail. | |
| 872 | write_predicate_mapping(_,_). | |
| 873 | ||
| 874 | write_expression_mapping(Stream,Indent) :- | |
| 875 | prExpr(Expr,Name,PrettyExpr), | |
| 876 | used_identifiers(Expr,Ids), sort(Ids,SIds), | |
| 877 | xml_attribute_escape_atom(PrettyExpr,EExpr), | |
| 878 | format_indent(Stream,'<org.eventb.core.prExpr name="~w" org.eventb.core.expression="~s">~n',[Name,EExpr],Indent), | |
| 879 | NIndent is Indent+1, | |
| 880 | write_identifiers(Stream,local,SIds,NIndent), | |
| 881 | format_indent(Stream,'</org.eventb.core.prExpr>~n',[],Indent), | |
| 882 | fail. | |
| 883 | write_expression_mapping(_,_). | |
| 884 | ||
| 885 | write_reasoner_mapping(Stream,Indent) :- | |
| 886 | prReas(Name,RID), | |
| 887 | format_indent(Stream,'<org.eventb.core.prReas name="~w" org.eventb.core.prRID="~w"/>~n',[Name,RID],Indent), | |
| 888 | fail. | |
| 889 | write_reasoner_mapping(_,_). | |
| 890 | ||
| 891 | :- use_module(probsrc(tools),[xml_attribute_escape/2]). | |
| 892 | xml_attribute_escape_atom(A,EC) :- \+ atom(A),!, | |
| 893 | add_internal_error('Not an atom: ',xml_attribute_escape_atom(A,EC)), EC='??'. | |
| 894 | xml_attribute_escape_atom(A,EC) :- atom_codes(A,C), xml_attribute_escape(C,EC). | |
| 895 | ||
| 896 | indent_ws(_Stream,X) :- X<1,!. | |
| 897 | indent_ws(Stream,X) :- format(Stream,' ',[]), X1 is X-1, indent_ws(Stream,X1). | |
| 898 | ||
| 899 | format_indent(S,A,L,I) :- indent_ws(S,I), format(S,A,L). | |
| 900 | %%%%%%%%% END PROOF TREE RODIN BPR EXPORT %%%%%%%%% | |
| 901 | ||
| 902 | %%%%%%%%% BEGIN PRETTY PRINT %%%%%%%%% | |
| 903 | :- use_module(probsrc(xtl_interface),[get_disprover_po/6]). | |
| 904 | pretty_print_pos(PP) :- | |
| 905 | findall(po(Lbl,G,AH,SH,Status), get_disprover_po(Lbl,_Ctx,G,AH,SH,Status), POs), | |
| 906 | pp_po(POs,PP,[]). | |
| 907 | ||
| 908 | pp_po([]) --> []. | |
| 909 | pp_po([po(POLabel,RawGoal,RawAllHyps,RawSelHyps,RodinStatus)|PT]) --> | |
| 910 | {atom_codes(POLabel,CLabel), atom_codes(RodinStatus,CStatus)}, CLabel, " (", CStatus, ")\n", | |
| 911 | "\x2550\\x2550\\x2550\\x2550\\x2550\\x2550\\x2550\\x2550\\n", | |
| 912 | pp_hyps(RawAllHyps,RawSelHyps), | |
| 913 | " \x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\x2500\\n", | |
| 914 | " ", translate:pp_raw_formula(RawGoal), "\n\n\n", | |
| 915 | pp_po(PT). | |
| 916 | ||
| 917 | pp_hyps([],_) --> []. | |
| 918 | pp_hyps([RawHyp|AT],SelHyps) --> | |
| 919 | ({member(RawHyp,SelHyps)} -> " \x2714\ " ; " "), | |
| 920 | translate:pp_raw_formula(RawHyp), "\n", | |
| 921 | pp_hyps(AT,SelHyps). | |
| 922 | %%%%%%%%% END PRETTY PRINT %%%%%%%%% |