helm/gTopLevel/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 ~status:(proof, goal) ~hyp =
  29  let module C = Cic in
  30   match hyp with
  31      None -> assert false
  32    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
  33    | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
  34       let curi,metasenv,pbo,pty =
  35        match proof with
  36           None -> assert false
  37         | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
  38       in
  39        let metano,_,_ =
  40         match goal with
  41            None -> assert false
  42          | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
  43        in
  44         let string_of_name =
  45          function
  46             C.Name n -> n
  47           | C.Anonimous -> "_"
  48         in
  49         let metasenv' =
  50          List.map
  51           (function
  52               (m,canonical_context,ty) when m = metano ->
  53                 let canonical_context' =
  54                  List.fold_right
  55                   (fun entry context ->
  56                     match entry with
  57                        t when t == hyp_to_clear_body ->
  58                         let cleared_entry =
  59                          let ty =
  60                           CicTypeChecker.type_of_aux' metasenv context term
  61                          in
  62                           Some (n_to_clear_body, Cic.Decl ty)
  63                         in
  64                          cleared_entry::context
  65                      | None -> None::context
  66                      | Some (n,C.Decl t)
  67                      | Some (n,C.Def t) ->
  68                         let _ =
  69                          try
  70                           CicTypeChecker.type_of_aux' metasenv context t
  71                          with
  72                           _ ->
  73                             raise
  74                              (Fail
  75                                ("The correctness of hypothesis " ^
  76                                 string_of_name n ^
  77                                 " relies on the body of " ^
  78                                 string_of_name n_to_clear_body)
  79                              )
  80                         in
  81                          entry::context
  82                   ) canonical_context []
  83                 in
  84                  let _ =
  85                   try
  86                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
  87                   with
  88                    _ ->
  89                     raise
  90                      (Fail
  91                       ("The correctness of the goal relies on the body of " ^
  92                        string_of_name n_to_clear_body))
  93                  in
  94                   m,canonical_context',ty
  95             | t -> t
  96           ) metasenv
  97         in
  98          (Some (curi,metasenv',pbo,pty), goal)
  99
 100 let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
 101  let module C = Cic in
 102   match hyp_to_clear with
 103      None -> assert false
 104    | Some (n_to_clear, _) ->
 105       let curi,metasenv,pbo,pty =
 106        match proof with
 107           None -> assert false
 108         | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 109       in
 110        let metano,context,ty =
 111         match goal with
 112            None -> assert false
 113          | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 114        in
 115         let string_of_name =
 116          function
 117             C.Name n -> n
 118           | C.Anonimous -> "_"
 119         in
 120         let metasenv' =
 121          List.map
 122           (function
 123               (m,canonical_context,ty) when m = metano ->
 124                 let canonical_context' =
 125                  List.fold_right
 126                   (fun entry context ->
 127                     match entry with
 128                        t when t == hyp_to_clear -> None::context
 129                      | None -> None::context
 130                      | Some (n,C.Decl t)
 131                      | Some (n,C.Def t) ->
 132                         let _ =
 133                          try
 134                           CicTypeChecker.type_of_aux' metasenv context t
 135                          with
 136                           _ ->
 137                             raise
 138                              (Fail
 139                                ("Hypothesis " ^
 140                                 string_of_name n ^
 141                                 " uses hypothesis " ^
 142                                 string_of_name n_to_clear)
 143                              )
 144                         in
 145                          entry::context
 146                   ) canonical_context []
 147                 in
 148                  let _ =
 149                   try
 150                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 151                   with
 152                    _ ->
 153                     raise
 154                      (Fail
 155                       ("Hypothesis " ^ string_of_name n_to_clear ^
 156                        " occurs in the goal"))
 157                  in
 158                   m,canonical_context',ty
 159             | t -> t
 160           ) metasenv
 161         in
 162          (Some (curi,metasenv',pbo,pty), goal)
 163