search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
134 stars 50 forks source link

Name clash in printing of results of derive.param2 #359

Open CohenCyril opened 2 years ago

CohenCyril commented 2 years ago 
From elpi Require Import derive.

Elpi derive.param2 eq.

Print eq_R.

prints

Inductive
eq_R (A A : Type) (A : A -> A -> Type) (x x : A) (x : A x x)
  : forall H H0 : A, A H H0 -> x = H -> x = H0 -> Prop :=
    eq_refl_R : eq_R A A A x x x x x x eq_refl eq_refl.

Obviously the de Brujin indices must be correct (otherwise it would not typecheck), but the names are not alpha-renamed. I wonder whether this is more a bug of Coq or Coq ELPI...

CC @gares

gares commented 2 years ago

I guess I did not do this in the code of param2:

https://github.com/LPCIC/coq-elpi/blob/cac2b9b4c802899ee6ef6ed3f63daecaae6ae3f6/apps/derive/elpi/param1.elpi#L25

CohenCyril commented 2 years ago

The culprit is a variable that does not exist in the unary version (it's the ' one)

gares commented 2 years ago

https://github.com/LPCIC/coq-elpi/blob/cac2b9b4c802899ee6ef6ed3f63daecaae6ae3f6/apps/derive/elpi/param2.elpi#L19

Instead of using N 3 times, one could use N1 and N2 and say coq.name-suffix N 1 N1 and coq.name-suffix N 2 N2 (or use "'" and "''" if you really want.

https://github.com/LPCIC/coq-elpi/blob/cac2b9b4c802899ee6ef6ed3f63daecaae6ae3f6/coq-builtin.elpi#L1287