Directories in Idris

Here’s the translation of the Go code to Idris, along with explanations in Markdown format suitable for Hugo:

Our first program demonstrates how to work with directories in Idris. Here’s the full source code:

import System.Directory
import System.File
import System.FilePath.Posix
import Data.String

-- Helper function to check for errors
checkError : Either String a -> IO a
checkError (Left err) = putStrLn err *> exitFailure
checkError (Right value) = pure value

-- Helper function to create an empty file
createEmptyFile : String -> IO ()
createEmptyFile name = do
  Right _ <- writeFile name ""
    | Left err => putStrLn $ "Error creating file: " ++ err
  pure ()

main : IO ()
main = do
  -- Create a new sub-directory in the current working directory
  Right _ <- createDir "subdir" 0o755
    | Left err => putStrLn $ "Error creating directory: " ++ err

  -- Create some files and directories
  createEmptyFile "subdir/file1"
  Right _ <- createDir "subdir/parent/child" 0o755
    | Left err => putStrLn $ "Error creating directory: " ++ err
  createEmptyFile "subdir/parent/file2"
  createEmptyFile "subdir/parent/file3"
  createEmptyFile "subdir/parent/child/file4"

  -- List directory contents
  Right entries <- listDir "subdir/parent"
    | Left err => putStrLn $ "Error listing directory: " ++ err
  putStrLn "Listing subdir/parent"
  traverse_ (\entry => do
    isDir <- doesDirExist $ "subdir/parent/" ++ entry
    putStrLn $ " " ++ entry ++ " " ++ show isDir) entries

  -- Change current working directory
  Right _ <- changeDir "subdir/parent/child"
    | Left err => putStrLn $ "Error changing directory: " ++ err

  -- List contents of current directory
  Right currentEntries <- listDir "."
    | Left err => putStrLn $ "Error listing directory: " ++ err
  putStrLn "Listing subdir/parent/child"
  traverse_ (\entry => do
    isDir <- doesDirExist entry
    putStrLn $ " " ++ entry ++ " " ++ show isDir) currentEntries

  -- Change back to the original directory
  Right _ <- changeDir "../../.."
    | Left err => putStrLn $ "Error changing directory: " ++ err

  -- Recursively visit directory
  putStrLn "Visiting subdir"
  visitDir "subdir"

  -- Clean up: remove the created directory and its contents
  Right _ <- removeDir "subdir"
    | Left err => putStrLn $ "Error removing directory: " ++ err
  pure ()

-- Helper function to recursively visit directories
visitDir : String -> IO ()
visitDir dir = do
  Right entries <- listDir dir
    | Left err => putStrLn $ "Error listing directory: " ++ err
  traverse_ (\entry -> do
    let path = dir </> entry
    isDir <- doesDirExist path
    putStrLn $ " " ++ path ++ " " ++ show isDir
    when isDir $ visitDir path) entries

This Idris program demonstrates various operations on directories:

We start by creating a new sub-directory using createDir.
We then create some empty files and nested directories using createEmptyFile and createDir.
We use listDir to list the contents of a directory and doesDirExist to check if each entry is a directory.
We demonstrate changing the current working directory with changeDir.
We implement a recursive directory traversal function visitDir that visits all subdirectories and files.
Finally, we clean up by removing the created directory and its contents with removeDir.

Note that Idris uses monadic IO operations and handles errors using the Either type. We use pattern matching to handle potential errors in each operation.

To run this program, save it as directories.idr and use the Idris compiler:

$ idris directories.idr -o directories
$ ./directories

This will compile and run the program, showing the directory operations in action.

Url Parsing in Idris

Base64 Encoding in Idris

Learn X By Example

Title here

Directories in Idris