feat: Print recursor rules

This commit is contained in:
Leni Aniva 2024-04-09 21:24:08 -07:00
parent c629163aa1
commit 8198fe5424
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
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), else pure (.none),
module? := module? module? := module?
} }
let result := match info with let result match info with
| .inductInfo induct => { core with inductInfo? := .some { | .inductInfo induct => pure { core with inductInfo? := .some {
numParams := induct.numParams, numParams := induct.numParams,
numIndices := induct.numIndices, numIndices := induct.numIndices,
all := induct.all.toArray.map (·.toString), all := induct.all.toArray.map (·.toString),
@ -79,21 +79,27 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
isReflexive := induct.isReflexive, isReflexive := induct.isReflexive,
isNested := induct.isNested, isNested := induct.isNested,
} } } }
| .ctorInfo ctor => { core with constructorInfo? := .some { | .ctorInfo ctor => pure { core with constructorInfo? := .some {
induct := ctor.induct.toString, induct := ctor.induct.toString,
cidx := ctor.cidx, cidx := ctor.cidx,
numParams := ctor.numParams, numParams := ctor.numParams,
numFields := ctor.numFields, numFields := ctor.numFields,
} } } }
| .recInfo r => { core with recursorInfo? := .some { | .recInfo r => pure { core with recursorInfo? := .some {
all := r.all.toArray.map (·.toString), all := r.all.toArray.map (·.toString),
numParams := r.numParams, numParams := r.numParams,
numIndices := r.numIndices, numIndices := r.numIndices,
numMotives := r.numMotives, numMotives := r.numMotives,
numMinors := r.numMinors, 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, k := r.k,
} } } }
| _ => core | _ => pure core
return .ok result return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv

View File

@ -138,12 +138,20 @@ structure ConstructorInfo where
numParams: Nat numParams: Nat
numFields: Nat numFields: Nat
deriving Lean.ToJson deriving Lean.ToJson
/-- See `Lean/Declaration.lean` -/
structure RecursorRule where
ctor: String
nFields: Nat
rhs: Expression
deriving Lean.ToJson
structure RecursorInfo where structure RecursorInfo where
all: Array String all: Array String
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
numMotives: Nat numMotives: Nat
numMinors: Nat numMinors: Nat
rules: Array RecursorRule
k: Bool k: Bool
deriving Lean.ToJson deriving Lean.ToJson
structure EnvInspectResult where structure EnvInspectResult where

View File

@ -11,6 +11,7 @@ open Pantograph
deriving instance DecidableEq, Repr for Protocol.InductInfo deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo 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.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
@ -69,6 +70,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 1, numIndices := 1,
numMotives := 1, numMotives := 1,
numMinors := 1, numMinors := 1,
rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
k := true, k := true,
}), }),
("ForM.rec", ConstantCat.recursor { ("ForM.rec", ConstantCat.recursor {
@ -77,6 +79,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 0, numIndices := 0,
numMotives := 1, numMotives := 1,
numMinors := 1, numMinors := 1,
rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
k := false, k := false,
}) })
] ]