From ffbea41f627741e70e2b1d01ac8663b9acd12777 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 25 Jun 2024 15:13:58 -0400
Subject: [PATCH] feat: Condensed interface

---
 Pantograph/Condensed.lean | 42 ++++++++++++++++++++++++++++++
 Pantograph/Serial.lean    | 54 ++++++++++++++++++++++++++++++++++++---
 Test/Common.lean          | 11 ++++++++
 3 files changed, 104 insertions(+), 3 deletions(-)
 create mode 100644 Pantograph/Condensed.lean

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
new file mode 100644
index 0000000..57a8517
--- /dev/null
+++ b/Pantograph/Condensed.lean
@@ -0,0 +1,42 @@
+/- structures for FFI based interface -/
+import Lean
+
+open Lean
+
+namespace Pantograph.Condensed
+
+/-
+These two functions are for user defiend names. For internal names such as
+`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
+construct hash maps for Lean names.
+-/
+@[export pantograph_str_to_name]
+def strToName (s: String) : Name := s.toName
+@[export pantograph_name_to_str]
+def nameToStr (s: String) : Name := s.toName
+@[export pantograph_name_is_inaccessible]
+def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
+
+-- Mirrors Lean's LocalDecl
+structure LocalDecl where
+  -- Default value is for testing
+  fvarId: FVarId := { name := .anonymous }
+  userName: Name
+
+  -- Normalized expression
+  type : Expr
+  value? : Option Expr := .none
+
+structure Goal where
+  mvarId: MVarId := { name := .anonymous }
+  userName: Name := .anonymous
+  context: Array LocalDecl
+  target: Expr
+
+@[export pantograph_goal_is_lhs]
+def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
+
+
+
+
+end Pantograph.Condensed
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index e729bee..2cdf3d6 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -4,10 +4,10 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
 using `Scope`s.
 -/
 import Lean
+import Pantograph.Condensed
 import Pantograph.Expr
-
-import Pantograph.Protocol
 import Pantograph.Goal
+import Pantograph.Protocol
 
 open Lean
 
@@ -201,6 +201,55 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
+@[export pantograph_to_condensed_goal]
+def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
+  let options: Protocol.Options := {}
+  let ppAuxDecls       := options.printAuxDecls
+  let ppImplDetailHyps := options.printImplementationDetailHyps
+  let mvarDecl ← mvarId.getDecl
+  let lctx     := mvarDecl.lctx
+  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
+      match localDecl with
+      | .cdecl _ fvarId userName type _ _ =>
+        let type ← instantiate type
+        return { fvarId, userName, type }
+      | .ldecl _ fvarId userName type value _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        let value ← instantiate value
+        return { fvarId, userName, type, value? := .some value }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        let var ← ppVar localDecl
+        return var::acc
+    return {
+        mvarId,
+        userName := mvarDecl.userName,
+        context := vars.reverse.toArray,
+        target := ← instantiate mvarDecl.type
+    }
+  where
+  instantiate := instantiateAll
+
+@[export pantograph_goal_state_to_condensed]
+protected def GoalState.toCondensed (state: GoalState):
+    CoreM (Array Condensed.Goal):= do
+  let metaM := do
+    let goals := state.goals.toArray
+    goals.mapM fun goal => do
+      match state.mctx.findDecl? goal with
+      | .some _ =>
+        let serializedGoal ← toCondensedGoal goal
+        pure serializedGoal
+      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
+  metaM.run' (s := state.savedState.term.meta.meta)
+
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
@@ -214,7 +263,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
     let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
       match localDecl with
       | .cdecl _ fvarId userName _ _ _ =>
-        let userName := userName.simpMacroScopes
         return {
           name := ofName fvarId.name,
           userName:= ofName userName.simpMacroScopes,
diff --git a/Test/Common.lean b/Test/Common.lean
index c656309..e4e1d4c 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -8,6 +8,17 @@ open Lean
 
 namespace Pantograph
 
+deriving instance Repr for Expr
+-- Use strict equality check for expressions
+--instance : BEq Expr := ⟨Expr.equal⟩
+instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
+  if h : Expr.equal x y then
+    .isTrue h
+  else
+    .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
+
+def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
+
 -- Auxiliary functions
 namespace Protocol
 def Goal.devolatilizeVars (goal: Goal): Goal :=