File.idr

||| Effectful file operations.
module Effect.File

import Effects
import Control.IOExcept

%access public export

-- -------------------------------------------------------------- [ Predicates ]

||| A record of the file modes that can read from a file.
data ValidModeRead : Mode -> Type where
  VMRRead   : ValidModeRead Read
  VMRReadW  : ValidModeRead ReadWrite
  VMRReadWT : ValidModeRead ReadWriteTruncate
  VMRReadA  : ValidModeRead ReadAppend

||| A record of the file modes that can write from a file.
data ValidModeWrite : Mode -> Type where
  VMWWrite  : ValidModeWrite WriteTruncate
  VMWAppend : ValidModeWrite Append
  VMWReadW  : ValidModeWrite ReadWrite
  VMWReadWT : ValidModeWrite ReadWriteTruncate

-- -------------------------------------------------- [ Custom Error Reporting ]

namespace FileResult

  ||| A type to describe the return type of file operations.
  data ResultDesc = SUCCESS | RESULT

  ||| A custom return type for file operations that is dependent on
  ||| the type of file operation.
  |||
  ||| @desc Parameterises the constructors to describe if the function
  |||       returns a value or not.
  ||| @ty   The return type for a file operation that returns a value.
  |||
  data FileOpReturnTy : (desc : ResultDesc)
                     -> (ty : Type)
                     -> Type where

    ||| The operation completed successfully and doesn't return a
    ||| result.
    Success : FileOpReturnTy SUCCESS ty

    ||| The operation returns a result of type `ty`.
    |||
    ||| @ty The value returned.
    Result : ty -> FileOpReturnTy RESULT ty

    ||| The operation failed and the RTS produced the given error.
    |||
    ||| @err The reported error code.
    FError : (err : FileError) -> FileOpReturnTy desc ty

  ||| Type alias to describe a file operatons that returns a result.
  FileOpResult : Type -> Type
  FileOpResult ty = FileOpReturnTy RESULT ty

  ||| Type alias to describe file oeprations that indicate success.
  FileOpSuccess : Type
  FileOpSuccess = FileOpReturnTy SUCCESS ()

-- ------------------------------------------------------------ [ The Resource ]

||| The file handle associated with the effect.
|||
||| @m The `Mode` that the handle was generated under.
data FileHandle : (m : Mode) -> Type where
    FH : File -> FileHandle m

-- ---------------------------------------------- [ Resource Type Construction ]

||| Calculates the type for the resource being computed over.  `Unit`
||| to describe pre-and-post file handle acquisition, and `FileHandle
||| m` when a file handle has been acquired.
|||
||| @m The mode the file handle was generated under.
||| @ty The functions return type.
calcResourceTy : (m  : Mode)
              -> (ty : FileOpReturnTy fOpTy retTy)
              -> Type
calcResourceTy _ (FError e) = ()
calcResourceTy m _          = FileHandle m

-- ------------------------------------------------------- [ Effect Definition ]

||| An effect to describe operations on a file.
data FileE : Effect where

  -- Open/Close

  Open : (fname : String)
      -> (m : Mode)
      -> sig FileE
             (FileOpSuccess)
             ()
             (\res => calcResourceTy m res)

  OpenX : (fname : String)
       -> (m : Mode)
       -> sig FileE
              (FileOpSuccess)
              ()
              (\res => calcResourceTy m res)

  Close : sig FileE () (FileHandle m) ()

  -- Read

  FGetC : {auto prf : ValidModeRead m}
       -> sig FileE
              (FileOpResult Char)
              (FileHandle m)
              (FileHandle m)

  FGetLine : {auto prf : ValidModeRead m}
          -> sig FileE
                 (FileOpResult String)
                 (FileHandle m)
                 (FileHandle m)

  FReadFile : (fname : String)
           -> sig FileE
                  (FileOpResult String)
                  ()
                  ()
  -- Write
  FPutStr : (str : String)
         -> {auto prf : ValidModeWrite m}
         -> sig FileE
                (FileOpSuccess)
                (FileHandle m)
                (FileHandle m)

  FPutStrLn : (str : String)
           -> {auto prf : ValidModeWrite m}
           -> sig FileE
                  (FileOpSuccess)
                  (FileHandle m)
                  (FileHandle m)

  FWriteFile : (fname    : String)
            -> (contents : String)
            -> sig FileE
                   (FileOpSuccess)
                   ()

  -- Flush
  FFlush : sig FileE
               ()
               (FileHandle m)
               (FileHandle m)

  -- Query
  FEOF : {auto prf : ValidModeRead m}
      -> sig FileE
             Bool
             (FileHandle m)

-- ---------------------------------------------------------------------- [ IO ]

Handler FileE IO where

  -- Open Close
  handle () (Open fname m) k = do
      res <- openFile fname m
      case res of
        Left err => k (FError err) ()
        Right fh => k Success      (FH fh)

  handle () (OpenX fname m) k = do
      res <- openFileX fname m
      case res of
        Left err => k (FError err) ()
        Right fh => k Success      (FH fh)

  handle (FH h) Close k = do
      closeFile h
      k () ()

  -- Read
  handle (FH h) FGetC k = do
      res <- fgetc h
      case res of
        Left err => k (FError err) (FH h)
        Right  c => k (Result c)   (FH h)

  handle (FH h) FGetLine k = do
      res <- fGetLine h
      case res of
        Left err => k (FError err) (FH h)
        Right ln => k (Result ln)  (FH h)

  handle () (FReadFile fname) k = do
      res <- readFile fname
      case res of
        Left err  => k (FError err) ()
        Right str => k (Result str) ()

  -- Write
  handle (FH fh) (FPutStr str) k = do
      res <- fPutStr fh str
      case res of
        Left err => k (FError err) (FH fh)
        Right () => k Success      (FH fh)

  handle (FH fh) (FPutStrLn str) k = do
      res <- fPutStr fh str
      case res of
        Left err => k (FError err) (FH fh)
        Right () => k Success      (FH fh)

  handle () (FWriteFile fname str) k = do
      res <- writeFile fname str
      case res of
        Left err => k (FError err) ()
        Right () => k Success      ()

  -- Flush
  handle (FH fh) FFlush k = do
      fflush fh
      k () (FH fh)

  -- Query
  handle (FH fh) FEOF k = do
      res <- fEOF fh
      k res (FH fh)

-- ---------------------------------------------------------------- [ IOExcept ]

Handler FileE (IOExcept a) where

  -- Open Close
  handle () (Open fname m) k = do
      res <- ioe_lift $ openFile fname m
      case res of
        Left err => k (FError err) ()
        Right fh => k Success      (FH fh)

  handle () (OpenX fname m) k = do
      res <- ioe_lift $ openFileX fname m
      case res of
        Left err => k (FError err) ()
        Right fh => k Success      (FH fh)

  handle (FH h) Close k = do
      ioe_lift $ closeFile h
      k () ()

  -- Read
  handle (FH h) FGetC k = do
      res <- ioe_lift $ fgetc h
      case res of
        Left err => k (FError err) (FH h)
        Right  c => k (Result c)   (FH h)

  handle (FH h) FGetLine k = do
      res <- ioe_lift $ fGetLine h
      case res of
        Left err => k (FError err) (FH h)
        Right ln => k (Result ln)  (FH h)

  handle () (FReadFile fname) k = do
      res <- ioe_lift $ readFile fname
      case res of
        Left err  => k (FError err) ()
        Right str => k (Result str) ()

  -- Write
  handle (FH fh) (FPutStr str) k = do
      res <- ioe_lift $ fPutStr fh str
      case res of
        Left err => k (FError err) (FH fh)
        Right () => k Success      (FH fh)

  handle (FH fh) (FPutStrLn str) k = do
      res <- ioe_lift $ fPutStr fh str
      case res of
        Left err => k (FError err) (FH fh)
        Right () => k Success      (FH fh)

  handle () (FWriteFile fname str) k = do
      res <- ioe_lift $ writeFile fname str
      case res of
        Left err => k (FError err) ()
        Right () => k Success      ()

  -- Flush
  handle (FH fh) FFlush k = do
      ioe_lift $ fflush fh
      k () (FH fh)


  -- Query
  handle (FH fh) FEOF k = do
      res <- ioe_lift $ fEOF fh
      k res (FH fh)

