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

    at once.
2.  To reduce several (sub)terms at once you can use the new multiple
    selection feature.

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
 ;;
 

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 99e6a081cdeaccb8940fe687eb30ae6bb380ea35..4751cb23f93b725dd15292f6bac8c95c5711375a 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -116,7 +116,7 @@ let perforate context term ty =
         let irl = identity_relocation_list_for_metavariable context in
 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
         let bo' =
-         ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
+         ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
         in
         (* It may be possible that some metavariables occurred only in *)
         (* the term we are perforating and they now occurs no more. We *)
@@ -137,7 +137,7 @@ let perforate context term ty =
 (************************************************************)
 
 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
-let reduction_tactic_in_scratch reduction_function term ty =
+let reduction_tactic_in_scratch reduction_function terms ty =
  let metasenv =
   match !proof with
      None -> []
@@ -148,9 +148,9 @@ let reduction_tactic_in_scratch reduction_function term ty =
      None -> assert false
    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
  in
-  let term' = reduction_function context term in
+  let terms' = List.map (reduction_function context) terms in
    ProofEngineReduction.replace
-    ~equality:(==) ~what:term ~with_what:term' ~where:ty
+    ~equality:(==) ~what:terms ~with_what:terms' ~where:ty
 ;;
 
 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd
@@ -184,15 +184,15 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 
   (* reduction tactics *)
 
-let whd term =
+let whd terms =
  apply_tactic
-  (ReductionTactics.whd_tac ~also_in_hypotheses:true ~term:(Some term))
-let reduce term =
+  (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms))
+let reduce terms =
  apply_tactic
-  (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~term:(Some term))
-let simpl term =
+  (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms))
+let simpl terms =
  apply_tactic
-  (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term))
+  (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms))
 
 let fold_whd term =
  apply_tactic

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c845c2b1ea2ee392ad7b0ed98568554d3da3e224..8f8b1261d4e6bfb66bf1a2133860719d90ab1587 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -31,17 +31,17 @@ val goal : ProofEngineTypes.goal option ref
 val perforate : Cic.context -> Cic.term -> Cic.term -> unit
 
   (* reduction tactics *)
-val whd : Cic.term -> unit
-val reduce : Cic.term -> unit
-val simpl : Cic.term -> unit
+val whd : Cic.term list -> unit
+val reduce : Cic.term list -> unit
+val simpl : Cic.term list -> unit
 val fold_whd : Cic.term -> unit
 val fold_reduce : Cic.term -> unit
 val fold_simpl : Cic.term -> unit
 
   (* scratch area reduction tactics *)
-val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
-val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term
-val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term
+val whd_in_scratch : Cic.term list -> Cic.term -> Cic.term
+val reduce_in_scratch : Cic.term list -> Cic.term -> Cic.term
+val simpl_in_scratch : Cic.term list -> Cic.term -> Cic.term
 
   (* "primitive" tactics *)
 val can_apply : Cic.term -> bool