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
ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+ (* 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=[]) =
(* 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 *)
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 aux2 test_equality_only t1 t2 then true
else
if aux2 test_equality_only t1 t2 then true
else
begin
debug t1 [t2] "PREWHD";
(*
begin
debug t1 [t2] "PREWHD";
(*