diff options
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r-- | kernel/nativecode.ml | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ef4b50130..7d76ecf3a 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) -> |