From 1c7d44e837b923a975aca6cad493b468965cec30 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 30 Nov 2013 16:33:57 +0000 Subject: [PATCH] Add Effects examples --- Effects/Expr.idr | 41 ++++++++++++++++++++++++++++++++ Effects/FileTest.idr | 34 +++++++++++++++++++++++++++ Effects/Queens.idr | 28 ++++++++++++++++++++++ Effects/README | 3 +++ Effects/TreeLabel.idr | 54 +++++++++++++++++++++++++++++++++++++++++++ Effects/ioreason.idr | 29 +++++++++++++++++++++++ Effects/testfile | 3 +++ LICENSE | 1 + README.md | 2 +- 9 files changed, 194 insertions(+), 1 deletion(-) create mode 100644 Effects/Expr.idr create mode 100644 Effects/FileTest.idr create mode 100644 Effects/Queens.idr create mode 100644 Effects/README create mode 100644 Effects/TreeLabel.idr create mode 100644 Effects/ioreason.idr create mode 100644 Effects/testfile diff --git a/Effects/Expr.idr b/Effects/Expr.idr new file mode 100644 index 0000000..d0ecfe5 --- /dev/null +++ b/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 + diff --git a/Effects/FileTest.idr b/Effects/FileTest.idr new file mode 100644 index 0000000..853c546 --- /dev/null +++ b/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 + + diff --git a/Effects/Queens.idr b/Effects/Queens.idr new file mode 100644 index 0000000..deaadf9 --- /dev/null +++ b/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 + diff --git a/Effects/README b/Effects/README new file mode 100644 index 0000000..93072f5 --- /dev/null +++ b/Effects/README @@ -0,0 +1,3 @@ +To load these into idris, use: + +$ idris [filename].idr -p effects diff --git a/Effects/TreeLabel.idr b/Effects/TreeLabel.idr new file mode 100644 index 0000000..c201dd3 --- /dev/null +++ b/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') +-} diff --git a/Effects/ioreason.idr b/Effects/ioreason.idr new file mode 100644 index 0000000..b8aea32 --- /dev/null +++ b/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 + diff --git a/Effects/testfile b/Effects/testfile new file mode 100644 index 0000000..dec8efe --- /dev/null +++ b/Effects/testfile @@ -0,0 +1,3 @@ +Hello +Code +Mesh! diff --git a/LICENSE b/LICENSE index 6d5006e..7f58fce 100644 --- a/LICENSE +++ b/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, diff --git a/README.md b/README.md index 8b3dd1f..67a1a0a 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -idris-demos +Idris demos =========== Collection of Idris tests and demonstration programs