diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /kernel/cbytecodes.ml | |
parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
-rw-r--r-- | kernel/cbytecodes.ml | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml new file mode 100644 index 000000000..48331a687 --- /dev/null +++ b/kernel/cbytecodes.ml @@ -0,0 +1,64 @@ +open Names +open Term + +type tag = int + +type structured_constant = + | Const_sorts of sorts + | Const_ind of inductive + | Const_b0 of tag + | Const_bn of tag * structured_constant array + +type reloc_table = (tag * int) array + +type annot_switch = + {ci : case_info; rtbl : reloc_table; tailcall : bool} + +module Label = + struct + type t = int + let no = -1 + let counter = ref no + let create () = incr counter; !counter + let reset_label_counter () = counter := no + end + + +type instruction = + | Klabel of Label.t + | Kacc of int + | Kenvacc of int + | Koffsetclosure of int + | 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 *) + | Kjump + | Krestart + | Kgrab of int (* number of arguments *) + | Kgrabrec of int (* rec arg *) + | Kcograb of int (* number of arguments *) + | Kclosure of Label.t * int (* label, number of free variables *) + | Kclosurerec of int * int * Label.t array * Label.t array + (* nb fv, init, lbl types, lbl bodies *) + | Kgetglobal of constant + | Kconst of structured_constant + | Kmakeblock of int * tag (* size, tag *) + | Kmakeprod + | Kmakeswitchblock of Label.t * Label.t * annot_switch * int + | Kforce + | Kswitch of Label.t array * Label.t array (* consts,blocks *) + | Kpushfield of int + | Kstop + | Ksequence of bytecodes * bytecodes + +and bytecodes = instruction list + +type fv_elem = FVnamed of identifier | FVrel of int + +type fv = fv_elem array + + + |