diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 48 |
1 files changed, 33 insertions, 15 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3104d57514..0766f49b39 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction @@ -257,6 +259,15 @@ let pos_universe_var i r sz = r.in_env := push_fv db env; Kenvacc(r.offset + pos) +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -427,6 +438,7 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont | FVuniv_var i -> pos_universe_var i reloc sz :: cont + | FVevar evk -> pos_evar evk reloc :: cont let rec compile_fv reloc l sz cont = match l with @@ -471,6 +483,12 @@ let rec compile_lam env reloc lam sz cont = | Lvar id -> pos_named id reloc :: cont + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem reloc (FVevar evk) sz cont + else + comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont | Lind (ind,u) -> @@ -480,23 +498,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) -> |