module Prelude.File

import Builtins
import Prelude.List
import Prelude.Maybe
import Prelude.Functor
import Prelude.Monad
import Prelude.Chars
import Prelude.Strings
import Prelude.Nat
import Prelude.Cast
import Prelude.Bool
import Prelude.Basics
import Prelude.Interfaces
import Prelude.Either
import Prelude.Show

import IO

%access public export

||| A file handle
data File : Type where
  FHandle : (p : Ptr) -> File

||| A directory handle
data Directory : Type where
  DHandle : (p : Ptr) -> Directory

-- Usage hints for erasure analysis
%used FHandle p
%used DHandle p

||| An error from a file operation
-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
-- the values correspond!

data FileError = GenericFileError Int -- errno
               | FileReadError
               | FileWriteError
               | FileNotFound
               | PermissionDenied

private
strError : Int -> String
strError err = unsafePerformIO -- yeah, yeah...
                  (foreign FFI_C "idris_showerror" (Int -> IO String) err)

getFileError : IO FileError
getFileError = do vm <- getMyVM
                  MkRaw err <- foreign FFI_C "idris_mkFileError"
                                    (Ptr -> IO (Raw FileError)) vm
                  pure err

Show FileError where
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show (GenericFileError errno) = strError errno

||| Standard input
export
stdin : File
stdin = FHandle prim__stdin

||| Standard output
export
stdout : File
stdout = FHandle prim__stdout

||| Standard output
export
stderr : File
stderr = FHandle prim__stderr

private
do_ferror : Ptr -> IO Int
do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h

export
ferror : File -> IO Bool
ferror (FHandle h) = do err <- do_ferror h
                        pure (err /= 0)

||| Call the RTS's file opening function
private
do_fopen : String -> String -> IO Ptr
do_fopen f m
   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m

||| Open a file
||| @ f the filename
||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)
export
fopen : (f : String) -> (m : String) -> IO (Either FileError File)
fopen f m = do h <- do_fopen f m
               if !(nullPtr h)
                  then Left <$> getFileError
                  else pure (Right (FHandle h))

||| Check whether a file handle is actually a null pointer
export
validFile : File -> IO Bool
validFile (FHandle h) = not <$> nullPtr h

||| Modes for opening files
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend

modeStr : Mode -> String
modeStr Read              = "rb"
modeStr WriteTruncate     = "wb"
modeStr Append            = "ab"
modeStr ReadWrite         = "rb+"
modeStr ReadWriteTruncate = "wb+"
modeStr ReadAppend        = "ab+"

||| Open a file
||| @ f the filename
||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite, ReadWriteTruncate, or ReadAppend
export
openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
openFile f m = fopen f (modeStr m)

||| Open a file using C11 extended modes.
||| @ f the filename
||| @ m the mode; either Read, WriteTruncate, Append, ReadWrite, ReadWriteTruncate, or ReadAppend
export
openFileX : (f : String) -> (m : Mode) -> IO (Either FileError File)
openFileX f m = fopen f $ modeStr m ++ "x"

private
do_fclose : Ptr -> IO ()
do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h

export
closeFile : File -> IO ()
closeFile (FHandle h) = do_fclose h

private
do_getFileSize : Ptr -> IO Int
do_getFileSize h = foreign FFI_C "fileSize" (Ptr -> IO Int) h

private
do_getFileAccessTime : Ptr -> IO Integer
do_getFileAccessTime h =
   do MkRaw i <- foreign FFI_C "fileAccessTime" (Ptr -> IO (Raw Integer)) h
      pure i

private
do_getFileModifiedTime : Ptr -> IO Integer
do_getFileModifiedTime h = 
   do vm <- getMyVM
      MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> Ptr -> IO (Raw Integer)) vm h
      pure i

private
do_getFileStatusTime : Ptr -> IO Integer
do_getFileStatusTime h = 
   do MkRaw i <- foreign FFI_C "fileStatusTime" (Ptr -> IO (Raw Integer)) h
      pure i

||| Return the size of a File
||| Returns an error if the File is not an ordinary file (e.g. a directory)
||| Also note that this currently returns an Int, which may overflow if the
||| file is very big
export
fileSize : File -> IO (Either FileError Int)
fileSize (FHandle h) 
    = do s <- do_getFileSize h
         if (s < 0)
            then Left <$> getFileError
            else pure (Right s)

export
fileModifiedTime : File -> IO (Either FileError Integer)
fileModifiedTime (FHandle h)
    = do s <- do_getFileModifiedTime h
         if (s == -1)
            then Left <$> getFileError
            else pure (Right s)

export
fileAccessTime : File -> IO (Either FileError Integer)
fileAccessTime (FHandle h)
    = do s <- do_getFileAccessTime h
         if (s < 0)
            then Left <$> getFileError
            else pure (Right s)

export
fileStatusTime : File -> IO (Either FileError Integer)
fileStatusTime (FHandle h)
    = do s <- do_getFileStatusTime h
         if (s < 0)
            then Left <$> getFileError
            else pure (Right s)

private
do_fread : Ptr -> IO' l String
do_fread h = prim_fread h

private
do_freadChars : Ptr -> Int -> IO' l String
do_freadChars h len = prim_freadChars len h

