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 change_tac and
  29 *  it could be unified by making the change function a callback *)
  30 let reduction_tac ~reduction ~pattern (proof,goal) =
  31   let curi,metasenv,pbo,pty = proof in
  32   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
  33   let change where terms =
  34    if terms = [] then where
  35    else
  36     let terms, terms' =
  37       List.split (List.map (fun (context, t) -> t, reduction context t) terms)
  38     in
  39      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
  40       ~where:where in
  41   let (selected_context,selected_ty) =
  42    ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
  43   let ty' = change ty selected_ty in
  44   let context' =
  45    List.fold_right2
  46     (fun entry selected_entry context' ->
  47       match entry,selected_entry with
  48          None,None -> None::context'
  49        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
  50           let ty' = change ty selected_ty in
  51            Some (name,Cic.Decl ty')::context'
  52        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
  53           let bo' = change bo selected_bo in
  54           let ty' =
  55            match ty,selected_ty with
  56               None,None -> None
  57             | Some ty,Some selected_ty -> Some (change ty selected_ty)
  58             | _,_ -> assert false
  59           in
  60            Some (name,Cic.Def (bo',ty'))::context'
  61        | _,_ -> assert false
  62     ) context selected_context [] in
  63   let metasenv' =
  64     List.map (function
  65       | (n,_,_) when n = metano -> (metano,context',ty')
  66       | _ as t -> t
  67     ) metasenv
  68   in
  69   (curi,metasenv',pbo,pty), [metano]
  70 ;;
  71
  72 let simpl_tac ~pattern =
  73  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
  74
  75 let reduce_tac ~pattern =
  76  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
  77
  78 let whd_tac ~pattern =
  79  mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
  80
  81 let normalize_tac ~pattern =
  82  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
  83
  84 exception NotConvertible
  85
  86 (* Note: this code is almost identical to reduction_tac and
  87 *  it could be unified by making the change function a callback *)
  88 (* CSC: with_what is parsed in the context of the goal, but it should replace
  89         something that lives in a completely different context. Thus we
  90         perform a delift + lift phase to move it in the right context. However,
  91         in this way the tactic is less powerful than expected: with_what cannot
  92         reference variables that are local to the term that is going to be
  93         replaced. To fix this we should parse with_what in the context of the
  94         term(s) to be replaced. *)
  95 let change_tac ~pattern with_what  =
  96  let change_tac ~pattern ~with_what (proof, goal) =
  97   let curi,metasenv,pbo,pty = proof in
  98   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
  99   let context_len = List.length context in
 100   let change context'_len where terms =
 101    if terms = [] then where
 102    else
 103     let terms, terms' =
 104       List.split
 105        (List.map
 106         (fun (context_of_t, t) ->
 107           let context_of_t_len = List.length context_of_t in
 108           let with_what_in_context' =
 109             if context_len > context'_len then
 110              begin
 111               let with_what,subst,metasenv' =
 112                CicMetaSubst.delift_rels [] metasenv
 113                 (context_len - context'_len) with_what
 114               in
 115                assert (subst = []);
 116                assert (metasenv = metasenv');
 117                with_what
 118              end
 119             else
 120              with_what in
 121           let with_what_in_context_of_t =
 122            if context_of_t_len > context'_len then
 123             CicSubstitution.lift (context_of_t_len - context'_len)
 124              with_what_in_context'
 125            else
 126             with_what in
 127           let _,u =
 128            CicTypeChecker.type_of_aux' metasenv context_of_t with_what
 129             CicUniv.empty_ugraph in
 130           let b,_ =
 131            CicReduction.are_convertible ~metasenv context_of_t t with_what u in
 132           if b then
 133            t, with_what_in_context_of_t
 134           else
 135            raise NotConvertible) terms)
 136     in
 137      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
 138       ~where:where in
 139   let (selected_context,selected_ty) =
 140    ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
 141   let ty' = change context_len ty selected_ty in
 142   let context' =
 143    List.fold_right2
 144     (fun entry selected_entry context' ->
 145      let context'_len = List.length context' in
 146      match entry,selected_entry with
 147          None,None -> None::context'
 148        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
 149           let ty' = change context'_len ty selected_ty in
 150            Some (name,Cic.Decl ty')::context'
 151        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
 152           let bo' = change context'_len bo selected_bo in
 153           let ty' =
 154            match ty,selected_ty with
 155               None,None -> None
 156             | Some ty,Some selected_ty ->
 157                Some (change context'_len ty selected_ty)
 158             | _,_ -> assert false
 159           in
 160            Some (name,Cic.Def (bo',ty'))::context'
 161        | _,_ -> assert false
 162     ) context selected_context [] in
 163  let metasenv' =
 164    List.map (function
 165      | (n,_,_) when n = metano -> (metano,context',ty')
 166      | _ as t -> t
 167    ) metasenv
 168  in
 169   (curi,metasenv',pbo,pty), [metano]
 170   in
 171     mk_tactic (change_tac ~pattern ~with_what)
 172
 173 let fold_tac ~reduction ~term ~pattern =
 174  let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
 175   assert (wanted = None); (* this should be checked syntactically *)
 176   let proof,goal = status in
 177   let _,metasenv,_,_ = proof in
 178   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 179   let reduced_term = reduction context term in
 180    apply_tactic
 181     (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
 182  in
 183   mk_tactic (fold_tac ~reduction ~term ~pattern)
 184 ;;