83 lines
2.6 KiB
Plaintext
83 lines
2.6 KiB
Plaintext
!import "base.tri" !Local
|
|
!import "list.tri" !Local
|
|
!import "conversions.tri" !Local
|
|
|
|
-- IO constructors for host-interpreted interaction trees.
|
|
-- See docs/io-in-tricu.md for the full protocol.
|
|
|
|
version = 1
|
|
|
|
io = action : pair "tricuIO" (pair version action)
|
|
pure = x : pair 0 x
|
|
putStr = s k : pair 1 (pair s k)
|
|
getLine = k : pair 2 k
|
|
readFile = p k : pair 3 (pair p k)
|
|
writeFile = p c k : pair 4 (pair p (pair c k))
|
|
|
|
-- ---------------------------------------------------------------------------
|
|
-- CPS sequencing helpers
|
|
-- ---------------------------------------------------------------------------
|
|
|
|
-- Print a string and finish successfully.
|
|
print = s : putStr s (_ : pure t)
|
|
|
|
-- Print a string plus newline and finish successfully.
|
|
printLn = s : putStr (append s "\n") (_ : pure t)
|
|
|
|
-- CPS print with newline.
|
|
putStrLn = s k : putStr (append s "\n") k
|
|
|
|
-- Sequence after putStr, ignoring Unit.
|
|
afterPutStr = s next : putStr s (_ : next)
|
|
|
|
-- Sequence after putStrLn, ignoring Unit.
|
|
afterPutStrLn = s next : putStr (append s "\n") (_ : next)
|
|
|
|
-- ---------------------------------------------------------------------------
|
|
-- Result-aware file helpers
|
|
-- ---------------------------------------------------------------------------
|
|
|
|
-- Read a file, forcing the caller to handle both success and error.
|
|
onReadFile = (path errCase okCase :
|
|
readFile path (result :
|
|
matchResult errCase okCase result))
|
|
|
|
-- Write a file, forcing the caller to handle both success and error.
|
|
onWriteFile = (path contents errCase okCase :
|
|
writeFile path contents (result :
|
|
matchResult errCase okCase result))
|
|
|
|
-- ---------------------------------------------------------------------------
|
|
-- Convenience helpers for the common cases
|
|
-- ---------------------------------------------------------------------------
|
|
|
|
-- Read a file; on error print a message and finish.
|
|
readFileOrPrintError = (path okCase :
|
|
onReadFile path
|
|
(err rest :
|
|
putStrLn "Read failed" (_ :
|
|
pure t))
|
|
okCase)
|
|
|
|
-- Write a file; on error print a message and finish.
|
|
writeFileOrPrintError = (path contents okCase :
|
|
onWriteFile path contents
|
|
(err rest :
|
|
putStrLn "Write failed" (_ :
|
|
pure t))
|
|
okCase)
|
|
|
|
-- Copy src to dst, then continue with k on success.
|
|
copyFile = (src dst k :
|
|
onReadFile src
|
|
(err rest :
|
|
putStrLn "Read failed" (_ :
|
|
pure t))
|
|
(contents rest :
|
|
onWriteFile dst contents
|
|
(err rest :
|
|
putStrLn "Write failed" (_ :
|
|
pure t))
|
|
(ok rest :
|
|
k t)))
|