Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ new ] IO buffering, and loops #2367

Merged
merged 12 commits into from
Apr 21, 2024
35 changes: 34 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
gallais marked this conversation as resolved.
Show resolved Hide resolved

Other major improvements
------------------------
Expand Down Expand Up @@ -66,6 +67,11 @@ Deprecated names
*-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣
```

* In `IO.Base`:
```agda
untilRight ↦ untilInj₂
```

New modules
-----------

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 _∼_ ⇒ _∼_
```

Expand Down
3 changes: 3 additions & 0 deletions GenerateEverything.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
24 changes: 20 additions & 4 deletions doc/README/IO.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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

------------------------------------------------------------------------
Expand Down Expand Up @@ -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
Expand All @@ -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!
Expand Down
2 changes: 1 addition & 1 deletion src/Foreign/Haskell/Coerce.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion src/IO.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -27,6 +27,7 @@ private
-- Re-exporting the basic type and functions

open import IO.Base public
open import IO.Handle public
gallais marked this conversation as resolved.
Show resolved Hide resolved

------------------------------------------------------------------------
-- Utilities
Expand Down
45 changes: 40 additions & 5 deletions src/IO/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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."
#-}
2 changes: 1 addition & 1 deletion src/IO/Finite.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
41 changes: 41 additions & 0 deletions src/IO/Handle.agda
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 1 addition & 1 deletion src/IO/Infinite.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
33 changes: 5 additions & 28 deletions src/IO/Primitive.agda
Original file line number Diff line number Diff line change
@@ -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."
#-}
Copy link
Member

@andreasabel andreasabel Jul 4, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@gallais: Are there plans to use IO.Primitive for something else?
(Otherwise, why the deprecation?)
(Maybe the end user want to import the "top-level" modules rather than Core modules.)

Question came up when updating the Agda testsuite to latest std-lib:

Copy link
Member Author

@gallais gallais Jul 4, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No plans on my end. It was a cleanup because having IO.Primitive sit "above" other primitive-binding
modules like IO.Primitive.Finite seemed at odds with our current practice of the X.Y module being
a partial re-export of X.Y.Z ones.

It's named Core because we don't expect anyone to be importing it (or any of the IO.Primitive modules
for that matter) as we provide a high-level IO interface.

38 changes: 38 additions & 0 deletions src/IO/Primitive/Core.agda
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading