From 8198fe542450a40dbea34fc202a7a4c96f31365f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 9 Apr 2024 21:24:08 -0700
Subject: [PATCH] feat: Print recursor rules

---
 Pantograph/Environment.lean | 16 +++++++++++-----
 Pantograph/Protocol.lean    |  8 ++++++++
 Test/Environment.lean       |  3 +++
 3 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 5e19bdf..0385cad 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -69,8 +69,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       else pure (.none),
     module? := module?
   }
-  let result := match info with
-    | .inductInfo induct => { core with inductInfo? := .some {
+  let result ← match info with
+    | .inductInfo induct => pure { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
           all := induct.all.toArray.map (·.toString),
@@ -79,21 +79,27 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
       } }
-    | .ctorInfo ctor => { core with constructorInfo? := .some {
+    | .ctorInfo ctor => pure { core with constructorInfo? := .some {
           induct := ctor.induct.toString,
           cidx := ctor.cidx,
           numParams := ctor.numParams,
           numFields := ctor.numFields,
       } }
-    | .recInfo r => { core with recursorInfo? := .some {
+    | .recInfo r => pure { core with recursorInfo? := .some {
           all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
           numMinors := r.numMinors,
+          rules := ← r.rules.toArray.mapM (λ rule => do
+              pure {
+                ctor := rule.ctor.toString,
+                nFields := rule.nfields,
+                rhs := ← (serialize_expression options rule.rhs).run',
+              })
           k := r.k,
       } }
-    | _ => core
+    | _ => pure core
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 6ee3354..0f27e48 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -138,12 +138,20 @@ structure ConstructorInfo where
   numParams: Nat
   numFields: Nat
   deriving Lean.ToJson
+
+/-- See `Lean/Declaration.lean` -/
+structure RecursorRule where
+  ctor: String
+  nFields: Nat
+  rhs: Expression
+  deriving Lean.ToJson
 structure RecursorInfo where
   all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
   numMinors: Nat
+  rules: Array RecursorRule
   k: Bool
   deriving Lean.ToJson
 structure EnvInspectResult where
diff --git a/Test/Environment.lean b/Test/Environment.lean
index 927793d..631ea54 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -11,6 +11,7 @@ open Pantograph
 
 deriving instance DecidableEq, Repr for Protocol.InductInfo
 deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
+deriving instance DecidableEq, Repr for Protocol.RecursorRule
 deriving instance DecidableEq, Repr for Protocol.RecursorInfo
 deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
 
@@ -69,6 +70,7 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 1,
       numMotives := 1,
       numMinors := 1,
+      rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
@@ -77,6 +79,7 @@ def test_inspect: IO LSpec.TestSeq := do
       numIndices := 0,
       numMotives := 1,
       numMinors := 1,
+      rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
       k := false,
     })
   ]