rewrite with Monad transformer

Doug/Basic.lean

@@ -4,31 +4,19 @@ structure Config where
   useASCII : Bool := false
   currentPrefix : String := ""
 
-def ConfigIO (α : Type) : Type :=
+abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α
-  Config → IO α
 
-instance : Monad ConfigIO where
+#check read
-  pure x := fun _ => pure x
-  bind result next := fun cfg => do
-    let v ← result cfg
-    next v cfg
 
 #print ConfigIO
 #check (Monad ConfigIO)
-#check Monad.mk
+#check MonadLift
-
+#check MonadWithReader
-def ConfigIO.run (action : ConfigIO α) (cfg : Config) : IO α :=
+#check outParam
-  action cfg
 
 def currentConfig : ConfigIO Config :=
   fun cfg => pure cfg
 
-def locally (change : Config → Config) (action : ConfigIO α) : ConfigIO α :=
-  fun cfg => action (change cfg)
-
-def runIO (action : IO α) : ConfigIO α :=
-  fun _ => action
-
 def usage : String :=
   "Usage: doug [--ascii]
 Options:
@@ -56,12 +44,6 @@ def Config.preFile (cfg : Config) :=
 def Config.preDir (cfg : Config) :=
   if cfg.useASCII then "|  " else "│  "
 
-def Config.fileName (cfg : Config) (file : String) : String :=
-  s!"{cfg.currentPrefix}{cfg.preFile} {file}"
-
-def Config.dirName (cfg : Config) (dir : String) : String :=
-  s!"{cfg.currentPrefix}{cfg.preDir} {dir}/"
-
 /--
 Modify `cfg` on entering a directory.
 -/
@@ -69,10 +51,10 @@ def Config.inDirectory (cfg : Config) : Config :=
   {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}
 
 def showFileName (file : String) : ConfigIO Unit := do
-  runIO (IO.println ((← currentConfig).fileName file))
+  IO.println s!"{(← read).currentPrefix}{(← read).preFile} {file}"
 
 def showDirName (dir : String) : ConfigIO Unit := do
-  runIO (IO.println ((← currentConfig).dirName dir))
+  IO.println s!"{(← read).currentPrefix}{(← read).preDir} {dir}/"
 
 def doList [Applicative f] : List α → (α → f Unit) → f Unit
   | [], _ => pure ()
@@ -81,13 +63,13 @@ def doList [Applicative f] : List α → (α → f Unit) → f Unit
     doList xs action
 
 partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
-  match ← runIO (toEntry path) with
+  match ← toEntry path with
   | none => pure ()
   | some (.file name) => showFileName name
   | some (.dir name) =>
     showDirName name
-    let contents ← runIO path.readDir
+    let contents ← path.readDir
-    locally (·.inDirectory)
+    withReader (·.inDirectory)
       (doList contents.toList fun d =>
         dirTree d.path)