main issue in Functional Programming in Lean, 6.1.3

Stream: new members

[Garrison Venn]

In section 6.1.3 the use of ReaderT was used to modify the code referenced in 6.1.2. Because no main was provided, the implication was to use the main in 6.1.2. However when comparing the two outputs one gets the following in a test directory.

The section 6.1.2 version gives:

├── gtest/
│   ├── adding
│   ├── adding.out
│   ├── inner/
│   │   ├── one
│   │   ├── two
│   ├── origAdding
│   ├── using
│   ├── using.out

The section 6.1.3 version gives:

gtest/
│    adding
│    adding.out
│    inner/
│   │    one
│   │    two
│    origAdding
│    using
│    using.out

To to fix this, I hacked configFromArgs to set the default Config.currentPrefix to be Config.preFile.

From:

def configFromArgs : List String → Option Config
  | [] => some {} -- both fields default
  | ["--ascii"] => some {useASCII := true}
  | _ => none

To:

def Config.prefixFixed (cfg : Config) :=
  {cfg with currentPrefix :=
    if cfg.currentPrefix.length == 0 then
      cfg.preFile
    else
      cfg.currentPrefix}

def configFromArgs : List String → Option Config
  | [] => some (({} : Config).prefixFixed) -- both fields default
  | ["--ascii"] => some ({useASCII := true} : Config).prefixFixed
  | _ => none

I may of course be missing something. However if such a similar change is necessary, I thought the tutorial should make both sections 6.1.2 and 6.1.3 have the same output. Sorry for the noise if this is incorrect. Also the main implementation, as used in the section 6.1.3 version, is using the ReaderT.run function because of the type change of dirTree in 6.1.3, but ReaderT.run is not discussed though is the same as 6.1.2's ConfigIO.run.

My full hacked code of 6.1.3 follows:

structure Config where
  useASCII : Bool := false
  currentPrefix : String := ""
deriving Repr

instance : ToString Config where
  toString c := s!"\{useASCII := {c.useASCII}"
                ++ s!", currentPrefix := {c.currentPrefix}}"

def Config.preFile (cfg : Config) :=
  if cfg.useASCII then "|--" else "├──"

def Config.preDir (cfg : Config) :=
  if cfg.useASCII then "|  " else "│  "

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

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

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

def Config.inDirectory (cfg : Config) : Config :=
  {cfg with currentPrefix := cfg.preDir ++ " " ++ cfg.currentPrefix}

def doList [Applicative f] : List α → (α → f Unit) → f Unit
  | [], _ => pure ()
  | x :: xs, action =>
    action x *>
    doList XS action

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 dirLT (e1 : IO.FS.DirEntry) (e2 : IO.FS.DirEntry) : Bool :=
  e1.fileName < e2.fileName

partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
  match ← toEntry path with
    | none => pure ()
    | some (.file name) => showFileName name
    | some (.dir name) =>
      showDirName name
      let contents ← path.readDir
      withReader (·.inDirectory)
        (doList (contents.qsort dirLT).toList fun d =>
          dirTree d.path)

def usage : String :=
  "Usage: doug [--ascii]
Options:
\t--ascii\tUse ASCII characters to display the directory structure"

--
-- Hacked configFromArgs
--

def Config.prefixFixed (cfg : Config) :=
  {cfg with currentPrefix :=
    if cfg.currentPrefix.length == 0 then
      cfg.preFile
    else
      cfg.currentPrefix}

def configFromArgs : List String → Option Config
  | [] => some (({} : Config).prefixFixed) -- both fields default
  | ["--ascii"] => some ({useASCII := true} : Config).prefixFixed
  | _ => none

--
-- Referenced main from 6.1.2
--

def main (args : List String) : IO UInt32 := do
    match configFromArgs args with
    | some config =>
      --dbg_trace config
      -- This is using ReaderT.run vs the 6.1.2 version of ConfigIO.run
      (dirTree (← IO.currentDir)).run config
      pure 0
    | none =>
      IO.eprintln s!"Didn't understand argument(s) {" ".intercalate args}\n"
      IO.eprintln usage
      pure 1

[Garrison Venn]

@David Thrane Christiansen I know you don't have a lot of time, but would you be willing to look at this? I know this is a bit more involved so is probably something I got incorrect.