From 241665dc27d7bfc40579a8fef2185a8fdb480a80 Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 23 Jun 2022 23:42:12 -0400 Subject: [PATCH] refactor: move `recurse` arg into the monad stack --- Lake/Build/Info.lean | 16 ++++--- Lake/Build/Module1.lean | 30 ++++++------ Lake/Build/Store.lean | 1 - Lake/Build/Topological.lean | 3 +- Lake/Util/EquipT.lean | 92 +++++++++++++++++++++++++++++++++++++ 5 files changed, 118 insertions(+), 24 deletions(-) create mode 100644 Lake/Util/EquipT.lean diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index ab369f94f3..bcd1584807 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ import Lake.Build.Data import Lake.Config.Module +import Lake.Util.EquipT namespace Lake @@ -29,20 +30,21 @@ def BuildInfo.key : (self : BuildInfo) → BuildKey | package p f => ⟨p.name, none, f⟩ | target p t f => ⟨p.name, t, f⟩ -/-- A build function for a single element of the Lake build index. -/ +/-- A build function for any element of the Lake build index. -/ abbrev IndexBuildFn (m : Type → Type v) := -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports (info : BuildInfo) → m (BuildData info.key) -@[inline] def Module.recBuildFacet {m : Type → Type v} -(mod : Module) (facet : WfName) [DynamicType ModuleData facet α] -(build : (info : BuildInfo) → m (BuildData info.key)) : m α := +/-- A transformer to equip a monad with a build function for the Lake index. -/ +abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m + +@[inline] def Module.recBuildFacet (mod : Module) (facet : WfName) +[DynamicType ModuleData facet α] : IndexT m α := fun build => let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type] cast to_data <| build <| BuildInfo.module mod facet -@[inline] def Package.recBuildFacet {m : Type → Type v} -(pkg : Package) (facet : WfName) [DynamicType PackageData facet α] -(build : (info : BuildInfo) → m (BuildData info.key)) : m α := +@[inline] def Package.recBuildFacet (pkg : Package) (facet : WfName) +[DynamicType PackageData facet α] : IndexT m α := fun build => let to_data := by unfold BuildData, BuildInfo.key; simp [eq_dynamic_type] cast to_data <| build <| BuildInfo.package pkg facet diff --git a/Lake/Build/Module1.lean b/Lake/Build/Module1.lean index 2a40aa3bd0..ca43462721 100644 --- a/Lake/Build/Module1.lean +++ b/Lake/Build/Module1.lean @@ -59,11 +59,11 @@ section variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m] /-- Build the dynlibs of the imports that want precompilation. -/ -def recBuildPrecompileDynlibs (imports : Array Module) -(recurse : IndexBuildFn m) : m (Array ActiveFileTarget) := do +@[specialize] def recBuildPrecompileDynlibs (imports : Array Module) +: IndexT m (Array ActiveFileTarget) := do imports.filterMapM fun imp => do if imp.shouldPrecompile then - return some <| ← imp.recBuildFacet &`lean.dynlib recurse + return some <| ← imp.recBuildFacet &`lean.dynlib else return none @@ -72,19 +72,19 @@ Recursively build a module and its (transitive, local) imports, optionally outputting a `.c` file as well if `c` is set to `true`. -/ @[specialize] def Module.recBuildLean (mod : Module) (c : Bool) -(recurse : IndexBuildFn m) : m ActiveOpaqueTarget := do +: IndexT m ActiveOpaqueTarget := do have : MonadLift BuildM m := ⟨liftM⟩ - let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep recurse - let (imports, transImports) ← mod.recBuildFacet &`lean.imports recurse + let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep + let (imports, transImports) ← mod.recBuildFacet &`lean.imports let dynlibsTarget ← ActiveTarget.collectArray - <| ← recBuildPrecompileDynlibs transImports recurse + <| ← recBuildPrecompileDynlibs transImports let importTarget ← if c then ActiveTarget.collectOpaqueArray - <| ← imports.mapM (·.recBuildFacet &`lean.c recurse) + <| ← imports.mapM (·.recBuildFacet &`lean.c) else ActiveTarget.collectOpaqueArray - <| ← imports.mapM (·.recBuildFacet &`lean recurse) + <| ← imports.mapM (·.recBuildFacet &`lean) let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync <| ← dynlibsTarget.mixOpaqueAsync importTarget let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate @@ -103,7 +103,7 @@ Recursively parse the Lean files of a module and its imports building an `Array` product of its direct and transitive local imports. -/ @[specialize] def Module.recParseImports (mod : Module) -(recurse : IndexBuildFn m) : m (Array Module × Array Module) := do +: IndexT m (Array Module × Array Module) := do have : MonadLift BuildM m := ⟨liftM⟩ let contents ← IO.FS.readFile mod.leanFile let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString @@ -112,7 +112,7 @@ building an `Array` product of its direct and transitive local imports. let mut imports := #[] let mut transImports := ModuleSet.empty for imp in importSet do - let (_, impTransImports) ← imp.recBuildFacet &`lean.imports recurse + let (_, impTransImports) ← imp.recBuildFacet &`lean.imports for imp in impTransImports do transImports := transImports.insert imp transImports := transImports.insert imp @@ -123,11 +123,11 @@ building an `Array` product of its direct and transitive local imports. Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/ @[specialize] def Module.recBuildDynLib (mod : Module) -(recurse : IndexBuildFn m) : m ActiveFileTarget := do +: IndexT m ActiveFileTarget := do have : MonadLift BuildM m := ⟨liftM⟩ - let oTarget ← mod.recBuildFacet &`lean.o recurse - let (_, transImports) ← mod.recBuildFacet &`lean.imports recurse - let dynlibTargets ← recBuildPrecompileDynlibs transImports recurse + let oTarget ← mod.recBuildFacet &`lean.o + let (_, transImports) ← mod.recBuildFacet &`lean.imports + let dynlibTargets ← recBuildPrecompileDynlibs transImports -- TODO: Link in external libraries -- let externLibTargets ← mod.pkg.externLibTargets.mapM (·.activate) -- let linkTargets := #[oTarget] ++ sharedLibTargets ++ externLibTargets |>.map Target.active diff --git a/Lake/Build/Store.lean b/Lake/Build/Store.lean index d3bb6a874d..906be8d7de 100644 --- a/Lake/Build/Store.lean +++ b/Lake/Build/Store.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Build.Data -import Lake.Build.Topological import Lake.Util.StoreInsts /-! diff --git a/Lake/Build/Topological.lean b/Lake/Build/Topological.lean index 9ef29e150b..f51d76207e 100644 --- a/Lake/Build/Topological.lean +++ b/Lake/Build/Topological.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Util.Store +import Lake.Util.EquipT /-! # Topological / Suspending Recursive Builder @@ -26,7 +27,7 @@ abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type /-- A dependently typed recursive object builder. -/ abbrev DRecBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) := - (i : ι) → DBuildFn ι β m → m (β i) + (i : ι) → EquipT (DBuildFn ι β m) m (β i) /-- A recursive object builder. -/ abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m diff --git a/Lake/Util/EquipT.lean b/Lake/Util/EquipT.lean new file mode 100644 index 0000000000..918161b74e --- /dev/null +++ b/Lake/Util/EquipT.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +namespace Lake + +/-- +A monad transformer that equips a monad with a value. +This is a generalization of `ReaderT` where the value is not +necessarily directly readable through the monad. +-/ +def EquipT (ρ : Type u) (m : Type v → Type w) (α : Type v) := + ρ → m α + +variable {ρ : Type u} {m : Type v → Type w} + +instance {α : Type v} [Inhabited (m α)] : Inhabited (EquipT ρ m α) where + default := fun _ => default + +namespace EquipT + +@[inline] protected +def run {α : Type v} (self : EquipT ρ m α) (r : ρ) : m α := + self r + +@[inline] protected +def map [Functor m] {α β : Type v} (f : α → β) (self : EquipT ρ m α) : EquipT ρ m β := + fun fetch => Functor.map f (self fetch) + +instance [Functor m] : Functor (EquipT ρ m) where + map := EquipT.map + +@[inline] protected +def pure [Pure m] {α : Type v} (a : α) : EquipT ρ m α := + fun _ => pure a + +instance [Pure m] : Pure (EquipT ρ m) where + pure := EquipT.pure + +@[inline] protected +def compose {α₁ α₂ β : Type v} (f : m α₁ → (Unit → m α₂) → m β) (x₁ : EquipT ρ m α₁) (x₂ : Unit → EquipT ρ m α₂) : EquipT ρ m β := + fun fetch => f (x₁ fetch) (fun _ => x₂ () fetch) + +@[inline] protected +def seq [Seq m] {α β : Type v} : EquipT ρ m (α → β) → (Unit → EquipT ρ m α) → EquipT ρ m β := + EquipT.compose Seq.seq + +instance [Seq m] : Seq (EquipT ρ m) where + seq := EquipT.seq + +instance [Applicative m] : Applicative (EquipT ρ m) := {} + +@[inline] protected +def bind [Bind m] {α β : Type v} (self : EquipT ρ m α) (f : α → EquipT ρ m β) : EquipT ρ m β := + fun fetch => bind (self fetch) fun a => f a fetch + +instance [Bind m] : Bind (EquipT ρ m) where + bind := EquipT.bind + +instance [Monad m] : Monad (EquipT ρ m) := {} + +@[inline] protected +def lift {α : Type v} (t : m α) : EquipT ρ m α := + fun _ => t + +instance : MonadLift m (EquipT ρ m) where + monadLift := EquipT.lift + +@[inline] protected +def failure [Alternative m] {α : Type v} : EquipT ρ m α := + fun _ => failure + +@[inline] protected +def orElse [Alternative m] {α : Type v} : EquipT ρ m α → (Unit → EquipT ρ m α) → EquipT ρ m α := + EquipT.compose Alternative.orElse + +instance [Alternative m] : Alternative (EquipT ρ m) where + failure := EquipT.failure + orElse := EquipT.orElse + +@[inline] protected +def throw {ε : Type v} [MonadExceptOf ε m] {α : Type v} (e : ε) : EquipT ρ m α := + fun _ => throw e + +@[inline] protected +def tryCatch {ε : Type v} [MonadExceptOf ε m] {α : Type v} (self : EquipT ρ m α) (c : ε → EquipT ρ m α) : EquipT ρ m α := + fun f => tryCatchThe ε (self f) fun e => (c e) f + +instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (EquipT ρ m) where + throw := EquipT.throw + tryCatch := EquipT.tryCatch