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
  30  (proof,goal)
  31 =
  32   let curi,metasenv,pbo,pty = proof in
  33   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
  34   let replace where terms =
  35    if terms = [] then where
  36    else
  37     let terms, terms' =
  38       List.split (List.map (fun (context, t) -> t, reduction context t) terms)
  39     in
  40      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
  41       ~where:where in
  42   let (selected_context,selected_ty) =
  43    ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
  44   let ty' = replace ty selected_ty in
  45   let context' =
  46    List.fold_right2
  47     (fun entry selected_entry context' ->
  48       match entry,selected_entry with
  49          None,None -> None::context'
  50        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
  51           let ty' = replace ty selected_ty in
  52            Some (name,Cic.Decl ty')::context'
  53        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
  54           let bo' = replace bo selected_bo in
  55           let ty' =
  56            match ty,selected_ty with
  57               None,None -> None
  58             | Some ty,Some selected_ty -> Some (replace ty selected_ty)
  59             | _,_ -> assert false
  60           in
  61            Some (name,Cic.Def (bo',ty'))::context'
  62        | _,_ -> assert false
  63     ) context selected_context [] in
  64   let metasenv' =
  65     List.map (function
  66       | (n,_,_) when n = metano -> (metano,context',ty')
  67       | _ as t -> t
  68     ) metasenv
  69   in
  70   (curi,metasenv',pbo,pty), [metano]
  71 ;;
  72
  73 let simpl_tac ~pattern =
  74  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
  75
  76 let reduce_tac ~pattern =
  77  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
  78
  79 let whd_tac ~pattern =
  80  mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
  81
  82 let normalize_tac ~pattern =
  83  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
  84
  85 let fold_tac ~reduction ~pattern =
  86 (*
  87  let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
  88  =
  89   let curi,metasenv,pbo,pty = proof in
  90   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  91    let term' = reduction context term in
  92     let replace =
  93      ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
  94     in
  95      let ty' = replace ty in
  96      let metasenv' =
  97       let context' =
  98        if also_in_hypotheses then
  99         List.map
 100          (function
 101              Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
 102            | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
 103            | None -> None
 104            | Some (_,Cic.Def (_,Some _)) -> assert false
 105          ) context
 106        else
 107         context
 108       in
 109        List.map
 110         (function
 111             (n,_,_) when n = metano -> (metano,context',ty')
 112           | _ as t -> t
 113         ) metasenv
 114
 115      in
 116       (curi,metasenv',pbo,pty), [metano]
 117  in
 118   mk_tactic (fold_tac ~reduction ~pattern ~term)
 119 *) assert false
 120 ;;