From 76f28817b6aefaf6c881016bb709c609f12c3ca9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 8 Dec 2023 15:12:48 +0100 Subject: [PATCH] feat: include expected Lean outputs and have the compiler check them --- src/leanblog/LeanDoc/Genre/Blog.lean | 71 ++++++++++++++++++++++++- src/leandoc/LeanDoc/Doc/Suggestion.lean | 37 +++++++++++++ 2 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 src/leandoc/LeanDoc/Doc/Suggestion.lean diff --git a/src/leanblog/LeanDoc/Genre/Blog.lean b/src/leanblog/LeanDoc/Genre/Blog.lean index 4019d89..a2f4965 100644 --- a/src/leanblog/LeanDoc/Genre/Blog.lean +++ b/src/leanblog/LeanDoc/Genre/Blog.lean @@ -6,6 +6,7 @@ import LeanDoc.Genre.Blog.Site import LeanDoc.Genre.Blog.Site.Syntax import LeanDoc.Genre.Blog.Template import LeanDoc.Genre.Blog.Theme +import LeanDoc.Doc.Suggestion open LeanDoc.Output Html open Lean (RBMap) @@ -141,7 +142,6 @@ def LeanBlockConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [M error := errorArg } else throwError "No arguments provided, expected at least a context name" - where asName (name : Name) (v : Doc.Elab.RoleArgumentValue) : m Name := do match v with @@ -241,6 +241,75 @@ def lean : CodeBlockExpander else pure #[] +structure LeanOutputConfig where + name : Ident + severity : Option MessageSeverity + +def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array RoleArgument) : m LeanOutputConfig := do + if h : 0 < args.size then + let .anonymous (.name outputName) := args[0] + | throwError s!"Expected output name, got {repr args[0]}" + let (severityArgs, args) := takeNamed `severity <| args.extract 1 args.size + let severityArg ← takeVal `severity severityArgs >>= Option.mapM (asSeverity `severity) + + if !args.isEmpty then + throwError s!"Unexpected arguments: {repr args}" + pure { + name := outputName + severity := severityArg + } + else throwError "No arguments provided, expected at least a context name" +where + asSeverity (name : Name) (v : Doc.Elab.RoleArgumentValue) : m MessageSeverity := do + match v with + | .name b => do + let b' ← resolveGlobalConstNoOverloadWithInfo b + if b' == ``MessageSeverity.error then pure MessageSeverity.error + else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning + else if b' == ``MessageSeverity.information then pure MessageSeverity.information + else throwErrorAt b "Expected 'error' or 'warning' or 'information'" + | other => throwError "Expected severity for '{name}', got {repr other}" + takeVal {α} (key : Name) (vals : Array α) : m (Option α) := do + if vals.size = 0 then pure none + else if h : vals.size = 1 then + have : 0 < vals.size := by rw [h]; trivial + pure (some vals[0]) + else throwError "Duplicate values for '{key}'" + + +@[code_block_expander leanOutput] +def leanOutput : Doc.Elab.CodeBlockExpander + | args, str => do + let config ← LeanOutputConfig.fromArgs args -- TODO actual parser for my args + + let some savedInfo := messageContextExt.getState (← getEnv) |>.messages |>.find? config.name.getId + | throwErrorAt str "No saved info for name '{config.name.getId}'" + let messages ← liftM <| savedInfo.msgs.toArray.mapM contents + for m in savedInfo.msgs do + if mostlyEqual str.getString (← contents m) then + if let some s := config.severity then + if s != m.severity then + throwErrorAt str s!"Expected severity {sev s}, but got {sev m.severity}" + return #[← `(Block.code none #[] 0 $(quote str.getString))] + for m in messages do + LeanDoc.Doc.Suggestion.saveSuggestion str (m.take 30 ++ "…") m + throwErrorAt str "Didn't match - expected one of: {indentD (toMessageData messages)}\nbut got:{indentD (toMessageData str.getString)}" +where + withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str + + sev : MessageSeverity → String + | .error => "error" + | .information => "information" + | .warning => "warning" + + contents (message : Message) : IO String := do + let head := if message.caption != "" then message.caption ++ ":\n" else "" + pure <| withNewline <| head ++ (← message.data.toString) + + mostlyEqual (s1 s2 : String) : Bool := + s1.trim == s2.trim + + private def filterString (p : Char → Bool) (str : String) : String := Id.run <| do let mut out := "" diff --git a/src/leandoc/LeanDoc/Doc/Suggestion.lean b/src/leandoc/LeanDoc/Doc/Suggestion.lean new file mode 100644 index 0000000..b3a3a08 --- /dev/null +++ b/src/leandoc/LeanDoc/Doc/Suggestion.lean @@ -0,0 +1,37 @@ +import Lean + +namespace LeanDoc.Doc.Suggestion + +open Lean Elab Server RequestM + +structure Suggestion where + summary : String + replacement : String +deriving TypeName + +def saveSuggestion [Monad m] [MonadInfoTree m] (stx : Syntax) (summary replacement: String) : m Unit := do + pushInfoLeaf <| .ofCustomInfo {stx := stx, value := Dynamic.mk (Suggestion.mk summary replacement) } + +@[code_action_provider] +def provideSuggestions : CodeActionProvider := fun params snap => do + let doc ← readDoc + let text := doc.meta.text + let startPos := text.lspPosToUtf8Pos params.range.start + let endPos := text.lspPosToUtf8Pos params.range.end + let suggestions := snap.infoTree.foldInfo (init := #[]) fun ctx info result => Id.run do + let .ofCustomInfo ⟨stx, data⟩ := info | result + let some suggestions := data.get? Suggestion | result + let (some head, some tail) := (stx.getPos? true, stx.getTailPos? true) | result + unless head ≤ endPos && startPos ≤ tail do return result + result.push (ctx, head, tail, suggestions) + pure <| suggestions.map fun (_, head, tail, ⟨summary, replacement⟩) => + { + eager := { + title := s!"Replace with {summary}", + kind? := some "quickfix", + edit? := some <| .ofTextDocumentEdit { + textDocument := doc.versionedIdentifier, + edits := #[{newText := replacement, range := ⟨text.utf8PosToLspPos head, text.utf8PosToLspPos tail⟩}] + } + } + }