Support for mutual inductives

Changelog.md

@@ -40,6 +40,8 @@ Requires Elpi 3.7.1 and Rocq 9.0, 9.1 or 9.2.
 - New argument `const-decl` can now be introduces by the `Lemma` keyword,
   and not just by `Definition`.
 - New `coq.scheme` to query registered schemes
+- New `coq.env.mutual-inductives` to list the inductive types in the same
+  mutual block without reifying the full inductive declaration
 
 
 # [3.3.1] 12/03/2026

apps/derive/elpi/derive.elpi

@@ -9,6 +9,25 @@ exists-indc I P :-
   coq.env.indt I _ _ _ _ KL _,
   std.exists! KL P.
 
+func mutual-ids indt-decl -> list id.
+mutual-ids (parameter ID _ Ty F) IDs :- !,
+  @pi-parameter ID Ty x\ mutual-ids (F x) IDs.
+mutual-ids (minductive ID _ Arity Rest) [ID|IDs] :- !,
+  @pi-inductive ID Arity i\ mutual-ids (Rest i) IDs.
+mutual-ids (mblock _) [].
+
+func mutual-indt-decl indt-decl ->.
+mutual-indt-decl D :- mutual-ids D IDs, std.length IDs N, N > 1.
+
+func mutual-inductive inductive ->.
+mutual-inductive I :- coq.env.mutual-inductives I GRS, std.length GRS N, N > 1.
+
+func id->indt id -> inductive.
+id->indt ID GR :- coq.locate ID (indt GR).
+
+func mutual-inductives inductive -> list inductive.
+mutual-inductives I GRS :- coq.env.mutual-inductives I GRS.
+
 func if-verbose (func) ->.
 if-verbose P :- (get-option "verbose" tt ; get-option "recursive" tt), !, P.
 if-verbose _.
@@ -148,7 +167,7 @@ decl+main TypeName DS :- std.do! [
   if-verbose (coq.say "Done"),
   if (HasModule = tt)
      (coq.env.end-module _,
-      decl+main.post TypeName I DS CL)
+      decl+main.post ModName DS CL)
      check-no-no-alias
 ].
 
@@ -157,24 +176,57 @@ check-no-no-alias :- get-option "no_alias" tt, !,
   coq.error "The no_alias attribute only has an effect when a wrapper module is generated.".
 check-no-no-alias.
 
