From 9c6487ba87f448daa28158c6e916e3d932c50645 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 20 Oct 2004 13:50:08 +0000
Subject: COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cbytecodes.ml | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 kernel/cbytecodes.ml

(limited to 'kernel/cbytecodes.ml')

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
+
+
+
-- 
cgit v1.2.3