Skip to content

Fixed File, and Changed "SWait" to more fitting "SClose" #246

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
MartimBaptista wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

Fixed File, and Changed "SWait" to more fitting "SClose" #246

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions FreeST/StandardLib/File.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,14 @@
module File where

__runWriteFile : FileHandle -> dualof OutStream 1-> ()
__runWriteFile fh ch =
match ch with {
PutChar ch -> let (c, ch) = receive ch in __putFileStr fh (show @Char c); __runWriteFile fh ch,
PutStr ch -> let (s, ch) = receive ch in __putFileStr fh s ; __runWriteFile fh ch,
PutStrLn ch -> let (s, ch) = receive ch in __putFileStr fh (s ^^ "\n") ; __runWriteFile fh ch,
SClose ch -> __closeFile fh; close ch
}

-- | Opens an `OutStream` channel endpoint to a file specified by a path, in write mode.
openWriteFile : FilePath -> OutStream
openWriteFile fp =
Expand All @@ -10,29 +19,20 @@ openAppendFile : FilePath -> OutStream
openAppendFile fp =
forkWith @OutStream @() $ __runWriteFile (__openFile fp AppendMode)

__runWriteFile : FileHandle -> dualof OutStream 1-> ()
__runWriteFile fh ch =
match ch with {
PutChar ch -> let (c, ch) = receive ch in __putFileStr fh (show @Char c); __runWriteFile fh ch,
PutStr ch -> let (s, ch) = receive ch in __putFileStr fh s ; __runWriteFile fh ch,
PutStrLn ch -> let (s, ch) = receive ch in __putFileStr fh (s ++ "\n") ; __runWriteFile fh ch,
Close ch -> __closeFile fh; close ch
}

-- | Opens an InStream channel endpoint to a file specified by a path, in read mode.
openReadFile : FilePath -> InStream
openReadFile fp =
forkWith @InStream @() $ __runReadFile (__openFile fp ReadMode)

__runReadFile : FileHandle -> dualof InStream 1-> ()
__runReadFile fh ch =
match ch with {
GetChar ch -> __runReadFile fh $ send (__readFileChar fh) ch,
GetLine ch -> __runReadFile fh $ send (__readFileLine fh) ch,
IsEOF ch -> __runReadFile fh $ send (__isEOF fh ) ch,
Close ch -> __closeFile fh; close ch
SClose ch -> __closeFile fh; close ch
}

-- | Opens an InStream channel endpoint to a file specified by a path, in read mode.
openReadFile : FilePath -> InStream
openReadFile fp =
forkWith @InStream @() $ __runReadFile (__openFile fp ReadMode)

-- | Writes a string to a file specified by a path.
-- | Does the same as `openWriteFile fp |> hPutStr s |> hCloseOut`.
writeFile : FilePath -> String -> ()
Expand Down
16 changes: 8 additions & 8 deletions FreeST/StandardLib/Prelude.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -474,15 +474,15 @@ runServer handle state c =
type OutStream : 1S = +{ PutChar : !Char ; OutStream
, PutStr : !String ; OutStream
, PutStrLn: !String ; OutStream
, SWait : Wait
, SClose : Wait
}

-- | Unrestricted session type for the `OutStream` type.
type OutStreamProvider : *A = *?OutStream

-- | Closes an `OutStream` channel endpoint. Behaves as a `close`.
hCloseOut : OutStream -> ()
hCloseOut c = c |> select SWait |> wait
hCloseOut c = c |> select SClose |> wait

__hGenericPut : forall a:*T . (OutStream -> !a ; OutStream) -> a -> OutStream -> OutStream
__hGenericPut sel x outStream = sel outStream |> send x
Expand Down Expand Up @@ -542,19 +542,19 @@ hPrint_ x c = __hGenericPut_ @a (hPrint @a) x c
-- | The `InStream` type describes input streams (such as `stdin` and read
-- | files). `GetChar` reads a single character, `GetLine` reads a line, and
-- | `IsEOF` checks for the EOF (End-Of-File) token, i.e., if an input stream
-- | reached the end. Operations in this channel end with the `SWait` option.
-- | reached the end. Operations in this channel end with the `SClose` option.
type InStream : 1S = +{ GetChar: ?Char ; InStream
, GetLine: ?String ; InStream
, IsEOF : ?Bool ; InStream
, SWait : Wait
, SClose : Wait
}

-- | Unrestricted session type for the `OutStream` type.
type InStreamProvider : *A = *?InStream

-- | Closes an `InStream` channel endpoint. Behaves as a `close`.
hCloseIn : InStream -> ()
hCloseIn c = c |> select SWait |> wait
hCloseIn c = c |> select SClose |> wait

__hGenericGet : forall a:*T . (InStream -> ?a ; InStream) -> InStream -> (a, InStream)
__hGenericGet sel c = receive $ sel c
Expand Down Expand Up @@ -665,7 +665,7 @@ __runPrinter _ (PutStr printer) =
readApply @String @dualof OutStream __putStrOut printer |> __runPrinter ()
__runPrinter _ (PutStrLn printer) =
readApply @String @dualof OutStream (\s:String -> __putStrOut (s ^^ "\n")) printer |> __runPrinter ()
__runPrinter _ (SWait printer) =
__runPrinter _ (SClose printer) =
close printer

__runStdout : ()
Expand All @@ -691,7 +691,7 @@ __runErrPrinter _ (PutStr printer) =
readApply @String @dualof OutStream __putStrErr printer |> __runErrPrinter ()
__runErrPrinter _ (PutStrLn printer) =
readApply @String @dualof OutStream (\s:String -> __putStrErr (s ^^ "\n")) printer |> __runErrPrinter ()
__runErrPrinter _ (SWait printer) =
__runErrPrinter _ (SClose printer) =
close printer

__runStderr : ()
Expand Down Expand Up @@ -726,7 +726,7 @@ __runReader _ (GetLine reader) =
__runReader () $ send (__getLine ()) reader
__runReader _ (IsEOF reader) =
__runReader () $ send False reader -- stdin is always open
__runReader _ (SWait reader) =
__runReader _ (SClose reader) =
close reader

__runStdin : ()
Expand Down