diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /kernel/vm.mli | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'kernel/vm.mli')
-rw-r--r-- | kernel/vm.mli | 43 |
1 files changed, 29 insertions, 14 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli index 5ecc8d99..58228eb8 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -3,15 +3,18 @@ open Term open Cbytecodes open Cemitcodes +(** Efficient Virtual Machine *) val set_drawinstr : unit -> unit val transp_values : unit -> bool val set_transp_values : bool -> unit -(* le code machine *) + +(** Machine code *) + type tcode -(* Les valeurs ***********) +(** Values *) type vprod type vfun @@ -26,11 +29,11 @@ type atom = | Aiddef of id_key * values | Aind of inductive -(* Les zippers *) +(** Zippers *) type zipper = | Zapp of arguments - | Zfix of vfix*arguments (* Peut-etre vide *) + | Zfix of vfix * arguments (** might be empty *) | Zswitch of vswitch type stack = zipper list @@ -48,6 +51,7 @@ type whd = | Vatom_stk of atom * stack (** Constructors *) + val val_of_str_const : structured_constant -> values val val_of_rel : int -> values @@ -62,45 +66,56 @@ val val_of_constant_def : int -> constant -> values -> values external val_of_annot_switch : annot_switch -> values = "%identity" (** Destructors *) + val whd_val : values -> whd -(* Arguments *) +(** Arguments *) + val nargs : arguments -> int val arg : arguments -> int -> values -(* Product *) +(** Product *) + val dom : vprod -> values val codom : vprod -> vfun -(* Function *) +(** Function *) + val body_of_vfun : int -> vfun -> values val decompose_vfun2 : int -> vfun -> vfun -> int * values * values -(* Fix *) +(** Fix *) + val current_fix : vfix -> int val check_fix : vfix -> vfix -> bool val rec_args : vfix -> int array val reduce_fix : int -> vfix -> vfun array * values array - (* bodies , types *) + (** bodies , types *) + +(** CoFix *) -(* CoFix *) val current_cofix : vcofix -> int val check_cofix : vcofix -> vcofix -> bool val reduce_cofix : int -> vcofix -> values array * values array - (* bodies , types *) -(* Block *) + (** bodies , types *) + +(** Block *) + val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values -(* Switch *) +(** Switch *) + val check_switch : vswitch -> vswitch -> bool val case_info : vswitch -> case_info val type_of_switch : vswitch -> values val branch_of_switch : int -> vswitch -> (int * values) array -(* Evaluation *) +(** Evaluation *) + val whd_stack : values -> stack -> whd val force_whd : values -> stack -> whd +val eta_whd : int -> whd -> values |