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