refactor: remove many used Target methods

tydeu · tydeu · commit f1d992169f54 · 2022-07-26T23:40:29.000-04:00
diff --git a/Lake/Build/Context.lean b/Lake/Build/Context.lean
@@ -19,7 +19,7 @@ namespace Lake
 abbrev BuildTask := OptionIOTask
 
 /-- A Lake build job. -/
-abbrev Job := BuildTask BuildTrace
+abbrev Job := BuildTask Unit
 
 /-- A Lake context with some additional caching for builds. -/
 structure BuildContext extends Context where
diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
@@ -42,12 +42,12 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
     let mods := (← getWorkspace).processImportList imports
     let (importTargets, bStore) ← RecBuildM.runIn {} <| mods.mapM fun mod =>
       if mod.shouldPrecompile then
-        buildIndexTop mod.dynlib <&> (·.withoutInfo)
+        (discard ·.task) <$> buildIndexTop mod.dynlib
       else
-        buildIndexTop mod.leanBin
+        (discard ·.task) <$> buildIndexTop mod.leanBin
     let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet
     let externLibTargets := bStore.collectSharedExternLibs
-    importTargets.forM (·.buildOpaque)
+    importTargets.forM (liftM <| await ·)
     -- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care)
     let dynlibs ← dynlibTargets.mapM fun dynlib => do
       return FilePath.mk <| nameToSharedLib (← dynlib.build).toString
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
@@ -102,7 +102,7 @@ export BuildInfo (build)
 @[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (ActiveBuildTarget α))
 [h : FamilyDef Fam facet (ActiveBuildTarget α)] : FacetConfig Fam ι facet where
   build := cast (by rw [← h.family_key_eq_type]) build
-  getJob? := some (fun data => let_fun target := ofFamily data; (·.2) <$> target.task)
+  getJob? := some fun data => discard <| ofFamily data
 
 /-! ### Lean Executable Builds -/
 
diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean
@@ -13,81 +13,72 @@ namespace Lake
 /-! # Active Targets -/
 --------------------------------------------------------------------------------
 
-structure ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) where
-  task : k (ι × τ)
-
-instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) :=
-  ⟨⟨pure default⟩⟩
+def ActiveTarget.{u,v} (ι : Type u) (k : Type u → Type v) (τ : Type u) :=
+  k (ι × τ)
 
 namespace ActiveTarget
 
-def withoutInfo [Functor k] (target :  ActiveTarget ι k t) : ActiveTarget PUnit k t :=
-  mk <| (fun (_,t) => ((),t)) <$> target.task
+@[inline] def  mk (task : k (ι × τ)) : ActiveTarget ι k τ :=
+  task
 
-def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t :=
-  mk <| ((), ·) <$> task
+@[inline] def  task (target : ActiveTarget ι k τ) : k (ι × τ) :=
+  target
 
-protected def pure [Pure k] (info : ι) (trace : τ) : ActiveTarget ι k τ :=
-  mk <| pure (info, trace)
-
-def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ :=
-  mk <| pure ((), nilTrace)
+instance [Inhabited ι] [Inhabited τ] [Pure k] : Inhabited (ActiveTarget ι k τ) :=
+  ⟨mk <| pure default⟩
 
-protected def bindSync [BindSync m n k] (self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) :=
-  bindSync self.task fun (i, a) => f i a
+@[inline] def «opaque» [Functor k] (task : k t) : ActiveTarget PUnit k t :=
+  mk <| ((), ·) <$> task
 
-protected def bindOpaqueSync [BindSync m n k] (self : ActiveTarget ι k α) (f : α → m β) : n (k β) :=
-  bindSync self.task fun (_, a) => f a
+@[inline] def nil [NilTrace τ] [Pure k] : ActiveTarget PUnit k τ :=
+  mk <| pure ((), nilTrace)
 
-protected def bindAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) :=
-  bindAsync self.task fun (i, a) => f i a
+@[inline] protected def bindSync [BindSync m n k]
+(self : ActiveTarget ι k α) (f : ι → α → m β) : n (k β) :=
+  bindSync self fun (i, a) => f i a
 
-protected def bindOpaqueAsync [BindAsync n k] (self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) :=
-  bindAsync self.task fun (_, a) => f a
+@[inline] protected def bindOpaqueSync [BindSync m n k]
+(self : ActiveTarget ι k α) (f : α → m β) : n (k β) :=
+  bindSync self fun (_, a) => f a
 
-def materialize [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m τ :=
-  (·.2) <$> liftM (await self.task)
+@[inline] protected def bindAsync [BindAsync n k]
+(self : ActiveTarget ι k α) (f : ι → α → n (k β)) : n (k β) :=
+  bindAsync self fun (i, a) => f i a
 
-def materializeAsync [Functor k] (self : ActiveTarget ι k τ) : k τ :=
-  (·.2) <$> self.task
+@[inline] protected def bindOpaqueAsync [BindAsync n k]
+(self : ActiveTarget ι k α) (f : α → n (k β)) : n (k β) :=
+  bindAsync self fun (_, a) => f a
 
-def build [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι :=
+@[inline] def build
+[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m ι :=
   (·.1) <$> liftM (await self.task)
 
-def buildOpaque [Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit :=
-  discard <| self.materialize
+@[inline] def buildOpaque
+[Await k n] [MonadLiftT n m] [Functor m] (self : ActiveTarget ι k τ) : m PUnit :=
+  discard <| liftM (await self.task)
 
-def mixOpaqueAsync
-[MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m]
-(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) := do
-  pure <| mk <| ← liftM <| seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.task t2.task
+variable [MixTrace τ] [SeqWithAsync n k] [MonadLiftT n m] [Monad m]
 
-section
-variable [NilTrace τ] [MixTrace τ]
-
-def materializeList [Await k n] [MonadLiftT n m] [Monad m] (targets : List (ActiveTarget ι k τ)) : m τ := do
-  targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace
-
-def materializeArray [Await k n] [MonadLiftT n m] [Monad m] (targets : Array (ActiveTarget ι k τ)) : m τ := do
-  targets.foldlM (fun tr t => return mixTrace tr <| ← t.materialize) nilTrace
+def mixOpaqueAsync
+(t1 : ActiveTarget α k τ) (t2 : ActiveTarget β k τ) : m (ActiveTarget PUnit k τ) :=
+  mk <$> liftM (seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1 t2)
 
-variable [SeqWithAsync n k] [Monad n] [MonadLiftT n m] [Monad m] [Pure k]
+variable [NilTrace τ] [Monad n] [Pure k]
 
 def collectList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget (List ι) k τ) := mk <$> do
-  liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) <| targets.map (·.task)
+  liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) targets
 
 def collectArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget (Array ι) k τ) := mk <$> do
