Add usleep from System to Effect.System #3749
Conversation
libs/effects/Effect/System.idr
Outdated
| @@ -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))} -> | |||
There was a problem hiding this comment.
Any reason you use fromInteger here explicitly? literals should be overloaded. The same with Delay.
There was a problem hiding this comment.
Also I would in the constructor probably not use auto, only in the external signature used by the user.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
@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)).
libs/effects/Effect/System.idr
Outdated
| @@ -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))} -> | |||
There was a problem hiding this comment.
Same comment regarding the use of fromInteger and Delay
There was a problem hiding this comment.
Is there any reason you do not use System.usleep here instead of copying it?
There was a problem hiding this comment.
Sorry, I missed that this calls the effect, whose handler uses the system one.
Unnecessary `fromInteger` and `Delay` were removed. `prf` is now explicit argument of type constructor, but it's still implicit in function as in `System.usleep`.
|
Thanks! |
* Add usleep from System to Effect.System
No description provided.