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