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