helm/ocaml/tactics/reductionTactics.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 (* The default of term is the thesis of the goal to be prooved *)
  29 let reduction_tac ~reduction ~pattern:(what,hyp_patterns,goal_pattern)
  30  (proof,goal)
  31 =
  32   let curi,metasenv,pbo,pty = proof in
  33   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  34   let replace where terms =
  35    let terms, terms' =
  36      List.split (List.map (fun (context, t) -> t, reduction context t) terms)
  37    in
  38     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
  39      ~where:where in
  40   let find_pattern_for name =
  41     try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
  42     with Not_found -> None in
  43   let ty' =
  44    let terms =
  45     ProofEngineHelpers.select ~context ~term:ty ~pattern:(what,goal_pattern)
  46    in
  47     replace ty terms in
  48   let context_len = List.length context in
  49   let context' =
  50     if hyp_patterns <> [] then
  51     List.fold_right
  52      (fun entry context ->
  53        match entry with
  54          None -> None::context
  55        | Some (name,Cic.Decl term) ->
  56            (match find_pattern_for name with
  57            | None -> entry::context
  58            | Some pat ->
  59               try
  60                let what =
  61                 match what with
  62                    None -> None
  63                  | Some what ->
  64                     let what,subst',metasenv' =
  65                      CicMetaSubst.delift_rels [] metasenv
  66                       (context_len - List.length context) what
  67                     in
  68                      assert (subst' = []);
  69                      assert (metasenv' = metasenv);
  70                      Some what in
  71                let terms =
  72                 ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in
  73                let term' = replace term terms in
  74                 Some (name,Cic.Decl term') :: context
  75               with
  76                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
  77                 raise
  78                  (ProofEngineTypes.Fail
  79                    ("The term the user wants to convert is not closed " ^
  80                     "in the context of the position of the substitution.")))
  81        | Some (name,Cic.Def (term, ty)) ->
  82            (match find_pattern_for name with
  83            | None -> entry::context
  84            | Some pat ->
  85               try
  86                let what =
  87                 match what with
  88                    None -> None
  89                  | Some what ->
  90                     let what,subst',metasenv' =
  91                      CicMetaSubst.delift_rels [] metasenv
  92                       (context_len - List.length context) what
  93                     in
  94                      assert (subst' = []);
  95                      assert (metasenv' = metasenv);
  96                      Some what in
  97                let terms =
  98                 ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in
  99                let term' = replace term terms in
 100                let ty' =
 101                 match ty with
 102                    None -> None
 103                  | Some ty ->
 104                     let terms =
 105                      ProofEngineHelpers.select
 106                       ~context ~term:ty ~pattern:(what,pat)
 107                     in
 108                      Some (replace ty terms)
 109                in
 110                 Some (name,Cic.Def (term',ty')) :: context
 111               with
 112                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 113                 raise
 114                  (ProofEngineTypes.Fail
 115                    ("The term the user wants to convert is not closed " ^
 116                     "in the context of the position of the substitution.")))
 117      ) context []
 118    else
 119     context
 120   in
 121   let metasenv' =
 122     List.map (function
 123       | (n,_,_) when n = metano -> (metano,context',ty')
 124       | _ as t -> t
 125     ) metasenv
 126   in
 127   (curi,metasenv',pbo,pty), [metano]
 128 ;;
 129
 130 let simpl_tac ~pattern =
 131  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
 132
 133 let reduce_tac ~pattern =
 134  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
 135
 136 let whd_tac ~pattern =
 137  mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
 138
 139 let normalize_tac ~pattern =
 140  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
 141
 142 let fold_tac ~reduction ~pattern =
 143 (*
 144  let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
 145  =
 146   let curi,metasenv,pbo,pty = proof in
 147   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 148    let term' = reduction context term in
 149     let replace =
 150      ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
 151     in
 152      let ty' = replace ty in
 153      let metasenv' =
 154       let context' =
 155        if also_in_hypotheses then
 156         List.map
 157          (function
 158              Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
 159            | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
 160            | None -> None
 161            | Some (_,Cic.Def (_,Some _)) -> assert false
 162          ) context
 163        else
 164         context
 165       in
 166        List.map
 167         (function
 168             (n,_,_) when n = metano -> (metano,context',ty')
 169           | _ as t -> t
 170         ) metasenv
 171
 172      in
 173       (curi,metasenv',pbo,pty), [metano]
 174  in
 175   mk_tactic (fold_tac ~reduction ~pattern ~term)
 176 *) assert false
 177 ;;