diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:54 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 14:27:54 +0000 |
| commit | f7c2010c34adbc5c20e14909546c0964a32764cc (patch) | |
| tree | 6355a75c786d9c37be0e05bb9e6008b20e50b6dc /pretyping | |
| parent | 03b12cc43ce24e708f0edb1b4ac3931d42527343 (diff) | |
- Improve unification (beta-reduction, and same heuristic as evarconv for reducing matches).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 50b1c6139..1bbecc4e2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -225,6 +225,10 @@ let oracle_order env cf1 cf2 = | None -> Some true | Some k2 -> Some (Conv_oracle.oracle_order k1 k2) +let do_reduce env sigma c = + let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in + applist (t, list_of_stack l) + let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm @@ -284,9 +288,12 @@ 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 | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec curenvnb topconv true) - (unirec_rec curenvnb topconv true - (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 + (try + array_fold_left2 (unirec_rec curenvnb topconv true) + (unirec_rec curenvnb topconv true + (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 + with ex when precatchable_exception ex -> + reduce curenvnb pb b substn cM cN) | App (f1,l1), _ when (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) & @@ -335,11 +342,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag expand curenvnb pb b substn cM f1 l1 cN f2 l2 and reduce curenvnb pb b (sigma, _, _ as substn) cM cN = - let cM' = whd_betaiotazeta sigma cM in + let cM' = do_reduce (fst curenvnb) sigma cM in if not (eq_constr cM cM') then unirec_rec curenvnb pb true substn cM' cN else - let cN' = whd_betaiotazeta sigma cN in + let cN' = do_reduce (fst curenvnb) sigma cN in if not (eq_constr cN cN') then unirec_rec curenvnb pb true substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) |