aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/vconv.ml5
-rw-r--r--kernel/vmbytegen.ml9
-rw-r--r--kernel/vmbytegen.mli6
-rw-r--r--kernel/vmlambda.ml18
-rw-r--r--kernel/vmlambda.mli2
-rw-r--r--kernel/vmsymtable.ml22
-rw-r--r--kernel/vmsymtable.mli2
-rw-r--r--pretyping/vnorm.ml6
-rw-r--r--test-suite/bugs/closed/bug_13841.v11
9 files changed, 51 insertions, 30 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1432fb9310..d31d7a03b6 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 =
TransparentState.full env univs t1 t2
else
try
- let v1 = val_of_constr env t1 in
- let v2 = val_of_constr env t2 in
+ let sigma _ = assert false in
+ let v1 = val_of_constr env sigma t1 in
+ let v2 = val_of_constr env sigma t2 in
fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
with Not_found | Invalid_argument _ ->
warn_bytecode_compiler_failed ();
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 20de4bc81b..7d3b3469b0 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -840,21 +840,21 @@ let dump_bytecodes init code fvs =
prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
fnl ())
-let compile ~fail_on_error ?universes:(universes=0) env c =
+let compile ~fail_on_error ?universes:(universes=0) env sigma c =
init_fun_code ();
Label.reset_label_counter ();
let cont = [Kstop] in
try
let cenv, init_code =
if Int.equal universes 0 then
- let lam = lambda_of_constr ~optimize:true env c in
+ let lam = lambda_of_constr ~optimize:true env sigma c in
let cenv = empty_comp_env () in
cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont
else
(* We are going to generate a lambda, but merge the universe closure
* with the function closure if it exists.
*)
- let lam = lambda_of_constr ~optimize:true env c in
+ let lam = lambda_of_constr ~optimize:true env sigma c in
let params, body = decompose_Llam lam in
let arity = Array.length params in
let cenv = empty_comp_env () in
@@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function
let con= Constant.make1 (Constant.canonical kn') in
Some (BCalias (get_alias env con))
| _ ->
- let res = compile ~fail_on_error ~universes:instance_size env body in
+ let sigma _ = assert false in
+ let res = compile ~fail_on_error ~universes:instance_size env sigma body in
Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli
index aef7ac3d6b..c724cad5ec 100644
--- a/kernel/vmbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -15,8 +15,10 @@ open Declarations
open Environ
(** Should only be used for monomorphic terms *)
-val compile : fail_on_error:bool ->
- ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
+val compile :
+ fail_on_error:bool -> ?universes:int ->
+ env -> (existential -> constr option) -> constr ->
+ (bytecodes * bytecodes * fv) option
(** init, fun, fv *)
val compile_constant_body : fail_on_error:bool ->
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 91de58b0e6..e353348ac7 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -591,12 +591,14 @@ struct
type t = {
global_env : env;
+ evar_body : existential -> constr option;
name_rel : Name.t Vect.t;
construct_tbl : (constructor, constructor_info) Hashtbl.t;
}
- let make env = {
+ let make env sigma = {
global_env = env;
+ evar_body = sigma;
name_rel = Vect.make 16 Anonymous;
construct_tbl = Hashtbl.create 111
}
@@ -633,9 +635,13 @@ open Renv
let rec lambda_of_constr env c =
match Constr.kind c with
| Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
- | Evar (evk, args) ->
- let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
- Levar (evk, args)
+ | Evar (evk, args as ev) ->
+ begin match env.evar_body ev with
+ | None ->
+ let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
+ Levar (evk, args)
+ | Some t -> lambda_of_constr env t
+ end
| Cast (c, _, _) -> lambda_of_constr env c
@@ -774,8 +780,8 @@ let optimize_lambda lam =
let lam = simplify subst_id lam in
remove_let subst_id lam
-let lambda_of_constr ~optimize genv c =
- let env = Renv.make genv in
+let lambda_of_constr ~optimize genv sigma c =
+ let env = Renv.make genv sigma in
let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in
Renv.push_rels env (Array.of_list ids);
let lam = lambda_of_constr env c in
diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli
index ad5f81638f..03d3393219 100644
--- a/kernel/vmlambda.mli
+++ b/kernel/vmlambda.mli
@@ -33,7 +33,7 @@ and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array
exception TooLargeInductive of Pp.t
-val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
+val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda
val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index ae0fa38571..90ee1c5378 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -144,7 +144,7 @@ let slot_for_proj_name key =
ProjNameTable.add proj_name_tbl key n;
n
-let rec slot_for_getglobal env kn =
+let rec slot_for_getglobal env sigma kn =
let (cb,(_,rk)) = lookup_constant_key kn env in
try key rk
with NotEvaluated ->
@@ -155,22 +155,22 @@ let rec slot_for_getglobal env kn =
| Some code ->
match Vmemitcodes.force code with
| BCdefined(code,pl,fv) ->
- let v = eval_to_patch env (code,pl,fv) in
+ let v = eval_to_patch env sigma (code,pl,fv) in
set_global v
- | BCalias kn' -> slot_for_getglobal env kn'
+ | BCalias kn' -> slot_for_getglobal env sigma kn'
| BCconstant -> set_global (val_of_constant kn)
in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (CEphemeron.create pos);
pos
-and slot_for_fv env fv =
+and slot_for_fv env sigma fv =
let fill_fv_cache cache id v_of_id env_of_id b =
let v,d =
match b with
| None -> v_of_id id, Id.Set.empty
| Some c ->
- val_of_constr (env_of_id id env) c,
+ val_of_constr (env_of_id id env) sigma c,
Environ.global_vars_set env c in
build_lazy_val cache (v, d); v in
let val_of_rel i = val_of_rel (nb_rel env - i) in
@@ -194,11 +194,11 @@ and slot_for_fv env fv =
| FVuniv_var _idu ->
assert false
-and eval_to_patch env (buff,pl,fv) =
+and eval_to_patch env sigma (buff,pl,fv) =
let slots = function
| Reloc_annot a -> slot_for_annot a
| Reloc_const sc -> slot_for_str_cst sc
- | Reloc_getglobal kn -> slot_for_getglobal env kn
+ | Reloc_getglobal kn -> slot_for_getglobal env sigma kn
| Reloc_proj_name p -> slot_for_proj_name p
| Reloc_caml_prim op -> slot_for_caml_prim op
in
@@ -207,13 +207,13 @@ and eval_to_patch env (buff,pl,fv) =
(* Environment should look like a closure, so free variables start at slot 2. *)
let a = Array.make (Array.length fv + 2) crazy_val in
a.(1) <- Obj.magic 2;
- Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv;
+ Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env sigma v) fv;
a in
eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
-and val_of_constr env c =
- match compile ~fail_on_error:true env c with
- | Some v -> eval_to_patch env (to_memory v)
+and val_of_constr env sigma c =
+ match compile ~fail_on_error:true env sigma c with
+ | Some v -> eval_to_patch env sigma (to_memory v)
| None -> assert false
let set_transparent_const _kn = () (* !?! *)
diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..c6dc09d944 100644
--- a/kernel/vmsymtable.mli
+++ b/kernel/vmsymtable.mli
@@ -14,7 +14,7 @@ open Names
open Constr
open Environ
-val val_of_constr : env -> constr -> Vmvalues.values
+val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values
val set_opaque_const : Constant.t -> unit
val set_transparent_const : Constant.t -> unit
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index cf6d581066..5622bd357a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -414,9 +414,9 @@ let cbv_vm env sigma c t =
if Termops.occur_meta sigma c then
CErrors.user_err Pp.(str "vm_compute does not support metas.");
(* This evar-normalizes terms beforehand *)
- let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
- let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
- let v = Vmsymtable.val_of_constr env c in
+ let c = EConstr.Unsafe.to_constr c in
+ let t = EConstr.Unsafe.to_constr t in
+ let v = Vmsymtable.val_of_constr env (Evd.existential_opt_value0 sigma) c in
EConstr.of_constr (nf_val env sigma v t)
let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
diff --git a/test-suite/bugs/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v
new file mode 100644
index 0000000000..60fca8b49c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13841.v
@@ -0,0 +1,11 @@
+Goal True.
+evar (p : bool).
+unify ?p true.
+let v := eval vm_compute in (orb p false) in
+match v with true => idtac end.
+assert (orb p false = true).
+vm_compute.
+match goal with |- true = _ => idtac end.
+easy.
+easy.
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:12:38 +0000