Merge of the V7_3_new_exportation branch.

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

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
new file mode 100644 (file)
index 0000000..d89420f
--- /dev/null
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -0,0 +1,149 @@
+(* Copyright (C) 2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+open ProofEngineTypes
+
+let clearbody ~hyp ~status:(proof, goal) =
+ let module C = Cic in
+  match hyp with
+     None -> assert false
+   | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
+   | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+      let curi,metasenv,pbo,pty = proof in
+       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+        let string_of_name =
+         function
+            C.Name n -> n
+          | C.Anonymous -> "_"
+        in
+        let metasenv' =
+         List.map
+          (function
+              (m,canonical_context,ty) when m = metano ->
+                let canonical_context' =
+                 List.fold_right
+                  (fun entry context ->
+                    match entry with
+                       t when t == hyp_to_clear_body ->
+                        let cleared_entry =
+                         let ty =
+                          CicTypeChecker.type_of_aux' metasenv context term
+                         in
+                          Some (n_to_clear_body, Cic.Decl ty)
+                        in
+                         cleared_entry::context
+                     | None -> None::context
+                     | Some (n,C.Decl t)
+                     | Some (n,C.Def t) ->
+                        let _ =
+                         try
+                          CicTypeChecker.type_of_aux' metasenv context t
+                         with
+                          _ ->
+                            raise
+                             (Fail
+                               ("The correctness of hypothesis " ^
+                                string_of_name n ^
+                                " relies on the body of " ^
+                                string_of_name n_to_clear_body)
+                             )
+                        in
+                         entry::context
+                  ) canonical_context []
+                in
+                 let _ =
+                  try
+                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+                  with
+                   _ ->
+                    raise
+                     (Fail
+                      ("The correctness of the goal relies on the body of " ^
+                       string_of_name n_to_clear_body))
+                 in
+                  m,canonical_context',ty
+            | t -> t
+          ) metasenv
+        in
+         (curi,metasenv',pbo,pty), [goal]
+
+let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
+ let module C = Cic in
+  match hyp_to_clear with
+     None -> assert false
+   | Some (n_to_clear, _) ->
+      let curi,metasenv,pbo,pty = proof in
+       let metano,context,ty =
+        List.find (function (m,_,_) -> m=goal) metasenv
+       in
+        let string_of_name =
+         function
+            C.Name n -> n
+          | C.Anonymous -> "_"
+        in
+        let metasenv' =
+         List.map
+          (function
+              (m,canonical_context,ty) when m = metano ->
+                let canonical_context' =
+                 List.fold_right
+                  (fun entry context ->
+                    match entry with
+                       t when t == hyp_to_clear -> None::context
+                     | None -> None::context
+                     | Some (n,C.Decl t)
+                     | Some (n,C.Def t) ->
+                        let _ =
+                         try
+                          CicTypeChecker.type_of_aux' metasenv context t
+                         with
+                          _ ->
+                            raise
+                             (Fail
+                               ("Hypothesis " ^
+                                string_of_name n ^
+                                " uses hypothesis " ^
+                                string_of_name n_to_clear)
+                             )
+                        in
+                         entry::context
+                  ) canonical_context []
+                in
+                 let _ =
+                  try
+                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+                  with
+                   _ ->
+                    raise
+                     (Fail
+                      ("Hypothesis " ^ string_of_name n_to_clear ^
+                       " occurs in the goal"))
+                 in
+                  m,canonical_context',ty
+            | t -> t
+          ) metasenv
+        in
+         (curi,metasenv',pbo,pty), [goal]
+