diff options
Diffstat (limited to 'source/Syntax/Concrete')
| -rw-r--r-- | source/Syntax/Concrete/Keywords.hs | 222 |
1 files changed, 222 insertions, 0 deletions
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs new file mode 100644 index 0000000..e0f577e --- /dev/null +++ b/source/Syntax/Concrete/Keywords.hs @@ -0,0 +1,222 @@ +{-# 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 Text.Earley (Prod, (<?>), terminal) +import Text.Megaparsec (SourcePos) + +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) SourcePos +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) SourcePos +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) SourcePos +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) SourcePos +_an = word "a" <|> word "an" <?> "indefinite article" +_and :: Prod r Text (Located Token) SourcePos +_and = word "and" ? "and" +_are :: Prod r Text (Located Token) SourcePos +_are = word "are" ? "are" +_asFollows :: Prod r Text (Located Token) SourcePos +_asFollows = word "as" <* word "follows" ? "as follows" +_assumption :: Prod r Text (Located Token) SourcePos +_assumption = word "assumption" ? "assumption" +_be :: Prod r Text (Located Token) SourcePos +_be = word "be" ? "be" +_by :: Prod r Text (Located Token) SourcePos +_by = word "by" ? "by" +_bySetExt :: Prod r Text (Located Token) SourcePos +_bySetExt = word "by" <* ((word "set" ? "set") <* word "extensionality") ? "by set extensionality" +_can :: Prod r Text (Located Token) SourcePos +_can = word "can" ? "can" +_consistsOf :: Prod r Text (Located Token) SourcePos +_consistsOf = word "consists" <* word "of" ? "consists of" +_contradiction :: Prod r Text (Located Token) SourcePos +_contradiction = optional (word "a") *> word "contradiction" ? "a contradiction" +_define :: Prod r Text (Located Token) SourcePos +_define = word "define" ? "define" +_definition :: Prod r Text (Located Token) SourcePos +_definition = word "definition" ? "definition" +_denote :: Prod r Text (Located Token) SourcePos +_denote = word "denote" <|> (word "stand" <* word "for") ? "denote" +_denotes :: Prod r Text (Located Token) SourcePos +_denotes = word "denotes" ? "denotes" +_do :: Prod r Text (Located Token) SourcePos +_do = word "do" ? "do" +_does :: Prod r Text (Located Token) SourcePos +_does = word "does" ? "does" +_either :: Prod r Text (Located Token) SourcePos +_either = word "either" ? "either" +_equipped :: Prod r Text (Located Token) SourcePos +_equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with" +_every :: Prod r Text (Located Token) SourcePos +_every = (word "every") ? "every" +_exist :: Prod r Text (Located Token) SourcePos +_exist = word "there" <* word "exist" ? "there exist" +_exists :: Prod r Text (Located Token) SourcePos +_exists = word "there" <* word "exists" ? "there exists" +_extends :: Prod r Text (Located Token) SourcePos +_extends = (_is) <|> (word "consists" <* word "of") ? "consists of" +_fix :: Prod r Text (Located Token) SourcePos +_fix = word "fix" ? "fix" +_follows :: Prod r Text (Located Token) SourcePos +_follows = word "follows" ? "follows" +_for :: Prod r Text (Located Token) SourcePos +_for = word "for" ? "for" +_forAll :: Prod r Text (Located Token) SourcePos +_forAll = (word "for" <* word "all") <|> word "all" ? "all" +_forEvery :: Prod r Text (Located Token) SourcePos +_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every" +_have :: Prod r Text (Located Token) SourcePos +_have = word "we" <* word "have" <* optional (word "that") ? "we have" +_if :: Prod r Text (Located Token) SourcePos +_if = word "if" ? "if" +_iff :: Prod r Text (Located Token) SourcePos +_iff = word "iff" <|> (word "if" <* word "and" <* word "only" <* word "if") ? "iff" +_inductively :: Prod r Text (Located Token) SourcePos +_inductively = word "inductively" ? "inductively" +_is :: Prod r Text (Located Token) SourcePos +_is = word "is" ? "is" +_itIsWrong :: Prod r Text (Located Token) SourcePos +_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) SourcePos +_let = word "let" ? "let" +_neither :: Prod r Text (Located Token) SourcePos +_neither = word "neither" ? "neither" +_no :: Prod r Text (Located Token) SourcePos +_no = word "no" ? "no" +_nor :: Prod r Text (Located Token) SourcePos +_nor = word "nor" ? "nor" +_not :: Prod r Text (Located Token) SourcePos +_not = word "not" ? "not" +_omitted :: Prod r Text (Located Token) SourcePos +_omitted = word "omitted" ? "omitted" +_on :: Prod r Text (Located Token) SourcePos +_on = word "on" ? "on" +_oneOf :: Prod r Text (Located Token) SourcePos +_oneOf = word "one" <* word "of" ? "one of" +_or :: Prod r Text (Located Token) SourcePos +_or = word "or" ? "or" +_particularly :: Prod r Text (Located Token) SourcePos +_particularly = (word "particularly" <|> (word "in" *> word "particular")) <* _comma ? "particularly" +_relation :: Prod r Text (Located Token) SourcePos +_relation = word "relation" ? "relation" +_satisfying :: Prod r Text (Located Token) SourcePos +_satisfying = _suchThat <|> word "satisfying" ? "satisfying" +_setOf :: Prod r Text (Located Token) SourcePos +_setOf = word "set" <* word "of" ? "set of" +_show :: Prod r Text (Located Token) SourcePos +_show = optional (word "first" <|> word "finally" <|> word "next" <|> word "now") *> optional (word "we") *> word "show" <* optional (word "that") +_since :: Prod r Text (Located Token) SourcePos +_since = word "since" <|> word "because" ? "since" +_some :: Prod r Text (Located Token) SourcePos +_some = word "some" ? "some" +_suchThat :: Prod r Text (Located Token) SourcePos +_suchThat = ((word "such" <* word "that") <|> (word "s" <* _dot <* word "t" <* _dot)) ? "such that" +_sufficesThat :: Prod r Text (Located Token) SourcePos +_sufficesThat = word "it" <* word "suffices" <* word "to" <* word "show" <* word "that" ? "it suffices to show" +_suppose :: Prod r Text (Located Token) SourcePos +_suppose = (word "suppose" <|> word "assume") <* optional (word "that") ? "assume" +_take :: Prod r Text (Located Token) SourcePos +_take = word "take" <|> word "consider" ? "take" +_that :: Prod r Text (Located Token) SourcePos +_that = word "that" ? "that" +_the :: Prod r Text (Located Token) SourcePos +_the = word "the" ? "the" +_then :: Prod r Text (Located Token) SourcePos +_then = word "then" ? "then" +_throughout :: Prod r Text (Located Token) SourcePos +_throughout = word "throughout" <* optional (word "this" <* word "section") <* optional _comma <|> (word "in" <* word "the" <* word "sequel") ? "throughout" +_thus :: Prod r Text (Located Token) SourcePos +_thus = word "thus" <|> word "then" <|> word "hence" <|> word "now" <|> word "finally" <|> word "therefore" ? "thus" +_trivial :: Prod r Text (Located Token) SourcePos +_trivial = word "straightforward" <|> word "trivial" ? "trivial" +_unique :: Prod r Text (Located Token) SourcePos +_unique = word "unique" ? "unique" +_write :: Prod r Text (Located Token) SourcePos +_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) SourcePos +_haveIntro = _thus <|> _particularly <|> _have + +-- * Symbols + +_colon :: Prod r Text (Located Token) SourcePos +_colon = symbol ":" ? ":" +_pipe :: Prod r Text (Located Token) SourcePos +_pipe = symbol "|" <|> command "mid" ? "\\mid" +_comma :: Prod r Text (Located Token) SourcePos +_comma = symbol "," ? "," +_commaAnd :: Prod r Text (Located Token) SourcePos +_commaAnd = symbol "," <* optional (word "and") ? ", and" +_commaOr :: Prod r Text (Located Token) SourcePos +_commaOr = symbol "," <* optional (word "or") ? ", or" +_defeq :: Prod r Text (Located Token) SourcePos +_defeq = symbol ":=" ? ":=" -- Should use `\coloneq` from unicode-math as display. +_dot :: Prod r Text (Located Token) SourcePos +_dot = symbol "." ? "." +_eq :: Prod r Text (Located Token) SourcePos +_eq = symbol "=" ? "=" +_in :: Prod r Text (Located Token) SourcePos +_in = symbol "∈" <|> command "in" ? "\\in" +_subseteq :: Prod r Text (Located Token) SourcePos +_subseteq = command "subseteq" ? ":" |