First working version of dependent effects

Effect/Exception.idr

@@ -0,0 +1,40 @@
+module Effect.Exception
+
+import Effects
+import System
+import Control.IOExcept
+
+data Exception : Type -> Effect where 
+     Raise : a -> Exception a b () (\v => ())
+
+instance Handler (Exception a) Maybe where
+     handle _ (Raise e) k = Nothing
+
+instance Show a => Handler (Exception a) IO where
+     handle _ (Raise e) k = do print e
+                               believe_me (exit 1)
+
+instance Handler (Exception a) (IOExcept a) where
+     handle _ (Raise e) k = ioM (return (Left e))
+
+instance Handler (Exception a) (Either a) where
+     handle _ (Raise e) k = Left e
+
+EXCEPTION : Type -> EFFECT
+EXCEPTION t = MkEff () (Exception t)
+
+raise : a -> Eff m b [EXCEPTION a]
+raise err = Raise err
+
+
+
+
+
+
+
+-- TODO: Catching exceptions mid program?
+-- probably need to invoke a new interpreter
+
+-- possibly add a 'handle' to the Eff language so that an alternative
+-- handler can be introduced mid interpretation?
+

Effect/File.idr

@@ -0,0 +1,61 @@
+module Effect.File
+
+import Effects
+import Control.IOExcept
+
+data OpenFile : Mode -> Type where
+     FH : File -> OpenFile m
+
+openOK : Mode -> Bool -> Type
+openOK m True = OpenFile m
+openOK m False = ()
+
+data FileIO : Effect where
+     Open  : String -> (m : Mode) -> 
+             FileIO Bool () (openOK m)
+     Close : FileIO () (OpenFile m) (\v => ())
+
+     ReadLine  :           FileIO String (OpenFile Read)  (\v => (OpenFile Read))
+     WriteLine : String -> FileIO ()     (OpenFile Write) (\v => (OpenFile Write))
+     EOF       :           FileIO Bool   (OpenFile Read)  (\v => (OpenFile Read))
+
+
+instance Handler FileIO IO where
+    handle () (Open fname m) k = do h <- openFile fname m
+                                    valid <- validFile h
+                                    case valid of
+                                         True => k True (FH h)
+                                         False => k False ()
+    handle (FH h) Close      k = do closeFile h
+                                    k () ()
+    handle (FH h) ReadLine        k = do str <- fread h
+                                         k str (FH h)
+    handle (FH h) (WriteLine str) k = do fwrite h str
+                                         k () (FH h)
+    handle (FH h) EOF             k = do e <- feof h
+                                         k e (FH h)
+
+FILE_IO : Type -> EFFECT
+FILE_IO t = MkEff t FileIO
+
+open : Handler FileIO e =>
+       String -> (m : Mode) -> EffM e Bool [FILE_IO ()]
+                                           (\v => [FILE_IO (openOK m v)])
+open f m = Open f m
+
+close : Handler FileIO e =>
+        EffM e () [FILE_IO (OpenFile m)] (\v => [FILE_IO ()])
+close = Close
+
+readLine : Handler FileIO e => Eff e String [FILE_IO (OpenFile Read)]
+readLine = ReadLine
+
+writeLine : Handler FileIO e => String -> Eff e () [FILE_IO (OpenFile Write)]
+writeLine str = WriteLine str
+
+eof : Handler FileIO e => Eff e Bool [FILE_IO (OpenFile Read)]
+eof = EOF
+
+
+
+

Effect/Memory.idr

