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 open ProofEngineTypes
  29
  30 let clearbody ~hyp =
  31  let clearbody ~hyp (proof, goal) =
  32   let module C = Cic in
  33    let curi,metasenv,pbo,pty = 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                           (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                   (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',pbo,pty), [goal]
  97  in
  98   mk_tactic (clearbody ~hyp)
  99
 100 let clear_one ~hyp =
 101  let clear_one ~hyp (proof, goal) =
 102   let module C = Cic in
 103    let curi,metasenv,pbo,pty = proof in
 104     let metano,context,ty =
 105      CicUtil.lookup_meta goal metasenv
 106     in
 107      let string_of_name =
 108       function
 109          C.Name n -> n
 110        | C.Anonymous -> "_"
 111      in
 112      let metasenv' =
 113       List.map
 114        (function
 115            (m,canonical_context,ty) when m = metano ->
 116              let context_changed, canonical_context' =
 117               List.fold_right
 118                (fun entry (b, context) ->
 119                  match entry with
 120                     Some (Cic.Name hyp',_) when hyp' = hyp ->
 121                       (true, None::context)
 122                   | None -> (b, None::context)
 123                   | Some (n,C.Decl t)
 124                   | Some (n,Cic.Def (t,Some _))
 125                   | Some (n,C.Def (t,None)) ->
 126                       if b then
 127                          let _,_ =
 128                           try
 129                            CicTypeChecker.type_of_aux' metasenv context t
 130                             CicUniv.empty_ugraph
 131                           with _ ->
 132                            raise
 133                             (Fail
 134                               (lazy ("Hypothesis " ^ string_of_name n ^
 135                                " uses hypothesis " ^ hyp)))
 136                          in
 137                           (b, entry::context)
 138                       else
 139                         (b, entry::context)
 140                ) canonical_context (false, [])
 141              in
 142              if not context_changed then
 143                raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
 144              let _,_ =
 145                try
 146                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 147                  CicUniv.empty_ugraph
 148                with _ ->
 149                 raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
 150               in
 151                m,canonical_context',ty
 152          | t -> t
 153        ) metasenv
 154      in
 155       (curi,metasenv',pbo,pty), [goal]
 156  in
 157   mk_tactic (clear_one ~hyp)
 158
 159 let clear ~hyps =
 160    let clear hyps status =
 161       let aux status hyp =
 162          match apply_tactic (clear_one ~hyp) status with
 163             | proof, [g] -> proof, g
 164             | _          -> raise (Fail (lazy "clear: internal error"))
 165       in
 166       let proof, g = List.fold_left aux status hyps in
 167       proof, [g]
 168    in
 169    mk_tactic (clear hyps)
 170
 171 (* Warning: this tactic has no effect on the proof term.
 172    It just changes the name of an hypothesis in the current sequent *)
 173 let rename ~from ~to_ =
 174  let rename ~from ~to_ (proof, goal) =
 175   let module C = Cic in
 176    let curi,metasenv,pbo,pty = proof in
 177     let metano,context,ty =
 178      CicUtil.lookup_meta goal metasenv
 179     in
 180      let metasenv' =
 181       List.map
 182        (function
 183            (m,canonical_context,ty) when m = metano ->
 184              let canonical_context' =
 185               List.map
 186                (function
 187                    Some (Cic.Name hyp,decl_or_def) when hyp = from ->
 188                     Some (Cic.Name to_,decl_or_def)
 189                  | item -> item
 190                ) canonical_context
 191              in
 192               m,canonical_context',ty
 193          | t -> t
 194        ) metasenv
 195      in
 196       (curi,metasenv',pbo,pty), [goal]
 197  in
 198   mk_tactic (rename ~from ~to_)
 199
 200 let set_goal n =
 201   ProofEngineTypes.mk_tactic
 202     (fun (proof, goal) ->
 203        let (_, metasenv, _, _) = proof in
 204        if CicUtil.exists_meta n metasenv then
 205          (proof, [n])
 206        else
 207          raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))