-func decl+main.post string, inductive, indt-decl -> list prop.
-decl+main.post TypeName I DS CL :- std.do! [
-  coq.env.indt I _ _ _ _ KS _,
+func indt-decl-ids indt-decl -> list id.
+indt-decl-ids (parameter ID _ Ty F) IDs :- !,
+  @pi-parameter ID Ty x\ indt-decl-ids (F x) IDs.
+indt-decl-ids (inductive ID _ _ _) [ID] :- !.
+indt-decl-ids (minductive ID _ Arity Rest) [ID|IDs] :- !,
+  @pi-inductive ID Arity i\ indt-decl-ids (Rest i) IDs.
+indt-decl-ids (record ID _ _ _) [ID] :- !.
+indt-decl-ids (mblock _) [].
+
+func module-indt string, id -> inductive.
+module-indt ModName ID I :-
+  QName is ModName ^ "." ^ ID,
+  coq.locate QName (indt I).
+
+func indt-constructors inductive -> list constructor.
+indt-constructors I KS :- coq.env.indt I _ _ _ _ KS _.
+
+func set-indt-implicits inductive, list implicit_kind ->.
+set-indt-implicits I Impl :-
+  if (coq.any-implicit? Impl)
+     (@global! ==> coq.arguments.set-implicit (indt I) [Impl])
+     true.
+
+func set-indc-implicits constructor, list implicit_kind ->.
+set-indc-implicits K Impl :-
+  if (coq.any-implicit? Impl)
+     (@global! ==> coq.arguments.set-implicit (indc K) [Impl])
+     true.
+
+func set-indcs-implicits list constructor, list (list implicit_kind) ->.
+set-indcs-implicits KS Impls :-
+  std.forall2 KS Impls set-indc-implicits.
+
+func decl+main.post string, indt-decl -> list prop.
+decl+main.post ModName DS CL :- std.do! [
+  indt-decl-ids DS IDs,
+  std.map IDs (module-indt ModName) IS,
+  std.map IS (i\r\ r = global (indt i)) ITS,
+  std.map IS indt-constructors KBlocks,
+  std.flatten KBlocks KS,
   std.map KS (k\r\ r = indc k) KGRS,
   std.map KGRS coq.gref->id KNS,
   std.map KGRS (gr\r\ r = global gr) KTS,
 
-  std.forall2 [TypeName|KNS] [global (indt I)|KTS] short-alias,
+  std.append IDs KNS AliasNames,
+  std.append ITS KTS AliasTerms,
+  std.forall2 AliasNames AliasTerms short-alias,
 
-  coq.indt-decl->implicits DS IndImpls KsImpls,
-  if (coq.any-implicit? IndImpls)
-     (@global! ==> coq.arguments.set-implicit (indt I) [IndImpls])
-     true,
-  std.forall2 KsImpls KS (i\k\
-    if (coq.any-implicit? i)
-       (@global! ==> coq.arguments.set-implicit (indc k) [i])
-       true
-    ),
+  coq.indt-decl->implicits-all DS IndImpls KsImpls,
+  std.forall2 IS IndImpls set-indt-implicits,
+  std.forall2 KBlocks KsImpls set-indcs-implicits,
   std.map-filter CL export? P,
   std.do! P,
 ].

apps/derive/elpi/eqType.elpi

@@ -5,11 +5,43 @@
 namespace derive.eqType.ast {
 
 func translate-indt inductive -> eqb.eqType, diagnostic.
+translate-indt I O D :-
+  coq.env.mutual-inductives I GRS, std.length GRS N, N > 1, !,
+  coq.env.indt I _ Lno _ Arity KN KT,
+  translate-param-arity Lno Arity I KN KT O D.
 translate-indt I O D :-
   coq.env.indt-decl I Decl,
   coq.env.indt I _ _ _ _ KN _,
   translate-param Decl I KN O D.
 
+func translate-param-arity int, term, inductive, list constructor, list term -> eqb.eqType, diagnostic.
+translate-param-arity N (prod ID Ty F) I KS KTS (eqb.type-param F1) D :- N > 0, whd Ty [] {{ Type }} _, !,
+  @pi-decl ID Ty x\ pi y\ (term->trm x y ok :- !) ==>
+    sigma KTS1\
+      std.map KTS (coq.subst-prod [x]) KTS1,
+      N1 is N - 1,
+      translate-param-arity N1 (F x) I KS KTS1 (F1 y) D.
+translate-param-arity N (prod ID Ty F) I KS KTS (eqb.value-param Ty1 F1) D :- N > 0, term->trm Ty Ty1 ok, !,
+  @pi-decl ID Ty x\ pi y\ (term->trm x y ok :- !) ==>
+    sigma KTS1\
+      std.map KTS (coq.subst-prod [x]) KTS1,
+      N1 is N - 1,
+      translate-param-arity N1 (F x) I KS KTS1 (F1 y) D.
+translate-param-arity N (prod ID _ _) _ _ _ _ (error S) :- N > 0, !,
+  coq.name->id ID IDS,
+  S is "unsupported parameter " ^ IDS.
+translate-param-arity 0 (sort _) I KS KTS (eqb.inductive I F) D :- !,
+  pi y\ (term->trm (global (indt I)) y ok :- !) => translate-constructors-terms KTS KS (F y) D.
+translate-param-arity _ _ _ _ _ _ (error "unsupported inductive arity").
+
+:index (1)
+func translate-constructors-terms list term, list constructor -> list eqb.constructor, diagnostic.
+translate-constructors-terms [] [] [] ok.
+translate-constructors-terms [A|KS] [K|KK] [eqb.constructor K Args|KS1] D :- std.do-ok! D [
+  translate-arguments A Args,
+  translate-constructors-terms KS KK KS1,
+].
+
 func translate-param indt-decl, inductive, list constructor -> eqb.eqType, diagnostic.
 translate-param (parameter ID _ Ty F) I KS (eqb.type-param F1) D :- whd Ty [] {{ Type }} _, !,
   @pi-parameter ID Ty x\ pi y\ (term->trm x y ok :- !) => translate-param (F x) I KS (F1 y) D.
@@ -44,6 +76,8 @@ translate-arguments (prod N Ty F) (eqb.dependent Ty1 F1) D :- !, std.do-ok! D [
   (d\ @pi-decl N Ty x\ pi y\ term->trm x y ok => translate-arguments (F x) (F1 y) d),
 ].
 translate-arguments Ty (eqb.stop Ty1) D :- name Ty, term->trm Ty Ty1 D, !.
+translate-arguments (global _ as Ty) (eqb.stop Ty1) D :- term->trm Ty Ty1 D, !.
+translate-arguments (app [global _|_] as Ty) (eqb.stop Ty1) D :- term->trm Ty Ty1 D, !.
 translate-arguments (app [N|_] as Ty) (eqb.stop Ty1) D :- name N, term->trm Ty Ty1 D, !.
 translate-arguments T _ (error S) :- S is "unsupported argument " ^ {coq.term->string T}.
 
@@ -135,6 +169,17 @@ validate-arguments (eqb.dependent T Args) D :- std.do-ok! D [
   (d\ pi x\ validate-arguments (Args x) d),
 ].
 
+func eqtype-clause inductive, eqb.eqType -> prop.
+eqtype-clause I EQT (eqType (indt I) EQT).
+
+func main-mutual list inductive -> list prop.
+main-mutual IS CL :- std.do! [
+  std.map IS (i\eqt\ std.assert-ok! (translate-indt i eqt) "derive.eqType.ast: translate") EQTS,
+  std.map2 IS EQTS eqtype-clause CL,
+  CL =!=> std.forall EQTS (eqt\ std.assert-ok! (validate-eqType eqt) "derive.eqType.ast: validate"),
+  std.forall CL (c\ coq.elpi.accumulate _ "derive.eqType.db" (clause _ _ c))
+].
+
 func main inductive -> list prop.
 main I [C] :-
   std.assert-ok! (translate-indt I EQT) "derive.eqType.ast: translate",