From dcb2bd480de585e456f2bfb77603bd087dc4767d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 4 Mar 2024 22:07:06 +0100 Subject: [PATCH] fix: fix capitalization of module names --- lakefile.lean | 8 +- src/examples/SubVerso/Examples.lean | 148 ++++++++++++++++++ src/examples/SubVerso/Examples/Env.lean | 54 +++++++ src/highlighting/SubVerso/Highlighting.lean | 2 + .../Highlighting/Code.lean | 4 +- .../Highlighting/Highlighted.lean | 2 +- src/highlighting/Subverso/Highlighting.lean | 2 - 7 files changed, 211 insertions(+), 9 deletions(-) create mode 100644 src/examples/SubVerso/Examples.lean create mode 100644 src/examples/SubVerso/Examples/Env.lean create mode 100644 src/highlighting/SubVerso/Highlighting.lean rename src/highlighting/{Subverso => SubVerso}/Highlighting/Code.lean (99%) rename src/highlighting/{Subverso => SubVerso}/Highlighting/Highlighted.lean (99%) delete mode 100644 src/highlighting/Subverso/Highlighting.lean diff --git a/lakefile.lean b/lakefile.lean index cc75f68..e42d4a8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,13 +4,13 @@ open Lake DSL package «subverso» where -- add package configuration options here -lean_lib SubversoHighlighting where +lean_lib SubVersoHighlighting where srcDir := "src/highlighting" - roots := #[`Subverso.Highlighting] + roots := #[`SubVerso.Highlighting] -lean_lib SubversoExamples where +lean_lib SubVersoExamples where srcDir := "src/examples" - roots := #[`Subverso.Examples] + roots := #[`SubVerso.Examples] @[default_target] lean_exe «subverso-tests» where diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean new file mode 100644 index 0000000..1d38f85 --- /dev/null +++ b/src/examples/SubVerso/Examples.lean @@ -0,0 +1,148 @@ +import SubVerso.Highlighting +import SubVerso.Examples.Env +import Lean.Environment + +namespace SubVerso.Examples + +open SubVerso Highlighting + +open Lean Elab Command Term + +scoped syntax "%ex" "{" ident (" : " term)? "}" "{" term "}" : term +scoped syntax "%ex" "{" ident "}" "{" tactic "}" : tactic +scoped syntax "%ex" "{" ident "}" "{" doElem "}" : doElem + + +class MonadMessageState (m : Type → Type v) where + getMessages : m MessageLog + setMessages : MessageLog → m Unit + +instance : MonadMessageState TermElabM where + getMessages := do return (← getThe Core.State).messages + setMessages msgs := modifyThe Core.State ({· with messages := msgs}) + +instance : MonadMessageState CommandElabM where + getMessages := do return (← get).messages + setMessages msgs := modify ({· with messages := msgs}) + +open MonadMessageState in +def savingNewMessages [Monad m] [MonadFinally m] [MonadMessageState m] + (act : m α) : m (α × MessageLog) := do + let startMessages ← getMessages + let mut endMessages := .empty + setMessages .empty + let res ← try + let res ← act + endMessages ← getMessages + pure res + finally + setMessages (startMessages ++ endMessages) + pure (res, endMessages) + +scoped syntax "%example" ident command command* "%end" : command + +example : TermElabM Unit := logError "foo" + +partial def extractExamples (stx : Syntax) : StateT (NameMap Syntax) Id Syntax := do + if let `(term|%ex { $n:ident }{ $tm:term }) := stx then + let next ← extractExamples tm + -- Save the erased version in case there's nested examples + modify fun st => st.insert n.getId next + pure next + else + match stx with + | .node info kind args => pure <| .node info kind (← args.mapM extractExamples) + | _ => pure stx + +elab_rules : command + | `(%example $name:ident $cmd $cmds* %end) => do + let allCommands := #[cmd] ++ cmds + let (allCommands, termExamples) := allCommands.mapM extractExamples .empty + let ((), newMessages) ← savingNewMessages (allCommands.forM elabCommand) + let trees ← getInfoTrees + let hl ← allCommands.mapM fun c => liftTermElabM (highlight c newMessages.toList.toArray trees) + let freshMsgs ← newMessages.toList.mapM fun m => do pure (m.severity, ← m.toString) + let .original leading startPos _ _ := allCommands[0]!.getHeadInfo + | throwErrorAt allCommands[0]! "Failed to get source position" + let .original _ _ trailing stopPos := allCommands.back.getTailInfo + | throwErrorAt allCommands.back "Failed to get source position" + let text ← getFileMap + let str := text.source.extract leading.startPos trailing.stopPos + modifyEnv fun ρ => highlighted.addEntry ρ (name.getId, {highlighted := hl, original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs}) + for (name, term) in termExamples do + let hl ← liftTermElabM (highlight term newMessages.toList.toArray trees) + let .original leading startPos _ _ := term.getHeadInfo + | throwErrorAt term "Failed to get source position" + let .original _ _ trailing stopPos := term.getTailInfo + | throwErrorAt term "Failed to get source position" + let str := text.source.extract leading.startPos trailing.stopPos + modifyEnv fun ρ => highlighted.addEntry ρ (name, {highlighted := #[hl], original := str, start := text.toPosition startPos, stop := text.toPosition stopPos, messages := freshMsgs}) + +scoped syntax "%dump" ident : command + +elab_rules : command + | `(%dump%$kw $name:ident) => do + let st := highlighted.getState (← getEnv) + if let some json := st.find? name.getId then + logInfoAt kw m!"{toString json}" + else + throwErrorAt name "No highlighting found for '{name}'" + +open System in +partial def loadExamples (leanProject : FilePath) : IO (NameMap Json) := do + -- Validate that the path is really a Lean project + let lakefile := leanProject / "lakefile.lean" + if !(← lakefile.pathExists) then + throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project" + -- Build the facet + let res ← IO.Process.output { + cmd := "lake" + args := #["build", ":examples"] + cwd := leanProject + } + if res.exitCode != 0 then + throw <| .userError <| + "Build process failed." ++ + decorateOut "stdout" res.stdout ++ + decorateOut "stderr" res.stderr + let hlDir := leanProject / ".lake" / "build" / "examples" + collectExamples .anonymous hlDir +where + decorateOut (name : String) (out : String) : String := + if out.isEmpty then "" else s!"\n{name}:\n{out}\n" + collectExamples (name : Name) (dir : FilePath) : IO (NameMap Json) := do + let contents ← dir.readDir + let mut out := {} + for f in contents do + match (← f.path.metadata).type with + | .dir => + let sub ← collectExamples (.str name f.fileName) f.path + out := out.mergeBy (fun _ _ j2 => j2) sub + | .file => + if f.path.extension == some "json" then + if let some mod := f.path.fileStem then + let name' : Name := .str name mod + let contents := Json.parse (← IO.FS.readFile f.path) + match contents with + | .error err => throw <| .userError s!"Couldn't parse {f.path} as JSON: {err}" + | .ok val => + out := out.insert name' val + | _ => pure () + return out + + +%example test3 +def wxyz (n : Nat) := 1 + 3 + n +#check wxyz +def xyz (n : Nat) := 1 + %ex{test2}{3 + n} +%end + +--%process_highlights + +-- %example test +-- #eval 5 +-- %end + +-- %dump test +%dump test2 +%dump test3 diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean new file mode 100644 index 0000000..fda414f --- /dev/null +++ b/src/examples/SubVerso/Examples/Env.lean @@ -0,0 +1,54 @@ +import Lean +import SubVerso.Highlighting + +open Lean + +namespace SubVerso.Examples +open SubVerso.Highlighting + +instance : ToJson Position where + toJson | ⟨l, c⟩ => toJson (l, c) + +instance : FromJson Position where + fromJson? + | .arr #[l, c] => Position.mk <$> fromJson? l <*> fromJson? c + | other => .error s!"Couldn't decode position from {other}" + +example : fromJson? (toJson (⟨1, 5⟩ : Position)) = .ok (⟨1, 5⟩ : Position) := rfl + +instance : ToJson MessageSeverity where + toJson + | .error => "error" + | .warning => "warning" + | .information => "information" + +instance : FromJson MessageSeverity where + fromJson? + | "error" => .ok .error + | "warning" => .ok .warning + | "information" => .ok .information + | other => .error s!"Expected 'error', 'warning', or 'information', got {other}" + +theorem MessageSeverity.fromJson_toJson_ok (s : MessageSeverity) : fromJson? (toJson s) = .ok s := by + cases s <;> simp [toJson, fromJson?] + +structure Example where + highlighted : Array Highlighted + messages : List (MessageSeverity × String) + original : String + start : Lean.Position + stop : Lean.Position +deriving ToJson, FromJson + +initialize highlighted : PersistentEnvExtension (NameMap Json) (Name × Example) (NameMap Json) ← + registerPersistentEnvExtension { + mkInitial := pure {} + addImportedFn := fun imported => do + let mut s := {} + for imp in imported do + for found in imp do + s := s.mergeBy (fun _ _ json => json) found + pure s + addEntryFn := fun s (n, val) => s.insert n (toJson val) + exportEntriesFn := fun s => #[s] + } diff --git a/src/highlighting/SubVerso/Highlighting.lean b/src/highlighting/SubVerso/Highlighting.lean new file mode 100644 index 0000000..0a0ae0d --- /dev/null +++ b/src/highlighting/SubVerso/Highlighting.lean @@ -0,0 +1,2 @@ +import SubVerso.Highlighting.Highlighted +import SubVerso.Highlighting.Code diff --git a/src/highlighting/Subverso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean similarity index 99% rename from src/highlighting/Subverso/Highlighting/Code.lean rename to src/highlighting/SubVerso/Highlighting/Code.lean index 1e3322f..3bcdc93 100644 --- a/src/highlighting/Subverso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -1,14 +1,14 @@ import Lean import Lean.Widget.TaggedText -import Subverso.Highlighting.Highlighted +import SubVerso.Highlighting.Highlighted open Lean Elab open Lean.Widget (TaggedText) open Lean.Widget open Lean.PrettyPrinter (InfoPerPos) -namespace Subverso.Highlighting +namespace SubVerso.Highlighting partial def Token.Kind.priority : Token.Kind → Nat | .var .. => 2 diff --git a/src/highlighting/Subverso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean similarity index 99% rename from src/highlighting/Subverso/Highlighting/Highlighted.lean rename to src/highlighting/SubVerso/Highlighting/Highlighted.lean index 526c32f..c4a1529 100644 --- a/src/highlighting/Subverso/Highlighting/Highlighted.lean +++ b/src/highlighting/SubVerso/Highlighting/Highlighted.lean @@ -2,7 +2,7 @@ import Lean open Lean -namespace Subverso.Highlighting +namespace SubVerso.Highlighting deriving instance Repr for Std.Format.FlattenBehavior deriving instance Repr for Std.Format diff --git a/src/highlighting/Subverso/Highlighting.lean b/src/highlighting/Subverso/Highlighting.lean deleted file mode 100644 index ab51c69..0000000 --- a/src/highlighting/Subverso/Highlighting.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Subverso.Highlighting.Highlighted -import Subverso.Highlighting.Code