From 050008cb84013ece09b28bcbed8294c8a7ba4ab2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Dec 2019 07:36:26 -0800
Subject: [PATCH] refactor: use `PersistentArray` instead of `Array` for
 default `[MonadTracer]` implementation

Motivation: flexibility. Now, the default implementation is better
suited for code that uses traces nonlinearly (e.g., `TermElabM`).
---
 src/Init/Data/PersistentArray/Basic.lean |  3 +++
 src/Init/Lean/Util/Trace.lean            | 29 +++++++++++++++---------
 2 files changed, 21 insertions(+), 11 deletions(-)

diff --git a/src/Init/Data/PersistentArray/Basic.lean b/src/Init/Data/PersistentArray/Basic.lean
index a41573e834..8f4553d326 100644
--- a/src/Init/Data/PersistentArray/Basic.lean
+++ b/src/Init/Data/PersistentArray/Basic.lean
@@ -243,6 +243,9 @@ end
 @[inline] def foldl {β} (t : PersistentArray α) (f : β → α → β) (b : β) : β :=
 Id.run (t.foldlM f b)
 
+def toArray (t : PersistentArray α) : Array α :=
+t.foldl Array.push #[]
+
 @[inline] def find? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β :=
 Id.run (t.findM? f)
 
diff --git a/src/Init/Lean/Util/Trace.lean b/src/Init/Lean/Util/Trace.lean
index a6e9c16fa3..58600e913c 100644
--- a/src/Init/Lean/Util/Trace.lean
+++ b/src/Init/Lean/Util/Trace.lean
@@ -18,8 +18,8 @@ class MonadTracerAdapter (m : Type → Type) :=
 (isTracingEnabledFor {} : Name → m Bool)
 (addContext {} : MessageData → m MessageData)
 (enableTracing {} : Bool → m Bool)
-(getTraces {} : m (Array MessageData))
-(modifyTraces {} : (Array MessageData → Array MessageData) → m Unit)
+(getTraces {} : m (PersistentArray MessageData))
+(modifyTraces {} : (PersistentArray MessageData → PersistentArray MessageData) → m Unit)
 
 namespace MonadTracerAdapter
 
@@ -28,14 +28,14 @@ variables {m : Type → Type}
 variables [Monad m] [MonadTracerAdapter m]
 variables {α : Type}
 
-private def addNode (oldTraces : Array MessageData) (cls : Name) : m Unit :=
+private def addNode (oldTraces : PersistentArray MessageData) (cls : Name) : m Unit :=
 modifyTraces $ fun traces =>
-  let d := MessageData.tagged cls (MessageData.node traces);
+  let d := MessageData.tagged cls (MessageData.node traces.toArray);
   oldTraces.push d
 
-private def getResetTraces : m (Array MessageData) := do
+private def getResetTraces : m (PersistentArray MessageData) := do
 oldTraces ← getTraces;
-modifyTraces $ fun _ => #[];
+modifyTraces $ fun _ => {};
 pure oldTraces
 
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
@@ -93,13 +93,20 @@ instance monadTracerAdapterExcept {ε : Type} {m : Type → Type} [Monad m] [Mon
 
 structure TraceState :=
 (enabled : Bool := true)
-(traces  : Array MessageData := #[])
+(traces  : PersistentArray MessageData := {})
 
 namespace TraceState
 
 instance : Inhabited TraceState := ⟨{}⟩
 
-instance : HasFormat TraceState := ⟨fun s => Format.joinArraySep s.traces Format.line⟩
+private def toFormat (traces : PersistentArray MessageData) (sep : Format) : Format :=
+traces.size.fold
+  (fun i r =>
+    let curr := format $ traces.get! i;
+    if i > 0 then r ++ sep ++ curr else r ++ curr)
+  Format.nil
+
+instance : HasFormat TraceState := ⟨fun s => toFormat s.traces Format.line⟩
 
 instance : HasToString TraceState := ⟨toString ∘ fmt⟩
 
@@ -134,13 +141,13 @@ let oldEnabled := s.enabled;
 modifyTraceState $ fun s => { enabled := b, .. s };
 pure oldEnabled
 
-@[inline] def getTraces : m (Array MessageData) := do
+@[inline] def getTraces : m (PersistentArray MessageData) := do
 s ← getTraceState; pure s.traces
 
-@[inline] def modifyTraces (f : Array MessageData → Array MessageData) : m Unit :=
+@[inline] def modifyTraces (f : PersistentArray MessageData → PersistentArray MessageData) : m Unit :=
 modifyTraceState $ fun s => { traces := f s.traces, .. s }
 
-@[inline] def setTrace (f : Array MessageData → Array MessageData) : m Unit :=
+@[inline] def setTrace (f : PersistentArray MessageData → PersistentArray MessageData) : m Unit :=
 modifyTraceState $ fun s => { traces := f s.traces, .. s }
 
 @[inline] def setTraceState (s : TraceState) : m Unit :=