refactor: use Ordering inside of rbmap instead of lt.
This commit is contained in:
Daniel Fabian
Leonardo de Moura
parent
bdce1a2a79
commit
0238bf8c33
21 changed files with 217 additions and 168 deletions
|
|
@ -10,7 +10,7 @@ import Init.Data.String
|
|||
|
||||
inductive Ordering where
|
||||
| lt | eq | gt
|
||||
deriving Inhabited
|
||||
deriving Inhabited, BEq
|
||||
|
||||
|
||||
class Ord (α : Type u) where
|
||||
|
|
@ -37,3 +37,14 @@ instance : Ord Bool where
|
|||
|
||||
instance : Ord String where
|
||||
compare x y := compareOfLessAndEq x y
|
||||
|
||||
instance (n : Nat) : Ord (Fin n) where
|
||||
compare x y := compare x.val y.val
|
||||
|
||||
def USize.cmp (a b : USize) : Ordering := compare a.val b.val
|
||||
|
||||
instance : Ord USize where
|
||||
compare x y := compare x.val y.val
|
||||
|
||||
instance : Ord Char where
|
||||
compare x y := compareOfLessAndEq x y
|
||||
|
|
@ -830,7 +830,7 @@ instance : LT UInt32 where
|
|||
|
||||
instance : LE UInt32 where
|
||||
le a b := LE.le a.val b.val
|
||||
|
||||
|
||||
set_option bootstrap.genMatcherCode false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
|
||||
|
|
|
|||
|
|
@ -440,7 +440,7 @@ end Decl
|
|||
open Std (RBTree RBTree.empty RBMap)
|
||||
|
||||
/-- Set of variable and join point names -/
|
||||
abbrev IndexSet := RBTree Index Index.lt
|
||||
abbrev IndexSet := RBTree Index compare
|
||||
instance : Inhabited IndexSet := ⟨{}⟩
|
||||
|
||||
def mkIndexSet (idx : Index) : IndexSet :=
|
||||
|
|
@ -451,7 +451,7 @@ inductive LocalContextEntry where
|
|||
| localVar : IRType → Expr → LocalContextEntry
|
||||
| joinPoint : Array Param → FnBody → LocalContextEntry
|
||||
|
||||
abbrev LocalContext := RBMap Index LocalContextEntry Index.lt
|
||||
abbrev LocalContext := RBMap Index LocalContextEntry compare
|
||||
|
||||
def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext :=
|
||||
ctx.insert x.idx (LocalContextEntry.localVar t v)
|
||||
|
|
@ -507,7 +507,7 @@ def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr :=
|
|||
| some (LocalContextEntry.localVar _ v) => some v
|
||||
| other => none
|
||||
|
||||
abbrev IndexRenaming := RBMap Index Index Index.lt
|
||||
abbrev IndexRenaming := RBMap Index Index compare
|
||||
|
||||
class AlphaEqv (α : Type) where
|
||||
aeqv : IndexRenaming → α → α → Bool
|
||||
|
|
@ -599,7 +599,7 @@ def FnBody.beq (b₁ b₂ : FnBody) : Bool :=
|
|||
|
||||
instance : BEq FnBody := ⟨FnBody.beq⟩
|
||||
|
||||
abbrev VarIdSet := RBTree VarId (fun x y => x.idx < y.idx)
|
||||
abbrev VarIdSet := RBTree VarId (fun x y => compare x.idx y.idx)
|
||||
instance : Inhabited VarIdSet := ⟨{}⟩
|
||||
|
||||
def mkIf (x : VarId) (t e : FnBody) : FnBody :=
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
|
|||
(IsLive.visitFnBody x.idx b).run' ctx
|
||||
|
||||
abbrev LiveVarSet := VarIdSet
|
||||
abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx)
|
||||
abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx)
|
||||
|
||||
instance : Inhabited LiveVarSet where
|
||||
default := {}
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ structure VarInfo where
|
|||
consume : Bool := false -- true if the variable RC must be "consumed"
|
||||
deriving Inhabited
|
||||
|
||||
abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => x.idx < y.idx)
|
||||
abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => compare x.idx y.idx)
|
||||
|
||||
structure Context where
|
||||
env : Environment
|
||||
|
|
|
|||
|
|
@ -45,6 +45,7 @@ protected def normalize : JsonNumber → Int × Nat × Int
|
|||
break
|
||||
(sign, mAbs, -(e : Int) + nDigits)
|
||||
|
||||
-- todo (Dany): We should have an Ordering version of this.
|
||||
def lt (a b : JsonNumber) : Bool :=
|
||||
let (as, am, ae) := a.normalize
|
||||
let (bs, bm, be) := b.normalize
|
||||
|
|
@ -77,6 +78,12 @@ instance : LT JsonNumber :=
|
|||
|
||||
instance (a b : JsonNumber) : Decidable (a < b) :=
|
||||
inferInstanceAs (Decidable (lt a b = true))
|
||||
|
||||
instance : Ord JsonNumber where
|
||||
compare x y :=
|
||||
if x < y then Ordering.lt
|
||||
else if x > y then Ordering.gt
|
||||
else Ordering.eq
|
||||
|
||||
protected def toString : JsonNumber → String
|
||||
| ⟨m, 0⟩ => m.repr
|
||||
|
|
@ -140,7 +147,7 @@ def mkObj (o : List (String × Json)) : Json :=
|
|||
obj $ do
|
||||
let mut kvPairs := RBNode.leaf
|
||||
for ⟨k, v⟩ in o do
|
||||
kvPairs := kvPairs.insert strLt k v
|
||||
kvPairs := kvPairs.insert compare k v
|
||||
kvPairs
|
||||
|
||||
instance : Coe Nat Json := ⟨fun n => Json.num n⟩
|
||||
|
|
@ -181,7 +188,7 @@ def getNum? : Json → Option JsonNumber
|
|||
| _ => none
|
||||
|
||||
def getObjVal? : Json → String → Option Json
|
||||
| obj kvs, k => kvs.find strLt k
|
||||
| obj kvs, k => kvs.find compare k
|
||||
| _ , _ => none
|
||||
|
||||
def getArrVal? : Json → Nat → Option Json
|
||||
|
|
@ -192,7 +199,7 @@ def getObjValD (j : Json) (k : String) : Json :=
|
|||
(j.getObjVal? k).getD null
|
||||
|
||||
def setObjVal! : Json → String → Json → Json
|
||||
| obj kvs, k, v => obj <| kvs.insert strLt k v
|
||||
| obj kvs, k, v => obj <| kvs.insert compare k v
|
||||
| j , _, _ => panic! "Json.setObjVal!: not an object: {j}"
|
||||
|
||||
inductive Structured where
|
||||
|
|
|
|||
|
|
@ -249,7 +249,7 @@ partial def objectCore (anyCore : Unit → Quickparse Json) : Quickparse (RBNode
|
|||
else if c = ',' then
|
||||
ws
|
||||
let kvs ← objectCore anyCore
|
||||
kvs.insert strLt k v
|
||||
kvs.insert compare k v
|
||||
else
|
||||
fail "unexpected character in object"
|
||||
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ inductive RequestID where
|
|||
| str (s : String)
|
||||
| num (n : JsonNumber)
|
||||
| null
|
||||
deriving Inhabited, BEq
|
||||
deriving Inhabited, BEq, Ord
|
||||
|
||||
instance : ToString RequestID where
|
||||
toString
|
||||
|
|
|
|||
|
|
@ -65,26 +65,46 @@ def isSuffixOf : Name → Name → Bool
|
|||
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
|
||||
| _, _ => false
|
||||
|
||||
def lt : Name → Name → Bool
|
||||
| anonymous, anonymous => false
|
||||
| anonymous, _ => true
|
||||
| num p₁ i₁ _, num p₂ i₂ _ => lt p₁ p₂ || (p₁ == p₂ && i₁ < i₂)
|
||||
| num _ _ _, str _ _ _ => true
|
||||
| str p₁ n₁ _, str p₂ n₂ _ => lt p₁ p₂ || (p₁ == p₂ && n₁ < n₂)
|
||||
| _, _ => false
|
||||
def cmp : Name → Name → Ordering
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num p₁ i₁ _, num p₂ i₂ _ =>
|
||||
match cmp p₁ p₂ with
|
||||
| Ordering.eq => compare i₁ i₂
|
||||
| ord => ord
|
||||
| num _ _ _, str _ _ _ => Ordering.lt
|
||||
| str _ _ _, num _ _ _ => Ordering.gt
|
||||
| str p₁ n₁ _, str p₂ n₂ _ =>
|
||||
match cmp p₁ p₂ with
|
||||
| Ordering.eq => compare n₁ n₂
|
||||
| ord => ord
|
||||
|
||||
def lt (x y : Name) : Bool :=
|
||||
cmp x y == Ordering.lt
|
||||
|
||||
def quickLtAux : Name → Name → Bool
|
||||
| anonymous, anonymous => false
|
||||
| anonymous, _ => true
|
||||
| num n v _, num n' v' _ => v < v' || (v = v' && n.quickLtAux n')
|
||||
| num _ _ _, str _ _ _ => true
|
||||
| str n s _, str n' s' _ => s < s' || (s = s' && n.quickLtAux n')
|
||||
| _, _ => false
|
||||
def quickCmpAux : Name → Name → Ordering
|
||||
| anonymous, anonymous => Ordering.eq
|
||||
| anonymous, _ => Ordering.lt
|
||||
| _, anonymous => Ordering.gt
|
||||
| num n v _, num n' v' _ =>
|
||||
match compare v v' with
|
||||
| Ordering.eq => n.quickCmpAux n'
|
||||
| ord => ord
|
||||
| num _ _ _, str _ _ _ => Ordering.lt
|
||||
| str _ _ _, num _ _ _ => Ordering.gt
|
||||
| str n s _, str n' s' _ =>
|
||||
match compare s s' with
|
||||
| Ordering.eq => n.quickCmpAux n'
|
||||
| ord => ord
|
||||
|
||||
def quickCmp (n₁ n₂ : Name) : Ordering :=
|
||||
match compare n₁.hash n₂.hash with
|
||||
| Ordering.eq => quickCmpAux n₁ n₂
|
||||
| ord => ord
|
||||
|
||||
def quickLt (n₁ n₂ : Name) : Bool :=
|
||||
if n₁.hash < n₂.hash then true
|
||||
else if n₁.hash > n₂.hash then false
|
||||
else quickLtAux n₁ n₂
|
||||
quickCmp n₁ n₂ == Ordering.lt
|
||||
|
||||
/- Alternative HasLt instance. -/
|
||||
@[inline] protected def hasLtQuick : LT Name :=
|
||||
|
|
@ -122,9 +142,9 @@ end Name
|
|||
|
||||
open Std (RBMap RBTree mkRBMap mkRBTree)
|
||||
|
||||
def NameMap (α : Type) := Std.RBMap Name α Name.quickLt
|
||||
def NameMap (α : Type) := Std.RBMap Name α Name.quickCmp
|
||||
|
||||
@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickLt
|
||||
@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickCmp
|
||||
|
||||
namespace NameMap
|
||||
variable {α : Type}
|
||||
|
|
@ -142,10 +162,10 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
|
|||
|
||||
end NameMap
|
||||
|
||||
def NameSet := RBTree Name Name.quickLt
|
||||
def NameSet := RBTree Name Name.quickCmp
|
||||
|
||||
namespace NameSet
|
||||
def empty : NameSet := mkRBTree Name Name.quickLt
|
||||
def empty : NameSet := mkRBTree Name Name.quickCmp
|
||||
instance : EmptyCollection NameSet := ⟨empty⟩
|
||||
instance : Inhabited NameSet := ⟨{}⟩
|
||||
def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n
|
||||
|
|
|
|||
|
|
@ -16,13 +16,19 @@ instance : ToString NamePart where
|
|||
| NamePart.str s => s
|
||||
| NamePart.num n => toString n
|
||||
|
||||
def NamePart.cmp : NamePart → NamePart → Ordering
|
||||
| NamePart.str a, NamePart.str b => compare a b
|
||||
| NamePart.num a, NamePart.num b => compare a b
|
||||
| NamePart.num _, NamePart.str _ => Ordering.lt
|
||||
| _, _ => Ordering.gt
|
||||
|
||||
def NamePart.lt : NamePart → NamePart → Bool
|
||||
| NamePart.str a, NamePart.str b => a < b
|
||||
| NamePart.num a, NamePart.num b => a < b
|
||||
| NamePart.num _, NamePart.str _ => true
|
||||
| _, _ => false
|
||||
|
||||
def NameTrie (β : Type u) := PrefixTree NamePart β NamePart.lt
|
||||
def NameTrie (β : Type u) := PrefixTree NamePart β NamePart.cmp
|
||||
|
||||
private def toKey (n : Name) : List NamePart :=
|
||||
loop n []
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ def empty : PrefixTreeNode α β :=
|
|||
PrefixTreeNode.Node none RBNode.leaf
|
||||
|
||||
@[specialize]
|
||||
partial def insert (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (val : β) : PrefixTreeNode α β :=
|
||||
partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (val : β) : PrefixTreeNode α β :=
|
||||
let rec insertEmpty (k : List α) : PrefixTreeNode α β :=
|
||||
match k with
|
||||
| [] => PrefixTreeNode.Node (some val) RBNode.leaf
|
||||
|
|
@ -32,24 +32,24 @@ partial def insert (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : Lis
|
|||
| PrefixTreeNode.Node v m, [] =>
|
||||
PrefixTreeNode.Node (some val) m -- overrides old value
|
||||
| PrefixTreeNode.Node v m, k :: ks =>
|
||||
let t := match RBNode.find lt m k with
|
||||
let t := match RBNode.find cmp m k with
|
||||
| none => insertEmpty ks
|
||||
| some t => loop t ks
|
||||
PrefixTreeNode.Node v (RBNode.insert lt m k t)
|
||||
PrefixTreeNode.Node v (RBNode.insert cmp m k t)
|
||||
loop t k
|
||||
|
||||
@[specialize]
|
||||
partial def find? (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) : Option β :=
|
||||
partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β :=
|
||||
let rec loop
|
||||
| PrefixTreeNode.Node val m, [] => val
|
||||
| PrefixTreeNode.Node val m, k :: ks =>
|
||||
match RBNode.find lt m k with
|
||||
match RBNode.find cmp m k with
|
||||
| none => none
|
||||
| some t => loop t ks
|
||||
loop t k
|
||||
|
||||
@[specialize]
|
||||
partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
|
||||
partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
|
||||
let rec fold : PrefixTreeNode α β → σ → m σ
|
||||
| PrefixTreeNode.Node b? n, d => do
|
||||
let d ← match b? with
|
||||
|
|
@ -59,19 +59,19 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (lt : α → α
|
|||
let rec find : List α → PrefixTreeNode α β → σ → m σ
|
||||
| [], t, d => fold t d
|
||||
| k::ks, PrefixTreeNode.Node _ m, d =>
|
||||
match RBNode.find lt m k with
|
||||
match RBNode.find cmp m k with
|
||||
| none => pure init
|
||||
| some t => find ks t d
|
||||
find k t init
|
||||
|
||||
inductive WellFormed (lt : α → α → Bool) : PrefixTreeNode α β → Prop where
|
||||
| emptyWff : WellFormed lt empty
|
||||
| insertWff {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed lt t → WellFormed lt (insert t lt k val)
|
||||
inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
|
||||
| emptyWff : WellFormed cmp empty
|
||||
| insertWff {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val)
|
||||
|
||||
end PrefixTreeNode
|
||||
|
||||
def PrefixTree (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
|
||||
{ t : PrefixTreeNode α β // t.WellFormed lt }
|
||||
def PrefixTree (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) :=
|
||||
{ t : PrefixTreeNode α β // t.WellFormed cmp }
|
||||
|
||||
open PrefixTreeNode
|
||||
|
||||
|
|
|
|||
|
|
@ -42,10 +42,10 @@ partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
|
|||
| false =>
|
||||
let c := s.get i
|
||||
let i := s.next i
|
||||
let t := match RBNode.find (.<.) m c with
|
||||
let t := match RBNode.find compare m c with
|
||||
| none => insertEmpty i
|
||||
| some t => loop t i
|
||||
Trie.Node v (RBNode.insert (.<.) m c t)
|
||||
Trie.Node v (RBNode.insert compare m c t)
|
||||
loop t 0
|
||||
|
||||
partial def find? (t : Trie α) (s : String) : Option α :=
|
||||
|
|
@ -56,7 +56,7 @@ partial def find? (t : Trie α) (s : String) : Option α :=
|
|||
| false =>
|
||||
let c := s.get i
|
||||
let i := s.next i
|
||||
match RBNode.find (.<.) m c with
|
||||
match RBNode.find compare m c with
|
||||
| none => none
|
||||
| some t => loop t i
|
||||
loop t 0
|
||||
|
|
@ -75,7 +75,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos
|
|||
let acc := updtAcc v i acc
|
||||
let c := s.get i
|
||||
let i := s.next i
|
||||
match RBNode.find (.<.) m c with
|
||||
match RBNode.find compare m c with
|
||||
| some t => loop t i acc
|
||||
| none => acc
|
||||
loop t i (i, none)
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ namespace Lean.Elab
|
|||
open Command
|
||||
open Meta
|
||||
|
||||
private abbrev IndexSet := Std.RBTree Nat (.<.)
|
||||
private abbrev IndexSet := Std.RBTree Nat compare
|
||||
private abbrev LocalInst2Index := NameMap Nat
|
||||
|
||||
private def implicitBinderF := Parser.Term.implicitBinder
|
||||
|
|
|
|||
|
|
@ -77,7 +77,7 @@ structure DefaultInstanceEntry where
|
|||
instanceName : Name
|
||||
priority : Nat
|
||||
|
||||
abbrev PrioritySet := Std.RBTree Nat (.>.)
|
||||
abbrev PrioritySet := Std.RBTree Nat (fun x y => compare y x)
|
||||
|
||||
structure DefaultInstances where
|
||||
defaultInstances : NameMap (List (Name × Nat)) := {}
|
||||
|
|
|
|||
|
|
@ -1535,7 +1535,7 @@ def eoiFn : ParserFn := fun c s =>
|
|||
open Std (RBMap RBMap.empty)
|
||||
|
||||
/-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
|
||||
def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt
|
||||
def TokenMap (α : Type) := RBMap Name (List α) Name.quickCmp
|
||||
|
||||
namespace TokenMap
|
||||
|
||||
|
|
|
|||
|
|
@ -165,7 +165,7 @@ def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
|
|||
def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true
|
||||
|
||||
/-- Associate pretty printer options to a specific subterm using a synthetic position. -/
|
||||
abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b)
|
||||
abbrev OptionsPerPos := Std.RBMap Nat Options compare
|
||||
|
||||
namespace PrettyPrinter
|
||||
namespace Delaborator
|
||||
|
|
|
|||
|
|
@ -150,7 +150,7 @@ section Elab
|
|||
end Elab
|
||||
|
||||
-- Pending requests are tracked so they can be cancelled
|
||||
abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b))
|
||||
abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) compare
|
||||
|
||||
structure ServerContext where
|
||||
hIn : FS.Stream
|
||||
|
|
|
|||
|
|
@ -96,7 +96,7 @@ section Utils
|
|||
| crashed (queuedMsgs : Array JsonRpc.Message)
|
||||
| running
|
||||
|
||||
abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message (fun a b => Decidable.decide (a < b))
|
||||
abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message compare
|
||||
|
||||
private def parseHeaderAst (input : String) : IO Syntax := do
|
||||
let inputCtx := Parser.mkInputContext input "<input>"
|
||||
|
|
@ -166,7 +166,7 @@ section FileWorker
|
|||
end FileWorker
|
||||
|
||||
section ServerM
|
||||
abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decide (a < b))
|
||||
abbrev FileWorkerMap := RBMap DocumentUri FileWorker compare
|
||||
|
||||
structure ServerContext where
|
||||
hIn : FS.Stream
|
||||
|
|
|
|||
|
|
@ -94,31 +94,32 @@ def isBlack : RBNode α β → Bool
|
|||
|
||||
section Insert
|
||||
|
||||
variable (lt : α → α → Bool)
|
||||
variable (cmp : α → α → Ordering)
|
||||
|
||||
@[specialize] def ins : RBNode α β → (k : α) → β k → RBNode α β
|
||||
| leaf, kx, vx => node red leaf kx vx leaf
|
||||
| node red a ky vy b, kx, vx =>
|
||||
if lt kx ky then node red (ins a kx vx) ky vy b
|
||||
else if lt ky kx then node red a ky vy (ins b kx vx)
|
||||
else node red a kx vx b
|
||||
match cmp kx ky with
|
||||
| Ordering.lt => node red (ins a kx vx) ky vy b
|
||||
| Ordering.gt => node red a ky vy (ins b kx vx)
|
||||
| Ordering.eq => node red a kx vx b
|
||||
| node black a ky vy b, kx, vx =>
|
||||
if lt kx ky then
|
||||
if isRed a then balance1 ky vy b (ins a kx vx)
|
||||
match cmp kx ky with
|
||||
| Ordering.lt =>
|
||||
if isRed a then balance1 ky vy b (ins a kx vx)
|
||||
else node black (ins a kx vx) ky vy b
|
||||
else if lt ky kx then
|
||||
| Ordering.gt =>
|
||||
if isRed b then balance2 a ky vy (ins b kx vx)
|
||||
else node black a ky vy (ins b kx vx)
|
||||
else
|
||||
node black a kx vx b
|
||||
| Ordering.eq => node black a kx vx b
|
||||
|
||||
def setBlack : RBNode α β → RBNode α β
|
||||
| node _ l k v r => node black l k v r
|
||||
| e => e
|
||||
|
||||
@[specialize] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
|
||||
if isRed t then setBlack (ins lt t k v)
|
||||
else ins lt t k v
|
||||
if isRed t then setBlack (ins cmp t k v)
|
||||
else ins cmp t k v
|
||||
|
||||
end Insert
|
||||
|
||||
|
|
@ -166,55 +167,59 @@ partial def appendTrees : RBNode α β → RBNode α β → RBNode α β
|
|||
|
||||
section Erase
|
||||
|
||||
variable (lt : α → α → Bool)
|
||||
variable (cmp : α → α → Ordering)
|
||||
|
||||
@[specialize] def del (x : α) : RBNode α β → RBNode α β
|
||||
| leaf => leaf
|
||||
| node _ a y v b =>
|
||||
if lt x y then
|
||||
match cmp x y with
|
||||
| Ordering.lt =>
|
||||
if a.isBlack then balLeft (del x a) y v b
|
||||
else node red (del x a) y v b
|
||||
else if lt y x then
|
||||
| Ordering.gt =>
|
||||
if b.isBlack then balRight a y v (del x b)
|
||||
else node red a y v (del x b)
|
||||
else appendTrees a b
|
||||
| Ordering.eq => appendTrees a b
|
||||
|
||||
@[specialize] def erase (x : α) (t : RBNode α β) : RBNode α β :=
|
||||
let t := del lt x t;
|
||||
let t := del cmp x t;
|
||||
t.setBlack
|
||||
|
||||
end Erase
|
||||
|
||||
section Membership
|
||||
variable (lt : α → α → Bool)
|
||||
variable (cmp : α → α → Ordering)
|
||||
|
||||
@[specialize] def findCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
|
||||
| leaf, x => none
|
||||
| node _ a ky vy b, x =>
|
||||
if lt x ky then findCore a x
|
||||
else if lt ky x then findCore b x
|
||||
else some ⟨ky, vy⟩
|
||||
match cmp x ky with
|
||||
| Ordering.lt => findCore a x
|
||||
| Ordering.gt => findCore b x
|
||||
| Ordering.eq => some ⟨ky, vy⟩
|
||||
|
||||
@[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β
|
||||
| leaf, x => none
|
||||
| node _ a ky vy b, x =>
|
||||
if lt x ky then find a x
|
||||
else if lt ky x then find b x
|
||||
else some vy
|
||||
match cmp x ky with
|
||||
| Ordering.lt => find a x
|
||||
| Ordering.gt => find b x
|
||||
| Ordering.eq => some vy
|
||||
|
||||
@[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
|
||||
| leaf, x, lb => lb
|
||||
| node _ a ky vy b, x, lb =>
|
||||
if lt x ky then lowerBound a x lb
|
||||
else if lt ky x then lowerBound b x (some ⟨ky, vy⟩)
|
||||
else some ⟨ky, vy⟩
|
||||
match cmp x ky with
|
||||
| Ordering.lt => lowerBound a x lb
|
||||
| Ordering.gt => lowerBound b x (some ⟨ky, vy⟩)
|
||||
| Ordering.eq => some ⟨ky, vy⟩
|
||||
|
||||
end Membership
|
||||
|
||||
inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop where
|
||||
| leafWff : WellFormed lt leaf
|
||||
| insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed lt n → n' = insert lt n k v → WellFormed lt n'
|
||||
| eraseWff {n n' : RBNode α β} {k : α} : WellFormed lt n → n' = erase lt k n → WellFormed lt n'
|
||||
inductive WellFormed (cmp : α → α → Ordering) : RBNode α β → Prop where
|
||||
| leafWff : WellFormed cmp leaf
|
||||
| insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed cmp n → n' = insert cmp n k v → WellFormed cmp n'
|
||||
| eraseWff {n n' : RBNode α β} {k : α} : WellFormed cmp n → n' = erase cmp k n → WellFormed cmp n'
|
||||
|
||||
end RBNode
|
||||
|
||||
|
|
@ -222,124 +227,124 @@ open Std.RBNode
|
|||
|
||||
/- TODO(Leo): define dRBMap -/
|
||||
|
||||
def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
|
||||
{t : RBNode α (fun _ => β) // t.WellFormed lt }
|
||||
def RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) :=
|
||||
{t : RBNode α (fun _ => β) // t.WellFormed cmp }
|
||||
|
||||
@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt :=
|
||||
@[inline] def mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : RBMap α β cmp :=
|
||||
⟨leaf, WellFormed.leafWff⟩
|
||||
|
||||
@[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt :=
|
||||
@[inline] def RBMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp :=
|
||||
mkRBMap ..
|
||||
|
||||
instance (α : Type u) (β : Type v) (lt : α → α → Bool) : EmptyCollection (RBMap α β lt) :=
|
||||
instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (RBMap α β cmp) :=
|
||||
⟨RBMap.empty⟩
|
||||
|
||||
namespace RBMap
|
||||
variable {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool}
|
||||
variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering}
|
||||
|
||||
def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
|
||||
def depth (f : Nat → Nat → Nat) (t : RBMap α β cmp) : Nat :=
|
||||
t.val.depth f
|
||||
|
||||
@[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
|
||||
@[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
|
||||
| b, ⟨t, _⟩ => t.fold f b
|
||||
|
||||
@[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
|
||||
@[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
|
||||
| b, ⟨t, _⟩ => t.revFold f b
|
||||
|
||||
@[inline] def foldM [Monad m] (f : σ → α → β → m σ) : (init : σ) → RBMap α β lt → m σ
|
||||
@[inline] def foldM [Monad m] (f : σ → α → β → m σ) : (init : σ) → RBMap α β cmp → m σ
|
||||
| b, ⟨t, _⟩ => t.foldM f b
|
||||
|
||||
@[inline] def forM [Monad m] (f : α → β → m PUnit) (t : RBMap α β lt) : m PUnit :=
|
||||
@[inline] def forM [Monad m] (f : α → β → m PUnit) (t : RBMap α β cmp) : m PUnit :=
|
||||
t.foldM (fun _ k v => f k v) ⟨⟩
|
||||
|
||||
@[inline] protected def forIn [Monad m] (t : RBMap α β lt) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
|
||||
@[inline] protected def forIn [Monad m] (t : RBMap α β cmp) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
|
||||
t.val.forIn init (fun a b acc => f (a, b) acc)
|
||||
|
||||
instance : ForIn m (RBMap α β lt) (α × β) where
|
||||
instance : ForIn m (RBMap α β cmp) (α × β) where
|
||||
forIn := RBMap.forIn
|
||||
|
||||
@[inline] def isEmpty : RBMap α β lt → Bool
|
||||
@[inline] def isEmpty : RBMap α β cmp → Bool
|
||||
| ⟨leaf, _⟩ => true
|
||||
| _ => false
|
||||
|
||||
@[specialize] def toList : RBMap α β lt → List (α × β)
|
||||
@[specialize] def toList : RBMap α β cmp → List (α × β)
|
||||
| ⟨t, _⟩ => t.revFold (fun ps k v => (k, v)::ps) []
|
||||
|
||||
@[inline] protected def min : RBMap α β lt → Option (α × β)
|
||||
@[inline] protected def min : RBMap α β cmp → 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 α β cmp → Option (α × β)
|
||||
| ⟨t, _⟩ =>
|
||||
match t.max with
|
||||
| some ⟨k, v⟩ => some (k, v)
|
||||
| none => none
|
||||
|
||||
instance [Repr α] [Repr β] : Repr (RBMap α β lt) where
|
||||
instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
|
||||
reprPrec m prec := Repr.addAppParen ("Std.rbmapOf " ++ repr m.toList) prec
|
||||
|
||||
@[inline] def insert : RBMap α β lt → α → β → RBMap α β lt
|
||||
| ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
|
||||
@[inline] def insert : RBMap α β cmp → α → β → RBMap α β cmp
|
||||
| ⟨t, w⟩, k, v => ⟨t.insert cmp k v, WellFormed.insertWff w rfl⟩
|
||||
|
||||
@[inline] def erase : RBMap α β lt → α → RBMap α β lt
|
||||
| ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩
|
||||
@[inline] def erase : RBMap α β cmp → α → RBMap α β cmp
|
||||
| ⟨t, w⟩, k => ⟨t.erase cmp k, WellFormed.eraseWff w rfl⟩
|
||||
|
||||
@[specialize] def ofList : List (α × β) → RBMap α β lt
|
||||
@[specialize] def ofList : List (α × β) → RBMap α β cmp
|
||||
| [] => mkRBMap ..
|
||||
| ⟨k,v⟩::xs => (ofList xs).insert k v
|
||||
|
||||
@[inline] def findCore? : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
|
||||
| ⟨t, _⟩, x => t.findCore lt x
|
||||
@[inline] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
|
||||
| ⟨t, _⟩, x => t.findCore cmp x
|
||||
|
||||
@[inline] def find? : RBMap α β lt → α → Option β
|
||||
| ⟨t, _⟩, x => t.find lt x
|
||||
@[inline] def find? : RBMap α β cmp → α → Option β
|
||||
| ⟨t, _⟩, x => t.find cmp x
|
||||
|
||||
@[inline] def findD (t : RBMap α β lt) (k : α) (v₀ : β) : β :=
|
||||
@[inline] def findD (t : RBMap α β cmp) (k : α) (v₀ : β) : β :=
|
||||
(t.find? k).getD v₀
|
||||
|
||||
/-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
|
||||
if it exists. -/
|
||||
@[inline] def lowerBound : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
|
||||
| ⟨t, _⟩, x => t.lowerBound lt x none
|
||||
@[inline] def lowerBound : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
|
||||
| ⟨t, _⟩, x => t.lowerBound cmp x none
|
||||
|
||||
@[inline] def contains (t : RBMap α β lt) (a : α) : Bool :=
|
||||
@[inline] def contains (t : RBMap α β cmp) (a : α) : Bool :=
|
||||
(t.find? a).isSome
|
||||
|
||||
@[inline] def fromList (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
|
||||
l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β lt)
|
||||
@[inline] def fromList (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
|
||||
l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
|
||||
|
||||
@[inline] def all : RBMap α β lt → (α → β → Bool) → Bool
|
||||
@[inline] def all : RBMap α β cmp → (α → β → Bool) → Bool
|
||||
| ⟨t, _⟩, p => t.all p
|
||||
|
||||
@[inline] def any : RBMap α β lt → (α → β → Bool) → Bool
|
||||
@[inline] def any : RBMap α β cmp → (α → β → Bool) → Bool
|
||||
| ⟨t, _⟩, p => t.any p
|
||||
|
||||
def size (m : RBMap α β lt) : Nat :=
|
||||
def size (m : RBMap α β cmp) : Nat :=
|
||||
m.fold (fun sz _ _ => sz+1) 0
|
||||
|
||||
def maxDepth (t : RBMap α β lt) : Nat :=
|
||||
def maxDepth (t : RBMap α β cmp) : Nat :=
|
||||
t.val.depth Nat.max
|
||||
|
||||
@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
|
||||
@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β :=
|
||||
match t.min with
|
||||
| some p => p
|
||||
| none => panic! "map is empty"
|
||||
|
||||
@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
|
||||
@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β :=
|
||||
match t.max with
|
||||
| some p => p
|
||||
| none => panic! "map is empty"
|
||||
|
||||
@[inline] def find! [Inhabited β] (t : RBMap α β lt) (k : α) : β :=
|
||||
@[inline] def find! [Inhabited β] (t : RBMap α β cmp) (k : α) : β :=
|
||||
match t.find? k with
|
||||
| some b => b
|
||||
| none => panic! "key is not in the map"
|
||||
|
||||
end RBMap
|
||||
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
|
||||
RBMap.fromList l lt
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
|
||||
RBMap.fromList l cmp
|
||||
|
||||
end Std
|
||||
|
|
|
|||
|
|
@ -7,99 +7,99 @@ import Std.Data.RBMap
|
|||
namespace Std
|
||||
universes u v w
|
||||
|
||||
def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=
|
||||
RBMap α Unit lt
|
||||
def RBTree (α : Type u) (cmp : α → α → Ordering) : Type u :=
|
||||
RBMap α Unit cmp
|
||||
|
||||
instance : Inhabited (RBTree α p) where
|
||||
default := RBMap.empty
|
||||
|
||||
@[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt :=
|
||||
mkRBMap α Unit lt
|
||||
@[inline] def mkRBTree (α : Type u) (cmp : α → α → Ordering) : RBTree α cmp :=
|
||||
mkRBMap α Unit cmp
|
||||
|
||||
instance (α : Type u) (lt : α → α → Bool) : EmptyCollection (RBTree α lt) :=
|
||||
⟨mkRBTree α lt⟩
|
||||
instance (α : Type u) (cmp : α → α → Ordering) : EmptyCollection (RBTree α cmp) :=
|
||||
⟨mkRBTree α cmp⟩
|
||||
|
||||
namespace RBTree
|
||||
variable {α : Type u} {β : Type v} {lt : α → α → Bool}
|
||||
variable {α : Type u} {β : Type v} {cmp : α → α → Ordering}
|
||||
|
||||
@[inline] def empty : RBTree α lt :=
|
||||
@[inline] def empty : RBTree α cmp :=
|
||||
RBMap.empty
|
||||
|
||||
@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat :=
|
||||
@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α cmp) : Nat :=
|
||||
RBMap.depth f t
|
||||
|
||||
@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
|
||||
@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α cmp) : β :=
|
||||
RBMap.fold (fun r a _ => f r a) init t
|
||||
|
||||
@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
|
||||
@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α cmp) : β :=
|
||||
RBMap.revFold (fun r a _ => f r a) init t
|
||||
|
||||
@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α lt) : m β :=
|
||||
@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α cmp) : m β :=
|
||||
RBMap.foldM (fun r a _ => f r a) init t
|
||||
|
||||
@[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α lt) : m PUnit :=
|
||||
@[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α cmp) : m PUnit :=
|
||||
t.foldM (fun _ a => f a) ⟨⟩
|
||||
|
||||
@[inline] protected def forIn [Monad m] (t : RBTree α lt) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
|
||||
@[inline] protected def forIn [Monad m] (t : RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
|
||||
t.val.forIn init (fun a _ acc => f a acc)
|
||||
|
||||
instance : ForIn m (RBTree α lt) α where
|
||||
instance : ForIn m (RBTree α cmp) α where
|
||||
forIn := RBTree.forIn
|
||||
|
||||
@[inline] def isEmpty (t : RBTree α lt) : Bool :=
|
||||
@[inline] def isEmpty (t : RBTree α cmp) : Bool :=
|
||||
RBMap.isEmpty t
|
||||
|
||||
@[specialize] def toList (t : RBTree α lt) : List α :=
|
||||
@[specialize] def toList (t : RBTree α cmp) : List α :=
|
||||
t.revFold (fun as a => a::as) []
|
||||
|
||||
@[inline] protected def min (t : RBTree α lt) : Option α :=
|
||||
@[inline] protected def min (t : RBTree α cmp) : Option α :=
|
||||
match RBMap.min t with
|
||||
| some ⟨a, _⟩ => some a
|
||||
| none => none
|
||||
|
||||
@[inline] protected def max (t : RBTree α lt) : Option α :=
|
||||
@[inline] protected def max (t : RBTree α cmp) : Option α :=
|
||||
match RBMap.max t with
|
||||
| some ⟨a, _⟩ => some a
|
||||
| none => none
|
||||
|
||||
instance [Repr α] : Repr (RBTree α lt) where
|
||||
instance [Repr α] : Repr (RBTree α cmp) where
|
||||
reprPrec t prec := Repr.addAppParen ("Std.rbtreeOf " ++ repr t.toList) prec
|
||||
|
||||
@[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt :=
|
||||
@[inline] def insert (t : RBTree α cmp) (a : α) : RBTree α cmp :=
|
||||
RBMap.insert t a ()
|
||||
|
||||
@[inline] def erase (t : RBTree α lt) (a : α) : RBTree α lt :=
|
||||
@[inline] def erase (t : RBTree α cmp) (a : α) : RBTree α cmp :=
|
||||
RBMap.erase t a
|
||||
|
||||
@[specialize] def ofList : List α → RBTree α lt
|
||||
@[specialize] def ofList : List α → RBTree α cmp
|
||||
| [] => mkRBTree ..
|
||||
| x::xs => (ofList xs).insert x
|
||||
|
||||
@[inline] def find? (t : RBTree α lt) (a : α) : Option α :=
|
||||
@[inline] def find? (t : RBTree α cmp) (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 α cmp) (a : α) : Bool :=
|
||||
(t.find? a).isSome
|
||||
|
||||
def fromList (l : List α) (lt : α → α → Bool) : RBTree α lt :=
|
||||
l.foldl insert (mkRBTree α lt)
|
||||
def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
|
||||
l.foldl insert (mkRBTree α cmp)
|
||||
|
||||
@[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool :=
|
||||
@[inline] def all (t : RBTree α cmp) (p : α → Bool) : Bool :=
|
||||
RBMap.all t (fun a _ => p a)
|
||||
|
||||
@[inline] def any (t : RBTree α lt) (p : α → Bool) : Bool :=
|
||||
@[inline] def any (t : RBTree α cmp) (p : α → Bool) : Bool :=
|
||||
RBMap.any t (fun a _ => p a)
|
||||
|
||||
def subset (t₁ t₂ : RBTree α lt) : Bool :=
|
||||
def subset (t₁ t₂ : RBTree α cmp) : Bool :=
|
||||
t₁.all fun a => (t₂.find? a).toBool
|
||||
|
||||
def seteq (t₁ t₂ : RBTree α lt) : Bool :=
|
||||
def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
|
||||
subset t₁ t₂ && subset t₂ t₁
|
||||
|
||||
end RBTree
|
||||
|
||||
def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Bool) : RBTree α lt :=
|
||||
RBTree.fromList l lt
|
||||
def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
|
||||
RBTree.fromList l cmp
|
||||
end Std
|
||||
|
|
|
|||
|
|
@ -4,14 +4,14 @@ open Std
|
|||
def check (b : Bool) : IO Unit := do
|
||||
unless b do IO.println "ERROR"
|
||||
|
||||
def sz {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
|
||||
def sz {α β : Type} {cmp : α → α → Ordering} (m : RBMap α β cmp) : Nat :=
|
||||
m.fold (fun sz _ _ => sz+1) 0
|
||||
|
||||
def depth {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
|
||||
def depth {α β : Type} {cmp : α → α → Ordering} (m : RBMap α β cmp) : Nat :=
|
||||
m.depth Nat.max
|
||||
|
||||
def tst1 : IO Unit :=
|
||||
do let Map := RBMap String Nat (fun a b => a < b)
|
||||
do let Map := RBMap String Nat compare
|
||||
let m : Map := {}
|
||||
let m := m.insert "hello" 0
|
||||
let m := m.insert "world" 1
|
||||
|
|
@ -23,7 +23,7 @@ do let Map := RBMap String Nat (fun a b => a < b)
|
|||
pure ()
|
||||
|
||||
def tst2 : IO Unit :=
|
||||
do let Map := RBMap Nat Nat (fun a b => a < b)
|
||||
do let Map := RBMap Nat Nat compare
|
||||
let m : Map := {}
|
||||
let n : Nat := 10000
|
||||
let mut m := n.fold (fun i (m : Map) => m.insert i (i*10)) m
|
||||
|
|
@ -37,7 +37,7 @@ do let Map := RBMap Nat Nat (fun a b => a < b)
|
|||
IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m))
|
||||
pure ()
|
||||
|
||||
abbrev Map := RBMap Nat Nat (fun a b => a < b)
|
||||
abbrev Map := RBMap Nat Nat compare
|
||||
|
||||
def mkRandMap (max : Nat) : Nat → Map → Array (Nat × Nat) → IO (Map × Array (Nat × Nat))
|
||||
| 0, m, a => pure (m, a)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue