fo_unif_subst
test_equality_only subst context metasenv
redappl1 redappl2 ugraph)
+ (*CSC: This is necessary because of the "elim H" tactic
+ where the type of H is only reducible to an
+ inductive type. This could be extended from inductive
+ types to any rigid term. However, the code is
+ duplicated in two places: inside applications and
+ outside them. Probably it would be better to
+ work with lambda-bar terms instead. *)
+ | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+ | (_, Cic.MutInd _::_) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "88")))
+ | (Cic.MutInd _::_,_) ->
+ let t2' = R.whd ~subst context t2 in
+ (match t2' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1 t2' ugraph
+ | _ -> raise (UnificationFailure (lazy "99")))
| _ -> raise exn)))
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv',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))))
+(* Works iff there are no arguments applied to it; similar to the
+ case below
+ | (_, C.MutInd _) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.MutInd _ ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "8")))
+*)
+(* 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