@@ -6,6 +6,7 @@ module Effect.System
6import Effects
6import Effects
7import System
7import System
8import Control.IOExcept
8import Control.IOExcept
10%access public export
11%access public export
@@ -14,18 +15,21 @@ data System : Effect where
14 Time : sig System Integer
15 Time : sig System Integer
15 GetEnv : String -> sig System (Maybe String)
16 GetEnv : String -> sig System (Maybe String)
16 CSystem : String -> sig System Int
17 CSystem : String -> sig System Int
18+ Usleep : (i : Int) -> (inbounds : So (i >= 0 && i <= 1000000)) -> sig System ()
18implementation Handler System IO where
20implementation Handler System IO where
19 handle () Args k = do x <- getArgs; k x ()
21 handle () Args k = do x <- getArgs; k x ()
20 handle () Time k = do x <- time; k x ()
22 handle () Time k = do x <- time; k x ()
21 handle () (GetEnv s) k = do x <- getEnv s; k x ()
23 handle () (GetEnv s) k = do x <- getEnv s; k x ()
22 handle () (CSystem s) k = do x <- system s; k x ()
24 handle () (CSystem s) k = do x <- system s; k x ()
25+ handle () (Usleep i prf) k = do usleep i; k () ()
24implementation Handler System (IOExcept a) where
27implementation Handler System (IOExcept a) where
25 handle () Args k = do x <- ioe_lift getArgs; k x ()
28 handle () Args k = do x <- ioe_lift getArgs; k x ()
26 handle () Time k = do x <- ioe_lift time; k x ()
29 handle () Time k = do x <- ioe_lift time; k x ()
27 handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()
30 handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()
28 handle () (CSystem s) k = do x <- ioe_lift $ system s; k x ()
31 handle () (CSystem s) k = do x <- ioe_lift $ system s; k x ()
32+ handle () (Usleep i prf) k = do ioe_lift $ usleep i; k () ()
30--- The Effect and associated functions
34--- The Effect and associated functions
@@ -43,3 +47,6 @@ getEnv s = call $ GetEnv s
44system : String -> Eff Int [SYSTEM]
48system : String -> Eff Int [SYSTEM]
45system s = call $ CSystem s
49system s = call $ CSystem s
51+usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> Eff () [SYSTEM]
52+usleep i {prf} = call $ Usleep i prf