now destruct takes an optional list of term rather than a sigle optional term

[helm.git] / components / tactics / proofEngineStructuralRules.ml

diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml
index 4677a33ac8221a1080d7d0f6953e9fe2b8a822ba..ea7586e164f77c3a03079bdc9142481eb396ac70 100644 (file)
--- a/components/tactics/proofEngineStructuralRules.ml
+++ b/components/tactics/proofEngineStructuralRules.ml
@@ -25,12 +25,12 @@
 
 (* $Id$ *)
 
-open ProofEngineTypes
+module PET = ProofEngineTypes
+module C = Cic
 
 let clearbody ~hyp = 
- let clearbody ~hyp (proof, goal) =
-  let module C = Cic in
-   let curi,metasenv,pbo,pty = proof in
+ let clearbody (proof, goal) =
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
      let string_of_name =
       function
@@ -68,7 +68,7 @@ let clearbody ~hyp =
                       with
                        _ ->
                          raise
-                          (Fail
+                          (PET.Fail
                             (lazy ("The correctness of hypothesis " ^
                              string_of_name n ^
                              " relies on the body of " ^ hyp)
@@ -85,7 +85,7 @@ let clearbody ~hyp =
                with
                 _ ->
                  raise
-                  (Fail
+                  (PET.Fail
                    (lazy ("The correctness of the goal relies on the body of " ^
                     hyp)))
               in
@@ -93,14 +93,13 @@ let clearbody ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
-  mk_tactic (clearbody ~hyp)
+  PET.mk_tactic clearbody
 
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
-  let module C = Cic in
-   let curi,metasenv,pbo,pty = proof in
+let clear_one ~hyp =
+ let clear_one (proof, goal) =
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,context,ty =
      CicUtil.lookup_meta goal metasenv
     in
@@ -130,7 +129,7 @@ let clear ~hyp =
                             CicUniv.empty_ugraph
                           with _ ->
                            raise
-                            (Fail
+                            (PET.Fail
                               (lazy ("Hypothesis " ^ string_of_name n ^
                                " uses hypothesis " ^ hyp)))
                          in
@@ -140,56 +139,58 @@ let clear ~hyp =
                ) canonical_context (false, [])
              in
              if not context_changed then
-               raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
+               raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
              let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
                  CicUniv.empty_ugraph 
                with _ ->
-                raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
+                raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
               in
                m,canonical_context',ty
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
-  mk_tactic (clear ~hyp)
+  PET.mk_tactic clear_one
+
+let clear ~hyps =
+   let clear status =
+      let aux status hyp = 
+         match PET.apply_tactic (clear_one ~hyp) status with
+           | proof, [g] -> proof, g
+           | _          -> raise (PET.Fail (lazy "clear: internal error"))
+      in
+      let proof, g = List.fold_left aux status hyps in
+      proof, [g]
+   in
+   PET.mk_tactic clear
 
 (* Warning: this tactic has no effect on the proof term.
    It just changes the name of an hypothesis in the current sequent *)
-let rename ~from ~to_ =
- let rename ~from ~to_ (proof, goal) =
-  let module C = Cic in
-   let curi,metasenv,pbo,pty = proof in
-    let metano,context,ty =
-     CicUtil.lookup_meta goal metasenv
-    in
-     let metasenv' =
-      List.map
-       (function
-           (m,canonical_context,ty) when m = metano ->
-             let canonical_context' =
-              List.map
-               (function
-                   Some (Cic.Name hyp,decl_or_def) when hyp = from ->
-                    Some (Cic.Name to_,decl_or_def)
-                 | item -> item
-               ) canonical_context
-             in
-              m,canonical_context',ty
-         | t -> t
-       ) metasenv
-     in
-      (curi,metasenv',pbo,pty), [goal]
- in
-  mk_tactic (rename ~from ~to_)
-
-let set_goal n =
-  ProofEngineTypes.mk_tactic
-    (fun (proof, goal) ->
-       let (_, metasenv, _, _) = proof in
-       if CicUtil.exists_meta n metasenv then
-         (proof, [n])
-       else
-         raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))
+let rename ~froms ~tos =
+   let rename (proof, goal) =
+      let error = "rename: lists of different length" in
+      let assocs = 
+         try List.combine froms tos
+        with Invalid_argument _ -> raise (PET.Fail (lazy error))
+      in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
+      let metano, _, _ = CicUtil.lookup_meta goal metasenv in      
+      let rename_map = function
+         | Some (Cic.Name hyp, decl_or_def) as entry ->
+           begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
+           with Not_found -> entry end
+         | entry -> entry
+      in
+      let map = function
+         | m, canonical_context, ty when m = metano ->
+           let canonical_context = List.map rename_map canonical_context in
+            m, canonical_context, ty
+         | conjecture -> conjecture
+      in
+      let metasenv = List.map map metasenv in
+      (curi, metasenv, _subst, pbo, pty, attrs), [goal]
+   in
+   PET.mk_tactic rename