module IOObjects where

open import Size
open import Data.Product
open import Data.String.Base

open import NativeIOSafe
open import IOTrees hiding (main)

-- The interface of an object is its set of methods,
-- and for each method, its result type.

-- The method parameters are considered part of the method,
-- thus, usually the method set will be infinite.

record Interface : Set₁ where
  field Method : Set
        Result : Method → Set
open Interface

-- An I/O-object will, upon a method call, do a possibly
-- infinite sequence of I/O-interactions, and finally
-- return the method result plus itself in its new state.

record IOObject (Iio : IOInterface) (I : Interface) i : Set where
  coinductive
  field method : ∀{j : Size< i} → (m : Method I) → IO Iio ∞ (Result I m × IOObject Iio I j)
open IOObject

-- Example: a simple Cell object that stores an element of type A.

-- Cell interface

data CellMethod A : Set where
  get : CellMethod A
  put : A → CellMethod A

CellResult : ∀{A} → CellMethod A → Set
CellResult {A} get = A
CellResult (put _) = Unit

CellInterface = λ A → record { Method = CellMethod A ; Result = CellResult }

-- Cell class

CellC = IOObject ConsoleInterface (CellInterface String)

-- A Cell object that logs the method calls via I/O.

simpleCell : ∀ {i} (s : String) → CellC i

method (simpleCell s) get =
  do (putStrLn ("getting (" ++ s ++ ")")) >>= λ _ →
  return (s , simpleCell s)

method (simpleCell s) (put x) =
  do (putStrLn ("putting (" ++ x ++ ")")) >>= λ _ →
  return (_ , simpleCell x)

-- A simple (co)recursive program using the simpleCell.

program : ∀{i} → IO ConsoleInterface i Unit
force program =
  let c₁ = simpleCell "Start" in
  do' getLine       λ{ nothing → return _; (just s) →
  method c₁ (put s)  >>= λ{ (_ , c₂) →
  method c₂ get      >>= λ{ (s' , c₃) →
  do (putStrLn s')  >>= λ _ →
  program           }}}

main : NativeIO Unit
main = translateIO translateConsole program