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

Pantograph/Goal.lean

@@ -63,9 +63,16 @@ protected def GoalState.mctx (state: GoalState): MetavarContext :=
 protected def GoalState.env (state: GoalState): Environment :=
   state.savedState.term.meta.core.env
 
+@[export pantograph_goal_state_meta_context_of_goal]
+protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
+  let mvarDecl ← state.mctx.findDecl? mvarId
+  return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
+@[export pantograph_goal_state_meta_state]
+protected def GoalState.metaState (state: GoalState): Meta.State :=
+  state.savedState.term.meta.meta
+
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
-  let metaM := mvarId.withContext m
+  mvarId.withContext m |>.run' (← read) state.metaState
-  metaM.run' (← read) state.savedState.term.meta.meta
 
 protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
   state.withContext state.parentMVar?.get! m
@@ -82,6 +89,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
   state.savedState.restore
   Elab.Tactic.setGoals [goal]
 
+
 private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
   mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
     if let .some prevMVarDecl := mctxOld.decls.find? mvarId then

Pantograph/Library.lean

@@ -204,15 +204,16 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
-inductive TacticExecute where
+inductive SyntheticTactic where
   | congruenceArg
   | congruenceFun
   | congruence
-@[export pantograph_goal_tactic_execute_m]
+/-- Executes a synthetic tactic which has no arguments -/
-def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult :=
+@[export pantograph_goal_synthetic_tactic_m]
+def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
   runTermElabM do
     state.restoreElabM
-    state.execute goalId $ match tacticExecute with
+    state.execute goalId $ match case with
       | .congruenceArg => Tactic.congruenceArg
       | .congruenceFun => Tactic.congruenceFun
       | .congruence => Tactic.congruence

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 := .none)
       : 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,
@@ -311,7 +359,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
         let pref := if goalState.newMVars.contains mvarId then "~" else " "
         printMVar pref mvarId decl
       )
-  pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
   where
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
       let resultFVars: List String ←
@@ -337,7 +385,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
               else pure $ value
             pure s!"\n := {← Meta.ppExpr value}"
           else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
-            pure s!"\n := $ {mvarIdPending.name}"
+            pure s!"\n ::= {mvarIdPending.name}"
           else
             pure ""
         else

Test/Tactic/Congruence.lean

@@ -7,6 +7,34 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Congruence
 
+def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let (newGoals, test) ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.30"),
+            (`a₁, "?α"),
+            (`a₂, "?α"),
+            (`f, "?α → List α"),
+            (`h, "?a₁ = ?a₂"),
+            (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
+          ])
+        return (newGoals, test)
+      tests := tests ++ test
+      let f := newGoals.get! 3
+      let h := newGoals.get! 4
+      let c := newGoals.get! 5
+      let results ← f.apply (← parseSentence "List.reverse")
+      tests := tests ++ (LSpec.check "apply" (results.length = 0))
+      tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
+      tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
+      return tests
 def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   runMetaMSeq env do
@@ -72,6 +100,7 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
+    ("congrArg List.reverse", test_congr_arg_list env),
     ("congrArg", test_congr_arg env),
     ("congrFun", test_congr_fun env),
     ("congr", test_congr env),