From d53c5a31cb752658129138bbfc55ad641c36fb30 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Dec 2019 08:11:20 -0800 Subject: [PATCH] refactor: use `PersistentArray` to implement `MessageLog` Motivation: consistency. Now, Traces and MessageLog use the same datastructure. --- src/Init/Data/PersistentArray/Basic.lean | 6 ++++++ src/Init/Lean/Elab/Import.lean | 6 +++++- src/Init/Lean/Parser/Module.lean | 4 ++-- src/Init/Lean/Util/Message.lean | 17 ++++++++++------- tests/lean/run/frontend1.lean | 5 +++-- 5 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/PersistentArray/Basic.lean b/src/Init/Data/PersistentArray/Basic.lean index 8f4553d326..c9bf7ce43d 100644 --- a/src/Init/Data/PersistentArray/Basic.lean +++ b/src/Init/Data/PersistentArray/Basic.lean @@ -246,6 +246,12 @@ Id.run (t.foldlM f b) def toArray (t : PersistentArray α) : Array α := t.foldl Array.push #[] +def append (t₁ t₂ : PersistentArray α) : PersistentArray α := +if t₁.isEmpty then t₂ +else t₂.foldl PersistentArray.push t₁ + +instance : HasAppend (PersistentArray α) := ⟨append⟩ + @[inline] def find? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β := Id.run (t.findM? f) diff --git a/src/Init/Lean/Elab/Import.lean b/src/Init/Lean/Elab/Import.lean index af6d1fd7b7..35ea571892 100644 --- a/src/Init/Lean/Elab/Import.lean +++ b/src/Init/Lean/Elab/Import.lean @@ -28,7 +28,6 @@ catch let pos := ctx.fileMap.toPosition spos; pure (env, messages.add { fileName := ctx.fileName, data := toString e, pos := pos })) -@[export lean_parse_imports] def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do env ← mkEmptyEnvironment; let fileName := fileName.getD ""; @@ -37,6 +36,11 @@ match Parser.parseHeader env ctx with | (header, parserState, messages) => do pure (headerToImports header, ctx.fileMap.toPosition parserState.pos, messages) +@[export lean_parse_imports] +def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do +(imports, pos, log) ← parseImports input fileName; +pure (imports, pos, log.toList) + @[export lean_print_deps] def printDeps (deps : List Import) : IO Unit := deps.forM $ fun dep => do diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean index bcba9f4e9a..f81ceff0e5 100644 --- a/src/Init/Lean/Parser/Module.lean +++ b/src/Init/Lean/Parser/Module.lean @@ -90,7 +90,7 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo match parseCommand env c s messages with | (stx, s, messages) => if isEOI stx || isExitCommand stx then do - messages.toList.forM $ fun msg => IO.println msg; + messages.forM $ fun msg => IO.println msg; pure (!messages.hasErrors) else do when displayStx (IO.println stx); @@ -113,7 +113,7 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP let stx := mkListNode stxs; pure stx.updateLeading else do - msgs.toList.forM $ fun msg => IO.println msg; + msgs.forM $ fun msg => IO.println msg; throw (IO.userError "failed to parse file") else parseFileAux state msgs (stxs.push stx) diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean index febbf2d09b..8694038476 100644 --- a/src/Init/Lean/Util/Message.lean +++ b/src/Init/Lean/Util/Message.lean @@ -121,32 +121,35 @@ instance : HasToString Message := end Message structure MessageLog := --- messages are stored in reverse for efficient append -(revList : List Message := []) +(msgs : PersistentArray Message := {}) namespace MessageLog def empty : MessageLog := ⟨{}⟩ def isEmpty (log : MessageLog) : Bool := -log.revList.isEmpty +log.msgs.isEmpty instance : Inhabited MessageLog := ⟨{}⟩ def add (msg : Message) (log : MessageLog) : MessageLog := -⟨msg :: log.revList⟩ +⟨log.msgs.push msg⟩ protected def append (l₁ l₂ : MessageLog) : MessageLog := -⟨l₂.revList ++ l₁.revList⟩ +⟨l₁.msgs ++ l₂.msgs⟩ instance : HasAppend MessageLog := ⟨MessageLog.append⟩ def hasErrors (log : MessageLog) : Bool := -log.revList.any $ fun m => match m.severity with +log.msgs.any $ fun m => match m.severity with | MessageSeverity.error => true | _ => false +def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit := +log.msgs.forM f + def toList (log : MessageLog) : List Message := -log.revList.reverse +(log.msgs.foldl (fun acc msg => msg :: acc) []).reverse + end MessageLog end Lean diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index 81b9937d8e..da5a0eb1c3 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -6,7 +6,7 @@ def run (input : String) (failIff : Bool := true) : MetaIO Unit := do env ← MetaIO.getEnv; opts ← MetaIO.getOptions; let (env, messages) := process input env opts; - messages.toList.forM $ fun msg => IO.println msg; + messages.forM $ fun msg => IO.println msg; when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found"); when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors"); pure () @@ -158,7 +158,8 @@ f a #eval run "#check #[1, 2].foldl (fun r a => r.push a $.push a $.push a) #[]" #eval run "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a $.push a" + #eval run "#check let x := one + zero; x + x" --- set_option trace.Elab true +set_option trace.Elab true #eval run "#check (fun x => let v := x.w; v + v) s4" #eval run "#check fun x => foo x (let v := x.w; v + one) s4"