chore(library/init/data/dlist): Dlist => DList

library/init/data/dlist.lean

@@ -12,42 +12,42 @@ contents of the difference List prepended to the given List.
 This structure supports `O(1)` `append` and `concat` operations on lists, making it
 useful for append-heavy uses such as logging and pretty printing.
 -/
-structure Dlist (α : Type u) :=
+structure DList (α : Type u) :=
 (apply     : List α → List α)
 (invariant : ∀ l, apply l = apply [] ++ l)
 
-namespace Dlist
+namespace DList
 variables {α : Type u}
 open List
 
-def ofList (l : List α) : Dlist α :=
+def ofList (l : List α) : DList α :=
 ⟨append l, λ t, (appendNil l).symm ▸ rfl⟩
 
-def empty : Dlist α :=
+def empty : DList α :=
 ⟨id, λ t, rfl⟩
 
-def toList : Dlist α → List α
+def toList : DList α → List α
 | ⟨f, h⟩ := f []
 
-def singleton (a : α) : Dlist α :=
+def singleton (a : α) : DList α :=
 ⟨λ t, a :: t, λ t, rfl⟩
 
-def cons : α → Dlist α → Dlist α
+def cons : α → DList α → DList α
 | a ⟨f, h⟩ := ⟨λ t, a :: f t, λ t,
                show a :: f t = a :: f [] ++ t, from
                have h₁ : a :: f t = a :: (f nil ++ t), from h t ▸ rfl,
                have h₂ : a :: (f nil ++ t) = a :: f nil ++ t, from (consAppend _ _ _).symm,
                Eq.trans h₁ h₂⟩
 
-def append : Dlist α → Dlist α → Dlist α
+def append : DList α → DList α → DList α
 | ⟨f, h₁⟩ ⟨g, h₂⟩ := ⟨f ∘ g, λ t,
                       show f (g t) = (f (g [])) ++ t, from
                       (h₁ (g [])).symm ▸ (appendAssoc (f []) (g []) t).symm ▸ h₂ t ▸ h₁ (g t) ▸ rfl⟩
 
-def push : Dlist α → α → Dlist α
+def push : DList α → α → DList α
 | ⟨f, h⟩ a := ⟨λ t, f (a :: t), λ t, (h (a::t)).symm ▸ (h [a]).symm ▸ (appendAssoc (f []) [a] t).symm ▸ rfl⟩
 
-instance : HasAppend (Dlist α) :=
-⟨Dlist.append⟩
+instance : HasAppend (DList α) :=
+⟨DList.append⟩
 
-end Dlist
+end DList

library/init/lean/parser/module.lean

@@ -85,7 +85,7 @@ private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
     -- unknown command: try to skip token, or else single character
     when (¬ recovering) $ do {
       it ← leftOver,
-      logMessage {expected := Dlist.singleton "command", it := it, custom := some ()}
+      logMessage {expected := DList.singleton "command", it := it, custom := some ()}
     },
     try (monadLift token *> pure ()) <|> (any *> pure ()),
     pure (true, none)

library/init/lean/parser/notation.lean

