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