From a3ea60dba4a46e32ab70a0ebda36367a8186a59f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Apr 2002 11:13:49 +0000 Subject: [PATCH] Reduction tactics in the scratch window implemented. NOTE: if you select an hypothesis and you apply a reduction tactic, nothing will happen and no error message will be reported! --- helm/gTopLevel/gTopLevel.ml | 99 +++++++++++++++++++++++++++++++---- helm/gTopLevel/proofEngine.ml | 21 ++++++++ 2 files changed, 109 insertions(+), 11 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 93924b9ad..3774ed0d7 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -53,6 +53,7 @@ let htmlheader_and_content = ref htmlheader;; let current_cic_infos = ref None;; let current_goal_infos = ref None;; +let current_scratch_infos = ref None;; (* MISC FUNCTIONS *) @@ -226,9 +227,11 @@ let mml_of_cic_term term = let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in - applyStylesheets sequent_doc sequent_styles sequent_args - (*CSC: magari prima o poi serve*) - (*current_scratch_infos := Some (ids_to_terms,ids_to_father_ids)*) + let res = + applyStylesheets sequent_doc sequent_styles sequent_args ; + in + current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ; + res ;; let output_html outputhtml msg = @@ -411,6 +414,43 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = ("

No term selected

") ;; +let call_tactic_with_goal_input_in_scratch tactic scratch_window () = + let module L = LogicalOperations in + let module G = Gdome in + let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in + let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match mmlwidget#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_scratch_infos with + (* term is the whole goal in the scratch_area *) + Some (term,ids_to_terms, ids_to_father_ids) -> + let id = xpath in + let expr = tactic term (Hashtbl.find ids_to_terms id) in + let mml = mml_of_cic_term expr in + scratch_window#show () ; + scratch_window#mmlwidget#load_tree ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; let exact rendering_window = call_tactic_with_input ProofEngine.exact rendering_window @@ -441,6 +481,19 @@ let change rendering_window = ;; +let whd_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch + scratch_window +;; +let reduce_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch + scratch_window +;; +let simpl_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch + scratch_window +;; + (**********************) @@ -582,6 +635,7 @@ let state rendering_window () = let check rendering_window scratch_window () = let inputt = (rendering_window#inputt : GEdit.text) in + let oldinputt = (rendering_window#oldinputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let output = (rendering_window#output : GMathView.math_view) in let proofw = (rendering_window#proofw : GMathView.math_view) in @@ -614,9 +668,9 @@ let check rendering_window scratch_window () = | Some expr -> try let ty = CicTypeChecker.type_of_aux' metasenv ciccontext expr in - let mml = mml_of_cic_term ty in + let mml = mml_of_cic_term (Cic.Cast (expr,ty)) in scratch_window#show () ; - scratch_window#display ~dom:mml + scratch_window#mmlwidget#load_tree ~dom:mml with e -> print_endline ("? " ^ CicPp.ppterm expr) ; @@ -624,7 +678,8 @@ let check rendering_window scratch_window () = done with CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen + inputt#delete_text 0 inputlen ; + ignore(oldinputt#insert_text input oldinputt#length) | e -> output_html outputhtml ("

" ^ Printexc.to_string e ^ "

") ; @@ -777,16 +832,38 @@ end;; (* Scratch window *) -class scratch_window () = +class scratch_window outputhtml = let window = GWindow.window ~title:"MathML viewer" ~border_width:2 () in + let vbox = + GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in let mmlwidget = - GMathView.math_view ~packing:(window#add) ~width:400 ~height:280 () in + GMathView.math_view + ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) - method display = mmlwidget#load_tree + method outputhtml = outputhtml + method mmlwidget = mmlwidget method show () = window#misc#hide () ; window#show () initializer - ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) + ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ; + ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; + ignore(whdb#connect#clicked (whd_in_scratch self)) ; + ignore(reduceb#connect#clicked (reduce_in_scratch self)) ; + ignore(simplb#connect#clicked (simpl_in_scratch self)) end;; (* Main window *) @@ -881,7 +958,7 @@ class rendering_window output proofw (label : GMisc.label) = ~width:400 ~height: 200 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) ~show:true () in - let scratch_window = new scratch_window () in + let scratch_window = new scratch_window outputhtml in object(self) method outputhtml = outputhtml method oldinputt = oldinputt diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 90d189981..97c84858c 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -574,10 +574,31 @@ let reduction_tactic reduction_function term = goal := Some (metano,(context',ty')) ;; +let reduction_tactic_in_scratch reduction_function ty term = + let curi,metasenv,pbo,pty = + match !proof with + None -> assert false + | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty + in + let (metano,context,_) = + match !goal with + None -> assert false + | Some (metano,(context,ty)) -> metano,context,ty + in + let term' = reduction_function term in + ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty +;; + let whd = reduction_tactic CicReduction.whd;; let reduce = reduction_tactic ProofEngineReduction.reduce;; let simpl = reduction_tactic ProofEngineReduction.simpl;; +let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;; +let reduce_in_scratch = + reduction_tactic_in_scratch ProofEngineReduction.reduce;; +let simpl_in_scratch = + reduction_tactic_in_scratch ProofEngineReduction.simpl;; + (* It is just the opposite of whd. The code should probably be merged. *) let fold term = let curi,metasenv,pbo,pty = -- 2.39.2