export
fgetc : File -> IO (Either FileError Char)
fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)
                       if !(ferror (FHandle h))
                          then pure (Left FileReadError)
                          else pure (Right c)

export
fflush : File -> IO ()
fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h

private
do_popen : String -> String -> IO Ptr
do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m

export
popen : String -> Mode -> IO (Either FileError File)
popen f m = do ptr <- do_popen f (modeStr m)
               if !(nullPtr ptr)
                  then do err <- getFileError
                          pure (Left err)
                  else pure (Right (FHandle ptr))

export
pclose : File -> IO ()
pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h


||| Read a line from a file
||| @h a file handle which must be open for reading
export
fGetLine : (h : File) -> IO (Either FileError String)
fGetLine (FHandle h) = do
  str <- do_fread h
  if !(ferror (FHandle h))
    then pure (Left FileReadError)
    else pure (Right str)

||| Read up to a number of characters from a file
||| @h a file handle which must be open for reading
export
fGetChars : (h : File) -> (len : Int) -> IO (Either FileError String)
fGetChars (FHandle h) len = do str <- do_freadChars h len
                               if !(ferror (FHandle h))
                                  then pure (Left FileReadError)
                                  else pure (Right str)


private
do_fwrite : Ptr -> String -> IO (Either FileError ())
do_fwrite h s = do res <- prim_fwrite h s
                   if (res /= 0)
                      then do errno <- getErrno
                              if errno == 0
                                 then pure (Left FileWriteError)
                                 else Left <$> getFileError
                      else pure (Right ())

||| Write a line to a file
||| @h a file handle which must be open for writing
||| @str the line to write to the file
export
fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
fPutStr (FHandle h) s = do_fwrite h s

export
fPutStrLn : File -> String -> IO (Either FileError ())
fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")

private
do_feof : Ptr -> IO Int
do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h

||| Check if a file handle has reached the end
export
fEOF : File -> IO Bool
fEOF (FHandle h) = do eof <- do_feof h
                      pure (eof /= 0)

private
do_fremove : String -> IO Int
do_fremove s = foreign FFI_C "fileRemove" (String -> IO Int) s

||| Remove a file
||| @s the file name
export
fRemove : (s : String) -> IO Bool
fRemove s = do res <- do_fremove s
               pure (res == 0)

export
fpoll : File -> IO Bool
fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
                       pure (p > 0)

||| Read the contents of a text 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.
||| This only works reliably with text files, since it relies on null-terminated
||| strings internally.
||| Returns an error if filepath is not a normal file.
export
readFile : (filepath : String) -> IO (Either FileError String)
readFile fn = do Right h <- openFile fn Read
                    | Left err => pure (Left err)
                 Right max <- fileSize h
                    | Left err => do closeFile h
                                     pure (Left err)
                 sb <- newStringBuffer (max + 1)
                 c <- readFile' h max sb
                 closeFile h
                 pure c
  where
    readFile' : File -> Int -> StringBuffer -> IO (Either FileError String)
    readFile' h max contents =
       do x <- fEOF h
          if not x && max > 0
                   then do Right l <- fGetChars h 1024000
                               | Left err => pure (Left err)
                           addToStringBuffer contents l
                           assert_total $
                             readFile' h (max - 1024000) contents
                   else do str <- getStringFromBuffer contents
                           pure (Right str)

||| Write a string to a file
export
writeFile : (filepath : String) -> (contents : String) ->
            IO (Either FileError ())
writeFile fn contents = do
     Right h  <- openFile fn WriteTruncate 
        | Left err => pure (Left err)
     Right () <- fPutStr h contents        
        | Left err => do closeFile h
                         pure (Left err)
     closeFile h
     pure (Right ())


export
dirOpen : (d : String) -> IO (Either FileError Directory)
dirOpen d
    = do dptr <- foreign FFI_C "idris_dirOpen" (String -> IO Ptr) d
         if !(nullPtr dptr)
            then Left <$> getFileError
            else pure (Right (DHandle dptr))

export
dirClose : Directory -> IO ()
dirClose (DHandle d) = foreign FFI_C "idris_dirClose" (Ptr -> IO ()) d

export
dirError : Directory -> IO Bool
dirError (DHandle d)
    = do err <- foreign FFI_C "idris_dirError" (Ptr -> IO Int) d
         pure (err /= 0)

export
dirEntry : Directory -> IO (Either FileError String)
dirEntry (DHandle d)
    = do fn <- foreign FFI_C "idris_nextDirEntry" (Ptr -> IO String) d
         if !(dirError (DHandle d))
            then pure (Left FileReadError)
            else pure (Right fn)

export
createDir : String -> IO (Either FileError ())
createDir d
    = do ok <- foreign FFI_C "idris_mkdir" (String -> IO Int) d
         if (ok == 0)
            then pure (Right ())
            else Left <$> getFileError

export
changeDir : String -> IO Bool
changeDir dir 
    = do ok <- foreign FFI_C "idris_chdir" (String -> IO Int) dir
         pure (ok == 0)

export
currentDir : IO String
currentDir = do
  MkRaw s <- foreign FFI_C "idris_currentDir" (IO (Raw String))
  pure s