diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-25 16:28:00 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-02 21:51:37 +0100 |
| commit | c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 (patch) | |
| tree | ce4477f62d286f44a0d6055fd2f6bc38455168c8 /kernel/cbytegen.ml | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
[VM] Unify Const_sorts and Const_type, and remove Vsort.
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3104d5751..0d7619e9f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -480,23 +480,23 @@ let rec compile_lam env reloc lam sz cont = (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sorts s) sz cont + compile_structured_constant reloc (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin + (* We separate global and local universes in [u]. The former will be part + of the structured constant, while the later (if any) will be applied as + arguments. *) + let open Univ in begin let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in if List.is_empty s then - compile_structured_constant reloc (Const_sorts (Sorts.Type u)) sz cont + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont else - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in comp_app compile_structured_constant compile_get_univ reloc - (Const_type u) (Array.of_list s) sz cont + (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont end | Llet (id,def,body) -> |