rewrite with custom Monad (without monad transformer)

Doug/Basic.lean

@@ -1,78 +1,103 @@
-def hello := "world"
+def hello := "world"
-
+
-structure Config where
+structure Config where
-  useASCII : Bool := false
+  useASCII : Bool := false
-  currentPrefix : String := ""
+  currentPrefix : String := ""
-
+
-def usage : String :=
+def ConfigIO (α : Type) : Type :=
-  "Usage: doug [--ascii]
+  Config → IO α
-Options:
+
-\t--ascii\tUse ASCII characters to display the directry structure"
+instance : Monad ConfigIO where
-
+  pure x := fun _ => pure x
-def configFromArgs : List String → Option Config
+  bind result next := fun cfg => do
-  | [] => some {}
+    let v ← result cfg
-  | ["--ascii"] => some {useASCII := true}
+    next v cfg
-  | _ => none
+
-
+#print ConfigIO
-inductive Entry where
+#check (Monad ConfigIO)
-  | file : String → Entry
+#check Monad.mk
-  | dir : String → Entry
+
-
+def ConfigIO.run (action : ConfigIO α) (cfg : Config) : IO α :=
-def toEntry (path : System.FilePath) : IO (Option Entry) := do
+  action cfg
-  match path.components.getLast? with
+
-  | none => pure (some (.dir ""))
+def currentConfig : ConfigIO Config :=
-  | some "." | some ".." => pure none
+  fun cfg => pure cfg
-  | some name =>
+
-    pure (some (if (← path.isDir) then .dir name else .file name))
+def locally (change : Config → Config) (action : ConfigIO α) : ConfigIO α :=
-
+  fun cfg => action (change cfg)
-def Config.preFile (cfg : Config) :=
+
-  if cfg.useASCII then "|--" else "├──"
+def runIO (action : IO α) : ConfigIO α :=
-
+  fun _ => action
-def Config.preDir (cfg : Config) :=
+
-  if cfg.useASCII then "|  " else "│  "
+def usage : String :=
-
+  "Usage: doug [--ascii]
-def Config.fileName (cfg : Config) (file : String) : String :=
+Options:
-  s!"{cfg.currentPrefix}{cfg.preFile} {file}"
+\t--ascii\tUse ASCII characters to display the directry structure"
-
+
-def Config.dirName (cfg : Config) (dir : String) : String :=
+def configFromArgs : List String → Option Config
-  s!"{cfg.currentPrefix}{cfg.preDir} {dir}/"
+  | [] => some {}
-
+  | ["--ascii"] => some {useASCII := true}
-/--
+  | _ => none
-Modify `cfg` on entering a directory.
+
--/
+inductive Entry where
-def Config.inDirectory (cfg : Config) : Config :=
+  | file : String → Entry
-  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}
+  | dir : String → Entry
-
+
-def showFileName (cfg : Config) (file : String) : IO Unit := do
+def toEntry (path : System.FilePath) : IO (Option Entry) := do
-  IO.println (cfg.fileName file)
+  match path.components.getLast? with
-
+  | none => pure (some (.dir ""))
-def showDirName (cfg : Config) (dir : String) : IO Unit := do
+  | some "." | some ".." => pure none
-  IO.println (cfg.dirName dir)
+  | some name =>
-
+    pure (some (if (← path.isDir) then .dir name else .file name))
-def doList [Applicative f] : List α → (α → f Unit) → f Unit
+
-  | [], _ => pure ()
+def Config.preFile (cfg : Config) :=
-  | x :: xs, action =>
+  if cfg.useASCII then "|--" else "├──"
-    action x *>
+
-    doList xs action
+def Config.preDir (cfg : Config) :=
-
+  if cfg.useASCII then "|  " else "│  "
-partial def dirTree (cfg : Config) (path : System.FilePath) : IO Unit := do
+
-  match ← toEntry path with
+def Config.fileName (cfg : Config) (file : String) : String :=
-  | none => pure ()
+  s!"{cfg.currentPrefix}{cfg.preFile} {file}"
-  | some (.file name) => showFileName cfg name
+
-  | some (.dir name) =>
+def Config.dirName (cfg : Config) (dir : String) : String :=
-    showDirName cfg name
+  s!"{cfg.currentPrefix}{cfg.preDir} {dir}/"
-    let contents ← path.readDir
+
-    let newConfig := cfg.inDirectory
+/--
-    doList contents.toList fun d =>
+Modify `cfg` on entering a directory.
-      dirTree newConfig d.path
+-/
-
+def Config.inDirectory (cfg : Config) : Config :=
-def main (args : List String) : IO UInt32 := do
+  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}
-  match configFromArgs args with
+
-  | some config =>
+def showFileName (file : String) : ConfigIO Unit := do
-    dirTree config (← IO.currentDir)
+  runIO (IO.println ((← currentConfig).fileName file))
-    pure 0
+
-  | none =>
+def showDirName (dir : String) : ConfigIO Unit := do
-    IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
+  runIO (IO.println ((← currentConfig).dirName dir))
-    IO.eprintln usage
+
-    pure 1
+def doList [Applicative f] : List α → (α → f Unit) → f Unit
-
+  | [], _ => pure ()
+  | x :: xs, action =>
+    action x *>
+    doList xs action
+
+partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
+  match ← runIO (toEntry path) with
+  | none => pure ()
+  | some (.file name) => showFileName name
+  | some (.dir name) =>
+    showDirName name
+    let contents ← runIO path.readDir
+    locally (·.inDirectory)
+      (doList contents.toList fun d =>
+        dirTree d.path)
+
+def main (args : List String) : IO UInt32 := do
+  match configFromArgs args with
+  | some config =>
+    (dirTree (← IO.currentDir)).run config
+    pure 0
+  | none =>
+    IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
+    IO.eprintln usage
+    pure 1
+