summaryrefslogtreecommitdiff
path: root/kernel/vm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vm.mli')
-rw-r--r--kernel/vm.mli109
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
+
+