Stream: Coq devs & plugin devs

Topic: polymorphic equivalent of constr_of_monomorphic_global


view this post on Zulip Jason Gross (Apr 02 2023 at 22:39):

MetaCoq has some code

  let resolve (tm : string) : Constr.t Lazy.t =
    lazy (
      let tm_ref = Coqlib.lib_ref tm in
      UnivGen.constr_of_monomorphic_global (Global.env ()) tm_ref
    )
    (* gen_constant_in_modules contrib_name [path] tm *)

Is there a (relatively) easy way to make this work for polymorphic constants, so that, e.g., resolve returns a (unit -> Constr.t) Lazy.t that will resolve the constant the first time it's forced, and give a fresh universe instance for the given constant every time the function is called? (Is there a more idiomatic way to do this?)

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2023 at 06:35):

Why don't you just return a unit -> constr? The cost of fetching the reference is not important since you'll also have to fetch again for universe generation.

view this post on Zulip Pierre-Marie Pédrot (Apr 03 2023 at 06:35):

Also, Global.env is a code smell.

view this post on Zulip Jason Gross (Apr 04 2023 at 04:00):

Is the string-lookup cost of Coqlib.lib_ref negligible?

view this post on Zulip Jason Gross (Apr 04 2023 at 04:05):

Luckily the place that I'm looking to use this has env and sigma already, so I guess I can just use Evd.fresh_global?

view this post on Zulip Jason Gross (Apr 04 2023 at 04:10):

But, hm, MetaCoq seems to use Global.env () all over the place, even in functions where there's already an env floating around...

view this post on Zulip Matthieu Sozeau (Apr 04 2023 at 14:51):

Clean-up PRs are welcome :) I guess you could just blindly parameterize by an env everywhere and pass (Global.env ()) almost everywhere. But beware that the monad actions do modify the env, so it has to be refreshed in some cases. A better Coq API giving the updated env after a definition/inductive is entered would help here


Last updated: Nov 29 2023 at 21:01 UTC