Imported Upstream version 8.5~beta3+dfsg

1 files changed, 144 insertions, 107 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 700de502..0a24a75d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,23 +17,28 @@ open Term
 
 type tag = int
 
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-(* It could be greate if OCaml export this value,
-   So fixme if this occur in a new version of OCaml *)
+let accu_tag = 0
+
+let type_atom_tag = 2
+let max_atom_tag = 2
+let proj_tag = 3
+let fix_app_tag = 4
+let switch_tag = 5
+let cofix_tag = 6
+let cofix_evaluated_tag = 7
+
+(* It would be great if OCaml exported this value,
+   So fixme if this happens in a new version of OCaml *)
 let last_variant_tag = 245 
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of pinductive
+  | Const_ind of inductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
-
+  | Const_univ_level of Univ.universe_level
+  | Const_type of Univ.universe
 
 type reloc_table = (tag * int) array
 
@@ -58,29 +63,30 @@ type instruction =
   | Kpush
   | Kpop of int
   | Kpush_retaddr of Label.t
-  | Kapply of int                       (*  number of arguments *)
-  | Kappterm of int * int               (* number of arguments, slot size *)
-  | Kreturn of int                      (* slot size *)
+  | Kapply of int
+  | Kappterm of int * int
+  | Kreturn of int
   | Kjump
   | Krestart
-  | Kgrab of int                        (* number of arguments *)
-  | Kgrabrec of int                     (* rec arg *)
-  | Kclosure of Label.t * int           (* label, number of free variables *)
+  | Kgrab of int
+  | Kgrabrec of int
+  | Kclosure of Label.t * int
   | Kclosurerec of int * int * Label.t array * Label.t array
