[ new ] IO buffering, and loops (#2367)

* [ new ] IO conditionals & loops

* [ new ] stdin, stdout, stderr, buffering, etc.

* [ fix ] and test for the new IO primitives

* [ fix ] compilation

* [ fix ] more import fixing

* [ done (?) ] with compilation fixes

* [ test ] add test to runner

* [ doc ] explain the loop

* [ compat ] add deprecated stub

* [ fix ] my silly mistake

* [ doc ] list re-exports in CHANGELOG

CHANGELOG.md

@@ -26,6 +26,7 @@ Non-backwards compatible changes
  parametrized by _raw_ bundles, and as such take a proof of transitivity.
 * The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
  parametrized by _raw_ bundles, and as such take a proof of reflexivity.
+* The module `IO.Primitive` was moved to `IO.Primitive.Core`.
 
 Other major improvements
 ------------------------
@@ -66,6 +67,11 @@ Deprecated names
  *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣
  ```
 
+* In `IO.Base`:
+ ```agda
+ untilRight ↦ untilInj₂
+ ```
+
 New modules
 -----------
 
@@ -137,6 +143,12 @@ New modules
  Data.Container.Indexed.Relation.Binary.Equality.Setoid
  ```
 
+* New IO primitives to handle buffering
+ ```agda
+ IO.Primitive.Handle
+ IO.Handle
+ ```
+
 * `System.Random` bindings:
  ```agda
  System.Random.Primitive
@@ -418,13 +430,34 @@ Additions to existing modules
  between : String → String → String → String
  ```
 
+* Re-exported new types and functions in `IO`:
+ ```agda
+ BufferMode : Set
+ noBuffering : BufferMode
+ lineBuffering : BufferMode
+ blockBuffering : Maybe ℕ → BufferMode
+ Handle : Set
+ stdin : Handle
+ stdout : Handle
+ stderr : Handle
+ hSetBuffering : Handle → BufferMode → IO ⊤
+ hGetBuffering : Handle → IO BufferMode
+ hFlush : Handle → IO ⊤
+ ```
+
+* Added new functions in `IO.Base`:
+ ```agda
+ whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤
+ forever : IO ⊤ → IO ⊤
+ ```
+
 * In `Data.Word.Base`:
  ```agda
  _≤_ : Rel Word64 zero
  ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
- ```
+ ```agda
  transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
  ```
 

GenerateEverything.hs

@@ -56,11 +56,14 @@ unsafeModules = map modToFile
  , "IO"
  , "IO.Base"
  , "IO.Categorical"
+ , "IO.Handle"
  , "IO.Infinite"
  , "IO.Instances"
  , "IO.Effectful"
  , "IO.Finite"
  , "IO.Primitive"
+ , "IO.Primitive.Core"
+ , "IO.Primitive.Handle"
  , "IO.Primitive.Infinite"
  , "IO.Primitive.Finite"
  , "Relation.Binary.PropositionalEquality.TrustMe"

doc/README/IO.agda

@@ -13,6 +13,7 @@ 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
 
 ------------------------------------------------------------------------
@@ -86,10 +87,21 @@ cat fp = do
  let ls = lines content
  List.mapM′ putStrLn ls
 
-open import Codata.Musical.Notation
-open import Codata.Musical.Colist
-open import Data.Bool
-open import Data.Unit.Polymorphic.Base
+------------------------------------------------------------------------
+-- 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
@@ -101,6 +113,10 @@ open import Data.Unit.Polymorphic.Base
 -- 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!

src/Foreign/Haskell/Coerce.agda

@@ -35,7 +35,7 @@ open import Level using (Level; _⊔_)
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Int
 
-import IO.Primitive  as STD
+import IO.Primitive.Core as STD
 import Data.List.Base as STD
 import Data.List.NonEmpty.Base as STD
 import Data.Maybe.Base as STD

src/IO.agda

@@ -14,7 +14,7 @@ open import Data.Unit.Polymorphic.Base
 open import Data.String.Base using (String)
 import Data.Unit.Base as Unit0
 open import Function.Base using (_∘_; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 open import Level
 
 private
@@ -27,6 +27,7 @@ private
 -- Re-exporting the basic type and functions
 
 open import IO.Base public
+open import IO.Handle public
 
 ------------------------------------------------------------------------
 -- Utilities

src/IO/Base.agda

@@ -16,13 +16,14 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 import Agda.Builtin.Unit as Unit0
 open import Data.Unit.Polymorphic.Base
 open import Function.Base using (_∘′_; const; flip)
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 
 private
  variable
- a b : Level
+ a b e : Level
  A : Set a
  B : Set b
+ E : Set e
 
 ------------------------------------------------------------------------
 -- The IO monad
@@ -106,18 +107,37 @@ lift′ io = lift (io Prim.>>= λ _ → Prim.pure _)
 ignore : IO A → IO ⊤
 ignore io = io >> pure _
 
+
+------------------------------------------------------------------------
 -- Conditional executions
+
+-- Only run the action if the boolean is true
 when : Bool → IO {a} ⊤ → IO ⊤
 when true m = m
 when false _ = pure _
 
+-- Only run the action if the boolean is false
 unless : Bool → IO {a} ⊤ → IO ⊤
 unless = when ∘′ not
 
+-- Run the action if the `Maybe` computation was successful
 whenJust : Maybe A → (A → IO {a} ⊤) → IO ⊤
 whenJust (just a) k = k a
 whenJust nothing _ = pure _
 
+-- Run the action if the `E ⊎_` computation was successful
+whenInj₂ : E ⊎ A → (A → IO {a} ⊤) → IO ⊤
+whenInj₂ (inj₂ a) k = k a
+whenInj₂ (inj₁ _) _ = pure _
+
+
+------------------------------------------------------------------------
+-- Loops
+
+-- Keep running the action forever
+forever : IO {a} ⊤ → IO {a} ⊤
+forever act = seq (♯ act) (♯ forever act)
+
 -- Keep running an IO action until we get a value. Convenient when user
 -- input is involved and it may be malformed.
 untilJust : IO (Maybe A) → IO A
@@ -127,7 +147,22 @@ untilJust m = bind (♯ m) λ where
  nothing → ♯ untilJust m
  (just a) → ♯ pure a
 
-untilRight : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
-untilRight f x = bind (♯ f x) λ where
- (inj₁ x′) → ♯ untilRight f x′
+untilInj₂ : {A B : Set a} → (A → IO (A ⊎ B)) → A → IO B
+untilInj₂ f x = bind (♯ f x) λ where
+ (inj₁ x′) → ♯ untilInj₂ f x′
  (inj₂ y) → ♯ pure y
+
+
+
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATIONS
+
+untilRight = untilInj₂
+{-# WARNING_ON_USAGE untilRight
+"Warning: untilRight was deprecated in v2.1.
+Please use untilInj₂ instead."
+#-}

src/IO/Finite.agda

@@ -12,7 +12,7 @@ open import Data.Unit.Polymorphic.Base
 open import Agda.Builtin.String
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Finite as Prim
 open import Level
 

src/IO/Handle.agda

@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --guardedness #-}
+
+module IO.Handle where
+
+open import Level using (Level)
+open import Data.Unit.Polymorphic.Base using (⊤)
+open import IO.Base using (IO; lift; lift′)
+
+private variable a : Level
+
+------------------------------------------------------------------------
+-- Re-exporting types and constructors
+
+open import IO.Primitive.Handle as Prim public
+ using ( BufferMode
+ ; noBuffering
+ ; lineBuffering
+ ; blockBuffering
+ ; Handle
+ ; stdin
+ ; stdout
+ ; stderr
+ )
+
+------------------------------------------------------------------------
+-- Wrapping functions
+
+hSetBuffering : Handle → BufferMode → IO {a} ⊤
+hSetBuffering hdl bm = lift′ (Prim.hSetBuffering hdl bm)
+
+hGetBuffering : Handle → IO BufferMode
+hGetBuffering hdl = lift (Prim.hGetBuffering hdl)
+
+hFlush : Handle → IO {a} ⊤
+hFlush hdl = lift′ (Prim.hFlush hdl)

src/IO/Infinite.agda

@@ -13,7 +13,7 @@ open import Agda.Builtin.String
 open import Data.Unit.Polymorphic.Base
 import Data.Unit.Base as Unit0
 open import IO.Base
-import IO.Primitive as Prim
+import IO.Primitive.Core as Prim
 import IO.Primitive.Infinite as Prim
 open import Level
 

src/IO/Primitive.agda

@@ -1,38 +1,15 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Primitive IO: simple bindings to Haskell types and functions
+-- This module is DEPRECATED. Please use IO.Primitive.Core instead
 ------------------------------------------------------------------------
 
--- NOTE: the contents of this module should be accessed via `IO`.
-
 {-# OPTIONS --cubical-compatible #-}
 
 module IO.Primitive where
 
-open import Level using (Level)
-private
- variable
- a : Level
- A B : Set a
-
-------------------------------------------------------------------------
--- The IO monad
-
-open import Agda.Builtin.IO public
- using (IO)
-
-infixl 1 _>>=_
-
-postulate
- pure : A → IO A
- _>>=_ : IO A → (A → IO B) → IO B
-
-{-# COMPILE GHC pure = \_ _ -> return #-}
-{-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-}
-{-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
-{-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+open import IO.Primitive.Core public
 
--- Haskell-style alternative syntax
-return : A → IO A
-return = pure
+{-# WARNING_ON_IMPORT
+"IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."
+#-}

src/IO/Primitive/Core.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive IO: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+-- NOTE: the contents of this module should be accessed via `IO`.
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive.Core where
+
+open import Level using (Level)
+private
+ variable
+ a : Level
+ A B : Set a
+
+------------------------------------------------------------------------
+-- The IO monad
+
+open import Agda.Builtin.IO public
+ using (IO)
+
+infixl 1 _>>=_
+
+postulate
+ pure : A → IO A
+ _>>=_ : IO A → (A → IO B) → IO B
+
+{-# COMPILE GHC pure = \_ _ -> return #-}
+{-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-}
+{-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
+{-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+
+-- Haskell-style alternative syntax
+return : A → IO A
+return = pure