Token.hs revision 7e4157a70efe2acab30dbe5079bba6db90923785
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- |
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDescription : parser for CASL 'Id's based on "Common.Lexer"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2004
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMaintainer : Christian.Maeder@dfki.de
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiStability : provisional
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPortability : portable
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiParser for CASL 'Id's based on "Common.Lexer"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- http://www.cofi.info/Documents/CASL/Summary/
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski from 25 March 2001
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski C.2.1 Basic Specifications with Subsorts
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSIMPLE-ID ::= WORDS
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiID ::= TOKEN-ID | MIXFIX-ID
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTOKEN-ID ::= TOKEN
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMIXFIX-ID ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | PLACE-TOKEN-ID ... PLACE-TOKEN-ID
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPLACE-TOKEN-ID ::= PLACE TOKEN-ID
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | PLACE
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPLACE ::= __
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu | SIGNS
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu SIGNS are adapted here and more permissive as in the summary
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu WORDS and NO-BRACKET-SIGNS are treated equally
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu legal are, ie. "{a}", "{+}", "a{}="
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu illegal is "a=" (no two SIMPLE-TOKEN stay beside each other)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu SIMPLE-TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu | NO-BRACKET-SIGNS
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu STB ::= SIMPLE-TOKEN BRACKETS
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu BST ::= BRACKETS SIMPLE-TOKEN
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu SIGNS ::= BRACKETS
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz | BRACKETS STB ... STB
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz | BRACKETS STB ... STB SIMPLE-TOKEN
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz | SIMPLE-TOKEN
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz | SIMPLE-TOKEN BST ... BST
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz | SIMPLE-TOKEN BST ... BST BRACKETS
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz A SIMPLE-TOKEN followed by "[" outside nested brackets
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz will be taken as the beginning of a compound list.
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz Within SIGNS brackets need not be balanced,
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz only after their composition to a MIXFIX-ID.
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz BRACKETS = BRACKET ... BRACKET
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz BRACKET ::= [ | ] | { | }
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz 2.4 Identifiers
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz brackets/braces within MIXFIX-ID must be balanced
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu C.2.2 Structured Specifications
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu TOKEN-ID ::= ... | TOKEN [ ID ,..., ID ]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu A compound list must follow the last TOKEN within MIXFIX-ID,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu so a compound list is never nested within (balanced) mixfix BRACKETS.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu Only PLACEs may follow a compound list.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu The IDs within the compound list may surely be compound IDs again.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu-}
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescumodule Common.Token where
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Common.Id
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Common.Keywords
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Common.Lexer
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Common.Parsec
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Text.ParserCombinators.Parsec
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuimport Data.List (delete)
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu-- * Casl keyword lists
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu-- | reserved signs
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescucasl_reserved_ops :: [String]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescucasl_reserved_ops = [colonS, colonQuMark, defnS, dotS, cDot, mapsTo]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | these formula signs are legal in terms, but illegal in declarations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiformula_ops :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiformula_ops = [equalS, implS, equivS, lOr, lAnd, negS]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | all reseverd signs
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_fops :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_fops = formula_ops ++ casl_reserved_ops
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | reserved keywords
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_basic_reserved_words :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_basic_reserved_words =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [axiomS, axiomS ++ sS, cogeneratedS, cotypeS, cotypeS ++ sS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski esortS, esortS ++ sS, etypeS, etypeS ++ sS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski existsS, forallS, freeS, generatedS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski opS, opS ++ sS, predS, predS ++ sS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski sortS, sortS ++ sS, typeS, typeS ++ sS, varS, varS ++ sS]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | reserved keywords
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_structured_reserved_words :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_structured_reserved_words =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [andS, archS, behaviourallyS, closedS, cofreeS, endS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fitS, freeS, fromS, getS, givenS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski hideS, lambdaS, libraryS, localS, logicS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski refinedS, refinementS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski resultS, revealS, specS, thenS, toS,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski unitS, unitS ++ sS, versionS, viewS, withS, withinS]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | reserved keywords
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_words :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_words =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski casl_basic_reserved_words ++ casl_structured_reserved_words
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | these formula words are legal in terms, but illegal in declarations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiformula_words :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiformula_words = [asS, defS, elseS, ifS, inS, whenS, falseS, notS, trueS]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | all reserved words
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_fwords :: [String]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_reserved_fwords = formula_words ++ casl_reserved_words
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- * a single 'Token' parser taking lists of key symbols and words as parameter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | a simple 'Token' parser depending on reserved signs and words
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- (including a quoted char, dot-words or a single digit)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisid :: ([String], [String]) -> GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisid (kOps, kWords) = pToken (scanQuotedChar <|> scanDotWords
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <|> scanDigit <|> reserved kOps scanAnySigns
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <|> reserved kWords scanAnyWords <?> "simple-id")
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- * 'Token' lists parsers
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | balanced mixfix components within braces
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskibraceP :: GenParser Char st [Token] -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskibraceP p = oBraceT <:> p <++> single cBraceT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <|> try (oBracketT <:> single cBracketT)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | balanced mixfix components within square brackets
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskibracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskibracketP p = oBracketT <:> p <++> single cBracketT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | an 'sid' optionally followed by other mixfix components
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- (without no two consecutive 'sid's)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerMix1 :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerMix1 l = sid l <:> optionL (innerMix2 l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | mixfix components not starting with a 'sid' (possibly places)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerMix2 :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerMix2 l = let p = innerList l in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski flat (many1 (braceP p <|> bracketP p <|> many1 placeT))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <++> optionL (innerMix1 l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | any mixfix components within braces or brackets
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerList :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinnerList l = optionL (innerMix1 l <|> innerMix2 l <?> "token")
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | mixfix components starting with a 'sid' (outside 'innerList')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix1 :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix1 l = sid l <:> optionL (topMix2 l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | mixfix components starting with braces ('braceP')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- that may follow 'sid' outside 'innerList'.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- (Square brackets after a 'sid' will be taken as a compound list.)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix2 :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix2 l = flat (many1 (braceP $ innerList l)) <++> optionL (topMix1 l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | mixfix components starting with square brackets ('bracketP')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- that may follow a place ('placeT') (outside 'innerList')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix3 :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitopMix3 l = let p = innerList l in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski bracketP p <++> flat (many (braceP p))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <++> optionL (topMix1 l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | any ('topMix1', 'topMix2', 'topMix3') mixfix components
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- that may follow a place ('placeT') at the top level
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiafterPlace :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiafterPlace l = topMix1 l <|> topMix2 l <|> topMix3 l
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | places possibly followed by other ('afterPlace') mixfix components
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimiddle :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimiddle l = many1 placeT <++> optionL (afterPlace l)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | many (balanced, top-level) mixfix components ('afterPlace')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- possibly interspersed with multiple places ('placeT')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitokStart :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskitokStart l = afterPlace l <++> flat (many (middle l))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | any (balanced, top-level) mixfix components
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- possibly starting with places but no single 'placeT' only.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistart :: ([String], [String]) -> GenParser Char st [Token]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistart l = tokStart l <|> placeT <:> (tokStart l <|>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski many1 placeT <++> optionL (tokStart l))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski <?> "id"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- * parser for mixfix and compound 'Id's
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | parsing a compound list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicomps :: ([String], [String]) -> GenParser Char st ([Id], Range)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicomps keys = do
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski o <- oBracketT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ts, ps) <- mixId keys keys `separatedBy` commaT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski c <- cBracketT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski return (ts, toRange o ps c)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{- | parse mixfix components ('start') and an optional compound list ('comps')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski if the last token was no place. Accept possibly further places.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Key strings (second argument) within compound list may differ from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski top-level key strings (first argument)!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimixId :: ([String], [String]) -> ([String], [String]) -> GenParser Char st Id
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimixId keys idKeys = do
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski l <- start keys
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski if isPlace (last l) then return (Id l [] nullRange) else do
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (c, p) <- option ([], nullRange) (comps idKeys)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski u <- many placeT
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski return (Id (l ++ u) c p)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the Casl key strings (signs first) with additional keywords
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_keys :: [String] -> ([String], [String])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicasl_keys ks = (ks ++ casl_reserved_fops, ks ++ casl_reserved_fwords)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Casl ids for operations and predicates
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiparseId :: [String] -> GenParser Char st Id
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiparseId ks = mixId (casl_keys ks) (casl_keys ks)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | disallow 'barS' within the top-level of constructor names
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiconsId :: [String] -> GenParser Char st Id
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiconsId ks = mixId (barS : ks ++ casl_reserved_fops,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ks ++ casl_reserved_fwords) $ casl_keys ks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Casl sorts are simple words ('varId'),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- but may have a compound list ('comps')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisortId :: [String] -> GenParser Char st Id
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisortId ks =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski do s <- varId ks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (c, p) <- option ([], nullRange) (comps $ casl_keys ks)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski return (Id [s] c p)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- * parser for simple 'Id's
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | parse a simple word not in 'casl_reserved_fwords'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskivarId :: [String] -> GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskivarId ks = pToken (reserved (ks ++ casl_reserved_fwords) scanAnyWords)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | like 'varId'. 'Common.Id.SIMPLE_ID' for spec- and view names
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisimpleId :: GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisimpleId = pToken (reserved casl_structured_reserved_words scanAnyWords)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- * parser for key 'Token's
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | parse a question mark key sign ('quMark')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiquMarkT :: GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiquMarkT = pToken $ toKey quMark
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | parse a 'colonS' possibly immediately followed by a 'quMark'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicolonST :: GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicolonST = pToken $ try $ string colonS << notFollowedBy
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (oneOf $ delete '?' signChars)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | parse the product key sign ('prodS' or 'timesS')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicrossT :: GenParser Char st Token
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskicrossT = pToken (toKey prodS <|> toKey timesS) <?> "cross"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski