NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
in
let ctx, ty = intros ty in
+ let ity =
+ match ity with
+ | NCic.Appl [eq;t;a;b] ->
+ NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
+ | t -> t
+ in
+ prerr_endline
+ (Printf.sprintf "%s == %s"
+ (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
+ (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
let metasenv, subst =
try
- NCicUnification.unify menv [] ctx ity sty
+ prerr_endline ("INIZIO: " ^ NUri.string_of_uri u);
+ NCicUnification.unify menv [] ctx ity sty
with
| NCicUnification.Uncertain msg
| NCicUnification.UnificationFailure msg
in
let ty_t =
try NCicTypeChecker.typeof ~subst ~metasenv context t
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ with NCicTypeChecker.TypeCheckerFailure msg ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+ prerr_endline (Lazy.force msg);
+ assert false
in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
- let ty = NCicSubstitution.subst_meta lc ty in
- let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in
+ let lty = NCicSubstitution.subst_meta lc ty in
+ let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
let (metasenv, subst), t =
NCicMetaSubst.delift metasenv subst context n lc t
in
and unify test_eq_only metasenv subst context t1 t2 =
let fo_unif test_eq_only metasenv subst t1 t2 =
+ prerr_endline ("A " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm
+ ~metasenv ~subst ~context t2 );
if t1 === t2 then
metasenv, subst
else
| NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
| NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
| NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true
+(* | NCic.Rel _ -> 1, WRONG *)
| _ when is_whd -> 0, false
- | _ -> 0, false (* !!! with max_int we diverge, with 0 we may do too much
- reduction *)
+ | _ -> max_int, false
in
let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
let h1, flex1 = height_of is_whd t1 in
in
let rec unif_machines metasenv subst = function
| ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
+ prerr_endline ("M(" ^ string_of_int delta^ " " ^
+ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
+ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind
+ m2));
try
let relevance = [] (* TO BE UNDERSTOOD
match t1 with
try
let t1 = NCicReduction.from_stack t1 in
let t2 = NCicReduction.from_stack t2 in
- unif_machines metasenv subst (small_delta_step true t1 t2)
+ unif_machines metasenv subst
+ (small_delta_step true t1 t2)
with UnificationFailure _ | Uncertain _ when not b ->
metasenv, subst
in
in
check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
with UnificationFailure _ | Uncertain _ when delta > 0 ->
+(*
let delta = delta - 1 in
let red = NCicReduction.reduce_machine ~delta ~subst context in
- unif_machines metasenv subst (red m1,red m2,delta)
+*)
+ prerr_endline ("RIPARTO RIDUCENDO"^string_of_int delta);
+ unif_machines metasenv subst (small_delta_step true m1 m2)
+ | exn -> prerr_endline ")"; raise exn
in
try fo_unif test_eq_only metasenv subst t1 t2
with UnificationFailure msg | Uncertain msg as exn ->