From d0fbc93143efa2ecf4771670a8b39f89ad2bd677 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 6 Aug 2021 01:58:41 -0400
Subject: [PATCH] refactor: improve Hash traces

---
 Lake/Build.lean       |  8 ++++----
 Lake/BuildTarget.lean |  2 +-
 Lake/BuildTrace.lean  | 41 +++++++++++++++++++++++++++++++----------
 3 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/Lake/Build.lean b/Lake/Build.lean
index e8593f7479..2437f55347 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -65,7 +65,7 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool :=
   try
     let contents ← IO.FS.readFile file
     match contents.toNat? with
-    | some h => Hash.ofNat h == hash
+    | some h => Hash.mk h.toUInt64 == hash
     | none => false
   catch _ =>
     false
@@ -109,11 +109,11 @@ def fetchAfterDirectLocalImports
     -- because other build processes (ex. `.o`) rely on the map being complete
     let importTargets ← imports.mapM fetch
     -- calculate trace
-    let leanHash := hash contents
     let leanMTime ← getMTime leanFile
+    let leanHash := Hash.compute contents
     let importHashes ← importTargets.map (·.hash)
     let importMTimes ← importTargets.map (·.mtime)
-    let fullHash := Hash.foldList leanHash (depsTarget.hash :: importHashes)
+    let fullHash := Hash.mixList (leanHash :: depsTarget.hash :: importHashes)
     let maxMTime := MTime.listMax (leanMTime :: depsTarget.mtime :: importMTimes)
     let hashFile := pkg.modToHashFile mod
     let sameHash ← checkIfSameHash fullHash hashFile
@@ -125,7 +125,7 @@ def fetchAfterDirectLocalImports
     ActiveTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
       skipIf sameHash <| afterTaskList (depsTarget.task :: importTasks) do
         compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs
-        IO.FS.writeFile hashFile (toString fullHash)
+        IO.FS.writeFile hashFile fullHash.toString
 
 /-
   Equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget IO`.
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 3a566a378e..80917465ad 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -235,7 +235,7 @@ def hash (self : LakeTarget a) := self.trace.hash
 def mtime (self : LakeTarget a) := self.trace.mtime
 
 def all (targets : List (LakeTarget a)) : IO (LakeTarget PUnit) := do
-  let hash := Hash.foldList 0 <| targets.map (·.hash)
+  let hash := Hash.mixList <| targets.map (·.hash)
   let mtime := MTime.listMax <| targets.map (·.mtime)
   let task ← BuildTask.all <| targets.map (·.task)
   return ActiveTarget.mk () ⟨hash, mtime⟩ task
diff --git a/Lake/BuildTrace.lean b/Lake/BuildTrace.lean
index 9aca4f6a06..79ae01bfac 100644
--- a/Lake/BuildTrace.lean
+++ b/Lake/BuildTrace.lean
@@ -8,15 +8,32 @@ namespace Lake
 
 -- # Hash Traces
 
-def Hash := UInt64
+structure Hash where
+  val : UInt64
+  deriving BEq, DecidableEq
 
-instance : OfNat Hash n := inferInstanceAs (OfNat UInt64 n)
-instance : Inhabited Hash := inferInstanceAs (Inhabited UInt64)
-instance : BEq Hash := inferInstanceAs (BEq UInt64)
+namespace Hash
 
-def Hash.ofNat (n : Nat) := UInt64.ofNat n
-def Hash.foldList (init : Hash) (hashes : List Hash) :=
-  List.foldl mixHash init hashes
+def nil : Hash :=
+  mk <| 1723 -- same as Name.anonymous
+
+instance : Inhabited Hash := ⟨nil⟩
+
+def compute (str : String) :=
+  mk <| mixHash 1723 (hash str) -- same as Name.mkSimple
+
+def mix (h1 h2 : Hash) : Hash :=
+  mk <| mixHash h1.val h2.val
+
+def mixList (hashes : List Hash) : Hash :=
+  hashes.foldl mix nil
+
+protected def toString (self : Hash) : String :=
+  toString self.val
+
+instance : ToString Hash := ⟨Hash.toString⟩
+
+end Hash
 
 -- # Modification Time Traces
 
@@ -24,6 +41,8 @@ open IO.FS (SystemTime)
 
 def MTime := SystemTime
 
+namespace MTime
+
 instance : Inhabited MTime := ⟨⟨0,0⟩⟩
 instance : OfNat MTime (nat_lit 0) := ⟨⟨0,0⟩⟩
 instance : BEq MTime := inferInstanceAs (BEq SystemTime)
@@ -32,8 +51,10 @@ instance : Ord MTime := inferInstanceAs (Ord SystemTime)
 instance : LT MTime := ltOfOrd
 instance : LE MTime := leOfOrd
 
-def MTime.listMax (mtimes : List MTime) := mtimes.foldl max 0
-def MTime.arrayMax (mtimes : Array MTime) := mtimes.foldl max 0
+def listMax (mtimes : List MTime) := mtimes.foldl max 0
+def arrayMax (mtimes : Array MTime) := mtimes.foldl max 0
+
+end MTime
 
 class GetMTime (α) where
   getMTime : α → IO MTime
@@ -60,6 +81,6 @@ def fromHash (hash : Hash) : LakeTrace :=
   LakeTrace.mk hash 0
 
 def fromMTime (mtime : MTime) : LakeTrace :=
-  LakeTrace.mk 0 mtime
+  LakeTrace.mk Hash.nil mtime
 
 end LakeTrace