helm/ocaml/tactics/proofEngineStructuralRules.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open ProofEngineTypes
  27
  28 let clearbody ~hyp (proof, goal) =
  29  let module C = Cic in
  30   match hyp with
  31      None -> assert false
  32    | Some (_, C.Def (_, Some _)) -> assert false
  33    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
  34    | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
  35       let curi,metasenv,pbo,pty = proof in
  36        let metano,_,_ = CicUtil.lookup_meta goal metasenv in
  37         let string_of_name =
  38          function
  39             C.Name n -> n
  40           | C.Anonymous -> "_"
  41         in
  42         let metasenv' =
  43          List.map
  44           (function
  45               (m,canonical_context,ty) when m = metano ->
  46                 let canonical_context' =
  47                  List.fold_right
  48                   (fun entry context ->
  49                     match entry with
  50                        t when t == hyp_to_clear_body ->
  51                         let cleared_entry =
  52                          let ty =
  53                           CicTypeChecker.type_of_aux' metasenv context term
  54                          in
  55                           Some (n_to_clear_body, Cic.Decl ty)
  56                         in
  57                          cleared_entry::context
  58                      | None -> None::context
  59                      | Some (n,C.Decl t)
  60                      | Some (n,C.Def (t,None)) ->
  61                         let _ =
  62                          try
  63                           CicTypeChecker.type_of_aux' metasenv context t
  64                          with
  65                           _ ->
  66                             raise
  67                              (Fail
  68                                ("The correctness of hypothesis " ^
  69                                 string_of_name n ^
  70                                 " relies on the body of " ^
  71                                 string_of_name n_to_clear_body)
  72                              )
  73                         in
  74                          entry::context
  75                      | Some (_,Cic.Def (_,Some _)) -> assert false
  76                   ) canonical_context []
  77                 in
  78                  let _ =
  79                   try
  80                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
  81                   with
  82                    _ ->
  83                     raise
  84                      (Fail
  85                       ("The correctness of the goal relies on the body of " ^
  86                        string_of_name n_to_clear_body))
  87                  in
  88                   m,canonical_context',ty
  89             | t -> t
  90           ) metasenv
  91         in
  92          (curi,metasenv',pbo,pty), [goal]
  93
  94 let clear ~hyp:hyp_to_clear (proof, goal) =
  95  let module C = Cic in
  96   match hyp_to_clear with
  97      None -> assert false
  98    | Some (n_to_clear, _) ->
  99       let curi,metasenv,pbo,pty = proof in
 100        let metano,context,ty =
 101         CicUtil.lookup_meta goal metasenv
 102        in
 103         let string_of_name =
 104          function
 105             C.Name n -> n
 106           | C.Anonymous -> "_"
 107         in
 108         let metasenv' =
 109          List.map
 110           (function
 111               (m,canonical_context,ty) when m = metano ->
 112                 let canonical_context' =
 113                  List.fold_right
 114                   (fun entry context ->
 115                     match entry with
 116                        t when t == hyp_to_clear -> None::context
 117                      | None -> None::context
 118                      | Some (_,Cic.Def (_,Some _)) -> assert false
 119                      | Some (n,C.Decl t)
 120                      | Some (n,C.Def (t,None)) ->
 121                         let _ =
 122                          try
 123                           CicTypeChecker.type_of_aux' metasenv context t
 124                          with
 125                           _ ->
 126                             raise
 127                              (Fail
 128                                ("Hypothesis " ^
 129                                 string_of_name n ^
 130                                 " uses hypothesis " ^
 131                                 string_of_name n_to_clear)
 132                              )
 133                         in
 134                          entry::context
 135                   ) canonical_context []
 136                 in
 137                  let _ =
 138                   try
 139                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 140                   with
 141                    _ ->
 142                     raise
 143                      (Fail
 144                       ("Hypothesis " ^ string_of_name n_to_clear ^
 145                        " occurs in the goal"))
 146                  in
 147                   m,canonical_context',ty
 148             | t -> t
 149           ) metasenv
 150         in
 151          (curi,metasenv',pbo,pty), [goal]
 152