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?)
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.
Also, Global.env is a code smell.
Is the string-lookup cost of
Luckily the place that I'm looking to use this has env and sigma already, so I guess I can just use
But, hm, MetaCoq seems to use
Global.env () all over the place, even in functions where there's already an
env floating around...
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