Add Effects examples

Effects/Expr.idr

@@ -0,0 +1,41 @@
+module Main
+
+import Effect.State
+import Effect.Exception
+import Effect.Random
+import Effect.StdIO
+
+data Expr = Var String
+          | Val Integer
+          | Add Expr Expr
+          | Random Integer
+
+Env : Type
+Env = List (String, Integer)
+
+eval : Expr -> Eff IO [RND, EXCEPTION String, STDIO, STATE Env] Integer
+eval (Var x) 
+   = do vs <- get
+        case lookup x vs of
+             Nothing => raise ("No such variable " ++ x)
+             Just val => return val
+eval (Val x) = return x
+eval (Add l r) = do l' <- eval l
+                    r' <- eval r
+                    return (l' + r')
+eval (Random upper) = do val <- rndInt 0 upper
+                         putStrLn (show val)
+                         return val
+
+testExpr : Expr
+testExpr = Add (Add (Var "foo") (Val 42)) (Random 100)
+
+runEval : List (String, Integer) -> Expr -> IO Integer
+runEval args expr = run [1234567, (), (), args] (eval expr)
+
+main : IO ()
+main = do putStr "Number: "
+          x <- getLine
+          val <- runEval [("foo", cast x)] testExpr
+          putStrLn $ "Answer: " ++ show val
+

Effects/FileTest.idr

@@ -0,0 +1,34 @@
+module Main
+
+import Effect.File
+import Effect.State
+import Effect.StdIO
+import Control.IOExcept
+
+data FName = Count | NotCount
+
+FileIO : Type -> Type -> Type
+FileIO st t
+   = Eff IO [FILE_IO st, STDIO, Count ::: STATE Int] t
+
+readFile : FileIO (OpenFile Read) (List String)
+readFile = readAcc [] where
+    readAcc : List String -> FileIO (OpenFile Read) (List String)
+    readAcc acc = do e <- eof
+                     if (not e)
+                        then do str <- readLine
+                                Count :- put (!(Count :- get) + 1)
+                                readAcc (str :: acc)
+                        else return (reverse acc)
+
+testFile : FileIO () ()
+testFile = do open "testFile" Read
+              if_valid then do putStrLn (show !readFile)
+                               close
+                               putStrLn (show !(Count :- get))
+                 else putStrLn ("Error!")
+
+main : IO ()
+main = run [(), (), Count := 0] testFile
+
+

Effects/Queens.idr

@@ -0,0 +1,28 @@
+module Main
+
+import Effect.Select
+
+no_attack : (Int, Int) -> (Int, Int) -> Bool
+no_attack (x, y) (x', y') 
+   = x /= x' && y /= y' && abs (x - x') /= abs (y - y')
+
+rowsIn : Int -> List (Int, Int) -> List Int
+rowsIn col qs = [ x | x <- [1..8], all (no_attack (x, col)) qs ]
+
+addQueens : Int -> List (Int, Int) -> Eff m [SELECT] (List (Int, Int)) 
+addQueens 0   qs = return qs
+addQueens col qs = do row <- select (rowsIn col qs)
+                      addQueens (col - 1) ((row, col) :: qs)
+
+getQueens : Maybe (List (Int, Int))
+getQueens = run [()] (addQueens 8 [])
+
+main : IO ()
+main = do let qs = getQueens
+          putStrLn ("Solution:\n" ++ show qs)
+
+--           let num = the Integer (cast (length qs))
+--           putStrLn (show num ++ " solutions:\n" ++ showAll qs)
+--     where showAll [] = ""
+--           showAll (x :: xs) = show x ++ "\n" ++ showAll xs 
+

Effects/README

@@ -0,0 +1,3 @@
+To load these into idris, use:
+
+$ idris [filename].idr -p effects

Effects/TreeLabel.idr

@@ -0,0 +1,54 @@
+module Main
+
+import Effect.State
+
+data Tree a = Leaf 
+            | Node (Tree a) a (Tree a)
+
+flattenTree : Tree a -> List a
+flattenTree Leaf = []
+flattenTree (Node l x r) = flattenTree l ++ (x :: flattenTree r)
+
+testTree : Tree String
+testTree = Node (Node Leaf "One" (Node Leaf "Two" Leaf))
+                "Three"
+                (Node (Node Leaf "Four" Leaf) "Five" Leaf)
+
+data Tag : Type where
+data Leaves : Type where
+
+label : Tree a -> Eff m  [Leaves ::: STATE Int,
+                          Tag ::: STATE Int] (Tree (Int, a))
+label Leaf = do Leaves :- update (+1)
+                return Leaf
+label (Node l x r) = do l' <- label l 
+                        lbl <- Tag :- get
+                        Tag :- put (lbl + 1)
+                        r' <- label r
+                        return (Node l' (lbl, x) r')
+
+main : IO ()
+main = do let ([Leaves := l, _], x) = runPureEnv [Leaves := 0, Tag := 1] (label testTree)
+          print (l, flattenTree x)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+{-
+label Leaf = return Leaf
+label (Node l x r) = do l' <- label l 
+                        lbl <- get
+                        put (lbl + 1)
+                        r' <- label r
+                        return (Node l' (lbl, x) r')
+-}

Effects/ioreason.idr

@@ -0,0 +1,29 @@
+module Main
+
+import Effect.StdIO
+import Effect.State
+
+instance Show () where
+    show () = "()"
+
+name : Handler StdIO e => Eff e [STDIO] ()
+name = do putStr "Name? "
+          n <- getStr
+          putStrLn ("Hello " ++ show n)
+
+echo : Handler StdIO e => Eff e [STDIO] ()
+echo = do n <- getStr
+          putStr (show n)
+
+streamName : List String -> ((), List String)
+streamName = mkStrFn [()] name
+
+streamEcho : List String -> ((), List String)
+streamEcho = mkStrFn [()] echo
+
+echoEchoes : (input : List String) -> streamEcho input = ((), input)
+echoEchoes [x] = ?ecase
+
+main : IO ()
+main = run [()] name
+

Effects/testfile

@@ -0,0 +1,3 @@
+Hello
+Code
+Mesh!

LICENSE

@@ -1,4 +1,5 @@
 Copyright (c) 2013, Edwin Brady
+    School of Computer Science, University of St Andrews
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification,

README.md

@@ -1,4 +1,4 @@
-idris-demos
+Idris demos
 ===========
 
 Collection of Idris tests and demonstration programs