- equality test on terms before trying convertibility now first tries

  phyisical equality between terms and then fallback to structural
  equality (same behaviour of ocaml < 3.08)
- changed behaviour of are_convertible. Before this change: equality was
  first tried on terms (as above) then, in case of failure, equality
  between weak head reduced terms was tried. Now weak head reduction is
  always performed. This change is motivated by the convertibility
  between "sin x" and "cos x" (no one was able to see the end of this
  test case). Now this test case completes almost immediately and
  regression test type checking the whole standard library does not
  shown any sensible slow down

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index f5684a9510196194727e7a9e48bc9aaf2954146d..f53471414b660a53e7e4c04310c1c0b0383ef54d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -769,17 +769,21 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
 
 let whd = R.whd;;
 
+  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+    * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
 (* t1, t2 must be well-typed *)
 let are_convertible ?(subst=[]) ?(metasenv=[]) =
- let module U = UriManager in
  let rec aux test_equality_only context t1 t2 =
   let aux2 test_equality_only t1 t2 =
    (* this trivial euristic cuts down the total time of about five times ;-) *)
    (* this because most of the time t1 and t2 are "sintactically" the same   *)
-   if t1 = t2 then
+   if t1 === t2 then
     true
    else
     begin
@@ -904,8 +908,10 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) =
         | (_,_) -> false
     end
   in
+(*
    if aux2 test_equality_only t1 t2 then true
    else
+*)
      begin
      debug t1 [t2] "PREWHD";
      (*