universe polymorphism

Changelog.md

@@ -4,12 +4,78 @@
 
 Requires Elpi 1.15.0 and Coq 8.16.
 
+The main changes are:
+- experimental support for universe polymorphism
+- command arguments are elaborated by Coq (unless told otherwise)
+
 ### HOAS
-- Change arguments are passed after elaboration
-- New attribute `#[arguments(raw)]` to get arguments in raw format
+- Change arguments to commands are elaborated by Coq
+- New attribute `#[arguments(raw)]` to get arguments in raw format (as in
+  version 1.14 or below)
 - Change raw inductive declaration using `|` to mark non-uniform
   parameters is expected to not pass uniform parameters to the inductive
-  type (the same behavior applies to elaborated arguments)
+  type (the same behavior applies to elaborated arguments, making the two
+  consistent)
+- New `pglobal` term constructor carrying a `gref` and a `univ-instance` for
+  universe polymorphic terms
+- New `upoly-indt-decl` argument type for polymorphic inductive types
+  declarations
+- New `upoly-const-decl` argument type for polymorphic definitions
+- New `upoly-decl` data type for universe parameters declarations, i.e.
+  the `@{u1 u2 | u1 < u2}` Coq syntax one can use for inductives or definitions
+- New `upoly-decl-cumul` data type for universe parameters declarations, i.e.
+  the `@{u1 u2 | u1 < u2}` Coq syntax one can use for cumulative inductives
+- Rename `univ` -> `sort` i.e. `(sort S)` is a `term` and `S` can be `prop` or
+  `(type U)` where `U` is a `univ`
+- New `univ-instance` opaque type to represent how a polymorphic constant is
+  instantiated, i.e. `(pglobal GR I)` where `GR` is a `gref` and `I` a
+  `univ-instance`
+- New `univ-variable` opaque type for `univ` which are not algebraic. This data
+  type is used in `upoly-decl` and `upoly-decl-cumul`
+
+### API
+- New `@uinstance!` attribute supported by many `coq.env.*` APIs that can be
+  used to read/write the universe instance of polymorphic constants. E.g.
+  `@uinstance! UI => coq.env.typeof GR Ty` can instantiate `Ty` to `UI` if
+  provided or set `UI` to a fresh instance if not
+- New `@udecl!` attribute to declare polymorphic constants or inductives,
+  like the `@{u1 u2 | u1 < u2}` Coq syntax
+- New `@udecl-cumul!` attribute to declare polymorphic inductives,
+  like the `@{+u1 u2 | u1 < u2}` Coq syntax
+- New `@univpoly!` shorter version of `@udecl!`,
+  like the `#[universes(polymorphic)]` Coq syntax (without giving any other
+  `@{u1 u2 | u1 < u2}` directive)
+- New `@univpoly-cumul!` shorter version of `@udecl-cumul!`, like
+  the `#[universes(polymorphic,cumulative)]` Coq syntax
+- New `coq.env.global` API to craft a `term` from a `gref`. When used with
+  spilling `{coq.env.global GR}` gives either `(global GR)` or `(pglobal GR I)`
+  depending on `GR` being universe polymorphic or not. It understands the
+  `@unistance!` attribute for both reading or setting `I`
+- New `coq.env.univpoly?` to tell if a `gref` is universe polymorphic and how
+  many parameters it has
+- Change `coq.univ.leq` -> `coq.sort.leq`
+- Change `coq.univ.eq` -> `coq.sort.eq`
+- Change `coq.univ.sup` -> `coq.sort.sup`
+- New `coq.sort.pts-triple` computes the resulting `sort` of a product
+- New `coq.univ.constraints` gives all the universe constraints in a first class
+  form
+- Change `coq.univ.new` does not take a list anymore
+- New `coq.univ` to find a global universe
+- New `coq.univ.global?` tests if a universe is global
+- New `coq.univ.variable` links a `univ` to a `univ-variable` (imposing an
+  equality constraint if needed)
+- New `coq.univ.variable.constraints` finds all constraints talking about a
+  variable
+- New `coq.univ-instance` links a `univ-instance` to a list of of
+  `univ-variable`
+- New `coq.univ-instance.unify-eq` unifies two `univ-instance`
+  (for the same `gref`)
+- New `coq.univ-instance.unify-leq` unifies two `univ-instance`
+  (for the same `gref`)
+- New `coq.univ.set` OCaml's set for `univ`
+- New `coq.univ.map` OCaml's map for `univ`
+- New `coq.univ-variable.set` OCaml's set for `univ-variable`
+- New `coq.univ-variable.map` OCaml's map for `univ-variable`
 
 ### Vernacular
 - New `Accumulate File <ident>` to be used in tandem with Coq 8.16

