From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 kernel/vm.mli | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index d31448ee13..045d02333c 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
 open Term
 open Cbytecodes
 
-(** Efficient Virtual Machine *)
+(** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
 (** Machine code *)
 
 type tcode
@@ -25,7 +22,6 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (** Zippers *)
@@ -106,10 +102,6 @@ val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
 
+val apply_whd : int -> whd -> values
-- 
cgit v1.2.3


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


From 8e7803224eeb32e83600905c2c855e32e7bf8ffb Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Mon, 9 Nov 2015 16:22:18 -0800
Subject: bug fixes to vm computation + test cases.

---
 kernel/vm.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 43a42eb9c4..6e9579aa46 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -48,8 +48,11 @@ type whd =
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.universe_level
 
+(** For debugging purposes only *)
+
 val pr_atom : atom -> Pp.std_ppcmds
 val pr_whd : whd -> Pp.std_ppcmds
+val pr_stack : stack -> Pp.std_ppcmds
 
 (** Constructors *)
 
-- 
cgit v1.2.3