Ali Caglayan (Mar 15 2022 at 16:44): Ali Caglayan (Mar 15 2022 at 16:44):Is there an econstr version of constr_expr?
Ali Caglayan (Mar 15 2022 at 17:01):Or let me ask a better question. I found something like this:
let c, ctx = Constrintern.interp_constr env sigma ce in
let c = EConstr.to_constr sigma c in
Here to_constr is failing because there are evars present in c. What is the correct way to check for the presence of evars and fail?
Gaëtan Gilbert (Mar 15 2022 at 17:03):interp_constr shouldn't return something that has evars
Ali Caglayan (Mar 15 2022 at 17:03):Its throwing this anomaly in Evd.to_constr however:
then anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term");
Well, the idea is that you should not use the constr API on an econstr, since that API does not request the quotient in sigma (an assigned evar is indistinguishable bfrom its value).
Enrico Tassi (Mar 15 2022 at 17:05):so what do you want to do, exactly?
Gaëtan Gilbert (Mar 15 2022 at 17:06):the econstr returned by interp_constr doesn't have evars
Gaëtan Gilbert (Mar 15 2022 at 17:06):that's why interp_constr returns a ustate and not an evar map
Ali Caglayan (Mar 15 2022 at 17:07):I'm investigating the anomaly in https://github.com/coq/coq/issues/6115
Ali Caglayan (Mar 15 2022 at 17:07):A similar patch a few months ago seems to only be a work around https://github.com/coq/coq/pull/14264
Ali Caglayan (Mar 15 2022 at 17:08):PMP said in that patch to use EConstr rather than Constr
Ali Caglayan (Mar 15 2022 at 17:08):but hint rewrite (extratactics.mlg ln 215) uses constr_expr
Ali Caglayan (Mar 15 2022 at 17:08):I'm confused as to why the anomaly is triggering
Gaëtan Gilbert (Mar 15 2022 at 17:10):Gaëtan Gilbert said:
the econstr returned by interp_constr doesn't have evars
I was wrong
it should have no new evars (ie no evars not appearing in the argument sigma)
weird spec
Ali Caglayan (Mar 15 2022 at 17:18):Right so somewhere something is introducing new evars?
Ali Caglayan (Mar 15 2022 at 17:19):let add_rewrite_hint ~locality ~poly bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
let f ce =
let c, ctx = Constrintern.interp_constr env sigma ce in
let c = EConstr.to_constr sigma c in
let ctx =
let ctx = UState.context_set ctx in
if poly then ctx
else (* This is a global universe context that shouldn't be
refreshed at every use of the hint, declare it globally. *)
(DeclareUctx.declare_universe_context ~poly:false ctx;
Univ.ContextSet.empty)
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
let eqs = List.map f lcsr in
let add_hints base = add_rew_rules ~locality base eqs in
List.iter add_hints bases
in https://github.com/coq/coq/blob/47ad43b361960f2bb9c5149cfb732cdf8b04e411/pretyping/pretyping.ml#L284-L301
somehow check_evars_are_solved succeeds even though there are unsolved evars
before the frozen_and_pending_holes sigma is
?X16==[ |- Type@{foo.4} => ?var] (underscore) (aliased to ?X17)
?X17==[ |- Type@{foo.4}] (underscore) {?var}
?X18==[ |- forall x y : ?var, Decidable (eq ?var x y) =>
?dec_eq_var] (underscore) (aliased to ?X19)
?X19==[ |- forall x y : ?var, Decidable (eq ?var x y)] (underscore) {?dec_eq_var}
TYPECLASSES:?X19
SHELF:
FUTURE GOALS STACK:?X19 ?X17
after apply_typeclasses sigma is
?X16==[ |- Type@{foo.4} => word ?sz] (underscore) (aliased to ?X17)
?X17==[ |- Type@{foo.4} => word ?sz] (underscore)
?X18==[ |- forall x y : word ?sz, Decidable (eq (word ?sz) x y)
=> dec_eq_word ?sz] (underscore) (aliased to ?X19)
?X19==[ |- forall x y : word ?sz, Decidable (eq (word ?sz) x y)
=> dec_eq_word ?sz] (underscore)
?X20==[ |- nat] (instance of sz) {?sz}
UNIVERSES:
{} |= foo.2 <= foo.4
ALGEBRAIC UNIVERSES:
{}
UNDEFINED UNIVERSES:
WEAK CONSTRAINTS:
SHELF:?X20
FUTURE GOALS STACK:
it seems it gets confused about the ?X20 evars somehow
Gaëtan Gilbert (Mar 15 2022 at 17:37):I don't understand what this frozen stuff is supposed to do tbh
Last updated: Sep 09 2024 at 05:02 UTC