Merge branch 'v8.5' into v8.6

1 files changed, 20 insertions, 4 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 87302dcf5..ad5b04f3d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -22,8 +22,12 @@ to OCaml code. *)
 
 (** Local names **)
 
+(* The first component is there for debugging purposes only *)
 type lname = { lname : name; luid : int }
 
+let eq_lname ln1 ln2 =
+  Int.equal ln1.luid ln2.luid
+
 let dummy_lname = { lname = Anonymous; luid = -1 }
 
 module LNord = 
@@ -82,6 +86,9 @@ let eq_gname gn1 gn2 =
   | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
   | _ -> false
 
+let dummy_gname =
+  Grel 0
+
 open Hashset.Combine
 
 let gname_hash gn = match gn with
@@ -404,9 +411,13 @@ let opush_lnames n env lns =
 let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
   match t1, t2 with
   | MLlocal ln1, MLlocal ln2 ->
+     (try
       Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2)
+     with Not_found ->
+      eq_lname ln1 ln2)
   | MLglobal gn1', MLglobal gn2' ->
       eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2')
+      || (eq_gname gn1 gn2' && eq_gname gn2 gn1')
   | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2
   | MLlam (lns1, ml1), MLlam (lns2, ml2) ->
       Int.equal (Array.length lns1) (Array.length lns2) &&
@@ -719,6 +730,11 @@ let push_global_norm gn params body =
 let push_global_case gn params annot a accu bs =
   push_global gn (Gletcase (gn, params, annot, a, accu, bs))
 
+(* Compares [t1] and [t2] up to alpha-equivalence. [t1] and [t2] may contain
+   free variables. *)
+let eq_mllambda t1 t2 =
+  eq_mllambda dummy_gname dummy_gname 0 LNmap.empty LNmap.empty t1 t2
+
 (*s Compilation environment *)
 
 type env =
@@ -897,9 +913,7 @@ let rec insert cargs body rl =
      let params = rm_params fv params in
      rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
  | Rcons(l,fv,body',rl) ->
-    (** ppedrot: It seems we only want to factorize common branches. It should
-        not matter to do so with a subapproximation by (==). *)
-     if body == body' then
+     if eq_mllambda body body' then
        let (c,params) = cargs in
        let params = rm_params fv params in
        l := (c,params)::!l
@@ -1446,12 +1460,14 @@ let optimize gdef l =
 
 	end
     | MLif(t,b1,b2) ->
+       (* This optimization is critical: it applies to all fixpoints that start
+       by matching on their recursive argument *)
 	let t = optimize s t in
 	let b1 = optimize s b1 in
 	let b2 = optimize s b2 in
 	begin match t, b2 with
 	| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
-	    when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *)
+	    when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
         | _, _ -> MLif(t, b1, b2)
 	end
     | MLmatch(annot,a,accu,bs) ->