Add usleep from System to Effect.System (idris-lang#3749)

* Add usleep from System to Effect.System

libs/effects/Effect/System.idr

@@ -6,6 +6,7 @@ module Effect.System
 import Effects
 import System
 import Control.IOExcept
+import public Data.So
 
 %access public export
 
@@ -14,18 +15,21 @@ data System : Effect where
      Time : sig System Integer
      GetEnv : String -> sig System (Maybe String)
      CSystem : String -> sig System Int
+     Usleep : (i : Int) -> (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 prf) 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 prf) k = do ioe_lift $ usleep i; k () ()
 
 --- The Effect and associated functions
 
@@ -43,3 +47,6 @@ getEnv s = call $ GetEnv s
 
 system : String -> Eff Int [SYSTEM]
 system s = call $ CSystem s
+
+usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> Eff () [SYSTEM]
+usleep i {prf} = call $ Usleep i prf