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

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

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