diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-04 14:22:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-05 02:00:07 +0200 |
| commit | a51cce369b9c634a93120092d4c7685a242d55b1 (patch) | |
| tree | dd68ea8dadf86f9a6eb400839f515ed5b9cf8f95 /kernel/cbytecodes.ml | |
| parent | 31c7542731a62f56bd60f443a84d68813f8780a8 (diff) | |
Fix handling of primitive projections in VM.
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
Diffstat (limited to 'kernel/cbytecodes.ml')
| -rw-r--r-- | kernel/cbytecodes.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 93fd61f02..3271ac145 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -31,6 +31,7 @@ let last_variant_tag = 245 type structured_constant = | Const_sorts of sorts | Const_ind of pinductive + | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -81,6 +82,8 @@ type instruction = | 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 @@ -167,6 +170,7 @@ 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_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) @@ -228,6 +232,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" |