diff options
Diffstat (limited to 'kernel/cbytecodes.ml')
-rw-r--r-- | kernel/cbytecodes.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 5d6d92ff..ae679027 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6 type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -67,7 +67,7 @@ type instruction = (* 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 constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod @@ -114,11 +114,14 @@ type instruction = | Kareconst of int*Label.t (* conditional jump *) | Kcompint31 (* dynamic compilation of int31 *) | Kdecompint31 (* dynamic decompilation of int31 *) + | Klorint31 (* bitwise operations: or and xor *) + | Klandint31 + | Klxorint31 (* /spiwack *) and bytecodes = instruction list -type fv_elem = FVnamed of identifier | FVrel of int +type fv_elem = FVnamed of Id.t | FVrel of int type fv = fv_elem array @@ -182,7 +185,7 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) + | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" | Kmakeblock(n, m) -> @@ -220,6 +223,9 @@ let rec instruction ppf = function | 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" (* /spiwack *) |