@@ -0,0 +1,175 @@
+module Effect.Memory
+
+import Effects
+import Control.IOExcept
+
+%access public
+
+abstract
+data MemoryChunk : Nat -> Nat -> Type where
+     CH : Ptr -> MemoryChunk size initialized
+
+abstract
+data RawMemory : Effect where
+     Allocate   : (n : Nat) ->
+                  RawMemory () () (\v => MemoryChunk n 0)
+     Free       : RawMemory () (MemoryChunk n i) (\v => ())
+     Initialize : Bits8 ->
+                  (size : Nat) ->
+                  so (i + size <= n) ->
+                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
+     Peek       : (offset : Nat) ->
+                  (size : Nat) ->
+                  so (offset + size <= i) ->
+                  RawMemory (Vect size Bits8)
+                            (MemoryChunk n i) (\v => MemoryChunk n i) 
+     Poke       :  (offset : Nat) ->
+                  (Vect size Bits8) ->
+                  so (offset <= i && offset + size <= n) ->
+                  RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size))) 
+     Move       : (src : MemoryChunk src_size src_init) ->
+                  (dst_offset : Nat) ->
+                  (src_offset : Nat) ->
+                  (size : Nat) ->
+                  so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
+                  so (src_offset + size <= src_init) ->
+                  RawMemory () (MemoryChunk dst_size dst_init)
+                            (\v => MemoryChunk dst_size (max dst_init (dst_offset + size))) 
+     GetRawPtr  : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i) 
+
+private
+do_malloc : Nat -> IOExcept String Ptr
+do_malloc size with (fromInteger (cast size) == size)
+  | True  = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt] FPtr) (fromInteger $ cast size)
+               fail  <- ioe_lift $ nullPtr ptr
+               if fail then ioe_fail "Cannot allocate memory"
+               else return ptr
+  | False = ioe_fail "The target architecture does not support adressing enough memory"
+
+private
+do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()
+do_memset ptr offset c size
+  = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)
+              ptr (fromInteger $ cast offset) c (fromInteger $ cast size)
+
+private
+do_free : Ptr -> IO ()
+do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr
+
+private
+do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()
+do_memmove dest src dest_offset src_offset size
+  = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt, FInt, FInt] FUnit)
+              dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)
+
+private
+do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)
+do_peek _   _       Z = return (Prelude.Vect.Nil)
+do_peek ptr offset (S n)
+  = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
+       bs <- do_peek ptr (S offset) n
+       Prelude.Monad.return (Prelude.Vect.(::) b bs)
+
+private
+do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()
+do_poke _   _      []     = return ()
+do_poke ptr offset (b::bs)
+  = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b
+       do_poke ptr (S offset) bs
+
+instance Handler RawMemory (IOExcept String) where
+  handle () (Allocate n) k
+    = do ptr <- do_malloc n
+         k () (CH ptr)
+  handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k
+    = ioe_lift (do_memset ptr offset c size) $> k () (CH ptr)
+  handle (CH ptr) (Free) k
+    = ioe_lift (do_free ptr) $> k () ()
+  handle (CH ptr) (Peek offset size _) k
+    = do res <- ioe_lift (do_peek ptr offset size)
+         k res (CH ptr)
+  handle (CH ptr) (Poke offset content _) k
+    = do ioe_lift (do_poke ptr offset content)
+         k () (CH ptr)
+  handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
+    = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
+         k () (CH dest_ptr)
+  handle chunk (GetRawPtr) k
+    = k chunk chunk
+
+RAW_MEMORY : Type -> EFFECT
+RAW_MEMORY t = MkEff t RawMemory
+
+allocate : (n : Nat) -> 
+           EffM m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
+allocate size = Allocate size
+
+initialize : {i : Nat} ->
+             {n : Nat} ->
+             Bits8 ->
+             (size : Nat) ->
+             so (i + size <= n) ->
+             EffM m () [RAW_MEMORY (MemoryChunk n i)] 
+                       (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
+initialize c size prf = Initialize c size prf
+
+free : EffM m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
+free = Free
+
+peek : {i : Nat} ->
+       (offset : Nat) ->
+       (size : Nat) ->
+       so (offset + size <= i) ->
+       Eff m (Vect size Bits8) [RAW_MEMORY (MemoryChunk n i)]
+peek offset size prf = Peek offset size prf
+
+poke : {n : Nat} ->
+       {i : Nat} ->
+       (offset : Nat) ->
+       Vect size Bits8 ->
+       so (offset <= i && offset + size <= n) ->
+       EffM m () [RAW_MEMORY (MemoryChunk n i)] 
+              (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
+poke offset content prf = Poke offset content prf
+
+private
+getRawPtr : Eff m (MemoryChunk n i) [RAW_MEMORY (MemoryChunk n i)] 
+getRawPtr = GetRawPtr
+
+private
+move' : {dst_size : Nat} ->
+        {dst_init : Nat} ->
+        {src_init : Nat} ->
+        (src_ptr : MemoryChunk src_size src_init) ->
+        (dst_offset : Nat) ->
+        (src_offset : Nat) ->
+        (size : Nat) ->
+        so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
+        so (src_offset + size <= src_init) ->
+        EffM m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
+               (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
+move' src_ptr dst_offset src_offset size dst_bounds src_bounds
+  = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
+
+data MoveDescriptor = Dst | Src
+
+move : {dst_size : Nat} ->
+       {dst_init : Nat} ->
+       {src_size : Nat} ->
+       {src_init : Nat} ->
+       (dst_offset : Nat) ->
+       (src_offset : Nat) ->
+       (size : Nat) ->
+       so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
+       so (src_offset + size <= src_init) ->
+       EffM m ()
+              [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
+              , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
+              (\v =>
+                [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
+                , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
+move dst_offset src_offset size dst_bounds src_bounds
+  = do src_ptr <- Src :- getRawPtr
+       Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
+       return () 
+

Effect/Monad.idr

@@ -0,0 +1,21 @@
+module Effect.Monad
+
+import Effects
+
+-- Eff is a monad too, so we can happily use it in a monad transformer.
+
+using (xs : List EFFECT, m : Type -> Type)
+  instance Functor (\a => EffM m a xs (\v => xs)) where
+    map f prog = do t <- prog
+                    value (f t)
+
+  instance Applicative (\a => EffM m a xs (\v => xs)) where
+    pure = value
+    (<$>) f a = do f' <- f
+                   a' <- a
+                   value (f' a')
+
+  instance Monad (\a => Eff m a xs (\v => xs)) where
+    (>>=) = Effects.(>>=)
+
+

Effect/Random.idr

@@ -0,0 +1,25 @@
+module Effect.Random
+
+import Effects
+
+data Random : Effect where 
+     getRandom : Random Integer Integer (\v => Integer)
+     setSeed   : Integer -> Random () Integer (\v => Integer)
+
+using (m : Type -> Type)
+  instance Handler Random m where
+     handle seed getRandom k
+              = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
+                    k seed' seed'
+     handle seed (setSeed n) k = k () n
+
+RND : EFFECT
+RND = MkEff Integer Random
+
+rndInt : Integer -> Integer -> Eff m Integer [RND]
+rndInt lower upper = do v <- getRandom
+                        return (v `prim__sremBigInt` (upper - lower) + lower)
+
+srand : Integer -> Eff m () [RND]
+srand n = setSeed n
+

Effect/Select.idr

@@ -0,0 +1,23 @@
+module Effect.Select
+
+import Effects
+
+data Selection : Effect where
+     Select : List a -> Selection a () (\v => ())
+
+instance Handler Selection Maybe where
+     handle _ (Select xs) k = tryAll xs where
+         tryAll [] = Nothing
+         tryAll (x :: xs) = case k x () of
+                                 Nothing => tryAll xs
+                                 Just v => Just v
+
+instance Handler Selection List where
+     handle r (Select xs) k = concatMap (\x => k x r) xs
+
+SELECT : EFFECT
+SELECT = MkEff () Selection
+
+select : List a -> Eff m a [SELECT]
+select xs = Select xs
+

Effect/State.idr

@@ -0,0 +1,40 @@
+module Effect.State
+
+import Effects
+
+%access public
+
+data State : Effect where
+     Get :      State a a (\v => a)
+     Put : b -> State () a (\v => b)
+
+using (m : Type -> Type)
+  instance Handler State m where
+     handle st Get     k = k st st
+     handle st (Put n) k = k () n
+
+STATE : Type -> EFFECT
+STATE t = MkEff t State
+
+get : Eff m x [STATE x]
+get = Get
+
+put : x -> Eff m () [STATE x]
+put val = Put val
+
+putM : y -> EffM m () [STATE x] (\v => [STATE y])
+putM val = Put val
+
+update : (x -> x) -> Eff m () [STATE x]
+update f = put (f !get)
+
+updateM : (x -> y) -> EffM m () [STATE x] (\v => [STATE y])
+updateM f = putM (f !get)
+
+locally : x -> Eff m t [STATE x] -> Eff m t [STATE y]
+locally newst prog = do st <- get
+                        putM newst
+                        val <- prog
+                        putM st
+                        return val
+