cleanup InteractiveGoal

server/GameServer/InteractiveGoal.lean

@@ -1,74 +1,62 @@
-/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
-
 import Lean.Widget.InteractiveGoal
 
-/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
+/-!
+This file is a modified copy of `Lean.Widget.InteractiveGoal`.
+
+We add the structure `GameHint` and extend two existing structures:
+
+* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
+* `hint` in `InteractiveGoal`: stores the game hints associated with the goal.
+
+The rest of this file is simply copied to use these new modified stuctures.
+-/
 
 namespace GameServer
+
 open Lean Lean.Widget Lean.Server
 
+/-- A hint in the game at the corresponding goal. -/
 structure GameHint where
   text : String
   hidden : Bool
 deriving FromJson, ToJson
 
-/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
-as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
-booleans to save space in the json encoding. -/
-structure InteractiveHypothesisBundle where
-  /-- The user-friendly name for each hypothesis. -/
-  names : Array Name
-  /-- The ids for each variable. Should have the same length as `names`. -/
-  fvarIds : Array FVarId
-  type : CodeWithInfos
-  /-- The value, in the case the hypothesis is a `let`-binder. -/
-  val? : Option CodeWithInfos := none
-  /-- The hypothesis is a typeclass instance. -/
-  isInstance? : Option Bool := none
-  /-- The hypothesis is a type. -/
-  isType? : Option Bool := none
+/-- Extend the interactive hypothesis bundle with an option to distinguish
+"assumptions" from "objects". "Assumptions" ate hyptheses of type `Prop`. -/
+-- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
+structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
   /-- The hypothesis's type is of type `Prop` -/
   isAssumption? : Option Bool := none
-  /-- If true, the hypothesis was not present on the previous tactic state.
-  Only present in tactic-mode goals. -/
-  isInserted? : Option Bool := none
-  /-- If true, the hypothesis will be removed in the next tactic state.
-  Only present in tactic-mode goals. -/
-  isRemoved? : Option Bool := none
-  deriving Inhabited, RpcEncodable
+deriving RpcEncodable
 
-/-- The shared parts of interactive term-mode and tactic-mode goals. -/
+-- duplicated but with custom `InteractiveHypothesisBundle`
+@[inherit_doc Lean.Widget.InteractiveGoalCore]
 structure InteractiveGoalCore where
   hyps : Array InteractiveHypothesisBundle
-  /-- The target type. -/
   type : CodeWithInfos
-  /-- Metavariable context that the goal is well-typed in. -/
   ctx : WithRpcRef Elab.ContextInfo
 
-/-- An interactive tactic-mode goal. -/
+-- duplicated but with custom `InteractiveGoalCore` and extended by `hints`
+@[inherit_doc Lean.Widget.InteractiveGoal]
 structure InteractiveGoal extends InteractiveGoalCore where
-  /-- The name `foo` in `case foo`, if any. -/
   userName? : Option String
-  /-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
-  and it could be extended. -/
   goalPrefix : String
-  /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
   mvarId : MVarId
-  /-- If true, the goal was not present on the previous tactic state. -/
   isInserted? : Option Bool := none
-  /-- If true, the goal will be removed on the next tactic state. -/
   isRemoved? : Option Bool := none
+  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
   hints : Array GameHint := #[]
-  deriving RpcEncodable
+deriving RpcEncodable
 
-/-- An interactive term-mode goal. -/
+-- duplicated with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveTermGoal]
 structure InteractiveTermGoal extends InteractiveGoalCore where
-  /-- Syntactic range of the term. -/
   range : Lsp.Range
-  /-- Information about the term whose type is the term-mode goal. -/
   term : WithRpcRef Elab.TermInfo
-  deriving RpcEncodable
+deriving RpcEncodable
 
+-- duplicated with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
     (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
@@ -79,8 +67,7 @@ def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option Str
     ret := addLine ret
     let names := hyp.names
         |>.toList
-        |>.filter (not ∘ Name.isAnonymous)
-        |>.map toString
+        |>.filter (· != toString Name.anonymous)
         |> " ".intercalate
     match names with
     | "" =>
@@ -97,16 +84,24 @@ where
   addLine (fmt : Format) : Format :=
     if fmt.isNil then fmt else fmt ++ Format.line
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoal.pretty]
 def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
   g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
 
+-- duplicated with custom `InteractiveTermGoal`
+-- @[inherit_doc Lean.Widget.InteractiveTermGoal.pretty]
 def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
   g.toInteractiveGoalCore.pretty none "⊢ "
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoals]
 structure InteractiveGoals where
   goals : Array InteractiveGoal
   deriving RpcEncodable
 
+-- duplicated with custom `InteractiveGoals`
+-- @[inherit_doc Lean.Widget.InteractiveGoals.append]
 def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
   goals := l.goals ++ r.goals
 
@@ -114,9 +109,10 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
 instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 
 open Meta in
-/-- Extend an array of hypothesis bundles with another bundle. -/
+-- duplicated with custom `InteractiveHypothesisBundle` and therefore added `isAssumption?`
+@[inherit_doc Lean.Widget.addInteractiveHypothesisBundle]
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
-    (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) :
     MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
     throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
@@ -125,11 +121,12 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
   return hyps.push {
     names
     fvarIds
-    type           := (← ppExprTagged type)
-    val?           := (← value?.mapM ppExprTagged)
-    isInstance?    := if (← isClass? type).isSome then true else none
-    isType?        := if (← instantiateMVars type).isSort then true else none
-    isAssumption?  := if (← inferType type).isProp then true else none
+    type        := (← ppExprTagged type)
+    val?        := (← value?.mapM ppExprTagged)
+    isInstance? := if (← isClass? type).isSome then true else none
+    isType?     := if (← instantiateMVars type).isSort then true else none
+    -- Added:
+    isAssumption? := if (← inferType type).isProp then true else none
   }
 
 open Meta in
@@ -142,13 +139,16 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
   withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
 
 open Meta in
-/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
+
+-- Copied from `Lean.Widget.goalToInteractive` but added
+-- argument `hint` which is simply passed along.
+@[inherit_doc Lean.Widget.goalToInteractive]
 def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
   withGoalCtx mvarId fun lctx mvarDecl => do
-    let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
+    let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
       if ids.isEmpty then
         pure hyps
@@ -156,7 +156,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
         match type? with
         | none      => pure hyps
         | some type => addInteractiveHypothesisBundle hyps ids type
-    let mut varNames : Array (Name × FVarId) := #[]
+    let mut varNames : Array (String × FVarId) := #[]
     let mut prevType? : Option Expr := none
     let mut hyps : Array InteractiveHypothesisBundle := #[]
     for localDecl in lctx do
@@ -165,7 +165,10 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       else
         match localDecl with
         | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          let varName := varName.simpMacroScopes
+          -- We rely on the fact that `withGoalCtx` runs `LocalContext.sanitizeNames`,
+          -- so the `userName`s of local hypotheses are already pretty-printed
+          -- and it suffices to simply `toString` them.
+          let varName := toString varName
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
             varNames := varNames.push (varName, fvarId)
@@ -174,7 +177,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
             varNames := #[(varName, fvarId)]
           prevType? := some type
         | LocalDecl.ldecl _index fvarId varName type val _ _ => do
-          let varName := varName.simpMacroScopes
+          let varName := toString varName
           hyps ← pushPending varNames prevType? hyps
           let type ← instantiateMVars type
           let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
@@ -194,6 +197,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId
+      -- Added:
       hints
     }