-                   (* nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of pconstant
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of int * tag             (* size, tag *)
+  | Kmakeblock of int * tag
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+  | Kswitch of Label.t array * Label.t array
   | Kpushfields of int
   | Kfield of int
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (* index of the projected argument,
+                                           name of projection *)
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
   | Kaddint31                           (* adds the int31 in the accu
@@ -124,7 +130,10 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+  | FVnamed of Id.t
+  | FVrel of int
+  | FVuniv_var of int
 
 type fv = fv_elem array
 
@@ -142,105 +151,138 @@ type vm_env = {
 
 
 type comp_env = {
-    nb_stack : int;              (* nbre de variables sur la pile          *)
-    in_stack : int list;         (* position dans la pile                  *)
-    nb_rec : int;                (* nbre de fonctions mutuellement         *)
-                                 (* recursives =  nbr                      *)
+    nb_uni_stack : int ;         (* number of universes on the stack,      *)
+                                 (* universes are always at the bottom.    *)
+    nb_stack : int;              (* number of variables on the stack       *)
+    in_stack : int list;         (* position in the stack                  *)
+    nb_rec : int;                (* number of mutually recursive functions *)
     pos_rec  : instruction list; (* instruction d'acces pour les variables *)
                                  (*  de point fix ou de cofix              *)
     offset : int;
-    in_env : vm_env ref
+    in_env : vm_env ref          (* The free variables of the expression   *)
   }
 
+(* --- Pretty print *)
+open Pp
+open Util
 
+let pp_sort s =
+  match family_of_sort s with
+  | InSet -> str "Set"
+  | InProp -> str "Prop"
+  | InType -> str "Type"
 
-(* --- Pretty print *)
-open Format
-let rec instruction ppf = function
-  | Klabel lbl -> fprintf ppf "L%i:" lbl
-  | Kacc n -> fprintf ppf "\tacc %i" n
-  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
-  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
-  | Kpush -> fprintf ppf "\tpush"
-  | Kpop n -> fprintf ppf "\tpop %i" n
-  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
-  | Kapply n -> fprintf ppf "\tapply %i" n
+let rec pp_struct_const = function
+  | Const_sorts s -> pp_sort s
+  | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i
+  | Const_proj p -> Constant.print p
+  | Const_b0 i -> int i
+  | Const_bn (i,t) ->
+     int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
+  | Const_univ_level l -> Univ.Level.pr l
+  | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
+
+let pp_lbl lbl = str "L" ++ int lbl
+
+let pp_pcon (id,u) =
+  pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+
+let pp_fv_elem = function
+  | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
+  | FVrel i -> str "Rel(" ++ int i ++ str ")"
+  | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+
+let rec pp_instr i =
+  match i with
+  | Klabel _   | Ksequence _ -> assert false
+  | Kacc n -> str "acc " ++ int n
+  | Kenvacc n -> str "envacc " ++ int n
+  | Koffsetclosure n -> str "offsetclosure " ++ int n
+  | Kpush -> str "push"
+  | Kpop n -> str "pop " ++ int n
+  | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+  | Kapply n -> str "apply " ++ int n
   | Kappterm(n, m) ->
-      fprintf ppf "\tappterm %i, %i" n m
-  | Kreturn n -> fprintf ppf "\treturn %i" n
-  | Kjump -> fprintf ppf "\tjump"
-  | Krestart -> fprintf ppf "\trestart"
-  | Kgrab n -> fprintf ppf "\tgrab %i" n
-  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+      str "appterm " ++ int n ++ str ", " ++ int m
+  | Kreturn n -> str "return " ++ int n
+  | Kjump -> str "jump"
+  | Krestart -> str "restart"
+  | Kgrab n -> str "grab " ++ int n
+  | Kgrabrec n -> str "grabrec " ++ int n
   | Kclosure(lbl, n) ->
-      fprintf ppf "\tclosure L%i, %i" lbl n
+      str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
   | Kclosurerec(fv,init,lblt,lblb) ->
-      fprintf ppf "\tclosurerec";
-      fprintf ppf "%i , %i, " fv init;
-      print_string "types = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
-      print_string " bodies = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+      h 1 (str "closurerec " ++
+	     int fv ++ str ", " ++ int init ++
+	     str " types = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+	     str " bodies = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kclosurecofix (fv,init,lblt,lblb) ->
-      fprintf ppf "\tclosurecofix";
-      fprintf ppf " %i , %i, " fv init;
-      print_string "types = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
-      print_string " bodies = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
-  | Kconst cst ->
-      fprintf ppf "\tconst"
+      h 1 (str "closurecofix " ++
+	     int fv ++ str ", " ++ int init ++
+	     str " types = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+	     str " bodies = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+  | Kgetglobal idu -> str "getglobal " ++ pr_con idu
+  | Kconst sc ->
+      str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
-      fprintf ppf "\tmakeblock %i, %i" n m
-  | Kmakeprod -> fprintf ppf "\tmakeprod"
+      str "makeblock " ++ int n ++ str ", " ++ int m
+  | Kmakeprod -> str "makeprod"
   | Kmakeswitchblock(lblt,lbls,_,sz) ->
-      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+      str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
+	pp_lbl lbls ++ str ", " ++ int sz
   | Kswitch(lblc,lblb) ->
-      fprintf ppf "\tswitch";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
-  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
-  | Kfield  n -> fprintf ppf "\tgetfield %i" n
-  | Kstop -> fprintf ppf "\tstop"
-  | Ksequence (c1,c2) ->
-      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
-(* spiwack *)
-  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
-  | Kaddint31 -> fprintf ppf "\taddint31"
-  | Kaddcint31 -> fprintf ppf "\taddcint31"
-  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
-  | Ksubint31 -> fprintf ppf "\tsubint31"
-  | Ksubcint31 -> fprintf ppf "\tsubcint31"
-  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
-  | Kmulint31 -> fprintf ppf "\tmulint31"
-  | Kmulcint31 -> fprintf ppf "\tmulcint31"
-  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
-  | Kdivint31 -> fprintf ppf "\tdivint31"
-  | Kcompareint31 -> fprintf ppf "\tcompareint31"
-  | Khead0int31 -> fprintf ppf "\thead0int31"
-  | Ktail0int31 -> fprintf ppf "\ttail0int31"
-  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
-  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
-  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
-  | Kcompint31 -> fprintf ppf "\tcompint31"
-  | Kdecompint31 -> fprintf ppf "\tdecompint"
-  | Klorint31 -> fprintf ppf "\tlorint31"
-  | Klandint31 -> fprintf ppf "\tlandint31"
-  | Klxorint31 -> fprintf ppf "\tlxorint31"
+      h 1 (str "switch " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
+	     str " | " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+  | Kpushfields n -> str "pushfields " ++ int n
+  | Kfield n -> str "field " ++ int n
+  | Ksetfield n -> str "set field" ++ int n
 
-(* /spiwack *)
+  | Kstop -> str "stop"
+
+  | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
+  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
 
-and instruction_list ppf = function
-    [] -> ()
-  | Klabel lbl :: il ->
-      fprintf ppf "L%i:%a" lbl instruction_list il
-  | instr :: il ->
-      fprintf ppf "%a@ %a" instruction instr instruction_list il
+  | Kaddint31 -> str "addint31"
+  | Kaddcint31 -> str "addcint31"
+  | Kaddcarrycint31 -> str "addcarrycint31"
+  | Ksubint31 -> str "subint31"
+  | Ksubcint31 -> str "subcint31"
+  | Ksubcarrycint31 -> str "subcarrycint31"
+  | Kmulint31 -> str "mulint31"
+  | Kmulcint31 -> str "mulcint31"
+  | Kdiv21int31 -> str "div21int31"
+  | Kdivint31 -> str "divint31"
+  | Kcompareint31 -> str "compareint31"
+  | Khead0int31 -> str "head0int31"
+  | Ktail0int31 -> str "tail0int31"
+  | Kaddmuldivint31 -> str "addmuldivint31"
+  | Kisconst lbl -> str "isconst " ++ int lbl
+  | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl
+  | Kcompint31 -> str "compint31"
+  | Kdecompint31 -> str "decompint"
+  | Klorint31 -> str "lorint31"
+  | Klandint31 -> str "landint31"
+  | Klxorint31 -> str "lxorint31"
 
 
+and pp_bytecodes c =
+  match c with
+  | [] -> str ""
+  | Klabel lbl :: c ->
+	str "L" ++ int lbl ++ str ":" ++ fnl () ++
+	pp_bytecodes c
+  | Ksequence (l1, l2) :: c ->
+      pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
+  | i :: c ->
+      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
 type block =
@@ -253,8 +295,3 @@ type block =
                 (* spiwack: compilation given by a function *)
                 (* compilation function (see get_vm_constant_dynamic_info in
                    retroknowledge.mli for more info) , argument array  *)
-
-
-
-let draw_instr c =
-  fprintf std_formatter "@[<v 0>%a@]" instruction_list c