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