Safer VM interfaces

We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.

This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).

This is also preliminary work for integers and arrays.

1 files changed, 8 insertions, 98 deletions

diff --git a/kernel/vm.mli b/kernel/vm.mli
index bc38452d4..c6d92ba26 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -6,118 +6,28 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constr
-open Cbytecodes
+open Vmvalues
 
 (** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-(** Machine code *)
-
-type tcode
-
-(** Values *)
-
-type vprod
-type vfun
-type vfix
-type vcofix
-type vblock
-type vswitch
-type arguments
-
-type atom =
-  | Aid of Vars.id_key
-  | Aind of inductive
-  | Atype of Univ.Universe.t
-
-(** Zippers *)
-
-type zipper =
-  | Zapp of arguments
-  | Zfix of vfix * arguments  (** might be empty *)
-  | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
-
-type stack = zipper list
-
-type to_up
-
-type whd =
-  | Vsort of Sorts.t
-  | Vprod of vprod
-  | Vfun of vfun
-  | 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
-  | Vuniv_level of Univ.Level.t
-
-(** For debugging purposes only *)
-
-val pr_atom : atom -> Pp.t
-val pr_whd : whd -> Pp.t
-val pr_stack : stack -> Pp.t
-
-(** Constructors *)
-
-val val_of_str_const : structured_constant -> values
-val val_of_rel : int -> values
-val val_of_named : Id.t -> values
-val val_of_constant : Constant.t -> values
-
-external val_of_annot_switch : annot_switch -> values = "%identity"
-
-(** Destructors *)
-
-val whd_val : values -> whd
-val uni_lvl_val : values -> Univ.Level.t
-
-(** 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
 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 *)
+val type_of_switch : vswitch -> values
 
-val btag  : vblock -> int
-val bsize : vblock -> int
-val bfield : vblock -> int -> values
+val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Switch *)
+val reduce_fun : int -> vfun -> values
 
-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
+(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current
+    DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced
+    bodies under those lambdas. *)
+val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
 (** Apply a value *)