git.iko.soy/Idris-dev
on master help sign in
Idris-dev/samples/ST/LoginCount.idr
77 lines 2.6 kB history raw
1import Control.ST
2import Control.ST.ImplicitCall
4data Access = LoggedOut | LoggedIn
5data LoginResult = OK | BadPassword
7interface DataStore (m : Type -> Type) where
8 data Store : Access -> Type
10 connect : ST m Var [add (Store LoggedOut)]
11 disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
13 readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
14 login : (store : Var) ->
15 ST m LoginResult [store ::: Store LoggedOut :->
16 (\res => Store (case res of
17 OK => LoggedIn
18 BadPassword => LoggedOut))]
19 logout : (store : Var) ->
20 ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
22getData : (ConsoleIO m, DataStore m) =>
23 (failcount : Var) -> ST m () [failcount ::: State Integer]
24getData failcount
25 = do st <- call connect
26 OK <- login st
27 | BadPassword => do putStrLn "Failure"
28 fc <- read failcount
29 write failcount (fc + 1)
30 putStrLn ("Number of failures: " ++ show (fc + 1))
31 disconnect st
32 getData failcount
33 secret <- readSecret st
34 putStrLn ("Secret is: " ++ show secret)
35 logout st
36 disconnect st
37 getData failcount
39getData2 : (ConsoleIO m, DataStore m) =>
40 (st, failcount : Var) ->
41 ST m () [st ::: Store {m} LoggedOut, failcount ::: State Integer]
42getData2 st failcount
43 = do OK <- login st
44 | BadPassword => do putStrLn "Failure"
45 fc <- read failcount
46 write failcount (fc + 1)
47 putStrLn ("Number of failures: " ++ show (fc + 1))
48 getData2 st failcount
49 secret <- readSecret st
50 putStrLn ("Secret is: " ++ show secret)
51 logout st
52 getData2 st failcount
54DataStore IO where
55 Store x = State String -- represents secret data
57 connect = do store <- new "Secret Data"
58 pure store
60 disconnect store = delete store
62 readSecret store = read store
64 login store = do putStr "Enter password: "
65 p <- getStr
66 if p == "Mornington Crescent"
67 then pure OK
68 else pure BadPassword
69 logout store = pure ()
71main : IO ()
72main = run (do fc <- new 0
73 st <- connect
74 getData2 st fc
75 disconnect st
76 delete fc)