components/tactics/compose.ml

   1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
  24  *)
  25
  26 let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
  27
  28 let compose_core t2 t1 (proof, goal) =
  29   let _,metasenv,_subst,_,_,_ = proof in
  30   let _,context,_ = CicUtil.lookup_meta goal metasenv in
  31   let ty1,_ =
  32     CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph
  33   in
  34   let ty2,_ =
  35     CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph
  36   in
  37   let saturated_ty2, menv_for_saturated_ty2 =
  38     let maxm = CicMkImplicit.new_meta metasenv [] in
  39     let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
  40     ty2, menv
  41   in
  42   (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
  43   let unif menv t =
  44     let m, menv2 =
  45       let n = CicMkImplicit.new_meta menv [] in
  46       let irl =
  47         CicMkImplicit.identity_relocation_list_for_metavariable context
  48       in
  49       Cic.Meta (n,irl), ((n,context,t)::menv)
  50     in
  51     try
  52       let _ =
  53         CicUnification.fo_unif menv context t saturated_ty2
  54           CicUniv.oblivion_ugraph
  55       in
  56         true, menv2, m
  57     with
  58     | CicUnification.UnificationFailure _
  59     | CicUnification.Uncertain _ -> false, menv2, m
  60   in
  61   (* check which "positions" in the input arrow unifies with saturated_ty2 *)
  62   let rec positions menv cur saturations = function
  63     | Cic.Prod (n,s,t) ->
  64         let b, newmenv, sb = unif menv s in
  65         if b then
  66           (saturations - cur - 1) ::
  67             (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
  68         else
  69           positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
  70     | _ -> []
  71   in
  72   (* position is a list of arities, that is if t1 : a -> b -> c and saturations is
  73    * 0 then the computed term will be (t1 ? t2) of type a -> c
  74    * if saturations is 1 then (t1 t2 ?) of type b -> c *)
  75   let rec generate positions menv acc =
  76     match positions with
  77     | [] -> acc, menv
  78     | saturations::tl ->
  79       try
  80         let t, menv1, _ =
  81           CloseCoercionGraph.generate_composite t2 t1 context menv
  82             CicUniv.oblivion_ugraph saturations
  83         in
  84         assert (List.length menv1 = List.length menv);
  85         generate tl menv (t::acc)
  86       with
  87       | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
  88   in
  89   let terms, metasenv =
  90     generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
  91   in
  92   (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
  93   let proof =
  94     let uri, _, _subst, bo, ty, attrs = proof in
  95     uri, metasenv, _subst, bo, ty, attrs
  96   in
  97   (* now we have the terms, we generalize them and intros them *)
  98   let proof, goal =
  99     List.fold_left
 100       (fun (proof,goal) t ->
 101         let lazy_of t =
 102           ProofEngineTypes.const_lazy_term t
 103         in
 104         let proof, gl =
 105           ProofEngineTypes.apply_tactic
 106             (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
 107             (proof,goal)
 108         in
 109         assert(List.length gl = 1);
 110         proof,List.hd gl)
 111       (proof,goal) terms
 112   in
 113   (proof, goal), List.length terms
 114 ;;
 115
 116 let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
 117   let ((proof, goal), k), n =
 118     match t2 with
 119     | Some t2 -> compose_core t1 t2 proofstatus, n-1
 120     | None ->
 121         let k =
 122           let proof, goal = proofstatus in
 123           let _,metasenv,subst,_,_,_ = proof in
 124           let _,_,ty = CicUtil.lookup_meta goal metasenv in
 125           count_pi (CicMetaSubst.apply_subst subst ty)
 126         in
 127         (proofstatus, k), n
 128   in
 129   let (proof, goal), k =
 130     (* fix iterates n times the composition *)
 131     let rec fix proofstatus k t = function
 132       | 0 -> proofstatus, k
 133       | n ->
 134           let t = CicSubstitution.lift k t in
 135           let proof, gl =
 136             ProofEngineTypes.apply_tactic
 137               (PrimitiveTactics.intros_tac
 138                 ~howmany:k ?mk_fresh_name_callback ()) proofstatus
 139           in
 140           assert (List.length gl = 1);
 141           let goal = List.hd gl in
 142           let k, proofstatus =
 143             (* aux compose t with every previous result *)
 144             let rec aux k proofstatus = function
 145               | 0 -> k, proofstatus
 146               | n ->
 147                  let (proof, goal), k1 =
 148                    compose_core t (Cic.Rel n) proofstatus
 149                  in
 150                  aux (k+k1) (proof, goal) (n-1)
 151             in
 152               aux 0 (proof, goal) k
 153           in
 154           fix proofstatus k t (n-1)
 155     in
 156       fix (proof, goal) k t1 n
 157   in
 158   let howmany =
 159     match howmany with
 160     | None -> None
 161     | Some i ->
 162         if i - k < 0 then (* we should generalize back and clear *) Some 0
 163         else Some (i - k)
 164   in
 165      ProofEngineTypes.apply_tactic
 166       (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
 167       (proof,goal)
 168 ;;
 169
 170 let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
 171   ProofEngineTypes.mk_tactic
 172     (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)
 173 ;;