git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/ST/Intro.idr
75 lines 2.8 kB history raw
1import Control.ST
2import Data.Vect
4-- Basic state
6-- increment : (x : Var) -> STrans m () [x ::: State Int]
7-- (const [x ::: State Int])
8increment : (x : Var) -> ST m () [x ::: State Int]
9increment x = do num <- read x
10 write x (num + 1)
12-- makeAndIncrement : Int -> STrans m Int [] (const [])
13makeAndIncrement : Int -> ST m Int []
14makeAndIncrement init = do var <- new init
15 increment var
16 x <- read var
17 delete var
18 pure x
20ioMakeAndIncrementBad : STrans IO () [] (const [])
21ioMakeAndIncrementBad
22 = do lift $ putStr "Enter a number: "
23 init <- lift $ getLine
24 var <- new (cast init)
25 lift $ putStrLn ("var = " ++ show !(read var))
26 increment var
27 lift $ putStrLn ("var = " ++ show !(read var))
28 delete var
30ioMakeAndIncrement : ConsoleIO io => STrans io () [] (const [])
31ioMakeAndIncrement
32 = do putStr "Enter a number: "
33 init <- getStr
34 var <- new (cast init)
35 putStrLn ("var = " ++ show !(read var))
36 increment var
37 putStrLn ("var = " ++ show !(read var))
38 delete var
40-- Dependent state
42-- addElement : (vec : Var) -> (item : a) ->
43-- STrans m () [vec ::: State (Vect n a)]
44-- (const [vec ::: State (Vect (S n) a)])
45addElement : (vec : Var) -> (item : a) ->
46 ST m () [vec ::: State (Vect n a) :-> State (Vect (S n) a)]
47addElement vec item = do xs <- read vec
48 write vec (item :: xs)
50addElement' : (vec : Var) -> (item : a) ->
51 STrans m () [vec ::: State (Vect n a)]
52 (const [vec ::: State (Vect (S n) a)])
53addElement' vec item = update vec (item ::)
55-- readAndAdd : ConsoleIO io => (vec : Var) ->
56-- STrans io Bool [vec ::: State (Vect n Integer)]
57-- (\res => [vec ::: State (if res then Vect (S n) Integer
58-- else Vect n Integer)])
59readAndAdd : ConsoleIO io => (vec : Var) ->
60 ST io Bool
61 [vec ::: State (Vect n Integer) :->
62 \res => State (if res then Vect (S n) Integer
63 else Vect n Integer)]
64readAndAdd vec = do putStr "Enter a number: "
65 num <- getStr
66 if all isDigit (unpack num)
67 then returning True (update vec ((cast num) ::))
68 else returning False (pure ())
70-- newState : STrans m Var [] (\lbl => [lbl ::: State Int])
71newState : ST m Var [add (State Int)]
73-- removeState : (lbl : Var) -> STrans m () [lbl ::: State Int] (const [])
74removeState : (lbl : Var) -> ST m () [remove lbl (State Int)]