helm/software/components/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 (* $Id$ *)
  27
  28 module PET = ProofEngineTypes
  29 module C = Cic
  30
  31 let clearbody ~hyp =
  32  let clearbody (proof, goal) =
  33    let curi,metasenv,_subst,pbo,pty, attrs = proof in
  34     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
  35      let string_of_name =
  36       function
  37          C.Name n -> n
  38        | C.Anonymous -> "_"
  39      in
  40      let metasenv' =
  41       List.map
  42        (function
  43            (m,canonical_context,ty) when m = metano ->
  44              let canonical_context' =
  45               List.fold_right
  46                (fun entry context ->
  47                  match entry with
  48                     Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
  49                      let cleared_entry =
  50                       let ty =
  51                        match ty with
  52                           Some ty -> ty
  53                         | None ->
  54                            fst
  55                             (CicTypeChecker.type_of_aux' metasenv context term
  56                               CicUniv.empty_ugraph) (* TASSI: FIXME *)
  57                       in
  58                        Some (C.Name hyp, Cic.Decl ty)
  59                      in
  60                       cleared_entry::context
  61                   | None -> None::context
  62                   | Some (n,C.Decl t)
  63                   | Some (n,C.Def (t,None)) ->
  64                      let _,_ =
  65                       try
  66                        CicTypeChecker.type_of_aux' metasenv context t
  67                         CicUniv.empty_ugraph (* TASSI: FIXME *)
  68                       with
  69                        _ ->
  70                          raise
  71                           (PET.Fail
  72                             (lazy ("The correctness of hypothesis " ^
  73                              string_of_name n ^
  74                              " relies on the body of " ^ hyp)
  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                   (PET.Fail
  89                    (lazy ("The correctness of the goal relies on the body of " ^
  90                     hyp)))
  91               in
  92                m,canonical_context',ty
  93          | t -> t
  94        ) metasenv
  95      in
  96       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  97  in
  98   PET.mk_tactic clearbody
  99
 100 let clear_one ~hyp =
 101  let clear_one (proof, goal) =
 102    let curi,metasenv,_subst,pbo,pty, attrs = proof in
 103     let metano,context,ty =
 104      CicUtil.lookup_meta goal metasenv
 105     in
 106      let string_of_name =
 107       function
 108          C.Name n -> n
 109        | C.Anonymous -> "_"
 110      in
 111      let metasenv' =
 112       List.map
 113        (function
 114            (m,canonical_context,ty) when m = metano ->
 115              let context_changed, canonical_context' =
 116               List.fold_right
 117                (fun entry (b, context) ->
 118                  match entry with
 119                     Some (Cic.Name hyp',_) when hyp' = hyp ->
 120                       (true, None::context)
 121                   | None -> (b, None::context)
 122                   | Some (n,C.Decl t)
 123                   | Some (n,Cic.Def (t,Some _))
 124                   | Some (n,C.Def (t,None)) ->
 125                       if b then
 126                          let _,_ =
 127                           try
 128                            CicTypeChecker.type_of_aux' metasenv context t
 129                             CicUniv.empty_ugraph
 130                           with _ ->
 131                            raise
 132                             (PET.Fail
 133                               (lazy ("Hypothesis " ^ string_of_name n ^
 134                                " uses hypothesis " ^ hyp)))
 135                          in
 136                           (b, entry::context)
 137                       else
 138                         (b, entry::context)
 139                ) canonical_context (false, [])
 140              in
 141              if not context_changed then
 142                raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
 143              let _,_ =
 144                try
 145                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 146                  CicUniv.empty_ugraph
 147                with _ ->
 148                 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
 149               in
 150                m,canonical_context',ty
 151          | t -> t
 152        ) metasenv
 153      in
 154       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
 155  in
 156   PET.mk_tactic clear_one
 157
 158 let clear ~hyps =
 159    let clear status =
 160       let aux status hyp =
 161          match PET.apply_tactic (clear_one ~hyp) status with
 162             | proof, [g] -> proof, g
 163             | _          -> raise (PET.Fail (lazy "clear: internal error"))
 164       in
 165       let proof, g = List.fold_left aux status hyps in
 166       proof, [g]
 167    in
 168    PET.mk_tactic clear
 169
 170 (* Warning: this tactic has no effect on the proof term.
 171    It just changes the name of an hypothesis in the current sequent *)
 172 let rename ~froms ~tos =
 173    let rename (proof, goal) =
 174       let error = "rename: lists of different length" in
 175       let assocs =
 176          try List.combine froms tos
 177          with Invalid_argument _ -> raise (PET.Fail (lazy error))
 178       in
 179       let curi, metasenv, _subst, pbo, pty, attrs = proof in
 180       let metano, _, _ = CicUtil.lookup_meta goal metasenv in
 181       let rename_map = function
 182          | Some (Cic.Name hyp, decl_or_def) as entry ->
 183             begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
 184             with Not_found -> entry end
 185          | entry -> entry
 186       in
 187       let map = function
 188          | m, canonical_context, ty when m = metano ->
 189             let canonical_context = List.map rename_map canonical_context in
 190             m, canonical_context, ty
 191          | conjecture -> conjecture
 192       in
 193       let metasenv = List.map map metasenv in
 194       (curi, metasenv, _subst, pbo, pty, attrs), [goal]
 195    in
 196    PET.mk_tactic rename