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/nativenorm.ml5
-rw-r--r--pretyping/vnorm.ml19
-rw-r--r--test-suite/bugs/closed/bug_13841.v11
-rw-r--r--test-suite/bugs/closed/bug_7631.v6
11 files changed, 67 insertions, 38 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/nativenorm.ml b/pretyping/nativenorm.ml
index 2c107502f4..b19dbd46be 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -135,8 +135,9 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
let construct_of_constr const env sigma tag typ =
- let t, l = app_type env typ in
- match EConstr.kind_upto sigma t with
+ let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in
+ let t, l = decompose_appvect (EConstr.Unsafe.to_constr typ) in
+ match Constr.kind t with
| Ind (ind,u) ->
construct_of_constr_notnative const env tag ind u l
| _ ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index cf6d581066..9939764069 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -78,8 +78,9 @@ let type_constructor mind mib u (ctx, typ) params =
-let construct_of_constr const env tag typ =
- let (t, allargs) = decompose_appvect (whd_all env typ) in
+let construct_of_constr const env sigma tag typ =
+ let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in
+ let t, allargs = decompose_appvect (EConstr.Unsafe.to_constr typ) in
match Constr.kind t with
| Ind ((mind,_ as ind), u as indu) ->
let mib,mip = lookup_mind_specif env ind in
@@ -92,8 +93,8 @@ let construct_of_constr const env tag typ =
assert (Constr.equal t (Typeops.type_of_int env));
(mkInt (Uint63.of_int tag), t)
-let construct_of_constr_const env tag typ =
- fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+ fst (construct_of_constr true env sigma tag typ)
let construct_of_constr_block = construct_of_constr false
@@ -156,7 +157,7 @@ and nf_whd env sigma whd typ =
let _, args = nf_args env sigma vargs t in
mkApp(cfd,args)
| Vconstr_const n ->
- construct_of_constr_const env n typ
+ construct_of_constr_const env sigma n typ
| Vconstr_block b ->
let tag = btag b in
let (tag,ofs) =
@@ -165,7 +166,7 @@ and nf_whd env sigma whd typ =
| Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1)
| _ -> assert false
else (tag, 0) in
- let capp,ctyp = construct_of_constr_block env tag typ in
+ let capp,ctyp = construct_of_constr_block env sigma tag typ in
let args = nf_bargs env sigma b ofs ctyp in
mkApp(capp,args)
| Vint64 i -> i |> Uint63.of_int64 |> mkInt
@@ -414,9 +415,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.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 93aeb83e28..14ab4de9b7 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x.
Definition barvm (x := foo) := Eval vm_compute in x.
End RelContext.
+
+Definition bar (t:=_) (x := true : t) := Eval native_compute in x.
+Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x.
+
+Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x.
+Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:24:50 +0000