108 lines
2.8 KiB
Text
108 lines
2.8 KiB
Text
/-
|
||
Copyright (c) 2021 Mac Malone. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Mac Malone
|
||
-/
|
||
import Lake.Task
|
||
|
||
open System
|
||
namespace Lake
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # Build Monad Definition
|
||
--------------------------------------------------------------------------------
|
||
|
||
-- Involves trickery patterned after `MacroM`
|
||
-- to allow `BuildMethods` to refer to `BuildM`
|
||
|
||
constant BuildMethodsRefPointed : PointedType.{0}
|
||
def BuildMethodsRef : Type := BuildMethodsRefPointed.type
|
||
|
||
structure BuildContext where
|
||
methodsRef : BuildMethodsRef
|
||
|
||
abbrev BuildM := ReaderT BuildContext IO
|
||
|
||
structure BuildMethods where
|
||
logInfo : String → BuildM PUnit
|
||
logError : String → BuildM PUnit
|
||
deriving Inhabited
|
||
|
||
namespace BuildMethodsRef
|
||
|
||
unsafe def mkImp (methods : BuildMethods) : BuildMethodsRef :=
|
||
unsafeCast methods
|
||
|
||
@[implementedBy mkImp]
|
||
constant mk (methods : BuildMethods) : BuildMethodsRef :=
|
||
BuildMethodsRefPointed.val
|
||
|
||
instance : Coe BuildMethods BuildMethodsRef := ⟨mk⟩
|
||
instance : Inhabited BuildMethodsRef := ⟨mk arbitrary⟩
|
||
|
||
unsafe def getImp (self : BuildMethodsRef) : BuildMethods :=
|
||
unsafeCast self
|
||
|
||
@[implementedBy getImp]
|
||
constant get (self : BuildMethodsRef) : BuildMethods
|
||
|
||
end BuildMethodsRef
|
||
|
||
--------------------------------------------------------------------------------
|
||
-- # Build Monad Utilities
|
||
--------------------------------------------------------------------------------
|
||
|
||
-- Ideally, this instance would be in the Lean core
|
||
instance [Pure m] : MonadLiftT Id m := ⟨pure⟩
|
||
|
||
namespace BuildContext
|
||
|
||
deriving instance Inhabited for BuildContext
|
||
|
||
def io : BuildContext where
|
||
methodsRef := BuildMethodsRef.mk {
|
||
logInfo := fun msg => IO.println msg
|
||
logError := fun msg => IO.eprintln msg
|
||
}
|
||
|
||
def methods (self : BuildContext) : BuildMethods :=
|
||
self.methodsRef.get
|
||
|
||
end BuildContext
|
||
|
||
namespace BuildM
|
||
|
||
def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
|
||
self ctx
|
||
|
||
def runIO (self : BuildM α) : IO α :=
|
||
self BuildContext.io
|
||
|
||
def getMethods : BuildM BuildMethods :=
|
||
read >>= (·.methods)
|
||
|
||
def logInfo (msg : String) : BuildM PUnit := do
|
||
(← getMethods).logInfo msg
|
||
|
||
def logError (msg : String) : BuildM PUnit := do
|
||
(← getMethods).logError msg
|
||
|
||
end BuildM
|
||
|
||
def runBuild (x : BuildM α) : IO PUnit :=
|
||
BuildM.runIO try discard x catch _ =>
|
||
-- actual error has already been logged earlier
|
||
BuildM.logError "Build failed."
|
||
|
||
def failOnImportCycle : Except (List Lean.Name) α → BuildM α
|
||
| Except.ok a => a
|
||
| Except.error cycle => do
|
||
let cycle := cycle.map (s!" {·}")
|
||
let msg := s!"import cycle detected:\n{"\n".intercalate cycle}"
|
||
BuildM.logError msg
|
||
throw <| IO.userError msg
|
||
|
||
abbrev BuildTask := IOTask
|
||
|
||
instance : HAndThen (BuildTask α) (BuildM β) (BuildM (BuildTask β)) :=
|
||
⟨seqRightAsync⟩
|