Propagated information from the reduction tactics to the kernel so

that the kernel conversion solves the delta/delta critical pair the
same way the tactics did. This allows to improve Qed time when slow
down is due to conversion having (arbitrarily) made the wrong choice.
Propagation is done thanks to a new kind of cast called REVERTcast.

Notes:
- Vm conversion not modified
- size of vo generally grows because of additional casts
- this remains a heuristic... for the record, when a reduction tactic
  is applied on the goal t leading to new goal t', this is translated
  in the kernel in a conversion t' <= t where, hence, reducing in t'
  must be preferred; what the propagation of reduction cast to the
  kernel does not do is whether it is preferable to first unfold c or
  to first compare u' and u in "c u' = c u"; in particular,
  intermediate casts are sometimes useful to solve this kind of issues
  (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the
  combination "simpl;red" needs the intermediate cast to ensure Qed
  answers quickly); henceforth the merge of nested casts in mkCast is
  deactivated
- for tactic "change", REVERTcast should be used when conversion is in
  the hypotheses, but convert_hyp does not (yet) support this (would
  require e.g. that convert_hyp overwrite some given hyp id with a
  body-cleared let-binding new_id := Cast(old_id,REVERTCast,t))

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c9112e86d..9173ab8cd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -18,7 +18,7 @@ open Reduction
 open Inductive
 open Type_errors
 
-let conv_leq = default_conv CUMUL
+let conv_leq l2r = default_conv CUMUL ~l2r
 
 let conv_leq_vecti env v1 v2 =
   array_fold_left2_i
@@ -191,6 +191,8 @@ 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
     | [] ->
@@ -201,7 +203,8 @@ let judge_of_apply env funj argjv =
         (match kind_of_term (whd_betadeltaiota env typ) with
           | Prod (_,c1,c2) ->
 	      (try
-		let c = conv_leq env hj.uj_type c1 in
+		let l2r = has_revert hj.uj_val in
+		let c = conv_leq l2r 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,7 +271,8 @@ let judge_of_cast env cj k tj =
     let cst =
       match k with
       | VMcast -> vm_conv CUMUL env cj.uj_type expected_type
-      | DEFAULTcast -> conv_leq env cj.uj_type expected_type in
+      | 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);
       uj_type = expected_type },
     cst