[ new ] IO buffering, and loops

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
 ------------------------
@@ -54,6 +55,11 @@ Deprecated names
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
   ```
 
+* In `IO.Base`:
+  ```agda
+  untilRight  ↦  untilInj₂
+  ```
+
 New modules
 -----------
 
@@ -125,6 +131,12 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* New IO primitives to handle buffering
+  ```agda
+  IO.Primitive.Handle
+  IO.Handle
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -378,9 +390,16 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  ```
 
-* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
+* Added new functions in `IO.Base`:
+  ```agda
+  whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤
+  forever : IO ⊤ → IO ⊤
   ```
+
+* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
+  ```agda
   transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
   ```
 

GenerateEverything.hs

@@ -56,11 +56,13 @@ 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 → src/IO/Primitive/Core.agda

@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible #-}
 
-module IO.Primitive where
+module IO.Primitive.Core where
 
 open import Level using (Level)
 private

src/IO/Primitive/Handle.agda

@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive IO handles: simple bindings to Haskell types and functions
+------------------------------------------------------------------------
+
+-- NOTE: the contents of this module should be accessed via `IO`.
+
+{-# OPTIONS --cubical-compatible #-}
+
+module IO.Primitive.Handle where
+
+open import Data.Maybe.Base using (Maybe)
+open import Data.Nat.Base using (ℕ)
+
+data BufferMode : Set where
+  noBuffering lineBuffering : BufferMode
+  blockBuffering : Maybe ℕ → BufferMode
+{-# FOREIGN GHC import System.IO #-}
+{-# FOREIGN GHC
+    data AgdaBufferMode
+      = AgdaNoBuffering
+      | AgdaLineBuffering
+      | AgdaBlockBuffering (Maybe Integer)
+    toBufferMode :: AgdaBufferMode -> BufferMode
+    toBufferMode x = case x of
+      AgdaNoBuffering       -> NoBuffering
+      AgdaLineBuffering     -> LineBuffering
+      AgdaBlockBuffering mi -> BlockBuffering (fromIntegral <$> mi)
+    fromBufferMode :: BufferMode -> AgdaBufferMode
+    fromBufferMode x = case x of
+      NoBuffering       -> AgdaNoBuffering
+      LineBuffering     -> AgdaLineBuffering
+      BlockBuffering mi -> AgdaBlockBuffering (fromIntegral <$> mi)
+#-}
+
+{-# COMPILE GHC BufferMode = data AgdaBufferMode
+                           ( AgdaNoBuffering
+                           | AgdaLineBuffering
+                           | AgdaBlockBuffering
+                           )
+#-}
+
+open import Data.Unit.Base using (⊤)
+open import IO.Primitive.Core using (IO)
+
+postulate
+  Handle : Set
+  stdin stdout stderr : Handle
+  hSetBuffering : Handle → BufferMode → IO ⊤
+  hGetBuffering : Handle → IO BufferMode
+  hFlush : Handle → IO ⊤
+
+{-# FOREIGN GHC import System.IO #-}
+{-# COMPILE GHC Handle = type Handle #-}
+{-# COMPILE GHC stdin = stdin #-}
+{-# COMPILE GHC stdout = stdout #-}
+{-# COMPILE GHC stderr = stderr #-}
+{-# COMPILE GHC hSetBuffering = \ h -> hSetBuffering h . toBufferMode #-}
+{-# COMPILE GHC hGetBuffering = fmap fromBufferMode . hGetBuffering #-}
+{-# COMPILE GHC hFlush = hFlush #-}

src/System/Clock/Primitive.agda

@@ -9,7 +9,7 @@
 module System.Clock.Primitive where
 
 open import Agda.Builtin.Nat using (Nat)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Foreign.Haskell using (Pair)
 
 data Clock : Set where

src/System/Environment/Primitive.agda

@@ -14,7 +14,7 @@
 
 module System.Environment.Primitive where
 
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
 open import Data.String.Base using (String)

src/System/FilePath/Posix/Primitive.agda

@@ -14,7 +14,7 @@ open import Agda.Builtin.List using (List)
 open import Agda.Builtin.Maybe using (Maybe)
 open import Agda.Builtin.String using (String)
 open import Foreign.Haskell as FFI using (Pair; Either)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 
 -- A filepath has a nature: it can be either relative or absolute.
 -- We postulate this nature rather than defining it as an inductive

src/System/Process/Primitive.agda

@@ -13,7 +13,7 @@ open import Agda.Builtin.List
 open import Agda.Builtin.String
 open import Agda.Builtin.Unit
 open import Foreign.Haskell using (Pair)
-open import IO.Primitive using (IO)
+open import IO.Primitive.Core using (IO)
 open import System.Exit.Primitive using (ExitCode)
 
 postulate