module IOTrees where

open import Size
open import Data.Unit.Base
open import Data.Maybe.Base
open import Data.String.Base

open import NativeIOSafe

-- Following Hancock and Setzer, a (client-side) interactive program
-- issues a command, waits for the response, and continues depending
-- on the received response.

-- We can view an interactive program as a potentially infinite tree
-- whose nodes are labelled with commands and whose edges are labelled
-- with the possible responses to a command.

-- The interface to the operating system consists of possible commands
-- and possible responses, by command.

record IOInterface : Set₁ where
  field Command  : Set
        Response : Command → Set
open IOInterface public

mutual
  data IO' (I : IOInterface) i A : Set where
    do'     : (c : Command I) (k : Response I c → IO I i A) → IO' I i A
    return' : (a : A) → IO' I i A

  record IO (I : IOInterface) i A : Set where
    coinductive
    field force : ∀{j : Size< i} → IO' I j A
open IO public

-- IO is a monad

return : ∀{I i A} → A → IO I (↑ i) A
force (return a) = return' a

_>>=_ : ∀{I i A B} → IO I i A → (A → IO I i B) → IO I i B
force (m >>= k) with force m
force (m >>= k) | do' c k₀ = do' c λ r → k₀ r >>= k
force (m >>= k) | return' a = force (k a)

-- executing a single command

do : ∀{I i} (c : Command I) → IO I (↑ i) (Response I c)
force (do c) = do' c return

-- Example: copy cat

-- We only require two commands from the OS.

data ConsoleCommand : Set where
  getLine  : ConsoleCommand            -- read stdin
  putStrLn : String → ConsoleCommand   -- write to stdout

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse getLine  = Maybe String
ConsoleResponse (putStrLn _) = Unit

ConsoleInterface : IOInterface
Command  ConsoleInterface = ConsoleCommand
Response ConsoleInterface = ConsoleResponse

cat : ∀{i} → IO ConsoleInterface i Unit
force cat =
  do' getLine      λ{ nothing → return _; (just s) →
  do (putStrLn s)  >>= λ _ →
  cat              }

-- Running the cat program

{-# NON_TERMINATING #-}
translateIO : ∀{I A} →
  (tr : (c : Command I) → NativeIO (Response I c)) →
  IO I ∞ A → NativeIO A
translateIO tr m with force m
... | do' c k = tr c  native>>= λ r → translateIO tr (k r)
... | return' a = nativeReturn a

translateConsole : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateConsole getLine      = nativeGetLine
translateConsole (putStrLn s) = nativePutStrLn s

main : NativeIO Unit
main = translateIO translateConsole cat