From 300af47e41201e445a372a6fbe0e49eed1681840 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jun 2021 07:25:10 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Data/Hashable.lean | 46 +- stage0/src/Init/Prelude.lean | 22 +- stage0/src/Lean/Compiler/IR/Basic.lean | 4 +- stage0/src/Lean/Compiler/IR/Borrow.lean | 10 +- stage0/src/Lean/Data/SMap.lean | 8 +- stage0/src/Lean/Elab/Deriving/Hashable.lean | 8 +- stage0/src/Lean/Exception.lean | 2 +- stage0/src/Lean/Expr.lean | 38 +- stage0/src/Lean/HeadIndex.lean | 12 +- stage0/src/Lean/Level.lean | 12 +- stage0/src/Lean/Meta/Basic.lean | 4 +- stage0/src/Lean/Meta/DiscrTreeTypes.lean | 8 +- stage0/src/Lean/Meta/TransparencyMode.lean | 2 +- stage0/src/Lean/Util/MonadCache.lean | 16 +- stage0/src/Lean/Util/SCC.lean | 4 +- stage0/src/Std/Data/HashMap.lean | 34 +- stage0/src/Std/Data/HashSet.lean | 30 +- stage0/src/Std/Data/PersistentHashMap.lean | 50 +- stage0/src/Std/Data/PersistentHashSet.lean | 6 +- stage0/stdlib/Init/Data/Hashable.c | 194 ++++---- stage0/stdlib/Init/Prelude.c | 51 +-- stage0/stdlib/Lean/Compiler/IR/Basic.c | 20 +- stage0/stdlib/Lean/Compiler/IR/Borrow.c | 38 +- stage0/stdlib/Lean/Elab/Deriving/Hashable.c | 482 +++++++++----------- stage0/stdlib/Lean/Elab/Term.c | 10 +- stage0/stdlib/Lean/Expr.c | 74 +-- stage0/stdlib/Lean/HeadIndex.c | 20 +- stage0/stdlib/Lean/Level.c | 20 +- stage0/stdlib/Lean/Meta/Basic.c | 24 +- stage0/stdlib/Lean/Meta/DiscrTreeTypes.c | 20 +- stage0/stdlib/Lean/Meta/FunInfo.c | 2 +- stage0/stdlib/Lean/Meta/InferType.c | 14 +- stage0/stdlib/Lean/Meta/Match/Match.c | 14 +- stage0/stdlib/Lean/Meta/TransparencyMode.c | 18 +- stage0/stdlib/Lean/Util/ForEachExpr.c | 6 +- 35 files changed, 629 insertions(+), 694 deletions(-) diff --git a/stage0/src/Init/Data/Hashable.lean b/stage0/src/Init/Data/Hashable.lean index 42b57cfb7a..1e7c328d4e 100644 --- a/stage0/src/Init/Data/Hashable.lean +++ b/stage0/src/Init/Data/Hashable.lean @@ -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) => mixHash (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 => mixHash (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 => mixHash (hash a) 13 + | some a => mixUSizeHash (hashUSize a) 13 -instance [Hashable α] : Hashable (List α) where - hash as := as.foldl (fun r a => mixHash 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 \ No newline at end of file +instance (P : Prop) : HashableUSize P where + hashUSize := Function.const P 0 diff --git a/stage0/src/Init/Prelude.lean b/stage0/src/Init/Prelude.lean index 38f11bae37..eb29853ac8 100644 --- a/stage0/src/Init/Prelude.lean +++ b/stage0/src/Init/Prelude.lean @@ -1587,22 +1587,22 @@ 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 -@[extern "lean_usize_mix_hash"] -constant mixHash (u₁ u₂ : USize) : USize +-- @[extern "lean_usize_mix_hash"] +-- constant mixHash (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 (mixHash (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 (mixHash (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 diff --git a/stage0/src/Lean/Compiler/IR/Basic.lean b/stage0/src/Lean/Compiler/IR/Basic.lean index 8931dcb121..f3a03fa022 100644 --- a/stage0/src/Lean/Compiler/IR/Basic.lean +++ b/stage0/src/Lean/Compiler/IR/Basic.lean @@ -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 := {} diff --git a/stage0/src/Lean/Compiler/IR/Borrow.lean b/stage0/src/Lean/Compiler/IR/Borrow.lean index 3f1c88ab65..4cdf9f439b 100644 --- a/stage0/src/Lean/Compiler/IR/Borrow.lean +++ b/stage0/src/Lean/Compiler/IR/Borrow.lean @@ -20,8 +20,8 @@ def beq : Key → Key → Bool instance : BEq Key := ⟨beq⟩ def getHash : Key → USize - | (f, x) => mixHash (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 => mixHash (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) diff --git a/stage0/src/Lean/Data/SMap.lean b/stage0/src/Lean/Data/SMap.lean index 07021ca686..9bb1cd68c6 100644 --- a/stage0/src/Lean/Data/SMap.lean +++ b/stage0/src/Lean/Data/SMap.lean @@ -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 diff --git a/stage0/src/Lean/Elab/Deriving/Hashable.lean b/stage0/src/Lean/Elab/Deriving/Hashable.lean index f49fa67726..9f5f5cc723 100644 --- a/stage0/src/Lean/Elab/Deriving/Hashable.lean +++ b/stage0/src/Lean/Elab/Deriving/Hashable.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 \ No newline at end of file + registerBuiltinDerivingHandler ``HashableUSize mkHashableHandler + registerTraceClass `Elab.Deriving.hashable diff --git a/stage0/src/Lean/Exception.lean b/stage0/src/Lean/Exception.lean index df2a590ed4..0f90ecca30 100644 --- a/stage0/src/Lean/Exception.lean +++ b/stage0/src/Lean/Exception.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 α] [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 diff --git a/stage0/src/Lean/Expr.lean b/stage0/src/Lean/Expr.lean index 38ddb876e5..1ed0f81af8 100644 --- a/stage0/src/Lean/Expr.lean +++ b/stage0/src/Lean/Expr.lean @@ -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 (mixHash 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 (mixHash 5 $ mixHash (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 (mixHash 7 $ hash idx) (idx+1) + Expr.bvar idx $ mkData (mixUSizeHash 7 $ hashUSize idx) (idx+1) def mkSort (lvl : Level) : Expr := - Expr.sort lvl $ mkData (mixHash 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 (mixHash 13 $ hash fvarId) 0 true + Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hashUSize fvarId) 0 true def mkMVar (fvarId : MVarId) : Expr := - Expr.mvar fvarId $ mkData (mixHash 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 (mixHash 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 (mixHash 23 $ mixHash (hash s) $ mixHash (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 (mixHash 29 $ mixHash (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 (mixHash 31 $ mixHash (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 (mixHash 37 $ mixHash (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 (mixHash 41 $ mixHash (hash t) $ mixHash (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 diff --git a/stage0/src/Lean/HeadIndex.lean b/stage0/src/Lean/HeadIndex.lean index 907279fcbc..fa7bf42d47 100644 --- a/stage0/src/Lean/HeadIndex.lean +++ b/stage0/src/Lean/HeadIndex.lean @@ -21,16 +21,16 @@ inductive HeadIndex where namespace HeadIndex protected def HeadIndex.hash : HeadIndex → USize - | fvar fvarId => mixHash 11 $ hash fvarId - | mvar mvarId => mixHash 13 $ hash mvarId - | const constName => mixHash 17 $ hash constName - | proj structName idx => mixHash 19 $ mixHash (hash structName) (hash idx) - | lit litVal => mixHash 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 diff --git a/stage0/src/Lean/Level.lean b/stage0/src/Lean/Level.lean index 2a8ff82e79..b40013739a 100644 --- a/stage0/src/Lean/Level.lean +++ b/stage0/src/Lean/Level.lean @@ -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 (mixHash 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 (mixHash 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 (mixHash 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 (mixHash 2251 $ mixHash (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 (mixHash 2267 $ mixHash (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) diff --git a/stage0/src/Lean/Meta/Basic.lean b/stage0/src/Lean/Meta/Basic.lean index fea3d4c869..7e6183d74a 100644 --- a/stage0/src/Lean/Meta/Basic.lean +++ b/stage0/src/Lean/Meta/Basic.lean @@ -80,8 +80,8 @@ structure InfoCacheKey where deriving Inhabited, BEq namespace InfoCacheKey -instance : Hashable InfoCacheKey := - ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (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) diff --git a/stage0/src/Lean/Meta/DiscrTreeTypes.lean b/stage0/src/Lean/Meta/DiscrTreeTypes.lean index bacbeb219d..655893cf99 100644 --- a/stage0/src/Lean/Meta/DiscrTreeTypes.lean +++ b/stage0/src/Lean/Meta/DiscrTreeTypes.lean @@ -21,14 +21,14 @@ inductive Key where deriving Inhabited, BEq protected def Key.hash : Key → USize - | Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a) - | Key.fvar n a => mixHash 3541 $ mixHash (hash n) (hash a) - | Key.lit v => mixHash 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 α diff --git a/stage0/src/Lean/Meta/TransparencyMode.lean b/stage0/src/Lean/Meta/TransparencyMode.lean index 4d07fc9ddb..7988bccadc 100644 --- a/stage0/src/Lean/Meta/TransparencyMode.lean +++ b/stage0/src/Lean/Meta/TransparencyMode.lean @@ -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 diff --git a/stage0/src/Lean/Util/MonadCache.lean b/stage0/src/Lean/Util/MonadCache.lean index 8b507d0837..7dd40544ca 100644 --- a/stage0/src/Lean/Util/MonadCache.lean +++ b/stage0/src/Lean/Util/MonadCache.lean @@ -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 ..) diff --git a/stage0/src/Lean/Util/SCC.lean b/stage0/src/Lean/Util/SCC.lean index 887e2926d9..f63bd0f0df 100644 --- a/stage0/src/Lean/Util/SCC.lean +++ b/stage0/src/Lean/Util/SCC.lean @@ -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 diff --git a/stage0/src/Std/Data/HashMap.lean b/stage0/src/Std/Data/HashMap.lean index 5b4a852247..4571ed1268 100644 --- a/stage0/src/Std/Data/HashMap.lean +++ b/stage0/src/Std/Data/HashMap.lean @@ -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 diff --git a/stage0/src/Std/Data/HashSet.lean b/stage0/src/Std/Data/HashSet.lean index 913fd4a9f2..e7ec3ad4b9 100644 --- a/stage0/src/Std/Data/HashSet.lean +++ b/stage0/src/Std/Data/HashSet.lean @@ -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 diff --git a/stage0/src/Std/Data/PersistentHashMap.lean b/stage0/src/Std/Data/PersistentHashMap.lean index 15a864b6ac..f7cb670e69 100644 --- a/stage0/src/Std/Data/PersistentHashMap.lean +++ b/stage0/src/Std/Data/PersistentHashMap.lean @@ -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 := diff --git a/stage0/src/Std/Data/PersistentHashSet.lean b/stage0/src/Std/Data/PersistentHashSet.lean index e5de05e8ca..9a7fff20ca 100644 --- a/stage0/src/Std/Data/PersistentHashSet.lean +++ b/stage0/src/Std/Data/PersistentHashSet.lean @@ -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 diff --git a/stage0/stdlib/Init/Data/Hashable.c b/stage0/stdlib/Init/Data/Hashable.c index 53ad9e5a0e..7377f4a7ee 100644 --- a/stage0/stdlib/Init/Data/Hashable.c +++ b/stage0/stdlib/Init/Data/Hashable.c @@ -13,58 +13,58 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* l_instHashableProd_match__1(lean_object*, lean_object*, lean_object*); size_t l_UInt32_toUSize(uint32_t); -size_t l_instHashableProd___rarg(lean_object*, lean_object*, lean_object*); -size_t l_instHashableUSize(size_t); -lean_object* l_instHashableList(lean_object*); -lean_object* l_instHashableUSize___boxed(lean_object*); -lean_object* l_List_foldl___at_instHashableList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSize(lean_object*); size_t l_Option_hash___rarg(lean_object*, lean_object*); -size_t l_instHashableBool(uint8_t); -lean_object* l_instHashableOption(lean_object*); -size_t l_instHashableInt(lean_object*); -lean_object* l_instHashable___closed__1___boxed__const__1; +size_t l_instHashableUSizeProd___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeOption(lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Option_hash_match__1(lean_object*, lean_object*); +size_t l_instHashableUSizeOption___rarg(lean_object*, lean_object*); +lean_object* l_instHashableUSizeBool_match__1(lean_object*); +lean_object* l_instHashableUSizeProd___rarg___boxed(lean_object*, lean_object*, lean_object*); size_t l_UInt64_toUSize(uint64_t); -lean_object* l_List_foldl___at_instHashableList___spec__1(lean_object*); +size_t l_instHashableUSizeUInt32(uint32_t); +lean_object* l_instHashableUSizeProd_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*); -lean_object* l_instHashableUInt64___boxed(lean_object*); -lean_object* l_instHashableProd(lean_object*, lean_object*); +lean_object* l_instHashableUSizeProd_match__1___rarg(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); -lean_object* l_instHashable___closed__1; -lean_object* l_instHashableBool_match__1(lean_object*); +size_t l_instHashableUSizeList___rarg(lean_object*, lean_object*); +size_t l_instHashableUSizeInt(lean_object*); +lean_object* l_instHashableUSizeList___rarg___boxed(lean_object*, lean_object*); lean_object* l_Option_hash___rarg___boxed(lean_object*, lean_object*); -lean_object* l_instHashableBool_match__1___rarg(uint8_t, lean_object*, lean_object*); -size_t l_instHashableUInt64(uint64_t); -lean_object* l_instHashableInt_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableList___rarg___boxed(lean_object*, lean_object*); +lean_object* l_instHashableUSizeBool_match__1___rarg(uint8_t, lean_object*, lean_object*); +lean_object* l_instHashableUSizeUInt64___boxed(lean_object*); lean_object* l_Option_hash_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableUInt32___boxed(lean_object*); +lean_object* l_instHashableUSizeOption___rarg___boxed(lean_object*, lean_object*); size_t lean_usize_of_nat(lean_object*); -size_t l_instHashableNat(lean_object*); -size_t l_instHashableList___rarg(lean_object*, lean_object*); -lean_object* l_instHashableOption___rarg___boxed(lean_object*, lean_object*); -lean_object* l_instHashableInt_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeInt___boxed(lean_object*); +lean_object* l_instHashableUSizeInt_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeBool___boxed(lean_object*); +lean_object* l_instHashableUSize___closed__1___boxed__const__1; +lean_object* l_instHashableUSizeNat___boxed(lean_object*); +size_t l_List_foldl___at_instHashableUSizeList___spec__1___rarg(lean_object*, size_t, lean_object*); +lean_object* l_instHashableUSizeList(lean_object*); uint8_t lean_int_dec_lt(lean_object*, lean_object*); extern lean_object* l_Int_instInhabitedInt___closed__1; +size_t l_instHashableUSizeNat(lean_object*); lean_object* lean_nat_mul(lean_object*, lean_object*); lean_object* lean_nat_abs(lean_object*); -lean_object* l_instHashableInt_match__1(lean_object*); -lean_object* l_instHashableBool_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableNat___boxed(lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); -lean_object* l_instHashable(lean_object*); -size_t l_instHashableOption___rarg(lean_object*, lean_object*); -lean_object* l_instHashableProd_match__1___rarg(lean_object*, lean_object*); -lean_object* l_instHashableBool___boxed(lean_object*); -size_t l_instHashableUInt32(uint32_t); +lean_object* l_instHashableUSizeUSize___boxed(lean_object*); +lean_object* l_instHashableUSizeBool_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSize___closed__1; +lean_object* l_instHashableUSizeInt_match__1(lean_object*); +size_t l_instHashableUSizeUSize(size_t); +size_t l_instHashableUSizeBool(uint8_t); +lean_object* l_List_foldl___at_instHashableUSizeList___spec__1(lean_object*); +lean_object* l_List_foldl___at_instHashableUSizeList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeUInt32___boxed(lean_object*); lean_object* l_Option_hash(lean_object*); -size_t l_List_foldl___at_instHashableList___spec__1___rarg(lean_object*, size_t, lean_object*); -lean_object* l_instHashableInt___boxed(lean_object*); -size_t l_instHashableNat(lean_object* x_1) { +size_t lean_usize_mix_hash(size_t, size_t); +lean_object* l_instHashableUSizeInt_match__1___rarg(lean_object*, lean_object*, lean_object*); +size_t l_instHashableUSizeUInt64(uint64_t); +lean_object* l_instHashableUSizeProd(lean_object*, lean_object*); +size_t l_instHashableUSizeNat(lean_object* x_1) { _start: { size_t x_2; @@ -72,17 +72,17 @@ x_2 = lean_usize_of_nat(x_1); return x_2; } } -lean_object* l_instHashableNat___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeNat___boxed(lean_object* x_1) { _start: { size_t x_2; lean_object* x_3; -x_2 = l_instHashableNat(x_1); +x_2 = l_instHashableUSizeNat(x_1); lean_dec(x_1); x_3 = lean_box_usize(x_2); return x_3; } } -lean_object* l_instHashableProd_match__1___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_instHashableUSizeProd_match__1___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; lean_object* x_5; @@ -95,15 +95,15 @@ x_5 = lean_apply_2(x_2, x_3, x_4); return x_5; } } -lean_object* l_instHashableProd_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeProd_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = lean_alloc_closure((void*)(l_instHashableProd_match__1___rarg), 2, 0); +x_4 = lean_alloc_closure((void*)(l_instHashableUSizeProd_match__1___rarg), 2, 0); return x_4; } } -size_t l_instHashableProd___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +size_t l_instHashableUSizeProd___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; lean_object* x_8; size_t x_9; size_t x_10; @@ -122,24 +122,24 @@ x_10 = lean_usize_mix_hash(x_7, x_9); return x_10; } } -lean_object* l_instHashableProd(lean_object* x_1, lean_object* x_2) { +lean_object* l_instHashableUSizeProd(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 0); +x_3 = lean_alloc_closure((void*)(l_instHashableUSizeProd___rarg___boxed), 3, 0); return x_3; } } -lean_object* l_instHashableProd___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeProd___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { size_t x_4; lean_object* x_5; -x_4 = l_instHashableProd___rarg(x_1, x_2, x_3); +x_4 = l_instHashableUSizeProd___rarg(x_1, x_2, x_3); x_5 = lean_box_usize(x_4); return x_5; } } -lean_object* l_instHashableBool_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeBool_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) { _start: { if (x_1 == 0) @@ -160,25 +160,25 @@ return x_7; } } } -lean_object* l_instHashableBool_match__1(lean_object* x_1) { +lean_object* l_instHashableUSizeBool_match__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_instHashableBool_match__1___rarg___boxed), 3, 0); +x_2 = lean_alloc_closure((void*)(l_instHashableUSizeBool_match__1___rarg___boxed), 3, 0); return x_2; } } -lean_object* l_instHashableBool_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeBool_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { uint8_t x_4; lean_object* x_5; x_4 = lean_unbox(x_1); lean_dec(x_1); -x_5 = l_instHashableBool_match__1___rarg(x_4, x_2, x_3); +x_5 = l_instHashableUSizeBool_match__1___rarg(x_4, x_2, x_3); return x_5; } } -size_t l_instHashableBool(uint8_t x_1) { +size_t l_instHashableUSizeBool(uint8_t x_1) { _start: { if (x_1 == 0) @@ -195,13 +195,13 @@ return x_3; } } } -lean_object* l_instHashableBool___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeBool___boxed(lean_object* x_1) { _start: { uint8_t x_2; size_t x_3; lean_object* x_4; x_2 = lean_unbox(x_1); lean_dec(x_1); -x_3 = l_instHashableBool(x_2); +x_3 = l_instHashableUSizeBool(x_2); x_4 = lean_box_usize(x_3); return x_4; } @@ -279,7 +279,7 @@ x_4 = lean_box_usize(x_3); return x_4; } } -size_t l_instHashableOption___rarg(lean_object* x_1, lean_object* x_2) { +size_t l_instHashableUSizeOption___rarg(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -304,24 +304,24 @@ return x_8; } } } -lean_object* l_instHashableOption(lean_object* x_1) { +lean_object* l_instHashableUSizeOption(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_instHashableOption___rarg___boxed), 2, 0); +x_2 = lean_alloc_closure((void*)(l_instHashableUSizeOption___rarg___boxed), 2, 0); return x_2; } } -lean_object* l_instHashableOption___rarg___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_instHashableUSizeOption___rarg___boxed(lean_object* x_1, lean_object* x_2) { _start: { size_t x_3; lean_object* x_4; -x_3 = l_instHashableOption___rarg(x_1, x_2); +x_3 = l_instHashableUSizeOption___rarg(x_1, x_2); x_4 = lean_box_usize(x_3); return x_4; } } -size_t l_List_foldl___at_instHashableList___spec__1___rarg(lean_object* x_1, size_t x_2, lean_object* x_3) { +size_t l_List_foldl___at_instHashableUSizeList___spec__1___rarg(lean_object* x_1, size_t x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_3) == 0) @@ -348,52 +348,52 @@ goto _start; } } } -lean_object* l_List_foldl___at_instHashableList___spec__1(lean_object* x_1) { +lean_object* l_List_foldl___at_instHashableUSizeList___spec__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_List_foldl___at_instHashableList___spec__1___rarg___boxed), 3, 0); +x_2 = lean_alloc_closure((void*)(l_List_foldl___at_instHashableUSizeList___spec__1___rarg___boxed), 3, 0); return x_2; } } -size_t l_instHashableList___rarg(lean_object* x_1, lean_object* x_2) { +size_t l_instHashableUSizeList___rarg(lean_object* x_1, lean_object* x_2) { _start: { size_t x_3; size_t x_4; x_3 = 7; -x_4 = l_List_foldl___at_instHashableList___spec__1___rarg(x_1, x_3, x_2); +x_4 = l_List_foldl___at_instHashableUSizeList___spec__1___rarg(x_1, x_3, x_2); return x_4; } } -lean_object* l_instHashableList(lean_object* x_1) { +lean_object* l_instHashableUSizeList(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_instHashableList___rarg___boxed), 2, 0); +x_2 = lean_alloc_closure((void*)(l_instHashableUSizeList___rarg___boxed), 2, 0); return x_2; } } -lean_object* l_List_foldl___at_instHashableList___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_List_foldl___at_instHashableUSizeList___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { size_t x_4; size_t x_5; lean_object* x_6; x_4 = lean_unbox_usize(x_2); lean_dec(x_2); -x_5 = l_List_foldl___at_instHashableList___spec__1___rarg(x_1, x_4, x_3); +x_5 = l_List_foldl___at_instHashableUSizeList___spec__1___rarg(x_1, x_4, x_3); x_6 = lean_box_usize(x_5); return x_6; } } -lean_object* l_instHashableList___rarg___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_instHashableUSizeList___rarg___boxed(lean_object* x_1, lean_object* x_2) { _start: { size_t x_3; lean_object* x_4; -x_3 = l_instHashableList___rarg(x_1, x_2); +x_3 = l_instHashableUSizeList___rarg(x_1, x_2); x_4 = lean_box_usize(x_3); return x_4; } } -size_t l_instHashableUInt32(uint32_t x_1) { +size_t l_instHashableUSizeUInt32(uint32_t x_1) { _start: { size_t x_2; @@ -401,18 +401,18 @@ x_2 = x_1; return x_2; } } -lean_object* l_instHashableUInt32___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeUInt32___boxed(lean_object* x_1) { _start: { uint32_t x_2; size_t x_3; lean_object* x_4; x_2 = lean_unbox_uint32(x_1); lean_dec(x_1); -x_3 = l_instHashableUInt32(x_2); +x_3 = l_instHashableUSizeUInt32(x_2); x_4 = lean_box_usize(x_3); return x_4; } } -size_t l_instHashableUInt64(uint64_t x_1) { +size_t l_instHashableUSizeUInt64(uint64_t x_1) { _start: { size_t x_2; @@ -420,35 +420,35 @@ x_2 = ((size_t)x_1); return x_2; } } -lean_object* l_instHashableUInt64___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeUInt64___boxed(lean_object* x_1) { _start: { uint64_t x_2; size_t x_3; lean_object* x_4; x_2 = lean_unbox_uint64(x_1); lean_dec(x_1); -x_3 = l_instHashableUInt64(x_2); +x_3 = l_instHashableUSizeUInt64(x_2); x_4 = lean_box_usize(x_3); return x_4; } } -size_t l_instHashableUSize(size_t x_1) { +size_t l_instHashableUSizeUSize(size_t x_1) { _start: { return x_1; } } -lean_object* l_instHashableUSize___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeUSize___boxed(lean_object* x_1) { _start: { size_t x_2; size_t x_3; lean_object* x_4; x_2 = lean_unbox_usize(x_1); lean_dec(x_1); -x_3 = l_instHashableUSize(x_2); +x_3 = l_instHashableUSizeUSize(x_2); x_4 = lean_box_usize(x_3); return x_4; } } -lean_object* l_instHashableInt_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeInt_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; uint8_t x_5; @@ -475,24 +475,24 @@ return x_11; } } } -lean_object* l_instHashableInt_match__1(lean_object* x_1) { +lean_object* l_instHashableUSizeInt_match__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_instHashableInt_match__1___rarg___boxed), 3, 0); +x_2 = lean_alloc_closure((void*)(l_instHashableUSizeInt_match__1___rarg___boxed), 3, 0); return x_2; } } -lean_object* l_instHashableInt_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_instHashableUSizeInt_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_instHashableInt_match__1___rarg(x_1, x_2, x_3); +x_4 = l_instHashableUSizeInt_match__1___rarg(x_1, x_2, x_3); lean_dec(x_1); return x_4; } } -size_t l_instHashableInt(lean_object* x_1) { +size_t l_instHashableUSizeInt(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; @@ -527,17 +527,17 @@ return x_14; } } } -lean_object* l_instHashableInt___boxed(lean_object* x_1) { +lean_object* l_instHashableUSizeInt___boxed(lean_object* x_1) { _start: { size_t x_2; lean_object* x_3; -x_2 = l_instHashableInt(x_1); +x_2 = l_instHashableUSizeInt(x_1); lean_dec(x_1); x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_instHashable___closed__1___boxed__const__1() { +static lean_object* _init_l_instHashableUSize___closed__1___boxed__const__1() { _start: { size_t x_1; lean_object* x_2; @@ -546,21 +546,21 @@ x_2 = lean_box_usize(x_1); return x_2; } } -static lean_object* _init_l_instHashable___closed__1() { +static lean_object* _init_l_instHashableUSize___closed__1() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_instHashable___closed__1___boxed__const__1; +x_1 = l_instHashableUSize___closed__1___boxed__const__1; x_2 = lean_alloc_closure((void*)(l_Function_const___rarg___boxed), 2, 1); lean_closure_set(x_2, 0, x_1); return x_2; } } -lean_object* l_instHashable(lean_object* x_1) { +lean_object* l_instHashableUSize(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_instHashable___closed__1; +x_2 = l_instHashableUSize___closed__1; return x_2; } } @@ -577,10 +577,10 @@ lean_dec_ref(res); res = initialize_Init_Data_String(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_instHashable___closed__1___boxed__const__1 = _init_l_instHashable___closed__1___boxed__const__1(); -lean_mark_persistent(l_instHashable___closed__1___boxed__const__1); -l_instHashable___closed__1 = _init_l_instHashable___closed__1(); -lean_mark_persistent(l_instHashable___closed__1); +l_instHashableUSize___closed__1___boxed__const__1 = _init_l_instHashableUSize___closed__1___boxed__const__1(); +lean_mark_persistent(l_instHashableUSize___closed__1___boxed__const__1); +l_instHashableUSize___closed__1 = _init_l_instHashableUSize___closed__1(); +lean_mark_persistent(l_instHashableUSize___closed__1); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Prelude.c b/stage0/stdlib/Init/Prelude.c index 1b7b3345f3..a7b64c7812 100644 --- a/stage0/stdlib/Init/Prelude.c +++ b/stage0/stdlib/Init/Prelude.c @@ -35,7 +35,6 @@ lean_object* l_instMonadWithReader___rarg(lean_object*); lean_object* l_EStateM_tryCatch(lean_object*, lean_object*, lean_object*); lean_object* l_UInt32_decLe___boxed(lean_object*, lean_object*); lean_object* l___private_Init_Prelude_0__String_utf8ByteSizeAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableString; lean_object* l_Lean_scientificLitKind___closed__1; lean_object* lean_erase_macro_scopes(lean_object*); lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__9; @@ -150,7 +149,6 @@ lean_object* l_Lean_Macro_instInhabitedMethods___closed__5; lean_object* l_id___rarg___boxed(lean_object*); size_t l_Lean_Name_mkNum___closed__1; lean_object* l_Monad_seqRight___default___rarg___lambda__1___boxed(lean_object*, lean_object*); -lean_object* l_Lean_instHashableName; uint8_t l_Fin_decLe___rarg(lean_object*, lean_object*); lean_object* l_String_csize___boxed(lean_object*); lean_object* l_Lean_instInhabitedParserDescr___closed__1; @@ -176,7 +174,6 @@ lean_object* l_USize_size___closed__1; lean_object* l_Lean_Macro_instInhabitedMethods___closed__3; lean_object* l_instInhabitedNat; lean_object* l_Lean_instInhabitedMacroScopesView; -lean_object* l_Lean_instHashableName___closed__1; lean_object* l_Lean_instInhabitedParserDescr___closed__2; lean_object* l_Lean_instInhabitedParserDescr; lean_object* l_instLTFin(lean_object*); @@ -328,7 +325,6 @@ lean_object* l_Lean_strLitKind; uint32_t l_Char_utf8Size___closed__5; lean_object* l_Nat_decEq_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_modifyGet___rarg(lean_object*, lean_object*); -lean_object* l_mixHash___boxed(lean_object*, lean_object*); uint8_t l_instDecidableEqList___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_map(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_mixUSizeHash___boxed(lean_object*, lean_object*); @@ -371,6 +367,7 @@ lean_object* l_Lean_Syntax_getArgs___boxed(lean_object*); lean_object* l_Lean_Syntax_setKind(lean_object*, lean_object*); lean_object* l_Applicative_seqLeft___default(lean_object*); lean_object* l_instInhabited___rarg(lean_object*, lean_object*); +lean_object* l_instHashableUSizeString; lean_object* l_UInt32_decLt___boxed(lean_object*, lean_object*); lean_object* l_UInt32_toNat___boxed(lean_object*); lean_object* l_Lean_MacroScopesView_review_match__1(lean_object*); @@ -494,6 +491,7 @@ lean_object* l___private_Init_Prelude_0__Lean_assembleParts_match__1(lean_object lean_object* l_Lean_Syntax_setKind_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Prelude_0__Lean_assembleParts(lean_object*, lean_object*); lean_object* l_min___boxed(lean_object*, lean_object*); +lean_object* l_Lean_instHashableUSizeName; lean_object* l_EStateM_instOrElseEStateM(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_instDecidableEqFin___rarg(lean_object*, lean_object*); uint8_t l_Fin_decLt___rarg(lean_object*, lean_object*); @@ -756,7 +754,6 @@ lean_object* l_Lean_Macro_instInhabitedMethods___lambda__4(lean_object*, lean_ob uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); lean_object* l_instDecidableLe___boxed(lean_object*, lean_object*); lean_object* l_instOfNatNat(lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_UInt32_size; lean_object* l_Lean_instInhabitedMacroScopesView___closed__1; lean_object* l_Array_sequenceMap_loop(lean_object*, lean_object*, lean_object*); @@ -794,7 +791,6 @@ lean_object* l_Lean_Macro_throwUnsupported(lean_object*, lean_object*); lean_object* l_List_hasDecEq_match__1___rarg(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Macro_instMonadRefMacroM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_appendCore_loop_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableString___closed__1; lean_object* l_Lean_Macro_instMonadRefMacroM___closed__3; lean_object* l_instMonadStateOf___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__7; @@ -832,11 +828,13 @@ lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*); lean_object* l_Array_appendCore_loop_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_throw(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_instHashableUSizeName___closed__1; lean_object* l_List_redLength_match__1(lean_object*, lean_object*); lean_object* lean_usize_to_nat(size_t); lean_object* l_instDecidableNot___rarg___boxed(lean_object*); uint16_t l_instInhabitedUInt16; lean_object* l_Option_getD___rarg(lean_object*, lean_object*); +lean_object* l_instHashableUSizeString___closed__1; lean_object* l_ReaderT_pure(lean_object*, lean_object*); lean_object* lean_uint16_to_nat(uint16_t); lean_object* l_List_get_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -7739,19 +7737,6 @@ x_6 = lean_box_usize(x_5); return x_6; } } -lean_object* l_mixHash___boxed(lean_object* x_1, lean_object* x_2) { -_start: -{ -size_t x_3; size_t x_4; size_t x_5; lean_object* x_6; -x_3 = lean_unbox_usize(x_1); -lean_dec(x_1); -x_4 = lean_unbox_usize(x_2); -lean_dec(x_2); -x_5 = lean_usize_mix_hash(x_3, x_4); -x_6 = lean_box_usize(x_5); -return x_6; -} -} lean_object* l_String_hash___boxed(lean_object* x_1) { _start: { @@ -7762,7 +7747,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_instHashableString___closed__1() { +static lean_object* _init_l_instHashableUSizeString___closed__1() { _start: { lean_object* x_1; @@ -7770,11 +7755,11 @@ x_1 = lean_alloc_closure((void*)(l_String_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_instHashableString() { +static lean_object* _init_l_instHashableUSizeString() { _start: { lean_object* x_1; -x_1 = l_instHashableString___closed__1; +x_1 = l_instHashableUSizeString___closed__1; return x_1; } } @@ -7876,7 +7861,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_instHashableName___closed__1() { +static lean_object* _init_l_Lean_instHashableUSizeName___closed__1() { _start: { lean_object* x_1; @@ -7884,11 +7869,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Name_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_instHashableName() { +static lean_object* _init_l_Lean_instHashableUSizeName() { _start: { lean_object* x_1; -x_1 = l_Lean_instHashableName___closed__1; +x_1 = l_Lean_instHashableUSizeName___closed__1; return x_1; } } @@ -12822,17 +12807,17 @@ l_EStateM_nonBacktrackable___closed__2 = _init_l_EStateM_nonBacktrackable___clos lean_mark_persistent(l_EStateM_nonBacktrackable___closed__2); l_EStateM_nonBacktrackable___closed__3 = _init_l_EStateM_nonBacktrackable___closed__3(); lean_mark_persistent(l_EStateM_nonBacktrackable___closed__3); -l_instHashableString___closed__1 = _init_l_instHashableString___closed__1(); -lean_mark_persistent(l_instHashableString___closed__1); -l_instHashableString = _init_l_instHashableString(); -lean_mark_persistent(l_instHashableString); +l_instHashableUSizeString___closed__1 = _init_l_instHashableUSizeString___closed__1(); +lean_mark_persistent(l_instHashableUSizeString___closed__1); +l_instHashableUSizeString = _init_l_instHashableUSizeString(); +lean_mark_persistent(l_instHashableUSizeString); l_Lean_instInhabitedName = _init_l_Lean_instInhabitedName(); lean_mark_persistent(l_Lean_instInhabitedName); l_Lean_Name_hash___closed__1 = _init_l_Lean_Name_hash___closed__1(); -l_Lean_instHashableName___closed__1 = _init_l_Lean_instHashableName___closed__1(); -lean_mark_persistent(l_Lean_instHashableName___closed__1); -l_Lean_instHashableName = _init_l_Lean_instHashableName(); -lean_mark_persistent(l_Lean_instHashableName); +l_Lean_instHashableUSizeName___closed__1 = _init_l_Lean_instHashableUSizeName___closed__1(); +lean_mark_persistent(l_Lean_instHashableUSizeName___closed__1); +l_Lean_instHashableUSizeName = _init_l_Lean_instHashableUSizeName(); +lean_mark_persistent(l_Lean_instHashableUSizeName); l_Lean_Name_mkNum___closed__1 = _init_l_Lean_Name_mkNum___closed__1(); l_Lean_Name_instBEqName___closed__1 = _init_l_Lean_Name_instBEqName___closed__1(); lean_mark_persistent(l_Lean_Name_instBEqName___closed__1); diff --git a/stage0/stdlib/Lean/Compiler/IR/Basic.c b/stage0/stdlib/Lean/Compiler/IR/Basic.c index eaf8e3bf33..8d181481cc 100644 --- a/stage0/stdlib/Lean/Compiler/IR/Basic.c +++ b/stage0/stdlib/Lean/Compiler/IR/Basic.c @@ -58,6 +58,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_mmodifyJPs___spec__1___rarg___l uint8_t l_Lean_IR_IRType_isStruct(lean_object*); lean_object* l_Lean_IR_mmodifyJPs(lean_object*); lean_object* l_Lean_IR_mmodifyJPs___rarg(lean_object*, lean_object*, lean_object*); +size_t l_Lean_IR_instHashableUSizeJoinPointId(lean_object*); uint8_t l_Lean_IR_IRType_isIrrelevant(lean_object*); uint8_t lean_name_eq(lean_object*, lean_object*); lean_object* l_Lean_IR_IRType_isObj_match__1(lean_object*); @@ -132,7 +133,6 @@ lean_object* l_Lean_IR_CtorInfo_isRef___boxed(lean_object*); lean_object* l_Lean_IR_VarId_alphaEqv___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_addParamRename(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_IRType_isUnion_match__1(lean_object*); -size_t l_Lean_IR_instHashableVarId(lean_object*); lean_object* l_Lean_IR_IRType_instBEqIRType___closed__1; lean_object* l_Lean_IR_FnBody_isTerminal___boxed(lean_object*); lean_object* l_Lean_IR_IRType_isIrrelevant_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -158,7 +158,6 @@ lean_object* l_Std_RBNode_balRight___rarg(lean_object*, lean_object*, lean_objec uint8_t l_Std_RBNode_isBlack___rarg(lean_object*); lean_object* l_Lean_IR_LocalContext_isLocalVar_match__1(lean_object*); extern lean_object* l_Lean_instQuoteBool___closed__3; -lean_object* l_Lean_IR_instHashableVarId___boxed(lean_object*); lean_object* l_Lean_IR_LocalContext_getValue(lean_object*, lean_object*); lean_object* l_Lean_IR_LocalContext_addParam(lean_object*, lean_object*); lean_object* l_Lean_IR_FnBody_body_match__1(lean_object*); @@ -199,7 +198,6 @@ lean_object* l_Lean_IR_instInhabitedParam; lean_object* l_Lean_IR_AltCore_mmodifyBody___rarg___closed__1; lean_object* l_Lean_IR_AltCore_setBody_match__1(lean_object*); lean_object* l_Std_RBNode_balLeft___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_instHashableJoinPointId___boxed(lean_object*); lean_object* lean_ir_mk_proj_expr(lean_object*, lean_object*); lean_object* l_Lean_IR_Alt_ctor(lean_object*, lean_object*); lean_object* l_Lean_IR_instInhabitedParam___closed__1; @@ -219,6 +217,7 @@ lean_object* l_Lean_IR_instToFormatVarId(lean_object*); lean_object* l_Lean_IR_AltCore_mmodifyBody(lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_mmodifyJPs___spec__1___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*); extern lean_object* l_Array_swapAt_x21___rarg___closed__3; +lean_object* l_Lean_IR_instHashableUSizeVarId___boxed(lean_object*); lean_object* l_Std_Range_forIn_loop___at_Lean_IR_addParamsRename___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_1318____closed__8; lean_object* l_Lean_IR_FnBody_body_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -233,6 +232,7 @@ extern lean_object* l_Lean_instQuoteBool___closed__2; uint8_t l_Lean_IR_instBEqVarId(lean_object*, lean_object*); lean_object* l_Lean_IR_VarId_alphaEqv_match__1(lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); +lean_object* l_Lean_IR_instHashableUSizeJoinPointId___boxed(lean_object*); uint8_t l_Std_RBNode_isRed___rarg(lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_mmodifyJPs___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_CtorInfo_isScalar___boxed(lean_object*); @@ -247,7 +247,6 @@ lean_object* lean_panic_fn(lean_object*, lean_object*); lean_object* l_Lean_IR_instAlphaEqvArg___closed__1; lean_object* lean_ir_mk_jmp(lean_object*, lean_object*); lean_object* l_Lean_IR_Expr_alphaEqv_match__1(lean_object*); -size_t l_Lean_IR_instHashableJoinPointId(lean_object*); lean_object* l_Lean_IR_IRType_isUnion_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_LocalContext_isJP___boxed(lean_object*, lean_object*); lean_object* l_Lean_IR_mkIf___closed__2; @@ -324,6 +323,7 @@ lean_object* l_Lean_IR_instInhabitedIndexSet; lean_object* l_Lean_IR_Alt_default(lean_object*); lean_object* l_Std_RBNode_insert___at_Lean_IR_mkIndexSet___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Decl_isExtern___boxed(lean_object*); +size_t l_Lean_IR_instHashableUSizeVarId(lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_IR_LocalContext_eraseJoinPointDecl___boxed(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -416,7 +416,7 @@ lean_ctor_set(x_5, 0, x_4); return x_5; } } -size_t l_Lean_IR_instHashableVarId(lean_object* x_1) { +size_t l_Lean_IR_instHashableUSizeVarId(lean_object* x_1) { _start: { size_t x_2; @@ -424,11 +424,11 @@ x_2 = lean_usize_of_nat(x_1); return x_2; } } -lean_object* l_Lean_IR_instHashableVarId___boxed(lean_object* x_1) { +lean_object* l_Lean_IR_instHashableUSizeVarId___boxed(lean_object* x_1) { _start: { size_t x_2; lean_object* x_3; -x_2 = l_Lean_IR_instHashableVarId(x_1); +x_2 = l_Lean_IR_instHashableUSizeVarId(x_1); lean_dec(x_1); x_3 = lean_box_usize(x_2); return x_3; @@ -485,7 +485,7 @@ lean_ctor_set(x_5, 0, x_4); return x_5; } } -size_t l_Lean_IR_instHashableJoinPointId(lean_object* x_1) { +size_t l_Lean_IR_instHashableUSizeJoinPointId(lean_object* x_1) { _start: { size_t x_2; @@ -493,11 +493,11 @@ x_2 = lean_usize_of_nat(x_1); return x_2; } } -lean_object* l_Lean_IR_instHashableJoinPointId___boxed(lean_object* x_1) { +lean_object* l_Lean_IR_instHashableUSizeJoinPointId___boxed(lean_object* x_1) { _start: { size_t x_2; lean_object* x_3; -x_2 = l_Lean_IR_instHashableJoinPointId(x_1); +x_2 = l_Lean_IR_instHashableUSizeJoinPointId(x_1); lean_dec(x_1); x_3 = lean_box_usize(x_2); return x_3; diff --git a/stage0/stdlib/Lean/Compiler/IR/Borrow.c b/stage0/stdlib/Lean/Compiler/IR/Borrow.c index 308ed81b0c..fca791b45e 100644 --- a/stage0/stdlib/Lean/Compiler/IR/Borrow.c +++ b/stage0/stdlib/Lean/Compiler/IR/Borrow.c @@ -35,7 +35,6 @@ lean_object* l_Lean_IR_Borrow_ParamMap_fmt___closed__3; lean_object* l_Lean_IR_Borrow_ParamMap_instBEqKey; lean_object* l_Lean_IR_Borrow_getParamInfo_match__1(lean_object*); extern lean_object* l_Std_Format_defWidth; -lean_object* l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1; lean_object* l_Lean_IR_Borrow_OwnedSet_beq_match__1(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Borrow_ownArgs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_forM_loop___at_Lean_IR_Borrow_ownParamsUsingArgs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -105,7 +104,6 @@ size_t l_Lean_IR_Borrow_ParamMap_getHash(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Borrow_collectFnBody___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); uint8_t l_Std_HashMapImp_contains___at_Lean_IR_Borrow_OwnedSet_contains___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Name_toString(lean_object*, uint8_t); -lean_object* l_Lean_IR_Borrow_ParamMap_instHashableKey; lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Borrow_ownArgs___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_getParamInfo___closed__3; @@ -133,16 +131,18 @@ lean_object* l_Lean_IR_Borrow_ownArgs(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_IR_instInhabitedDecl; lean_object* l_Lean_IR_Borrow_InitParamMap_initBorrow(lean_object*); lean_object* l_Nat_forM_loop___at_Lean_IR_Borrow_ownParamsUsingArgs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1; lean_object* l_Lean_IR_Borrow_infer(lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_InitParamMap_visitDecls___boxed(lean_object*, lean_object*, lean_object*); size_t lean_usize_modn(size_t, lean_object*); lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey; lean_object* l_Lean_IR_Borrow_updateParamMap(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_IR_instInhabitedParam; lean_object* l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1(lean_object*, lean_object*); uint8_t l_Std_AssocList_contains___at_Lean_IR_Borrow_OwnedSet_insert___spec__2(lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_OwnedSet_getHash_match__1___rarg(lean_object*, lean_object*); -lean_object* l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1; +lean_object* l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey; lean_object* l_Std_HashMapImp_find_x3f___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___spec__1___boxed(lean_object*, lean_object*); lean_object* l_ReaderT_pure___at_Lean_IR_Borrow_collectDecls___spec__1(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Borrow_ownArgsIfParam___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); @@ -154,7 +154,6 @@ lean_object* l_Lean_IR_Borrow_collectExpr___lambda__1(lean_object*, lean_object* lean_object* l_Std_HashMapImp_expand___at_Lean_IR_Borrow_OwnedSet_insert___spec__3(lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_Borrow_InitParamMap_initBorrow___spec__1___boxed(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_isExport(lean_object*, lean_object*); -lean_object* l_Lean_IR_Borrow_OwnedSet_instHashableKey; lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_Borrow_ApplyParamMap_visitFnBody___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_markModified(lean_object*); size_t l_Lean_IR_Borrow_OwnedSet_getHash(lean_object*); @@ -202,8 +201,8 @@ lean_object* l_Lean_IR_Borrow_InitParamMap_initBorrowIfNotExported___boxed(lean_ lean_object* l_Lean_IR_Borrow_markModified___boxed(lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_ApplyParamMap_visitFnBody___boxed(lean_object*, lean_object*, lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Std_mkHashMap___at_Lean_IR_Borrow_BorrowInfState_owned___default___spec__1(lean_object*); +lean_object* l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1; lean_object* lean_ir_find_env_decl(lean_object*, lean_object*); extern lean_object* l_Std_HashMap_instInhabitedHashMap___closed__1; lean_object* l_Lean_IR_Borrow_ownArgs___boxed(lean_object*, lean_object*, lean_object*); @@ -230,6 +229,7 @@ lean_object* l_Lean_IR_Borrow_ParamMap_getHash_match__1___rarg(lean_object*, lea lean_object* l_Lean_IR_Borrow_updateParamSet(lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_ownArg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_InitParamMap_visitDecls_match__1(lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Std_mkHashMap___at_Lean_IR_Borrow_mkInitParamMap___spec__1(lean_object*); lean_object* l_Lean_IR_Decl_params(lean_object*); lean_object* l_Lean_IR_Borrow_applyParamMap___boxed(lean_object*, lean_object*); @@ -370,7 +370,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1() { +static lean_object* _init_l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1() { _start: { lean_object* x_1; @@ -378,11 +378,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_IR_Borrow_OwnedSet_getHash___boxed), 1, return x_1; } } -static lean_object* _init_l_Lean_IR_Borrow_OwnedSet_instHashableKey() { +static lean_object* _init_l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey() { _start: { lean_object* x_1; -x_1 = l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1; +x_1 = l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1; return x_1; } } @@ -974,7 +974,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1() { +static lean_object* _init_l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1() { _start: { lean_object* x_1; @@ -982,11 +982,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_IR_Borrow_ParamMap_getHash___boxed), 1, return x_1; } } -static lean_object* _init_l_Lean_IR_Borrow_ParamMap_instHashableKey() { +static lean_object* _init_l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey() { _start: { lean_object* x_1; -x_1 = l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1; +x_1 = l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1; return x_1; } } @@ -5623,18 +5623,18 @@ l_Lean_IR_Borrow_OwnedSet_instBEqKey___closed__1 = _init_l_Lean_IR_Borrow_OwnedS lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instBEqKey___closed__1); l_Lean_IR_Borrow_OwnedSet_instBEqKey = _init_l_Lean_IR_Borrow_OwnedSet_instBEqKey(); lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instBEqKey); -l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1 = _init_l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1(); -lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instHashableKey___closed__1); -l_Lean_IR_Borrow_OwnedSet_instHashableKey = _init_l_Lean_IR_Borrow_OwnedSet_instHashableKey(); -lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instHashableKey); +l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1 = _init_l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1(); +lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey___closed__1); +l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey = _init_l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey(); +lean_mark_persistent(l_Lean_IR_Borrow_OwnedSet_instHashableUSizeKey); l_Lean_IR_Borrow_ParamMap_instBEqKey___closed__1 = _init_l_Lean_IR_Borrow_ParamMap_instBEqKey___closed__1(); lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instBEqKey___closed__1); l_Lean_IR_Borrow_ParamMap_instBEqKey = _init_l_Lean_IR_Borrow_ParamMap_instBEqKey(); lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instBEqKey); -l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1 = _init_l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1(); -lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instHashableKey___closed__1); -l_Lean_IR_Borrow_ParamMap_instHashableKey = _init_l_Lean_IR_Borrow_ParamMap_instHashableKey(); -lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instHashableKey); +l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1 = _init_l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1(); +lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey___closed__1); +l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey = _init_l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey(); +lean_mark_persistent(l_Lean_IR_Borrow_ParamMap_instHashableUSizeKey); l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__1 = _init_l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__1(); lean_mark_persistent(l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__1); l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__2 = _init_l_Std_AssocList_foldlM___at_Lean_IR_Borrow_ParamMap_fmt___spec__1___closed__2(); diff --git a/stage0/stdlib/Lean/Elab/Deriving/Hashable.c b/stage0/stdlib/Lean/Elab/Deriving/Hashable.c index 96ee50be02..385d38de03 100644 --- a/stage0/stdlib/Lean/Elab/Deriving/Hashable.c +++ b/stage0/stdlib/Lean/Elab/Deriving/Hashable.c @@ -16,10 +16,11 @@ extern "C" { lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); size_t l_USize_add(size_t, size_t); +lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2; lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*); -lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1; lean_object* lean_mk_empty_array_with_capacity(lean_object*); lean_object* l_Lean_Elab_Deriving_Hashable_mkHashableHandler(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1; extern lean_object* l_Lean_Elab_Deriving_mkContext___closed__2; lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); @@ -29,7 +30,6 @@ uint8_t l_USize_decEq(size_t, size_t); lean_object* lean_array_uget(lean_object*, size_t); lean_object* l_Array_append___rarg(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__1; -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10; lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___closed__1; lean_object* l_Lean_Elab_Deriving_Hashable_mkHashableHeader___rarg___closed__1; extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1094____closed__23; @@ -70,13 +70,13 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_13362____closed__2; lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__1; +lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3; extern lean_object* l_Lean_numLitKind; lean_object* l_Lean_Elab_Deriving_Hashable_mkAuxFunction(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Deriving_mkInstanceCmds(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_13362____closed__8; extern lean_object* l_myMacro____x40_Init_Notation___hyg_14133____closed__9; -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13; lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_903____closed__4; lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts_match__2(lean_object*); @@ -134,7 +134,6 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___privat lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___lambda__1___boxed(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Command_end___elambda__1___closed__1; extern lean_object* l_myMacro____x40_Init_Notation___hyg_1318____closed__9; -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9; uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l_Lean_Elab_Deriving_Hashable_mkHashableHeader(lean_object*); extern lean_object* l_Lean_Parser_Command_private___elambda__1___closed__1; @@ -143,7 +142,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_14569____closed__11; lean_object* l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__7; extern lean_object* l_myMacro____x40_Init_Notation___hyg_13362____closed__1; lean_object* l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__3; -lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587_(lean_object*); +lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575_(lean_object*); extern lean_object* l_Lean_Core_betaReduce___closed__1; lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__2; uint8_t l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___lambda__1(lean_object*, lean_object*); @@ -174,10 +173,8 @@ lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch(lean_object*, lean_object*, l lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts_match__3___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts_match__3(lean_object*); -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12; extern lean_object* l_myMacro____x40_Init_Notation___hyg_13362____closed__6; lean_object* l_Lean_mkConst(lean_object*, lean_object*); -lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11; lean_object* l_Lean_Expr_constName_x21(lean_object*); lean_object* l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__6; lean_object* l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -572,51 +569,27 @@ return x_3; static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__4; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__6() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7() { -_start: -{ lean_object* x_1; x_1 = lean_mk_string("hash"); return x_1; } } -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8() { +static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__6() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; +x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5; x_2 = lean_string_utf8_byte_size(x_1); return x_2; } } -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9() { +static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; +x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5; x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8; +x_3 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__6; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -624,50 +597,16 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10() { +static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; +x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Deriving_Hashable_mkHashableHeader___rarg___closed__2; -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16) { _start: { @@ -727,7 +666,7 @@ x_47 = lean_array_get_size(x_3); x_48 = l_Array_findIdx_x3f_loop___rarg(x_3, x_46, x_47, x_19, lean_box(0)); if (lean_obj_tag(x_48) == 0) { -lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; +lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; x_49 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg(x_14, x_15, x_43); x_50 = lean_ctor_get(x_49, 0); lean_inc(x_50); @@ -750,183 +689,182 @@ x_58 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___ lean_inc(x_53); lean_inc(x_56); x_59 = l_Lean_addMacroScope(x_56, x_58, x_53); -x_60 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__3; -x_61 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__6; +x_60 = lean_box(0); +x_61 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__3; lean_inc(x_50); x_62 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_62, 0, x_50); -lean_ctor_set(x_62, 1, x_60); +lean_ctor_set(x_62, 1, x_61); lean_ctor_set(x_62, 2, x_59); -lean_ctor_set(x_62, 3, x_61); +lean_ctor_set(x_62, 3, x_60); x_63 = l_prec_x28___x29___closed__3; lean_inc(x_50); x_64 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_64, 0, x_50); lean_ctor_set(x_64, 1, x_63); -x_65 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10; +x_65 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8; x_66 = l_Lean_addMacroScope(x_56, x_65, x_53); -x_67 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9; -x_68 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13; +x_67 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; lean_inc(x_50); -x_69 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_69, 0, x_50); -lean_ctor_set(x_69, 1, x_67); -lean_ctor_set(x_69, 2, x_66); -lean_ctor_set(x_69, 3, x_68); -x_70 = l_myMacro____x40_Init_Notation___hyg_71____closed__2; -x_71 = lean_array_push(x_70, x_44); -x_72 = l_Lean_nullKind___closed__2; -x_73 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_73, 0, x_72); -lean_ctor_set(x_73, 1, x_71); -x_74 = l_myMacro____x40_Init_Notation___hyg_1318____closed__8; -x_75 = lean_array_push(x_74, x_69); -x_76 = lean_array_push(x_75, x_73); -x_77 = l_myMacro____x40_Init_Notation___hyg_1997____closed__4; -x_78 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_78, 0, x_77); -lean_ctor_set(x_78, 1, x_76); +x_68 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_68, 0, x_50); +lean_ctor_set(x_68, 1, x_67); +lean_ctor_set(x_68, 2, x_66); +lean_ctor_set(x_68, 3, x_60); +x_69 = l_myMacro____x40_Init_Notation___hyg_71____closed__2; +x_70 = lean_array_push(x_69, x_44); +x_71 = l_Lean_nullKind___closed__2; +x_72 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_72, 0, x_71); +lean_ctor_set(x_72, 1, x_70); +x_73 = l_myMacro____x40_Init_Notation___hyg_1318____closed__8; +x_74 = lean_array_push(x_73, x_68); +x_75 = lean_array_push(x_74, x_72); +x_76 = l_myMacro____x40_Init_Notation___hyg_1997____closed__4; +x_77 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_77, 0, x_76); +lean_ctor_set(x_77, 1, x_75); lean_inc(x_2); -x_79 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_79, 0, x_72); -lean_ctor_set(x_79, 1, x_2); -x_80 = lean_array_push(x_74, x_78); -x_81 = lean_array_push(x_80, x_79); -x_82 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_82, 0, x_72); -lean_ctor_set(x_82, 1, x_81); -x_83 = l_prec_x28___x29___closed__7; -x_84 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_84, 0, x_50); -lean_ctor_set(x_84, 1, x_83); -x_85 = l_unexpand____x40_Init_Notation___hyg_1981____closed__1; -x_86 = lean_array_push(x_85, x_64); -x_87 = lean_array_push(x_86, x_82); -x_88 = lean_array_push(x_87, x_84); -x_89 = l_myMacro____x40_Init_Notation___hyg_12862____closed__8; -x_90 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_90, 0, x_89); -lean_ctor_set(x_90, 1, x_88); -x_91 = lean_array_push(x_74, x_31); -x_92 = lean_array_push(x_91, x_90); -x_93 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_93, 0, x_72); -lean_ctor_set(x_93, 1, x_92); -x_94 = lean_array_push(x_74, x_62); -x_95 = lean_array_push(x_94, x_93); -x_96 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_96, 0, x_77); +x_78 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_78, 0, x_71); +lean_ctor_set(x_78, 1, x_2); +x_79 = lean_array_push(x_73, x_77); +x_80 = lean_array_push(x_79, x_78); +x_81 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_81, 0, x_71); +lean_ctor_set(x_81, 1, x_80); +x_82 = l_prec_x28___x29___closed__7; +x_83 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_83, 0, x_50); +lean_ctor_set(x_83, 1, x_82); +x_84 = l_unexpand____x40_Init_Notation___hyg_1981____closed__1; +x_85 = lean_array_push(x_84, x_64); +x_86 = lean_array_push(x_85, x_81); +x_87 = lean_array_push(x_86, x_83); +x_88 = l_myMacro____x40_Init_Notation___hyg_12862____closed__8; +x_89 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_89, 0, x_88); +lean_ctor_set(x_89, 1, x_87); +x_90 = lean_array_push(x_73, x_31); +x_91 = lean_array_push(x_90, x_89); +x_92 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_92, 0, x_71); +lean_ctor_set(x_92, 1, x_91); +x_93 = lean_array_push(x_73, x_62); +x_94 = lean_array_push(x_93, x_92); +x_95 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_95, 0, x_76); +lean_ctor_set(x_95, 1, x_94); +x_96 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_96, 0, x_45); lean_ctor_set(x_96, 1, x_95); -x_97 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_97, 0, x_45); -lean_ctor_set(x_97, 1, x_96); -x_98 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_98, 0, x_97); -x_23 = x_98; +x_97 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_97, 0, x_96); +x_23 = x_97; x_24 = x_57; goto block_29; } else { -lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; -x_99 = lean_ctor_get(x_48, 0); -lean_inc(x_99); +lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; +x_98 = lean_ctor_get(x_48, 0); +lean_inc(x_98); lean_dec(x_48); -x_100 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg(x_14, x_15, x_43); -x_101 = lean_ctor_get(x_100, 0); +x_99 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg(x_14, x_15, x_43); +x_100 = lean_ctor_get(x_99, 0); +lean_inc(x_100); +x_101 = lean_ctor_get(x_99, 1); lean_inc(x_101); -x_102 = lean_ctor_get(x_100, 1); -lean_inc(x_102); -lean_dec(x_100); -x_103 = l_Lean_Elab_Term_getCurrMacroScope(x_10, x_11, x_12, x_13, x_14, x_15, x_102); -x_104 = lean_ctor_get(x_103, 0); -lean_inc(x_104); -x_105 = lean_ctor_get(x_103, 1); -lean_inc(x_105); -lean_dec(x_103); -x_106 = l_Lean_Elab_Term_getMainModule___rarg(x_15, x_105); -x_107 = lean_ctor_get(x_106, 0); -lean_inc(x_107); -x_108 = lean_ctor_get(x_106, 1); -lean_inc(x_108); -lean_dec(x_106); -x_109 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__4; -x_110 = l_Lean_addMacroScope(x_107, x_109, x_104); -x_111 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__3; -x_112 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__6; -lean_inc(x_101); -x_113 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_113, 0, x_101); -lean_ctor_set(x_113, 1, x_111); -lean_ctor_set(x_113, 2, x_110); -lean_ctor_set(x_113, 3, x_112); -x_114 = l_prec_x28___x29___closed__3; -lean_inc(x_101); -x_115 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_115, 0, x_101); -lean_ctor_set(x_115, 1, x_114); -x_116 = lean_ctor_get(x_1, 1); -x_117 = l_Lean_instInhabitedName; -x_118 = lean_array_get(x_117, x_116, x_99); lean_dec(x_99); -x_119 = lean_mk_syntax_ident(x_118); -x_120 = l_myMacro____x40_Init_Notation___hyg_71____closed__2; -x_121 = lean_array_push(x_120, x_44); -x_122 = l_Lean_nullKind___closed__2; -x_123 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_123, 0, x_122); -lean_ctor_set(x_123, 1, x_121); -x_124 = l_myMacro____x40_Init_Notation___hyg_1318____closed__8; -x_125 = lean_array_push(x_124, x_119); -x_126 = lean_array_push(x_125, x_123); -x_127 = l_myMacro____x40_Init_Notation___hyg_1997____closed__4; -x_128 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_128, 0, x_127); -lean_ctor_set(x_128, 1, x_126); +x_102 = l_Lean_Elab_Term_getCurrMacroScope(x_10, x_11, x_12, x_13, x_14, x_15, x_101); +x_103 = lean_ctor_get(x_102, 0); +lean_inc(x_103); +x_104 = lean_ctor_get(x_102, 1); +lean_inc(x_104); +lean_dec(x_102); +x_105 = l_Lean_Elab_Term_getMainModule___rarg(x_15, x_104); +x_106 = lean_ctor_get(x_105, 0); +lean_inc(x_106); +x_107 = lean_ctor_get(x_105, 1); +lean_inc(x_107); +lean_dec(x_105); +x_108 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__4; +x_109 = l_Lean_addMacroScope(x_106, x_108, x_103); +x_110 = lean_box(0); +x_111 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__3; +lean_inc(x_100); +x_112 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_112, 0, x_100); +lean_ctor_set(x_112, 1, x_111); +lean_ctor_set(x_112, 2, x_109); +lean_ctor_set(x_112, 3, x_110); +x_113 = l_prec_x28___x29___closed__3; +lean_inc(x_100); +x_114 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_114, 0, x_100); +lean_ctor_set(x_114, 1, x_113); +x_115 = lean_ctor_get(x_1, 1); +x_116 = l_Lean_instInhabitedName; +x_117 = lean_array_get(x_116, x_115, x_98); +lean_dec(x_98); +x_118 = lean_mk_syntax_ident(x_117); +x_119 = l_myMacro____x40_Init_Notation___hyg_71____closed__2; +x_120 = lean_array_push(x_119, x_44); +x_121 = l_Lean_nullKind___closed__2; +x_122 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_122, 0, x_121); +lean_ctor_set(x_122, 1, x_120); +x_123 = l_myMacro____x40_Init_Notation___hyg_1318____closed__8; +x_124 = lean_array_push(x_123, x_118); +x_125 = lean_array_push(x_124, x_122); +x_126 = l_myMacro____x40_Init_Notation___hyg_1997____closed__4; +x_127 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_127, 0, x_126); +lean_ctor_set(x_127, 1, x_125); lean_inc(x_2); -x_129 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_129, 0, x_122); -lean_ctor_set(x_129, 1, x_2); -x_130 = lean_array_push(x_124, x_128); -x_131 = lean_array_push(x_130, x_129); -x_132 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_132, 0, x_122); -lean_ctor_set(x_132, 1, x_131); -x_133 = l_prec_x28___x29___closed__7; -x_134 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_134, 0, x_101); -lean_ctor_set(x_134, 1, x_133); -x_135 = l_unexpand____x40_Init_Notation___hyg_1981____closed__1; -x_136 = lean_array_push(x_135, x_115); -x_137 = lean_array_push(x_136, x_132); -x_138 = lean_array_push(x_137, x_134); -x_139 = l_myMacro____x40_Init_Notation___hyg_12862____closed__8; -x_140 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_140, 0, x_139); -lean_ctor_set(x_140, 1, x_138); -x_141 = lean_array_push(x_124, x_31); -x_142 = lean_array_push(x_141, x_140); -x_143 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_143, 0, x_122); -lean_ctor_set(x_143, 1, x_142); -x_144 = lean_array_push(x_124, x_113); -x_145 = lean_array_push(x_144, x_143); -x_146 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_146, 0, x_127); +x_128 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_128, 0, x_121); +lean_ctor_set(x_128, 1, x_2); +x_129 = lean_array_push(x_123, x_127); +x_130 = lean_array_push(x_129, x_128); +x_131 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_131, 0, x_121); +lean_ctor_set(x_131, 1, x_130); +x_132 = l_prec_x28___x29___closed__7; +x_133 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_133, 0, x_100); +lean_ctor_set(x_133, 1, x_132); +x_134 = l_unexpand____x40_Init_Notation___hyg_1981____closed__1; +x_135 = lean_array_push(x_134, x_114); +x_136 = lean_array_push(x_135, x_131); +x_137 = lean_array_push(x_136, x_133); +x_138 = l_myMacro____x40_Init_Notation___hyg_12862____closed__8; +x_139 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_139, 0, x_138); +lean_ctor_set(x_139, 1, x_137); +x_140 = lean_array_push(x_123, x_31); +x_141 = lean_array_push(x_140, x_139); +x_142 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_142, 0, x_121); +lean_ctor_set(x_142, 1, x_141); +x_143 = lean_array_push(x_123, x_112); +x_144 = lean_array_push(x_143, x_142); +x_145 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_145, 0, x_126); +lean_ctor_set(x_145, 1, x_144); +x_146 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_146, 0, x_45); lean_ctor_set(x_146, 1, x_145); -x_147 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_147, 0, x_45); -lean_ctor_set(x_147, 1, x_146); -x_148 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_148, 0, x_147); -x_23 = x_148; -x_24 = x_108; +x_147 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_147, 0, x_146); +x_23 = x_147; +x_24 = x_107; goto block_29; } } else { -uint8_t x_149; +uint8_t x_148; lean_dec(x_31); lean_dec(x_30); lean_dec(x_22); @@ -936,23 +874,23 @@ lean_dec(x_13); lean_dec(x_12); lean_dec(x_8); lean_dec(x_2); -x_149 = !lean_is_exclusive(x_35); -if (x_149 == 0) +x_148 = !lean_is_exclusive(x_35); +if (x_148 == 0) { return x_35; } else { -lean_object* x_150; lean_object* x_151; lean_object* x_152; -x_150 = lean_ctor_get(x_35, 0); -x_151 = lean_ctor_get(x_35, 1); -lean_inc(x_151); +lean_object* x_149; lean_object* x_150; lean_object* x_151; +x_149 = lean_ctor_get(x_35, 0); +x_150 = lean_ctor_get(x_35, 1); lean_inc(x_150); +lean_inc(x_149); lean_dec(x_35); -x_152 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_152, 0, x_150); -lean_ctor_set(x_152, 1, x_151); -return x_152; +x_151 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_151, 0, x_149); +lean_ctor_set(x_151, 1, x_150); +return x_151; } } block_29: @@ -973,6 +911,22 @@ goto _start; } else { +lean_object* x_152; +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_2); +x_152 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_152, 0, x_9); +lean_ctor_set(x_152, 1, x_16); +return x_152; +} +} +else +{ lean_object* x_153; lean_dec(x_15); lean_dec(x_14); @@ -987,22 +941,6 @@ lean_ctor_set(x_153, 1, x_16); return x_153; } } -else -{ -lean_object* x_154; -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_2); -x_154 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_154, 0, x_9); -lean_ctor_set(x_154, 1, x_16); -return x_154; -} -} } lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__5___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16) { _start: @@ -2950,7 +2888,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_ x_9 = l_Lean_instInhabitedName; x_10 = lean_unsigned_to_nat(0u); x_11 = lean_array_get(x_9, x_1, x_10); -x_12 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7; +x_12 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__5; lean_inc(x_2); x_13 = l_Lean_Elab_Deriving_mkContext(x_12, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8); if (lean_obj_tag(x_13) == 0) @@ -3745,7 +3683,25 @@ lean_dec(x_1); return x_9; } } -static lean_object* _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1() { +static lean_object* _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("HashableUSize"); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3() { _start: { lean_object* x_1; @@ -3753,12 +3709,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Deriving_Hashable_mkHashableHandler return x_1; } } -lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587_(lean_object* x_1) { +lean_object* l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Elab_Deriving_Hashable_mkHashableHeader___rarg___closed__2; -x_3 = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1; +x_2 = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2; +x_3 = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3; x_4 = l_Lean_Elab_registerBuiltinDerivingHandler(x_2, x_3, x_1); if (lean_obj_tag(x_4) == 0) { @@ -3835,16 +3791,6 @@ l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4 lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__7); l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8(); lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__8); -l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__9); -l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__10); -l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__11); -l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__12); -l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13 = _init_l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13(); -lean_mark_persistent(l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__13); l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___closed__1 = _init_l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___closed__1(); lean_mark_persistent(l_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___closed__1); l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__1 = _init_l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__1(); @@ -3865,9 +3811,13 @@ l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashabl lean_mark_persistent(l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__1); l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__2 = _init_l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__2(); lean_mark_persistent(l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__2); -l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1 = _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1(); -lean_mark_persistent(l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587____closed__1); -res = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1587_(lean_io_mk_world()); +l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1 = _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1(); +lean_mark_persistent(l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__1); +l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2 = _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2(); +lean_mark_persistent(l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__2); +l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3 = _init_l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3(); +lean_mark_persistent(l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575____closed__3); +res = l_Lean_Elab_Deriving_Hashable_initFn____x40_Lean_Elab_Deriving_Hashable___hyg_1575_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Elab/Term.c b/stage0/stdlib/Lean/Elab/Term.c index 0ce16de32a..35cdc96aa5 100644 --- a/stage0/stdlib/Lean/Elab/Term.c +++ b/stage0/stdlib/Lean/Elab/Term.c @@ -207,6 +207,7 @@ lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_throwMVarError___spe lean_object* l_Lean_Elab_Term_State_letRecsToLift___default; lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__3; lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Level_instHashableUSizeLevel; lean_object* l_Lean_MetavarContext_getExprAssignment_x3f(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_applyResult___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -430,6 +431,7 @@ lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_HashSetImp_moveEntries___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__4; +lean_object* l_instHashableUSizeProd___rarg___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_1997____closed__4; extern lean_object* l_Lean_maxRecDepth; lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_elabOpen___spec__13(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -569,7 +571,6 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_saveContext(lean_objec lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__1; lean_object* l___private_Init_Data_String_Basic_0__Substring_takeRightWhileAux___at_Lean_Elab_Term_resolveName_x27___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_mkTypeMismatchError___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Level_instHashableLevel; lean_object* l_Lean_Elab_Term_isExprMVarAssigned___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabProp___rarg(lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambdaAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1227,7 +1228,6 @@ lean_object* l___private_Lean_MonadEnv_0__Lean_checkUnsupported___at_Lean_Elab_T lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabStrLit___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__2; lean_object* l_List_map___at_Lean_Elab_Term_resolveName_x27___spec__4(lean_object*, lean_object*); extern lean_object* l_Lean_Meta_Context_config___default___closed__1; @@ -1252,7 +1252,6 @@ lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_ob lean_object* l_Lean_Elab_Term_instToStringSyntheticMVarKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabByTactic___closed__3; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Elab_Term_getLetRecsToLift___boxed(lean_object*); lean_object* l_List_foldlM___at_Lean_Elab_Term_evalExpr___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Exception___hyg_3____closed__1; @@ -1436,6 +1435,7 @@ lean_object* l_Array_contains___at_Lean_Elab_Term_logUnassignedUsingErrorInfos__ lean_object* l_Lean_Elab_Term_resolveName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_withAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_setPostponed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Elab_Term_resolveName___closed__1; lean_object* l_Lean_Elab_Term_mkAuxName___closed__1; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -52580,8 +52580,8 @@ static lean_object* _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuc _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Level_instHashableLevel; -x_2 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2); +x_1 = l_Lean_Level_instHashableUSizeLevel; +x_2 = lean_alloc_closure((void*)(l_instHashableUSizeProd___rarg___boxed), 3, 2); lean_closure_set(x_2, 0, x_1); lean_closure_set(x_2, 1, x_1); return x_2; diff --git a/stage0/stdlib/Lean/Expr.c b/stage0/stdlib/Lean/Expr.c index 49d6a7f5e8..063409f34e 100644 --- a/stage0/stdlib/Lean/Expr.c +++ b/stage0/stdlib/Lean/Expr.c @@ -67,7 +67,6 @@ uint8_t l_USize_decEq(size_t, size_t); lean_object* lean_array_uget(lean_object*, size_t); lean_object* l_Lean_Expr_replaceFVarId___boxed(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_isProp(lean_object*); -lean_object* l_Lean_Expr_instHashableExpr___closed__1; lean_object* lean_expr_update_mdata(lean_object*, lean_object*); lean_object* l_Lean_Expr_bindingDomain_x21(lean_object*); lean_object* l_Lean_Expr_getAppArgs(lean_object*); @@ -86,7 +85,6 @@ lean_object* l_Lean_BinderInfo_isExplicit_match__1___rarg(uint8_t, lean_object*, lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParams___spec__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_isMVar_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_isApp_match__1(lean_object*); -lean_object* l_Lean_ExprStructEq_instHashableExprStructEq; uint64_t l_Bool_toUInt64(uint8_t); lean_object* l_Lean_Expr_updateMData_x21___closed__2; lean_object* l_Lean_Expr_instantiateLevelParamsArray___boxed(lean_object*, lean_object*, lean_object*); @@ -160,6 +158,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_betaRevAux_match__1___rarg(lean_ lean_object* l_Lean_Expr_ctorName___closed__4; uint8_t l_List_foldr___at_Lean_mkConst___spec__2(uint8_t, lean_object*); uint8_t l_Lean_Expr_isBVar(lean_object*); +lean_object* l_Lean_instHashableUSizeLiteral___closed__1; lean_object* lean_expr_instantiate1(lean_object*, lean_object*); lean_object* l_Lean_Literal_type___closed__3; lean_object* l_Lean_Expr_isLet_match__1(lean_object*); @@ -169,7 +168,6 @@ lean_object* lean_expr_lift_loose_bvars(lean_object*, lean_object*, lean_object* uint8_t lean_expr_has_level_mvar(lean_object*); lean_object* l_Lean_ExprStructEq_instBEqExprStructEq___closed__1; lean_object* l_Lean_Expr_updateForall_x21___closed__1; -lean_object* l_Lean_ExprStructEq_instHashableExprStructEq___closed__1; lean_object* l_Lean_Expr_appFn_x21___closed__3; lean_object* l_Lean_Expr_isNatLit_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_getOptParamDefault_x3f(lean_object*); @@ -212,6 +210,7 @@ lean_object* l_Lean_ExprStructEq_instBEqExprStructEq; lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Expr_hasExprMVarEx___boxed(lean_object*); lean_object* l_Lean_Expr_hasExprMVar___boxed(lean_object*); +lean_object* l_Lean_Expr_instHashableUSizeExpr; lean_object* l_Lean_mkAppRev___boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_getAppNumArgs(lean_object*); lean_object* l_Lean_mkFreshFVarId(lean_object*); @@ -341,7 +340,6 @@ lean_object* l_Lean_Expr_setAppPPExplicitForExposingMVars(lean_object*); lean_object* l_Lean_Expr_fvarId_x21___closed__1; lean_object* l_Lean_Expr_updateConst_x21___closed__2; lean_object* lean_expr_mk_bvar(lean_object*); -lean_object* l_Lean_Expr_instHashableExpr; lean_object* l_Lean_mkDecIsTrue___closed__2; size_t l_Lean_Expr_hash(lean_object*); lean_object* l_Lean_Expr_mvarId_x21___closed__3; @@ -362,7 +360,9 @@ lean_object* lean_expr_mk_const(lean_object*, lean_object*); lean_object* l_Lean_Expr_data_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Literal_lt_match__1(lean_object*); lean_object* l_Lean_mkAppRange(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_ExprStructEq_instHashableUSizeExprStructEq; lean_object* l_Lean_Expr_isCharLit___closed__3; +lean_object* l_Lean_instHashableUSizeBinderInfo; lean_object* l_Lean_Literal_type___closed__4; lean_object* l_Lean_mkDecIsTrue___closed__4; lean_object* lean_expr_mk_lit(lean_object*); @@ -380,6 +380,7 @@ lean_object* l___private_Lean_Expr_0__Lean_mkAppRangeAux___boxed(lean_object*, l lean_object* l_Lean_Expr_updateProj_x21___closed__3; lean_object* l_Lean_Expr_hasAnyFVar_visit_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Literal_type___closed__2; +lean_object* l_Lean_instHashableUSizeLiteral; lean_object* l_Lean_Expr_mkDataForLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_instantiate___boxed(lean_object*, lean_object*); uint8_t l___private_Lean_Expr_0__Lean_beqLiteral____x40_Lean_Expr___hyg_30_(lean_object*, lean_object*); @@ -474,7 +475,6 @@ lean_object* l_Lean_Expr_appFn_x21___boxed(lean_object*); lean_object* l_Lean_Expr_hasLevelMVarEx___boxed(lean_object*); lean_object* l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_237____boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_isAtomic_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_instHashableBinderInfo___closed__1; lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_eta(lean_object*); lean_object* lean_expr_mk_mvar(lean_object*); @@ -505,7 +505,6 @@ uint8_t l_Lean_Expr_hasMVar(lean_object*); lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*); uint64_t l_Lean_instInhabitedData__1; lean_object* l_Lean_instBEqLiteral___closed__1; -lean_object* l_Lean_instHashableBinderInfo; lean_object* l_Lean_BinderInfo_isInstImplicit___boxed(lean_object*); extern lean_object* l_Lean_KVMap_empty; lean_object* l_Lean_Expr_isLambda_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -565,6 +564,7 @@ lean_object* l_Lean_ExprStructEq_instToStringExprStructEq___boxed(lean_object*); lean_object* l_Lean_Expr_inferImplicit___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Expr_setAppPPExplicit___spec__1(size_t, size_t, lean_object*); lean_object* l_Lean_BinderInfo_isAuxDecl___boxed(lean_object*); +lean_object* l_Lean_instHashableUSizeBinderInfo___closed__1; lean_object* l_List_foldl___at_Lean_mkConst___spec__1___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Expr_0__Lean_Expr_mkAppRevRangeAux(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Expr_0__Lean_Expr_etaExpandedAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -589,7 +589,6 @@ lean_object* lean_expr_mk_sort(lean_object*); lean_object* l_Lean_Literal_hash___boxed(lean_object*); lean_object* lean_level_update_succ(lean_object*, lean_object*); lean_object* l_Lean_Expr_isBVar___boxed(lean_object*); -lean_object* l_Lean_instHashableLiteral___closed__1; lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*); lean_object* l_Lean_Expr_instantiateLevelParams___boxed(lean_object*, lean_object*, lean_object*); lean_object* lean_expr_mk_fvar(lean_object*); @@ -609,9 +608,7 @@ uint8_t l_Lean_Expr_isProj(lean_object*); uint8_t l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_237_(uint8_t, uint8_t); lean_object* l_Lean_ExprStructEq_hash_match__1___rarg(lean_object*, lean_object*); uint8_t l_Lean_Expr_binderInfo(lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); uint8_t l_Lean_Expr_isOptParam(lean_object*); -lean_object* l_Lean_instHashableLiteral; uint8_t l_Lean_Expr_isAtomic(lean_object*); lean_object* lean_expr_abstract(lean_object*, lean_object*); lean_object* l_Lean_Expr_getArg_x21(lean_object*, lean_object*, lean_object*); @@ -685,6 +682,7 @@ lean_object* l_Lean_Expr_equal___boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateLet_x21(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Literal_lt(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_mkConst(lean_object*, lean_object*); lean_object* l_Lean_Expr_bindingInfo_x21___boxed(lean_object*); lean_object* l_Lean_mkSimpleThunk(lean_object*); @@ -703,7 +701,9 @@ lean_object* l_Lean_Expr_updateForallE_x21___closed__1; lean_object* l_Lean_Expr_hasAnyFVar_visit(lean_object*, lean_object*); lean_object* lean_expr_update_const(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateSort_x21___closed__1; +lean_object* l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1; lean_object* l_Lean_Expr_isConst___boxed(lean_object*); +lean_object* l_Lean_Expr_instHashableUSizeExpr___closed__1; lean_object* l_Lean_Expr_isConstOf_match__1(lean_object*); size_t lean_string_hash(lean_object*); lean_object* l_Lean_Expr_isNatLit___boxed(lean_object*); @@ -938,7 +938,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_instHashableLiteral___closed__1() { +static lean_object* _init_l_Lean_instHashableUSizeLiteral___closed__1() { _start: { lean_object* x_1; @@ -946,11 +946,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Literal_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_instHashableLiteral() { +static lean_object* _init_l_Lean_instHashableUSizeLiteral() { _start: { lean_object* x_1; -x_1 = l_Lean_instHashableLiteral___closed__1; +x_1 = l_Lean_instHashableUSizeLiteral___closed__1; return x_1; } } @@ -1631,7 +1631,7 @@ x_4 = lean_box(x_3); return x_4; } } -static lean_object* _init_l_Lean_instHashableBinderInfo___closed__1() { +static lean_object* _init_l_Lean_instHashableUSizeBinderInfo___closed__1() { _start: { lean_object* x_1; @@ -1639,11 +1639,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_BinderInfo_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_instHashableBinderInfo() { +static lean_object* _init_l_Lean_instHashableUSizeBinderInfo() { _start: { lean_object* x_1; -x_1 = l_Lean_instHashableBinderInfo___closed__1; +x_1 = l_Lean_instHashableUSizeBinderInfo___closed__1; return x_1; } } @@ -3105,7 +3105,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_Expr_instHashableExpr___closed__1() { +static lean_object* _init_l_Lean_Expr_instHashableUSizeExpr___closed__1() { _start: { lean_object* x_1; @@ -3113,11 +3113,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Expr_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_Expr_instHashableExpr() { +static lean_object* _init_l_Lean_Expr_instHashableUSizeExpr() { _start: { lean_object* x_1; -x_1 = l_Lean_Expr_instHashableExpr___closed__1; +x_1 = l_Lean_Expr_instHashableUSizeExpr___closed__1; return x_1; } } @@ -9809,7 +9809,7 @@ x_1 = l_Lean_ExprStructEq_instBEqExprStructEq___closed__1; return x_1; } } -static lean_object* _init_l_Lean_ExprStructEq_instHashableExprStructEq___closed__1() { +static lean_object* _init_l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1() { _start: { lean_object* x_1; @@ -9817,11 +9817,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_ExprStructEq_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_ExprStructEq_instHashableExprStructEq() { +static lean_object* _init_l_Lean_ExprStructEq_instHashableUSizeExprStructEq() { _start: { lean_object* x_1; -x_1 = l_Lean_ExprStructEq_instHashableExprStructEq___closed__1; +x_1 = l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1; return x_1; } } @@ -15204,10 +15204,10 @@ l_Lean_instBEqLiteral___closed__1 = _init_l_Lean_instBEqLiteral___closed__1(); lean_mark_persistent(l_Lean_instBEqLiteral___closed__1); l_Lean_instBEqLiteral = _init_l_Lean_instBEqLiteral(); lean_mark_persistent(l_Lean_instBEqLiteral); -l_Lean_instHashableLiteral___closed__1 = _init_l_Lean_instHashableLiteral___closed__1(); -lean_mark_persistent(l_Lean_instHashableLiteral___closed__1); -l_Lean_instHashableLiteral = _init_l_Lean_instHashableLiteral(); -lean_mark_persistent(l_Lean_instHashableLiteral); +l_Lean_instHashableUSizeLiteral___closed__1 = _init_l_Lean_instHashableUSizeLiteral___closed__1(); +lean_mark_persistent(l_Lean_instHashableUSizeLiteral___closed__1); +l_Lean_instHashableUSizeLiteral = _init_l_Lean_instHashableUSizeLiteral(); +lean_mark_persistent(l_Lean_instHashableUSizeLiteral); l_Lean_instLTLiteral = _init_l_Lean_instLTLiteral(); lean_mark_persistent(l_Lean_instLTLiteral); l_Lean_instInhabitedBinderInfo = _init_l_Lean_instInhabitedBinderInfo(); @@ -15215,10 +15215,10 @@ l_Lean_instBEqBinderInfo___closed__1 = _init_l_Lean_instBEqBinderInfo___closed__ lean_mark_persistent(l_Lean_instBEqBinderInfo___closed__1); l_Lean_instBEqBinderInfo = _init_l_Lean_instBEqBinderInfo(); lean_mark_persistent(l_Lean_instBEqBinderInfo); -l_Lean_instHashableBinderInfo___closed__1 = _init_l_Lean_instHashableBinderInfo___closed__1(); -lean_mark_persistent(l_Lean_instHashableBinderInfo___closed__1); -l_Lean_instHashableBinderInfo = _init_l_Lean_instHashableBinderInfo(); -lean_mark_persistent(l_Lean_instHashableBinderInfo); +l_Lean_instHashableUSizeBinderInfo___closed__1 = _init_l_Lean_instHashableUSizeBinderInfo___closed__1(); +lean_mark_persistent(l_Lean_instHashableUSizeBinderInfo___closed__1); +l_Lean_instHashableUSizeBinderInfo = _init_l_Lean_instHashableUSizeBinderInfo(); +lean_mark_persistent(l_Lean_instHashableUSizeBinderInfo); l_Lean_MData_empty = _init_l_Lean_MData_empty(); lean_mark_persistent(l_Lean_MData_empty); l_Lean_instInhabitedData__1 = _init_l_Lean_instInhabitedData__1(); @@ -15264,10 +15264,10 @@ l_Lean_Expr_ctorName___closed__8 = _init_l_Lean_Expr_ctorName___closed__8(); lean_mark_persistent(l_Lean_Expr_ctorName___closed__8); l_Lean_Expr_ctorName___closed__9 = _init_l_Lean_Expr_ctorName___closed__9(); lean_mark_persistent(l_Lean_Expr_ctorName___closed__9); -l_Lean_Expr_instHashableExpr___closed__1 = _init_l_Lean_Expr_instHashableExpr___closed__1(); -lean_mark_persistent(l_Lean_Expr_instHashableExpr___closed__1); -l_Lean_Expr_instHashableExpr = _init_l_Lean_Expr_instHashableExpr(); -lean_mark_persistent(l_Lean_Expr_instHashableExpr); +l_Lean_Expr_instHashableUSizeExpr___closed__1 = _init_l_Lean_Expr_instHashableUSizeExpr___closed__1(); +lean_mark_persistent(l_Lean_Expr_instHashableUSizeExpr___closed__1); +l_Lean_Expr_instHashableUSizeExpr = _init_l_Lean_Expr_instHashableUSizeExpr(); +lean_mark_persistent(l_Lean_Expr_instHashableUSizeExpr); l_Lean_Literal_type___closed__1 = _init_l_Lean_Literal_type___closed__1(); lean_mark_persistent(l_Lean_Literal_type___closed__1); l_Lean_Literal_type___closed__2 = _init_l_Lean_Literal_type___closed__2(); @@ -15386,10 +15386,10 @@ l_Lean_ExprStructEq_instBEqExprStructEq___closed__1 = _init_l_Lean_ExprStructEq_ lean_mark_persistent(l_Lean_ExprStructEq_instBEqExprStructEq___closed__1); l_Lean_ExprStructEq_instBEqExprStructEq = _init_l_Lean_ExprStructEq_instBEqExprStructEq(); lean_mark_persistent(l_Lean_ExprStructEq_instBEqExprStructEq); -l_Lean_ExprStructEq_instHashableExprStructEq___closed__1 = _init_l_Lean_ExprStructEq_instHashableExprStructEq___closed__1(); -lean_mark_persistent(l_Lean_ExprStructEq_instHashableExprStructEq___closed__1); -l_Lean_ExprStructEq_instHashableExprStructEq = _init_l_Lean_ExprStructEq_instHashableExprStructEq(); -lean_mark_persistent(l_Lean_ExprStructEq_instHashableExprStructEq); +l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1 = _init_l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1(); +lean_mark_persistent(l_Lean_ExprStructEq_instHashableUSizeExprStructEq___closed__1); +l_Lean_ExprStructEq_instHashableUSizeExprStructEq = _init_l_Lean_ExprStructEq_instHashableUSizeExprStructEq(); +lean_mark_persistent(l_Lean_ExprStructEq_instHashableUSizeExprStructEq); l_Lean_Expr_getOptParamDefault_x3f___closed__1 = _init_l_Lean_Expr_getOptParamDefault_x3f___closed__1(); lean_mark_persistent(l_Lean_Expr_getOptParamDefault_x3f___closed__1); l_Lean_Expr_getOptParamDefault_x3f___closed__2 = _init_l_Lean_Expr_getOptParamDefault_x3f___closed__2(); diff --git a/stage0/stdlib/Lean/HeadIndex.c b/stage0/stdlib/Lean/HeadIndex.c index 395c2bbbf9..b074486896 100644 --- a/stage0/stdlib/Lean/HeadIndex.c +++ b/stage0/stdlib/Lean/HeadIndex.c @@ -19,6 +19,7 @@ lean_object* l_Lean_Expr_toHeadIndex___closed__2; lean_object* l_Lean_Expr_head___boxed(lean_object*); uint8_t lean_name_eq(lean_object*, lean_object*); lean_object* l_Lean_Expr_toHeadIndex___closed__4; +lean_object* l_Lean_HeadIndex_instHashableUSizeHeadIndex; lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Expr_head(lean_object*); lean_object* l___private_Lean_HeadIndex_0__Lean_Expr_headNumArgsAux_match__1(lean_object*); @@ -26,11 +27,10 @@ lean_object* l_Lean_HeadIndex_HeadIndex_hash___boxed(lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Expr_toHeadIndex___closed__3; lean_object* l_Lean_Expr_head_match__1(lean_object*); -lean_object* l_Lean_HeadIndex_instHashableHeadIndex___closed__1; +lean_object* l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1; size_t l_Lean_HeadIndex_HeadIndex_hash(lean_object*); size_t l_Lean_Name_hash(lean_object*); lean_object* l_Lean_Expr_headNumArgs(lean_object*); -lean_object* l_Lean_HeadIndex_instHashableHeadIndex; uint8_t l___private_Lean_Expr_0__Lean_beqLiteral____x40_Lean_Expr___hyg_30_(lean_object*, lean_object*); lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_HeadIndex_HeadIndex_hash_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -52,8 +52,8 @@ lean_object* l_Lean_HeadIndex_HeadIndex_hash_match__1(lean_object*); lean_object* l_Lean_instBEqHeadIndex___closed__1; lean_object* lean_panic_fn(lean_object*, lean_object*); lean_object* l_Lean_Expr_head_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l___private_Lean_HeadIndex_0__Lean_beqHeadIndex____x40_Lean_HeadIndex___hyg_65____boxed(lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Expr_toHeadIndex_match__1(lean_object*); static lean_object* _init_l_Lean_instInhabitedHeadIndex___closed__1() { _start: @@ -716,7 +716,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_HeadIndex_instHashableHeadIndex___closed__1() { +static lean_object* _init_l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1() { _start: { lean_object* x_1; @@ -724,11 +724,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_HeadIndex_HeadIndex_hash___boxed), 1, 0) return x_1; } } -static lean_object* _init_l_Lean_HeadIndex_instHashableHeadIndex() { +static lean_object* _init_l_Lean_HeadIndex_instHashableUSizeHeadIndex() { _start: { lean_object* x_1; -x_1 = l_Lean_HeadIndex_instHashableHeadIndex___closed__1; +x_1 = l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1; return x_1; } } @@ -1456,10 +1456,10 @@ l_Lean_instBEqHeadIndex___closed__1 = _init_l_Lean_instBEqHeadIndex___closed__1( lean_mark_persistent(l_Lean_instBEqHeadIndex___closed__1); l_Lean_instBEqHeadIndex = _init_l_Lean_instBEqHeadIndex(); lean_mark_persistent(l_Lean_instBEqHeadIndex); -l_Lean_HeadIndex_instHashableHeadIndex___closed__1 = _init_l_Lean_HeadIndex_instHashableHeadIndex___closed__1(); -lean_mark_persistent(l_Lean_HeadIndex_instHashableHeadIndex___closed__1); -l_Lean_HeadIndex_instHashableHeadIndex = _init_l_Lean_HeadIndex_instHashableHeadIndex(); -lean_mark_persistent(l_Lean_HeadIndex_instHashableHeadIndex); +l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1 = _init_l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1(); +lean_mark_persistent(l_Lean_HeadIndex_instHashableUSizeHeadIndex___closed__1); +l_Lean_HeadIndex_instHashableUSizeHeadIndex = _init_l_Lean_HeadIndex_instHashableUSizeHeadIndex(); +lean_mark_persistent(l_Lean_HeadIndex_instHashableUSizeHeadIndex); l_Lean_Expr_toHeadIndex___closed__1 = _init_l_Lean_Expr_toHeadIndex___closed__1(); lean_mark_persistent(l_Lean_Expr_toHeadIndex___closed__1); l_Lean_Expr_toHeadIndex___closed__2 = _init_l_Lean_Expr_toHeadIndex___closed__2(); diff --git a/stage0/stdlib/Lean/Level.c b/stage0/stdlib/Lean/Level.c index ffd91ed3a7..437528b001 100644 --- a/stage0/stdlib/Lean/Level.c +++ b/stage0/stdlib/Lean/Level.c @@ -58,10 +58,10 @@ lean_object* l___private_Lean_Level_0__Lean_Level_mkIMaxAux(lean_object*, lean_o lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Level_PP_Result_quote___spec__2(size_t, size_t, lean_object*); lean_object* l_Lean_Level_getOffsetAux___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Level_instHashableUSizeLevel; lean_object* l_Lean_Level_updateMax_x21(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_normLtAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_level_mk_max(lean_object*, lean_object*); -lean_object* l_Lean_Level_instHashableLevel___closed__1; lean_object* l_Lean_Level_instToStringLevel(lean_object*); extern lean_object* l_Array_empty___closed__1; lean_object* l_Lean_Level_mkData___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -140,7 +140,6 @@ uint32_t lean_level_depth(lean_object*); lean_object* l_Lean_Level_isIMax___boxed(lean_object*); lean_object* l___private_Lean_Level_0__Lean_Level_getMaxArgsAux___at_Lean_Level_normalize___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Level_instHashableLevel; uint64_t l_Lean_levelZero___closed__1; lean_object* l_Lean_Level_isExplicit_match__1(lean_object*); uint64_t l_Lean_Level_data(lean_object*); @@ -295,7 +294,6 @@ lean_object* l___private_Lean_Level_0__Lean_Level_getMaxArgsAux_match__1(lean_ob lean_object* l___private_Lean_Level_0__Lean_Level_skipExplicit(lean_object*, lean_object*); lean_object* l_Lean_Level_isEquiv___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Level_0__Lean_Level_getMaxArgsAux___at_Lean_Level_normalize___spec__1(lean_object*, uint8_t, lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* lean_level_mk_zero(lean_object*); uint8_t l_Lean_Level_isZero(lean_object*); extern lean_object* l_prec_x28___x29___closed__7; @@ -317,6 +315,7 @@ lean_object* l_Lean_Level_hash___boxed(lean_object*); extern lean_object* l_unexpand____x40_Init_Notation___hyg_1981____closed__1; lean_object* l_Lean_Level_instantiateParams(lean_object*, lean_object*); uint8_t l_Lean_Level_isSucc(lean_object*); +lean_object* l_Lean_Level_instHashableUSizeLevel___closed__1; lean_object* l_Lean_Level_PP_Result_quote___lambda__5___closed__1; lean_object* l_Lean_Level_PP_Result_max_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_isZero_match__1(lean_object*); @@ -341,6 +340,7 @@ lean_object* l_Lean_Level_addOffsetAux_match__1___rarg___boxed(lean_object*, lea lean_object* l_Lean_Level_instantiateParams_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_level_mk_mvar(lean_object*); lean_object* l_Lean_Level_format(lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Level_quote(lean_object*, lean_object*); lean_object* lean_uint32_to_nat(uint32_t); lean_object* l_Lean_Name_replacePrefix(lean_object*, lean_object*, lean_object*); @@ -836,7 +836,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_Level_instHashableLevel___closed__1() { +static lean_object* _init_l_Lean_Level_instHashableUSizeLevel___closed__1() { _start: { lean_object* x_1; @@ -844,11 +844,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Level_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_Level_instHashableLevel() { +static lean_object* _init_l_Lean_Level_instHashableUSizeLevel() { _start: { lean_object* x_1; -x_1 = l_Lean_Level_instHashableLevel___closed__1; +x_1 = l_Lean_Level_instHashableUSizeLevel___closed__1; return x_1; } } @@ -7446,10 +7446,10 @@ l_Lean_instInhabitedLevel___closed__1 = _init_l_Lean_instInhabitedLevel___closed lean_mark_persistent(l_Lean_instInhabitedLevel___closed__1); l_Lean_instInhabitedLevel = _init_l_Lean_instInhabitedLevel(); lean_mark_persistent(l_Lean_instInhabitedLevel); -l_Lean_Level_instHashableLevel___closed__1 = _init_l_Lean_Level_instHashableLevel___closed__1(); -lean_mark_persistent(l_Lean_Level_instHashableLevel___closed__1); -l_Lean_Level_instHashableLevel = _init_l_Lean_Level_instHashableLevel(); -lean_mark_persistent(l_Lean_Level_instHashableLevel); +l_Lean_Level_instHashableUSizeLevel___closed__1 = _init_l_Lean_Level_instHashableUSizeLevel___closed__1(); +lean_mark_persistent(l_Lean_Level_instHashableUSizeLevel___closed__1); +l_Lean_Level_instHashableUSizeLevel = _init_l_Lean_Level_instHashableUSizeLevel(); +lean_mark_persistent(l_Lean_Level_instHashableUSizeLevel); l_Lean_levelZero___closed__1 = _init_l_Lean_levelZero___closed__1(); l_Lean_levelZero___closed__2 = _init_l_Lean_levelZero___closed__2(); lean_mark_persistent(l_Lean_levelZero___closed__2); diff --git a/stage0/stdlib/Lean/Meta/Basic.c b/stage0/stdlib/Lean/Meta/Basic.c index 4e4cb98db8..91bda4e4a5 100644 --- a/stage0/stdlib/Lean/Meta/Basic.c +++ b/stage0/stdlib/Lean/Meta/Basic.c @@ -43,7 +43,6 @@ lean_object* l_Lean_Meta_instInhabitedParamInfo___closed__1; lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_instantiateMVars___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); size_t l_Lean_Meta_TransparencyMode_hash(uint8_t); lean_object* l_Lean_stringToMessageData(lean_object*); -size_t l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey(lean_object*); lean_object* l_List_foldlM___at___private_Lean_Meta_Basic_0__Lean_Meta_withExistingLocalDeclsImp___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_modifyCache_match__1___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstanceImp_match__1___rarg(uint8_t, lean_object*, lean_object*); @@ -340,7 +339,7 @@ lean_object* l_Lean_Meta_withNewMCtxDepth___rarg(lean_object*, lean_object*, lea lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1735____spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1621____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey_match__1___rarg(lean_object*, lean_object*); +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey_match__1(lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_3____closed__2; lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getPostponed___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -441,7 +440,6 @@ lean_object* l_Lean_Meta_withDefault(lean_object*); lean_object* l_Lean_Meta_approxDefEq___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_instInhabitedLevel___closed__1; -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_3____closed__1; lean_object* l_Lean_Meta_Cache_whnfAll___default; lean_object* l_Lean_Meta_liftMkBindingM(lean_object*); @@ -700,12 +698,10 @@ lean_object* l_Lean_Meta_withTransparency___rarg___lambda__1(uint8_t, lean_objec lean_object* l_Lean_Meta_mkFreshLevelMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_instInhabitedState; lean_object* lean_mk_array(lean_object*, lean_object*); -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey_match__1(lean_object*); lean_object* l___private_Lean_Expr_0__Lean_mkAppRangeAux(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_getDefInfoTemp_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_withLocalDeclsD___spec__1(lean_object*); lean_object* l_Lean_Meta_Cache_inferType___default___closed__1; -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_throwError___at_Lean_Meta_getLocalDeclFromUserName___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_expr_abstract(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withExistingLocalDeclsImp(lean_object*); @@ -771,6 +767,7 @@ lean_object* l_Std_HashMapImp_find_x3f___at_Lean_MetavarContext_instantiateExprM lean_object* l_IO_mkRef___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1735____spec__2(lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_getParamNames___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_local_ctx_find(lean_object*, lean_object*); +size_t l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey(lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); @@ -795,10 +792,13 @@ lean_object* l_Lean_Meta_getLocalDeclFromUserName___closed__1; lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_getConstTemp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_withNewLocalInstance(lean_object*); lean_object* l_List_mapM___at_Lean_Meta_instantiateMVars___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey___boxed(lean_object*); lean_object* l_Lean_throwUnknownConstant___at___private_Lean_Meta_Basic_0__Lean_Meta_getConstTemp_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Meta_getLocalDeclFromUserName___closed__2; lean_object* l_Lean_Meta_setPostponed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_saveState___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Meta_withReducible(lean_object*); lean_object* l_Lean_Meta_withoutProofIrrelevance___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_fvarsSizeLtMaxFVars_match__1(lean_object*); @@ -1247,7 +1247,7 @@ x_1 = l_Lean_Meta_instBEqInfoCacheKey___closed__1; return x_1; } } -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey_match__1___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey_match__1___rarg(lean_object* x_1, lean_object* x_2) { _start: { uint8_t x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; @@ -1262,15 +1262,15 @@ x_7 = lean_apply_3(x_2, x_6, x_4, x_5); return x_7; } } -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey_match__1(lean_object* x_1) { +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey_match__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey_match__1___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey_match__1___rarg), 2, 0); return x_2; } } -size_t l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey(lean_object* x_1) { +size_t l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey(lean_object* x_1) { _start: { uint8_t x_2; lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; @@ -1300,11 +1300,11 @@ return x_15; } } } -lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object* x_1) { +lean_object* l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey___boxed(lean_object* x_1) { _start: { size_t x_2; lean_object* x_3; -x_2 = l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey(x_1); +x_2 = l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey(x_1); lean_dec(x_1); x_3 = lean_box_usize(x_2); return x_3; @@ -1334,7 +1334,7 @@ static lean_object* _init_l_Lean_Meta_Cache_funInfo___default___closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableUSizeInfoCacheKey___boxed), 1, 0); return x_1; } } diff --git a/stage0/stdlib/Lean/Meta/DiscrTreeTypes.c b/stage0/stdlib/Lean/Meta/DiscrTreeTypes.c index 565728b937..fda1e0df3f 100644 --- a/stage0/stdlib/Lean/Meta/DiscrTreeTypes.c +++ b/stage0/stdlib/Lean/Meta/DiscrTreeTypes.c @@ -18,9 +18,9 @@ lean_object* l_Lean_Meta_DiscrTree_instBEqKey___closed__1; lean_object* l___private_Lean_Meta_DiscrTreeTypes_0__Lean_Meta_DiscrTree_beqKey____x40_Lean_Meta_DiscrTreeTypes___hyg_73____boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_DiscrTree_root___default(lean_object*); lean_object* l_Lean_Meta_DiscrTree_instInhabitedKey___closed__1; -lean_object* l_Lean_Meta_DiscrTree_instHashableKey; extern lean_object* l_Std_PersistentHashMap_root___default___closed__2; uint8_t lean_name_eq(lean_object*, lean_object*); +lean_object* l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1; uint8_t l___private_Lean_Meta_DiscrTreeTypes_0__Lean_Meta_DiscrTree_beqKey____x40_Lean_Meta_DiscrTreeTypes___hyg_73_(lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Meta_DiscrTree_Key_hash_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -29,13 +29,13 @@ size_t l_Lean_Name_hash(lean_object*); lean_object* l_Lean_Meta_DiscrTree_instBEqKey; uint8_t l___private_Lean_Expr_0__Lean_beqLiteral____x40_Lean_Expr___hyg_30_(lean_object*, lean_object*); size_t lean_usize_of_nat(lean_object*); -lean_object* l_Lean_Meta_DiscrTree_instHashableKey___closed__1; lean_object* l_Lean_Meta_DiscrTree_instInhabitedKey; size_t l_Lean_Literal_hash(lean_object*); lean_object* l___private_Lean_Meta_DiscrTreeTypes_0__Lean_Meta_DiscrTree_beqKey____x40_Lean_Meta_DiscrTreeTypes___hyg_73__match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l___private_Lean_Meta_DiscrTreeTypes_0__Lean_Meta_DiscrTree_beqKey____x40_Lean_Meta_DiscrTreeTypes___hyg_73__match__1(lean_object*); lean_object* l_Lean_Meta_DiscrTree_Key_hash___boxed(lean_object*); +lean_object* l_Lean_Meta_DiscrTree_instHashableUSizeKey; +size_t lean_usize_mix_hash(size_t, size_t); size_t l_Lean_Meta_DiscrTree_Key_hash(lean_object*); static lean_object* _init_l_Lean_Meta_DiscrTree_instInhabitedKey___closed__1() { _start: @@ -554,7 +554,7 @@ x_3 = lean_box_usize(x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_DiscrTree_instHashableKey___closed__1() { +static lean_object* _init_l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1() { _start: { lean_object* x_1; @@ -562,11 +562,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_DiscrTree_Key_hash___boxed), 1, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_DiscrTree_instHashableKey() { +static lean_object* _init_l_Lean_Meta_DiscrTree_instHashableUSizeKey() { _start: { lean_object* x_1; -x_1 = l_Lean_Meta_DiscrTree_instHashableKey___closed__1; +x_1 = l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1; return x_1; } } @@ -611,10 +611,10 @@ l_Lean_Meta_DiscrTree_instBEqKey___closed__1 = _init_l_Lean_Meta_DiscrTree_instB lean_mark_persistent(l_Lean_Meta_DiscrTree_instBEqKey___closed__1); l_Lean_Meta_DiscrTree_instBEqKey = _init_l_Lean_Meta_DiscrTree_instBEqKey(); lean_mark_persistent(l_Lean_Meta_DiscrTree_instBEqKey); -l_Lean_Meta_DiscrTree_instHashableKey___closed__1 = _init_l_Lean_Meta_DiscrTree_instHashableKey___closed__1(); -lean_mark_persistent(l_Lean_Meta_DiscrTree_instHashableKey___closed__1); -l_Lean_Meta_DiscrTree_instHashableKey = _init_l_Lean_Meta_DiscrTree_instHashableKey(); -lean_mark_persistent(l_Lean_Meta_DiscrTree_instHashableKey); +l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1 = _init_l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1(); +lean_mark_persistent(l_Lean_Meta_DiscrTree_instHashableUSizeKey___closed__1); +l_Lean_Meta_DiscrTree_instHashableUSizeKey = _init_l_Lean_Meta_DiscrTree_instHashableUSizeKey(); +lean_mark_persistent(l_Lean_Meta_DiscrTree_instHashableUSizeKey); l_Lean_Meta_DiscrTree_root___default___closed__1 = _init_l_Lean_Meta_DiscrTree_root___default___closed__1(); lean_mark_persistent(l_Lean_Meta_DiscrTree_root___default___closed__1); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Meta/FunInfo.c b/stage0/stdlib/Lean/Meta/FunInfo.c index 6d50d7266d..66fb7c182c 100644 --- a/stage0/stdlib/Lean/Meta/FunInfo.c +++ b/stage0/stdlib/Lean/Meta/FunInfo.c @@ -90,7 +90,6 @@ lean_object* l_Lean_Meta_getTransparency(lean_object*, lean_object*, lean_object lean_object* l_Std_PersistentHashMap_insertAux_traverse___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2; uint8_t l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_237_(uint8_t, uint8_t); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Std_PersistentHashMap_insertAux___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit_match__1___boxed(lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_findAux___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__2(lean_object*, size_t, lean_object*); @@ -102,6 +101,7 @@ lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit_match_ lean_object* lean_usize_to_nat(size_t); uint8_t l_Lean_Expr_hasFVar(lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___boxed(lean_object*, lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_indexOfAux___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_updateHasFwdDeps___boxed(lean_object*, lean_object*); diff --git a/stage0/stdlib/Lean/Meta/InferType.c b/stage0/stdlib/Lean/Meta/InferType.c index 96f108f549..4316b36ce9 100644 --- a/stage0/stdlib/Lean/Meta/InferType.c +++ b/stage0/stdlib/Lean/Meta/InferType.c @@ -41,7 +41,6 @@ lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferMVarType___boxed( lean_object* l_Lean_throwError___at_Lean_Meta_throwFunctionExpected___spec__1(lean_object*); lean_object* l_Lean_Expr_instantiateBetaRevRange_visit___closed__1; lean_object* l_Std_PersistentHashMap_insertAux_traverse___at___private_Lean_Meta_InferType_0__Lean_Meta_checkInferTypeCache___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_ExprStructEq_instHashableExprStructEq; lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Expr_instantiateBetaRevRange_visit___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferForallType___spec__2(lean_object*); @@ -90,6 +89,7 @@ extern lean_object* l_Lean_ExprStructEq_instBEqExprStructEq; lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Std_AssocList_foldlM___at_Lean_Expr_instantiateBetaRevRange_visit___spec__7(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isArrowProp_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeProd___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Expr_instantiateBetaRevRange_visit___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_isPropQuick___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -146,6 +146,7 @@ lean_object* l_Std_PersistentHashMap_findAtAux___at___private_Lean_Meta_InferTyp lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isArrowType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_throwTypeExcepted___spec__1(lean_object*); lean_object* l_Lean_Expr_instantiateBetaRevRange_visit___closed__11; +extern lean_object* l_Lean_ExprStructEq_instHashableUSizeExprStructEq; lean_object* l_Lean_Meta_throwTypeExcepted___rarg___closed__2; lean_object* l_Lean_Meta_inferTypeImp_infer___closed__2; lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferFVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -196,6 +197,7 @@ lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); lean_object* l_Lean_Meta_isTypeQuick(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkLevelSucc(lean_object*); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isAlwaysZero_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeNat___boxed(lean_object*); uint8_t lean_expr_equal(lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); uint8_t l_USize_decLe(size_t, size_t); @@ -231,17 +233,14 @@ lean_object* l_Lean_Meta_throwUnknownMVar___rarg(lean_object*, lean_object*, lea lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferConstType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_hasLooseBVars(lean_object*); lean_object* l_Lean_Meta_inferTypeImp_infer_match__1(lean_object*); -lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_insert___at___private_Lean_Meta_InferType_0__Lean_Meta_checkInferTypeCache___spec__4(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferForallType___closed__1; extern lean_object* l_Lean_Position_lt___closed__1; lean_object* lean_mk_array(lean_object*, lean_object*); extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2; lean_object* l___private_Lean_Expr_0__Lean_mkAppRangeAux(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_instHashableNat___boxed(lean_object*); lean_object* l_Std_mkHashMap___at_Lean_Expr_instantiateBetaRevRange___spec__1(lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_throwUnknownMVar___spec__1(lean_object*); -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Meta_isProofQuick___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_instantiateBetaRevRange_visit___closed__5; lean_object* l_Lean_Meta_lambdaLetTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___spec__1(lean_object*); @@ -282,6 +281,7 @@ lean_object* l_Lean_indentExpr(lean_object*); lean_object* l_Lean_mkBVar(lean_object*); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_inferAppType_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__1___rarg(lean_object*, lean_object*); +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l___private_Lean_Meta_InferType_0__Lean_Meta_isArrowProp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkConst(lean_object*, lean_object*); lean_object* l_Lean_Meta_isTypeQuick___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1269,7 +1269,7 @@ static lean_object* _init_l_Lean_Expr_instantiateBetaRevRange_visit___closed__3( _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_instHashableNat___boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l_instHashableUSizeNat___boxed), 1, 0); return x_1; } } @@ -1277,9 +1277,9 @@ static lean_object* _init_l_Lean_Expr_instantiateBetaRevRange_visit___closed__4( _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_ExprStructEq_instHashableExprStructEq; +x_1 = l_Lean_ExprStructEq_instHashableUSizeExprStructEq; x_2 = l_Lean_Expr_instantiateBetaRevRange_visit___closed__3; -x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2); +x_3 = lean_alloc_closure((void*)(l_instHashableUSizeProd___rarg___boxed), 3, 2); lean_closure_set(x_3, 0, x_1); lean_closure_set(x_3, 1, x_2); return x_3; diff --git a/stage0/stdlib/Lean/Meta/Match/Match.c b/stage0/stdlib/Lean/Meta/Match/Match.c index 513d15eafe..bf2b7b8ce5 100644 --- a/stage0/stdlib/Lean/Meta/Match/Match.c +++ b/stage0/stdlib/Lean/Meta/Match/Match.c @@ -234,6 +234,7 @@ extern lean_object* l_Lean_levelZero; lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__5; lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_commitWhenSome_x3f___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__1___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__2___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Expr_instHashableUSizeExpr; lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___lambda__1___closed__4; lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f_match__1(lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandNatValuePattern(lean_object*); @@ -242,6 +243,7 @@ lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_ uint8_t l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasNonTrivialExample___spec__1(uint8_t, lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_Match_withMkMatcherInput___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeProd___rarg___boxed(lean_object*, lean_object*, lean_object*); uint32_t l_UInt32_add(uint32_t, uint32_t); lean_object* l_ReaderT_pure___at_Lean_Meta_Match_mkMatcher___spec__5(lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_mkMinorType___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -403,7 +405,6 @@ lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_6859___ lean_object* l_Lean_Meta_Match_mkMatcher___lambda__2___closed__4; lean_object* l_Lean_Meta_Match_matcherExt; lean_object* l_Lean_addTrace___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_Expr_instHashableExpr; lean_object* l_Lean_Meta_Match_Unify_assign(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_foldr___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_inLocalDecls___spec__1___boxed(lean_object*, lean_object*, lean_object*); size_t l_Lean_Expr_hash(lean_object*); @@ -544,6 +545,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Match_Match_0__Lean lean_object* l_List_redLength___rarg(lean_object*); lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_instHashableUSizeBool___boxed(lean_object*); lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__4(lean_object*); lean_object* l_Lean_Meta_Cases_cases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes___closed__1; @@ -695,7 +697,6 @@ lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__5___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_throwError___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwInductiveTypeExpected___spec__1(lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwNonSupported___closed__1; -lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_Match_MatcherInfo_arity(lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_Match_Unify_unify(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -715,7 +716,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f(lean lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_checkVarDeps___closed__1; lean_object* l_Lean_Meta_Match_Unify_occurs___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_traceStep___closed__1; -size_t lean_usize_mix_hash(size_t, size_t); lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_GeneralizeTelescope_generalizeTelescopeAux___spec__1___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -782,7 +782,6 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*); uint8_t l_List_isEmpty___rarg(lean_object*); lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_search___closed__3; -lean_object* l_instHashableBool___boxed(lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkLevelParam(lean_object*); @@ -813,6 +812,7 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasAsPattern_m lean_object* l_List_mapM___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processVariable___spec__1___closed__1; lean_object* l_Lean_Meta_kabstract(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_6883____closed__6; +size_t lean_usize_mix_hash(size_t, size_t); lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_search___closed__1; lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Closure_mkBinding___spec__1(size_t, size_t, lean_object*); lean_object* l_Lean_mkConst(lean_object*, lean_object*); @@ -22916,7 +22916,7 @@ static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match_ _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_instHashableBool___boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l_instHashableUSizeBool___boxed), 1, 0); return x_1; } } @@ -22924,9 +22924,9 @@ static lean_object* _init_l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match_ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Expr_instHashableExpr; +x_1 = l_Lean_Expr_instHashableUSizeExpr; x_2 = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_Match___hyg_6883____closed__4; -x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2); +x_3 = lean_alloc_closure((void*)(l_instHashableUSizeProd___rarg___boxed), 3, 2); lean_closure_set(x_3, 0, x_1); lean_closure_set(x_3, 1, x_2); return x_3; diff --git a/stage0/stdlib/Lean/Meta/TransparencyMode.c b/stage0/stdlib/Lean/Meta/TransparencyMode.c index d269a06a5b..c7dee72635 100644 --- a/stage0/stdlib/Lean/Meta/TransparencyMode.c +++ b/stage0/stdlib/Lean/Meta/TransparencyMode.c @@ -20,11 +20,9 @@ lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparenc lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__10; uint8_t l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_11_(uint8_t, uint8_t); lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_11__match__1(lean_object*); -lean_object* l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59__match__1(lean_object*); lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__12; uint8_t l_Lean_Meta_instInhabitedTransparencyMode; -lean_object* l_Lean_Meta_TransparencyMode_instHashableTransparencyMode; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59__match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_TransparencyMode_lt___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59_(uint8_t, lean_object*); @@ -45,6 +43,7 @@ lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparency lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__21; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__13; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__23; +lean_object* l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__6; uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_beqTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_11__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -56,6 +55,7 @@ lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparenc lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__22; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__5; lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__14; +lean_object* l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1; lean_object* l_Lean_Meta_TransparencyMode_lt_match__1(lean_object*); lean_object* l_Lean_Meta_TransparencyMode_hash___boxed(lean_object*); lean_object* l___private_Lean_Meta_TransparencyMode_0__Lean_Meta_reprTransparencyMode____x40_Lean_Meta_TransparencyMode___hyg_59____closed__3; @@ -797,7 +797,7 @@ x_4 = lean_box_usize(x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1() { +static lean_object* _init_l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1() { _start: { lean_object* x_1; @@ -805,11 +805,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_hash___boxed), 1, return x_1; } } -static lean_object* _init_l_Lean_Meta_TransparencyMode_instHashableTransparencyMode() { +static lean_object* _init_l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode() { _start: { lean_object* x_1; -x_1 = l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1; +x_1 = l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1; return x_1; } } @@ -1143,10 +1143,10 @@ l_Lean_Meta_instReprTransparencyMode___closed__1 = _init_l_Lean_Meta_instReprTra lean_mark_persistent(l_Lean_Meta_instReprTransparencyMode___closed__1); l_Lean_Meta_instReprTransparencyMode = _init_l_Lean_Meta_instReprTransparencyMode(); lean_mark_persistent(l_Lean_Meta_instReprTransparencyMode); -l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1 = _init_l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1(); -lean_mark_persistent(l_Lean_Meta_TransparencyMode_instHashableTransparencyMode___closed__1); -l_Lean_Meta_TransparencyMode_instHashableTransparencyMode = _init_l_Lean_Meta_TransparencyMode_instHashableTransparencyMode(); -lean_mark_persistent(l_Lean_Meta_TransparencyMode_instHashableTransparencyMode); +l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1 = _init_l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1(); +lean_mark_persistent(l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode___closed__1); +l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode = _init_l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode(); +lean_mark_persistent(l_Lean_Meta_TransparencyMode_instHashableUSizeTransparencyMode); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Lean/Util/ForEachExpr.c b/stage0/stdlib/Lean/Util/ForEachExpr.c index b87efd2cf8..f925129bc5 100644 --- a/stage0/stdlib/Lean/Util/ForEachExpr.c +++ b/stage0/stdlib/Lean/Util/ForEachExpr.c @@ -35,6 +35,7 @@ lean_object* l_Lean_ForEachExpr_visit___rarg___lambda__4(lean_object*, lean_obje lean_object* l_Lean_ForEachExpr_visit___at_Lean_Expr_forEach___spec__1___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_forEach___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); +extern lean_object* l_Lean_Expr_instHashableUSizeExpr; lean_object* lean_array_fget(lean_object*, lean_object*); lean_object* l_Lean_Expr_forEach___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_HashMapImp_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -48,7 +49,6 @@ lean_object* l_Lean_ForEachExpr_visit___at_Lean_Expr_forEach___spec__1___rarg___ lean_object* l_Lean_ForEachExpr_visit___at_Lean_Expr_forEach___spec__1___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ForEachExpr_visit___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_MonadCacheT_run___rarg___closed__1; -extern lean_object* l_Lean_Expr_instHashableExpr; size_t l_Lean_Expr_hash(lean_object*); size_t lean_usize_modn(size_t, lean_object*); lean_object* l_Lean_ForEachExpr_visit___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -244,7 +244,7 @@ _start: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; x_4 = l_Lean_Expr_instBEqExpr; -x_5 = l_Lean_Expr_instHashableExpr; +x_5 = l_Lean_Expr_instHashableUSizeExpr; x_6 = l_Std_HashMapImp_find_x3f___rarg(x_4, x_5, x_3, x_1); x_7 = lean_ctor_get(x_2, 0); lean_inc(x_7); @@ -459,7 +459,7 @@ _start: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_4 = l_Lean_Expr_instBEqExpr; -x_5 = l_Lean_Expr_instHashableExpr; +x_5 = l_Lean_Expr_instHashableUSizeExpr; x_6 = l_Std_HashMapImp_insert___rarg(x_4, x_5, x_3, x_1, x_2); x_7 = lean_box(0); x_8 = lean_alloc_ctor(0, 2, 0);