Jonathan Chan (May 20 2020 at 21:54): Jonathan Chan (May 20 2020 at 21:54):Where is it that universe levels are added to the (global?) environment?
In particular, I'm looking at DeclareDef.declare_mutually_recursive, and I can see that vars contains all the levels from fixdecls, but I can't find the specific step where the env gets updated. I'm not sure what part of the env is updated either, but I'm assuming it's env_stratification.env_universes or .env_universes_lbound.
The issue I'm running into is that I'm experimenting with calling Typeops.infer/.execute from Pretyping.search_guard, but I get the error Anomaly "Universe Top.x undefined". I was hoping there'd be a quick way to stick the universe level variables in the right place for now.
Jonathan Chan (May 20 2020 at 22:17):The docs here also mention the Universes.constr_of_global function, but it doesn't seem to exist anymore.
Gaëtan Gilbert (May 21 2020 at 09:42):During elaboration universe levels are in the evar map. You can't use typeops with an evar map so use Typing instead (pretyping/typing.ml)
Jonathan Chan (May 21 2020 at 22:01):Okay, thanks. Where exactly does elaboration happen (e.g. where Top.xx gets created)? Is it in pretyping, or constrintern?
Jonathan Chan (May 21 2020 at 23:27):So I'm not sure how I could use Typing from inside of search_guard, since it doesn't take a evar_map (and it seems like I have to go through search_guard, since places that guess the fixpoint indices call search_guard, not esearch_guard).
Also, is there a paper or a reference I could read that describes what Pretyping/Typing/elaboration is doing? Something like the CIC chapter in the Coq manual, but for how (I'm assuming) all the type (and universe?) unification is done.
Gaëtan Gilbert (May 22 2020 at 09:14):Why are you doing typing inside search_guard anyway?
Jonathan Chan (May 22 2020 at 09:26):I've got a sized types implementation in Typeops (size inference and checking) and I'm trying to figure out how to modify search_guard so it can use that when guessing the fixpoint indices
I used to have a workaround where I'd ignore search_guard and stick the user-provided indices in Fix during pretyping and do the guessing later inside of Typeops, but at some point things shifted around and other places are calling search_guard directly instead of going through pretyping
Gaëtan Gilbert (May 22 2020 at 10:16):I see.
Indeed we call search_guard at the end of Fixpoint and similar commands with an environment missing universes.
I guess this is similar to how we used to cal it in an environment without the side effects (= constants declared by abstract) which caused https://github.com/coq/coq/issues/3344 fixed by https://github.com/coq/coq/commit/efa3add0c03b70ecda3890cc6c69e66850605e7d (this code is https://github.com/coq/coq/blob/90389df4d03a6a6232e0372ff3efee720f85d284/vernac/declare.ml#L1767 in master).
As you can see it does some ad-hoc adding to the environment.
Emilio Jesús Gallego Arias (May 22 2020 at 10:38):I hadn't' seen your paper, https://arxiv.org/pdf/1912.05601.pdf , interesting!
Jonathan Chan (May 22 2020 at 16:25):Yeah I'm planning on making a draft pull request at some point just to bring it into visibility, after I fix all these small issues
Jonathan Chan (Aug 13 2020 at 22:56):Is AcyclicGraph.sort the place where universe level variables get instantiated with concrete levels? I'm looking for where Print Sorted Universes would be doing the sorting
Last updated: Jun 09 2023 at 07:01 UTC