From 3befc219c9561ebdf327be6e94f3cec4654e6170 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Mar 2019 16:59:36 -0700 Subject: [PATCH] chore(library/init): `Empty` => `empty` when it is a function --- library/init/data/array/basic.lean | 6 +++--- library/init/data/dlist.lean | 2 +- library/init/data/hashmap/basic.lean | 6 +++--- library/init/data/rbmap/basic.lean | 2 +- library/init/data/rbtree/basic.lean | 4 ++-- library/init/lean/elaborator.lean | 12 ++++++------ library/init/lean/message.lean | 2 +- library/init/lean/parser/basic.lean | 4 ++-- library/init/lean/parser/combinators.lean | 2 +- library/init/lean/parser/module.lean | 2 +- library/init/lean/parser/parsec.lean | 12 ++++++------ tests/compiler/array_test.lean | 2 +- 12 files changed, 28 insertions(+), 28 deletions(-) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 2c48e70bff..31d4ecb7b3 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -40,10 +40,10 @@ def mkNil (_ : Unit) : Array α := { sz := 0, data := λ ⟨x, h⟩, absurd h (Nat.notLtZero x) } -def nil : Array α := +def empty : Array α := mkNil () -def Empty (a : Array α) : Bool := +def isEmpty (a : Array α) : Bool := a.size = 0 @[extern cpp inline "lean::array_read(#2, #3)"] @@ -155,4 +155,4 @@ def List.toArrayAux {α : Type u} : List α → Array α → Array α | (a::as) r := List.toArrayAux as (r.push a) def List.toArray {α : Type u} (l : List α) : Array α := -l.toArrayAux Array.nil +l.toArrayAux Array.empty diff --git a/library/init/data/dlist.lean b/library/init/data/dlist.lean index cc3c72dd7e..db95db5365 100644 --- a/library/init/data/dlist.lean +++ b/library/init/data/dlist.lean @@ -23,7 +23,7 @@ open List 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 α diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index e482958e80..24be337c70 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -135,7 +135,7 @@ def size (m : DHashmap α β) : Nat := match m with | ⟨ {size := sz, ..}, _ ⟩ := sz -@[inline] def Empty (m : DHashmap α β) : Bool := +@[inline] def empty (m : DHashmap α β) : Bool := m.size = 0 end DHashmap @@ -167,7 +167,7 @@ DHashmap.fold m d f @[inline] def size (m : Hashmap α β) : Nat := DHashmap.size m -@[inline] def Empty (m : Hashmap α β) : Bool := -DHashmap.Empty m +@[inline] def empty (m : Hashmap α β) : Bool := +DHashmap.empty m end Hashmap diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index b80c27bc2d..3691718a01 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -166,7 +166,7 @@ t.val.depth f @[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : RBMap α β lt) : m PUnit := t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩ -@[inline] def Empty : RBMap α β lt → Bool +@[inline] def empty : RBMap α β lt → Bool | ⟨leaf, _⟩ := true | _ := false diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 5b45d2fda4..eada58f689 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -31,8 +31,8 @@ RBMap.mfold (λ a _ r, f a r) t b @[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : RBTree α lt) : m PUnit := t.mfold (λ a _, f a *> pure ⟨⟩) ⟨⟩ -@[inline] def Empty (t : RBTree α lt) : Bool := -RBMap.Empty t +@[inline] def empty (t : RBTree α lt) : Bool := +RBMap.empty t @[specialize] def toList (t : RBTree α lt) : List α := t.revFold (::) [] diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 0b019b72fb..97d9ced266 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -66,7 +66,7 @@ structure OrderedRBMap (α β : Type) (lt : α → α → Prop) := namespace OrderedRBMap variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRBMap α β lt) -def Empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0} +def empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0} def insert (k : α) (v : β) : OrderedRBMap α β lt := {entries := (k, v)::m.entries, map := m.map.insert k (m.size, v), size := m.size + 1} @@ -75,7 +75,7 @@ def find (a : α) : Option (Nat × β) := m.map.find a def ofList (l : List (α × β)) : OrderedRBMap α β lt := -l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.Empty +l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.empty end OrderedRBMap structure ElaboratorConfig extends FrontendConfig := @@ -93,9 +93,9 @@ structure Scope := (notations : List NotationMacro := []) /- The set of local universe variables. We remember their insertion order so that we can keep the order when copying them to declarations. -/ -(univs : OrderedRBMap Name Level (<) := OrderedRBMap.Empty) +(univs : OrderedRBMap Name Level (<) := OrderedRBMap.empty) /- The set of local variables. -/ -(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.Empty) +(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.empty) /- The subset of `vars` that is tagged as always included. -/ (includeVars : RBTree Name (<) := mkRBTree _ _) /- The stack of nested active `namespace` commands. -/ @@ -120,7 +120,7 @@ structure ElaboratorState := -- Stack of current scopes. The bottom-most Scope is the Module Scope. (scopes : List Scope) -(messages : MessageLog := MessageLog.Empty) +(messages : MessageLog := MessageLog.empty) (parserCfg : ModuleParserConfig) (expanderCfg : Expander.ExpanderConfig) (env : environment) @@ -988,7 +988,7 @@ def mkState (cfg : ElaboratorConfig) (env : environment) (opts : Options) : Elab scopes := [{cmd := "MODULE", header := `MODULE, Options := opts}]} def processCommand (cfg : ElaboratorConfig) (st : ElaboratorState) (cmd : Syntax) : ElaboratorState := -let st := {st with messages := MessageLog.Empty} in +let st := {st with messages := MessageLog.empty} in let r := @ExceptT.run _ id _ $ flip StateT.run st $ flip ReaderT.run cfg $ RecT.run (command.elaborate cmd) (λ _, error cmd "Elaborator.run: recursion depth exceeded") diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index dd5e9e1521..5d0adf713b 100644 --- a/library/init/lean/message.lean +++ b/library/init/lean/message.lean @@ -40,7 +40,7 @@ structure MessageLog := (revList : List Message) namespace MessageLog -def Empty : MessageLog := +def empty : MessageLog := ⟨[]⟩ def add (msg : Message) (log : MessageLog) : MessageLog := diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 95c2e6506c..f85cab03f6 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -127,10 +127,10 @@ def messageOfParsecMessage {μ : Type} (cfg : FrontendConfig) (msg : Parsec.Mess /-- Run Parser stack, returning a partial Syntax tree in case of a fatal error -/ protected def run {m : Type → Type} {α ρ : Type} [Monad m] [HasCoeT ρ FrontendConfig] (cfg : ρ) (s : String) (r : StateT ParserState (ParserT ρ m) α) : m (Sum α Syntax × MessageLog) := -do (r, _) ← (((r.run {messages:=MessageLog.Empty}).run cfg).parse s).run {}, +do (r, _) ← (((r.run {messages:=MessageLog.empty}).run cfg).parse s).run {}, pure $ match r with | Except.ok (a, st) := (Sum.inl a, st.messages) -| Except.error msg := (Sum.inr msg.custom.get, MessageLog.Empty.add (messageOfParsecMessage cfg msg)) +| Except.error msg := (Sum.inr msg.custom.get, MessageLog.empty.add (messageOfParsecMessage cfg msg)) open MonadParsec open Parser.HasView diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean index a94a79b6e6..78d9b4ba24 100644 --- a/library/init/lean/parser/combinators.lean +++ b/library/init/lean/parser/combinators.lean @@ -69,7 +69,7 @@ instance many.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (many ⟨tokens r⟩ instance many.view (r : Parser) [HasView α r] : Parser.HasView (List α) (many r) := -/- Remark: `many1.view` can handle Empty List. -/ +/- Remark: `many1.view` can handle empty list. -/ {..many1.view r} private def sepByAux (p : m Syntax) (sep : Parser) (allowTrailingSep : Bool) : Bool → List Syntax → Nat → Parser diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index 81cdc8ac76..7a43fbbdf0 100644 --- a/library/init/lean/parser/module.lean +++ b/library/init/lean/parser/module.lean @@ -114,7 +114,7 @@ structure ModuleParserSnapshot := -- return (partial) Syntax tree and single fatal or multiple non-fatal messages def resumeModuleParser {α : Type} (cfg : ModuleParserConfig) (snap : ModuleParserSnapshot) (mkRes : α → Syntax × ModuleParserSnapshot) (p : ModuleParserM α) : Syntax × Except Message (ModuleParserSnapshot × MessageLog) := -let (r, _) := ((((Prod.mk <$> p <*> leftOver).run {messages:=MessageLog.Empty}).run cfg).runFrom snap.it).run {} in +let (r, _) := ((((Prod.mk <$> p <*> leftOver).run {messages:=MessageLog.empty}).run cfg).runFrom snap.it).run {} in match r with | Except.ok ((a, it), st) := let (stx, snap) := mkRes a in (stx, Except.ok ({snap with it := it}, st.messages)) | Except.error msg := (msg.custom.get, Except.error $ messageOfParsecMessage cfg msg) diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 54127b9352..7d80e65390 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 @@ -59,7 +59,7 @@ inductive Result (μ α : Type) | 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 @@ -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 @@ -279,7 +279,7 @@ 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 @@ -470,7 +470,7 @@ 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, @@ -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/tests/compiler/array_test.lean b/tests/compiler/array_test.lean index a7da88fbb0..3aa48bb9d3 100644 --- a/tests/compiler/array_test.lean +++ b/tests/compiler/array_test.lean @@ -7,7 +7,7 @@ a def main : IO UInt32 := do - let a : Array Nat := Array.nil, + let a : Array Nat := Array.empty, IO.println (toString a), IO.println (toString a.sz), let a := foo a,