Pantograph/Goal.lean

@@ -143,7 +143,12 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep
     }
 
 protected def GoalState.rootExpr (goalState: GoalState): Option Expr :=
-  goalState.mctx.eAssignment.find? goalState.root |>.filter (λ e => ¬ e.hasMVar)
+  let expr := goalState.mctx.eAssignment.find! goalState.root
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasMVar then
+    .none
+  else
+    .some expr
 
 -- Diagnostics functions
 
@@ -183,7 +188,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do
       if options.printContext then
         decl.lctx.fvarIdToDecl.forM printFVar
-      let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
+      let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
       IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
       if options.printValue then
         if let Option.some value := (← getMCtx).eAssignment.find? mvarId then

Pantograph/Protocol.lean

@@ -43,7 +43,10 @@ structure Expression where
   deriving Lean.ToJson
 
 structure Variable where
-  name: String
+  /-- The internal name used in raw expressions -/
+  name: String := ""
+  /-- The name displayed to the user -/
+  userName: String
   /-- Does the name contain a dagger -/
   isInaccessible?: Option Bool := .none
   type?: Option Expression  := .none

Pantograph/Serial.lean

@@ -102,8 +102,8 @@ def serialize_sort_level_ast (level: Level): String :=
 /--
  Completely serializes an expression tree. Json not used due to compactness
 -/
-def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
+def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
-  return self expr
+  self expr
   where
   self (e: Expr): String :=
     match e with
@@ -175,7 +175,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
   let pp?: Option String := match options.printExprPretty with
       | true => .some pp
       | false => .none
-  let sexp: String := (← serialize_expression_ast e)
+  let sexp: String := serialize_expression_ast e
   let sexp?: Option String := match options.printExprAST with
       | true => .some sexp
       | false => .none
@@ -196,27 +196,30 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
   Meta.withLCtx lctx mvarDecl.localInstances do
     let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
       match localDecl with
-      | .cdecl _ _ varName _ _ _ =>
+      | .cdecl _ fvarId userName _ _ _ =>
-        let varName := varName.simpMacroScopes
+        let userName := userName.simpMacroScopes
         return {
-          name := toString varName,
+          name := of_name fvarId.name,
+          userName:= of_name userName.simpMacroScopes,
         }
-      | .ldecl _ _ varName _ _ _ _ => do
+      | .ldecl _ fvarId userName _ _ _ _ => do
         return {
-          name := toString varName,
+          name := of_name fvarId.name,
+          userName := toString userName.simpMacroScopes,
         }
     let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
       match localDecl with
-      | .cdecl _ _ varName type _ _ =>
+      | .cdecl _ fvarId userName type _ _ =>
-        let varName := varName.simpMacroScopes
+        let userName := userName.simpMacroScopes
         let type ← instantiateMVars type
         return {
-          name := toString varName,
+          name := of_name fvarId.name,
-          isInaccessible? := .some varName.isInaccessibleUserName
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serialize_expression options type)
         }
-      | .ldecl _ _ varName type val _ _ => do
+      | .ldecl _ fvarId userName type val _ _ => do
-        let varName := varName.simpMacroScopes
+        let userName := userName.simpMacroScopes
         let type ← instantiateMVars type
         let value? ← if showLetValues then
           let val ← instantiateMVars val
@@ -224,8 +227,9 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
         else
           pure $ .none
         return {
-          name := toString varName,
+          name := of_name fvarId.name,
-          isInaccessible? := .some varName.isInaccessibleUserName
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serialize_expression options type)
           value? := value?
         }
@@ -242,13 +246,13 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
           | false => ppVar localDecl
         return var::acc
     return {
-      caseName? := match mvarDecl.userName with
+      caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
-        | Name.anonymous => .none
-        | name => .some <| toString name,
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
+  where
+  of_name (n: Name) := name_to_ast n (sanitize := false)
 
 
 

Test/Common.lean

@@ -0,0 +1,19 @@
+import Pantograph.Protocol
+
+namespace Pantograph
+
+namespace Protocol
+/-- Set internal names to "" -/
+def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal with
+    vars := goal.vars.map removeInternalAux,
+  }
+  where removeInternalAux (v: Variable): Variable :=
+    {
+      v with
+      name := ""
+    }
+end Protocol
+
+end Pantograph

Test/Proofs.lean

@@ -4,6 +4,7 @@ Tests pertaining to goals with no interdependencies
 import LSpec
 import Pantograph.Goal
 import Pantograph.Serial
+import Test.Common
 
 namespace Pantograph
 
@@ -69,7 +70,7 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa
   {
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
-      name := x.fst,
+      userName := x.fst,
       type? := .some { pp? := .some x.snd },
       isInaccessible? := .some false
     })).toArray
@@ -79,7 +80,7 @@ def buildGoalSelective (nameType: List (String × Option String)) (target: Strin
   {
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
-      name := x.fst,
+      userName := x.fst,
       type? := x.snd.map (λ type => { pp? := type }),
       isInaccessible? := x.snd.map (λ _ => false)
     })).toArray
@@ -104,7 +105,6 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
   | .ok (_, a) =>
     return a
 
-
 -- Individual test cases
 example: ∀ (a b: Nat), a + b = b + a := by
   intro n m
@@ -125,7 +125,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n")
+  addTest $ LSpec.check "intro n m" (goal1.devolatilize = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n")
 
   match ← state1.execute (goalId := 0) (tactic := "assumption") with
   | .failure #[message] =>
@@ -170,14 +170,14 @@ def proof_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p")
+  addTest $ LSpec.check "p q h" (goal1.devolatilize = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p")
   let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
     | .success state #[goal1, goal2] => pure (state, goal1, goal2)
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p")
+  addTest $ LSpec.check "cases h/1" (goal1.devolatilize = branchGoal "inl" "p")
-  addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q")
+  addTest $ LSpec.check "cases h/2" (goal2.devolatilize = branchGoal "inr" "q")
 
   let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
     | .success state #[goal] => pure (state, goal)
@@ -200,6 +200,7 @@ def proof_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
 
+  addTest $ LSpec.check "4_2 root" state4_2.rootExpr.isNone
   -- Ensure the proof can continue from `state4_2`.
   let state2b ← match state2.continue state4_2 with
     | .error msg => do
@@ -217,8 +218,8 @@ def proof_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  IO.println "=====  4_1  ====="
+  state4_1.print
-  state4_1.print ({ printNonVisible := false })
+  addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome
 
   return ()
   where
@@ -227,9 +228,9 @@ def proof_or_comm: TestM Unit := do
       caseName? := .some caseName,
       target := { pp? := .some "q ∨ p" },
       vars := #[
-        { name := "p", type? := .some typeProp, isInaccessible? := .some false },
+        { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
-        { name := "q", type? := .some typeProp, isInaccessible? := .some false },
+        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
-        { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
+        { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
       ]
     }
 

Test/Serial.lean

@@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := str_to_name symbol |> env.find? |>.get! |>.type
-    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
+    let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
-    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   let coreM := metaM.run'
   let coreContext: Core.Context := {
     currNamespace := Lean.Name.str .anonymous "Aniva"