* http://helm.cs.unibo.it/
*)
+let debug = false;;
+let debug_print =
+ if not debug then (fun _ -> ()) else (fun s -> prerr_endline (Lazy.force s))
+;;
+
let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
let compose_core t2 t1 (proof, goal) =
let ty2,_ =
CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph
in
- let saturated_ty2, menv_for_saturated_ty2 =
+ let saturated_ty2, menv_for_saturated_ty2, args_t2 =
let maxm = CicMkImplicit.new_meta metasenv [] in
- let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
- ty2, menv
+ let ty2, menv, args, _ =
+ TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in
+ ty2, menv, args
+ in
+ let saturations_t2 =
+ let rec aux n = function
+ | Cic.Meta (i,_)::tl ->
+ let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in
+ if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop)
+ CicUniv.oblivion_ugraph)
+ then n else aux (n+1) tl
+ | _::tl -> aux (n+1) tl
+ | [] -> n+1
+ in
+ List.length args_t2 - aux 0 args_t2 +1
in
+ debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context
+ [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^
+ " saturations_t2:" ^ string_of_int saturations_t2));
(* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
let unif menv t =
let m, menv2 =
let b, newmenv, sb = unif menv s in
if b then
(saturations - cur - 1) ::
- (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
+ (positions newmenv (cur + 1) saturations
+ (CicSubstitution.subst sb t))
else
positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
| _ -> []
in
- (* position is a list of arities, that is if t1 : a -> b -> c and saturations is
- * 0 then the computed term will be (t1 ? t2) of type a -> c
- * if saturations is 1 then (t1 t2 ?) of type b -> c *)
+ (* position is a list of arities, that is if t1 : a -> b -> c and saturations
+ * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations
+ * is 1 then (t1 t2 ?) of type b -> c *)
let rec generate positions menv acc =
match positions with
| [] -> acc, menv
- | saturations::tl ->
+ | saturations_t1::tl ->
try
let t, menv1, _ =
CloseCoercionGraph.generate_composite t2 t1 context menv
- CicUniv.oblivion_ugraph saturations
+ CicUniv.oblivion_ugraph saturations_t2 saturations_t1
in
assert (List.length menv1 = List.length menv);
generate tl menv (t::acc)
in
let proof, gl =
ProofEngineTypes.apply_tactic
- (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
+ (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None))
(proof,goal)
in
assert(List.length gl = 1);