chore: remove HashableUSize
This commit is contained in:
Leonardo de Moura
parent
37da993032
commit
7424f9c8b0
14 changed files with 107 additions and 118 deletions
|
|
@ -1587,11 +1587,6 @@ instance nonBacktrackable : Backtrackable PUnit σ where
|
|||
|
||||
end EStateM
|
||||
|
||||
class HashableUSize (α : Sort u) where
|
||||
hashUSize : α → USize
|
||||
|
||||
export HashableUSize (hashUSize)
|
||||
|
||||
class Hashable (α : Sort u) where
|
||||
hash : α → UInt64
|
||||
|
||||
|
|
@ -1603,15 +1598,9 @@ constant UInt64.toUSize (u : UInt64) : USize
|
|||
@[extern c inline "(uint64_t)#1"]
|
||||
constant USize.toUInt64 (u : USize) : UInt64
|
||||
|
||||
instance [Hashable α] : HashableUSize α where
|
||||
hashUSize n := hash n |>.toUSize
|
||||
|
||||
@[extern "lean_uint64_mix_hash"]
|
||||
constant mixHash (u₁ u₂ : UInt64) : UInt64
|
||||
|
||||
@[extern "lean_usize_mix_hash"]
|
||||
constant mixUSizeHash (u₁ u₂ : USize) : USize
|
||||
|
||||
@[extern "lean_string_hash"]
|
||||
protected constant String.hash (s : @& String) : UInt64
|
||||
|
||||
|
|
|
|||
|
|
@ -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 α] [HashableUSize α] where
|
||||
structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
|
||||
stage₁ : Bool := true
|
||||
map₁ : HashMap α β := {}
|
||||
map₂ : PHashMap α β := {}
|
||||
|
||||
namespace SMap
|
||||
variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
|
||||
instance : Inhabited (SMap α β) := ⟨{}⟩
|
||||
def empty : SMap α β := {}
|
||||
|
|
@ -92,10 +92,10 @@ def toList (m : SMap α β) : List (α × β) :=
|
|||
|
||||
end SMap
|
||||
|
||||
def List.toSMap [BEq α] [HashableUSize α] (es : List (α × β)) : SMap α β :=
|
||||
def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
|
||||
es.foldl (init := {}) fun s (a, b) => s.insert a b
|
||||
|
||||
instance {_ : BEq α} {_ : HashableUSize α} [Repr α] [Repr β] : Repr (SMap α β) where
|
||||
instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where
|
||||
reprPrec v prec := Repr.addAppParen (reprArg v.toList ++ ".toSMap") prec
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -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 α] [HashableUSize α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
|
||||
instance [BEq α] [Hashable α] [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
|
||||
|
|
|
|||
|
|
@ -121,7 +121,7 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
|
|||
| BinderInfo.auxDecl => 4
|
||||
|
||||
@[inline] private def Expr.mkDataCore
|
||||
(h : USize) (looseBVarRange : Nat)
|
||||
(h : UInt64) (looseBVarRange : Nat)
|
||||
(hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo)
|
||||
: Expr.Data :=
|
||||
if looseBVarRange > Nat.pow 2 24 - 1 then panic! "bound variable index is too big"
|
||||
|
|
@ -137,13 +137,13 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
|
|||
looseBVarRange.toUInt64.shiftLeft 40
|
||||
r
|
||||
|
||||
def Expr.mkData (h : USize) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
|
||||
def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
|
||||
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
|
||||
|
||||
def Expr.mkDataForBinder (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
|
||||
def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
|
||||
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
|
||||
|
||||
def Expr.mkDataForLet (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
|
||||
def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
|
||||
Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
|
||||
|
||||
open Expr
|
||||
|
|
@ -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 := hashUSize
|
||||
@[export lean_expr_hash] def hashEx : Expr → UInt64 := hash
|
||||
@[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 (hashUSize l))
|
||||
Expr.lit l $ mkData (mixHash 3 (hash 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 (hashUSize n) (hashUSize lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
|
||||
Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash 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 $ hashUSize idx) (idx+1)
|
||||
Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1)
|
||||
|
||||
def mkSort (lvl : Level) : Expr :=
|
||||
Expr.sort lvl $ mkData (mixUSizeHash 11 $ hashUSize lvl) 0 false false lvl.hasMVar lvl.hasParam
|
||||
Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
|
||||
|
||||
def mkFVar (fvarId : FVarId) : Expr :=
|
||||
Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hashUSize fvarId) 0 true
|
||||
Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true
|
||||
|
||||
def mkMVar (fvarId : MVarId) : Expr :=
|
||||
Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hashUSize fvarId) 0 false true
|
||||
Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true
|
||||
|
||||
def mkMData (d : MData) (e : Expr) : Expr :=
|
||||
Expr.mdata d e $ mkData (mixUSizeHash 19 $ hashUSize e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
|
||||
Expr.mdata d e $ mkData (mixHash 19 $ hash 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 (hashUSize s) $ mixUSizeHash (hashUSize i) (hashUSize e))
|
||||
Expr.proj s i e $ mkData (mixHash 23 $ mixHash (hash s) $ mixHash (hash i) (hash 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 (hashUSize f) (hashUSize a))
|
||||
Expr.app f a $ mkData (mixHash 29 $ mixHash (hash f) (hash 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 (hashUSize t) (hashUSize b))
|
||||
Expr.lam x t b $ mkDataForBinder (mixHash 31 $ mixHash (hash t) (hash 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 (hashUSize t) (hashUSize b))
|
||||
Expr.forallE x t b $ mkDataForBinder (mixHash 37 $ mixHash (hash t) (hash 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 (hashUSize t) $ mixUSizeHash (hashUSize v) (hashUSize b))
|
||||
Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash v) (hash b))
|
||||
(Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
|
||||
(t.hasFVar || v.hasFVar || b.hasFVar)
|
||||
(t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ def Level.Data.hasMVar (c : Level.Data) : Bool :=
|
|||
def Level.Data.hasParam (c : Level.Data) : Bool :=
|
||||
((c.shiftRight 33).land 1) == 1
|
||||
|
||||
def Level.mkData (h : USize) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
|
||||
def Level.mkData (h : UInt64) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
|
||||
if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
|
||||
else
|
||||
let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
|
||||
|
|
@ -94,21 +94,21 @@ def levelZero :=
|
|||
Level.zero $ mkData 2221 0 false false
|
||||
|
||||
def mkLevelMVar (mvarId : Name) :=
|
||||
Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hashUSize mvarId) 0 true false
|
||||
Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
|
||||
|
||||
def mkLevelParam (name : Name) :=
|
||||
Level.param name $ mkData (mixUSizeHash 2239 $ hashUSize name) 0 false true
|
||||
Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
|
||||
|
||||
def mkLevelSucc (u : Level) :=
|
||||
Level.succ u $ mkData (mixUSizeHash 2243 $ hashUSize u) (u.depth + 1) u.hasMVar u.hasParam
|
||||
Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
|
||||
|
||||
def mkLevelMax (u v : Level) :=
|
||||
Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
|
||||
Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash 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 (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
|
||||
Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
|
||||
(u.hasMVar || v.hasMVar)
|
||||
(u.hasParam || v.hasParam)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 α] [HashableUSize α] where
|
||||
class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] where
|
||||
getCache : m (HashMap α β)
|
||||
modifyCache : (HashMap α β → HashMap α β) → m Unit
|
||||
|
||||
namespace MonadHashMapCacheAdapter
|
||||
|
||||
@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
|
||||
@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
|
||||
let c ← getCache
|
||||
pure (c.find? a)
|
||||
|
||||
@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
|
||||
@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
|
||||
modifyCache fun s => s.insert a b
|
||||
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
|
||||
findCached? := MonadHashMapCacheAdapter.findCached?
|
||||
cache := MonadHashMapCacheAdapter.cache
|
||||
|
||||
end MonadHashMapCacheAdapter
|
||||
|
||||
def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [HashableUSize α] := StateRefT (HashMap α β) m
|
||||
def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m
|
||||
|
||||
namespace MonadCacheT
|
||||
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [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 α] [HashableUSize α] := StateT (HashMap α β) m
|
||||
def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := StateT (HashMap α β) m
|
||||
|
||||
namespace MonadStateCacheT
|
||||
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [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 α] [HashableUSize α]
|
||||
variable (α : Type) [BEq α] [Hashable α]
|
||||
|
||||
structure Data where
|
||||
index? : Option Nat := none
|
||||
|
|
@ -30,7 +30,7 @@ structure State where
|
|||
abbrev M := StateM (State α)
|
||||
end
|
||||
|
||||
variable {α : Type} [BEq α] [HashableUSize α]
|
||||
variable {α : Type} [BEq α] [Hashable α]
|
||||
|
||||
private def getDataOf (a : α) : M α Data := do
|
||||
let s ← get
|
||||
|
|
|
|||
|
|
@ -31,8 +31,8 @@ variable {α : Type u} {β : Type v}
|
|||
def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
|
||||
⟨u % n, USize.modn_lt _ h⟩
|
||||
|
||||
@[inline] def reinsertAux (hashFn : α → USize) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
|
||||
let ⟨i, h⟩ := mkIdx data.property (hashFn a)
|
||||
@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
|
||||
let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
|
||||
data.update i (AssocList.cons a b (data.val.uget i h)) h
|
||||
|
||||
@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
|
||||
|
|
@ -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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
|
||||
def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
(buckets.val.uget i h).findEntry? a
|
||||
|
||||
def find? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option β :=
|
||||
def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
(buckets.val.uget i h).find? a
|
||||
|
||||
def contains [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Bool :=
|
||||
def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
(buckets.val.uget i h).contains a
|
||||
|
||||
-- TODO: remove `partial` by using well-founded recursion
|
||||
partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
|
||||
partial def moveEntries [Hashable α] (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 hashUSize) target
|
||||
let target := es.foldl (reinsertAux hash) target
|
||||
moveEntries (i+1) source target
|
||||
else target
|
||||
|
||||
def expand [HashableUSize α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
|
||||
def expand [Hashable α] (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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
|
||||
def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
|
||||
match m with
|
||||
| ⟨size, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β)
|
|||
else
|
||||
expand size' buckets'
|
||||
|
||||
def erase [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
|
||||
def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
|
||||
match m with
|
||||
| ⟨ size, buckets ⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
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 α] [HashableUSize α] : HashMapImp α β → Prop where
|
||||
inductive WellFormed [BEq α] [Hashable α] : 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 α] [HashableUSize α] :=
|
||||
def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
|
||||
{ m : HashMapImp α β // m.WellFormed }
|
||||
|
||||
open Std.HashMapImp
|
||||
|
||||
def mkHashMap {α : Type u} {β : Type v} [BEq α] [HashableUSize α] (nbuckets := 8) : HashMap α β :=
|
||||
def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
|
||||
⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
|
||||
|
||||
namespace HashMap
|
||||
variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
|
||||
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
|
||||
|
||||
instance : Inhabited (HashMap α β) where
|
||||
default := mkHashMap
|
||||
|
|
|
|||
|
|
@ -30,8 +30,8 @@ variable {α : Type u}
|
|||
def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
|
||||
⟨u % n, USize.modn_lt _ h⟩
|
||||
|
||||
@[inline] def reinsertAux (hashFn : α → USize) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
|
||||
let ⟨i, h⟩ := mkIdx data.property (hashFn a)
|
||||
@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
|
||||
let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
|
||||
data.update i (a :: data.val.uget i h) h
|
||||
|
||||
@[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
|
||||
|
|
@ -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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : Option α :=
|
||||
def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
(buckets.val.uget i h).find? (fun a' => a == a')
|
||||
|
||||
def contains [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Bool :=
|
||||
def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
|
||||
match m with
|
||||
| ⟨_, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
(buckets.val.uget i h).contains a
|
||||
|
||||
-- TODO: remove `partial` by using well-founded recursion
|
||||
partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
|
||||
partial def moveEntries [Hashable α] (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 hashUSize) target
|
||||
let target := es.foldl (reinsertAux hash) target
|
||||
moveEntries (i+1) source target
|
||||
else target
|
||||
|
||||
def expand [HashableUSize α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
|
||||
def expand [Hashable α] (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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
match m with
|
||||
| ⟨size, buckets⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp
|
|||
then { size := size', buckets := buckets' }
|
||||
else expand size' buckets'
|
||||
|
||||
def erase [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
|
||||
match m with
|
||||
| ⟨ size, buckets ⟩ =>
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
|
||||
let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
|
||||
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 α] [HashableUSize α] : HashSetImp α → Prop where
|
||||
inductive WellFormed [BEq α] [Hashable α] : 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 α] [HashableUSize α] :=
|
||||
def HashSet (α : Type u) [BEq α] [Hashable α] :=
|
||||
{ m : HashSetImp α // m.WellFormed }
|
||||
|
||||
open HashSetImp
|
||||
|
||||
def mkHashSet {α : Type u} [BEq α] [HashableUSize α] (nbuckets := 8) : HashSet α :=
|
||||
def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α :=
|
||||
⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
|
||||
|
||||
namespace HashSet
|
||||
variable {α : Type u} [BEq α] [HashableUSize α]
|
||||
variable {α : Type u} [BEq α] [Hashable α]
|
||||
|
||||
instance : Inhabited (HashSet α) where
|
||||
default := mkHashSet
|
||||
|
|
|
|||
|
|
@ -31,21 +31,21 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
|
|||
|
||||
end PersistentHashMap
|
||||
|
||||
structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] where
|
||||
structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
|
||||
root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
|
||||
size : Nat := 0
|
||||
|
||||
abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] := PersistentHashMap α β
|
||||
abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
|
||||
|
||||
namespace PersistentHashMap
|
||||
variable {α : Type u} {β : Type v}
|
||||
|
||||
def empty [BEq α] [HashableUSize α] : PersistentHashMap α β := {}
|
||||
def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
|
||||
|
||||
def isEmpty [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Bool :=
|
||||
def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
|
||||
m.size == 0
|
||||
|
||||
instance [BEq α] [HashableUSize α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
|
||||
instance [BEq α] [Hashable α] : 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 α] [HashableUSize α] : Node α β → USize → USize → α → β → Node α β
|
||||
partial def insertAux [BEq α] [Hashable α] : 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 α] [HashableUSize α] : Node α β → USize → USi
|
|||
if h : i < keys.size then
|
||||
let k := keys.get ⟨i, h⟩
|
||||
let v := vals.get ⟨i, heq ▸ h⟩
|
||||
let h := hashUSize k
|
||||
let h := hash k |>.toUSize
|
||||
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 α] [HashableUSize α] : Node α β → USize → USi
|
|||
if k == k' then Entry.entry k v
|
||||
else Entry.ref $ mkCollisionNode k' v' k v
|
||||
|
||||
def insert [BEq α] [HashableUSize α] : PersistentHashMap α β → α → β → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k, v => { root := insertAux n (hashUSize k) 1 k v, size := sz + 1 }
|
||||
def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → Option β
|
||||
| { root := n, .. }, k => findAux n (hashUSize k) k
|
||||
def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
|
||||
| { root := n, .. }, k => findAux n (hash k |>.toUSize) k
|
||||
|
||||
@[inline] def getOp [BEq α] [HashableUSize α] (self : PersistentHashMap α β) (idx : α) : Option β :=
|
||||
@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
|
||||
self.find? idx
|
||||
|
||||
@[inline] def findD [BEq α] [HashableUSize α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
|
||||
@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
|
||||
(m.find? a).getD b₀
|
||||
|
||||
@[inline] def find! [BEq α] [HashableUSize α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
|
||||
@[inline] def find! [BEq α] [Hashable α] [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 α] [HashableUSize α] : PersistentHashMap α β → α → Option (α × β)
|
||||
| { root := n, .. }, k => findEntryAux n (hashUSize k) k
|
||||
def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
|
||||
| { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → Bool
|
||||
| { root := n, .. }, k => containsAux n (hashUSize k) k
|
||||
def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
|
||||
| { root := n, .. }, k => containsAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → PersistentHashMap α β
|
||||
def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
|
||||
| { root := n, size := sz }, k =>
|
||||
let h := hashUSize k
|
||||
let h := hash k |>.toUSize
|
||||
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 α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
|
||||
@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
|
||||
foldlMAux f map.root init
|
||||
|
||||
@[specialize] def forM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
|
||||
@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
|
||||
map.foldlM (fun _ => f) ⟨⟩
|
||||
|
||||
@[specialize] def foldl [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
|
||||
@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
|
||||
Id.run $ map.foldlM f init
|
||||
end
|
||||
|
||||
def toList [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : List (α × β) :=
|
||||
def toList [BEq α] [Hashable α] (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 α] [HashableUSize α] (m : PersistentHashMap α β) : Stats :=
|
||||
def stats [BEq α] [Hashable α] (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 α] [HashableUSize α] where
|
||||
structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
|
||||
(set : PersistentHashMap α Unit)
|
||||
|
||||
abbrev PHashSet (α : Type u) [BEq α] [HashableUSize α] := PersistentHashSet α
|
||||
abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
|
||||
|
||||
namespace PersistentHashSet
|
||||
|
||||
variable {α : Type u} [BEq α] [HashableUSize α]
|
||||
variable {α : Type u} [BEq α] [Hashable α]
|
||||
|
||||
@[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
|
||||
s.set.isEmpty
|
||||
|
|
|
|||
|
|
@ -23,14 +23,14 @@ abbrev Object : Type := NonScalar
|
|||
unsafe def Object.ptrEq (a b : Object) : Bool :=
|
||||
ptrAddrUnsafe a == ptrAddrUnsafe b
|
||||
|
||||
unsafe def Object.ptrHash (a : Object) : USize :=
|
||||
ptrAddrUnsafe a
|
||||
unsafe abbrev Object.ptrHash (a : Object) : UInt64 :=
|
||||
ptrAddrUnsafe a |>.toUInt64
|
||||
|
||||
@[extern "lean_sharecommon_eq"]
|
||||
unsafe constant Object.eq (a b : @& Object) : Bool
|
||||
|
||||
@[extern "lean_sharecommon_hash"]
|
||||
unsafe constant Object.hash (a : @& Object) : USize
|
||||
unsafe constant Object.hash (a : @& Object) : UInt64
|
||||
|
||||
unsafe def ObjectMap : Type := @HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
|
||||
unsafe def ObjectSet : Type := @HashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ binder_info binding_info(expr const & e) { return static_cast<binder_info>(lean_
|
|||
extern "C" object * lean_lit_type(obj_arg e);
|
||||
expr lit_type(literal const & lit) { return expr(lean_lit_type(lit.to_obj_arg())); }
|
||||
|
||||
extern "C" usize lean_expr_hash(obj_arg e);
|
||||
extern "C" uint64_t lean_expr_hash(obj_arg e);
|
||||
unsigned hash(expr const & e) { return lean_expr_hash(e.to_obj_arg()); }
|
||||
|
||||
extern "C" uint8 lean_expr_has_fvar(obj_arg e);
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ extern "C" uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
|
|||
return memcmp(reinterpret_cast<char*>(o1) + header_sz, reinterpret_cast<char*>(o2) + header_sz, sz1 - header_sz) == 0;
|
||||
}
|
||||
|
||||
extern "C" usize lean_sharecommon_hash(b_obj_arg o) {
|
||||
extern "C" uint64_t lean_sharecommon_hash(b_obj_arg o) {
|
||||
lean_assert(!lean_is_scalar(o));
|
||||
size_t sz = lean_object_byte_size(o);
|
||||
size_t header_sz = sizeof(lean_object);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue