- Ajout d'un cast vm dans la syntaxe : x <: t

    Part contre ces cas sont detruis dans les "Definition" 
    (pas dans les "Lemma") je comprends pas ou ils sont enlev'e...
    Si une id'ee ...

- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.

- Meilleur compilation des coinductifs, on utilise maintenant vraimment
  du lazy. 

- Enfin un peu plus de doc dans le code de la vm.

  Benjamin



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 30 insertions, 35 deletions

diff --git a/kernel/vm.mli b/kernel/vm.mli
index b5fd9b9db..279ac9370 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