blob: 94b1dcabd9e20b73cd051b4609e82c42dbd4ef6e (
plain)
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
(.module:
[lux (#- nat)
[abstract
[equivalence (#+ Equivalence)]
[order (#+ Order)]
[enum (#+ Enum)]
[codec (#+ Codec)]]
[control
["." try]
["." exception (#+ exception:)]]
[data
["." text]]
[math
[number
["n" nat]]]])
(type: #export Day
#Sunday
#Monday
#Tuesday
#Wednesday
#Thursday
#Friday
#Saturday)
(structure: #export equivalence
(Equivalence Day)
(def: (= reference sample)
(case [reference sample]
(^template [<tag>]
[[<tag> <tag>]
#1])
([#Sunday]
[#Monday]
[#Tuesday]
[#Wednesday]
[#Thursday]
[#Friday]
[#Saturday])
_
#0)))
(def: (nat day)
(-> Day Nat)
(case day
#Sunday 0
#Monday 1
#Tuesday 2
#Wednesday 3
#Thursday 4
#Friday 5
#Saturday 6))
(structure: #export order
(Order Day)
(def: &equivalence ..equivalence)
(def: (< reference sample)
(n.< (..nat reference) (..nat sample))))
(structure: #export enum
(Enum Day)
(def: &order ..order)
(def: (succ day)
(case day
#Sunday #Monday
#Monday #Tuesday
#Tuesday #Wednesday
#Wednesday #Thursday
#Thursday #Friday
#Friday #Saturday
#Saturday #Sunday))
(def: (pred day)
(case day
#Monday #Sunday
#Tuesday #Monday
#Wednesday #Tuesday
#Thursday #Wednesday
#Friday #Thursday
#Saturday #Friday
#Sunday #Saturday)))
(exception: #export (not_a_day_of_the_week {value Text})
(exception.report
["Value" (text.format value)]))
(structure: #export codec
(Codec Text Day)
(def: (encode value)
(case value
#Monday "Monday"
#Tuesday "Tuesday"
#Wednesday "Wednesday"
#Thursday "Thursday"
#Friday "Friday"
#Saturday "Saturday"
#Sunday "Sunday"))
(def: (decode value)
(case value
"Monday" (#try.Success #..Monday)
"Tuesday" (#try.Success #..Tuesday)
"Wednesday" (#try.Success #..Wednesday)
"Thursday" (#try.Success #..Thursday)
"Friday" (#try.Success #..Friday)
"Saturday" (#try.Success #..Saturday)
"Sunday" (#try.Success #..Sunday)
_ (exception.throw ..not_a_day_of_the_week [value]))))
|
