feat: Print recursor rules

This commit is contained in:
Leni Aniva 2024-04-09 21:24:08 -07:00 committed by Leni Aniva
parent 823c9635c7
commit a11df9f2e9
3 changed files with 22 additions and 5 deletions

View File

@ -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

View File

@ -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

View File

@ -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,
})
]