-
Notifications
You must be signed in to change notification settings - Fork 5
/
Main.idr
52 lines (41 loc) · 1.2 KB
/
Main.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
module Main
import Erlang
%default total
readFile : String -> IO (Maybe String)
readFile filename = do
Right result <- erlCall "file" "read_file" [filename]
| Left _ => do
putStrLn "Failed to read file"
pure Nothing
let Right (MkTuple2 ok content) = erlDecode
(tuple2 (exact (MkAtom "ok")) string)
result
| Left _ => do
putStrLn "Failed to decode"
pure Nothing
pure $ Just content
main : IO ()
main = do
Just content <- readFile "secret.txt"
| Nothing => putStrLn "Failed to read content"
putStrLn content
examplePerson : ErlAnyMap
examplePerson = insert "loves_idris" (MkAtom "true") $ insert "age" 34 $ insert "name" "Christian" empty
record Person where
constructor MkPerson
name : String
age : Integer
lovesIdris : Bool
Show Person where
show (MkPerson name age lovesIdris) = "MkPerson \{show name} \{show age} \{show lovesIdris}"
main2 : IO ()
main2 = do
let Just [name, age, lovesIdris] = erlDecodeMay
(mapEntries
[ "name" .= string
, "age" .= integer
, "loves_idris" .= bool
])
examplePerson
| Nothing => putStrLn "Unable to decode person"
printLn (MkPerson name age lovesIdris)