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!

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 93924b9ada6a71331a28f5cb7002844dc88659c6..3774ed0d7b8c5e55fe03677945aa3d343685c245 100644 (file)
--- 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 () =
        ("<h1 color=\"red\">No term selected</h1>")
 ;;
 
+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
+            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+        end
+   | None ->
+      output_html outputhtml
+       ("<h1 color=\"red\">No term selected</h1>")
+;;
+
 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
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
@@ -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 90d18998111695f18578ddc6ae031f27c89876e0..97c84858c2ab4bad1210fabaeaf4498659b556d3 100644 (file)
--- 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 =