aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-09 14:00:06 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-09 14:00:06 +0200
commit3456726bd4a8ee04393bd0f89794c9fadb9649e9 (patch)
treef2e2072e6abde16556f34b41fb521fa0729e6288 /kernel
parentdee69387bd4b2944c9e81ee422fb9900ab0e6c4d (diff)
parent7a037b8c1de11b18d47b01e5b0262090f32bfc40 (diff)
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml24
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) ->