let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
let type_of_aux' metasenv subst context term ugraph =
let foo () =
try
- CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
+ profile.HExtlib.profile
+ (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
with
CicTypeChecker.TypeCheckerFailure msg ->
let msg =
(lower m1 m2) (upper m1 m2) ugraph
in
begin
- let subst,metasenv,ugraph1 =
+ let subst,metasenv,ugraph1 =
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
let tyt,ugraph1 =
in
fo_unif_subst test_equality_only subst context metasenv
beta_expanded (C.Meta (i,l)) ugraph1
- | (C.Sort _ ,_) | (_, C.Sort _)
- | (C.Const _, _) | (_, C.Const _)
- | (C.MutInd _, _) | (_, C.MutInd _)
- | (C.MutConstruct _, _) | (_, C.MutConstruct _)
- | (C.Fix _, _) | (_, C.Fix _)
- | (C.CoFix _, _) | (_, C.CoFix _) ->
- if t1 = t2 then
- subst, metasenv, ugraph
- else
- let b,ugraph1 =
- R.are_convertible ~subst ~metasenv context t1 t2 ugraph
- in
- if b then
- subst, metasenv, ugraph1
- else
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+(* The following idea could be exploited again; right now we have no
+ longer any example requiring it
| (C.Prod _, t2) ->
let t2' = R.whd ~subst context t2 in
(match t2' with
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)
(CicMetaSubst.ppterm subst t2)))))
+*)
| (_,_) ->
- raise (UnificationFailure (lazy "10"))
- (* (sprintf
+ (* delta-beta reduction should almost never be a problem for
+ unification since:
+ 1. long computations require iota reduction
+ 2. it is extremely rare that a close term t1 (that could be unified
+ to t2) beta-delta reduces to t1' while t2 does not beta-delta
+ reduces in the same way. This happens only if one meta of t2
+ occurs in head position during beta reduction. In this unluky
+ case too much reduction will be performed on t1 and unification
+ will surely fail. *)
+ let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
+ let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
+ if t1 = t1' && t2 = t2' then
+ raise (UnificationFailure
+ (lazy
+ (sprintf
"Can't unify %s with %s because they are not convertible"
(CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (CicMetaSubst.ppterm subst t2))))
+ else
+ try
+ fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
+ with
+ UnificationFailure _
+ | Uncertain _ ->
+ raise (UnificationFailure
+ (lazy
+ (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (CicMetaSubst.ppterm subst t1)
+ (CicMetaSubst.ppterm subst t2))))
and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
exp_named_subst1 exp_named_subst2 ugraph