Stream: Elpi users & devs

Topic: ✔ Adding universe polymorphic inductive type

Enzo Crance (Jul 16 2022 at 14:12):

Hello. I am trying to forge universe polymorphic inductive types with Elpi.

When querying the Coq context, there are 2 ways to express inductives: one expressing the whole inductive type in a single Elpi value thanks to binders, and the other one with the type of the inductive type constructor, the names of the data constructors as well as their types, all split into several values. In write mode, IIUC only the first one has an API. If the other one is available (or a function to translate one into the other), please tell me.

However, I have noticed different behaviours.

Inductive tree (A : Type) :=
  | leaf : A -> tree A
  | node : A -> list (tree A) -> tree A.

Elpi Query lp:{{
  pglobal (indt I) _ = {{ tree }},
  coq.env.indt-decl I D,
  coq.env.indt I _ _ _ Ty Ks KTs.
}}.

The query gives the following result for the binder version:

D = parameter A explicit (sort typ «Var(0)») c0 \
 inductive tree tt (arity sort typ «Test.37») c1 \
  [constructor leaf (arity prod `_` c0 c2 \ c1),
   constructor node
    (arity prod `_` c0 c2 \ prod `_` (app [global indt «list», c1]) c3 \ c1)]

and the following one for the other version:

I = «tree»
  KTs = [prod `A` (sort typ «Test.38») c0 \
  prod `_` c0 c1 \ app [pglobal (indt «tree») «Test.38», c0],
 prod `A` (sort typ «Test.38») c0 \
  prod `_` c0 c1 \
   prod `_`
    (app
      [global indt «list», app [pglobal (indt «tree») «Test.38», c0]])
    c2 \ app [pglobal (indt «tree») «Test.38», c0]]
Ks = [«leaf», «node»]
Ty = prod `A` (sort typ «Test.38») c0 \ sort typ «Test.39»

Suppose I change the names in the first version and try to re-submit it, I get this error:

Anomaly "in Univ.repr: Universe Var(0) undefined."
Please report at http://coq.inria.fr/bugs/.

So I think the universe for the variable A is bound in the inductive declaration. I think it's the expected behaviour, but then how can I declare a new inductive forged from this one? Is there a predicate to check whether a universe is bound to a declaration? If I replace it with a fresh one, does it become free? Is that a problem? Thanks in advance!

Notification Bot (Jul 16 2022 at 14:14):

Enzo Crance has marked this topic as unresolved.

Enrico Tassi (Jul 16 2022 at 14:24):

I think it is a bug, we should have substituted these variables for fresh univs in coq.env.indt-decl but we did not. (I guess)

Enrico Tassi (Jul 16 2022 at 14:25):

Like we do here: https://github.com/LPCIC/coq-elpi/blob/24df91cd476c072ad15f3c6402e6dd12e43e96f3/src/coq_elpi_HOAS.ml#L2965

Enrico Tassi (Jul 16 2022 at 14:32):

The coq data structure is different, dunno if we have the api that does the subst all at once or not. Maybe we do call it on the types of contructors but I forgot parameters... I don't have time now, it should be indtdecl2lp or something like that.

Enrico Tassi (Jul 16 2022 at 19:17):

Here it is: I do it for the constructors: https://github.com/LPCIC/coq-elpi/blob/24df91cd476c072ad15f3c6402e6dd12e43e96f3/src/coq_elpi_HOAS.ml#L3085 but I forgot to do it for params : https://github.com/LPCIC/coq-elpi/blob/24df91cd476c072ad15f3c6402e6dd12e43e96f3/src/coq_elpi_HOAS.ml#L3142

Enrico Tassi (Jul 16 2022 at 20:36):

fixed in master

Notification Bot (Jul 16 2022 at 20:36):

Enrico Tassi has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC