From 28320f80ee085f06b3a2e33b27aa08d39da02ed7 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 19 Aug 2021 12:05:28 -0400
Subject: [PATCH] refactor: minor API tweaks

---
 Lake/Target.lean | 14 +++++++-------
 Lake/Trace.lean  | 20 ++++++++++++++++++--
 2 files changed, 25 insertions(+), 9 deletions(-)

diff --git a/Lake/Target.lean b/Lake/Target.lean
index b70fe63100..46a2d2c85c 100644
--- a/Lake/Target.lean
+++ b/Lake/Target.lean
@@ -133,6 +133,9 @@ def opaque (trace : t) (task : m PUnit) : Target t m PUnit :=
 protected def pure [Pure m] (artifact : a) (trace : t) : Target t m a :=
   ⟨artifact, trace, pure ()⟩
 
+def compute [Monad m] [ComputeTrace a m t] (artifact : a) : m (Target t m a) := do
+  Target.pure artifact <| ← computeTrace artifact
+
 def runAsync [Monad m] [Async m n] (self : Target t m a) : m (ActiveTarget t n a) := do
   self.withTask <| ← async self.task
 
@@ -180,9 +183,6 @@ namespace LakeTarget
 def nil : LakeTarget PUnit :=
   Target.pure () LakeTrace.nil
 
-def pure (artifact : a) (hash : Hash) (mtime : MTime) : LakeTarget a :=
-  Target.pure artifact ⟨hash, mtime⟩
-
 def hash (self : LakeTarget a) := self.trace.hash
 def mtime (self : LakeTarget a) := self.trace.mtime
 
@@ -214,8 +214,8 @@ abbrev FileTarget :=
 
 namespace FileTarget
 
-def compute (file : FilePath) : IO FileTarget := do
-  Target.pure file <| ← LakeTrace.compute file
+def compute (file : FilePath) : IO FileTarget :=
+  Target.compute file
 
 end FileTarget
 
@@ -235,8 +235,8 @@ def filesAsList (self : FilesTarget) : List FilePath :=
 def filesAsArray (self : FilesTarget) : Array FilePath :=
   self.artifact
 
-def compute (files : Array FilePath) : IO FilesTarget := do
-  Target.pure files <| mixTraceArray <| ← files.mapM LakeTrace.compute
+def compute (files : Array FilePath) : IO FilesTarget :=
+  Target.compute files
 
 def singleton (target : FileTarget) : FilesTarget :=
   target.withArtifact #[target.file]
diff --git a/Lake/Trace.lean b/Lake/Trace.lean
index 42b31ed1cc..5fbe171f0a 100644
--- a/Lake/Trace.lean
+++ b/Lake/Trace.lean
@@ -34,12 +34,28 @@ class MixTrace.{u} (t : Type u) where
 
 export MixTrace (mixTrace)
 
-def mixTraceList [MixTrace t] [NilTrace t] (traces : List t) : t :=
+section
+variable [MixTrace t] [NilTrace t]
+
+def mixTraceList (traces : List t) : t :=
   traces.foldl mixTrace nilTrace
 
-def mixTraceArray [MixTrace t] [NilTrace t] (traces : Array t) : t :=
+def mixTraceArray (traces : Array t) : t :=
   traces.foldl mixTrace nilTrace
 
+variable [ComputeTrace a m t] [Monad m]
+
+def computeListTrace  (artifacts : List a) : m t :=
+  mixTraceList <$> artifacts.mapM computeTrace
+
+instance : ComputeTrace (List a) m t := ⟨computeListTrace⟩
+
+def computeArrayTrace (artifacts : Array a) : m t :=
+  mixTraceArray <$> artifacts.mapM computeTrace
+
+instance : ComputeTrace (Array a) m t := ⟨computeArrayTrace⟩
+end
+
 --------------------------------------------------------------------------------
 -- # Hash Trace
 --------------------------------------------------------------------------------