git.iko.soy/Idris-dev
on 4162113 help sign in
Idris-dev/libs/effects/Effect/System.idr
52 lines 1.6 kB history raw
1module Effect.System
3-- Various system interaction features (this is not necessarily the right way
4-- to split them up, I just need some of them now :))
6import Effects
7import System
8import Control.IOExcept
9import public Data.So
11%access public export
13data System : Effect where
14 Args : sig System (List String)
15 Time : sig System Integer
16 GetEnv : String -> sig System (Maybe String)
17 CSystem : String -> sig System Int
18 Usleep : (i : Int) -> (inbounds : So (i >= 0 && i <= 1000000)) -> sig System ()
20implementation Handler System IO where
21 handle () Args k = do x <- getArgs; k x ()
22 handle () Time k = do x <- time; k x ()
23 handle () (GetEnv s) k = do x <- getEnv s; k x ()
24 handle () (CSystem s) k = do x <- system s; k x ()
25 handle () (Usleep i prf) k = do usleep i; k () ()
27implementation Handler System (IOExcept a) where
28 handle () Args k = do x <- ioe_lift getArgs; k x ()
29 handle () Time k = do x <- ioe_lift time; k x ()
30 handle () (GetEnv s) k = do x <- ioe_lift $ getEnv 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 () ()
34--- The Effect and associated functions
36SYSTEM : EFFECT
37SYSTEM = MkEff () System
39getArgs : Eff (List String) [SYSTEM]
40getArgs = call Args
42time : Eff Integer [SYSTEM]
43time = call Time
45getEnv : String -> Eff (Maybe String) [SYSTEM]
46getEnv s = call $ GetEnv s
48system : String -> Eff Int [SYSTEM]
49system s = call $ CSystem s
51usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> Eff () [SYSTEM]
52usleep i {prf} = call $ Usleep i prf