Fix #748 (coq.typecheck-indt-decl failing)

#748

Changelog.md

@@ -1,3 +1,11 @@
+# Development version
+
+### API
+- `coq.count-prods` now count products modulo reduction,
+  rather than purely syntactically
+- `coq.arity->sort` now attempts reduction to find a sort or prod,
+  before failing
+
 # [2.4.0] 15/1/2025
 
 Requires Elpi 2.0.7 and Coq 8.20.

apps/derive/elpi/projK.elpi

@@ -129,9 +129,14 @@ allK-projs Prefix J JN Paramsno Arity IT K KTy Clauses :- do! [
   allK-projs Prefix J1 JN Paramsno Arity IT K KTy ClausesRest
 ].
 
+pred count-prods-nored i:term, o:int.
+count-prods-nored (prod _ _ B) N :- !, (pi x\ count-prods-nored (B x) M), N is M + 1.
+count-prods-nored (let _ _ _ B) N :- !, (pi x\ count-prods-nored (B x) N).
+count-prods-nored _ 0.
+
 pred for-K i:string, i:int, i:term, i:term,  i:constructor, i:term, o:list prop.
 for-K Prefix Paramsno Arity IT K KT Clauses :- do! [
-  coq.count-prods KT N,
+  count-prods-nored KT N,
   Argsno is N - Paramsno,
   allK-projs Prefix 0 Argsno Paramsno Arity IT K KT Clauses
 ].

elpi/coq-lib.elpi

@@ -51,7 +51,9 @@ pred coq.count-prods i:term, o:int.
 coq.count-prods (prod _ _ B) N :- !, (pi x\ coq.count-prods (B x) M), N is M + 1.
 coq.count-prods (let _ _ _ B) N :- !, (pi x\ coq.count-prods (B x) N).
 :name "count-prod:end"
-coq.count-prods _ 0 :- !.
+coq.count-prods T N :- !,
+  coq.reduction.lazy.whd T Tr,
+  if (T = Tr) (N is 0) (coq.count-prods Tr N).
 
 pred coq.mk-n-holes  i:int, o:list A.
 coq.mk-n-holes  0 [] :- !.
@@ -455,6 +457,8 @@ coq.term->arity (prod Name S T) N (parameter ID explicit S R) :-
 pred coq.arity->sort i:term, o:sort.
 coq.arity->sort (prod N S X) Y :- !, @pi-decl N S x\ coq.arity->sort (X x) Y.
 coq.arity->sort (sort X) X :- !.
+coq.arity->sort X Y :- coq.reduction.lazy.whd X Xr, not (X = Xr), !,
+  coq.arity->sort Xr Y.
 :name "arity->sort:fail"
 coq.arity->sort T _ :- fatal-error-w-data "arity->sort: not a sort or prod" T.
 

tests/bug_748.v

@@ -0,0 +1,16 @@
+From elpi Require Import elpi.
+
+Definition myType := Type.
+Variant indd : myType := Indd : indd.
+
+Definition myType_R u v := u -> v -> Type.
+
+Elpi Command foo.
+Elpi Accumulate "
+main _ :-
+  std.assert-ok! (coq.typecheck-indt-decl (inductive ""indt_R"" tt
+    (arity {{ myType_R indd indd }})
+    c1 \
+      [ constructor ""Indd_R"" (arity {{ lp:c1 Indd Indd }}) ])) ""error"".
+".
+Elpi foo.