-  liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) <| targets.map (·.task)
+  liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) targets
 
 variable [Functor k]
 
 def collectOpaqueList (targets : List (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do
-  liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace <| targets.map (·.task)
+  liftM <| foldLeftListAsync (fun (_,t') t => mixTrace t t') nilTrace targets
 
 def collectOpaqueArray (targets : Array (ActiveTarget ι k τ)) : m (ActiveTarget PUnit k τ) := «opaque» <$> do
-  liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace <| targets.map (·.task)
+  liftM <| foldRightArrayAsync (fun t (_,t') => mixTrace t t') nilTrace targets
 
-end
 end ActiveTarget
 
 --------------------------------------------------------------------------------
@@ -102,88 +93,46 @@ instance [Inhabited ι] [Inhabited τ] [Pure n] [Pure k] : Inhabited (Target ι
 
 namespace Target
 
-def «opaque» [Functor n] [Functor k] (task : n (k τ)) : Target PUnit n k τ :=
-  mk <| ((fun t => ((), t)) <$> ·) <$> task
-
-def opaqueSync [Sync m n k] [Functor m] (act : m τ) : Target PUnit n k τ :=
-  mk <| sync <| ((), ·) <$> act
-
-def opaqueAsync [Async m n k] [Functor m] (act : m τ) : Target PUnit n k τ :=
-  mk <| async <| ((), ·) <$> act
+@[inline] def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ :=
+  mk <| pure target
 
-protected def sync [Sync m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ :=
-  mk <| sync <| (info, ·) <$> act
-
-protected def async [Async m n k] [Functor m] (info : ι) (act : m τ) : Target ι n k τ :=
-  mk <| async <| (info, ·) <$> act
-
-def active [Pure n] (target : ActiveTarget ι k τ) : Target ι n k τ :=
-  mk <| pure target.task
-
-protected def pure [Pure n] [Pure k] (info : ι) (trace : τ) : Target ι n k τ :=
-  mk <| pure <| pure (info, trace)
-
-def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ :=
+@[inline] def nil [NilTrace τ] [Pure n] [Pure k] : Target PUnit n k τ :=
   mk <| pure <| pure <| ((), nilTrace)
 
-def computeSync [Functor m] [ComputeTrace ι m τ] [Sync m n k] (info : ι) : Target ι n k τ :=
-  mk <| sync <| (info, ·) <$> ComputeTrace.computeTrace info
-
-def computeAsync [Functor m]  [ComputeTrace ι m τ] [Async m n k] (info : ι) : Target ι n k τ :=
-  mk <| async <| (info, ·) <$> ComputeTrace.computeTrace info
-
-def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) :=
+@[inline] def activate [Functor n] (self : Target ι n k τ) : n (ActiveTarget ι k τ) :=
   (.mk ·) <$> self.task
 
-def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) :=
+@[inline] def materializeAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k τ) :=
   ((·.2) <$> ·) <$> self.task
 
 def materialize [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m τ :=
   liftM self.task >>= fun t => (·.2) <$> liftM (await t)
 
-def build [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m ι :=
-  liftM self.task >>= fun t => (·.1) <$> liftM (await t)
-
-def buildOpaque [Await k m'] [MonadLiftT m' m] [MonadLiftT n m] [Functor m] [Bind m] (self : Target ι n k τ) : m PUnit :=
-  discard self.materialize
-
-def buildAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k ι) :=
-  ((·.1) <$> ·) <$> self.task
-
-def buildOpaqueAsync [Functor n] [Functor k] (self : Target ι n k τ) : n (k PUnit) :=
-  discard <$> self.task
-
-protected def bindSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → m β) : n (k β) :=
+@[inline] protected def bindSync [BindSync m n k] [Bind n]
+(self : Target ι n k τ) (f : ι → τ → m β) : n (k β) :=
   self.task >>= fun tk => bindSync tk fun (i,t) => f i t
 
-protected def bindOpaqueSync [BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) :=
+@[inline] protected def bindOpaqueSync
+[BindSync m n k] [Bind n] (self : Target ι n k τ) (f : τ → m β) : n (k β) :=
   self.task >>= fun tk => bindSync tk fun (_,t) => f t
 
-protected def bindAsync [BindAsync n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → n (k β)) : n (k β) :=
+@[inline] protected def bindAsync
+[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : ι → τ → n (k β)) : n (k β) :=
   self.task >>= fun tk => bindAsync tk fun (i,t) => f i t
 
-protected def bindOpaqueAsync [BindAsync n k] [Bind n] (self : Target ι n k τ) (f : τ → n (k β)) : n (k β) :=
+@[inline] protected def bindOpaqueAsync
+[BindAsync n k] [Bind n] (self : Target ι n k τ) (f : τ → n (k β)) : n (k β) :=
   self.task >>= fun tk => bindAsync tk fun (_,t) => f t
 
 def mixOpaqueAsync
 [MixTrace τ] [SeqWithAsync n k] [Functor k] [Monad n]
-(t1 : Target α n k τ) (t2 :  Target β n k τ) : Target PUnit n k τ :=
-  mk do
-    let tk1 ← t1.materializeAsync
-    let tk2 ← t2.materializeAsync
-    ((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2
+(t1 : Target α n k τ) (t2 :  Target β n k τ) : Target PUnit n k τ := mk do
+  let tk1 ← t1.materializeAsync
+  let tk2 ← t2.materializeAsync
+  ((fun t => ((),t)) <$> ·) <$> seqWithAsync mixTrace tk1 tk2
 
 section
 variable [NilTrace τ] [MixTrace τ]
-
-def materializeList [Await k m] [MonadLiftT n m] [Monad m] (targets : List (Target ι n k τ)) : m τ := do
-  let tasks ← targets.mapM (·.task)
-  tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace
-
-def materializeArray [Await k m] [MonadLiftT n m] [Monad m] (targets : Array (Target ι n k τ)) : m τ := do
-  let tasks ← targets.mapM (·.task)
-  tasks.foldlM (fun tr τ => return mixTrace tr (← liftM <| await τ).2) nilTrace
-
 variable [SeqWithAsync n' k] [Monad n'] [MonadLiftT n' n] [Monad n] [Pure k] [Functor k]
 
 def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do
@@ -192,15 +141,15 @@ def materializeListAsync (targets : List (Target ι n k τ)) : n (k τ) := do
 def materializeArrayAsync (targets : Array (Target ι n k τ)) : n (k τ) := do
   liftM <| foldRightArrayAsync mixTrace nilTrace (← targets.mapM (·.materializeAsync))
 
-def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ :=
-  mk do
-    let tasks ← targets.mapM (·.task)
-    liftM <| foldLeftListAsync (fun (i,t') (a,t) => (i :: a, mixTrace t t')) ([], nilTrace) tasks
+def collectList (targets : List (Target ι n k τ)) : Target (List ι) n k τ := mk do
+  let tasks ← targets.mapM (·.task)
+  let f := fun (i,t') (a,t) => (i :: a, mixTrace t t')
+  liftM <| foldLeftListAsync f ([], nilTrace) tasks
 
-def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ :=
-  mk do
-    let tasks ← targets.mapM (·.task)
-    liftM <| foldRightArrayAsync (fun (a,t) (i,t') => (a.push i, mixTrace t t')) (#[], nilTrace) tasks
+def collectArray (targets : Array (Target ι n k τ)) : Target (Array ι) n k τ := mk do
+  let tasks ← targets.mapM (·.task)
+  let f := fun (a,t) (i,t') => (a.push i, mixTrace t t')
+  liftM <| foldRightArrayAsync f (#[], nilTrace) tasks
 
 def collectOpaqueList (targets : List (Target ι n k τ)) : Target PUnit n k τ :=
   mk <| ((fun t => ((), t)) <$> ·) <$> materializeListAsync targets
diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean
@@ -73,16 +73,3 @@ abbrev OpaqueTarget := BuildTarget Unit
 
 /-- An `ActiveBuildTarget` with no artifact information. -/
 abbrev ActiveOpaqueTarget := ActiveBuildTarget Unit
-
-namespace OpaqueTarget
-
-abbrev mk (task : SchedulerM Job) : OpaqueTarget :=
-  Target.opaque task
-
-abbrev mk' (task : BuildM Job) : OpaqueTarget :=
-  Target.opaque <| task.catchFailure fun _ => pure failure
-
-abbrev async (act : BuildM BuildTrace) : OpaqueTarget :=
-  Target.opaqueAsync act
-
-end OpaqueTarget
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
@@ -17,7 +17,7 @@ structure BuildSpec where
 /-- Get the `Job` associated with some `ActiveBuildTarget` `BuildData`. -/
 @[inline] def BuildData.toJob
 [FamilyDef BuildData k (ActiveBuildTarget α)] (data : BuildData k) : Job :=
-  ofFamily data |>.materializeAsync
+  discard <| ofFamily data
 
 @[inline] def mkBuildSpec (info : BuildInfo)
 [FamilyDef BuildData info.key (ActiveBuildTarget α)] : BuildSpec :=
