From 3124f2bf78efc7507e9246d6e8669c3a4183b486 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Mon, 21 Oct 2024 12:37:11 +0900
Subject: [PATCH] before creating custom monad & lake script to run main

---
 Doug/Basic.lean | 76 +++++++++++++++++++++++++++++++++++++++++++++++++
 Main.lean       |  4 +--
 lakefile.lean   | 16 +++++++++--
 3 files changed, 91 insertions(+), 5 deletions(-)

diff --git a/Doug/Basic.lean b/Doug/Basic.lean
index 38721e1..930262a 100644
--- a/Doug/Basic.lean
+++ b/Doug/Basic.lean
@@ -1,2 +1,78 @@
 def hello := "world"
 
+structure Config where
+  useASCII : Bool := false
+  currentPrefix : String := ""
+
+def usage : String :=
+  "Usage: doug [--ascii]
+Options:
+\t--ascii\tUse ASCII characters to display the directry structure"
+
+def configFromArgs : List String → Option Config
+  | [] => some {}
+  | ["--ascii"] => some {useASCII := true}
+  | _ => none
+
+inductive Entry where
+  | file : String → Entry
+  | dir : String → Entry
+
+def toEntry (path : System.FilePath) : IO (Option Entry) := do
+  match path.components.getLast? with
+  | none => pure (some (.dir ""))
+  | some "." | some ".." => pure none
+  | some name =>
+    pure (some (if (← path.isDir) then .dir name else .file name))
+
+def Config.preFile (cfg : Config) :=
+  if cfg.useASCII then "|--" else "├──"
+
+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.
+-/
+def Config.inDirectory (cfg : Config) : Config :=
+  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}
+
+def showFileName (cfg : Config) (file : String) : IO Unit := do
+  IO.println (cfg.fileName file)
+
+def showDirName (cfg : Config) (dir : String) : IO Unit := do
+  IO.println (cfg.dirName dir)
+
+def doList [Applicative f] : List α → (α → f Unit) → f Unit
+  | [], _ => pure ()
+  | x :: xs, action =>
+    action x *>
+    doList xs action
+
+partial def dirTree (cfg : Config) (path : System.FilePath) : IO Unit := do
+  match ← toEntry path with
+  | none => pure ()
+  | some (.file name) => showFileName cfg name
+  | some (.dir name) =>
+    showDirName cfg name
+    let contents ← path.readDir
+    let newConfig := cfg.inDirectory
+    doList contents.toList fun d =>
+      dirTree newConfig d.path
+
+def main (args : List String) : IO UInt32 := do
+  match configFromArgs args with
+  | some config =>
+    dirTree config (← IO.currentDir)
+    pure 0
+  | none =>
+    IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
+    IO.eprintln usage
+    pure 1
+
diff --git a/Main.lean b/Main.lean
index 054c7b5..c094578 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,4 @@
 import Doug
 
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+-- def main : IO Unit :=
+--   IO.println s!"Hello, {hello}!"
diff --git a/lakefile.lean b/lakefile.lean
index 48fdeae..8289cfc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "v4.12.0"
+require "leanprover" / "doc-gen4"
 
 package "doug" where
   version := v!"0.1.0"
@@ -18,5 +18,15 @@ lean_exe "doug" where
 Doug
 -/
 script test (args) do
-  IO.println args
-  pure 0
+  let exe := (← doug.get).file
+  IO.println s!"exe: {exe}"
+  IO.println s!"args: {args}"
+  let proc ← IO.Process.spawn
+    ⟨{stdin := .inherit, stdout := .piped, stderr := .piped},
+      exe.toString, args.toArray, none, #[], false ⟩
+  IO.println s!"{← proc.tryWait}"
+  IO.print (← proc.stdout.readToEnd)
+  IO.eprintln (← IO.FS.Handle.readToEnd proc.stderr)
+  let ret ← proc.wait
+  IO.println s!"returned: {ret}"
+  pure ret