219 lines
8.9 KiB
Text
219 lines
8.9 KiB
Text
/-
|
||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
||
Authors: Wojciech Nawrocki
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Lean.Meta.PPGoal
|
||
public import Lean.Widget.InteractiveCode
|
||
public import Lean.Data.Lsp.Extra
|
||
|
||
public section
|
||
|
||
/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
|
||
|
||
namespace Lean.Widget
|
||
open Server
|
||
|
||
/-- 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.
|
||
Note that these are not `Name`s: they are pretty-printed
|
||
and do not remember the macro scopes. -/
|
||
names : Array String
|
||
/-- 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
|
||
/-- 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
|
||
|
||
/-- The shared parts of interactive term-mode and tactic-mode goals. -/
|
||
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. -/
|
||
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
|
||
deriving RpcEncodable
|
||
|
||
/-- An interactive term-mode goal. -/
|
||
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
|
||
|
||
def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
|
||
(goalPrefix : String) : Format := Id.run do
|
||
let indent := 2 -- Use option
|
||
let mut ret := match userName? with
|
||
| some userName => f!"case {userName}"
|
||
| none => Format.nil
|
||
for hyp in g.hyps do
|
||
ret := addLine ret
|
||
let names := hyp.names
|
||
|>.toList
|
||
|>.filter (· != toString Name.anonymous)
|
||
|> " ".intercalate
|
||
match names with
|
||
| "" =>
|
||
ret := ret ++ Format.group f!":{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
|
||
| _ =>
|
||
match hyp.val? with
|
||
| some val =>
|
||
ret := ret ++ Format.group f!"{names} : {hyp.type.stripTags} :={Format.nest indent (Format.line ++ val.stripTags)}"
|
||
| none =>
|
||
ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
|
||
ret := addLine ret
|
||
ret ++ f!"{goalPrefix}{Format.nest indent g.type.stripTags}"
|
||
where
|
||
addLine (fmt : Format) : Format :=
|
||
if fmt.isNil then fmt else fmt ++ Format.line
|
||
|
||
def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
|
||
g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
|
||
|
||
def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
|
||
g.toInteractiveGoalCore.pretty none "⊢ "
|
||
|
||
structure InteractiveGoals where
|
||
goals : Array InteractiveGoal
|
||
deriving RpcEncodable
|
||
|
||
def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
|
||
goals := l.goals ++ r.goals
|
||
|
||
instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
|
||
instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
|
||
|
||
open Meta in
|
||
/-- Extend an array of hypothesis bundles with another bundle. -/
|
||
def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
|
||
(ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) (tactic := false ) :
|
||
MetaM (Array InteractiveHypothesisBundle) := do
|
||
if ids.size == 0 then
|
||
throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
|
||
let fvarIds := ids.map Prod.snd
|
||
let names := ids.map Prod.fst
|
||
return hyps.push {
|
||
names
|
||
fvarIds
|
||
type := (← ppExprTagged type)
|
||
val? := (← value?.mapM ppLetValueExprTagged)
|
||
isInstance? := if (← isClass? type).isSome then true else none
|
||
isType? := if (← instantiateMVars type).isSort then true else none
|
||
}
|
||
where
|
||
ppLetValueExprTagged (value : Expr) : MetaM CodeWithInfos := do
|
||
if ← ppGoal.shouldShowLetValue tactic value then
|
||
ppExprTagged value
|
||
else
|
||
ppExprTagged value do PrettyPrinter.Delaborator.omission <| .string <|
|
||
if tactic then
|
||
"Value omitted since `pp.showLetValues` is false and \
|
||
the expression's depth exceeds both `pp.showLetValues.tactic.threshold` and `pp.showLetValues.threshold`."
|
||
else
|
||
"Value omitted since `pp.showLetValues` is false and \
|
||
the expression's depth exceeds `pp.showLetValues.threshold`."
|
||
|
||
open Meta in
|
||
variable [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] in
|
||
def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α) : n α := do
|
||
let mctx ← getMCtx
|
||
let some mvarDecl := mctx.findDecl? goal
|
||
| throwError "unknown goal {goal.name}"
|
||
let lctx := mvarDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)}
|
||
withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
|
||
|
||
open Meta in
|
||
/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
|
||
def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
|
||
let ppAuxDecls := pp.auxDecls.get (← getOptions)
|
||
let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
|
||
withGoalCtx mvarId fun lctx mvarDecl => do
|
||
-- See comment in `Lean.Meta.ppGoal` about this synthetic opaque heuristic.
|
||
let tactic := mvarDecl.kind.isSyntheticOpaque
|
||
let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
|
||
: MetaM (Array InteractiveHypothesisBundle) :=
|
||
if ids.isEmpty then
|
||
pure hyps
|
||
else
|
||
match type? with
|
||
| none => pure hyps
|
||
| some type => addInteractiveHypothesisBundle hyps ids type
|
||
let mut varNames : Array (String × FVarId) := #[]
|
||
let mut prevType? : Option Expr := none
|
||
let mut hyps : Array InteractiveHypothesisBundle := #[]
|
||
for localDecl in lctx do
|
||
if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then
|
||
continue
|
||
else
|
||
match localDecl with
|
||
| LocalDecl.cdecl _index fvarId varName type ..
|
||
| LocalDecl.ldecl _index fvarId varName type (nondep := true) .. =>
|
||
-- 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)
|
||
else
|
||
hyps ← pushPending varNames prevType? hyps
|
||
varNames := #[(varName, fvarId)]
|
||
prevType? := some type
|
||
| LocalDecl.ldecl _index fvarId varName type val (nondep := false) .. => do
|
||
let varName := toString varName
|
||
hyps ← pushPending varNames prevType? hyps
|
||
let type ← instantiateMVars type
|
||
let val ← instantiateMVars val
|
||
hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val tactic
|
||
varNames := #[]
|
||
prevType? := none
|
||
hyps ← pushPending varNames prevType? hyps
|
||
let goalTp ← instantiateMVars mvarDecl.type
|
||
let goalFmt ← ppExprTagged goalTp
|
||
let userName? := match mvarDecl.userName with
|
||
| Name.anonymous => none
|
||
| name => some <| toString name.eraseMacroScopes
|
||
return {
|
||
hyps
|
||
type := goalFmt
|
||
ctx := ← WithRpcRef.mk {← Elab.CommandContextInfo.save with }
|
||
userName?
|
||
goalPrefix := getGoalPrefix mvarDecl
|
||
mvarId
|
||
}
|
||
|
||
end Lean.Widget
|