Token.hs revision 7325bbe03797fd413af504fb3fac109b2c652a7b
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Authors: Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maeder parser for CASL IDs
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder http://www.cofi.info/Documents/CASL/Summary/
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder from 25 March 2001
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder C.2.1 Basic Specifications with Subsorts
967e5f3c25249c779575864692935627004d3f9eChristian MaederSIMPLE-ID ::= WORDS
967e5f3c25249c779575864692935627004d3f9eChristian MaederID ::= TOKEN-ID | MIXFIX-ID
967e5f3c25249c779575864692935627004d3f9eChristian MaederTOKEN-ID ::= TOKEN
967e5f3c25249c779575864692935627004d3f9eChristian MaederMIXFIX-ID ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder | PLACE-TOKEN-ID ... PLACE-TOKEN-ID
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian MaederPLACE-TOKEN-ID ::= PLACE TOKEN-ID
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaederTOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
967e5f3c25249c779575864692935627004d3f9eChristian Maeder SIGNS are adapted here and more permissive as in the summary
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski WORDS and NO-BRACKET-SIGNS are treated equally
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder legal are, ie. "{a}", "{+}", "a{}="
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder illegal is "a=" (no two SIMPLE-TOKEN stay beside each other)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder SIMPLE-TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder | NO-BRACKET-SIGNS
967e5f3c25249c779575864692935627004d3f9eChristian Maeder STB ::= SIMPLE-TOKEN BRACKETS
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder BST ::= BRACKETS SIMPLE-TOKEN
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder SIGNS ::= BRACKETS
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder | BRACKETS STB ... STB
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder | BRACKETS STB ... STB SIMPLE-TOKEN
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder | SIMPLE-TOKEN
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder | SIMPLE-TOKEN BST ... BST
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder | SIMPLE-TOKEN BST ... BST BRACKETS
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder A SIMPLE-TOKEN followed by "[" outside nested brackets
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder will be taken as the beginning of a compound list.
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Within SIGNS brackets need not be balanced,
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder only after their composition to a MIXFIX-ID.
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder BRACKETS = BRACKET ... BRACKET
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder BRACKET ::= [ | ] | { | }
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder 2.4 Identifiers
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder brackets/braces within MIXFIX-ID must be balanced
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder C.2.2 Structured Specifications
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder TOKEN-ID ::= ... | TOKEN [ ID ,..., ID ]
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder A compound list must follow the last TOKEN within MIXFIX-ID,
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder so a compound list is never nested within (balanced) mixfix BRACKETS.
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Only PLACEs may follow a compound list.
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder The IDs within the compound list may surely be compound IDs again.
d48085f765fca838c1d972d2123601997174583dChristian Maederimport Common.Id (Id(Id), Token(..), Pos, toPos, isPlace)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- ----------------------------------------------
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-- casl keyword handling
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- ----------------------------------------------
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedercasl_reserved_ops, formula_ops, casl_reserved_fops :: [String]
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedercasl_reserved_ops = [colonS, colonS++quMark, defnS, dotS, cDot, mapsTo]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- these signs are legal in terms, but illegal in declarations
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederformula_ops = [equalS, implS, equivS, lOr, lAnd, negS]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedercasl_reserved_fops = formula_ops ++ casl_reserved_ops
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-- letter keywords
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedercasl_reserved_words, formula_words, casl_reserved_fwords :: [String]
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedercasl_reserved_words =
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder [andS, archS, asS, assocS, axiomS, axiomS ++ sS, closedS, commS, endS,
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder existsS, fitS, forallS, freeS, fromS, generatedS, getS, givenS,
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder hideS, idemS, inS, lambdaS, libraryS, localS, logicS,
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder opS, opS ++ sS, predS, predS ++ sS, propS, propS ++ sS, resultS, revealS,
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sortS, sortS ++ sS, specS, thenS, toS, typeS, typeS ++ sS,
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder unitS, unitS ++ sS, varS, varS ++ sS, versionS, viewS, withS, withinS]
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-- these words are legal in terms, but illegal in declarations
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederformula_words = [defS, elseS, ifS, whenS, falseS, notS, trueS]
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maedercasl_reserved_fwords = formula_words ++ casl_reserved_words
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- ----------------------------------------------
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- bracket-token (for ids)
20e16bdd7481741d0b6b14f952aea42ee7a65efbChristian Maeder-- pass list of key symbols and keuwords as parameter
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- ----------------------------------------------
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- simple id (but more than only words)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedersid :: ([String], [String]) -> GenParser Char st Token
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedersid (kOps, kWords) = pToken (scanQuotedChar <|> scanDotWords
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder <|> scanDigit <|> reserved kOps scanAnySigns
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder <|> reserved kWords scanAnyWords <?> "simple-id")
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder-- balanced mixfix-components {...}, [...]
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederbraceP, bracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederbraceP p = begDoEnd oBraceT p cBraceT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederbracketP p = begDoEnd oBracketT p cBracketT
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder-- alternating sid and other mixfix components (including places)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- no two sid stand side by side
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinnerMix1, innerMix2 :: ([String], [String]) -> GenParser Char st [Token]
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinnerMix1 l = sid l <:> option [] (innerMix2 l)
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinnerMix2 l = let p = innerList l in
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder flat (many1 (braceP p <|> bracketP p <|> many1 placeT))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <++> option [] (innerMix1 l)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- ingredients starting either with an sid or brackets, braces or place
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederinnerList :: ([String], [String]) -> GenParser Char st [Token]
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederinnerList l = option [] (innerMix1 l <|> innerMix2 l <?> "token")
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder-- a mixfix component starting with an sid (outside innerList)
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedertopMix1, topMix2, topMix3 :: ([String], [String]) -> GenParser Char st [Token]
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedertopMix1 l = sid l <:> option [] (topMix2 l)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-- following an sid only braced mixfix-components are acceptable
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-- square brackets after an sid will be taken as compound part
967e5f3c25249c779575864692935627004d3f9eChristian MaedertopMix2 l = flat (many1 (braceP $ innerList l)) <++> option [] (topMix1 l)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- square brackets (as mixfix component) are ok following a place
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedertopMix3 l = let p = innerList l in
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder bracketP p <++> flat (many (braceP p))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <++> option [] (topMix1 l)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederafterPlace, middle :: ([String], [String]) -> GenParser Char st [Token]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederafterPlace l = topMix1 l <|> topMix2 l<|> topMix3 l
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- places and something balanced possibly including places as well
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedermiddle l = many1 placeT <++> option [] (afterPlace l)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- balanced stuff interspersed with places
967e5f3c25249c779575864692935627004d3f9eChristian MaedertokStart, start :: ([String], [String]) -> GenParser Char st [Token]
967e5f3c25249c779575864692935627004d3f9eChristian MaedertokStart l = afterPlace l <++> flat (many (middle l))
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- at least two places on its own or a non-place possibly preceded by places
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederstart l = tokStart l <|> placeT <:> (tokStart l <|>
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder many1 placeT <++> option [] (tokStart l))
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- ----------------------------------------------
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- mixfix and compound ids
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- ----------------------------------------------
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- a compound list
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maedercomps :: ([String], [String]) -> GenParser Char st ([Id], [Pos])
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maedercomps keys = do o <- oBracketT
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (ts, ps) <- mixId keys keys `separatedBy` commaT
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder c <- cBracketT
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder return (ts, toPos o ps c)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder <?> "[<id>,...,<id>]"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- a compound list does not follow a place
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- but after a compound list further places may follow
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- keywords within components may be different
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermixId :: ([String], [String]) -> ([String], [String]) -> GenParser Char st Id
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermixId keys idKeys =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder do l <- start keys
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder if isPlace (last l) then return (Id l [] [])
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else do (c, p) <- option ([], []) (comps idKeys)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder u <- many placeT
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder return (Id (l++u) c p)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- ----------------------------------------------
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- CASL mixfix Ids
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- ----------------------------------------------
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedercasl_keys :: ([String], [String])
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedercasl_keys = (casl_reserved_fops, casl_reserved_fwords)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederparseId, casl_id :: GenParser Char st Id
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederparseId = mixId casl_keys casl_keys
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedercasl_id = parseId
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- disallow barS within (the top-level) constructor names
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederconsId :: GenParser Char st Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederconsId = mixId (barS:casl_reserved_fops, casl_reserved_fwords) casl_keys
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder-- ----------------------------------------------
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- ----------------------------------------------
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- no compound ids (just a word)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedervarId :: GenParser Char st Token
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedervarId = pToken (reserved casl_reserved_fwords scanAnyWords)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder-- ----------------------------------------------
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder-- ----------------------------------------------
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- sortIds are words, but possibly compound ids
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedersortId :: GenParser Char st Id
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedersortId = do s <- varId
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (c, p) <- option ([], []) (comps casl_keys)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder return (Id [s] c p)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder------------------------------------------------------------------------
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- simpleIds for spec- and view-name
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder------------------------------------------------------------------------
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedersimpleId :: GenParser Char st Token
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedersimpleId = varId
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- ----------------------------------------------