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