refactor: use PersistentArray to implement MessageLog

Motivation: consistency. Now, Traces and MessageLog use the same datastructure.

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)
 

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 "<input>";
@@ -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

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)

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

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"