From 137e8b1636fa0b25c232ed42944ecaed058732ee Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 14 Apr 2019 12:51:30 +0200
Subject: [native compiler] Distinguish constant constructors in lambda code

---
 kernel/nativelambda.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/nativelambda.mli')

diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 687789e82b..c357819da5 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -33,9 +33,10 @@ type lambda =
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
+  | Lint          of int (* a constant constructor *)
   | Lmakeblock    of prefix * pconstructor * int * lambda array
                   (* prefix, constructor Name.t, constructor tag, arguments *)
-        (* A fully applied constructor *)
+        (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
-- 
cgit v1.2.3


From 7205996bf25a542224c815b38f92da0ffef76b5d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 14 Apr 2019 14:02:16 +0200
Subject: [native compiler] Remove unused universe argument in Lmakeblock

---
 kernel/nativelambda.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelambda.mli')

diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index c357819da5..093665df9b 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -34,7 +34,7 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
-  | Lmakeblock    of prefix * pconstructor * int * lambda array
+  | Lmakeblock    of prefix * constructor * int * lambda array
                   (* prefix, constructor Name.t, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
-- 
cgit v1.2.3


From 8b886a0a201444b7eb782f3fa0dc52a7b6fe8837 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 15 Apr 2019 15:23:39 +0200
Subject: [native compiler] Encoding of constructors based on tags

This serves two purposes:

1. It makes the native compiler use the same encoding and
   lambda-representation as the bytecode compiler

2. It avoid relying on fragile invariants relating tags and constructor
   indices. For example, previously, the mapping from indices to tags
   had to be increasing.
---
 kernel/nativelambda.mli | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel/nativelambda.mli')

diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 093665df9b..446df1a1ea 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -34,8 +34,8 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
-  | Lmakeblock    of prefix * constructor * int * lambda array
-                  (* prefix, constructor Name.t, constructor tag, arguments *)
+  | Lmakeblock    of prefix * inductive * int * lambda array
+                  (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
@@ -44,7 +44,10 @@ type lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+  }
 
 and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
 
-- 
cgit v1.2.3