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                             (lazy ("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                    (lazy ("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 context_changed, canonical_context' =
 115               List.fold_right
 116                (fun entry (b, context) ->
 117                  match entry with
 118                     Some (Cic.Name hyp',_) when hyp' = hyp ->
 119                       (true, None::context)
 120                   | None -> (b, None::context)
 121                   | Some (n,C.Decl t)
 122                   | Some (n,Cic.Def (t,Some _))
 123                   | Some (n,C.Def (t,None)) ->
 124                       if b then
 125                          let _,_ =
 126                           try
 127                            CicTypeChecker.type_of_aux' metasenv context t
 128                             CicUniv.empty_ugraph
 129                           with _ ->
 130                            raise
 131                             (Fail
 132                               (lazy ("Hypothesis " ^ string_of_name n ^
 133                                " uses hypothesis " ^ hyp)))
 134                          in
 135                           (b, entry::context)
 136                       else
 137                         (b, entry::context)
 138                ) canonical_context (false, [])
 139              in
 140              if not context_changed then
 141                raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
 142              let _,_ =
 143                try
 144                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 145                  CicUniv.empty_ugraph
 146                with _ ->
 147                 raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
 148               in
 149                m,canonical_context',ty
 150          | t -> t
 151        ) metasenv
 152      in
 153       (curi,metasenv',pbo,pty), [goal]
 154  in
 155   mk_tactic (clear ~hyp)
 156
 157 (* Warning: this tactic has no effect on the proof term.
 158    It just changes the name of an hypothesis in the current sequent *)
 159 let rename ~from ~to_ =
 160  let rename ~from ~to_ (proof, goal) =
 161   let module C = Cic in
 162    let curi,metasenv,pbo,pty = proof in
 163     let metano,context,ty =
 164      CicUtil.lookup_meta goal metasenv
 165     in
 166      let metasenv' =
 167       List.map
 168        (function
 169            (m,canonical_context,ty) when m = metano ->
 170              let canonical_context' =
 171               List.map
 172                (function
 173                    Some (Cic.Name hyp,decl_or_def) when hyp = from ->
 174                     Some (Cic.Name to_,decl_or_def)
 175                  | item -> item
 176                ) canonical_context
 177              in
 178               m,canonical_context',ty
 179          | t -> t
 180        ) metasenv
 181      in
 182       (curi,metasenv',pbo,pty), [goal]
 183  in
 184   mk_tactic (rename ~from ~to_)
 185
 186 let set_goal n =
 187   ProofEngineTypes.mk_tactic
 188     (fun (proof, goal) ->
 189        let (_, metasenv, _, _) = proof in
 190        if CicUtil.exists_meta n metasenv then
 191          (proof, [n])
 192        else
 193          raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))