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    let curi,metasenv,pbo,pty = proof in
  32     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
  33      let string_of_name =
  34       function
  35          C.Name n -> n
  36        | C.Anonymous -> "_"
  37      in
  38      let metasenv' =
  39       List.map
  40        (function
  41            (m,canonical_context,ty) when m = metano ->
  42              let canonical_context' =
  43               List.fold_right
  44                (fun entry context ->
  45                  match entry with
  46                     Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
  47                      let cleared_entry =
  48                       let ty =
  49                        match ty with
  50                           Some ty -> ty
  51                         | None ->
  52                            fst
  53                             (CicTypeChecker.type_of_aux' metasenv context term
  54                               CicUniv.empty_ugraph) (* TASSI: FIXME *)
  55                       in
  56                        Some (C.Name hyp, 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                         CicUniv.empty_ugraph (* TASSI: FIXME *)
  66                       with
  67                        _ ->
  68                          raise
  69                           (Fail
  70                             ("The correctness of hypothesis " ^
  71                              string_of_name n ^
  72                              " relies on the body of " ^ hyp)
  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                  CicUniv.empty_ugraph (* TASSI: FIXME *)
  83                with
  84                 _ ->
  85                  raise
  86                   (Fail
  87                    ("The correctness of the goal relies on the body of " ^
  88                     hyp))
  89               in
  90                m,canonical_context',ty
  91          | t -> t
  92        ) metasenv
  93      in
  94       (curi,metasenv',pbo,pty), [goal]
  95  in
  96   mk_tactic (clearbody ~hyp)
  97
  98 let clear ~hyp =
  99  let clear ~hyp (proof, goal) =
 100   let module C = Cic in
 101    let curi,metasenv,pbo,pty = proof in
 102     let metano,context,ty =
 103      CicUtil.lookup_meta goal metasenv
 104     in
 105      let string_of_name =
 106       function
 107          C.Name n -> n
 108        | C.Anonymous -> "_"
 109      in
 110      let metasenv' =
 111       List.map
 112        (function
 113            (m,canonical_context,ty) when m = metano ->
 114              let canonical_context' =
 115               List.fold_right
 116                (fun entry context ->
 117                  match entry with
 118                     Some (Cic.Name hyp',_) when hyp' = hyp -> None::context
 119                   | None -> None::context
 120                   | Some (_,Cic.Def (_,Some _)) -> assert false
 121                   | Some (n,C.Decl t)
 122                   | Some (n,C.Def (t,None)) ->
 123                      let _,_ =
 124                       try
 125                        CicTypeChecker.type_of_aux' metasenv context t
 126                         CicUniv.empty_ugraph (* TASSI: FIXME *)
 127                       with _ ->
 128                        raise
 129                         (Fail
 130                           ("Hypothesis " ^ string_of_name n ^
 131                            " uses hypothesis " ^ hyp))
 132                      in
 133                       entry::context
 134                ) canonical_context []
 135              in
 136               let _,_ =
 137                try
 138                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 139                  CicUniv.empty_ugraph (* TASSI: FIXME *)
 140                with _ ->
 141                 raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal"))
 142               in
 143                m,canonical_context',ty
 144          | t -> t
 145        ) metasenv
 146      in
 147       (curi,metasenv',pbo,pty), [goal]
 148  in
 149   mk_tactic (clear ~hyp)
 150
 151 let set_goal n =
 152   ProofEngineTypes.mk_tactic
 153     (fun (proof, goal) ->
 154        let (_, metasenv, _, _) = proof in
 155        if CicUtil.exists_meta n metasenv then
 156          (proof, [n])
 157        else
 158          raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))