From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 kernel/vm.mli | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 045d02333c..bc19786632 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -22,7 +22,8 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (** Zippers *)
 
@@ -45,19 +46,25 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.universe_level
+
+val pr_atom : atom -> Pp.std_ppcmds
+val pr_whd : whd -> Pp.std_ppcmds
 
 (** Constructors *)
 
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
-val val_of_constant : pconstant -> values
+val val_of_constant : constant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
 
 val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.universe_level
+val instantiate_universe : Univ.universe -> stack -> Univ.universe
 
 (** Arguments *)
 
-- 
cgit v1.2.3


From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 28 Oct 2015 11:16:24 +0100
Subject: Refine Gregory Malecha's patch on VM and universe polymorphism.

- Universes are now represented in the VM by a structured constant containing the
  global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
  a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
  constructor arguments, which has to be prevented.
  Was showing up for instance when evaluating [cons _ list (nil _)] with
  a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
  Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.

Patch written with Benjamin Grégoire.
---
 kernel/vm.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index bc19786632..43a42eb9c4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
 
 val whd_val : values -> whd
 val uni_lvl_val : values -> Univ.universe_level
-val instantiate_universe : Univ.universe -> stack -> Univ.universe
 
 (** Arguments *)
 
-- 
cgit v1.2.3