From 97e5aa2411fe610c33e5e8d029932e312d6118dd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 21 Mar 2019 10:35:52 +0100 Subject: [PATCH] chore(library): s/Punit/PUnit/g etc --- library/init/control/combinators.lean | 4 +- library/init/control/estate.lean | 50 ++++++------ library/init/control/state.lean | 14 ++-- library/init/core.lean | 76 +++++++++--------- library/init/data/rbmap/basic.lean | 108 +++++++++++++------------- library/init/data/rbtree/basic.lean | 80 +++++++++---------- library/init/io.lean | 4 +- library/init/lean/elaborator.lean | 42 +++++----- library/init/lean/expander.lean | 4 +- library/init/lean/kvmap.lean | 4 +- library/init/lean/name.lean | 18 ++--- library/init/lean/parser/basic.lean | 10 +-- library/init/lean/parser/trie.lean | 14 ++-- library/init/lean/position.lean | 4 +- library/init/lean/trace.lean | 4 +- library/init/wf.lean | 14 ++-- src/library/constants.cpp | 32 ++++---- src/library/constants.txt | 32 ++++---- src/util/rb_tree.h | 1 + 19 files changed, 258 insertions(+), 257 deletions(-) diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 0f5d620a3f..ad97791a37 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -19,12 +19,12 @@ def List.mmap {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : | (h :: t) := do h' ← f h, t' ← List.mmap t, pure (h' :: t') @[specialize] -def List.mmap' {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m Punit +def List.mmap' {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit | [] := pure ⟨⟩ | (h :: t) := f h *> List.mmap' t @[specialize] -def List.mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m Punit := +def List.mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit := List.mmap' f def mjoin {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α := diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean index 58a0ec130f..da96ca03db 100644 --- a/library/init/control/estate.lean +++ b/library/init/control/estate.lean @@ -11,7 +11,7 @@ prelude import init.control.state init.control.except universes u v -namespace Estate +namespace EState inductive Result (ε σ α : Type u) | ok {} : α → σ → Result @@ -44,57 +44,57 @@ protected def Result.repr [HasRepr ε] [HasRepr α] : Result ε σ α → String instance [HasToString ε] [HasToString α] : HasToString (Result ε σ α) := ⟨Result.toString⟩ instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := ⟨Result.repr⟩ -end Estate +end EState -def Estate (ε σ α : Type u) := Estate.resultOk Punit σ Punit → Estate.Result ε σ α +def EState (ε σ α : Type u) := EState.resultOk PUnit σ PUnit → EState.Result ε σ α -namespace Estate +namespace EState variables {ε σ α β : Type u} -instance [Inhabited ε] : Inhabited (Estate ε σ α) := +instance [Inhabited ε] : Inhabited (EState ε σ α) := ⟨λ r, match r with | ⟨Result.ok _ s, _⟩ := Result.error (default ε) s | ⟨Result.error _ _, h⟩ := unreachableError h⟩ -@[inline] protected def pure (a : α) : Estate ε σ α := +@[inline] protected def pure (a : α) : EState ε σ α := λ r, match r with | ⟨Result.ok _ s, _⟩ := Result.ok a s | ⟨Result.error _ _, h⟩ := unreachableError h -@[inline] protected def put (s : σ) : Estate ε σ Punit := +@[inline] protected def put (s : σ) : EState ε σ PUnit := λ r, match r with | ⟨Result.ok _ _, _⟩ := Result.ok ⟨⟩ s | ⟨Result.error _ _, h⟩ := unreachableError h -@[inline] protected def get : Estate ε σ σ := +@[inline] protected def get : EState ε σ σ := λ r, match r with | ⟨Result.ok _ s, _⟩ := Result.ok s s | ⟨Result.error _ _, h⟩ := unreachableError h -@[inline] protected def modify (f : σ → σ) : Estate ε σ Punit := +@[inline] protected def modify (f : σ → σ) : EState ε σ PUnit := λ r, match r with | ⟨Result.ok _ s, _⟩ := Result.ok ⟨⟩ (f s) | ⟨Result.error _ _, h⟩ := unreachableError h -@[inline] protected def throw (e : ε) : Estate ε σ α := +@[inline] protected def throw (e : ε) : EState ε σ α := λ r, match r with | ⟨Result.ok _ s, _⟩ := Result.error e s | ⟨Result.error _ _, h⟩ := unreachableError h -@[inline] protected def catch (x : Estate ε σ α) (handle : ε → Estate ε σ α) : Estate ε σ α := +@[inline] protected def catch (x : EState ε σ α) (handle : ε → EState ε σ α) : EState ε σ α := λ r, match x r with | Result.error e s := handle e (resultOk.mk ⟨⟩ s) | ok := ok -@[inline] protected def orelse (x₁ x₂ : Estate ε σ α) : Estate ε σ α := +@[inline] protected def orelse (x₁ x₂ : EState ε σ α) : EState ε σ α := λ r, match x₁ r with | Result.error _ s := x₂ (resultOk.mk ⟨⟩ s) | ok := ok /-- Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orelse` uses the second. -/ -@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := true) : Estate ε σ α := +@[inline] protected def orelse' (x₁ x₂ : EState ε σ α) (useFirstEx := true) : EState ε σ α := λ r, match x₁ r with | Result.error e₁ s₁ := (match x₂ (resultOk.mk ⟨⟩ s₁) with @@ -102,31 +102,31 @@ instance [Inhabited ε] : Inhabited (Estate ε σ α) := | ok := ok) | ok := ok -@[inline] def adaptExcept {ε' : Type u} [HasLift ε ε'] (x : Estate ε σ α) : Estate ε' σ α := +@[inline] def adaptExcept {ε' : Type u} [HasLift ε ε'] (x : EState ε σ α) : EState ε' σ α := λ r, match x r with | Result.error e s := Result.error (lift e) s | Result.ok a s := Result.ok a s -@[inline] protected def bind (x : Estate ε σ α) (f : α → Estate ε σ β) : Estate ε σ β := +@[inline] protected def bind (x : EState ε σ α) (f : α → EState ε σ β) : EState ε σ β := λ r, match x r with | Result.ok a s := f a (resultOk.mk ⟨⟩ s) | Result.error e s := Result.error e s -@[inline] protected def map (f : α → β) (x : Estate ε σ α) : Estate ε σ β := +@[inline] protected def map (f : α → β) (x : EState ε σ α) : EState ε σ β := λ r, match x r with | Result.ok a s := Result.ok (f a) s | Result.error e s := Result.error e s -instance : Monad (Estate ε σ) := -{ bind := @Estate.bind _ _, pure := @Estate.pure _ _, map := @Estate.map _ _ } +instance : Monad (EState ε σ) := +{ bind := @EState.bind _ _, pure := @EState.pure _ _, map := @EState.map _ _ } -instance : HasOrelse (Estate ε σ) := -{ orelse := @Estate.orelse _ _ } +instance : HasOrelse (EState ε σ) := +{ orelse := @EState.orelse _ _ } -instance : MonadState σ (Estate ε σ) := -{ put := @Estate.put _ _, get := @Estate.get _ _, modify := @Estate.modify _ _ } +instance : MonadState σ (EState ε σ) := +{ put := @EState.put _ _, get := @EState.get _ _, modify := @EState.modify _ _ } -instance : MonadExcept ε (Estate ε σ) := -{ throw := @Estate.throw _ _, catch := @Estate.catch _ _} +instance : MonadExcept ε (EState ε σ) := +{ throw := @EState.throw _ _, catch := @EState.catch _ _} -end Estate +end EState diff --git a/library/init/control/state.lean b/library/init/control/state.lean index 8019d0bb4d..a8efbee977 100644 --- a/library/init/control/state.lean +++ b/library/init/control/state.lean @@ -52,11 +52,11 @@ section @[inline] protected def get : StateT σ m σ := λ s, pure (s, s) - @[inline] protected def put : σ → StateT σ m Punit := - λ s' s, pure (Punit.star, s') + @[inline] protected def put : σ → StateT σ m PUnit := + λ s' s, pure (PUnit.star, s') - @[inline] protected def modify (f : σ → σ) : StateT σ m Punit := - λ s, pure (Punit.star, f s) + @[inline] protected def modify (f : σ → σ) : StateT σ m PUnit := + λ s, pure (PUnit.star, f s) @[inline] protected def lift {α : Type u} (t : m α) : StateT σ m α := λ s, do a ← t, pure (a, s) @@ -86,12 +86,12 @@ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) := /- Obtain the top-most State of a Monad stack. -/ (get {} : m σ) /- Set the top-most State of a Monad stack. -/ -(put {} : σ → m Punit) +(put {} : σ → m PUnit) /- Map the top-most State of a Monad stack. Note: `modify f` may be preferable to `f <$> get >>= put` because the latter does not use the State linearly (without sufficient inlining). -/ -(modify {} : (σ → σ) → m Punit) +(modify {} : (σ → σ) → m PUnit) export MonadState (get put modify) @@ -152,7 +152,7 @@ section variables {σ σ' : Type u} {m m' : Type u → Type v} def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α := -adaptState (λ st, (toSigma st, Punit.star)) (λ st _, fromSigma st) +adaptState (λ st, (toSigma st, PUnit.star)) (λ st _, fromSigma st) export MonadStateAdapter (adaptState') instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' := diff --git a/library/init/core.lean b/library/init/core.lean index 490b6b6e4b..53baec0795 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -127,15 +127,15 @@ a issues when proving equational lemmas. The equation Compiler uses it as a marker. -/ @[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a -inductive Punit : Sort u -| star : Punit +inductive PUnit : Sort u +| star : PUnit -/-- An abbreviation for `Punit.{0}`, its most common instantiation. - This Type should be preferred over `Punit` where possible to avoid +/-- An abbreviation for `PUnit.{0}`, its most common instantiation. + This Type should be preferred over `PUnit` where possible to avoid unnecessary universe parameters. -/ -abbrev Unit : Type := Punit +abbrev Unit : Type := PUnit -@[pattern] abbrev Unit.star : Unit := Punit.star +@[pattern] abbrev Unit.star : Unit := PUnit.star /- Remark: thunks have an efficient implementation in the runtime. -/ structure Thunk (α : Type u) : Type u := @@ -219,7 +219,7 @@ structure Prod (α : Type u) (β : Type v) := /-- Similar to `Prod`, but α and β can be propositions. We use this Type internally to automatically generate the brecOn recursor. -/ -structure Pprod (α : Sort u) (β : Sort v) := +structure PProd (α : Sort u) (β : Sort v) := (fst : α) (snd : β) structure And (a b : Prop) : Prop := @@ -265,9 +265,9 @@ inductive Sum (α : Type u) (β : Type v) | inl {} (val : α) : Sum | inr {} (val : β) : Sum -inductive Psum (α : Sort u) (β : Sort v) -| inl {} (val : α) : Psum -| inr {} (val : β) : Psum +inductive PSum (α : Sort u) (β : Sort v) +| inl {} (val : α) : PSum +| inr {} (val : β) : PSum inductive Or (a b : Prop) : Prop | inl {} (h : a) : Or @@ -282,7 +282,7 @@ Or.inr hb structure Sigma {α : Type u} (β : α → Type v) := mk :: (fst : α) (snd : β fst) -structure Psigma {α : Sort u} (β : α → Sort v) := +structure PSigma {α : Sort u} (β : α → Sort v) := mk :: (fst : α) (snd : β fst) inductive Bool : Type @@ -296,7 +296,7 @@ structure Subtype {α : Sort u} (p : α → Prop) := inductive Exists {α : Sort u} (p : α → Prop) : Prop | intro (w : α) (h : p w) : Exists -attribute [ppAnonymousCtor] Sigma Psigma Subtype Pprod And +attribute [ppAnonymousCtor] Sigma PSigma Subtype PProd And class inductive Decidable (p : Prop) | isFalse (h : ¬p) : Decidable @@ -358,10 +358,10 @@ class HasAppend (α : Type u) := (append : α → α → α) class HasAndthen (α : Type u) (β : Type v) (σ : outParam $ Type w) := (andthen : α → β → σ) class HasUnion (α : Type u) := (union : α → α → α) class HasInter (α : Type u) := (inter : α → α → α) -class HasSdiff (α : Type u) := (sdiff : α → α → α) +class HasSDiff (α : Type u) := (sdiff : α → α → α) class HasEquiv (α : Sort u) := (equiv : α → α → Prop) class HasSubset (α : Type u) := (subset : α → α → Prop) -class HasSsubset (α : Type u) := (ssubset : α → α → Prop) +class HasSSubset (α : Type u) := (ssubset : α → α → Prop) /- Type classes HasEmptyc and HasInsert are used to implement polymorphic notation for collections. Example: {a, b, c}. -/ @@ -399,8 +399,8 @@ notation `∅` := HasEmptyc.emptyc _ infix ∪ := HasUnion.union infix ∩ := HasInter.inter infix ⊆ := HasSubset.subset -infix ⊂ := HasSsubset.ssubset -infix \ := HasSdiff.sdiff +infix ⊂ := HasSSubset.ssubset +infix \ := HasSDiff.sdiff infix ≈ := HasEquiv.equiv infixr ^ := HasPow.pow infixr /\ := And @@ -422,7 +422,7 @@ infix ≥ := ge infix > := gt @[reducible] def superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.subset b a -@[reducible] def ssuperset {α : Type u} [HasSsubset α] (a b : α) : Prop := HasSsubset.ssubset b a +@[reducible] def ssuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.ssubset b a infix ⊇ := superset infix ⊃ := ssuperset @@ -518,12 +518,12 @@ protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) := ⟨Sum.sizeof⟩ -protected def Psum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Psum α β) → Nat -| (Psum.inl a) := 1 + sizeof a -| (Psum.inr b) := 1 + sizeof b +protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat +| (PSum.inl a) := 1 + sizeof a +| (PSum.inr b) := 1 + sizeof b -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Psum α β) := -⟨Psum.sizeof⟩ +instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := +⟨PSum.sizeof⟩ protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat | ⟨a, b⟩ := 1 + sizeof a + sizeof b @@ -531,16 +531,16 @@ protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [ instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) := ⟨Sigma.sizeof⟩ -protected def Psigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Psigma β → Nat +protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat | ⟨a, b⟩ := 1 + sizeof a + sizeof b -instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Psigma β) := -⟨Psigma.sizeof⟩ +instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) := +⟨PSigma.sizeof⟩ -protected def Punit.sizeof : Punit → Nat +protected def PUnit.sizeof : PUnit → Nat | u := 1 -instance : HasSizeof Punit := ⟨Punit.sizeof⟩ +instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩ protected def Bool.sizeof : Bool → Nat | b := 1 @@ -1420,7 +1420,7 @@ instance : Inhabited True := ⟨trivial⟩ instance : Inhabited Nat := ⟨0⟩ -instance : Inhabited PointedType := ⟨{type := Punit, val := ⟨⟩}⟩ +instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩ class inductive nonempty (α : Sort u) : Prop | intro (val : α) : nonempty @@ -1667,7 +1667,7 @@ def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β /- Dependent products -/ notation `Σ` binders `, ` r:(scoped p, Sigma p) := r -notation `Σ'` binders `, ` r:(scoped p, Psigma p) := r +notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r theorem exOfPsig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x | ⟨x, hx⟩ := ⟨x, hx⟩ @@ -1682,25 +1682,25 @@ end section variables {α : Sort u} {β : α → Sort v} -protected theorem Psigma.Eq : ∀ {p₁ p₂ : Psigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂ +protected theorem PSigma.Eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂ | ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl end /- Universe polymorphic unit -/ -theorem punitEq (a b : Punit) : a = b := -Punit.recOn a (Punit.recOn b rfl) +theorem punitEq (a b : PUnit) : a = b := +PUnit.recOn a (PUnit.recOn b rfl) -theorem punitEqPunit (a : Punit) : a = () := +theorem punitEqPUnit (a : PUnit) : a = () := punitEq a () -instance : subsingleton Punit := +instance : subsingleton PUnit := subsingleton.intro punitEq -instance : Inhabited Punit := +instance : Inhabited PUnit := ⟨()⟩ -instance : DecidableEq Punit := +instance : DecidableEq PUnit := {decEq := λ a b, isTrue (punitEq a b)} /- Setoid -/ @@ -1800,13 +1800,13 @@ variable {β : Quot r → Sort v} local notation `⟦`:max a `⟧` := Quot.mk r a @[reducible, macroInline] -protected def indep (f : Π a, β ⟦a⟧) (a : α) : Psigma β := +protected def indep (f : Π a, β ⟦a⟧) (a : α) : PSigma β := ⟨⟦a⟧, f a⟩ protected theorem indepCoherent (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : ∀ a b, r a b → Quot.indep f a = Quot.indep f b := -λ a b e, Psigma.Eq (sound e) (h a b e) +λ a b e, PSigma.Eq (sound e) (h a b e) protected theorem liftIndepPr1 (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index ad1d79d422..b80c27bc2d 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -11,62 +11,62 @@ universes u v w w' inductive Rbcolor | red | black -inductive Rbnode (α : Type u) (β : α → Type v) -| leaf {} : Rbnode -| Node (color : Rbcolor) (lchild : Rbnode) (key : α) (val : β key) (rchild : Rbnode) : Rbnode +inductive RBNode (α : Type u) (β : α → Type v) +| leaf {} : RBNode +| Node (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode -namespace Rbnode +namespace RBNode variables {α : Type u} {β : α → Type v} {σ : Type w} open Rbcolor Nat -def depth (f : Nat → Nat → Nat) : Rbnode α β → Nat +def depth (f : Nat → Nat → Nat) : RBNode α β → Nat | leaf := 0 | (Node _ l _ _ r) := succ (f (depth l) (depth r)) -protected def min : Rbnode α β → Option (Σ k : α, β k) +protected def min : RBNode α β → Option (Σ k : α, β k) | leaf := none | (Node _ leaf k v _) := some ⟨k, v⟩ | (Node _ l k v _) := min l -protected def max : Rbnode α β → Option (Σ k : α, β k) +protected def max : RBNode α β → Option (Σ k : α, β k) | leaf := none | (Node _ _ k v leaf) := some ⟨k, v⟩ | (Node _ _ k v r) := max r -@[specialize] def fold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ +@[specialize] def fold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ | leaf b := b | (Node _ l k v r) b := fold r (f k v (fold l b)) -@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : Rbnode α β → σ → m σ +@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : RBNode α β → σ → m σ | leaf b := pure b | (Node _ l k v r) b := do b₁ ← mfold l b, b₂ ← f k v b₁, mfold r b₂ -@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ +@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ | leaf b := b | (Node _ l k v r) b := revFold l (f k v (revFold r b)) -@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool +@[specialize] def all (p : Π k : α, β k → Bool) : RBNode α β → Bool | leaf := true | (Node _ l k v r) := p k v && all l && all r -@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool +@[specialize] def any (p : Π k : α, β k → Bool) : RBNode α β → Bool | leaf := false | (Node _ l k v r) := p k v || any l || any r -def balance1 : Rbnode α β → Rbnode α β → Rbnode α β +def balance1 : RBNode α β → RBNode α β → RBNode α β | (Node _ _ kv vv t) (Node _ (Node red l kx vx r₁) ky vy r₂) := Node red (Node black l kx vx r₁) ky vy (Node black r₂ kv vv t) | (Node _ _ kv vv t) (Node _ l₁ ky vy (Node red l₂ kx vx r)) := Node red (Node black l₁ ky vy l₂) kx vx (Node black r kv vv t) | (Node _ _ kv vv t) (Node _ l ky vy r) := Node black (Node red l ky vy r) kv vv t | _ _ := leaf -- unreachable -def balance2 : Rbnode α β → Rbnode α β → Rbnode α β +def balance2 : RBNode α β → RBNode α β → RBNode α β | (Node _ t kv vv _) (Node _ (Node red l kx₁ vx₁ r₁) ky vy r₂) := Node red (Node black t kv vv l) kx₁ vx₁ (Node black r₁ ky vy r₂) | (Node _ t kv vv _) (Node _ l₁ ky vy (Node red l₂ kx₂ vx₂ r₂)) := Node red (Node black t kv vv l₁) ky vy (Node black l₂ kx₂ vx₂ r₂) | (Node _ t kv vv _) (Node _ l ky vy r) := Node black t kv vv (Node red l ky vy r) | _ _ := leaf -- unreachable -def isRed : Rbnode α β → Bool +def isRed : RBNode α β → Bool | (Node red _ _ _ _) := true | _ := false @@ -74,7 +74,7 @@ section insert variables (lt : α → α → Prop) [DecidableRel lt] -def ins : Rbnode α β → Π k : α, β k → Rbnode α β +def ins : RBNode α β → Π k : α, β k → RBNode α β | leaf kx vx := Node red leaf kx vx leaf | (Node red a ky vy b) kx vx := (match cmpUsing lt kx ky with @@ -91,11 +91,11 @@ def ins : Rbnode α β → Π k : α, β k → Rbnode α β if isRed b then balance2 (Node black a ky vy leaf) (ins b kx vx) else Node black a ky vy (ins b kx vx) -def setBlack : Rbnode α β → Rbnode α β +def setBlack : RBNode α β → RBNode α β | (Node _ l k v r) := Node black l k v r | e := e -def insert (t : Rbnode α β) (k : α) (v : β k) : Rbnode α β := +def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β := if isRed t then setBlack (ins lt t k v) else ins lt t k v @@ -106,7 +106,7 @@ variable (lt : α → α → Prop) variable [DecidableRel lt] -def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k) +def findCore : RBNode α β → Π k : α, Option (Σ k : α, β k) | leaf x := none | (Node _ a ky vy b) x := (match cmpUsing lt x ky with @@ -114,7 +114,7 @@ def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k) | Ordering.Eq := some ⟨ky, vy⟩ | Ordering.gt := findCore b x) -def find {β : Type v} : Rbnode α (λ _, β) → α → Option β +def find {β : Type v} : RBNode α (λ _, β) → α → Option β | leaf x := none | (Node _ a ky vy b) x := (match cmpUsing lt x ky with @@ -122,7 +122,7 @@ def find {β : Type v} : Rbnode α (λ _, β) → α → Option β | Ordering.Eq := some vy | Ordering.gt := find b x) -def lowerBound : Rbnode α β → α → Option (Sigma β) → Option (Sigma β) +def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β) | leaf x lb := lb | (Node _ a ky vy b) x lb := (match cmpUsing lt x ky with @@ -132,95 +132,95 @@ def lowerBound : Rbnode α β → α → Option (Sigma β) → Option (Sigma β) end membership -inductive WellFormed (lt : α → α → Prop) : Rbnode α β → Prop +inductive WellFormed (lt : α → α → Prop) : RBNode α β → Prop | leafWff : WellFormed leaf -| insertWff {n n' : Rbnode α β} {k : α} {v : β k} [DecidableRel lt] : WellFormed n → n' = insert lt n k v → WellFormed n' +| insertWff {n n' : RBNode α β} {k : α} {v : β k} [DecidableRel lt] : WellFormed n → n' = insert lt n k v → WellFormed n' -end Rbnode +end RBNode -open Rbnode +open RBNode -/- TODO(Leo): define dRbmap -/ +/- TODO(Leo): define dRBMap -/ -def Rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) := -{t : Rbnode α (λ _, β) // t.WellFormed lt } +def RBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) := +{t : RBNode α (λ _, β) // t.WellFormed lt } -@[inline] def mkRbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Rbmap α β lt := +@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : RBMap α β lt := ⟨leaf, WellFormed.leafWff lt⟩ -namespace Rbmap +namespace RBMap variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Prop} -def depth (f : Nat → Nat → Nat) (t : Rbmap α β lt) : Nat := +def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat := t.val.depth f -@[inline] def fold (f : α → β → σ → σ) : Rbmap α β lt → σ → σ +@[inline] def fold (f : α → β → σ → σ) : RBMap α β lt → σ → σ | ⟨t, _⟩ b := t.fold f b -@[inline] def revFold (f : α → β → σ → σ) : Rbmap α β lt → σ → σ +@[inline] def revFold (f : α → β → σ → σ) : RBMap α β lt → σ → σ | ⟨t, _⟩ b := t.revFold f b -@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : α → β → σ → m σ) : Rbmap α β lt → σ → m σ +@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : α → β → σ → m σ) : RBMap α β lt → σ → m σ | ⟨t, _⟩ b := t.mfold f b -@[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : Rbmap α β lt) : m Punit := +@[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 -@[specialize] def toList : Rbmap α β lt → List (α × β) +@[specialize] def toList : RBMap α β lt → List (α × β) | ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) [] -@[inline] protected def min : Rbmap α β lt → Option (α × β) +@[inline] protected def min : RBMap α β lt → Option (α × β) | ⟨t, _⟩ := match t.min with | some ⟨k, v⟩ := some (k, v) | none := none -@[inline] protected def max : Rbmap α β lt → Option (α × β) +@[inline] protected def max : RBMap α β lt → Option (α × β) | ⟨t, _⟩ := match t.max with | some ⟨k, v⟩ := some (k, v) | none := none -instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) := +instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := ⟨λ t, "rbmapOf " ++ repr t.toList⟩ variables [DecidableRel lt] -def insert : Rbmap α β lt → α → β → Rbmap α β lt +def insert : RBMap α β lt → α → β → RBMap α β lt | ⟨t, w⟩ k v := ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩ -@[specialize] def ofList : List (α × β) → Rbmap α β lt -| [] := mkRbmap _ _ _ +@[specialize] def ofList : List (α × β) → RBMap α β lt +| [] := mkRBMap _ _ _ | (⟨k,v⟩::xs) := (ofList xs).insert k v -def findCore : Rbmap α β lt → α → Option (Σ k : α, β) +def findCore : RBMap α β lt → α → Option (Σ k : α, β) | ⟨t, _⟩ x := t.findCore lt x -def find : Rbmap α β lt → α → Option β +def find : RBMap α β lt → α → Option β | ⟨t, _⟩ x := t.find lt x /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`, if it exists. -/ -def lowerBound : Rbmap α β lt → α → Option (Σ k : α, β) +def lowerBound : RBMap α β lt → α → Option (Σ k : α, β) | ⟨t, _⟩ x := t.lowerBound lt x none -@[inline] def contains (t : Rbmap α β lt) (a : α) : Bool := +@[inline] def contains (t : RBMap α β lt) (a : α) : Bool := (t.find a).isSome -def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt := -l.foldl (λ r p, r.insert p.1 p.2) (mkRbmap α β lt) +def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt := +l.foldl (λ r p, r.insert p.1 p.2) (mkRBMap α β lt) -@[inline] def all : Rbmap α β lt → (α → β → Bool) → Bool +@[inline] def all : RBMap α β lt → (α → β → Bool) → Bool | ⟨t, _⟩ p := t.all p -@[inline] def any : Rbmap α β lt → (α → β → Bool) → Bool +@[inline] def any : RBMap α β lt → (α → β → Bool) → Bool | ⟨t, _⟩ p := t.any p -end Rbmap +end RBMap -def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt := -Rbmap.fromList l lt +def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt := +RBMap.fromList l lt diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 651835c4cd..5b45d2fda4 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -7,82 +7,82 @@ prelude import init.data.rbmap.basic universes u v w -def Rbtree (α : Type u) (lt : α → α → Prop) : Type u := -Rbmap α Unit lt +def RBTree (α : Type u) (lt : α → α → Prop) : Type u := +RBMap α Unit lt -@[inline] def mkRbtree (α : Type u) (lt : α → α → Prop) : Rbtree α lt := -mkRbmap α Unit lt +@[inline] def mkRBTree (α : Type u) (lt : α → α → Prop) : RBTree α lt := +mkRBMap α Unit lt -namespace Rbtree +namespace RBTree variables {α : Type u} {β : Type v} {lt : α → α → Prop} -@[inline] def depth (f : Nat → Nat → Nat) (t : Rbtree α lt) : Nat := -Rbmap.depth f t +@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat := +RBMap.depth f t -@[inline] def fold (f : α → β → β) (t : Rbtree α lt) (b : β) : β := -Rbmap.fold (λ a _ r, f a r) t b +@[inline] def fold (f : α → β → β) (t : RBTree α lt) (b : β) : β := +RBMap.fold (λ a _ r, f a r) t b -@[inline] def revFold (f : α → β → β) (t : Rbtree α lt) (b : β) : β := -Rbmap.revFold (λ a _ r, f a r) t b +@[inline] def revFold (f : α → β → β) (t : RBTree α lt) (b : β) : β := +RBMap.revFold (λ a _ r, f a r) t b -@[inline] def mfold {m : Type v → Type w} [Monad m] (f : α → β → m β) (t : Rbtree α lt) (b : β) : m β := -Rbmap.mfold (λ a _ r, f a r) t b +@[inline] def mfold {m : Type v → Type w} [Monad m] (f : α → β → m β) (t : RBTree α lt) (b : β) : m β := +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 := +@[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 α := +@[specialize] def toList (t : RBTree α lt) : List α := t.revFold (::) [] -@[inline] protected def min (t : Rbtree α lt) : Option α := -match Rbmap.min t with +@[inline] protected def min (t : RBTree α lt) : Option α := +match RBMap.min t with | some ⟨a, _⟩ := some a | none := none -@[inline] protected def max (t : Rbtree α lt) : Option α := -match Rbmap.max t with +@[inline] protected def max (t : RBTree α lt) : Option α := +match RBMap.max t with | some ⟨a, _⟩ := some a | none := none -instance [HasRepr α] : HasRepr (Rbtree α lt) := +instance [HasRepr α] : HasRepr (RBTree α lt) := ⟨λ t, "rbtreeOf " ++ repr t.toList⟩ variables [DecidableRel lt] -@[inline] def insert (t : Rbtree α lt) (a : α) : Rbtree α lt := -Rbmap.insert t a () +@[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt := +RBMap.insert t a () -@[specialize] def ofList : List α → Rbtree α lt -| [] := mkRbtree _ _ +@[specialize] def ofList : List α → RBTree α lt +| [] := mkRBTree _ _ | (x::xs) := (ofList xs).insert x -def find (t : Rbtree α lt) (a : α) : Option α := -match Rbmap.findCore t a with +def find (t : RBTree α lt) (a : α) : Option α := +match RBMap.findCore t a with | some ⟨a, _⟩ := some a | none := none -@[inline] def contains (t : Rbtree α lt) (a : α) : Bool := +@[inline] def contains (t : RBTree α lt) (a : α) : Bool := (t.find a).isSome -def fromList (l : List α) (lt : α → α → Prop) [DecidableRel lt] : Rbtree α lt := -l.foldl insert (mkRbtree α lt) +def fromList (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt := +l.foldl insert (mkRBTree α lt) -@[inline] def all (t : Rbtree α lt) (p : α → Bool) : Bool := -Rbmap.all t (λ a _, p a) +@[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool := +RBMap.all t (λ a _, p a) -@[inline] def any (t : Rbtree α lt) (p : α → Bool) : Bool := -Rbmap.any t (λ a _, p a) +@[inline] def any (t : RBTree α lt) (p : α → Bool) : Bool := +RBMap.any t (λ a _, p a) -def subset (t₁ t₂ : Rbtree α lt) : Bool := +def subset (t₁ t₂ : RBTree α lt) : Bool := t₁.all $ λ a, (t₂.find a).toBool -def seteq (t₁ t₂ : Rbtree α lt) : Bool := +def seteq (t₁ t₂ : RBTree α lt) : Bool := subset t₁ t₂ && subset t₂ t₁ -end Rbtree +end RBTree -def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Prop) [DecidableRel lt] : Rbtree α lt := -Rbtree.fromList l lt +def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt := +RBTree.fromList l lt diff --git a/library/init/io.lean b/library/init/io.lean index 3b9f6ca3ca..312d157c90 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -18,10 +18,10 @@ constant IO.RealWorld : Type := Unit ``` -/ @[derive Monad MonadExcept] -def EIO (ε : Type) : Type → Type := Estate ε IO.RealWorld +def EIO (ε : Type) : Type → Type := EState ε IO.RealWorld instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) := -inferInstanceAs (Inhabited (Estate ε IO.RealWorld α)) +inferInstanceAs (Inhabited (EState ε IO.RealWorld α)) /- In the future, we may want to give more concrete data diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index ddb7d9cb27..409d6e1609 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -57,26 +57,26 @@ open Expander local attribute [instance] Name.hasLtQuick -- TODO(Sebastian): move -/-- An Rbmap that remembers the insertion order. -/ -structure OrderedRbmap (α β : Type) (lt : α → α → Prop) := +/-- An RBMap that remembers the insertion order. -/ +structure OrderedRBMap (α β : Type) (lt : α → α → Prop) := (entries : List (α × β)) -(map : Rbmap α (Nat × β) lt) +(map : RBMap α (Nat × β) lt) (size : Nat) -namespace OrderedRbmap -variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRbmap α β lt) +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 := +def insert (k : α) (v : β) : OrderedRBMap α β lt := {entries := (k, v)::m.entries, map := m.map.insert k (m.size, v), size := m.size + 1} 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 -end OrderedRbmap +def ofList (l : List (α × β)) : OrderedRBMap α β lt := +l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.Empty +end OrderedRBMap structure ElaboratorConfig extends FrontendConfig := (initialParserCfg : ModuleParserConfig) @@ -93,11 +93,11 @@ 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 _ _) +(includeVars : RBTree Name (<) := mkRBTree _ _) /- The stack of nested active `namespace` commands. -/ (nsStack : List Name := []) /- The set of active `open` declarations. -/ @@ -364,9 +364,9 @@ do cfg ← read, ..st}, match st' with | some st' := do modifyCurrentScope $ λ sc, {sc with - univs := OrderedRbmap.ofList st'.univs, - vars := OrderedRbmap.ofList st'.vars, - includeVars := Rbtree.ofList st'.includeVars, + univs := OrderedRBMap.ofList st'.univs, + vars := OrderedRBMap.ofList st'.vars, + includeVars := RBTree.ofList st'.includeVars, Options := st'.Options, }, modify $ λ st, {..st', ..st} @@ -423,7 +423,7 @@ match dl with match dl.oldUnivParams with | some uparams := modifyCurrentScope $ λ sc, {sc with univs := - (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs} + (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs} | none := pure (), -- do we actually need this?? let uparams := namesToPexpr $ match dl.oldUnivParams with @@ -500,7 +500,7 @@ def Declaration.elaborate : Elaborator := match ind.oldUnivParams with | some uparams := modifyCurrentScope $ λ sc, {sc with univs := - (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs} + (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs} | none := pure (), let uparams := namesToPexpr $ match ind.oldUnivParams with | some uparams := uparams.ids.map mangleIdent @@ -531,7 +531,7 @@ def Declaration.elaborate : Elaborator := match s.oldUnivParams with | some uparams := modifyCurrentScope $ λ sc, {sc with univs := - (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs} + (uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs} | none := pure (), let uparams := namesToPexpr $ match s.oldUnivParams with | some uparams := uparams.ids.map mangleIdent @@ -600,7 +600,7 @@ def include.elaborate : Elaborator := modifyCurrentScope $ λ sc, {sc with includeVars := v.ids.foldl (λ vars v, vars.insert $ mangleIdent v) sc.includeVars} --- TODO: Rbmap.remove +-- TODO: RBMap.remove /- def omit.elaborate : Elaborator := λ stx, do @@ -893,7 +893,7 @@ def eoi.elaborate : Elaborator := error cmd "invalid end of input, expected 'end'" -- TODO(Sebastian): replace with attribute -def elaborators : Rbmap Name Elaborator (<) := Rbmap.fromList [ +def elaborators : RBMap Name Elaborator (<) := RBMap.fromList [ (Module.header.name, Module.header.elaborate), (notation.name, notation.elaborate), (reserveNotation.name, reserveNotation.elaborate), diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index c337547597..36a72e45d2 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -471,7 +471,7 @@ def sorry.transform : transformer := local attribute [instance] Name.hasLtQuick -- TODO(Sebastian): replace with attribute -def builtinTransformers : Rbmap Name transformer (<) := Rbmap.fromList [ +def builtinTransformers : RBMap Name transformer (<) := RBMap.fromList [ (mixfix.name, mixfix.transform), (reserveMixfix.name, reserveMixfix.transform), (bracketedBinders.name, bracketedBinders.transform), @@ -497,7 +497,7 @@ structure ExpanderState := (nextScope : MacroScope) structure ExpanderConfig extends TransformerConfig := -(transformers : Rbmap Name transformer (<)) +(transformers : RBMap Name transformer (<)) instance ExpanderConfig.HasLift : HasLift ExpanderConfig TransformerConfig := ⟨ExpanderConfig.toTransformerConfig⟩ diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index c128ff5489..ddd12253de 100644 --- a/library/init/lean/kvmap.lean +++ b/library/init/lean/kvmap.lean @@ -22,8 +22,8 @@ def DataValue.beq : DataValue → DataValue → Bool instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩ -/- Remark: we do not use Rbmap here because we need to manipulate Kvmap objects in - C++ and Rbmap is implemented in Lean. So, we use just a List until we can +/- Remark: we do not use RBMap here because we need to manipulate Kvmap objects in + C++ and RBMap is implemented in Lean. So, we use just a List until we can generate C++ code from Lean code. -/ structure Kvmap := (entries : List (Name × DataValue) := []) diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index efad80aa38..c352d93cec 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -157,27 +157,27 @@ end Name section local attribute [instance] Name.hasLtQuick -def NameMap (α : Type) := Rbmap Name α (<) +def NameMap (α : Type) := RBMap Name α (<) variable {α : Type} @[inline] def mkNameMap : NameMap α := -mkRbmap Name α (<) +mkRBMap Name α (<) def NameMap.insert (m : NameMap α) (n : Name) (a : α) := -Rbmap.insert m n a +RBMap.insert m n a def NameMap.contains (m : NameMap α) (n : Name) : Bool := -Rbmap.contains m n +RBMap.contains m n @[inline] def NameMap.find (m : NameMap α) (n : Name) : Option α := -Rbmap.find m n +RBMap.find m n end section local attribute [instance] Name.hasLtQuick -def NameSet := Rbtree Name (<) +def NameSet := RBTree Name (<) @[inline] def mkNameSet : NameSet := -mkRbtree Name (<) +mkRBTree Name (<) def NameSet.insert (s : NameSet) (n : Name) := -Rbtree.insert s n +RBTree.insert s n def NameSet.contains (s : NameSet) (n : Name) : Bool := -Rbmap.contains s n +RBMap.contains s n end end Lean diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 6f0ef59d7f..9d0edd9062 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -84,7 +84,7 @@ local attribute [reducible] BasicParserM ParserT parserCoreT @[inline] def getCache : BasicParserM ParserCache := monadLift (get : StateT ParserCache id _) -@[inline] def putCache : ParserCache → BasicParserM Punit := +@[inline] def putCache : ParserCache → BasicParserM PUnit := λ c, monadLift (put c : StateT ParserCache id _) end @@ -192,7 +192,7 @@ instance trailingTermParserCoe : HasCoe termParser trailingTermParser := local attribute [instance] Name.hasLtQuick /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/ -def TokenMap (α : Type) := Rbmap Name (List α) (<) +def TokenMap (α : Type) := RBMap Name (List α) (<) def TokenMap.insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α := match map.find k with @@ -200,7 +200,7 @@ match map.find k with | some vs := map.insert k (v::vs) def TokenMap.ofList {α : Type} : List (Name × α) → TokenMap α -| [] := mkRbmap _ _ _ +| [] := mkRBMap _ _ _ | (⟨k,v⟩::xs) := (TokenMap.ofList xs).insert k v instance tokenMapNil.tokens : Parser.HasTokens $ @TokenMap.ofList ρ [] := @@ -215,8 +215,8 @@ structure CommandParserConfig extends ParserConfig := (leadingTermParsers : TokenMap termParser) (trailingTermParsers : TokenMap trailingTermParser) -- local Term parsers (such as from `local notation`) hide previous parsers instead of overloading them -(localLeadingTermParsers : TokenMap termParser := mkRbmap _ _ _) -(localTrailingTermParsers : TokenMap trailingTermParser := mkRbmap _ _ _) +(localLeadingTermParsers : TokenMap termParser := mkRBMap _ _ _) +(localTrailingTermParsers : TokenMap trailingTermParser := mkRBMap _ _ _) instance commandParserConfigCoeParserConfig : HasCoe CommandParserConfig ParserConfig := ⟨CommandParserConfig.toParserConfig⟩ diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 9578ae51be..f05d431953 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -13,19 +13,19 @@ namespace Lean namespace Parser inductive Trie (α : Type) -| Node : Option α → Rbnode Char (λ _, Trie) → Trie +| Node : Option α → RBNode Char (λ _, Trie) → Trie namespace Trie variables {α : Type} protected def mk : Trie α := -⟨none, Rbnode.leaf⟩ +⟨none, RBNode.leaf⟩ private def insertAux (val : α) : Nat → Trie α → String.Iterator → Trie α | 0 (Trie.Node _ map) _ := Trie.Node (some val) map -- NOTE: overrides old value | (n+1) (Trie.Node val map) it := - let t' := (Rbnode.find (<) map it.curr).getOrElse Trie.mk in - Trie.Node val (Rbnode.insert (<) map it.curr (insertAux n t' it.next)) + let t' := (RBNode.find (<) map it.curr).getOrElse Trie.mk in + Trie.Node val (RBNode.insert (<) map it.curr (insertAux n t' it.next)) def insert (t : Trie α) (s : String) (val : α) : Trie α := insertAux val s.length t s.mkIterator @@ -33,7 +33,7 @@ insertAux val s.length t s.mkIterator private def findAux : Nat → Trie α → String.Iterator → Option α | 0 (Trie.Node val _) _ := val | (n+1) (Trie.Node val map) it := do - t' ← Rbnode.find (<) map it.curr, + t' ← RBNode.find (<) map it.curr, findAux n t' it.next def find (t : Trie α) (s : String) : Option α := @@ -43,7 +43,7 @@ private def matchPrefixAux : Nat → Trie α → String.Iterator → Option (Str | 0 (Trie.Node val map) it Acc := Prod.mk it <$> val <|> Acc | (n+1) (Trie.Node val map) it Acc := let Acc' := Prod.mk it <$> val <|> Acc in - match Rbnode.find (<) map it.curr with + match RBNode.find (<) map it.curr with | some t := matchPrefixAux n t it.next Acc' | none := Acc' @@ -51,7 +51,7 @@ def matchPrefix {α : Type} (t : Trie α) (it : String.Iterator) : Option (Strin matchPrefixAux it.remaining t it none private def toStringAux {α : Type} : Trie α → List Format -| (Trie.Node val map) := flip Rbnode.fold map (λ c t Fs, +| (Trie.Node val map) := flip RBNode.fold map (λ c t Fs, toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] instance {α : Type} : HasToString (Trie α) := diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean index d4c8589b97..3af3dff346 100644 --- a/library/init/lean/position.lean +++ b/library/init/lean/position.lean @@ -37,7 +37,7 @@ end Position /-- A precomputed cache for quickly mapping Char offsets to positionitions. -/ structure FileMap := -- A mapping from Char offset of line start to line index -(lines : Rbmap Nat Nat (<)) +(lines : RBMap Nat Nat (<)) namespace FileMap private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat) @@ -49,7 +49,7 @@ private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat | other := fromStringAux k it.next line def fromString (s : String) : FileMap := -{lines := Rbmap.ofList $ fromStringAux s.length s.mkIterator 1} +{lines := RBMap.ofList $ fromStringAux s.length s.mkIterator 1} def toPosition (m : FileMap) (off : Nat) : Position := match m.lines.lowerBound off with diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 14b4462002..ba2e864ac9 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -25,7 +25,7 @@ fmt ++ Format.nest 2 (Format.join $ subtraces.map (λ t, Format.line ++ t.pp)) namespace Trace -def TraceMap := Rbmap Position Trace (<) +def TraceMap := RBMap Position Trace (<) structure TraceState := (opts : Options) @@ -77,7 +77,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) := } unsafe def TraceT.run {m α} [Monad m] (opts : Options) (x : TraceT m α) : m (α × TraceMap) := -do (a, st) ← StateT.run x {opts := opts, roots := mkRbmap _ _ _, curPos := none, curTraces := []}, +do (a, st) ← StateT.run x {opts := opts, roots := mkRBMap _ _ _, curPos := none, curTraces := []}, pure (a, st.roots) end Trace diff --git a/library/init/wf.lean b/library/init/wf.lean index d3c369bf3b..ba53adb053 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -203,14 +203,14 @@ instance HasWellFounded {α : Type u} {β : Type v} [s₁ : HasWellFounded α] [ end Prod -namespace Psigma +namespace PSigma section variables {α : Sort u} {β : α → Sort v} variable (r : α → α → Prop) variable (s : ∀ a, β a → β a → Prop) -- Lexicographical order based on r and s -inductive Lex : Psigma β → Psigma β → Prop +inductive Lex : PSigma β → PSigma β → Prop | left : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → Lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ | right : ∀ (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → Lex ⟨a, b₁⟩ ⟨a, b₂⟩ end @@ -229,7 +229,7 @@ Acc.ndrecOn aca (ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩), Acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), have aux : xa = xa → xb ≅ xb → Acc (Lex r s) p, from - @Psigma.Lex.recOn α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → Acc (Lex r s) p₁) + @PSigma.Lex.recOn α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → Acc (Lex r s) p₁) p ⟨xa, xb⟩ lt (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ ≅ xb), have aux : (∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩) → @@ -269,7 +269,7 @@ section variables {α : Sort u} {β : Sort v} -- Reverse lexicographical order based on r and s -inductive RevLex (r : α → α → Prop) (s : β → β → Prop) : @Psigma α (λ a, β) → @Psigma α (λ a, β) → Prop +inductive RevLex (r : α → α → Prop) (s : β → β → Prop) : @PSigma α (λ a, β) → @PSigma α (λ a, β) → Prop | left : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → RevLex ⟨a₁, b⟩ ⟨a₂, b⟩ | right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → RevLex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ end @@ -305,7 +305,7 @@ WellFounded.intro $ λ ⟨a, b⟩, revLexAccessible (apply hb b) (WellFounded.ap end section -def skipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @Psigma α (λ a, β) → @Psigma α (λ a, β) → Prop := +def skipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (λ a, β) → @PSigma α (λ a, β) → Prop := RevLex emptyRelation s def skipLeftWf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) : WellFounded (skipLeft α s) := @@ -316,10 +316,10 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P RevLex.right _ _ _ h end -instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (Psigma β) := +instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (PSigma β) := {r := Lex s₁.r (λ a, (s₂ a).r), wf := lexWf s₁.wf (λ a, (s₂ a).wf)} -end Psigma +end PSigma /- Temporary hack for bootstrapping Lean. TODO: DELETE!!!! diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 606fd7295e..2e7d55a703 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -495,14 +495,14 @@ void initialize_constants() { g_out_param = new name{"outParam"}; g_pexpr = new name{"pexpr"}; g_pexpr_subst = new name{"pexpr", "subst"}; - g_punit = new name{"Punit"}; - g_punit_cases_on = new name{"Punit", "casesOn"}; - g_punit_star = new name{"Punit", "star"}; + g_punit = new name{"PUnit"}; + g_punit_cases_on = new name{"PUnit", "casesOn"}; + g_punit_star = new name{"PUnit", "star"}; g_prod_mk = new name{"Prod", "mk"}; - g_pprod = new name{"Pprod"}; - g_pprod_mk = new name{"Pprod", "mk"}; - g_pprod_fst = new name{"Pprod", "fst"}; - g_pprod_snd = new name{"Pprod", "snd"}; + g_pprod = new name{"PProd"}; + g_pprod_mk = new name{"PProd", "mk"}; + g_pprod_fst = new name{"PProd", "fst"}; + g_pprod_snd = new name{"PProd", "snd"}; g_propext = new name{"propext"}; g_to_pexpr = new name{"toPexpr"}; g_quot_mk = new name{"Quot", "mk"}; @@ -513,11 +513,11 @@ void initialize_constants() { g_rfl = new name{"rfl"}; g_scope_trace = new name{"scopeTrace"}; g_set_of = new name{"setOf"}; - g_psigma = new name{"Psigma"}; - g_psigma_cases_on = new name{"Psigma", "casesOn"}; - g_psigma_mk = new name{"Psigma", "mk"}; - g_psigma_fst = new name{"Psigma", "fst"}; - g_psigma_snd = new name{"Psigma", "snd"}; + g_psigma = new name{"PSigma"}; + g_psigma_cases_on = new name{"PSigma", "casesOn"}; + g_psigma_mk = new name{"PSigma", "mk"}; + g_psigma_fst = new name{"PSigma", "fst"}; + g_psigma_snd = new name{"PSigma", "snd"}; g_singleton = new name{"singleton"}; g_sizeof = new name{"sizeof"}; g_sorry_ax = new name{"sorryAx"}; @@ -537,10 +537,10 @@ void initialize_constants() { g_subtype_mk = new name{"Subtype", "mk"}; g_subtype_val = new name{"Subtype", "val"}; g_subtype_rec = new name{"Subtype", "rec"}; - g_psum = new name{"Psum"}; - g_psum_cases_on = new name{"Psum", "casesOn"}; - g_psum_inl = new name{"Psum", "inl"}; - g_psum_inr = new name{"Psum", "inr"}; + g_psum = new name{"PSum"}; + g_psum_cases_on = new name{"PSum", "casesOn"}; + g_psum_inl = new name{"PSum", "inl"}; + g_psum_inr = new name{"PSum", "inr"}; g_tactic = new name{"tactic"}; g_tactic_try = new name{"tactic", "try"}; g_tactic_triv = new name{"tactic", "triv"}; diff --git a/src/library/constants.txt b/src/library/constants.txt index 9b8013c5a5..17f4ce2373 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -206,14 +206,14 @@ Or outParam pexpr pexpr.subst -Punit -Punit.casesOn -Punit.star +PUnit +PUnit.casesOn +PUnit.star Prod.mk -Pprod -Pprod.mk -Pprod.fst -Pprod.snd +PProd +PProd.mk +PProd.fst +PProd.snd propext toPexpr Quot.mk @@ -224,11 +224,11 @@ repr rfl scopeTrace setOf -Psigma -Psigma.casesOn -Psigma.mk -Psigma.fst -Psigma.snd +PSigma +PSigma.casesOn +PSigma.mk +PSigma.fst +PSigma.snd singleton sizeof sorryAx @@ -248,10 +248,10 @@ Subtype Subtype.mk Subtype.val Subtype.rec -Psum -Psum.casesOn -Psum.inl -Psum.inr +PSum +PSum.casesOn +PSum.inl +PSum.inr tactic tactic.try tactic.triv diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h index a6da3a8982..bc380d583d 100644 --- a/src/util/rb_tree.h +++ b/src/util/rb_tree.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#pragma clang diagnostic ignored "-Wreturn-std-move" #include #include #include "runtime/optional.h"