From 8198fe542450a40dbea34fc202a7a4c96f31365f Mon Sep 17 00:00:00 2001 From: Leni Aniva 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, }) ] -- 2.44.1