chore: Hashable => HashableUSize
This commit is contained in:
Leonardo de Moura
parent
6a87bba9c0
commit
43812444a7
19 changed files with 156 additions and 156 deletions
|
|
@ -8,42 +8,42 @@ import Init.Data.UInt
|
|||
import Init.Data.String
|
||||
universes u
|
||||
|
||||
instance : Hashable Nat where
|
||||
hash n := USize.ofNat n
|
||||
instance : HashableUSize Nat where
|
||||
hashUSize n := USize.ofNat n
|
||||
|
||||
instance [Hashable α] [Hashable β] : Hashable (α × β) where
|
||||
hash | (a, b) => mixUSizeHash (hash a) (hash b)
|
||||
instance [HashableUSize α] [HashableUSize β] : HashableUSize (α × β) where
|
||||
hashUSize | (a, b) => mixUSizeHash (hashUSize a) (hashUSize b)
|
||||
|
||||
instance : Hashable Bool where
|
||||
hash
|
||||
instance : HashableUSize Bool where
|
||||
hashUSize
|
||||
| true => 11
|
||||
| false => 13
|
||||
|
||||
protected def Option.hash [Hashable α] : Option α → USize
|
||||
protected def Option.hash [HashableUSize α] : Option α → USize
|
||||
| none => 11
|
||||
| some a => mixUSizeHash (hash a) 13
|
||||
| some a => mixUSizeHash (hashUSize a) 13
|
||||
|
||||
instance [Hashable α] : Hashable (Option α) where
|
||||
hash
|
||||
instance [HashableUSize α] : HashableUSize (Option α) where
|
||||
hashUSize
|
||||
| none => 11
|
||||
| some a => mixUSizeHash (hash a) 13
|
||||
| some a => mixUSizeHash (hashUSize a) 13
|
||||
|
||||
instance [Hashable α] : Hashable (List α) where
|
||||
hash as := as.foldl (fun r a => mixUSizeHash r (hash a)) 7
|
||||
instance [HashableUSize α] : HashableUSize (List α) where
|
||||
hashUSize as := as.foldl (fun r a => mixUSizeHash r (hashUSize a)) 7
|
||||
|
||||
instance : Hashable UInt32 where
|
||||
hash n := n.toUSize
|
||||
instance : HashableUSize UInt32 where
|
||||
hashUSize n := n.toUSize
|
||||
|
||||
instance : Hashable UInt64 where
|
||||
hash n := n.toUSize
|
||||
instance : HashableUSize UInt64 where
|
||||
hashUSize n := n.toUSize
|
||||
|
||||
instance : Hashable USize where
|
||||
hash n := n
|
||||
instance : HashableUSize USize where
|
||||
hashUSize n := n
|
||||
|
||||
instance : Hashable Int where
|
||||
hash
|
||||
instance : HashableUSize Int where
|
||||
hashUSize
|
||||
| Int.ofNat n => USize.ofNat (2 * n)
|
||||
| Int.negSucc n => USize.ofNat (2 * n + 1)
|
||||
|
||||
instance (P : Prop) : Hashable P where
|
||||
hash := Function.const P 0
|
||||
instance (P : Prop) : HashableUSize P where
|
||||
hashUSize := Function.const P 0
|
||||
|
|
|
|||
|
|
@ -1587,10 +1587,10 @@ instance nonBacktrackable : Backtrackable PUnit σ where
|
|||
|
||||
end EStateM
|
||||
|
||||
class Hashable (α : Sort u) where
|
||||
hash : α → USize
|
||||
class HashableUSize (α : Sort u) where
|
||||
hashUSize : α → USize
|
||||
|
||||
export Hashable (hash)
|
||||
export HashableUSize (hashUSize)
|
||||
|
||||
@[extern "lean_usize_mix_hash"]
|
||||
constant mixUSizeHash (u₁ u₂ : USize) : USize
|
||||
|
|
@ -1601,8 +1601,8 @@ constant mixUSizeHash (u₁ u₂ : USize) : USize
|
|||
@[extern "lean_string_hash"]
|
||||
protected constant String.hash (s : @& String) : USize
|
||||
|
||||
instance : Hashable String where
|
||||
hash := String.hash
|
||||
instance : HashableUSize String where
|
||||
hashUSize := String.hash
|
||||
|
||||
namespace Lean
|
||||
|
||||
|
|
@ -1620,18 +1620,18 @@ protected def Name.hash : Name → USize
|
|||
| Name.str p s h => h
|
||||
| Name.num p v h => h
|
||||
|
||||
instance : Hashable Name where
|
||||
hash := Name.hash
|
||||
instance : HashableUSize Name where
|
||||
hashUSize := Name.hash
|
||||
|
||||
namespace Name
|
||||
|
||||
@[export lean_name_mk_string]
|
||||
def mkStr (p : Name) (s : String) : Name :=
|
||||
Name.str p s (mixUSizeHash (hash p) (hash s))
|
||||
Name.str p s (mixUSizeHash (hashUSize p) (hashUSize s))
|
||||
|
||||
@[export lean_name_mk_numeral]
|
||||
def mkNum (p : Name) (v : Nat) : Name :=
|
||||
Name.num p v (mixUSizeHash (hash p) (dite (LT.lt v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 (by decide))))
|
||||
Name.num p v (mixUSizeHash (hashUSize p) (dite (LT.lt v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 (by decide))))
|
||||
|
||||
def mkSimple (s : String) : Name :=
|
||||
mkStr Name.anonymous s
|
||||
|
|
|
|||
|
|
@ -35,12 +35,12 @@ abbrev Index.lt (a b : Index) : Bool := a < b
|
|||
instance : BEq VarId := ⟨fun a b => a.idx == b.idx⟩
|
||||
instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩
|
||||
instance : ToFormat VarId := ⟨fun a => toString a⟩
|
||||
instance : Hashable VarId := ⟨fun a => hash a.idx⟩
|
||||
instance : HashableUSize VarId := ⟨fun a => hashUSize a.idx⟩
|
||||
|
||||
instance : BEq JoinPointId := ⟨fun a b => a.idx == b.idx⟩
|
||||
instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
|
||||
instance : ToFormat JoinPointId := ⟨fun a => toString a⟩
|
||||
instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩
|
||||
instance : HashableUSize JoinPointId := ⟨fun a => hashUSize a.idx⟩
|
||||
|
||||
abbrev MData := KVMap
|
||||
abbrev MData.empty : MData := {}
|
||||
|
|
|
|||
|
|
@ -20,8 +20,8 @@ def beq : Key → Key → Bool
|
|||
instance : BEq Key := ⟨beq⟩
|
||||
|
||||
def getHash : Key → USize
|
||||
| (f, x) => mixUSizeHash (hash f) (hash x)
|
||||
instance : Hashable Key := ⟨getHash⟩
|
||||
| (f, x) => mixUSizeHash (hashUSize f) (hashUSize x)
|
||||
instance : HashableUSize Key := ⟨getHash⟩
|
||||
end OwnedSet
|
||||
|
||||
open OwnedSet (Key) in
|
||||
|
|
@ -41,10 +41,10 @@ inductive Key where
|
|||
deriving BEq
|
||||
|
||||
def getHash : Key → USize
|
||||
| Key.decl n => hash n
|
||||
| Key.jp n id => mixUSizeHash (hash n) (hash id)
|
||||
| Key.decl n => hashUSize n
|
||||
| Key.jp n id => mixUSizeHash (hashUSize n) (hashUSize id)
|
||||
|
||||
instance : Hashable Key := ⟨getHash⟩
|
||||
instance : HashableUSize Key := ⟨getHash⟩
|
||||
end ParamMap
|
||||
|
||||
open ParamMap (Key)
|
||||
|
|
|
|||
|
|
@ -27,13 +27,13 @@ open Std (HashMap PHashMap)
|
|||
that an entry was "removed" from the hashtable.
|
||||
- We do not need additional bookkeeping for extracting the local entries.
|
||||
-/
|
||||
structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
|
||||
structure SMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] where
|
||||
stage₁ : Bool := true
|
||||
map₁ : HashMap α β := {}
|
||||
map₂ : PHashMap α β := {}
|
||||
|
||||
namespace SMap
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
|
||||
|
||||
instance : Inhabited (SMap α β) := ⟨{}⟩
|
||||
def empty : SMap α β := {}
|
||||
|
|
@ -92,10 +92,10 @@ def toList (m : SMap α β) : List (α × β) :=
|
|||
|
||||
end SMap
|
||||
|
||||
def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
|
||||
def List.toSMap [BEq α] [HashableUSize α] (es : List (α × β)) : SMap α β :=
|
||||
es.foldl (init := {}) fun s (a, b) => s.insert a b
|
||||
|
||||
instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where
|
||||
instance {_ : BEq α} {_ : HashableUSize α} [Repr α] [Repr β] : Repr (SMap α β) where
|
||||
reprPrec v prec := Repr.addAppParen (reprArg v.toList ++ ".toSMap") prec
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -61,9 +61,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
|
|||
let binders := header.binders
|
||||
if ctx.usePartial then
|
||||
-- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
|
||||
`(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
|
||||
`(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
|
||||
else
|
||||
`(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
|
||||
`(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
|
||||
|
||||
def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
|
||||
let mut auxDefs := #[]
|
||||
|
|
@ -86,5 +86,5 @@ def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
|
|||
return false
|
||||
|
||||
builtin_initialize
|
||||
registerBuiltinDerivingHandler ``Hashable mkHashableHandler
|
||||
registerTraceClass `Elab.Deriving.hashable
|
||||
registerBuiltinDerivingHandler ``HashableUSize mkHashableHandler
|
||||
registerTraceClass `Elab.Deriving.hashable
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ instance [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) where
|
|||
instance [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
|
||||
inferInstanceAs (MonadRecDepth (ReaderT _ _))
|
||||
|
||||
instance [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
|
||||
instance [BEq α] [HashableUSize α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
|
||||
inferInstanceAs (MonadRecDepth (StateRefT' _ _ _))
|
||||
|
||||
@[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
|
||||
|
|
|
|||
|
|
@ -14,10 +14,10 @@ inductive Literal where
|
|||
deriving Inhabited, BEq
|
||||
|
||||
protected def Literal.hash : Literal → USize
|
||||
| Literal.natVal v => hash v
|
||||
| Literal.strVal v => hash v
|
||||
| Literal.natVal v => hashUSize v
|
||||
| Literal.strVal v => hashUSize v
|
||||
|
||||
instance : Hashable Literal := ⟨Literal.hash⟩
|
||||
instance : HashableUSize Literal := ⟨Literal.hash⟩
|
||||
|
||||
def Literal.lt : Literal → Literal → Bool
|
||||
| Literal.natVal _, Literal.strVal _ => true
|
||||
|
|
@ -47,7 +47,7 @@ def BinderInfo.isExplicit : BinderInfo → Bool
|
|||
| BinderInfo.instImplicit => false
|
||||
| _ => true
|
||||
|
||||
instance : Hashable BinderInfo := ⟨BinderInfo.hash⟩
|
||||
instance : HashableUSize BinderInfo := ⟨BinderInfo.hash⟩
|
||||
|
||||
def BinderInfo.isInstImplicit : BinderInfo → Bool
|
||||
| BinderInfo.instImplicit => true
|
||||
|
|
@ -201,7 +201,7 @@ def ctorName : Expr → String
|
|||
protected def hash (e : Expr) : USize :=
|
||||
e.data.hash
|
||||
|
||||
instance : Hashable Expr := ⟨Expr.hash⟩
|
||||
instance : HashableUSize Expr := ⟨Expr.hash⟩
|
||||
|
||||
def hasFVar (e : Expr) : Bool :=
|
||||
e.data.hasFVar
|
||||
|
|
@ -225,7 +225,7 @@ def looseBVarRange (e : Expr) : Nat :=
|
|||
def binderInfo (e : Expr) : BinderInfo :=
|
||||
e.data.binderInfo
|
||||
|
||||
@[export lean_expr_hash] def hashEx : Expr → USize := hash
|
||||
@[export lean_expr_hash] def hashEx : Expr → USize := hashUSize
|
||||
@[export lean_expr_has_fvar] def hasFVarEx : Expr → Bool := hasFVar
|
||||
@[export lean_expr_has_expr_mvar] def hasExprMVarEx : Expr → Bool := hasExprMVar
|
||||
@[export lean_expr_has_level_mvar] def hasLevelMVarEx : Expr → Bool := hasLevelMVar
|
||||
|
|
@ -237,7 +237,7 @@ def binderInfo (e : Expr) : BinderInfo :=
|
|||
end Expr
|
||||
|
||||
def mkLit (l : Literal) : Expr :=
|
||||
Expr.lit l $ mkData (mixUSizeHash 3 (hash l))
|
||||
Expr.lit l $ mkData (mixUSizeHash 3 (hashUSize l))
|
||||
|
||||
def mkNatLit (n : Nat) : Expr :=
|
||||
mkLit (Literal.natVal n)
|
||||
|
|
@ -246,7 +246,7 @@ def mkStrLit (s : String) : Expr :=
|
|||
mkLit (Literal.strVal s)
|
||||
|
||||
def mkConst (n : Name) (lvls : List Level := []) : Expr :=
|
||||
Expr.const n lvls $ mkData (mixUSizeHash 5 $ mixUSizeHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
|
||||
Expr.const n lvls $ mkData (mixUSizeHash 5 $ mixUSizeHash (hashUSize n) (hashUSize lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
|
||||
|
||||
def Literal.type : Literal → Expr
|
||||
| Literal.natVal _ => mkConst `Nat
|
||||
|
|
@ -256,26 +256,26 @@ def Literal.type : Literal → Expr
|
|||
def Literal.typeEx : Literal → Expr := Literal.type
|
||||
|
||||
def mkBVar (idx : Nat) : Expr :=
|
||||
Expr.bvar idx $ mkData (mixUSizeHash 7 $ hash idx) (idx+1)
|
||||
Expr.bvar idx $ mkData (mixUSizeHash 7 $ hashUSize idx) (idx+1)
|
||||
|
||||
def mkSort (lvl : Level) : Expr :=
|
||||
Expr.sort lvl $ mkData (mixUSizeHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
|
||||
Expr.sort lvl $ mkData (mixUSizeHash 11 $ hashUSize lvl) 0 false false lvl.hasMVar lvl.hasParam
|
||||
|
||||
def mkFVar (fvarId : FVarId) : Expr :=
|
||||
Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hash fvarId) 0 true
|
||||
Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hashUSize fvarId) 0 true
|
||||
|
||||
def mkMVar (fvarId : MVarId) : Expr :=
|
||||
Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hash fvarId) 0 false true
|
||||
Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hashUSize fvarId) 0 false true
|
||||
|
||||
def mkMData (d : MData) (e : Expr) : Expr :=
|
||||
Expr.mdata d e $ mkData (mixUSizeHash 19 $ hash e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
|
||||
Expr.mdata d e $ mkData (mixUSizeHash 19 $ hashUSize e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
|
||||
|
||||
def mkProj (s : Name) (i : Nat) (e : Expr) : Expr :=
|
||||
Expr.proj s i e $ mkData (mixUSizeHash 23 $ mixUSizeHash (hash s) $ mixUSizeHash (hash i) (hash e))
|
||||
Expr.proj s i e $ mkData (mixUSizeHash 23 $ mixUSizeHash (hashUSize s) $ mixUSizeHash (hashUSize i) (hashUSize e))
|
||||
e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
|
||||
|
||||
def mkApp (f a : Expr) : Expr :=
|
||||
Expr.app f a $ mkData (mixUSizeHash 29 $ mixUSizeHash (hash f) (hash a))
|
||||
Expr.app f a $ mkData (mixUSizeHash 29 $ mixUSizeHash (hashUSize f) (hashUSize a))
|
||||
(Nat.max f.looseBVarRange a.looseBVarRange)
|
||||
(f.hasFVar || a.hasFVar)
|
||||
(f.hasExprMVar || a.hasExprMVar)
|
||||
|
|
@ -284,7 +284,7 @@ def mkApp (f a : Expr) : Expr :=
|
|||
|
||||
def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
|
||||
-- let x := x.eraseMacroScopes
|
||||
Expr.lam x t b $ mkDataForBinder (mixUSizeHash 31 $ mixUSizeHash (hash t) (hash b))
|
||||
Expr.lam x t b $ mkDataForBinder (mixUSizeHash 31 $ mixUSizeHash (hashUSize t) (hashUSize b))
|
||||
(Nat.max t.looseBVarRange (b.looseBVarRange - 1))
|
||||
(t.hasFVar || b.hasFVar)
|
||||
(t.hasExprMVar || b.hasExprMVar)
|
||||
|
|
@ -294,7 +294,7 @@ def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
|
|||
|
||||
def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
|
||||
-- let x := x.eraseMacroScopes
|
||||
Expr.forallE x t b $ mkDataForBinder (mixUSizeHash 37 $ mixUSizeHash (hash t) (hash b))
|
||||
Expr.forallE x t b $ mkDataForBinder (mixUSizeHash 37 $ mixUSizeHash (hashUSize t) (hashUSize b))
|
||||
(Nat.max t.looseBVarRange (b.looseBVarRange - 1))
|
||||
(t.hasFVar || b.hasFVar)
|
||||
(t.hasExprMVar || b.hasExprMVar)
|
||||
|
|
@ -312,7 +312,7 @@ def mkSimpleThunk (type : Expr) : Expr :=
|
|||
|
||||
def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
|
||||
-- let x := x.eraseMacroScopes
|
||||
Expr.letE x t v b $ mkDataForLet (mixUSizeHash 41 $ mixUSizeHash (hash t) $ mixUSizeHash (hash v) (hash b))
|
||||
Expr.letE x t v b $ mkDataForLet (mixUSizeHash 41 $ mixUSizeHash (hashUSize t) $ mixUSizeHash (hashUSize v) (hashUSize b))
|
||||
(Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
|
||||
(t.hasFVar || v.hasFVar || b.hasFVar)
|
||||
(t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
|
||||
|
|
@ -719,7 +719,7 @@ protected def hash : ExprStructEq → USize
|
|||
| ⟨e⟩ => e.hash
|
||||
|
||||
instance : BEq ExprStructEq := ⟨ExprStructEq.beq⟩
|
||||
instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
|
||||
instance : HashableUSize ExprStructEq := ⟨ExprStructEq.hash⟩
|
||||
instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩
|
||||
|
||||
end ExprStructEq
|
||||
|
|
|
|||
|
|
@ -21,16 +21,16 @@ inductive HeadIndex where
|
|||
namespace HeadIndex
|
||||
|
||||
protected def HeadIndex.hash : HeadIndex → USize
|
||||
| fvar fvarId => mixUSizeHash 11 $ hash fvarId
|
||||
| mvar mvarId => mixUSizeHash 13 $ hash mvarId
|
||||
| const constName => mixUSizeHash 17 $ hash constName
|
||||
| proj structName idx => mixUSizeHash 19 $ mixUSizeHash (hash structName) (hash idx)
|
||||
| lit litVal => mixUSizeHash 23 $ hash litVal
|
||||
| fvar fvarId => mixUSizeHash 11 $ hashUSize fvarId
|
||||
| mvar mvarId => mixUSizeHash 13 $ hashUSize mvarId
|
||||
| const constName => mixUSizeHash 17 $ hashUSize constName
|
||||
| proj structName idx => mixUSizeHash 19 $ mixUSizeHash (hashUSize structName) (hashUSize idx)
|
||||
| lit litVal => mixUSizeHash 23 $ hashUSize litVal
|
||||
| sort => 29
|
||||
| lam => 31
|
||||
| forallE => 37
|
||||
|
||||
instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
|
||||
instance : HashableUSize HeadIndex := ⟨HeadIndex.hash⟩
|
||||
|
||||
end HeadIndex
|
||||
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ namespace Level
|
|||
protected def hash (u : Level) : USize :=
|
||||
u.data.hash
|
||||
|
||||
instance : Hashable Level := ⟨Level.hash⟩
|
||||
instance : HashableUSize Level := ⟨Level.hash⟩
|
||||
|
||||
def depth (u : Level) : Nat :=
|
||||
u.data.depth.toNat
|
||||
|
|
@ -94,21 +94,21 @@ def levelZero :=
|
|||
Level.zero $ mkData 2221 0 false false
|
||||
|
||||
def mkLevelMVar (mvarId : Name) :=
|
||||
Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hash mvarId) 0 true false
|
||||
Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hashUSize mvarId) 0 true false
|
||||
|
||||
def mkLevelParam (name : Name) :=
|
||||
Level.param name $ mkData (mixUSizeHash 2239 $ hash name) 0 false true
|
||||
Level.param name $ mkData (mixUSizeHash 2239 $ hashUSize name) 0 false true
|
||||
|
||||
def mkLevelSucc (u : Level) :=
|
||||
Level.succ u $ mkData (mixUSizeHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
|
||||
Level.succ u $ mkData (mixUSizeHash 2243 $ hashUSize u) (u.depth + 1) u.hasMVar u.hasParam
|
||||
|
||||
def mkLevelMax (u v : Level) :=
|
||||
Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
|
||||
Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
|
||||
(u.hasMVar || v.hasMVar)
|
||||
(u.hasParam || v.hasParam)
|
||||
|
||||
def mkLevelIMax (u v : Level) :=
|
||||
Level.imax u v $ mkData (mixUSizeHash 2267 $ mixUSizeHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
|
||||
Level.imax u v $ mkData (mixUSizeHash 2267 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
|
||||
(u.hasMVar || v.hasMVar)
|
||||
(u.hasParam || v.hasParam)
|
||||
|
||||
|
|
|
|||
|
|
@ -80,8 +80,8 @@ structure InfoCacheKey where
|
|||
deriving Inhabited, BEq
|
||||
|
||||
namespace InfoCacheKey
|
||||
instance : Hashable InfoCacheKey :=
|
||||
⟨fun ⟨transparency, expr, nargs⟩ => mixUSizeHash (hash transparency) <| mixUSizeHash (hash expr) (hash nargs)⟩
|
||||
instance : HashableUSize InfoCacheKey :=
|
||||
⟨fun ⟨transparency, expr, nargs⟩ => mixUSizeHash (hashUSize transparency) <| mixUSizeHash (hashUSize expr) (hashUSize nargs)⟩
|
||||
end InfoCacheKey
|
||||
|
||||
open Std (PersistentArray PersistentHashMap)
|
||||
|
|
|
|||
|
|
@ -21,14 +21,14 @@ inductive Key where
|
|||
deriving Inhabited, BEq
|
||||
|
||||
protected def Key.hash : Key → USize
|
||||
| Key.const n a => mixUSizeHash 5237 $ mixUSizeHash (hash n) (hash a)
|
||||
| Key.fvar n a => mixUSizeHash 3541 $ mixUSizeHash (hash n) (hash a)
|
||||
| Key.lit v => mixUSizeHash 1879 $ hash v
|
||||
| Key.const n a => mixUSizeHash 5237 $ mixUSizeHash (hashUSize n) (hashUSize a)
|
||||
| Key.fvar n a => mixUSizeHash 3541 $ mixUSizeHash (hashUSize n) (hashUSize a)
|
||||
| Key.lit v => mixUSizeHash 1879 $ hashUSize v
|
||||
| Key.star => 7883
|
||||
| Key.other => 2411
|
||||
| Key.arrow => 17
|
||||
|
||||
instance : Hashable Key := ⟨Key.hash⟩
|
||||
instance : HashableUSize Key := ⟨Key.hash⟩
|
||||
|
||||
inductive Trie (α : Type) where
|
||||
| node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ def hash : TransparencyMode → USize
|
|||
| reducible => 13
|
||||
| instances => 17
|
||||
|
||||
instance : Hashable TransparencyMode := ⟨hash⟩
|
||||
instance : HashableUSize TransparencyMode := ⟨hash⟩
|
||||
|
||||
def lt : TransparencyMode → TransparencyMode → Bool
|
||||
| reducible, default => true
|
||||
|
|
|
|||
|
|
@ -33,30 +33,30 @@ open Std (HashMap)
|
|||
|
||||
/-- Adapter for implementing `MonadCache` interface using `HashMap`s.
|
||||
We just have to specify how to extract/modify the `HashMap`. -/
|
||||
class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] where
|
||||
class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [HashableUSize α] where
|
||||
getCache : m (HashMap α β)
|
||||
modifyCache : (HashMap α β → HashMap α β) → m Unit
|
||||
|
||||
namespace MonadHashMapCacheAdapter
|
||||
|
||||
@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
|
||||
@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
|
||||
let c ← getCache
|
||||
pure (c.find? a)
|
||||
|
||||
@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
|
||||
@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
|
||||
modifyCache fun s => s.insert a b
|
||||
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
|
||||
findCached? := MonadHashMapCacheAdapter.findCached?
|
||||
cache := MonadHashMapCacheAdapter.cache
|
||||
|
||||
end MonadHashMapCacheAdapter
|
||||
|
||||
def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m
|
||||
def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [HashableUSize α] := StateRefT (HashMap α β) m
|
||||
|
||||
namespace MonadCacheT
|
||||
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
|
||||
getCache := (get : StateRefT' ..)
|
||||
|
|
@ -75,11 +75,11 @@ instance [MonadRef m] : MonadRef (MonadCacheT α β m) := inferInstanceAs (Monad
|
|||
end MonadCacheT
|
||||
|
||||
/- Similar to `MonadCacheT`, but using `StateT` instead of `StateRefT` -/
|
||||
def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := StateT (HashMap α β) m
|
||||
def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [HashableUSize α] := StateT (HashMap α β) m
|
||||
|
||||
namespace MonadStateCacheT
|
||||
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
|
||||
getCache := (get : StateT ..)
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ namespace Lean.SCC
|
|||
open Std
|
||||
|
||||
section
|
||||
variable (α : Type) [BEq α] [Hashable α]
|
||||
variable (α : Type) [BEq α] [HashableUSize α]
|
||||
|
||||
structure Data where
|
||||
index? : Option Nat := none
|
||||
|
|
@ -30,7 +30,7 @@ structure State where
|
|||
abbrev M := StateM (State α)
|
||||
end
|
||||
|
||||
variable {α : Type} [BEq α] [Hashable α]
|
||||
variable {α : Type} [BEq α] [HashableUSize α]
|
||||
|
||||
private def getDataOf (a : α) : M α Data := do
|
||||
let s ← get
|
||||
|
|
|
|||
|
|
@ -53,46 +53,46 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
|
|||
@[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMapImp α β) : m PUnit :=
|
||||
forBucketsM h.buckets f
|
||||
|
||||
def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
|
||||
def findEntry? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
(buckets.val.uget i h).findEntry? a
|
||||
|
||||
def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
|
||||
def find? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option β :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
(buckets.val.uget i h).find? a
|
||||
|
||||
def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
|
||||
def contains [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Bool :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
(buckets.val.uget i h).contains a
|
||||
|
||||
-- TODO: remove `partial` by using well-founded recursion
|
||||
partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
|
||||
partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
|
||||
if h : i < source.size then
|
||||
let idx : Fin source.size := ⟨i, h⟩
|
||||
let es : AssocList α β := source.get idx
|
||||
-- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
|
||||
let source := source.set idx AssocList.nil
|
||||
let target := es.foldl (reinsertAux hash) target
|
||||
let target := es.foldl (reinsertAux hashUSize) target
|
||||
moveEntries (i+1) source target
|
||||
else target
|
||||
|
||||
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
|
||||
def expand [HashableUSize α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
|
||||
let nbuckets := buckets.val.size * 2
|
||||
have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
|
||||
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by simp; assumption⟩
|
||||
{ size := size,
|
||||
buckets := moveEntries 0 buckets.val new_buckets }
|
||||
|
||||
def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
|
||||
def insert [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
|
||||
match m with
|
||||
| ⟨size, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let bkt := buckets.val.uget i h
|
||||
if bkt.contains a then
|
||||
⟨size, buckets.update i (bkt.replace a b) h⟩
|
||||
|
|
@ -104,31 +104,31 @@ def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : Has
|
|||
else
|
||||
expand size' buckets'
|
||||
|
||||
def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
|
||||
def erase [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
|
||||
match m with
|
||||
| ⟨ size, buckets ⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let bkt := buckets.val.uget i h
|
||||
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
|
||||
else m
|
||||
|
||||
inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
|
||||
inductive WellFormed [BEq α] [HashableUSize α] : HashMapImp α β → Prop where
|
||||
| mkWff : ∀ n, WellFormed (mkHashMapImp n)
|
||||
| insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b)
|
||||
| eraseWff : ∀ m a, WellFormed m → WellFormed (erase m a)
|
||||
|
||||
end HashMapImp
|
||||
|
||||
def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
|
||||
def HashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] :=
|
||||
{ m : HashMapImp α β // m.WellFormed }
|
||||
|
||||
open Std.HashMapImp
|
||||
|
||||
def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
|
||||
def mkHashMap {α : Type u} {β : Type v} [BEq α] [HashableUSize α] (nbuckets := 8) : HashMap α β :=
|
||||
⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
|
||||
|
||||
namespace HashMap
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
|
||||
|
||||
instance : Inhabited (HashMap α β) where
|
||||
default := mkHashMap
|
||||
|
|
|
|||
|
|
@ -46,40 +46,40 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
|
|||
@[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
|
||||
foldBuckets m.buckets d f
|
||||
|
||||
def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
|
||||
def find? [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Option α :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
(buckets.val.uget i h).find? (fun a' => a == a')
|
||||
|
||||
def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
|
||||
def contains [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Bool :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
(buckets.val.uget i h).contains a
|
||||
|
||||
-- TODO: remove `partial` by using well-founded recursion
|
||||
partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
|
||||
partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
|
||||
if h : i < source.size then
|
||||
let idx : Fin source.size := ⟨i, h⟩
|
||||
let es : List α := source.get idx
|
||||
-- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
|
||||
let source := source.set idx []
|
||||
let target := es.foldl (reinsertAux hash) target
|
||||
let target := es.foldl (reinsertAux hashUSize) target
|
||||
moveEntries (i+1) source target
|
||||
else target
|
||||
|
||||
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
|
||||
def expand [HashableUSize α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
|
||||
let nbuckets := buckets.val.size * 2
|
||||
have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
|
||||
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.size_mkArray]; assumption⟩
|
||||
{ size := size,
|
||||
buckets := moveEntries 0 buckets.val new_buckets }
|
||||
|
||||
def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
def insert [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
match m with
|
||||
| ⟨size, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let bkt := buckets.val.uget i h
|
||||
if bkt.contains a
|
||||
then ⟨size, buckets.update i (bkt.replace a a) h⟩
|
||||
|
|
@ -90,31 +90,31 @@ def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :
|
|||
then { size := size', buckets := buckets' }
|
||||
else expand size' buckets'
|
||||
|
||||
def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
def erase [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
match m with
|
||||
| ⟨ size, buckets ⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let bkt := buckets.val.uget i h
|
||||
if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
|
||||
else m
|
||||
|
||||
inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop where
|
||||
inductive WellFormed [BEq α] [HashableUSize α] : HashSetImp α → Prop where
|
||||
| mkWff : ∀ n, WellFormed (mkHashSetImp n)
|
||||
| insertWff : ∀ m a, WellFormed m → WellFormed (insert m a)
|
||||
| eraseWff : ∀ m a, WellFormed m → WellFormed (erase m a)
|
||||
|
||||
end HashSetImp
|
||||
|
||||
def HashSet (α : Type u) [BEq α] [Hashable α] :=
|
||||
def HashSet (α : Type u) [BEq α] [HashableUSize α] :=
|
||||
{ m : HashSetImp α // m.WellFormed }
|
||||
|
||||
open HashSetImp
|
||||
|
||||
def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α :=
|
||||
def mkHashSet {α : Type u} [BEq α] [HashableUSize α] (nbuckets := 8) : HashSet α :=
|
||||
⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
|
||||
|
||||
namespace HashSet
|
||||
variable {α : Type u} [BEq α] [Hashable α]
|
||||
variable {α : Type u} [BEq α] [HashableUSize α]
|
||||
|
||||
instance : Inhabited (HashSet α) where
|
||||
default := mkHashSet
|
||||
|
|
|
|||
|
|
@ -31,21 +31,21 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
|
|||
|
||||
end PersistentHashMap
|
||||
|
||||
structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
|
||||
structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] where
|
||||
root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
|
||||
size : Nat := 0
|
||||
|
||||
abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
|
||||
abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] := PersistentHashMap α β
|
||||
|
||||
namespace PersistentHashMap
|
||||
variable {α : Type u} {β : Type v}
|
||||
|
||||
def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
|
||||
def empty [BEq α] [HashableUSize α] : PersistentHashMap α β := {}
|
||||
|
||||
def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
|
||||
def isEmpty [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Bool :=
|
||||
m.size == 0
|
||||
|
||||
instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
|
||||
instance [BEq α] [HashableUSize α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
|
||||
|
||||
def mkEmptyEntries {α β} : Node α β :=
|
||||
Node.entries mkEmptyEntriesArray
|
||||
|
|
@ -98,7 +98,7 @@ def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β
|
|||
let vs := (vs.push v₁).push v₂
|
||||
Node.collision ks vs rfl
|
||||
|
||||
partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
|
||||
partial def insertAux [BEq α] [HashableUSize α] : Node α β → USize → USize → α → β → Node α β
|
||||
| Node.collision keys vals heq, _, depth, k, v =>
|
||||
let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
|
||||
if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
|
||||
|
|
@ -109,7 +109,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
|
|||
if h : i < keys.size then
|
||||
let k := keys.get ⟨i, h⟩
|
||||
let v := vals.get ⟨i, heq ▸ h⟩
|
||||
let h := hash k
|
||||
let h := hashUSize k
|
||||
let h := div2Shift h (shift * (depth - 1))
|
||||
traverse (i+1) (insertAux entries h depth k v)
|
||||
else
|
||||
|
|
@ -125,8 +125,8 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
|
|||
if k == k' then Entry.entry k v
|
||||
else Entry.ref $ mkCollisionNode k' v' k v
|
||||
|
||||
def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k, v => { root := insertAux n (hash k) 1 k v, size := sz + 1 }
|
||||
def insert [BEq α] [HashableUSize α] : PersistentHashMap α β → α → β → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k, v => { root := insertAux n (hashUSize k) 1 k v, size := sz + 1 }
|
||||
|
||||
partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
|
||||
if h : i < keys.size then
|
||||
|
|
@ -144,16 +144,16 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
|
|||
| Entry.entry k' v => if k == k' then some v else none
|
||||
| Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
|
||||
|
||||
def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
|
||||
| { root := n, .. }, k => findAux n (hash k) k
|
||||
def find? [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Option β
|
||||
| { root := n, .. }, k => findAux n (hashUSize k) k
|
||||
|
||||
@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
|
||||
@[inline] def getOp [BEq α] [HashableUSize α] (self : PersistentHashMap α β) (idx : α) : Option β :=
|
||||
self.find? idx
|
||||
|
||||
@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
|
||||
@[inline] def findD [BEq α] [HashableUSize α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
|
||||
(m.find? a).getD b₀
|
||||
|
||||
@[inline] def find! [BEq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
|
||||
@[inline] def find! [BEq α] [HashableUSize α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
|
||||
match m.find? a with
|
||||
| some b => b
|
||||
| none => panic! "key is not in the map"
|
||||
|
|
@ -174,8 +174,8 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
|
|||
| Entry.entry k' v => if k == k' then some (k', v) else none
|
||||
| Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
|
||||
|
||||
def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
|
||||
| { root := n, .. }, k => findEntryAux n (hash k) k
|
||||
def findEntry? [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Option (α × β)
|
||||
| { root := n, .. }, k => findEntryAux n (hashUSize k) k
|
||||
|
||||
partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
|
||||
if h : i < keys.size then
|
||||
|
|
@ -193,8 +193,8 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
|
|||
| Entry.entry k' v => k == k'
|
||||
| Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
|
||||
|
||||
def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
|
||||
| { root := n, .. }, k => containsAux n (hash k) k
|
||||
def contains [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Bool
|
||||
| { root := n, .. }, k => containsAux n (hashUSize k) k
|
||||
|
||||
partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
|
||||
if h : i < a.size then
|
||||
|
|
@ -240,9 +240,9 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
|
|||
| none => (Node.entries (entries.set! j (Entry.ref newNode)), true)
|
||||
| some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
|
||||
|
||||
def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
|
||||
def erase [BEq α] [HashableUSize α] : PersistentHashMap α β → α → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k =>
|
||||
let h := hash k
|
||||
let h := hashUSize k
|
||||
let (n, del) := eraseAux n h k
|
||||
{ root := n, size := if del then sz - 1 else sz }
|
||||
|
||||
|
|
@ -267,17 +267,17 @@ variable {σ : Type w}
|
|||
| Entry.ref node => foldlMAux f node acc)
|
||||
acc
|
||||
|
||||
@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
|
||||
@[specialize] def foldlM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
|
||||
foldlMAux f map.root init
|
||||
|
||||
@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
|
||||
@[specialize] def forM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
|
||||
map.foldlM (fun _ => f) ⟨⟩
|
||||
|
||||
@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
|
||||
@[specialize] def foldl [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
|
||||
Id.run $ map.foldlM f init
|
||||
end
|
||||
|
||||
def toList [BEq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) :=
|
||||
def toList [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : List (α × β) :=
|
||||
m.foldl (init := []) fun ps k v => (k, v) :: ps
|
||||
|
||||
structure Stats where
|
||||
|
|
@ -304,7 +304,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
|
|||
| Entry.entry _ _ => stats)
|
||||
stats
|
||||
|
||||
def stats [BEq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
|
||||
def stats [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Stats :=
|
||||
collectStats m.root {} 1
|
||||
|
||||
def Stats.toString (s : Stats) : String :=
|
||||
|
|
|
|||
|
|
@ -8,14 +8,14 @@ import Std.Data.PersistentHashMap
|
|||
namespace Std
|
||||
universes u v
|
||||
|
||||
structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
|
||||
structure PersistentHashSet (α : Type u) [BEq α] [HashableUSize α] where
|
||||
(set : PersistentHashMap α Unit)
|
||||
|
||||
abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
|
||||
abbrev PHashSet (α : Type u) [BEq α] [HashableUSize α] := PersistentHashSet α
|
||||
|
||||
namespace PersistentHashSet
|
||||
|
||||
variable {α : Type u} [BEq α] [Hashable α]
|
||||
variable {α : Type u} [BEq α] [HashableUSize α]
|
||||
|
||||
@[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
|
||||
s.set.isEmpty
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue