diff options
| author | Pierre-Marie Pédrot | 2017-07-30 16:10:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-03 18:05:56 +0100 |
| commit | e82856f3108a25f7b0cabff4190bc56d3a0cafa1 (patch) | |
| tree | 712336a242276c7ceb9dcde72999ad0769faa669 /kernel/clambda.ml | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Handling evars in the VM.
We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.
This grants wish BZ#5659.
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 636ed35107..7b637c20e6 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -29,6 +29,9 @@ let rec pp_lam lam = match lam with | Lrel (id,n) -> pp_rel id n | Lvar id -> Id.print id + | Levar (evk, args) -> + hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") | Lprod(dom,codom) -> hov 1 (str "forall(" ++ pp_lam dom ++ @@ -148,6 +151,9 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Levar (evk, args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -344,6 +350,8 @@ let rec occurrence k kind lam = if kind then false else raise Not_found else kind | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Levar (_, args) -> + occurrence_args k kind args | Lprod(dom, codom) -> occurrence k (occurrence k kind dom) codom | Llam(ids,body) -> @@ -600,7 +608,9 @@ open Renv let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar") + | Evar (evk, args) -> + let args = lambda_of_args env 0 args in + Levar (evk, args) | Cast (c, _, _) -> lambda_of_constr env c |