From 0d703faa14a2a8fefd9cd1554fbc2afc456301be Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 21 Jan 2025 10:43:37 +0100
Subject: [PATCH] Fix #748 (coq.typecheck-indt-decl failing)

https://github.com/LPCIC/coq-elpi/issues/748
---
 Changelog.md      |  9 +++++++++
 elpi/coq-lib.elpi | 15 ++++++++++-----
 tests/bug_748.v   | 16 ++++++++++++++++
 3 files changed, 35 insertions(+), 5 deletions(-)
 create mode 100644 tests/bug_748.v

diff --git a/Changelog.md b/Changelog.md
index 5e7b867f6..e0af52942 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,12 @@
+# 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
+- `coq.arity->sort` now handles let-in
+
 # [2.4.0] 15/1/2025
 
 Requires Elpi 2.0.7 and Coq 8.20.
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
index f7222e22b..abe409132 100644
--- a/elpi/coq-lib.elpi
+++ b/elpi/coq-lib.elpi
@@ -48,10 +48,13 @@ coq.prod->fun (let N T B F) (let N T B R) :- !, pi x\ coq.prod->fun (F x) (R x).
 coq.prod->fun X X.
 
 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 (prod N T B) C :- !,
+  (@pi-decl N T x\ coq.count-prods (B x) C'), C is C' + 1.
+coq.count-prods (let N T V B) C :- !,
+  (@pi-def N T V x\ coq.count-prods (B x) C).
+coq.count-prods T C :- !,
+  coq.reduction.lazy.whd T Tr,
+  if (T == Tr) (C = 0) (coq.count-prods Tr C).
 
 pred coq.mk-n-holes  i:int, o:list A.
 coq.mk-n-holes  0 [] :- !.
@@ -454,8 +457,10 @@ coq.term->arity (prod Name S T) N (parameter ID explicit S R) :-
 % extracts the sort at the end of an arity
 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 (let N T V X) Y :- !, @pi-def N T V x\ coq.arity->sort (X x) Y.
 coq.arity->sort (sort X) X :- !.
-:name "arity->sort:fail"
+coq.arity->sort X Y :- coq.reduction.lazy.whd X Xr, not (X == Xr), !,
+  coq.arity->sort Xr Y.
 coq.arity->sort T _ :- fatal-error-w-data "arity->sort: not a sort or prod" T.
 
 % Counts how many parameters are there
diff --git a/tests/bug_748.v b/tests/bug_748.v
new file mode 100644
index 000000000..e96d7be0a
--- /dev/null
+++ b/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.