git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/samples/ST/Login.idr
55 lines 1.7 kB history raw
1import Control.ST
3data Access = LoggedOut | LoggedIn
4data LoginResult = OK | BadPassword
6interface DataStore (m : Type -> Type) where
7 data Store : Access -> Type
9 connect : ST m Var [add (Store LoggedOut)]
10 disconnect : (store : Var) -> ST m () [remove store (Store LoggedOut)]
12 readSecret : (store : Var) -> ST m String [store ::: Store LoggedIn]
13 login : (store : Var) ->
14 ST m LoginResult [store ::: Store LoggedOut :->
15 (\res => Store (case res of
16 OK => LoggedIn
17 BadPassword => LoggedOut))]
18 logout : (store : Var) ->
19 ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
21getData : (ConsoleIO m, DataStore m) => ST m () []
22getData = do st <- connect
23 OK <- login st
24 | BadPassword => do putStrLn "Failure"
25 disconnect st
26 secret <- readSecret st
27 putStrLn ("Secret is: " ++ show secret)
28 logout st
29 disconnect st
31-- badGet : DataStore m => ST m () []
32-- badGet = do st <- connect
33-- secret <- readSecret st
34-- disconnect st
36DataStore IO where
37 Store x = State String -- represents secret data
39 connect = do store <- new "Secret Data"
40 pure store
42 disconnect store = delete store
44 readSecret store = read store
46 login store = do putStr "Enter password: "
47 p <- getStr
48 if p == "Mornington Crescent"
49 then pure OK
50 else pure BadPassword
51 logout store = pure ()
53main : IO ()
54main = run getData