Stream: Coq devs & plugin devs

Topic: econstr version of constr_expr


view this post on Zulip Ali Caglayan (Mar 15 2022 at 16:44):

Is there an econstr version of constr_expr?

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Mar 15 2022 at 17:03):

interp_constr shouldn't return something that has evars

view this post on Zulip 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");

view this post on Zulip Enrico Tassi (Mar 15 2022 at 17:04):

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).

view this post on Zulip Enrico Tassi (Mar 15 2022 at 17:05):

so what do you want to do, exactly?

view this post on Zulip Gaëtan Gilbert (Mar 15 2022 at 17:06):

the econstr returned by interp_constr doesn't have evars

view this post on Zulip Gaëtan Gilbert (Mar 15 2022 at 17:06):

that's why interp_constr returns a ustate and not an evar map

view this post on Zulip Ali Caglayan (Mar 15 2022 at 17:07):

I'm investigating the anomaly in https://github.com/coq/coq/issues/6115

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 15 2022 at 17:08):

PMP said in that patch to use EConstr rather than Constr

view this post on Zulip Ali Caglayan (Mar 15 2022 at 17:08):

but hint rewrite (extratactics.mlg ln 215) uses constr_expr

view this post on Zulip Ali Caglayan (Mar 15 2022 at 17:08):

I'm confused as to why the anomaly is triggering

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Mar 15 2022 at 17:18):

Right so somewhere something is introducing new evars?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Mar 15 2022 at 17:36):

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

view this post on Zulip Gaëtan Gilbert (Mar 15 2022 at 17:37):

I don't understand what this frozen stuff is supposed to do tbh


Last updated: Feb 05 2023 at 20:03 UTC