diff options
| author | Matthieu Sozeau | 2014-08-28 12:37:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-28 19:55:01 +0200 |
| commit | 469c5bfc849e06d5a32d7aaabdf9b2fa3f451f4a (patch) | |
| tree | b227dd4e28501b2c325a99711fb4c659a6ac6ba2 /pretyping | |
| parent | 3fdfb3ccb7986b1e4c7685b440a62730107a639f (diff) | |
Fix bugs #3484 and #3546.
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 33 |
1 files changed, 23 insertions, 10 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 29d721577f..aee7be9816 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -395,7 +395,12 @@ let oracle_order env cf1 cf2 = match cf2 with | None -> Some true | Some k2 -> - Some (Conv_oracle.oracle_order (Environ.oracle env) false (translate_key k1) (translate_key k2)) + match k1, k2 with + | IsProj (p, _), IsKey (ConstKey (p',_)) when eq_constant p p' -> Some false + | IsKey (ConstKey (p,_)), IsProj (p', _) when eq_constant p p' -> Some true + | _ -> + Some (Conv_oracle.oracle_order (Environ.oracle env) false + (translate_key k1) (translate_key k2)) let is_rigid_head flags t = match kind_of_term t with @@ -574,15 +579,23 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) - | App (f, l1), _ when flags.modulo_eta && is_eta_constructor_app env f l1 -> - let l1', l2' = eta_constructor_app env f l1 cN in - Array.fold_left2 - (unirec_rec curenvnb CONV true wt) substn l1' l2' - - | _, App (f, l2) when flags.modulo_eta && is_eta_constructor_app env f l2 -> - let l2', l1' = eta_constructor_app env f l2 cM in - Array.fold_left2 - (unirec_rec curenvnb CONV true wt) substn l1' l2' + | App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app env f1 l1 -> + (try let l1', l2' = eta_constructor_app env f1 l1 cN in + Array.fold_left2 + (unirec_rec curenvnb CONV true wt) substn l1' l2' + with ex when precatchable_exception ex -> + (match kind_of_term cN with + | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)) + + | _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app env f2 l2 -> + (try let l2', l1' = eta_constructor_app env f2 l2 cM in + Array.fold_left2 + (unirec_rec curenvnb CONV true wt) substn l1' l2' + with ex when precatchable_exception ex -> + (match kind_of_term cM with + | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 + | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try |