!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)))