summaryrefslogtreecommitdiff
path: root/kernel/vm.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /kernel/vm.mli
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'kernel/vm.mli')
-rw-r--r--kernel/vm.mli65
1 files changed, 30 insertions, 35 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
index b5fd9b9d..279ac937 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -13,45 +13,41 @@ 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 atom =
+ | Aid of id_key
+ | Aiddef of id_key * values
+ | Aind of inductive
+
+(* Les zippers *)
+
type zipper =
| Zapp of arguments
- | Zfix of vfix_app
+ | Zfix of vfix*arguments (* Peut-etre vide *)
| 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 to_up
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
+ | Vfix of vfix * arguments option
+ | Vcofix of vcofix * to_up * arguments option
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
-
-(* Constructors *)
+
+(** Constructors *)
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
@@ -63,44 +59,43 @@ val val_of_named_def : identifier -> values -> values
val val_of_constant : constant -> values
val val_of_constant_def : int -> constant -> values -> values
-(* Destructors *)
+(** 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 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 current_fix : vfix -> int
val check_fix : vfix -> vfix -> bool
-val bodies_of_fix : int -> vfix -> vfun array
-val types_of_fix : vfix -> values array
+val rec_args : vfix -> int array
+val reduce_fix : int -> vfix -> vfun array * values array
+ (* bodies , types *)
+
(* CoFix *)
-val cofix : vcofix_app -> vcofix
-val args_of_cofix : vcofix_app -> arguments
-val cofix_init : vcofix -> int
-val cofix_ndef : vcofix -> int
+val current_cofix : vcofix -> int
val check_cofix : vcofix -> vcofix -> bool
-val bodies_of_cofix : int -> vcofix -> values array
-val types_of_cofix : vcofix -> values array
+val reduce_cofix : int -> vcofix -> values array * values array
+ (* bodies , types *)
(* Block *)
val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> values
+
(* Switch *)
-val eq_tbl : vswitch -> vswitch -> bool
+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
-(* Arguments *)
-val nargs : arguments -> int
-val arg : arguments -> int -> values
(* Evaluation *)
val whd_stack : values -> stack -> whd