<commit_before>-- -------------------------------------------------------- [ Effectful FileIO ]
module Effect.File

import Effects
import Control.IOExcept


||| A Dependent type to describe File Handles. File handles are
||| parameterised with the current state of the file: Closed; Open for
||| reading; and Open for writing.
||| 
||| @ m The file mode. 
data OpenFile : (m : Mode) -> Type where
     FH : File -> OpenFile m

openOK : Mode -> Bool -> Type
openOK m True = OpenFile m
openOK m False = ()

-- ------------------------------------------------------------ [ The Protocol ]

||| Here the protocol for resource access is defined as an effect.
||| The state transitions diagram for the protocol is as follows:
||| 
|||     digraph G {
||| 
|||       empty; read; write; // States
||| 
|||       empty -> read [label="Open R"];
|||       read -> empty [label="Close"];
|||       read -> read [label="ReadLine"];
|||       read -> read [label="EOF"];
|||           
|||       empty -> write [label="Open W"];
|||       write -> empty [label="Close"];
|||       write -> write [label="WriteLine"];
||| 
|||     }
data FileIO : Effect where
  ||| Open a file with the specified mode.
  ||| 
  ||| Opening a file successful moves the state from 'empty' to the
  ||| specified mode. If not successful the state is still 'empty'.
  ||| 
  ||| @ fname The file name to be opened.
  ||| @ m The file mode.
  Open : (fname: String)
         -> (m : Mode)
         -> {() ==> {res} if res
                             then OpenFile m
                             else ()} FileIO Bool

  ||| Close a file.
  ||| 
  ||| Closing a file moves the state from Open to closed.
  Close : {OpenFile m ==> ()} FileIO () 

  ||| Read a line from the file.
  ||| 
  ||| Only files that are open for reading can be read.
  ReadLine : {OpenFile Read}  FileIO String 
  
  ||| Write a string to a file.
  ||| 
  ||| Only file that are open for writing can be written to.
  WriteString : String -> {OpenFile Write} FileIO ()

  ||| End of file?
  ||| 
  ||| Only files open for reading can be tested for EOF
  EOF : {OpenFile Read}  FileIO Bool

-- ------------------------------------------------------------ [ The Handlers ]

--- An implementation of the resource access protocol for the IO Context.
instance Handler FileIO IO where
    handle () (Open fname m) k = do h <- openFile fname m
                                    valid <- validFile h
                                    if valid then k True (FH h) 
                                             else k False ()
    handle (FH h) Close      k = do closeFile h
                                    k () ()
    handle (FH h) ReadLine        k = do str <- fread h
                                         k str (FH h)
    handle (FH h) (WriteString str) k = do fwrite h str
                                           k () (FH h)
    handle (FH h) EOF             k = do e <- feof h
                                         k e (FH h)

-- -------------------------------------------------------------- [ The Effect ]
FILE_IO : Type -> EFFECT
FILE_IO t = MkEff t FileIO

-- ------------------------------------------------------------ [ The Bindings ]
--
-- Bind the IO context handlers to functions. These functions will run
-- in the IO context.<commit_msg>added IOExcept handler to FileIO effect<commit_after>-- -------------------------------------------------------- [ Effectful FileIO ]
module Effect.File

import Effects
import Control.IOExcept


||| A Dependent type to describe File Handles. File handles are
||| parameterised with the current state of the file: Closed; Open for
||| reading; and Open for writing.
||| 
||| @ m The file mode. 
data OpenFile : (m : Mode) -> Type where
     FH : File -> OpenFile m

openOK : Mode -> Bool -> Type
openOK m True = OpenFile m
openOK m False = ()

-- ------------------------------------------------------------ [ The Protocol ]

||| Here the protocol for resource access is defined as an effect.
||| The state transitions diagram for the protocol is as follows:
||| 
|||     digraph G {
||| 
|||       empty; read; write; // States
||| 
|||       empty -> read [label="Open R"];
|||       read -> empty [label="Close"];
|||       read -> read [label="ReadLine"];
|||       read -> read [label="EOF"];
|||           
|||       empty -> write [label="Open W"];
|||       write -> empty [label="Close"];
|||       write -> write [label="WriteLine"];
||| 
|||     }
data FileIO : Effect where
  ||| Open a file with the specified mode.
  ||| 
  ||| Opening a file successful moves the state from 'empty' to the
  ||| specified mode. If not successful the state is still 'empty'.
  ||| 
  ||| @ fname The file name to be opened.
  ||| @ m The file mode.
  Open : (fname: String)
         -> (m : Mode)
         -> {() ==> {res} if res
                             then OpenFile m
                             else ()} FileIO Bool

  ||| Close a file.
  ||| 
  ||| Closing a file moves the state from Open to closed.
  Close : {OpenFile m ==> ()} FileIO () 

  ||| Read a line from the file.
  ||| 
  ||| Only files that are open for reading can be read.
  ReadLine : {OpenFile Read}  FileIO String 
  
  ||| Write a string to a file.
  ||| 
  ||| Only file that are open for writing can be written to.
  WriteString : String -> {OpenFile Write} FileIO ()

  ||| End of file?
  ||| 
  ||| Only files open for reading can be tested for EOF
  EOF : {OpenFile Read}  FileIO Bool

-- ------------------------------------------------------------ [ The Handlers ]

--- An implementation of the resource access protocol for the IO Context.
instance Handler FileIO IO where
    handle () (Open fname m) k = do h <- openFile fname m
                                    valid <- validFile h
                                    if valid then k True (FH h) 
                                             else k False ()
    handle (FH h) Close      k = do closeFile h
                                    k () ()
    handle (FH h) ReadLine        k = do str <- fread h
                                         k str (FH h)
    handle (FH h) (WriteString str) k = do fwrite h str
                                           k () (FH h)
    handle (FH h) EOF             k = do e <- feof h
                                         k e (FH h)

instance Handler FileIO (IOExcept a) where
    handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m
                                    valid <- ioe_lift $ validFile h
                                    if valid then k True (FH h)
                                             else k False ()
    handle (FH h) Close      k = do ioe_lift $ closeFile h
                                    k () ()
    handle (FH h) ReadLine        k = do str <- ioe_lift $ fread h
                                         k str (FH h)
    handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str
                                           k () (FH h)
    handle (FH h) EOF             k = do e <- ioe_lift $ feof h
                                         k e (FH h)

-- -------------------------------------------------------------- [ The Effect ]
FILE_IO : Type -> EFFECT
FILE_IO t = MkEff t FileIO

-- ------------------------------------------------------------ [ The Bindings ]
--
-- Bind the IO context handlers to functions. These functions will run
-- in the IO context.
{'fraction_non_alphanumeric': 0.18515012172031378, 'fraction_numerical': 0.0, 'mean_word_length': 1.2937344913151365, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 33, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4711500', 'n_tokens_mistral': 1991, 'n_tokens_neox': 1894, 'n_words': 815}