-- ------------------------------------------------------ [ Effect and Helpers ]

||| Effectful operations for interacting with files.
|||
||| The `FILE` effect is parameterised by a file handle once a handle has been acquired, and Unit (`()`) if the file handle is expected to be released once the function has returned.
|||
FILE : (ty : Type) -> EFFECT
FILE t = MkEff t FileE

||| A file has been opened for reading.
R : Type
R = FileHandle Read

||| A file has been opened for writing.
W : Type
W = FileHandle WriteTruncate

||| A file can only be appended to.
A : Type
A = FileHandle Append

||| A file can be read and written to.
RW : Type
RW = FileHandle ReadWrite

||| A file opened for reading and writing and has been truncated to
||| zero if it previously existed.
RWPlus : Type
RWPlus = FileHandle ReadWriteTruncate

||| A file will read from the beginning and write at the end.
APlus : Type
APlus = FileHandle ReadAppend

-- --------------------------------------------------------------------- [ API ]

-- -------------------------------------------------------- [ Open/Close/Query ]

||| Open a file.
|||
||| @ fname the filename.
||| @ m     the mode; either Read, WriteTruncate, Append, ReadWrite,
|||         ReadWriteTruncate, or ReadAppend
|||
open : (fname : String)
    -> (m : Mode)
    -> Eff (FileOpSuccess)
           [FILE ()]
           (\res => [FILE (calcResourceTy m res)])
open f m = call $ Open f m

||| Open a file using C11 extended modes.
|||
||| @ fname the filename
||| @ m     the mode; either Read, WriteTruncate, Append, ReadWrite,
|||         ReadWriteTruncate, or ReadAppend
openX : (fname : String)
     -> (m : Mode)
     -> Eff (FileOpSuccess)
            [FILE ()]
            (\res => [FILE (calcResourceTy m res)])
openX f m = call $ OpenX f m

||| Close a file.
close : Eff () [FILE (FileHandle m)] [FILE ()]
close = call (Close)

||| Have we reached the end of the file.
eof : {auto prf : ValidModeRead m}
    -> Eff Bool [FILE (FileHandle m)]
eof = call FEOF

flush : Eff () [FILE (FileHandle m)]
flush = call FFlush

-- -------------------------------------------------------------------- [ Read ]

||| Read a `Char`.
readChar : {auto prf : ValidModeRead m}
      -> Eff (FileOpResult Char)
             [FILE (FileHandle m)]
readChar = call FGetC

||| Read a complete line.
readLine : {auto prf : ValidModeRead m}
        -> Eff (FileOpResult String)
               [FILE (FileHandle m)]
readLine = call FGetLine

-- ------------------------------------------------------------------- [ Write ]

||| Write a string to the file.
writeString : (str : String)
           -> {auto prf : ValidModeWrite m}
           -> Eff (FileOpSuccess)
                  [FILE (FileHandle m)]
writeString str = call $ FPutStr str

||| Write a complete line to the file.
writeLine : (str : String)
         -> {auto prf : ValidModeWrite m}
         -> Eff (FileOpSuccess)
                [FILE (FileHandle m)]
writeLine str = call $ FPutStrLn str

-- -------------------------------------------------------------- [ Whole File ]

||| Read the contents of a file into a string.
|||
||| This checks the size of
||| the file before beginning to read, and only reads that many bytes,
||| to ensure that it remains a total function if the file is appended
||| to while being read.
|||
||| Returns an error if fname is not a normal file.
readFile : (fname : String)
        -> Eff (FileOpResult String)
               [FILE ()]
readFile fn = call $ FReadFile fn

||| Create a file and write contents to the file.
writeFile : (fname    : String)
         -> (contents : String)
         -> Eff (FileOpSuccess)
                [FILE ()]
writeFile fn str = call $ FWriteFile fn str

-- --------------------------------------------------------------------- [ EOF ]