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.

Sign up for GitHub

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

Jump to bottom

Add usleep from System to Effect.System #3749

Merged
merged 3 commits into from
Apr 18, 2017
Merged

Add usleep from System to Effect.System #3749

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7c54765
Add usleep from System to Effect.System
artemohanjanyan Apr 8, 2017
f0b776d
Fix typo
artemohanjanyan Apr 8, 2017
2541947
Clean up the types
artemohanjanyan Apr 16, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
11 changes: 11 additions & 0 deletions libs/effects/Effect/System.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ module Effect.System
import Effects
import System
import Control.IOExcept
import public Data.So

%access public export

Expand All @@ -14,18 +15,23 @@ data System : Effect where
Time : sig System Integer
GetEnv : String -> sig System (Maybe String)
CSystem : String -> sig System Int
Usleep : (i : Int) ->
{auto prf : So (i >= fromInteger 0 && Delay (i <= fromInteger 1000000))} ->
Copy link

Choose a reason for hiding this comment

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

Any reason you use fromInteger here explicitly? literals should be overloaded. The same with Delay.

Copy link

Choose a reason for hiding this comment

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

Also I would in the constructor probably not use auto, only in the external signature used by the user.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I just copied the type from System.usleep. fromInteger is probably not necessary, it's shown when you type :t usleep in REPL, but it's not present in the source file. However, auto is used in that source file. Should I still remove it?

Copy link

Choose a reason for hiding this comment

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

@artemohanjanyan Yeah, so I am not sure it is necessary for a constructor to have it. I would just take an argument (inbounds : So (i >= 0 && i <= 1000000)).

sig System ()

implementation Handler System IO where
handle () Args k = do x <- getArgs; k x ()
handle () Time k = do x <- time; k x ()
handle () (GetEnv s) k = do x <- getEnv s; k x ()
handle () (CSystem s) k = do x <- system s; k x ()
handle () (Usleep i) k = do usleep i; k () ()

implementation Handler System (IOExcept a) where
handle () Args k = do x <- ioe_lift getArgs; k x ()
handle () Time k = do x <- ioe_lift time; k x ()
handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()
handle () (CSystem s) k = do x <- ioe_lift $ system s; k x ()
handle () (Usleep i) k = do ioe_lift $ usleep i; k () ()

--- The Effect and associated functions

Expand All @@ -43,3 +49,8 @@ getEnv s = call $ GetEnv s

system : String -> Eff Int [SYSTEM]
system s = call $ CSystem s

usleep : (i : Int) ->
{auto prf : So (i >= fromInteger 0 && Delay (i <= fromInteger 1000000))} ->
Copy link

Choose a reason for hiding this comment

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

Same comment regarding the use of fromInteger and Delay

Copy link

Choose a reason for hiding this comment

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

Is there any reason you do not use System.usleep here instead of copying it?

Copy link

Choose a reason for hiding this comment

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

Sorry, I missed that this calls the effect, whose handler uses the system one.

Eff () [SYSTEM]
usleep i = call $ Usleep i