blob: d72229832fbf03f1de3f7a789d1f8d9dbadc7811 (
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
(.module:
lux
(lux (control codec
monad)
(data [text]
(text format
["l" lexer "l/" Monad<Lexer>])
[number]
["e" error]
(coll [list "L/" Functor<List>]))
(lang [type "type/" Eq<Type>]))
["&" ../common])
(do-template [<name> <code>]
[(def: <name> &.Signal <code>)]
[type-signal "T"]
[primitive-signal "^"]
[void-signal "0"]
[unit-signal "1"]
[product-signal "*"]
[sum-signal "+"]
[function-signal ">"]
[application-signal "%"]
[uq-signal "U"]
[eq-signal "E"]
[bound-signal "$"]
[ex-signal "!"]
[var-signal "?"]
[named-signal "@"]
)
(def: (encode-type type)
(-> Type Text)
(if (or (is Type type)
(type/= Type type))
type-signal
(case type
(#.Primitive name params)
(format primitive-signal name &.stop-signal (&.encode-list encode-type params))
#.Void
void-signal
#.Unit
unit-signal
(^template [<tag> <prefix>]
(<tag> left right)
(format <prefix> (encode-type left) (encode-type right)))
([#.Product product-signal]
[#.Sum sum-signal]
[#.Function function-signal]
[#.App application-signal])
(^template [<tag> <prefix>]
(<tag> env body)
(format <prefix> (&.encode-list encode-type env) (encode-type body)))
([#.UnivQ uq-signal]
[#.ExQ eq-signal])
(^template [<tag> <prefix>]
(<tag> idx)
(format <prefix> (%i (nat-to-int idx)) &.stop-signal))
([#.Bound bound-signal]
[#.Ex ex-signal]
[#.Var var-signal])
(#.Named [module name] type*)
(format named-signal module &.ident-separator name &.stop-signal (encode-type type*))
)))
(def: type-decoder
(l.Lexer Type)
(l.rec
(function [type-decoder]
(with-expansions
[<simple> (do-template [<type> <signal>]
[(|> (l/wrap <type>) (l.after (l.text <signal>)))]
[Type type-signal]
[#.Void void-signal]
[#.Unit unit-signal])
<combinators> (do-template [<tag> <prefix>]
[(do l.Monad<Lexer>
[_ (l.text <prefix>)
left type-decoder
right type-decoder]
(wrap (<tag> left right)))]
[#.Product product-signal]
[#.Sum sum-signal]
[#.Function function-signal]
[#.App application-signal])
<abstractions> (do-template [<tag> <prefix>]
[(do l.Monad<Lexer>
[_ (l.text <prefix>)
env (&.decode-list type-decoder)
body type-decoder]
(wrap (<tag> env body)))]
[#.UnivQ uq-signal]
[#.ExQ eq-signal])
<wildcards> (do-template [<tag> <prefix>]
[(do l.Monad<Lexer>
[_ (l.text <prefix>)
id (l.codec number.Codec<Text,Int>
(l.some' l.digit))
_ (l.text &.stop-signal)]
(wrap (<tag> (int-to-nat id))))]
[#.Bound bound-signal]
[#.Ex ex-signal]
[#.Var var-signal])]
($_ l.either
(do l.Monad<Lexer>
[_ (l.text primitive-signal)
name (l.many' (l.none-of &.stop-signal))
_ (l.text &.stop-signal)
params (&.decode-list type-decoder)]
(wrap (#.Primitive name params)))
<simple>
<combinators>
<abstractions>
<wildcards>
(do l.Monad<Lexer>
[_ (l.text named-signal)
module (l.some' (l.none-of &.ident-separator))
_ (l.text &.ident-separator)
name (l.many' (l.none-of &.stop-signal))
_ (l.text &.stop-signal)
unnamed type-decoder]
(wrap (#.Named [module name] unnamed)))
)))))
(def: (decode-type input)
(-> Text (e.Error Type))
(|> type-decoder
(l.before l.end)
(l.run input)))
(struct: #export _ (Codec Text Type)
(def: encode encode-type)
(def: decode decode-type))
|
