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