------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple examples of programs using IO
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module README.IO where

open import Level
open import Data.Nat.Base
open import Data.Nat.Show using (show)
open import Data.String.Base using (String; _++_; lines)
open import Data.Unit.Polymorphic
open import Function.Base using (_$_)
open import IO

------------------------------------------------------------------------
-- Basic programs
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Hello World!

-- Minimal example of an IO program.
-- * The entrypoint of the executable is given type `Main`
-- * It is implemented using `run`, a function that converts a description
--   of an IO-computation into a computation that actually invokes the magic
--   primitives that will perform the side effects.

helloWorld : Main
helloWorld = run (putStrLn "Hello World!")

------------------------------------------------------------------------
-- Hello {{name}}!

-- We can of course write little auxiliary functions that may be used in
-- larger IO programs. Here we are going to first write a function displaying
-- "Hello {{name}}!" when {{name}} is passed as an argument.

-- `IO` primitives whose sole purpose is generating side effects (e.g.
-- printing a string on the screen) are typically given a level polymorphic
-- type which means we may need to add explicit level annotations.
-- Here we state that the `IO` computation will be at level zero (`0ℓ`).

sayHello : String → IO {0ℓ} ⊤
sayHello name = putStrLn ("Hello " ++ name ++ "!")

-- Functions can be sequenced using monadic combinators or `do` notations.
-- The two following definitions are equivalent. They start by asking the
-- user what their name is, listen for an answer and respond by saying hello
-- using the `sayHello` auxiliary function we just defined.

helloName : Main
helloName = run (putStrLn "What is your name?" >> getLine >>= sayHello)

doHelloName : Main
doHelloName = run do
  putStrLn "What is your name?"
  name ← getLine
  sayHello name

------------------------------------------------------------------------
-- (Co)Recursive programs
------------------------------------------------------------------------

------------------------------------------------------------------------
-- NO GUARDEDNESS

-- If you do not need to rely on guardedness for the function to be seen as
-- terminating (for instance because it is structural in an inductive argument)
-- then you can use `do` notations to write fairly readable programs.

-- Countdown to explosion
countdown : ℕ → IO {0ℓ} _
countdown zero      = putStrLn "BOOM!"
countdown m@(suc n) = do
  let str = show m
  putStrLn str
  countdown n

-- cat the content of a finite file
cat : String → IO _
cat fp = do
  content ← readFiniteFile fp
  let ls = lines content
  List.mapM′ putStrLn ls

------------------------------------------------------------------------
-- TOP-LEVEL LOOP

-- If you simply want to repeat the same action over and over again, you
-- can use `forever` e.g. the following defines a REPL that echos whatever
-- the user types

echo : IO ⊤
echo = do
  hSetBuffering stdout noBuffering
  forever $ do
    putStr "echo< "
    str ← getLine
    putStrLn ("echo> " ++ str)


------------------------------------------------------------------------
-- GUARDEDNESS

-- If you are performing coinduction on a potentially infinite piece of codata
-- then you need to rely on guardedness. That is to say that the coinductive
-- call needs to be obviously under a coinductive constructor and guarded by a
-- sharp (♯_).
-- In this case you cannot use the convenient combinators that make `do`-notations
-- and have to revert back to the underlying coinductive constructors.

open import Codata.Musical.Notation
open import Codata.Musical.Colist using (Colist; []; _∷_)
open import Data.Bool
open import Data.Unit.Polymorphic.Base

-- Whether a colist is finite is semi decidable: just let the user wait until
-- you reach the end!
isFinite : ∀ {a} {A : Set a} → Colist A → IO Bool
isFinite []       = pure true
isFinite (x ∷ xs) = seq (♯ pure tt) (♯ isFinite (♭ xs))