File.agda

module IO.File where

open import Base
open import IO

{-# IMPORT System.IO #-}

FilePath = String

data IOMode : Set where
  readMode      : IOMode
  writeMode     : IOMode
  appendMode    : IOMode
  readWriteMode : IOMode

{-# COMPILED_DATA IOMode ReadMode WriteMode AppendMode ReadWriteMode #-}

canRead : IOMode -> Bool
canRead readMode      = true
canRead writeMode     = false
canRead appendMode    = false
canRead readWriteMode = true

canWrite : IOMode -> Bool
canWrite readMode      = false
canWrite writeMode     = true
canWrite appendMode    = true
canWrite readWriteMode = true

CanRead : IOMode -> Set
CanRead m = IsTrue (canRead m)

CanWrite : IOMode -> Set
CanWrite m = IsTrue (canWrite m)

postulate
  Handle : Set

private
 postulate
  hs-openFile : FilePath -> IOMode -> IO Handle
  hs-hClose   : Handle -> IO Unit

  hs-hGetChar : Handle -> IO Char
  hs-hGetLine : Handle -> IO String
  hs-hGetContents : Handle -> IO String

  hs-hPutStr  : Handle -> String -> IO Unit

{-# COMPILED hs-openFile     openFile #-}
{-# COMPILED hs-hClose       hClose #-}
{-# COMPILED hs-hGetChar     hGetChar #-}
{-# COMPILED hs-hGetLine     hGetLine #-}
{-# COMPILED hs-hGetContents hGetContents #-}
{-# COMPILED hs-hPutStr      hPutStr #-}

Handles = List (Handle × IOMode)

abstract
 -- The FileIO monad. Records the list of open handles before and after
 -- a computation. The open handles after the computation may depend on
 -- the computed value.
 data FileIO (A : Set)(hs₁ : Handles)(hs₂ : A -> Handles) : Set where
   fileIO : IO A -> FileIO A hs₁ hs₂

private
 abstract
  unFileIO : forall {A hs f} -> FileIO A hs f -> IO A
  unFileIO (fileIO io) = io

FileIO₋ : Set -> Handles -> Handles -> Set
FileIO₋ A hs₁ hs₂ = FileIO A hs₁ (\_ -> hs₂)

abstract
  openFile : {hs : Handles} -> FilePath -> (m : IOMode) ->
             FileIO Handle hs (\h -> (h , m) :: hs)
  openFile file mode = fileIO (hs-openFile file mode)

infix 30 _∈_
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

delete : {A : Set}{x : A}(xs : List A) -> x ∈ xs -> List A
delete [] ()
delete (x :: xs)  hd    = xs
delete (x :: xs) (tl p) = x :: delete xs p

abstract
  hClose : {hs : Handles}{m : IOMode}(h : Handle)(p : (h , m) ∈ hs) ->
           FileIO₋ Unit hs (delete hs p)
  hClose h _ = fileIO (hs-hClose h)

  hGetLine : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
             (p : (h , m) ∈ hs) -> FileIO₋ String hs hs
  hGetLine h _ = fileIO (hs-hGetLine h)

  hGetContents : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
             (p : (h , m) ∈ hs) -> FileIO₋ String hs (delete hs p)
  hGetContents h _ = fileIO (hs-hGetContents h)

abstract
  -- You can only run file computations that don't leave any open
  -- handles.
  runFileIO : {A : Set} -> FileIO₋ A [] [] -> IO A
  runFileIO (fileIO m) = m

abstract
  _>>=_ : forall {A B hs f g} ->
          FileIO A hs f -> ((x : A) -> FileIO B (f x) g) -> FileIO B hs g
  fileIO m >>= k = fileIO (bindIO m \x -> unFileIO (k x))

  return : forall {A hs} -> A -> FileIO₋ A hs hs
  return x = fileIO (returnIO x)