1. All the reduction tactics have been modified to reduce several (sub)terms

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f00261d8e412d8a4a191dca313eb992e88306a99..5626600f79ee8d5eee62ba3dcb07a6bebcae1efa 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1990,6 +1990,65 @@ let call_tactic_with_goal_input tactic () =
        ("<h1 color=\"red\">Many terms selected</h1>")
 ;;
 
+let call_tactic_with_goal_inputs tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+  let notebook = (rendering_window ())#notebook in
+  let output =
+   ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+  let savedproof = !ProofEngine.proof in
+  let savedgoal  = !ProofEngine.goal in
+   try
+    let term_of_node 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
+       match !current_goal_infos with
+          Some (ids_to_terms, ids_to_father_ids,_) ->
+           let id = xpath in
+            (Hashtbl.find ids_to_terms id)
+        | None -> assert false (* "ERROR: No current term!!!" *)
+    in
+     match notebook#proofw#get_selections with
+        [] ->
+         output_html outputhtml
+          ("<h1 color=\"red\">No term selected</h1>")
+      | l ->
+         let terms = List.map term_of_node l in
+           match !current_goal_infos with
+              Some (ids_to_terms, ids_to_father_ids,_) ->
+               tactic terms ;
+               refresh_sequent notebook ;
+               refresh_proof output
+            | None -> assert false (* "ERROR: No current term!!!" *)
+   with
+      RefreshSequentException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent notebook
+    | RefreshProofException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent notebook ;
+       refresh_proof output
+    | e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal
+;;
+
 let call_tactic_with_input_and_goal_input tactic () =
  let module L = LogicalOperations in
  let module G = Gdome in
@@ -2107,6 +2166,46 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
        ("<h1 color=\"red\">Many terms selected</h1>")
 ;;
 
+let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+  let mmlwidget =
+   (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+  let savedproof = !ProofEngine.proof in
+  let savedgoal  = !ProofEngine.goal in
+   match mmlwidget#get_selections with
+      [] ->
+       output_html outputhtml
+        ("<h1 color=\"red\">No term selected</h1>")
+    | l ->
+       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 term_of_node 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
+               let id = xpath in
+                Hashtbl.find ids_to_terms id
+            in
+             let terms = List.map term_of_node l in
+              let expr = tactic terms term in
+               let mml = mml_of_cic_term 111 expr in
+                scratch_window#show () ;
+                scratch_window#mmlwidget#load_doc ~dom:mml
+         | None -> assert false (* "ERROR: No current term!!!" *)
+       with
+        e ->
+         output_html outputhtml
+          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
 let call_tactic_with_hypothesis_input tactic () =
  let module L = LogicalOperations in
  let module G = Gdome in
@@ -2169,9 +2268,9 @@ let exact = call_tactic_with_input ProofEngine.exact;;
 let apply = call_tactic_with_input ProofEngine.apply;;
 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
-let whd = call_tactic_with_goal_input ProofEngine.whd;;
-let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
-let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
+let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
+let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
+let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
@@ -2201,15 +2300,15 @@ let decompose =
   (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
 
 let whd_in_scratch scratch_window =
- call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
+ call_tactic_with_goal_inputs_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
+ call_tactic_with_goal_inputs_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
+ call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
   scratch_window
 ;;