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