From 5219593823be00ef2435e04109d031f1bd5f2f8c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Jun 2021 08:00:23 -0700
Subject: [PATCH] chore: use `UInt64` to define `Name`

---
 src/Init/Prelude.lean   | 26 +++++++++++++++-----------
 src/Lean/Data/Name.lean | 18 +++++++++---------
 2 files changed, 24 insertions(+), 20 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index cd952c9db9..8d0b070829 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1610,41 +1610,45 @@ constant mixHash (u₁ u₂ : UInt64) : UInt64
 constant mixUSizeHash (u₁ u₂ : USize) : USize
 
 @[extern "lean_string_hash"]
-protected constant String.hash (s : @& String) : USize
-@[extern "lean_string_hash"]
-protected constant String.hashUSize (s : @& String) : USize
+protected constant String.hash (s : @& String) : UInt64
 
 instance : HashableUSize String where
-  hashUSize := String.hash
+  hashUSize s := String.hash s |>.toUSize
+
+instance : Hashable String where
+  hash := String.hash
 
 namespace Lean
 
 /- Hierarchical names -/
 inductive Name where
   | anonymous : Name
-  | str : Name → String → USize → Name
-  | num : Name → Nat → USize → Name
+  | str : Name → String → UInt64 → Name
+  | num : Name → Nat → UInt64 → Name
 
 instance : Inhabited Name where
   default := Name.anonymous
 
-protected def Name.hash : Name → USize
-  | Name.anonymous => USize.ofNat32 1723 (by decide)
+protected def Name.hash : Name → UInt64
+  | Name.anonymous => UInt64.ofNatCore 1723 (by decide)
   | 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
+  hashUSize n := Name.hash n |>.toUSize
 
 namespace Name
 
 @[export lean_name_mk_string]
 def mkStr (p : Name) (s : String) : Name :=
-  Name.str p s (mixUSizeHash (hashUSize p) (hashUSize s))
+  Name.str p s (mixHash (hash p) (hash s))
 
 @[export lean_name_mk_numeral]
 def mkNum (p : Name) (v : Nat) : Name :=
-  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))))
+  Name.num p v (mixHash (hash p) (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide))))
 
 def mkSimple (s : String) : Name :=
   mkStr Name.anonymous s
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 92334a9d56..17d43a8bbd 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -13,7 +13,7 @@ instance : Coe String Name := ⟨Name.mkSimple⟩
 namespace Name
 
 @[export lean_name_hash] def hashEx : Name → USize :=
-  Name.hash
+  fun n => Name.hash n |>.toUSize
 
 def getPrefix : Name → Name
   | anonymous => anonymous
@@ -62,31 +62,31 @@ def cmp : Name → Name → Ordering
   | anonymous,   anonymous   => Ordering.eq
   | anonymous,   _           => Ordering.lt
   | _,           anonymous   => Ordering.gt
-  | num p₁ i₁ _, num p₂ i₂ _ => 
-    match cmp p₁ p₂ with  
+  | num p₁ i₁ _, num p₂ i₂ _ =>
+    match cmp p₁ p₂ with
     | Ordering.eq => compare i₁ i₂
     | ord => ord
   | num _ _ _,   str _ _ _   => Ordering.lt
   | str _ _ _,   num _ _ _   => Ordering.gt
-  | str p₁ n₁ _, str p₂ n₂ _ => 
-    match cmp p₁ p₂ with 
+  | str p₁ n₁ _, str p₂ n₂ _ =>
+    match cmp p₁ p₂ with
     | Ordering.eq => compare n₁ n₂
     | ord => ord
-    
+
 def lt (x y : Name) : Bool :=
   cmp x y == Ordering.lt
 
-def quickCmpAux : Name → Name → Ordering 
+def quickCmpAux : Name → Name → Ordering
   | anonymous, anonymous   => Ordering.eq
   | anonymous, _           => Ordering.lt
   | _,         anonymous   => Ordering.gt
-  | num n v _, num n' v' _ => 
+  | num n v _, num n' v' _ =>
     match compare v v' with
     | Ordering.eq => n.quickCmpAux n'
     | ord => ord
   | num _ _ _, str _ _ _   => Ordering.lt
   | str _ _ _, num _ _ _   => Ordering.gt
-  | str n s _, str n' s' _ => 
+  | str n s _, str n' s' _ =>
     match compare s s' with
     | Ordering.eq => n.quickCmpAux n'
     | ord => ord