search

gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

Reification of Universes! #1

Open gmalecha opened 10 years ago

gmalecha commented 10 years ago

It probably isn't too bad to determine the universe levels, but there doesn't seem to be any convenient way to denote them.

gmalecha commented 10 years ago

I can just use the type as the universe level (though this could induce universe problems if you try to quote something with syntax inside of it).

This means that you can't see if two universes are the same, but this information does not readily exist in the kernel anyways.

gmalecha commented 10 years ago

demo of this in f250e6d66015193fdd67bb409a889118436f9730

gmalecha commented 9 years ago

Going to solve this in master using a reification map.

mattam82 commented 8 years ago

One could reify using a map from level list (level being a positive with a boolean for +1 potentially) to Type. (That last type will be higher than any other). In the universe polymorphic case the term under the universe context refers to the universe context variables (internally, using de Bruijn indices, but you probably don't see it if you get the body of e.g. id@{i} := fun (A : Type@{Var 0}) (a : A) => a then the body you get is "fun (A: Type@{i}) (a : A) => A".

gmalecha commented 8 years ago

One issue that we might run into is that you can never write a Gallina term that is universe polymorphic because the top-level always instantiates it with fresh variables. When we quote, we will either need to figure this out, or not really quote universe polymorphism.

Potentially the annoying bit with universes is that constraints might dictate that two universes are equal, but they will appear syntactically different. Perhaps this isn't a problem though because it appears the same way in Coq.

aa755 commented 7 years ago

Because one cannot analyze a Type in Gallina, writing program transformations with an intent of unquoting can be problematic if we define Ast.universe:=Type. Can we instead define Ast.universe:=string? To support universe polymorphism, quoting of definitions will perhaps need to be updated to also reify the context of universes (as list of names?). Analogous changes would be needed in the unquoting function: the user will have to specify the local universe context as a list of names. For universe names not in the context, the unquoting function would create fresh rigid universe levels?

Also, is there a way to implement unquoting (e.g. Make Definition) such that the user doesn't have to specify the universe constraints needed for a definition to typecheck and let Coq figure them out?