From 91204a52d697e20ad48cd8a2e5a353f355d47e1a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Mar 2019 17:03:22 -0700 Subject: [PATCH] chore(library/init/data/dlist): `Dlist` => `DList` --- library/init/data/dlist.lean | 24 +++++++++--------- library/init/lean/parser/module.lean | 2 +- library/init/lean/parser/notation.lean | 2 +- library/init/lean/parser/parsec.lean | 34 +++++++++++++------------- library/init/lean/parser/token.lean | 12 ++++----- 5 files changed, 37 insertions(+), 37 deletions(-) diff --git a/library/init/data/dlist.lean b/library/init/data/dlist.lean index db95db5365..a1c37a3544 100644 --- a/library/init/data/dlist.lean +++ b/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 diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index 7a43fbbdf0..9c40ca39f6 100644 --- a/library/init/lean/parser/module.lean +++ b/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) diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean index 2198cb63c8..bce3240f6d 100644 --- a/library/init/lean/parser/notation.lean +++ b/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" diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 7d80e65390..d93b308082 100644 --- a/library/init/lean/parser/parsec.lean +++ b/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 diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index f50fd0e6ab..4cb79a2fda 100644 --- a/library/init/lean/parser/token.lean +++ b/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) :=