From e2003d089833ea3a6075ecb742e23a49da491993 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Tue, 22 Oct 2024 17:02:57 +0900
Subject: [PATCH] rewrite with Monad transformer

---
 Doug/Basic.lean | 38 ++++++++++----------------------------
 1 file changed, 10 insertions(+), 28 deletions(-)

diff --git a/Doug/Basic.lean b/Doug/Basic.lean
index 4f8377b..7189115 100644
--- a/Doug/Basic.lean
+++ b/Doug/Basic.lean
@@ -4,31 +4,19 @@ structure Config where
   useASCII : Bool := false
   currentPrefix : String := ""
 
-def ConfigIO (α : Type) : Type :=
-  Config → IO α
+abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α
 
-instance : Monad ConfigIO where
-  pure x := fun _ => pure x
-  bind result next := fun cfg => do
-    let v ← result cfg
-    next v cfg
+#check read
 
 #print ConfigIO
 #check (Monad ConfigIO)
-#check Monad.mk
-
-def ConfigIO.run (action : ConfigIO α) (cfg : Config) : IO α :=
-  action cfg
+#check MonadLift
+#check MonadWithReader
+#check outParam
 
 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
-    locally (·.inDirectory)
+    let contents ← path.readDir
+    withReader (·.inDirectory)
       (doList contents.toList fun d =>
         dirTree d.path)