doug/Doug/Basic.lean

def hello := "world"

structure Config where
  useASCII : Bool := false
  printAll : Bool := false
  rootPath : System.FilePath := "."
  currentPrefix : String := ""
deriving Repr

abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α

#check read

#print ConfigIO
#check (Monad ConfigIO)
#check MonadLift
#check MonadWithReader
#check outParam

def currentConfig : ConfigIO Config :=
  fun cfg => pure cfg

def usage : String :=
  "Usage: doug [--ascii]
Options:
\t--ascii\tUse ASCII characters to display the directry structure
\t-a\tShow hidden entries"

def configFromArgs (args : List String) : Option Config :=
  let parse_arg cfg arg :=
    match arg with
    | "--ascii" => some {cfg with useASCII := true}
    | "-a" => some {cfg with printAll := true}
    | path =>
      if path.startsWith "-" then
        none
      else
        some {cfg with rootPath := path}
  args.foldlM parse_arg {}

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 "│  "

/--
Modify `cfg` on entering a directory.
-/
def Config.inDirectory (cfg : Config) : Config :=
  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}

def showFileName (file : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix}{(← read).preFile} {file}"

def showDirName (dir : String) : ConfigIO Unit := do
  IO.println s!"{(← read).currentPrefix}{(← read).preDir} {dir}/"

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 ← toEntry path with
  | none => pure ()
  | some (.file name) =>
    if ((← read).printAll) || !(name.startsWith ".") then
      showFileName name
  | some (.dir name) =>
    if ((← read).printAll) || !(name.startsWith ".") then
      showDirName name
      let contents ← path.readDir
      withReader (·.inDirectory)
        (doList contents.toList fun d =>
          dirTree d.path)

def main (args : List String) : IO UInt32 := do
  match configFromArgs args with
  | some config =>
    if ← config.rootPath.pathExists then
      (dirTree (← IO.FS.realPath config.rootPath)).run config
      IO.println s!"config {repr config}"
      pure 0
    else
      IO.eprintln s!"Path doesn't exist {config.rootPath}"
      pure 1
  | none =>
    IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
    IO.eprintln usage
    pure 1