Stream: Elpi users & devs

Topic: Adding universe polymorphic inductive type


view this post on Zulip 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!

view this post on Zulip Notification Bot (Jul 16 2022 at 14:14):

Enzo Crance has marked this topic as unresolved.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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


Last updated: Feb 05 2023 at 14:02 UTC