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 (n,Cic.Def (te,Some ty)) ->
  79                      (try
  80                        ignore
  81                         (CicTypeChecker.type_of_aux' metasenv context te
  82                           CicUniv.empty_ugraph (* TASSI: FIXME *));
  83                        ignore
  84                         (CicTypeChecker.type_of_aux' metasenv context ty
  85                           CicUniv.empty_ugraph (* TASSI: FIXME *));
  86                       with
  87                        _ ->
  88                          raise
  89                           (PET.Fail
  90                             (lazy ("The correctness of hypothesis " ^
  91                              string_of_name n ^
  92                              " relies on the body of " ^ hyp)
  93                           )));
  94                      entry::context
  95                ) canonical_context []
  96              in
  97               let _,_ =
  98                try
  99                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 100                  CicUniv.empty_ugraph (* TASSI: FIXME *)
 101                with
 102                 _ ->
 103                  raise
 104                   (PET.Fail
 105                    (lazy ("The correctness of the goal relies on the body of " ^
 106                     hyp)))
 107               in
 108                m,canonical_context',ty
 109          | t -> t
 110        ) metasenv
 111      in
 112       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
 113  in
 114   PET.mk_tactic clearbody
 115
 116 let clear_one ~hyp =
 117  let clear_one (proof, goal) =
 118    let curi,metasenv,_subst,pbo,pty, attrs = proof in
 119     let metano,context,ty =
 120      CicUtil.lookup_meta goal metasenv
 121     in
 122      let string_of_name =
 123       function
 124          C.Name n -> n
 125        | C.Anonymous -> "_"
 126      in
 127      let metasenv' =
 128       List.map
 129        (function
 130            (m,canonical_context,ty) when m = metano ->
 131              let context_changed, canonical_context' =
 132               List.fold_right
 133                (fun entry (b, context) ->
 134                  match entry with
 135                     Some (Cic.Name hyp',_) when hyp' = hyp ->
 136                       (true, None::context)
 137                   | None -> (b, None::context)
 138                   | Some (n,C.Decl t)
 139                   | Some (n,Cic.Def (t,Some _))
 140                   | Some (n,C.Def (t,None)) ->
 141                       if b then
 142                          let _,_ =
 143                           try
 144                            CicTypeChecker.type_of_aux' metasenv context t
 145                             CicUniv.empty_ugraph
 146                           with _ ->
 147                            raise
 148                             (PET.Fail
 149                               (lazy ("Hypothesis " ^ string_of_name n ^
 150                                " uses hypothesis " ^ hyp)))
 151                          in
 152                           (b, entry::context)
 153                       else
 154                         (b, entry::context)
 155                ) canonical_context (false, [])
 156              in
 157              if not context_changed then
 158                raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
 159              let _,_ =
 160                try
 161                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 162                  CicUniv.empty_ugraph
 163                with _ ->
 164                 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
 165               in
 166                m,canonical_context',ty
 167          | t -> t
 168        ) metasenv
 169      in
 170       (curi,metasenv',_subst,pbo,pty, attrs), [goal]
 171  in
 172   PET.mk_tactic clear_one
 173
 174 let clear ~hyps =
 175    let clear status =
 176       let aux status hyp =
 177          match PET.apply_tactic (clear_one ~hyp) status with
 178             | proof, [g] -> proof, g
 179             | _          -> raise (PET.Fail (lazy "clear: internal error"))
 180       in
 181       let proof, g = List.fold_left aux status hyps in
 182       proof, [g]
 183    in
 184    PET.mk_tactic clear
 185
 186 (* Warning: this tactic has no effect on the proof term.
 187    It just changes the name of an hypothesis in the current sequent *)
 188 let rename ~froms ~tos =
 189    let rename (proof, goal) =
 190       let error = "rename: lists of different length" in
 191       let assocs =
 192          try List.combine froms tos
 193          with Invalid_argument _ -> raise (PET.Fail (lazy error))
 194       in
 195       let curi, metasenv, _subst, pbo, pty, attrs = proof in
 196       let metano, _, _ = CicUtil.lookup_meta goal metasenv in
 197       let rename_map = function
 198          | Some (Cic.Name hyp, decl_or_def) as entry ->
 199             begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
 200             with Not_found -> entry end
 201          | entry -> entry
 202       in
 203       let map = function
 204          | m, canonical_context, ty when m = metano ->
 205             let canonical_context = List.map rename_map canonical_context in
 206             m, canonical_context, ty
 207          | conjecture -> conjecture
 208       in
 209       let metasenv = List.map map metasenv in
 210       (curi, metasenv, _subst, pbo, pty, attrs), [goal]
 211    in
 212    PET.mk_tactic rename