@@ -74,7 +74,7 @@ node! symbolQuote [
 def unquotedSymbol.Parser : termParser :=
 try $ do {
   it ← leftOver,
-  stx@(Syntax.atom _) ← monadLift token | error "" (Dlist.singleton "symbol") it,
+  stx@(Syntax.atom _) ← monadLift token | error "" (DList.singleton "symbol") it,
   pure stx
 } <?> "symbol"
 

library/init/lean/parser/parsec.lean

@@ -21,7 +21,7 @@ namespace Parsec
 structure Message (μ : Type := Unit) :=
 (it         : Iterator)
 (unexpected : String       := "")          -- unexpected input
-(expected   : Dlist String := Dlist.empty) -- expected productions
+(expected   : DList String := DList.empty) -- expected productions
 (custom     : Option μ)
 
 def expected.toString : List String → String
@@ -55,11 +55,11 @@ They contain the error that would have occurred if a
 successful "epsilon" Alternative was not taken.
 -/
 inductive Result (μ α : Type)
-| ok {} (a : α) (it : Iterator) (expected : Option $ Dlist String) : Result
+| ok {} (a : α) (it : Iterator) (expected : Option $ DList String) : Result
 | error {} (msg : Message μ) (consumed : Bool)                     : Result
 
 @[inline] def Result.mkEps {μ α : Type} (a : α) (it : Iterator) : Result μ α :=
-Result.ok a it (some Dlist.empty)
+Result.ok a it (some DList.empty)
 end Parsec
 
 open Parsec
@@ -99,7 +99,7 @@ protected def failure : ParsecT μ m α :=
 def merge (msg₁ msg₂ : Message μ) : Message μ :=
 { expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
 
-@[inlineIfReduce] def bindMkRes (ex₁ : Option (Dlist String)) (r : Result μ β) : Result μ β :=
+@[inlineIfReduce] def bindMkRes (ex₁ : Option (DList String)) (r : Result μ β) : Result μ β :=
 match ex₁, r with
 | none,     ok b it _          := ok b it none
 | none,     error msg _        := error msg true
@@ -155,15 +155,15 @@ instance : HasMonadLift m (ParsecT μ m) :=
 { monadLift := λ α x it, do a ← x, pure (mkEps a it) }
 
 def expect (msg : Message μ) (exp : String) : Message μ :=
-{expected := Dlist.singleton exp, ..msg}
+{expected := DList.singleton exp, ..msg}
 
-@[inlineIfReduce] def labelsMkRes (r : Result μ α) (lbls : Dlist String) : Result μ α :=
+@[inlineIfReduce] def labelsMkRes (r : Result μ α) (lbls : DList String) : Result μ α :=
 match r with
   | ok a it (some _) := ok a it (some lbls)
   | error msg false     := error {expected := lbls, ..msg} false
   | other            := other
 
-@[inline] def labels (p : ParsecT μ m α) (lbls : Dlist String) : ParsecT μ m α :=
+@[inline] def labels (p : ParsecT μ m α) (lbls : DList String) : ParsecT μ m α :=
 λ it, do
   r ← p it,
   pure $ labelsMkRes r lbls
@@ -259,7 +259,7 @@ namespace MonadParsec
 open ParsecT
 variables {m : Type → Type} [Monad m] [MonadParsec μ m] {α β : Type}
 
-def error {α : Type} (unexpected : String) (expected : Dlist String := Dlist.empty)
+def error {α : Type} (unexpected : String) (expected : DList String := DList.empty)
           (it : Option Iterator := none) (custom : Option μ := none) : m α :=
 lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } false
 
@@ -270,16 +270,16 @@ lift $ λ it, Result.mkEps it it
 @[inline] def remaining : m Nat :=
 String.Iterator.remaining <$> leftOver
 
-@[inline] def labels (p : m α) (lbls : Dlist String) : m α :=
+@[inline] def labels (p : m α) (lbls : DList String) : m α :=
 map (λ m' inst β p, @ParsecT.labels m' inst μ β p lbls) p
 
 @[inline] def label (p : m α) (lbl : String) : m α :=
-labels p (Dlist.singleton lbl)
+labels p (DList.singleton lbl)
 
 infixr ` <?> `:2 := label
 
 @[inline] def hidden (p : m α) : m α :=
-labels p Dlist.empty
+labels p DList.empty
 
 /--
 `try p` behaves like `p`, but it pretends `p` hasn't
@@ -364,14 +364,14 @@ This Parser consumes no input if it fails (even if a partial match).
 Note: The behaviour of this Parser is different to that the `String` Parser in the ParsecT Μ M Haskell library,
 as this one is all-or-nothing.
 -/
-def strCore (s : String) (ex : Dlist String) : m String :=
+def strCore (s : String) (ex : DList String) : m String :=
 if s.isEmpty then pure ""
 else lift $ λ it, match strAux s.length s.mkIterator it with
   | some it' := Result.ok s it' none
   | none     := Result.error { it := it, expected := ex, custom := none } false
 
 @[inline] def str (s : String) : m String :=
-strCore s (Dlist.singleton (repr s))
+strCore s (DList.singleton (repr s))
 
 private def takeAux : Nat → String → Iterator → Result μ String
 | 0     r it := Result.ok r it none
@@ -459,7 +459,7 @@ String.toNat <$> (takeWhile1 Char.isDigit)
 def ensure (n : Nat) : m Unit :=
 do it ← leftOver,
    if n ≤ it.remaining then pure ()
-   else error "end of input" (Dlist.singleton ("at least " ++ toString n ++ " characters"))
+   else error "end of input" (DList.singleton ("at least " ++ toString n ++ " characters"))
 
 /-- Return the current Position. -/
 def pos : m Position :=
@@ -470,12 +470,12 @@ String.Iterator.offset <$> leftOver
 @[inline] def notFollowedBy [MonadExcept (Message μ) m] (p : m α) (msg : String := "input") : m Unit :=
 do it ← leftOver,
    b ← lookahead $ catch (p *> pure false) (λ _, pure true),
-   if b then pure () else error msg Dlist.empty it
+   if b then pure () else error msg DList.empty it
 
 def eoi : m Unit :=
 do it ← leftOver,
    if it.remaining = 0 then pure ()
-   else error (repr it.curr) (Dlist.singleton ("end of input"))
+   else error (repr it.curr) (DList.singleton ("end of input"))
 
 @[specialize] def many1Aux [Alternative m] (p : m α) : Nat → m (List α)
 | 0     := do a ← p, pure [a]
@@ -534,7 +534,7 @@ def unexpected (msg : String) : m α :=
 error msg
 
 def unexpectedAt (msg : String) (it : Iterator) : m α :=
-error msg Dlist.empty it
+error msg DList.empty it
 
 /- Execute all parsers in `ps` and return the Result of the longest parse(s) if any,
    or else the Result of the furthest error. If there are two parses of

library/init/lean/parser/token.lean

@@ -234,7 +234,7 @@ observing (try (lookahead token))
 
 variable [monadBasicParser m]
 
-def symbolCore (sym : String) (lbp : Nat) (ex : Dlist String) : Parser :=
+def symbolCore (sym : String) (lbp : Nat) (ex : DList String) : Parser :=
 lift $ try $ do {
   it ← leftOver,
   stx@(Syntax.atom ⟨_, sym'⟩) ← token | error "" ex it,
@@ -245,7 +245,7 @@ lift $ try $ do {
 
 @[inline] def symbol (sym : String) (lbp := 0) : Parser :=
 let sym := sym.trim in
-symbolCore sym lbp (Dlist.singleton sym)
+symbolCore sym lbp (DList.singleton sym)
 
 instance symbol.tokens (sym lbp) : Parser.HasTokens (symbol sym lbp : Parser) :=
 ⟨[⟨sym.trim, lbp, none⟩]⟩
@@ -261,7 +261,7 @@ def number.Parser : Parser :=
 lift $ try $ do {
   it ← leftOver,
   stx ← token,
-  some _ ← pure $ tryView number stx | error "" (Dlist.singleton "number") it,
+  some _ ← pure $ tryView number stx | error "" (DList.singleton "number") it,
   pure stx
 } <?> "number"
 
@@ -299,7 +299,7 @@ def stringLit.Parser : Parser :=
 lift $ try $ do {
   it ← leftOver,
   stx ← token,
-  some _ ← pure $ tryView stringLit stx | error "" (Dlist.singleton "String") it,
+  some _ ← pure $ tryView stringLit stx | error "" (DList.singleton "String") it,
   pure stx
 } <?> "String"
 
@@ -316,7 +316,7 @@ def stringLit.View.value (lit : stringLit.View) : Option String := do
 def ident.Parser : Parser :=
 lift $ try $ do {
   it ← leftOver,
-  stx@(Syntax.ident _) ← token | error "" (Dlist.singleton "identifier") it,
+  stx@(Syntax.ident _) ← token | error "" (DList.singleton "identifier") it,
   pure stx
 } <?> "identifier"
 
@@ -351,7 +351,7 @@ lift $ try $ do
   | Syntax.ident id := some id.rawVal.toString
   | _ := none,
   when (sym' ≠ some sym) $
-    error "" (Dlist.singleton (repr sym)) it,
+    error "" (DList.singleton (repr sym)) it,
   pure stx
 
 instance symbolOrIdent.tokens (sym) : Parser.HasTokens (symbolOrIdent sym : Parser) :=