1 files changed, 109 insertions, 0 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
new file mode 100644
index 00000000..b5fd9b9d
--- /dev/null
+++ b/kernel/vm.mli
@@ -0,0 +1,109 @@
+open Names
+open Term
+open Cbytecodes
+open Cemitcodes
+
+
+val set_drawinstr : unit -> unit
+
+val transp_values : unit -> bool
+val set_transp_values : bool -> unit
+(* le code machine *)
+type tcode 
+
+(* Les valeurs ***********)
+
+type accumulator
+type vprod 
+type vfun
+type vfix
+type vfix_app
+type vcofix
+type vcofix_app 
+type vblock
+type vswitch
+type arguments
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix_app
+  | Zswitch of vswitch
+
+type stack = zipper list
+
+
+type atom = 
+  | Aid of id_key
+  | Aiddef of id_key * values
+  | Aind of inductive
+  | Afix_app of accumulator * vfix_app
+  | Aswitch of accumulator * vswitch
+
+type whd =
+  | Vsort of sorts
+  | Vprod of vprod 
+  | Vfun of vfun
+  | Vfix of vfix
+  | Vfix_app of vfix_app
+  | Vcofix of vcofix
+  | Vcofix_app of vcofix_app
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+
+(* Constructors *)
+val val_of_str_const : structured_constant -> values
+
+val val_of_rel : int -> values 
+val val_of_rel_def : int -> values -> values 
+
+val val_of_named : identifier -> values
+val val_of_named_def : identifier -> values -> values
+
+val val_of_constant : constant -> values 
+val val_of_constant_def : int -> constant -> values -> values
+
+(* Destructors *)
+val whd_val : values -> whd
+
+(* Product *)
+val dom : vprod -> values
+val codom : vprod -> vfun
+(* Function *)
+val body_of_vfun : int -> vfun -> values 
+val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
+(* Fix *)
+val fix : vfix_app -> vfix
+val args_of_fix : vfix_app -> arguments
+val fix_init : vfix -> int
+val fix_ndef : vfix -> int 
+val rec_args : vfix -> int array 
+val check_fix : vfix -> vfix -> bool
+val bodies_of_fix : int -> vfix -> vfun array
+val types_of_fix : vfix -> values array
+(* CoFix *)
+val cofix : vcofix_app -> vcofix
+val args_of_cofix : vcofix_app -> arguments
+val cofix_init : vcofix -> int 
+val cofix_ndef : vcofix -> int
+val check_cofix : vcofix -> vcofix -> bool
+val bodies_of_cofix : int -> vcofix -> values array
+val types_of_cofix : vcofix -> values array
+(* Block *)
+val btag : vblock -> int
+val bsize : vblock -> int
+val bfield : vblock -> int -> values
+(* Switch *)
+val eq_tbl : vswitch -> vswitch -> bool
+val case_info : vswitch -> case_info
+val type_of_switch : vswitch -> values
+val branch_of_switch : int -> vswitch -> (int * values) array
+(* Arguments *)  
+val nargs : arguments -> int
+val arg : arguments -> int -> values
+
+(* Evaluation *)
+val whd_stack : values -> stack -> whd
+val force_whd : values -> stack -> whd
+
+