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