apps/derive/elpi/cast.elpi

@@ -8,7 +8,7 @@ namespace derive.cast {
 
 namespace aux {
 
-arity [] _ (sort (typ U)) :- coq.univ.new [] U.
+arity [] _ (sort (typ U)) :- coq.univ.new U.
 arity [V|VS] Acc (prod `x` T R) :-
   coq.mk-app V {rev Acc} T,
   pi x\ arity VS [x|Acc] (R x).

apps/derive/elpi/induction.elpi

@@ -78,7 +78,7 @@ hyps [] [] Ity Arity (fix `IH` Recno Fty Bo) :-
 
 pred truncated-predicate-ty i:term, o:term.
 truncated-predicate-ty (sort _) T :- informative, !,
-  T = sort (typ U), coq.univ.new [] U.
+  T = sort (typ U), coq.univ.new U.
 truncated-predicate-ty (sort _) (sort prop).
 
 truncated-predicate-ty (prod N S T) (prod N S R) :-

apps/derive/elpi/param1.elpi

@@ -12,7 +12,7 @@ coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS.
 % this is outside the namespace since the predicate is also the db-one
 reali (sort prop as P) (fun `s` P x\ prod `s1` x _\ P) :- !.
 reali (sort _) (fun `s` (sort (typ U)) x\ prod `s1` x _\ (sort (typ V))) :- !,
-  coq.univ.new [] U, coq.univ.new [] V.
+  coq.univ.new U, coq.univ.new V.
 
 reali (fun N T B) (fun N T x\ fun N1 (TRsubst x) xR\ BR x xR) :- !, do! [
   coq.name-suffix `P` N N1,

apps/derive/elpi/param2.elpi

@@ -13,7 +13,7 @@ coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS.
 param (sort prop as P) P (fun `s` P x\ fun `s` P y\ prod `s1` x _\ prod `s2` y _\ P) :- !.
 param (sort _ as P) P
   (fun `u` (sort (typ U)) x\ fun `v` (sort (typ V)) y\ prod `s1` x _\ prod `s2` y _\ P) :- !,
-  coq.univ.new [] U, coq.univ.new [] V.
+  coq.univ.new U, coq.univ.new V.
 
 param (fun N T B) (fun N T1 B1)
       (fun N T x\ fun N T1 x1\ fun N (TRsubst x x1) xR\ BR x x1 xR) :- !, do! [

apps/locker/elpi/locker.elpi

@@ -4,23 +4,25 @@
 
 namespace locker {
 
-pred key-lock i:id, i:term, i:arity.
-key-lock ID BoSkel AritySkel :- std.do! [
+pred key-lock i:id, i:term, i:arity, i:option upoly-decl.
+key-lock ID Bo Arity UnivDecl :- std.spy-do! [
   make-key ID Key,
 
-  coq.arity->term AritySkel TySkel,
+  coq.arity->term Arity Ty,
+  Def = {{ @locked_with lp:Key lp:Ty lp:Bo }},
   std.assert-ok!
-    (coq.elaborate-skeleton
-      {{ @locked_with lp:Key lp:TySkel lp:BoSkel }} DefTy Def)
+    (coq.typecheck Def _)
     "locker: illtyped definition",
-  coq.env.add-const ID Def DefTy @transparent! C,
 
-  coq.arity->implicits AritySkel CImpls,
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-const ID Def Ty @transparent! C,
+
+  coq.arity->implicits Arity CImpls,
   if (coq.any-implicit? CImpls)
      (coq.arguments.set-implicit (const C) [CImpls])
      true,
 
-  make-key-unlockable ID Def DefTy (global (const C)) Key,
+  make-key-unlockable ID Def Ty {coq.env.global (const C)} Key,
 ].
 
 pred make-key i:id, o:term.
@@ -31,16 +33,26 @@ make-key ID (global (const C)) :- std.do! [
 
 % -------------------------------------------------------------------------
 
-pred module-lock i:id, i:term, i:arity.
-module-lock ID BoSkel AritySkel :- std.do! [
-  std.assert-ok! (coq.elaborate-arity-skeleton AritySkel _ Arity)
-    "locker: definition type illtyped",
+pred module-lock i:id, i:term, i:arity, i:option upoly-decl.
+module-lock ID Bo Arity UnivDecl :- std.do! [
   coq.arity->term Arity Ty,
-  std.assert-ok! (coq.elaborate-skeleton BoSkel Ty Bo)
-    "locker: definition body illtyped",
-
-  lock-module-type ID Ty Bo Signature,
-  lock-module-body Signature ID Ty Bo Symbol Module,
+  std.assert-ok! (coq.typecheck-ty Ty _) "locker: definition type illtyped",
+  std.assert-ok! (coq.typecheck Bo Ty) "locker: definition body illtyped",
+
+  % we craft all constants now since we need to put *in the interface* the
+  % extra universe constraints (if upoly) which are necessary for the body!
+  if (UnivDecl = some UD)
+    (std.do![
+      PTY = {{ lp:Bo = lp:Bo }},
+      std.assert-ok! (coq.typecheck-ty PTY _) "lock: unlock statement illtyped",
+      P = {{ @refl_equal lp:Ty lp:Bo }},
+      std.assert-ok! (coq.typecheck P PTY) "locker: unlock proof illtyped",
+      coq.upoly-decl.complete-constraints UD UD1,
+      UnivDecl1 = some UD1])
+    (UnivDecl1 = none),
+
+  lock-module-type ID Ty Bo UnivDecl1 Signature,
+  lock-module-body Signature ID Ty Bo UnivDecl1 Symbol Module,
 
   @global! => coq.notation.add-abbreviation ID 0 Symbol ff _,
 
@@ -52,46 +64,51 @@ module-lock ID BoSkel AritySkel :- std.do! [
   make-module-unlockable ID Module,
 ].
 
-pred lock-module-type i:id, i:term, i:term, o:modtypath.
-lock-module-type ID Ty Bo M :- std.do! [
+pred lock-module-type i:id, i:term, i:term, i:option upoly-decl, o:modtypath.
+lock-module-type ID Ty Bo UnivDecl M :- std.do! [
   Module is ID ^ "_Locked",
   coq.env.begin-module-type Module,
-  coq.env.add-axiom "body" Ty C, B = global (const C),
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-axiom "body" Ty C, coq.env.global (const C) B,
   PTY = {{ lp:B = lp:Bo }},
   std.assert-ok! (coq.typecheck-ty PTY _) "lock: unlock statement illtyped",
-  coq.env.add-axiom "unlock" PTY _,
+  if (UnivDecl = some UD) (coq.upoly-decl.complete-constraints UD UD1, coq.upoly-decl->attribute UD1 Poly1!) (Poly1! = true),
+  Poly1! => coq.env.add-axiom "unlock" PTY _,
   coq.env.end-module-type M,
 ].
 
-pred lock-module-body o:modtypath, i:id, i:term, i:term, o:term, o:modpath.
-lock-module-body Signature ID Ty Bo B M :- std.do! [
+pred lock-module-body o:modtypath, i:id, i:term, i:term, i:option upoly-decl, o:term, o:modpath.
+lock-module-body Signature ID Ty Bo UnivDecl B M :- std.do! [
   coq.env.begin-module ID (some Signature),
-  coq.env.add-const "body" Bo Ty @transparent! C,
-  B = global (const C),
+  if (UnivDecl = some UD) (coq.upoly-decl->attribute UD Poly!) (Poly! = true),
+  Poly! => coq.env.add-const "body" Bo Ty @transparent! C,
+  coq.env.global (const C) B,
   P = {{ @refl_equal lp:Ty lp:B }},
   std.assert-ok! (coq.typecheck P _) "locker: unlock proof illtyped",
   PTY = {{ lp:B = lp:Bo }},
   std.assert-ok! (coq.typecheck-ty PTY _) "locker: unlock statement illtyped",
-  coq.env.add-const "unlock" P PTY @opaque! _,
+  if (UnivDecl = some UD) (coq.upoly-decl.complete-constraints UD UD1, coq.upoly-decl->attribute UD1 Poly1!) (Poly1! = true),
+  Poly1! => coq.env.add-const "unlock" P PTY @opaque! _,
   coq.env.end-module M,
 ].
 
 % -------------------------------------------------------------------------
 % Unlocking via the ssreflect Unlockable interface (CS instance)
 
 pred make-key-unlockable i:string, i:term, i:term, i:term, i:term.
-make-key-unlockable ID DefBo DefTy LockedDef Key :- std.do! [
+make-key-unlockable ID DefBo Ty LockedDef Key :- std.do! [
   % we extract the real body in order to be precise in the unlocking equation
   DefBo = {{ @locked_with _ _ lp:Bo }},
-  UnlockEQ = {{ @locked_withE lp:DefTy lp:Key lp:Bo }},
+  UnlockEQ = {{ @locked_withE lp:Ty lp:Key lp:Bo }},
   Unlock = {{ @Unlockable _ _ lp:LockedDef lp:UnlockEQ }},
   make-unlockable ID Unlock,
 ].
 
 pred make-module-unlockable i:id, i:modpath.
 make-module-unlockable ID Module :- std.do! [
   coq.env.module Module [_,UnlockEQ],
-  Unlock = {{ Unlockable lp:{{ global UnlockEQ }} }},
+  coq.env.global UnlockEQ UnlockEQT,
+  Unlock = {{ Unlockable lp:UnlockEQT }},
   make-unlockable ID Unlock,
 ].
 

apps/locker/tests/test_locker.v

@@ -62,3 +62,17 @@ Module elab.
 mlock Definition y (z : nat) := ltac:(exact z).
 mlock Definition q (b : bool) := if b then 1 else 0.
 End elab.
+
+(* ----------------------- *)
+
+Set Printing Universes.
+
+lock #[universes(polymorphic)] Definition id1@{u} (T : Type@{u}) (x : T) := x.
+About id1.
+
+mlock #[universes(polymorphic)] Definition id2@{u} (T : Type@{u}) (x : T) := x.
+About id2.
+About id2.body.
+(* id2.body@{u} : forall T : Type@{u}, T -> T
+    (* u |= u < eq.u0 *)
+*)

apps/locker/theories/locker.v

@@ -37,7 +37,13 @@ Elpi Accumulate lp:{{
     coq.parse-attributes A [
       att "key" string,
     ] Opts, !,
-    Opts => locker.key-lock ID Bo Ty.
+    Opts => locker.key-lock ID Bo Ty none.
+  main [upoly-const-decl ID (some Bo) Ty UnivDecl] :- !,
+    attributes A,
+    coq.parse-attributes A [
+      att "key" string,
+    ] Opts, !,
+    Opts => locker.key-lock ID Bo Ty (some UnivDecl).
   main _ :- coq.error "Usage: lock Definition ...".
 }}.
 Elpi Typecheck.
@@ -67,7 +73,8 @@ mlock Definition foo : T := bo.
 Elpi Command mlock.
 Elpi Accumulate File locker.
 Elpi Accumulate lp:{{
-  main [const-decl ID (some Bo) Ty] :- !, locker.module-lock ID Bo Ty.
+  main [const-decl ID (some Bo) Ty] :- !, locker.module-lock ID Bo Ty none.
+  main [upoly-const-decl ID (some Bo) Ty UD] :- !, locker.module-lock ID Bo Ty (some UD).
   main _ :- coq.error "Usage: mlock Definition ...".
 }}.
 Elpi Typecheck.