in
(* TASSI: sure this is in serial? *)
subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
- | C.LetIn (nn,s,t) ->
+ | C.LetIn (nn,s,ty,t) ->
let subst,metasenv,s',ugraph1 =
aux metasenv subst n context s ugraph in
+ let subst,metasenv,ty',ugraph1 =
+ aux metasenv subst n context ty ugraph in
let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
ugraph1
in
(* TASSI: sure this is in serial? *)
- subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
| C.Appl l ->
let subst,metasenv,revl',ugraph1 =
List.fold_left
let module S = CicSubstitution in
let t1 = deref subst t1 in
let t2 = deref subst t2 in
- let b,ugraph =
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+ if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+ false,ugraph
+ else
let foo () =
R.are_convertible ~subst ~metasenv context t1 t2 ugraph
in profiler_are_convertible.HExtlib.profile foo ()
in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
if b then
subst, metasenv, ugraph
else
in
fo_unif_subst test_equality_only
subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.LetIn (_,s1,t1), t2)
- | (t2, C.LetIn (_,s1,t1)) ->
+ | (C.LetIn (_,s1,ty1,t1), t2)
+ | (t2, C.LetIn (_,s1,ty1,t1)) ->
fo_unif_subst
test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
| (C.Appl l1, C.Appl l2) ->