diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-04 21:36:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-04 21:36:17 +0000 |
| commit | 82406b12adc9f59a186a38f863b0180855314b50 (patch) | |
| tree | 4308eb8ae1202d5b211eaaf9007601e2e2993a6e /kernel | |
| parent | b08076bc71c7813038f2cefedff9c5b678d225a8 (diff) | |
Having added a special Cast for remembering the use of conversion
tactic steps (r14407) increased the size of proof-terms, leading in
some cases (e.g. in Nijmegen/Algebra) to calls to simpl becoming
extremely costly on such terms built with tactics.
We try as a workaround to remove the newly introduced Cast after it
has been used by the type-checking algorithm.
We incidentally fixed eq_constr which was not fully transparent wrt
casts. We also removed useless code in judge_of_apply (has_revert).
Note: checker still to be updated to reflect a possible use of this
new kind of cast.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14448 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 21 |
2 files changed, 14 insertions, 9 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index b308b22a4..b4ddbfc8c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -562,6 +562,8 @@ let compare_constr f t1 t2 = | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 + | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 + | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) | App (c1,l1), App (c2,l2) -> Array.length l1 = Array.length l2 && f c1 c2 && array_for_all2 f l1 l2 diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9173ab8cd..6e0e098c0 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -191,8 +191,6 @@ let judge_of_letin env name defj typj j = (* Type of an application. *) -let has_revert c = match kind_of_term c with Cast (c,REVERTcast,_) -> true | _ -> false - let judge_of_apply env funj argjv = let rec apply_rec n typ cst = function | [] -> @@ -203,8 +201,7 @@ let judge_of_apply env funj argjv = (match kind_of_term (whd_betadeltaiota env typ) with | Prod (_,c1,c2) -> (try - let l2r = has_revert hj.uj_val in - let c = conv_leq l2r env hj.uj_type c1 in + let c = conv_leq false env hj.uj_type c1 in let cst' = union_constraints cst c in apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> @@ -268,12 +265,18 @@ let judge_of_product env name t1 t2 = let judge_of_cast env cj k tj = let expected_type = tj.utj_val in try - let cst = + let c, cst = match k with - | VMcast -> vm_conv CUMUL env cj.uj_type expected_type - | DEFAULTcast -> conv_leq false env cj.uj_type expected_type - | REVERTcast -> conv_leq true env cj.uj_type expected_type in - { uj_val = mkCast (cj.uj_val, k, expected_type); + | VMcast -> + mkCast (cj.uj_val, k, expected_type), + vm_conv CUMUL env cj.uj_type expected_type + | DEFAULTcast -> + mkCast (cj.uj_val, k, expected_type), + conv_leq false env cj.uj_type expected_type + | REVERTcast -> + cj.uj_val, + conv_leq true env cj.uj_type expected_type in + { uj_val = c; uj_type = expected_type }, cst with NotConvertible -> |