diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-14 16:16:13 -0800 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-26 09:18:03 +0100 |
commit | 42d91c271a176de5029c216ef74e913ac7dec2e1 (patch) | |
tree | 85e06970be224d3f11bb07f9af5015bb70014fe1 /kernel/pre_env.mli | |
parent | 05e0b45a254ab37e912e677d732aca20389263a8 (diff) |
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.
Diffstat (limited to 'kernel/pre_env.mli')
-rw-r--r-- | kernel/pre_env.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 335ca1057..a6b57bd1b 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -36,9 +36,9 @@ type stratification = { type lazy_val -val force_lazy_val : lazy_val -> (values * Id.Set.t) option +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit type named_context_val = private { env_named_ctx : Context.Named.t; |