Token.hs revision 1600a2e47d5ed599df94d20411f0767fb6d68587
e83ed59502a681713982f25c559aae77a4145734Christian Maeder{- |
eb483f2216949400bfef8f6deb5320f071445626Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : parser for CASL 'Id's based on "Common.Lexer"
eb483f2216949400bfef8f6deb5320f071445626Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
eb483f2216949400bfef8f6deb5320f071445626Christian MaederStability : provisional
eb483f2216949400bfef8f6deb5320f071445626Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiParser for CASL 'Id's based on "Common.Lexer"
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-}
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder{- http://www.cofi.info/Documents/CASL/Summary/
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder from 25 March 2001
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder C.2.1 Basic Specifications with Subsorts
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederSIMPLE-ID ::= WORDS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederID ::= TOKEN-ID | MIXFIX-ID
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederTOKEN-ID ::= TOKEN
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederMIXFIX-ID ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | PLACE-TOKEN-ID ... PLACE-TOKEN-ID
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederPLACE-TOKEN-ID ::= PLACE TOKEN-ID
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | PLACE
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederPLACE ::= __
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian MaederTOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | SIGNS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder SIGNS are adapted here and more permissive as in the summary
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder WORDS and NO-BRACKET-SIGNS are treated equally
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder legal are, ie. "{a}", "{+}", "a{}="
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder illegal is "a=" (no two SIMPLE-TOKEN stay beside each other)
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder SIMPLE-TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | NO-BRACKET-SIGNS
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder STB ::= SIMPLE-TOKEN BRACKETS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder BST ::= BRACKETS SIMPLE-TOKEN
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder SIGNS ::= BRACKETS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | BRACKETS STB ... STB
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | BRACKETS STB ... STB SIMPLE-TOKEN
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | SIMPLE-TOKEN
e83ed59502a681713982f25c559aae77a4145734Christian Maeder | SIMPLE-TOKEN BST ... BST
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | SIMPLE-TOKEN BST ... BST BRACKETS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder A SIMPLE-TOKEN followed by "[" outside nested brackets
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder will be taken as the beginning of a compound list.
e83ed59502a681713982f25c559aae77a4145734Christian Maeder Within SIGNS brackets need not be balanced,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder only after their composition to a MIXFIX-ID.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder BRACKETS = BRACKET ... BRACKET
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder BRACKET ::= [ | ] | { | }
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 2.4 Identifiers
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder brackets/braces within MIXFIX-ID must be balanced
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder C.2.2 Structured Specifications
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TOKEN-ID ::= ... | TOKEN [ ID ,..., ID ]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder A compound list must follow the last TOKEN within MIXFIX-ID,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder so a compound list is never nested within (balanced) mixfix BRACKETS.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Only PLACEs may follow a compound list.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder The IDs within the compound list may surely be compound IDs again.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maedermodule Common.Token where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport Common.Id
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maederimport Common.Keywords
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maederimport Common.Lexer
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport Common.Parsec
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maederimport Text.ParserCombinators.Parsec
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- * Casl keyword lists
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | reserved signs
eb483f2216949400bfef8f6deb5320f071445626Christian Maedercasl_reserved_ops :: [String]
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maedercasl_reserved_ops = [colonS, colonQuMark, defnS, dotS, cDot, mapsTo]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | these formula signs are legal in terms, but illegal in declarations
eb483f2216949400bfef8f6deb5320f071445626Christian Maederformula_ops :: [String]
e83ed59502a681713982f25c559aae77a4145734Christian Maederformula_ops = [equalS, implS, equivS, lOr, lAnd, negS]
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | all reseverd signs
eb483f2216949400bfef8f6deb5320f071445626Christian Maedercasl_reserved_fops :: [String]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercasl_reserved_fops = formula_ops ++ casl_reserved_ops
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski-- | reserved keywords
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskicasl_basic_reserved_words :: [String]
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskicasl_basic_reserved_words =
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder [axiomS, axiomS ++ sS, cogeneratedS, cotypeS, cotypeS ++ sS,
58564afba8f0bb6b57783c4b440d0b666edf5f67Christian Maeder esortS, esortS ++ sS, etypeS, etypeS ++ sS,
e83ed59502a681713982f25c559aae77a4145734Christian Maeder existsS, forallS, freeS, generatedS,
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder opS, opS ++ sS, predS, predS ++ sS,
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder sortS, sortS ++ sS, typeS, typeS ++ sS, varS, varS ++ sS]
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski-- | reserved keywords
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskicasl_structured_reserved_words :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maedercasl_structured_reserved_words = libraryS :
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder continuationKeywords ++ otherStartKeywords
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder ++ criticalKeywords
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder-- | keywords terminating a basic spec or starting a new library item
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaedercriticalKeywords :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaedercriticalKeywords = terminatingKeywords ++ startingKeywords
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder-- | keywords terminating a basic spec
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederterminatingKeywords :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederterminatingKeywords =
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder [andS, endS, fitS, hideS, revealS, thenS, withS, withinS]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder-- | keywords starting a library item
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederstartingKeywords :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederstartingKeywords =
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder [archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder-- | keywords that may follow a defining equal sign
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederotherStartKeywords :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaederotherStartKeywords =
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder [closedS, cofreeS, freeS, localS, unitS ++ sS]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder-- | other intermediate keywords
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaedercontinuationKeywords :: [String]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian MaedercontinuationKeywords =
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder [behaviourallyS, getS, givenS, lambdaS, refinedS, resultS, toS, versionS]
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | reserved keywords
eb483f2216949400bfef8f6deb5320f071445626Christian Maedercasl_reserved_words :: [String]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercasl_reserved_words =
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder casl_basic_reserved_words ++ casl_structured_reserved_words
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | these formula words are legal in terms, but illegal in declarations
eb483f2216949400bfef8f6deb5320f071445626Christian Maederformula_words :: [String]
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maederformula_words = [asS, defS, elseS, ifS, inS, whenS, falseS, notS, trueS]
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | all reserved words
eb483f2216949400bfef8f6deb5320f071445626Christian Maedercasl_reserved_fwords :: [String]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercasl_reserved_fwords = formula_words ++ casl_reserved_words
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder-- * a single 'Token' parser taking lists of key symbols and words as parameter
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | a simple 'Token' parser depending on reserved signs and words
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder (including a quoted char, dot-words or a single digit) -}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedersid :: ([String], [String]) -> GenParser Char st Token
e83ed59502a681713982f25c559aae77a4145734Christian Maedersid (kOps, kWords) = pToken (scanQuotedChar <|> scanDotWords
e83ed59502a681713982f25c559aae77a4145734Christian Maeder <|> scanDigit <|> reserved kOps scanAnySigns
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder <|> reserved kWords scanAnyWords <?> "simple-id")
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- * 'Token' lists parsers
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | balanced mixfix components within braces
eb483f2216949400bfef8f6deb5320f071445626Christian MaederbraceP :: GenParser Char st [Token] -> GenParser Char st [Token]
dc427a9450cd7b463717a2255c804afa47a54365Christian MaederbraceP p = oBraceT <:> p <++> single cBraceT
dc427a9450cd7b463717a2255c804afa47a54365Christian Maeder <|> try (oBracketT <:> single cBracketT)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | balanced mixfix components within square brackets
eb483f2216949400bfef8f6deb5320f071445626Christian MaederbracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
dc427a9450cd7b463717a2255c804afa47a54365Christian MaederbracketP p = oBracketT <:> p <++> single cBracketT
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | an 'sid' optionally followed by other mixfix components
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder (without no two consecutive 'sid's) -}
eb483f2216949400bfef8f6deb5320f071445626Christian MaederinnerMix1 :: ([String], [String]) -> GenParser Char st [Token]
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaederinnerMix1 l = sid l <:> optionL (innerMix2 l)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | mixfix components not starting with a 'sid' (possibly places)
eb483f2216949400bfef8f6deb5320f071445626Christian MaederinnerMix2 :: ([String], [String]) -> GenParser Char st [Token]
e83ed59502a681713982f25c559aae77a4145734Christian MaederinnerMix2 l = let p = innerList l in
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder flat (many1 (braceP p <|> bracketP p <|> many1 placeT))
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder <++> optionL (innerMix1 l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | any mixfix components within braces or brackets
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinnerList :: ([String], [String]) -> GenParser Char st [Token]
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaederinnerList l = optionL (innerMix1 l <|> innerMix2 l <?> "token")
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | mixfix components starting with a 'sid' (outside 'innerList')
eb483f2216949400bfef8f6deb5320f071445626Christian MaedertopMix1 :: ([String], [String]) -> GenParser Char st [Token]
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaedertopMix1 l = sid l <:> optionL (topMix2 l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | mixfix components starting with braces ('braceP')
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder that may follow 'sid' outside 'innerList'.
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder (Square brackets after a 'sid' will be taken as a compound list.) -}
eb483f2216949400bfef8f6deb5320f071445626Christian MaedertopMix2 :: ([String], [String]) -> GenParser Char st [Token]
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaedertopMix2 l = flat (many1 (braceP $ innerList l)) <++> optionL (topMix1 l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | mixfix components starting with square brackets ('bracketP')
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder that may follow a place ('placeT') (outside 'innerList') -}
eb483f2216949400bfef8f6deb5320f071445626Christian MaedertopMix3 :: ([String], [String]) -> GenParser Char st [Token]
e83ed59502a681713982f25c559aae77a4145734Christian MaedertopMix3 l = let p = innerList l in
e83ed59502a681713982f25c559aae77a4145734Christian Maeder bracketP p <++> flat (many (braceP p))
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder <++> optionL (topMix1 l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | any ('topMix1', 'topMix2', 'topMix3') mixfix components
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder that may follow a place ('placeT') at the top level -}
eb483f2216949400bfef8f6deb5320f071445626Christian MaederafterPlace :: ([String], [String]) -> GenParser Char st [Token]
7e4157a70efe2acab30dbe5079bba6db90923785Christian MaederafterPlace l = topMix1 l <|> topMix2 l <|> topMix3 l
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder-- | places possibly followed by other ('afterPlace') mixfix components
eb483f2216949400bfef8f6deb5320f071445626Christian Maedermiddle :: ([String], [String]) -> GenParser Char st [Token]
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maedermiddle l = many1 placeT <++> optionL (afterPlace l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | many (balanced, top-level) mixfix components ('afterPlace')
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder possibly interspersed with multiple places ('placeT') -}
eb483f2216949400bfef8f6deb5320f071445626Christian MaedertokStart :: ([String], [String]) -> GenParser Char st [Token]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedertokStart l = afterPlace l <++> flat (many (middle l))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | any (balanced, top-level) mixfix components
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder possibly starting with places but no single 'placeT' only. -}
eb483f2216949400bfef8f6deb5320f071445626Christian Maederstart :: ([String], [String]) -> GenParser Char st [Token]
e83ed59502a681713982f25c559aae77a4145734Christian Maederstart l = tokStart l <|> placeT <:> (tokStart l <|>
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder many1 placeT <++> optionL (tokStart l))
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder <?> "id"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- * parser for mixfix and compound 'Id's
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | parsing a compound list
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskicomps :: ([String], [String]) -> GenParser Char st ([Id], Range)
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maedercomps keys = do
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder o <- oBracketT
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder (ts, ps) <- mixId keys keys `separatedBy` commaT
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder c <- cBracketT
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder return (ts, toRange o ps c)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder{- | parse mixfix components ('start') and an optional compound list ('comps')
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder if the last token was no place. Accept possibly further places.
e83ed59502a681713982f25c559aae77a4145734Christian Maeder Key strings (second argument) within compound list may differ from
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder top-level key strings (first argument)!
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermixId :: ([String], [String]) -> ([String], [String]) -> GenParser Char st Id
7e4157a70efe2acab30dbe5079bba6db90923785Christian MaedermixId keys idKeys = do
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder l <- start keys
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder if isPlace (last l) then return (Id l [] nullRange) else do
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder (c, p) <- option ([], nullRange) (comps idKeys)
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder u <- many placeT
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder return (Id (l ++ u) c p)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder-- | the Casl key strings (signs first) with additional keywords
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maedercasl_keys :: [String] -> ([String], [String])
e83ed59502a681713982f25c559aae77a4145734Christian Maedercasl_keys ks = (ks ++ casl_reserved_fops, ks ++ casl_reserved_fwords)
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | Casl ids for operations and predicates
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederparseId :: [String] -> GenParser Char st Id
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederparseId ks = mixId (casl_keys ks) (casl_keys ks)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder-- | disallow 'barS' within the top-level of constructor names
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederconsId :: [String] -> GenParser Char st Id
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian MaederconsId ks = mixId (barS : ks ++ casl_reserved_fops,
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder ks ++ casl_reserved_fwords) $ casl_keys ks
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder{- | Casl sorts are simple words ('varId'),
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder but may have a compound list ('comps') -}
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaedersortId :: [String] -> GenParser Char st Id
e83ed59502a681713982f25c559aae77a4145734Christian MaedersortId ks =
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder do s <- varId ks
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski (c, p) <- option ([], nullRange) (comps $ casl_keys ks)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder return (Id [s] c p)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- * parser for simple 'Id's
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- | parse a simple word not in 'casl_reserved_fwords'
50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaedervarId :: [String] -> GenParser Char st Token
7e4157a70efe2acab30dbe5079bba6db90923785Christian MaedervarId ks = pToken (reserved (ks ++ casl_reserved_fwords) scanAnyWords)
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder-- | like 'varId'. 'Common.Id.SIMPLE_ID' for spec- and view names
90bf4bf40789422552e566b73738ba5efae144c3Christian MaedersimpleId :: GenParser Char st Token
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian MaedersimpleId = pToken (reserved casl_structured_reserved_words scanAnyWords)
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- * parser for key 'Token's
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | parse a question mark key sign ('quMark')
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederquMarkT :: GenParser Char st Token
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederquMarkT = pToken $ toKey quMark
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian Maeder-- | parse a 'colonS' possibly immediately followed by a 'quMark'
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercolonST :: GenParser Char st Token
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian MaedercolonST = pToken $ try $ string colonS << notFollowedBy
1600a2e47d5ed599df94d20411f0767fb6d68587Christian Maeder (satisfy $ \ c -> c /= '?' && isSignChar c)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | parse the product key sign ('prodS' or 'timesS')
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercrossT :: GenParser Char st Token
57c51f0673511217c416090de812b779612e7551Christian MaedercrossT = pToken (toKey prodS <|> toKey timesS) <?> show prodS