aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vm.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 16:06:42 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 16:06:42 +0000
commitccba6c718af6a5a15f278fc9365b6ad27108e98f (patch)
treef0229aa4d08eb12db1fb1e76f227076c117d59bf /kernel/vm.mli
parent06456c76b7fa2f0c69380faf27a6ca403b1e6f3f (diff)
Various minor improvements of comments in mli for ocamldoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vm.mli')
-rw-r--r--kernel/vm.mli25
1 files changed, 19 insertions, 6 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
index ff76e7cd5..cd5999f04 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -3,16 +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
@@ -27,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
@@ -49,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
@@ -63,21 +66,26 @@ 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 *)
+
val nargs : arguments -> int
val arg : arguments -> int -> values
(** 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 current_fix : vfix -> int
val check_fix : vfix -> vfix -> bool
val rec_args : vfix -> int array
@@ -85,22 +93,27 @@ val reduce_fix : int -> vfix -> vfun array * values array
(** bodies , types *)
(** 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 *)
+
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 *)
+
val whd_stack : values -> stack -> whd
val force_whd : values -> stack -> whd