fix: Use Arrays only in the ABI

This commit is contained in:
Leni Aniva 2024-03-14 22:40:14 -07:00
parent 3debcc021a
commit e6dbf88ce2
3 changed files with 11 additions and 10 deletions

View File

@ -66,8 +66,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
| .inductInfo induct => { core with inductInfo? := .some { | .inductInfo induct => { core with inductInfo? := .some {
numParams := induct.numParams, numParams := induct.numParams,
numIndices := induct.numIndices, numIndices := induct.numIndices,
all := induct.all.map (·.toString), all := induct.all.toArray.map (·.toString),
ctors := induct.ctors.map (·.toString), ctors := induct.ctors.toArray.map (·.toString),
isRec := induct.isRec, isRec := induct.isRec,
isReflexive := induct.isReflexive, isReflexive := induct.isReflexive,
isNested := induct.isNested, isNested := induct.isNested,
@ -79,7 +79,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
numFields := ctor.numFields, numFields := ctor.numFields,
} } } }
| .recInfo r => { core with recursorInfo? := .some { | .recInfo r => { core with recursorInfo? := .some {
all := r.all.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,

View File

@ -124,8 +124,8 @@ structure EnvInspect where
structure InductInfo where structure InductInfo where
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
all: List String all: Array String
ctors: List String ctors: Array String
isRec: Bool := false isRec: Bool := false
isReflexive: Bool := false isReflexive: Bool := false
isNested: Bool := false isNested: Bool := false
@ -138,7 +138,7 @@ structure ConstructorInfo where
numFields: Nat numFields: Nat
deriving Lean.ToJson deriving Lean.ToJson
structure RecursorInfo where structure RecursorInfo where
all: List String all: Array String
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
numMotives: Nat numMotives: Nat
@ -230,6 +230,7 @@ structure GoalContinueResult where
-- Remove goal states -- Remove goal states
structure GoalDelete where structure GoalDelete where
-- This is ok being a List because it doesn't show up in the ABI
stateIds: List Nat stateIds: List Nat
deriving Lean.FromJson deriving Lean.FromJson
structure GoalDeleteResult where structure GoalDeleteResult where

View File

@ -34,8 +34,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
("Or", ConstantCat.induct { ("Or", ConstantCat.induct {
numParams := 2, numParams := 2,
numIndices := 0, numIndices := 0,
all := ["Or"], all := #["Or"],
ctors := ["Or.inl", "Or.inr"], ctors := #["Or.inl", "Or.inr"],
}), }),
("Except.ok", ConstantCat.ctor { ("Except.ok", ConstantCat.ctor {
induct := "Except", induct := "Except",
@ -44,7 +44,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
numFields := 1, numFields := 1,
}), }),
("Eq.rec", ConstantCat.recursor { ("Eq.rec", ConstantCat.recursor {
all := ["Eq"], all := #["Eq"],
numParams := 2, numParams := 2,
numIndices := 1, numIndices := 1,
numMotives := 1, numMotives := 1,
@ -52,7 +52,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
k := true, k := true,
}), }),
("ForM.rec", ConstantCat.recursor { ("ForM.rec", ConstantCat.recursor {
all := ["ForM"], all := #["ForM"],
numParams := 3, numParams := 3,
numIndices := 0, numIndices := 0,
numMotives := 1, numMotives := 1,