- tactics:

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

diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml
index b1e23751f413afb1b7280bc56a2b1879ca943f73..acc4bb1640ac112819ff403e2728d34f3ffe864f 100644 (file)
--- a/components/tactics/proofEngineStructuralRules.ml
+++ b/components/tactics/proofEngineStructuralRules.ml
@@ -25,11 +25,11 @@
 
 (* $Id$ *)
 
-open ProofEngineTypes
+module PET = ProofEngineTypes
+module C = Cic
 
 let clearbody ~hyp = 
- let clearbody ~hyp (proof, goal) =
-  let module C = Cic in
+ let clearbody (proof, goal) =
    let curi,metasenv,pbo,pty = proof in
     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
      let string_of_name =
@@ -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
@@ -95,11 +95,10 @@ let clearbody ~hyp =
      in
       (curi,metasenv',pbo,pty), [goal]
  in
-  mk_tactic (clearbody ~hyp)
+  PET.mk_tactic clearbody
 
 let clear_one ~hyp =
- let clear_one ~hyp (proof, goal) =
-  let module C = Cic in
+ let clear_one (proof, goal) =
    let curi,metasenv,pbo,pty = proof in
     let metano,context,ty =
      CicUtil.lookup_meta goal metasenv
@@ -130,7 +129,7 @@ let clear_one ~hyp =
                             CicUniv.empty_ugraph
                           with _ ->
                            raise
-                            (Fail
+                            (PET.Fail
                               (lazy ("Hypothesis " ^ string_of_name n ^
                                " uses hypothesis " ^ hyp)))
                          in
@@ -140,13 +139,13 @@ let clear_one ~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
@@ -154,54 +153,53 @@ let clear_one ~hyp =
      in
       (curi,metasenv',pbo,pty), [goal]
  in
-  mk_tactic (clear_one ~hyp)
+  PET.mk_tactic clear_one
 
 let clear ~hyps =
-   let clear hyps status =
+   let clear status =
       let aux status hyp = 
-         match apply_tactic (clear_one ~hyp) status with
+         match PET.apply_tactic (clear_one ~hyp) status with
            | proof, [g] -> proof, g
-           | _          -> raise (Fail (lazy "clear: internal error"))
+           | _          -> raise (PET.Fail (lazy "clear: internal error"))
       in
       let proof, g = List.fold_left aux status hyps in
       proof, [g]
    in
-   mk_tactic (clear hyps)
+   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 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, pbo, pty = 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, pbo, pty), [goal]
+   in
+   PET.mk_tactic rename
 
 let set_goal n =
-  ProofEngineTypes.mk_tactic
+  PET.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))))
+         raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))