From 689112d973404ce6da01aae6bd476e0fb7892343 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 14 Mar 2024 22:40:14 -0700
Subject: [PATCH] fix: Use Arrays only in the ABI

---
 Pantograph/Environment.lean | 6 +++---
 Pantograph/Protocol.lean    | 7 ++++---
 Test/Environment.lean       | 8 ++++----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index f37225f..ecae517 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -66,8 +66,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | .inductInfo induct => { core with inductInfo? := .some {
           numParams := induct.numParams,
           numIndices := induct.numIndices,
-          all := induct.all.map (·.toString),
-          ctors := induct.ctors.map (·.toString),
+          all := induct.all.toArray.map (·.toString),
+          ctors := induct.ctors.toArray.map (·.toString),
           isRec := induct.isRec,
           isReflexive := induct.isReflexive,
           isNested := induct.isNested,
@@ -79,7 +79,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           numFields := ctor.numFields,
       } }
     | .recInfo r => { core with recursorInfo? := .some {
-          all := r.all.map (·.toString),
+          all := r.all.toArray.map (·.toString),
           numParams := r.numParams,
           numIndices := r.numIndices,
           numMotives := r.numMotives,
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 91c44a8..e9a5f87 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -124,8 +124,8 @@ structure EnvInspect where
 structure InductInfo where
   numParams: Nat
   numIndices: Nat
-  all: List String
-  ctors: List String
+  all: Array String
+  ctors: Array String
   isRec:       Bool := false
   isReflexive: Bool := false
   isNested:    Bool := false
@@ -138,7 +138,7 @@ structure ConstructorInfo where
   numFields: Nat
   deriving Lean.ToJson
 structure RecursorInfo where
-  all: List String
+  all: Array String
   numParams: Nat
   numIndices: Nat
   numMotives: Nat
@@ -230,6 +230,7 @@ structure GoalContinueResult where
 
 -- Remove goal states
 structure GoalDelete where
+  -- This is ok being a List because it doesn't show up in the ABI
   stateIds: List Nat
   deriving Lean.FromJson
 structure GoalDeleteResult where
diff --git a/Test/Environment.lean b/Test/Environment.lean
index df3f3ae..977ed7d 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -34,8 +34,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
     ("Or", ConstantCat.induct {
       numParams := 2,
       numIndices := 0,
-      all := ["Or"],
-      ctors := ["Or.inl", "Or.inr"],
+      all := #["Or"],
+      ctors := #["Or.inl", "Or.inr"],
     }),
     ("Except.ok", ConstantCat.ctor {
       induct := "Except",
@@ -44,7 +44,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       numFields := 1,
     }),
     ("Eq.rec", ConstantCat.recursor {
-      all := ["Eq"],
+      all := #["Eq"],
       numParams := 2,
       numIndices := 1,
       numMotives := 1,
@@ -52,7 +52,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
       k := true,
     }),
     ("ForM.rec", ConstantCat.recursor {
-      all := ["ForM"],
+      all := #["ForM"],
       numParams := 3,
       numIndices := 0,
       numMotives := 1,