From fd016c6065e74c4119df3282aff8e008a3caa7c8 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 16 Aug 2021 15:37:27 +0200 Subject: [PATCH] chore: address some comments --- src/Lean/Data/Json/Basic.lean | 4 +- src/Lean/Data/Lsp/Extra.lean | 5 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 10 ++-- .../Server/FileWorker/RequestHandling.lean | 2 +- src/Lean/Server/Snapshots.lean | 50 +++++++++---------- src/Lean/Widget/InteractiveDiagnostic.lean | 5 +- src/Lean/Widget/TaggedText.lean | 32 ++++++------ 7 files changed, 52 insertions(+), 56 deletions(-) diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 72ca4134d7..6d61cf1658 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -152,7 +152,9 @@ private partial def beq' : Json → Json → Bool a == b | obj a, obj b => let _ : BEq Json := ⟨beq'⟩ - a.all fun field fa => + let szA := a.fold (init := 0) (fun a _ _ => a + 1) + let szB := b.fold (init := 0) (fun a _ _ => a + 1) + szA == szB && a.all fun field fa => match b.find compare field with | none => false | some fb => fa == fb diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean index 9ce8426d48..59e395b74e 100644 --- a/src/Lean/Data/Lsp/Extra.lean +++ b/src/Lean/Data/Lsp/Extra.lean @@ -48,12 +48,15 @@ structure LeanFileProgressParams where /-- `$/lean/plainGoal` client->server request. -Returns the goal(s) at the specified position, pretty-printed as a string. -/ +If there is a tactic proof at the specified position, returns the current goals. +Otherwise returns `null`. -/ structure PlainGoalParams extends TextDocumentPositionParams deriving FromJson, ToJson structure PlainGoal where + /-- The goals as pretty-printed Markdown, or something like "no goals" if accomplished. -/ rendered : String + /-- The pretty-printed goals, empty if all accomplished. -/ goals : Array String deriving FromJson, ToJson diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 8a04bcea91..b52b9864f4 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -269,18 +269,16 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then withTheReader Core.Context (fun ctx => { ctx with options := opts }) do topDownAnalyze e else optionsPerPos - let run : Delaborator.DelabM (Syntax × Std.RBMap Pos Elab.Info compare) := do - let stx ← Delaborator.delab - pure (stx, (← get).infos) - catchInternalId Delaborator.delabFailureId - (run + let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId + (Delaborator.delab { defaultOptions := opts optionsPerPos := optionsPerPos currNamespace := currNamespace openDecls := openDecls subExpr := Delaborator.SubExpr.mkRoot e } - |>.run' { : Delaborator.State }) + |>.run { : Delaborator.State }) (fun _ => unreachable!) + return (stx, infos) /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 055db1333e..362337d3f4 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -222,7 +222,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams) let doc ← readDoc asTask do let ⟨cmdSnaps, e?⟩ ← doc.cmdSnaps.updateFinishedPrefix - let mut stxs := cmdSnaps.finishedPrefix.map fun s => s.stx + let mut stxs := cmdSnaps.finishedPrefix.map (·.stx) match e? with | some ElabTaskError.aborted => throw RequestError.fileChanged diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index 3657ec252c..f3b7a78478 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -106,21 +106,21 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog let cmdPos := cmdStx.getPos?.get! if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then - let endSnap : Snapshot := - { beginPos := cmdPos - stx := cmdStx - mpState := cmdParserState - cmdState := snap.cmdState - interactiveDiags := ← newInteractiveDiags msgLog - } + let endSnap : Snapshot := { + beginPos := cmdPos + stx := cmdStx + mpState := cmdParserState + cmdState := snap.cmdState + interactiveDiags := ← newInteractiveDiags msgLog + } endSnap else let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog } - let cmdCtx : Elab.Command.Context := - { cmdPos := snap.endPos - fileName := inputCtx.fileName - fileMap := inputCtx.fileMap - } + let cmdCtx : Elab.Command.Context := { + cmdPos := snap.endPos + fileName := inputCtx.fileName + fileMap := inputCtx.fileMap + } let (output, _) ← IO.FS.withIsolatedStreams do EIO.toIO ioErrorFromEmpty do Elab.Command.catchExceptions @@ -130,20 +130,20 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) : IO Snapshot := do if !output.isEmpty then postCmdState := { postCmdState with - messages := postCmdState.messages.add - { fileName := inputCtx.fileName - severity := MessageSeverity.information - pos := inputCtx.fileMap.toPosition snap.endPos - data := output - } - } - let postCmdSnap : Snapshot := - { beginPos := cmdPos - stx := cmdStx - mpState := cmdParserState - cmdState := postCmdState - interactiveDiags := ← newInteractiveDiags postCmdState.messages + messages := postCmdState.messages.add { + fileName := inputCtx.fileName + severity := MessageSeverity.information + pos := inputCtx.fileMap.toPosition snap.endPos + data := output + } } + let postCmdSnap : Snapshot := { + beginPos := cmdPos + stx := cmdStx + mpState := cmdParserState + cmdState := postCmdState + interactiveDiags := ← newInteractiveDiags postCmdState.messages + } postCmdSnap where diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 9bfb680e17..f071cc5660 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -139,10 +139,7 @@ where | nCtx, _, withContext ctx d => go nCtx ctx d | _, ctx, withNamingContext nCtx d => go nCtx ctx d | nCtx, ctx, tagged t d => do - -- tagged is *almost* perfect for detecting traces - -- expect for the following two other occurrences: - -- src/Lean/Elab/Term.lean:454 - -- src/Lean/Elab/Tactic/Basic.lean:33 + -- We postfix trace contexts with `_traceCtx` in order to detect them in messages. if let Name.str cls "_traceCtx" _ := t then let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d Format.tag f s!"[{cls}] (trace hidden)" diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 01ed95fe74..68c6b2a2dd 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -38,33 +38,29 @@ def appendTag (acc : TaggedText α) (t₀ : α) (a₀ : TaggedText α) : TaggedT | text "" => tag t₀ a₀ | a => append #[a, tag t₀ a₀] -partial def map (f : α → β) : TaggedText α → TaggedText β := - go -where go : TaggedText α → TaggedText β +variable (f : α → β) in +partial def map : TaggedText α → TaggedText β | text s => text s - | append as => append (as.map go) - | tag t a => tag (f t) (go a) + | append as => append (as.map map) + | tag t a => tag (f t) (map a) -partial def mapM [Monad m] (f : α → m β) : TaggedText α → m (TaggedText β) := - go -where go : TaggedText α → m (TaggedText β) +variable (f : α → m β) in +partial def mapM [Monad m] : TaggedText α → m (TaggedText β) | text s => text s - | append as => do append (← as.mapM go) - | tag t a => do tag (← f t) (← go a) + | append as => do append (← as.mapM mapM) + | tag t a => do tag (← f t) (← mapM a) -partial def rewrite (f : α → TaggedText α → TaggedText β) : TaggedText α → TaggedText β := - go -where go : TaggedText α → TaggedText β +variable (f : α → TaggedText α → TaggedText β) in +partial def rewrite : TaggedText α → TaggedText β | text s => text s - | append as => append (as.map go) + | append as => append (as.map rewrite) | tag t a => f t a +variable (f : α → TaggedText α → m (TaggedText β)) in /-- Like `mapM` but allows rewriting the whole subtree at `tag` nodes. -/ -partial def rewriteM [Monad m] (f : α → TaggedText α → m (TaggedText β)) : TaggedText α → m (TaggedText β) := - go -where go : TaggedText α → m (TaggedText β) +partial def rewriteM [Monad m] : TaggedText α → m (TaggedText β) | text s => text s - | append as => do append (← as.mapM go) + | append as => do append (← as.mapM rewriteM) | tag t a => f t a instance [RpcEncoding α β] : RpcEncoding (TaggedText α) (TaggedText β) where