From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/cbytecodes.ml | 251 +++++++++++++++++++++++++++++---------------------- 1 file changed, 144 insertions(+), 107 deletions(-) (limited to 'kernel/cbytecodes.ml') 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 "@[%a@]" instruction_list c -- cgit v1.2.3