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