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
The issue I'm running into is that I'm experimenting with calling
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.
The docs here also mention the
Universes.constr_of_global function, but it doesn't seem to exist anymore.
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)
Okay, thanks. Where exactly does elaboration happen (e.g. where Top.xx gets created)? Is it in pretyping, or constrintern?
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.
Why are you doing typing inside search_guard anyway?
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
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.
I hadn't' seen your paper, https://arxiv.org/pdf/1912.05601.pdf , interesting!
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
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: Feb 22 2024 at 04:02 UTC