git.iko.soy/Idris-dev
on master help sign in
Add neweffects library
99376f4Edwin Brady
libs/neweffects/Effect/Default.idrnew file+44
compare with master
unifiedsplit
@@ -0,0 +1,44 @@
1+module Default
2+
3+class Default a where
4+ default : a
5+
6+instance Default Int where
7+ default = 0
8+
9+instance Default Integer where
10+ default = 0
11+
12+instance Default Float where
13+ default = 0
14+
15+instance Default Nat where
16+ default = 0
17+
18+instance Default Char where
19+ default = '\0'
20+
21+instance Default String where
22+ default = ""
23+
24+instance Default Bool where
25+ default = False
26+
27+instance Default () where
28+ default = ()
29+
30+instance (Default a, Default b) => Default (a, b) where
31+ default = (default, default)
32+
33+instance Default (Maybe a) where
34+ default = Nothing
35+
36+instance Default (List a) where
37+ default = []
38+
39+instance Default a => Default (Vect n a) where
40+ default = mkDef _ where
41+ mkDef : (n : Nat) -> Vect n a
42+ mkDef Z = []
43+ mkDef (S k) = default :: mkDef k
44+
libs/neweffects/Effect/Exception.idrnew file+39
@@ -0,0 +1,39 @@
1+module Effect.Exception
2+
3+import Effects
4+import System
5+import Control.IOExcept
6+
7+data Exception : Type -> Effect where
8+ Raise : a -> { () } Exception a b
9+
10+instance Handler (Exception a) Maybe where
11+ handle _ (Raise e) k = Nothing
12+
13+instance Show a => Handler (Exception a) IO where
14+ handle _ (Raise e) k = do print e
15+ believe_me (exit 1)
16+
17+instance Handler (Exception a) (IOExcept a) where
18+ handle _ (Raise e) k = ioM (return (Left e))
19+
20+instance Handler (Exception a) (Either a) where
21+ handle _ (Raise e) k = Left e
22+
23+EXCEPTION : Type -> EFFECT
24+EXCEPTION t = MkEff () (Exception t)
25+
26+raise : a -> { [EXCEPTION a ] } Eff m b
27+raise err = Raise err
28+
29+
30+
31+
32+
33+
34+-- TODO: Catching exceptions mid program?
35+-- probably need to invoke a new interpreter
36+
37+-- possibly add a 'handle' to the Eff language so that an alternative
38+-- handler can be introduced mid interpretation?
39+
libs/neweffects/Effect/File.idrnew file+62
@@ -0,0 +1,62 @@
1+module Effect.File
2+
3+import Effects
4+import Control.IOExcept
5+
6+data OpenFile : Mode -> Type where
7+ FH : File -> OpenFile m
8+
9+openOK : Mode -> Bool -> Type
10+openOK m True = OpenFile m
11+openOK m False = ()
12+
13+data FileIO : Effect where
14+ Open : String -> (m : Mode) ->
15+ {() ==> if result then OpenFile m else ()} FileIO Bool
16+ Close : {OpenFile m ==> ()} FileIO ()
17+
18+ ReadLine : {OpenFile Read} FileIO String
19+ WriteLine : String -> {OpenFile Write} FileIO ()
20+ EOF : {OpenFile Read} FileIO Bool
21+
22+instance Handler FileIO IO where
23+ handle () (Open fname m) k = do h <- openFile fname m
24+ valid <- validFile h
25+ if valid then k True (FH h)
26+ else k False ()
27+ handle (FH h) Close k = do closeFile h
28+ k () ()
29+ handle (FH h) ReadLine k = do str <- fread h
30+ k str (FH h)
31+ handle (FH h) (WriteLine str) k = do fwrite h str
32+ k () (FH h)
33+ handle (FH h) EOF k = do e <- feof h
34+ k e (FH h)
35+
36+FILE_IO : Type -> EFFECT
37+FILE_IO t = MkEff t FileIO
38+
39+open : Handler FileIO e =>
40+ String -> (m : Mode) ->
41+ { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool
42+open f m = Open f m
43+
44+close : Handler FileIO e =>
45+ { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
46+close = Close
47+
48+readLine : Handler FileIO e =>
49+ { [FILE_IO (OpenFile Read)] } Eff e String
50+readLine = ReadLine
51+
52+writeLine : Handler FileIO e =>
53+ String -> { [FILE_IO (OpenFile Write)] } Eff e ()
54+writeLine str = WriteLine str
55+
56+eof : Handler FileIO e =>
57+ { [FILE_IO (OpenFile Read)] } Eff e Bool
58+eof = EOF
59+
60+
61+
62+
libs/neweffects/Effect/Memory.idrnew file+175
@@ -0,0 +1,175 @@
1+module Effect.Memory
2+
3+import Effects
4+import Control.IOExcept
5+
6+%access public
7+
8+abstract
9+data MemoryChunk : Nat -> Nat -> Type where
10+ CH : Ptr -> MemoryChunk size initialized
11+
12+abstract
13+data RawMemory : Effect where
14+ Allocate : (n : Nat) ->
15+ RawMemory () () (\v => MemoryChunk n 0)
16+ Free : RawMemory () (MemoryChunk n i) (\v => ())
17+ Initialize : Bits8 ->
18+ (size : Nat) ->
19+ so (i + size <= n) ->
20+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
21+ Peek : (offset : Nat) ->
22+ (size : Nat) ->
23+ so (offset + size <= i) ->
24+ RawMemory (Vect size Bits8)
25+ (MemoryChunk n i) (\v => MemoryChunk n i)
26+ Poke : (offset : Nat) ->
27+ (Vect size Bits8) ->
28+ so (offset <= i && offset + size <= n) ->
29+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
30+ Move : (src : MemoryChunk src_size src_init) ->
31+ (dst_offset : Nat) ->
32+ (src_offset : Nat) ->
33+ (size : Nat) ->
34+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
35+ so (src_offset + size <= src_init) ->
36+ RawMemory () (MemoryChunk dst_size dst_init)
37+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
38+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
39+
40+private
41+do_malloc : Nat -> IOExcept String Ptr
42+do_malloc size with (fromInteger (cast size) == size)
43+ | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
44+ fail <- ioe_lift $ nullPtr ptr
45+ if fail then ioe_fail "Cannot allocate memory"
46+ else return ptr
47+ | False = ioe_fail "The target architecture does not support adressing enough memory"
48+
49+private
50+do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
51+do_memset ptr offset c size
52+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
53+ ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
54+
55+private
56+do_free : Ptr -> IO ()
57+do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
58+
59+private
60+do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
61+do_memmove dest src dest_offset src_offset size
62+ = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
63+ dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
64+
65+private
66+do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
67+do_peek _ _ Z = return (Prelude.Vect.Nil)
68+do_peek ptr offset (S n)
69+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
70+ bs <- do_peek ptr (S offset) n
71+ Prelude.Monad.return (Prelude.Vect.(::) b bs)
72+
73+private
74+do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
75+do_poke _ _ [] = return ()
76+do_poke ptr offset (b::bs)
77+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
78+ do_poke ptr (S offset) bs
79+
80+instance Handler RawMemory (IOExcept String) where
81+ handle () (Allocate n) k
82+ = do ptr <- do_malloc n
83+ k () (CH ptr)
84+ handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
85+ = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
86+ handle (CH ptr) (Free) k
87+ = ioe_lift (do_free ptr) $> k () ()
88+ handle (CH ptr) (Peek offset size _) k
89+ = do res <- ioe_lift (do_peek ptr offset size)
90+ k res (CH ptr)
91+ handle (CH ptr) (Poke offset content _) k
92+ = do ioe_lift (do_poke ptr offset content)
93+ k () (CH ptr)
94+ handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
95+ = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
96+ k () (CH dest_ptr)
97+ handle chunk (GetRawPtr) k
98+ = k chunk chunk
99+
100+RAW_MEMORY : Type -> EFFECT
101+RAW_MEMORY t = MkEff t RawMemory
102+
103+allocate : (n : Nat) ->
104+ Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
105+allocate size = Allocate size
106+
107+initialize : {i : Nat} ->
108+ {n : Nat} ->
109+ Bits8 ->
110+ (size : Nat) ->
111+ so (i + size <= n) ->
112+ Eff m () [RAW_MEMORY (MemoryChunk n i)]
113+ (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
114+initialize c size prf = Initialize c size prf
115+
116+free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
117+free = Free
118+
119+peek : {i : Nat} ->
120+ (offset : Nat) ->
121+ (size : Nat) ->
122+ so (offset + size <= i) ->
123+ { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)
124+peek offset size prf = Peek offset size prf
125+
126+poke : {n : Nat} ->
127+ {i : Nat} ->
128+ (offset : Nat) ->
129+ Vect size Bits8 ->
130+ so (offset <= i && offset + size <= n) ->
131+ Eff m () [RAW_MEMORY (MemoryChunk n i)]
132+ (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
133+poke offset content prf = Poke offset content prf
134+
135+private
136+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)
137+getRawPtr = GetRawPtr
138+
139+private
140+move' : {dst_size : Nat} ->
141+ {dst_init : Nat} ->
142+ {src_init : Nat} ->
143+ (src_ptr : MemoryChunk src_size src_init) ->
144+ (dst_offset : Nat) ->
145+ (src_offset : Nat) ->
146+ (size : Nat) ->
147+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
148+ so (src_offset + size <= src_init) ->
149+ Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
150+ (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
151+move' src_ptr dst_offset src_offset size dst_bounds src_bounds
152+ = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
153+
154+data MoveDescriptor = Dst | Src
155+
156+move : {dst_size : Nat} ->
157+ {dst_init : Nat} ->
158+ {src_size : Nat} ->
159+ {src_init : Nat} ->
160+ (dst_offset : Nat) ->
161+ (src_offset : Nat) ->
162+ (size : Nat) ->
163+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
164+ so (src_offset + size <= src_init) ->
165+ Eff m ()
166+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
167+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
168+ (\v =>
169+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
170+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
171+move dst_offset src_offset size dst_bounds src_bounds
172+ = do src_ptr <- Src :- getRawPtr
173+ Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
174+ return ()
175+
libs/neweffects/Effect/Monad.idrnew file+21
@@ -0,0 +1,21 @@
1+module Effect.Monad
2+
3+import Effects
4+
5+-- Eff is a monad too, so we can happily use it in a monad transformer.
6+
7+using (xs : List EFFECT, m : Type -> Type)
8+ instance Functor (\a => EffM m a xs (\v => xs)) where
9+ map f prog = do t <- prog
10+ value (f t)
11+
12+ instance Applicative (\a => EffM m a xs (\v => xs)) where
13+ pure = value
14+ (<$>) f a = do f' <- f
15+ a' <- a
16+ value (f' a')
17+
18+ instance Monad (\a => Eff m a xs (\v => xs)) where
19+ (>>=) = Effects.(>>=)
20+
21+
libs/neweffects/Effect/Random.idrnew file+25
@@ -0,0 +1,25 @@
1+module Effect.Random
2+
3+import Effects
4+
5+data Random : Effect where
6+ getRandom : { Integer } Random Integer
7+ setSeed : Integer -> { Integer } Random ()
8+
9+using (m : Type -> Type)
10+ instance Handler Random m where
11+ handle seed getRandom k
12+ = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
13+ k seed' seed'
14+ handle seed (setSeed n) k = k () n
15+
16+RND : EFFECT
17+RND = MkEff Integer Random
18+
19+rndInt : Integer -> Integer -> { [RND] } Eff m Integer
20+rndInt lower upper = do v <- getRandom
21+ return (v `prim__sremBigInt` (upper - lower) + lower)
22+
23+srand : Integer -> { [RND] } Eff m ()
24+srand n = setSeed n
25+
libs/neweffects/Effect/Select.idrnew file+23
@@ -0,0 +1,23 @@
1+module Effect.Select
2+
3+import Effects
4+
5+data Selection : Effect where
6+ Select : List a -> { () } Selection a
7+
8+instance Handler Selection Maybe where
9+ handle _ (Select xs) k = tryAll xs where
10+ tryAll [] = Nothing
11+ tryAll (x :: xs) = case k x () of
12+ Nothing => tryAll xs
13+ Just v => Just v
14+
15+instance Handler Selection List where
16+ handle r (Select xs) k = concatMap (\x => k x r) xs
17+
18+SELECT : EFFECT
19+SELECT = MkEff () Selection
20+
21+select : List a -> { [SELECT] } Eff m a
22+select xs = Select xs
23+
libs/neweffects/Effect/State.idrnew file+40
@@ -0,0 +1,40 @@
1+module Effect.State
2+
3+import Effects
4+
5+%access public
6+
7+data State : Effect where
8+ Get : { a } State a
9+ Put : b -> { a ==> b } State ()
10+
11+using (m : Type -> Type)
12+ instance Handler State m where
13+ handle st Get k = k st st
14+ handle st (Put n) k = k () n
15+
16+STATE : Type -> EFFECT
17+STATE t = MkEff t State
18+
19+get : { [STATE x] } Eff m x
20+get = Get
21+
22+put : x -> { [STATE x] } Eff m ()
23+put val = Put val
24+
25+putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
26+putM val = Put val
27+
28+update : (x -> x) -> { [STATE x] } Eff m ()
29+update f = put (f !get)
30+
31+updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff m ()
32+updateM f = putM (f !get)
33+
34+locally : x -> ({ [STATE x] } Eff m t) -> { [STATE y] } Eff m t
35+locally newst prog = do st <- get
36+ putM newst
37+ val <- prog
38+ putM st
39+ return val
40+
libs/neweffects/Effect/StdIO.idrnew file+63
@@ -0,0 +1,63 @@
1+module Effect.StdIO
2+
3+import Effects
4+import Control.IOExcept
5+
6+data StdIO : Effect where
7+ PutStr : String -> { () } StdIO ()
8+ GetStr : { () } StdIO String
9+
10+instance Handler StdIO IO where
11+ handle () (PutStr s) k = do putStr s; k () ()
12+ handle () GetStr k = do x <- getLine; k x ()
13+
14+{-
15+instance Handler StdIO (IOExcept a) where
16+ handle () (PutStr s) k = do ioe_lift (putStr s); k () ()
17+ handle () GetStr k = do x <- ioe_lift getLine; k () x
18+
19+-- Handle effects in a pure way, for simulating IO for unit testing/proof
20+
21+data IOStream a = MkStream (List String -> (a, List String))
22+
23+instance Handler StdIO IOStream where
24+ handle () (PutStr s) k
25+ = MkStream (\x => case k () () of
26+ MkStream f => let (res, str) = f x in
27+ (res, s :: str))
28+ handle {a} () GetStr k
29+ = MkStream (\x => case x of
30+ [] => cont "" []
31+ (t :: ts) => cont t ts)
32+ where
33+ cont : String -> List String -> (a, List String)
34+ cont t ts = case k () t of
35+ MkStream f => f ts
36+
37+-}
38+
39+--- The Effect and associated functions
40+
41+STDIO : EFFECT
42+STDIO = MkEff () StdIO
43+
44+putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
45+putStr s = PutStr s
46+
47+putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
48+putStrLn s = putStr (s ++ "\n")
49+
50+getStr : Handler StdIO e => { [STDIO] } Eff e String
51+getStr = GetStr
52+
53+-- mkStrFn : Env IOStream xs ->
54+-- Eff IOStream xs a ->
55+-- List String -> (a, List String)
56+-- mkStrFn {a} env p input = case mkStrFn' of
57+-- MkStream f => f input
58+-- where injStream : a -> IOStream a
59+-- injStream v = MkStream (\x => (v, []))
60+-- mkStrFn' : IOStream a
61+-- mkStrFn' = runWith injStream env p
62+--
63+--
libs/neweffects/Effects.idrnew file+271
@@ -0,0 +1,271 @@
1+module Effects
2+
3+import Language.Reflection
4+import Control.Catchable
5+import Effect.Default
6+
7+%access public
8+
9+---- Effects
10+
11+Effect : Type
12+Effect = (x : Type) -> Type -> (x -> Type) -> Type
13+
14+data EFFECT : Type where
15+ MkEff : Type -> Effect -> EFFECT
16+
17+class Handler (e : Effect) (m : Type -> Type) where
18+ handle : res -> (eff : e t res resk) ->
19+ ((x : t) -> resk x -> m a) -> m a
20+
21+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
22+-- up to a small number of parameters...)
23+
24+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
25+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
26+
27+---- Properties and proof construction
28+
29+using (xs : List a, ys : List a)
30+ data SubList : List a -> List a -> Type where
31+ SubNil : SubList {a} [] []
32+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
33+ Drop : SubList xs ys -> SubList xs (x :: ys)
34+
35+ subListId : SubList xs xs
36+ subListId {xs = Nil} = SubNil
37+ subListId {xs = x :: xs} = Keep subListId
38+
39+namespace Env
40+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
41+ Nil : Env m Nil
42+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
43+
44+data EffElem : Effect -> Type ->
45+ List EFFECT -> Type where
46+ Here : EffElem x a (MkEff a x :: xs)
47+ There : EffElem x a xs -> EffElem x a (y :: xs)
48+
49+-- make an environment corresponding to a sub-list
50+dropEnv : Env m ys -> SubList xs ys -> Env m xs
51+dropEnv [] SubNil = []
52+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
53+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
54+
55+updateWith : (ys' : List a) -> (xs : List a) ->
56+ SubList ys xs -> List a
57+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
58+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
59+updateWith [] [] SubNil = []
60+updateWith (y :: ys) [] SubNil = y :: ys
61+updateWith [] (x :: xs) (Keep rest) = []
62+
63+-- put things back, replacing old with new in the sub-environment
64+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
65+ Env m xs -> Env m (updateWith ys' xs prf)
66+rebuildEnv [] SubNil env = env
67+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
68+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
69+rebuildEnv (x :: xs) SubNil [] = x :: xs
70+
71+---- The Effect EDSL itself ----
72+
73+-- some proof automation
74+
75+%reflection
76+reflectListEffElem : List a -> Tactic
77+reflectListEffElem [] = Refine "Here" `Seq` Solve
78+reflectListEffElem (x :: xs)
79+ = Try (Refine "Here" `Seq` Solve)
80+ (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))
81+-- TMP HACK! FIXME!
82+-- The evaluator needs a 'function case' to know its a reflection function
83+-- until we propagate that information! Without this, the _ case won't get
84+-- matched.
85+reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve
86+reflectListEffElem _ = Refine "Here" `Seq` Solve
87+
88+%reflection
89+reflectSubList : List a -> Tactic
90+reflectSubList [] = Refine "subListId" `Seq` Solve
91+reflectSubList (x :: xs)
92+ = Try (Refine "subListId" `Seq` Solve)
93+ (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
94+ (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))
95+reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
96+reflectSubList _ = Refine "subListId" `Seq` Solve
97+
98+%reflection
99+reflectEff : (P : Type) -> Tactic
100+reflectEff (EffElem m a xs)
101+ = reflectListEffElem xs `Seq` Solve
102+reflectEff (SubList xs ys)
103+ = reflectSubList ys `Seq` Solve
104+
105+updateResTy : (val : t) ->
106+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
107+ List EFFECT
108+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
109+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
110+
111+-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
112+-- List EFFECT
113+-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
114+-- updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
115+
116+infix 5 :::, :-, :=
117+
118+data LRes : lbl -> Type -> Type where
119+ (:=) : (x : lbl) -> res -> LRes x res
120+
121+(:::) : lbl -> EFFECT -> EFFECT
122+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
123+
124+using (lbl : Type)
125+ instance Default a => Default (LRes lbl a) where
126+ default = lbl := default
127+
128+private
129+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
130+unlabel {m} {x = MkEff a eff} [l := v] = [v]
131+
132+private
133+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
134+relabel {xs = []} l [] = []
135+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
136+
137+-- the language of Effects
138+
139+data Eff : (m : Type -> Type) ->
140+ (x : Type) ->
141+ List EFFECT -> (x -> List EFFECT) -> Type where
142+ value : a -> Eff m a xs (\v => xs)
143+ ebind : Eff m a xs xs' ->
144+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
145+ effect : (prf : EffElem e a xs) ->
146+ (eff : e t a b) ->
147+ Eff m t xs (\v => updateResTy v xs prf eff)
148+
149+ lift : (prf : SubList ys xs) ->
150+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
151+ new : Handler e m =>
152+ res ->
153+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
154+ Eff m a xs (\v => xs')
155+ catch : Catchable m err =>
156+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->
157+ Eff m a xs xs'
158+
159+ (:-) : (l : ty) ->
160+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
161+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))
162+
163+(>>=) : Eff m a xs xs' ->
164+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
165+(>>=) = ebind
166+
167+implicit
168+lift' : Eff m t ys ys' ->
169+ {default tactics { byReflection reflectEff; }
170+ prf : SubList ys xs} ->
171+ Eff m t xs (\v => updateWith (ys' v) xs prf)
172+lift' e {prf} = lift prf e
173+
174+implicit
175+effect' : {a, b: _} -> {e : Effect} ->
176+ (eff : e t a b) ->
177+ {default tactics { byReflection reflectEff; }
178+ prf : EffElem e a xs} ->
179+ Eff m t xs (\v => updateResTy v xs prf eff)
180+effect' e {prf} = effect prf e
181+
182+return : a -> Eff m a xs (\v => xs)
183+return x = value x
184+
185+-- for idiom brackets
186+
187+infixl 2 <$>
188+
189+pure : a -> Eff m a xs (\v => xs)
190+pure = value
191+
192+(<$>) : Eff m (a -> b) xs (\v => xs) ->
193+ Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
194+(<$>) prog v = do fn <- prog
195+ arg <- v
196+ return (fn arg)
197+
198+-- an interpreter
199+
200+private
201+execEff : Env m xs -> (p : EffElem e res xs) ->
202+ (eff : e a res resk) ->
203+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
204+execEff (val :: env) Here eff' k
205+ = handle val eff' (\v, res => k v (res :: env))
206+execEff (val :: env) (There p) eff k
207+ = execEff env p eff (\v, env' => k v (val :: env'))
208+
209+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
210+-- updates can be propagated even through failing computations?
211+
212+eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
213+eff env (value x) k = k x env
214+eff env (prog `ebind` c) k
215+ = eff env prog (\p', env' => eff env' (c p') k)
216+eff env (effect prf effP) k = execEff env prf effP k
217+eff env (lift prf effP) k
218+ = let env' = dropEnv env prf in
219+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
220+eff env (new r prog) k
221+ = let env' = r :: env in
222+ eff env' prog (\p' => \ (v :: envk) => k p' envk)
223+eff env (catch prog handler) k
224+ = catch (eff env prog k)
225+ (\e => eff env (handler e) k)
226+-- FIXME:
227+-- xs is needed explicitly because otherwise the pattern binding for
228+-- 'l' appears too late. Solution seems to be to reorder patterns at the
229+-- end so that everything is in scope when it needs to be.
230+eff {xs = [l ::: x]} env (l :- prog) k
231+ = let env' = unlabel env in
232+ eff env' prog (\p', envk => k p' (relabel l envk))
233+
234+run : Applicative m => Env m xs -> Eff m a xs xs' -> m a
235+run env prog = eff env prog (\r, env => pure r)
236+
237+-- yuck :)
238+syntax MkDefaultEnv = (| [], [default], [default, default],
239+ [default, default, default],
240+ [default, default, default, default],
241+ [default, default, default, default, default],
242+ [default, default, default, default, default, default],
243+ [default, default, default, default, default, default, default],
244+ [default, default, default, default, default, default, default, default] |)
245+
246+run' : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
247+run' {env} prog = eff env prog (\r, env => pure r)
248+
249+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
250+ m (x : a ** Env m (xs' x))
251+runEnv env prog = eff env prog (\r, env => pure (r ** env))
252+
253+runPure : Env id xs -> Eff id a xs xs' -> a
254+runPure env prog = eff env prog (\r, env => r)
255+
256+-- runPureEnv : Env id xs -> Eff id a xs xs' -> (x : a ** Env id (xs' x))
257+-- runPureEnv env prog = eff env prog (%unifyLog (\r, env => id (r ** env)))
258+
259+runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
260+runWith inj env prog = eff env prog (\r, env => inj r)
261+
262+-- some higher order things
263+
264+mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
265+mapE f [] = pure []
266+mapE f (x :: xs) = [| f x :: mapE f xs |]
267+
268+when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
269+when True e = e
270+when False e = pure ()
271+
libs/neweffects/Makefilenew file+14
@@ -0,0 +1,14 @@
1+IDRIS := idris
2+
3+build:
4+ $(IDRIS) --build effects.ipkg
5+
6+clean:
7+ $(IDRIS) --clean effects.ipkg
8+
9+install:
10+ $(IDRIS) --install effects.ipkg
11+
12+rebuild: clean build
13+
14+.PHONY: build clean install rebuild
libs/neweffects/neweffects.ipkgnew file+8
@@ -0,0 +1,8 @@
1+package neweffects
2+
3+modules = Effects, Effect.Default,
4+
5+ Effect.Exception, Effect.File, Effect.State,
6+ Effect.Random, Effect.StdIO, Effect.Select,
7+ Effect.Memory
8+