diff options
author | 2013-05-08 18:03:54 +0200 | |
---|---|---|
committer | 2013-05-08 18:03:54 +0200 | |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /kernel/vm.mli | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
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 |