From 72ffab5b46a480bd25f4ec00e5031283fdd330c4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 1 Feb 2024 14:05:24 +0100 Subject: [PATCH] cleanup InteractiveGoal --- server/GameServer/InteractiveGoal.lean | 112 +++++++++++++------------ 1 file changed, 58 insertions(+), 54 deletions(-) diff --git a/server/GameServer/InteractiveGoal.lean b/server/GameServer/InteractiveGoal.lean index 30e7213..ca75ba5 100644 --- a/server/GameServer/InteractiveGoal.lean +++ b/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 }