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.
---
 dev/vm_printers.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 802b0f9d80..272df7b421 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -13,7 +13,7 @@ let ppripos (ri,pos) =
 	("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
   | Reloc_const _ ->
       print_string "structured constant\n"
-  | Reloc_getglobal (kn,_) ->
+  | Reloc_getglobal kn ->
       print_string ("getglob "^(string_of_con kn)^"\n"));
    print_flush ()
 
@@ -30,7 +30,7 @@ let ppsort = function
 
 let print_idkey idk =
   match idk with
-  | ConstKey (sp,_) ->
+  | ConstKey sp ->
       print_string "Cons(";
       print_string (string_of_con sp);
       print_string ")"
@@ -61,7 +61,8 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aind((sp,i),_) ->  print_string "Ind(";
+  | Atype u -> print_string "Type(...)"
+  | Aind(sp,i) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
       print_string ")"
-- 
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.
---
 dev/vm_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 272df7b421..1c501df808 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -79,6 +79,7 @@ and ppwhd whd =
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
+  | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl)
 
 and ppvblock b =
   open_hbox();
-- 
cgit v1.2.3