From 295cabed2e3f930d893849aa3af9fb561e71cb5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Jul 2019 10:27:16 -0700 Subject: [PATCH] chore(library/init): remove unnecessary notations --- library/init/core.lean | 53 ++------------------- library/init/data/list/basic.lean | 3 -- library/init/data/rbtree/basic.lean | 5 +- library/init/data/repr.lean | 2 +- library/init/data/tostring.lean | 2 +- library/init/lean/compiler/ir/basic.lean | 3 ++ library/init/lean/compiler/ir/livevars.lean | 3 ++ library/init/lean/compiler/ir/pushproj.lean | 2 +- library/init/lean/compiler/ir/rc.lean | 2 +- library/init/lean/parser/term.lean | 3 +- 10 files changed, 18 insertions(+), 60 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 01a7173b3a..be2469ba62 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -13,7 +13,6 @@ notation f ` $ `:1 a:0 := f a /- Logical operations and relations -/ reserve prefix `¬`:40 -reserve prefix `~`:40 reserve infixr ` ∧ `:35 reserve infixr ` /\ `:35 reserve infixr ` \/ `:30 @@ -27,15 +26,10 @@ reserve infix ` ~= `:50 reserve infix ` ≅ `:50 reserve infix ` ≠ `:50 reserve infix ` ≈ `:50 -reserve infix ` ~ `:50 -reserve infix ` ≡ `:50 -reserve infixl ` ⬝ `:75 reserve infixr ` ▸ `:75 -reserve infixr ` ▹ `:75 /- types and Type constructors -/ -reserve infixr ` ⊕ `:30 reserve infixr ` × `:35 /- arithmetic operations -/ @@ -68,17 +62,9 @@ reserve infixl ` || `:30 reserve infix ` ∈ `:50 reserve infix ` ∉ `:50 -reserve infixl ` ∩ `:70 -reserve infixl ` ∪ `:65 -reserve infix ` ⊆ `:50 -reserve infix ` ⊇ `:50 -reserve infix ` ⊂ `:50 -reserve infix ` ⊃ `:50 -reserve infix ` \ `:70 /- other symbols -/ -reserve infix ` ∣ `:50 reserve infixl ` ++ `:65 reserve infixr ` :: `:67 @@ -354,7 +340,6 @@ class HasMul (α : Type u) := (mul : α → α → α) class HasNeg (α : Type u) := (neg : α → α) class HasSub (α : Type u) := (sub : α → α → α) class HasDiv (α : Type u) := (div : α → α → α) -class HasDivides (α : Type u) := (Divides : α → α → Prop) class HasMod (α : Type u) := (mod : α → α → α) class HasModn (α : Type u) := (modn : α → Nat → α) class HasLessEq (α : Type u) := (LessEq : α → α → Prop) @@ -363,20 +348,8 @@ class HasBeq (α : Type u) := (beq : α → α → Bool) class HasAppend (α : Type u) := (append : α → α → α) class HasOrelse (α : Type u) := (orelse : α → α → α) class HasAndthen (α : Type u) := (andthen : α → α → α) -class HasUnion (α : Type u) := (union : α → α → α) -class HasInter (α : Type u) := (inter : α → α → α) -class HasSDiff (α : Type u) := (sdiff : α → α → α) class HasEquiv (α : Sort u) := (Equiv : α → α → Prop) -class HasSubset (α : Type u) := (Subset : α → α → Prop) -class HasSSubset (α : Type u) := (SSubset : α → α → Prop) -/- Type classes HasEmptyc and HasInsert are - used to implement polymorphic notation for collections. - Example: {a, b, c}. -/ class HasEmptyc (α : Type u) := (emptyc : α) -class HasInsert (α : outParam $ Type u) (γ : Type v) := (insert : α → γ → γ) -/- Type class used to implement the notation { a ∈ c | p a } -/ -class HasSep (α : outParam $ Type u) (γ : Type v) := -(sep : (α → Prop) → γ → γ) /- Type class for set-like membership -/ class HasMem (α : outParam $ Type u) (γ : Type v) := (mem : α → γ → Prop) @@ -392,7 +365,6 @@ infix + := HasAdd.add infix * := HasMul.mul infix - := HasSub.sub infix / := HasDiv.div -infix ∣ := HasDivides.Divides infix % := HasMod.mod infix %ₙ := HasModn.modn prefix - := HasNeg.neg @@ -402,11 +374,6 @@ infix < := HasLess.Less infix == := HasBeq.beq infix ++ := HasAppend.append notation `∅` := HasEmptyc.emptyc _ -infix ∪ := HasUnion.union -infix ∩ := HasInter.inter -infix ⊆ := HasSubset.Subset -infix ⊂ := HasSSubset.SSubset -infix \ := HasSDiff.sdiff infix ≈ := HasEquiv.Equiv infixr ^ := HasPow.pow infixr /\ := And @@ -429,23 +396,11 @@ infix >= := GreaterEq infix ≥ := GreaterEq infix > := Greater -@[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 - -infix ⊇ := Superset -infix ⊃ := SSuperset - @[inline] def bit0 {α : Type u} [s : HasAdd α] (a : α) : α := a + a @[inline] def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α := (bit0 a) + 1 attribute [matchPattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg -export HasInsert (insert) - -/- The Empty collection -/ -@[inline] def singleton {α : Type u} {γ : Type v} [HasEmptyc γ] [HasInsert α γ] (a : α) : γ := -HasInsert.insert a ∅ - /- Nat basic instances -/ @[extern cpp "lean::nat_add"] protected def Nat.add : (@& Nat) → (@& Nat) → Nat @@ -1239,18 +1194,16 @@ end Subtype /- Sum -/ -infixr ⊕ := Sum - section variables {α : Type u} {β : Type v} -instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (α ⊕ β) := +instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) := ⟨Sum.inl (default α)⟩ -instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) := +instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) := ⟨Sum.inr (default β)⟩ -instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) := +instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := {decEq := fun a b => match a, b with | (Sum.inl a), (Sum.inl b) => diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 59b0d7e990..44cd0ffc25 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -266,9 +266,6 @@ def unzip : List (α × β) → List α × List β protected def insert [DecidableEq α] (a : α) (l : List α) : List α := if a ∈ l then l else a :: l -instance [DecidableEq α] : HasInsert α (List α) := -⟨List.insert⟩ - def replicate (n : Nat) (a : α) : List α := n.repeat (fun xs => a :: xs) [] diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 52d3a940ed..8492c3b275 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -19,6 +19,9 @@ instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) := namespace RBTree variables {α : Type u} {β : Type v} {lt : α → α → Bool} +@[inline] def empty : RBTree α lt := +RBMap.empty + @[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat := RBMap.depth f t @@ -56,8 +59,6 @@ instance [HasRepr α] : HasRepr (RBTree α lt) := @[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt := RBMap.insert t a () -instance : HasInsert α (RBTree α lt) := ⟨fun a s => s.insert a⟩ - @[inline] def erase (t : RBTree α lt) (a : α) : RBTree α lt := RBMap.erase t a diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index ad2977c716..31bd787b08 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -42,7 +42,7 @@ instance : HasRepr Unit := instance {α : Type u} [HasRepr α] : HasRepr (Option α) := ⟨fun o => match o with | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α ⊕ β) := +instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (Sum α β) := ⟨fun s => match s with | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩ instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) := diff --git a/library/init/data/tostring.lean b/library/init/data/tostring.lean index 4c2898d157..351bd658f4 100644 --- a/library/init/data/tostring.lean +++ b/library/init/data/tostring.lean @@ -76,7 +76,7 @@ instance : HasToString USize := instance {α : Type u} [HasToString α] : HasToString (Option α) := ⟨fun o => match o with | none => "none" | (some a) => "(some " ++ toString a ++ ")"⟩ -instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α ⊕ β) := +instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) := ⟨fun s => match s with | (inl a) => "(inl " ++ toString a ++ ")" | (inr b) => "(inr " ++ toString b ++ ")"⟩ instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) := diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index a5ae79bdba..5e821c5919 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -390,6 +390,9 @@ Decl.extern f xs ty e abbrev IndexSet := RBTree Index Index.lt instance vsetInh : Inhabited IndexSet := ⟨{}⟩ +def mkIndexSet (idx : Index) : IndexSet := +RBTree.empty.insert idx + inductive LocalContextEntry | param : IRType → LocalContextEntry | localVar : IRType → Expr → LocalContextEntry diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 26c8a53c83..0b9eb38a01 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -88,6 +88,9 @@ abbrev JPLiveVarMap := RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < instance LiveVarSet.inhabited : Inhabited LiveVarSet := ⟨{}⟩ +def mkLiveVarSet (x : VarId) : LiveVarSet := +RBTree.empty.insert x + namespace LiveVars abbrev Collector := LiveVarSet → LiveVarSet diff --git a/library/init/lean/compiler/ir/pushproj.lean b/library/init/lean/compiler/ir/pushproj.lean index 0235e3d37b..0e4fa2a9f9 100644 --- a/library/init/lean/compiler/ir/pushproj.lean +++ b/library/init/lean/compiler/ir/pushproj.lean @@ -45,7 +45,7 @@ partial def FnBody.pushProj : FnBody → FnBody match term with | FnBody.case tid x alts => let altsF := alts.map $ fun alt => alt.body.freeIndices; - let (bs, alts) := pushProjs bs alts altsF Array.empty {x.idx}; + let (bs, alts) := pushProjs bs alts altsF Array.empty (mkIndexSet x.idx); let alts := alts.map $ fun alt => alt.modifyBody FnBody.pushProj; let term := FnBody.case tid x alts; reshape bs term diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean index b982db0a00..e7699d25a3 100644 --- a/library/init/lean/compiler/ir/rc.lean +++ b/library/init/lean/compiler/ir/rc.lean @@ -260,7 +260,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet) match x with | Arg.var x => let info := getVarInfo ctx x; - if info.ref && !info.persistent && !info.consume then (addInc x b, {x}) else (b, {x}) + if info.ref && !info.persistent && !info.consume then (addInc x b, mkLiveVarSet x) else (b, mkLiveVarSet x) | _ => (b, {}) | b@(FnBody.jmp j xs) ctx := let jLiveVars := getJPLiveVars ctx j; diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 0dcca40d40..aa99f1af9d 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -45,7 +45,8 @@ pushLeading >> symbol sym lbp >> termParser lbp @[builtinTermParser] def sort := parser! symbol "Sort" appPrec @[builtinTermParser] def hole := parser! symbol "_" appPrec @[builtinTermParser] def «sorry» := parser! symbol "sorry" appPrec -@[builtinTermParser] def cdot := parser! symbol "·" appPrec +@[builtinTermParser] def cdot := parser! symbol "·" appPrec +@[builtinTermParser] def emptyC := parser! symbol "∅" appPrec def typeAscription := parser! " : " >> termParser def tupleTail := parser! ", " >> sepBy1 termParser ", " def parenSpecial : Parser := optional (tupleTail <|> typeAscription)