0 | module Interactive.FS
 1 |
 2 | import Data.Container
 3 | import Data.Container.Morphism
 4 | import Data.Container.Kleene
 5 | import Data.Sum
 6 |
 7 | import Data.Sigma
 8 |
 9 | import System.File
10 |
11 | -- A file system example
12 | data OpenFile = MkOpen String
13 | data WriteFile = MkWrite String File
14 | data CloseFile = MkClose File
15 |
16 | -- filesystem monad
17 | FSMonad : Type -> Type
18 | FSMonad = IO . Either FileError
19 |
20 | Functor FSMonad where
21 |   map f = map (map f)
22 |
23 | Applicative FSMonad where
24 |   pure = pure . pure
25 |   x <*> y = do x' <- x
26 |                y' <- y
27 |                pure (x' <*> y')
28 |
29 | Monad FSMonad where
30 |   x >>= f = do x' <- x
31 |                r <- traverse f x'
32 |                pure (join r)
33 |
34 | OpenC : Container
35 | OpenC = OpenFile :- File
36 |
37 | WriteC : Container
38 | WriteC = WriteFile :- Unit
39 |
40 | CloseC : Container
41 | CloseC = CloseFile :- Unit
42 |
43 | -- interacting with the file system is a choice of those actions
44 | FileAPI : Container
45 | FileAPI = OpenC + WriteC + CloseC
46 |
47 | writeMany : F FSMonad (WriteC).º =%> CUnit
48 | writeMany = embed writeFS
49 |   where
50 |   writeFS : (x : StarShp WriteC) -> FSMonad (StarPos WriteC x)
51 |   writeFS Done = pure (pure StarU)
52 |   writeFS (More ((MkWrite content file) ## p2)) = do
53 |     putStrLn "writing `\{content}` to file"
54 |     Right () <- fPutStrLn {io = IO} file content
55 |     | Left err =>  putStrLn "error \{show err}" *> pure (Left err)
56 |     map (map (StarM ())) (writeFS (p2 ()))
57 |
58 | -- The only valid way to interact with the file system however is with
59 | -- this sequence of actions
60 | FileSession : Container
61 | FileSession = OpenC ○ (WriteC).º ○ CloseC
62 |
63 | testWrite : F FSMonad WriteC =%> CUnit
64 | testWrite = embed (\(MkWrite content fh) => fPutStr fh content)
65 |
66 | testOpen : F FSMonad OpenC =%> CUnit
67 | testOpen = embed (\(MkOpen filename) => openFile filename ReadWrite)
68 |
69 | testClose : F FSMonad CloseC =%> CUnit
70 | testClose = embed (\(MkClose fh) => map pure (closeFile fh))
71 |
72 | testFS : F FSMonad FileAPI =%> CUnit
73 | testFS = distrib_plus_3 {a = OpenC, b = WriteC, c = CloseC, f = FSMonad}
74 |       |> (testOpen + testWrite + testClose |> dia3)
75 |
76 |
77 | writeHello : (FileSession).req
78 | writeHello = ((MkOpen "append"
79 |              ## (\file => single (MkWrite "hello" file)))
80 |              ## (\val => MkClose val.π1))
81 |
82 | runSession : (FileSession).req -> IO Unit
83 | runSession p1
84 |   = let rr := runSequenceM3 p1 testOpen writeMany testClose
85 |                  {a = OpenC, b = (WriteC).º, c = CloseC, m = FSMonad}
86 |     in rr *> pure ()
87 |
88 | main : IO Unit
89 | main = runSession writeHello
90 |