diff options
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 93 |
1 files changed, 55 insertions, 38 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 93fd61f02a..f9cf2691ee 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,18 +151,17 @@ 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 @@ -166,13 +174,24 @@ let pp_sort s = let rec pp_struct_const = function | Const_sorts s -> pp_sort s - | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i + | 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 @@ -206,7 +225,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal (id,u) -> str "getglobal " ++ pr_con id + | Kgetglobal idu -> str "getglobal " ++ pr_con idu | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> @@ -228,6 +247,8 @@ let rec pp_instr i = | Kbranch lbl -> str "branch " ++ pp_lbl lbl + | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p + | Kaddint31 -> str "addint31" | Kaddcint31 -> str "addcint31" | Kaddcarrycint31 -> str "addcarrycint31" @@ -255,16 +276,12 @@ and pp_bytecodes c = match c with | [] -> str "" | Klabel lbl :: c -> - str "L" ++ int lbl ++ str ":" ++ str "\n" ++ + str "L" ++ int lbl ++ str ":" ++ fnl () ++ pp_bytecodes c | Ksequence (l1, l2) :: c -> pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> - str "\t" ++ pp_instr i ++ str "\n" ++ pp_bytecodes c - -let dump_bytecode c = - pperrnl (pp_bytecodes c); - flush_all() + 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 *) |