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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
|
{-# LANGUAGE NoImplicitPrelude #-}
{-|
This module defines lots of keywords and various filler
phrases. The prefix underscore indicates that we do not
care about the parse result (analogous to discarding
like @...; _ <- action; ...@ in do-notation). Moreover,
this convention allows the use of short names that would
otherwise be Haskell keywords or clash with other definitions.
Care should be taken with introducing too many variants of
a keyword, lest the grammar becomes needlessly ambiguous!
The names are chosen using the following criteria:
* As short as possible (e.g.: @_since@ over @_because@).
* Sound like a keyword (e.g.: @_show@).
This module also defines symbols that have special uses
(such as @_colon@ for its use in type signatures).
-}
module Syntax.Concrete.Keywords where
import Base
import Syntax.Token
import Report.Location
import Text.Earley (Prod, (<?>), terminal)
infixr 0 ?
-- | Variant of '<?>' for annotating literal tokens.
(?) :: Prod r Text t a -> Text -> Prod r Text t a
p ? e = p <?> ("\"" <> e <> "\"")
word :: Text -> Prod r Text (Located Token) Location
word w = terminal maybeToken
where
maybeToken ltok = case unLocated ltok of
Word w' | w == w' -> Just (startPos ltok)
_ -> Nothing
symbol :: Text -> Prod r Text (Located Token) Location
symbol s = terminal maybeToken
where
maybeToken ltok = case unLocated ltok of
Symbol s' | s == s' -> Just (startPos ltok)
_ -> Nothing
command :: Text -> Prod r Text (Located Token) Location
command cmd = terminal maybeToken
where
maybeToken ltok = case unLocated ltok of
Command cmd' | cmd == cmd' -> Just (startPos ltok)
_ -> Nothing
_arity :: Prod r Text (Located Token) Int
_arity = asum
[ 1 <$ word "unary"
, 2 <$ word "binary"
, 3 <$ word "ternary"
, 4 <$ word "quaternary"
, 5 <$ word "quinary"
, 6 <$ word "senary"
, 7 <$ word "septenary"
, 8 <$ word "octonary"
, 9 <$ word "nonary"
, 10 <$ word "denary"
] <?> "\"unary\", \"binary\', ..."
-- * Keywords
_an :: Prod r Text (Located Token) Location
_an = word "a" <|> word "an" <?> "indefinite article"
_and :: Prod r Text (Located Token) Location
_and = word "and" ? "and"
_are :: Prod r Text (Located Token) Location
_are = word "are" ? "are"
_asFollows :: Prod r Text (Located Token) Location
_asFollows = word "as" <* word "follows" ? "as follows"
_assumption :: Prod r Text (Located Token) Location
_assumption = word "assumption" ? "assumption"
_be :: Prod r Text (Located Token) Location
_be = word "be" ? "be"
_by :: Prod r Text (Located Token) Location
_by = word "by" ? "by"
_bySetExt :: Prod r Text (Located Token) Location
_bySetExt = word "by" <* ((word "set" ? "set") <* word "extensionality") ? "by set extensionality"
_can :: Prod r Text (Located Token) Location
_can = word "can" ? "can"
_consistsOf :: Prod r Text (Located Token) Location
_consistsOf = word "consists" <* word "of" ? "consists of"
_contradiction :: Prod r Text (Located Token) Location
_contradiction = optional (word "a") *> word "contradiction" ? "a contradiction"
_define :: Prod r Text (Located Token) Location
_define = word "define" ? "define"
_definition :: Prod r Text (Located Token) Location
_definition = word "definition" ? "definition"
_denote :: Prod r Text (Located Token) Location
_denote = word "denote" <|> (word "stand" <* word "for") ? "denote"
_denotes :: Prod r Text (Located Token) Location
_denotes = word "denotes" ? "denotes"
_do :: Prod r Text (Located Token) Location
_do = word "do" ? "do"
_does :: Prod r Text (Located Token) Location
_does = word "does" ? "does"
_either :: Prod r Text (Located Token) Location
_either = word "either" ? "either"
_equipped :: Prod r Text (Located Token) Location
_equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with"
_every :: Prod r Text (Located Token) Location
_every = word "every" ? "every"
_exist :: Prod r Text (Located Token) Location
_exist = word "there" <* word "exist" ? "there exist"
_exists :: Prod r Text (Located Token) Location
_exists = word "there" <* word "exists" ? "there exists"
_extends :: Prod r Text (Located Token) Location
_extends = (_is) <|> (word "consists" <* word "of") ? "consists of"
_fix :: Prod r Text (Located Token) Location
_fix = word "fix" ? "fix"
_follows :: Prod r Text (Located Token) Location
_follows = word "follows" ? "follows"
_for :: Prod r Text (Located Token) Location
_for = word "for" ? "for"
_forAll :: Prod r Text (Located Token) Location
_forAll = (word "for" <* word "all") <|> word "all" ? "all"
_forEvery :: Prod r Text (Located Token) Location
_forEvery = (word "for" <* word "every") <|> word "every" ? "for every"
_have :: Prod r Text (Located Token) Location
_have = word "we" <* word "have" <* optional (word "that") ? "we have"
_if :: Prod r Text (Located Token) Location
_if = word "if" ? "if"
_iff :: Prod r Text (Located Token) Location
_iff = word "iff" <|> (word "if" <* word "and" <* word "only" <* word "if") ? "iff"
_inductively :: Prod r Text (Located Token) Location
_inductively = word "inductively" ? "inductively"
_is :: Prod r Text (Located Token) Location
_is = word "is" ? "is"
_itIsWrong :: Prod r Text (Located Token) Location
_itIsWrong = word "it" <* word "is" <* (word "not" <* word "the" <* word "case" <|> word "wrong") <* word "that" ? "it is wrong that"
_let :: Prod r Text (Located Token) Location
_let = word "let" ? "let"
_neither :: Prod r Text (Located Token) Location
_neither = word "neither" ? "neither"
_no :: Prod r Text (Located Token) Location
_no = word "no" ? "no"
_nor :: Prod r Text (Located Token) Location
_nor = word "nor" ? "nor"
_not :: Prod r Text (Located Token) Location
_not = word "not" ? "not"
_omitted :: Prod r Text (Located Token) Location
_omitted = word "omitted" ? "omitted"
_on :: Prod r Text (Located Token) Location
_on = word "on" ? "on"
_oneOf :: Prod r Text (Located Token) Location
_oneOf = word "one" <* word "of" ? "one of"
_or :: Prod r Text (Located Token) Location
_or = word "or" ? "or"
_particularly :: Prod r Text (Located Token) Location
_particularly = (word "particularly" <|> (word "in" *> word "particular")) <* _comma ? "particularly"
_relation :: Prod r Text (Located Token) Location
_relation = word "relation" ? "relation"
_satisfying :: Prod r Text (Located Token) Location
_satisfying = _suchThat <|> word "satisfying" ? "satisfying"
_setOf :: Prod r Text (Located Token) Location
_setOf = word "set" <* word "of" ? "set of"
_now :: Prod r Text (Located Token) Location
_now = (word "then" <|> word "next" <|> word "now" <|> word "first" <|> word "finally" <|> word "subsequently" <|> word "ultimately")
_show :: Prod r Text (Located Token) Location
_show = optional _now *> optional (word "we") *> word "show" <* optional (word "that")
_since :: Prod r Text (Located Token) Location
_since = word "since" <|> word "because" ? "since"
_some :: Prod r Text (Located Token) Location
_some = word "some" ? "some"
_suchThat :: Prod r Text (Located Token) Location
_suchThat = ((word "such" <* word "that") <|> (word "s" <* _dot <* word "t" <* _dot)) ? "such that"
_sufficesThat :: Prod r Text (Located Token) Location
_sufficesThat = word "it" <* word "suffices" <* word "to" <* word "show" <* word "that" ? "it suffices to show"
_suppose :: Prod r Text (Located Token) Location
_suppose = (word "suppose" <|> word "assume") <* optional (word "that") ? "assume"
_take :: Prod r Text (Located Token) Location
_take = optional _now *> (word "take" <|> word "consider") ? "take"
_that :: Prod r Text (Located Token) Location
_that = word "that" ? "that"
_the :: Prod r Text (Located Token) Location
_the = word "the" ? "the"
_then :: Prod r Text (Located Token) Location
_then = word "then" ? "then"
_thus :: Prod r Text (Located Token) Location
_thus = word "thus" <|> word "hence" <|> _now <|> word "therefore" ? "thus"
_trivial :: Prod r Text (Located Token) Location
_trivial = word "straightforward" <|> word "trivial" ? "trivial"
_unique :: Prod r Text (Located Token) Location
_unique = word "unique" ? "unique"
_write :: Prod r Text (Located Token) Location
_write = (optional (word "we") *> word "say" <* optional (word "that")) <|> (optional (word "we") *> word "write") ? "write"
-- | Introducing plain claims in proofs.
_haveIntro :: Prod r Text (Located Token) Location
_haveIntro = _thus <|> _particularly <|> _have
-- * Symbols
_colon :: Prod r Text (Located Token) Location
_colon = symbol ":" ? ":"
_pipe :: Prod r Text (Located Token) Location
_pipe = (optional (command "middle") *> symbol "|") <|> command "mid" ? "\\mid"
_comma :: Prod r Text (Located Token) Location
_comma = symbol "," ? ","
_commaAnd :: Prod r Text (Located Token) Location
_commaAnd = symbol "," <* optional (word "and") ? ", and"
_commaOr :: Prod r Text (Located Token) Location
_commaOr = symbol "," <* optional (word "or") ? ", or"
_defeq :: Prod r Text (Located Token) Location
_defeq = symbol ":=" ? ":=" -- Should use `\coloneq` from unicode-math as display.
_dot :: Prod r Text (Located Token) Location
_dot = symbol "." ? "."
_eq :: Prod r Text (Located Token) Location
_eq = symbol "=" ? "="
_in :: Prod r Text (Located Token) Location
_in = command "in" ? "\\in"
_subseteq :: Prod r Text (Located Token) Location
_subseteq = command "subseteq" ? "\\subseteq"
_to :: Prod r Text (Located Token) Location
_to = command "to" ? "\\to"
_mapsto :: Prod r Text (Located Token) Location
_mapsto = command "mapsto" ? "\\mapsto"
_ampersand :: Prod r Text (Located Token) Location
_ampersand = symbol "&" ? "&"
|
