{- |
Module : ./Common/Token.hs
Description : parser for CASL 'Id's based on "Common.Lexer"
Copyright : (c) Christian Maeder and Uni Bremen 2002-2004
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
Parser for CASL 'Id's based on "Common.Lexer"
-}
from 25 March 2001
C.2.1 Basic Specifications with Subsorts
SIMPLE-ID ::= WORDS
ID ::= TOKEN-ID | MIXFIX-ID
TOKEN-ID ::= TOKEN
MIXFIX-ID ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
| PLACE-TOKEN-ID ... PLACE-TOKEN-ID
PLACE-TOKEN-ID ::= PLACE TOKEN-ID
| PLACE
PLACE ::= __
TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
| SIGNS
SIGNS are adapted here and more permissive as in the summary
WORDS and NO-BRACKET-SIGNS are treated equally
legal are, ie. "{a}", "{+}", "a{}="
illegal is "a=" (no two SIMPLE-TOKEN stay beside each other)
SIMPLE-TOKEN ::= WORDS | DOT-WORDS | DIGIT | QUOTED-CHAR
| NO-BRACKET-SIGNS
STB ::= SIMPLE-TOKEN BRACKETS
BST ::= BRACKETS SIMPLE-TOKEN
SIGNS ::= BRACKETS
| BRACKETS STB ... STB
| BRACKETS STB ... STB SIMPLE-TOKEN
| SIMPLE-TOKEN
| SIMPLE-TOKEN BST ... BST
| SIMPLE-TOKEN BST ... BST BRACKETS
A SIMPLE-TOKEN followed by "[" outside nested brackets
will be taken as the beginning of a compound list.
Within SIGNS brackets need not be balanced,
only after their composition to a MIXFIX-ID.
BRACKETS = BRACKET ... BRACKET
BRACKET ::= [ | ] | { | }
2.4 Identifiers
brackets/braces within MIXFIX-ID must be balanced
C.2.2 Structured Specifications
TOKEN-ID ::= ... | TOKEN [ ID ,..., ID ]
A compound list must follow the last TOKEN within MIXFIX-ID,
so a compound list is never nested within (balanced) mixfix BRACKETS.
Only PLACEs may follow a compound list.
The IDs within the compound list may surely be compound IDs again.
-}
module Common.Token where
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
-- * Casl keyword lists
-- | reserved signs
casl_reserved_ops :: [String]
casl_reserved_ops = [colonS, colonQuMark, defnS, dotS, cDot, mapsTo]
-- | these formula signs are legal in terms, but illegal in declarations
formula_ops :: [String]
formula_ops = [equalS, implS, equivS, lOr, lAnd, negS]
-- | all reseverd signs
casl_reserved_fops :: [String]
casl_reserved_fops = formula_ops ++ casl_reserved_ops
-- | reserved keywords
casl_basic_reserved_words :: [String]
casl_basic_reserved_words =
[axiomS, axiomS ++ sS, cogeneratedS, cotypeS, cotypeS ++ sS,
esortS, esortS ++ sS, etypeS, etypeS ++ sS,
existsS, forallS, freeS, generatedS,
opS, opS ++ sS, predS, predS ++ sS,
sortS, sortS ++ sS, typeS, typeS ++ sS, varS, varS ++ sS]
-- | reserved keywords
casl_structured_reserved_words :: [String]
casl_structured_reserved_words = libraryS :
continuationKeywords ++ otherStartKeywords
++ criticalKeywords
-- | keywords terminating a basic spec or starting a new library item
criticalKeywords :: [String]
criticalKeywords = terminatingKeywords ++ startingKeywords
-- | keywords terminating a basic spec
terminatingKeywords :: [String]
terminatingKeywords =
[ andS, endS, extractS, fitS, forgetS, hideS, keepS, rejectS, removeS,
revealS, selectS, thenS, withS, withinS, ofS, forS, toS, intersectS]
-- | keywords starting a library item
startingKeywords :: [String]
startingKeywords =
[ archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS
, ontologyS, alignmentS, networkS, equivalenceS, newcomorphismS
, interpretationS, entailmentS ]
-- | keywords that may follow a defining equal sign
otherStartKeywords :: [String]
otherStartKeywords =
[closedS, cofreeS, freeS, localS, unitS ++ sS, combineS]
-- | other intermediate keywords
continuationKeywords :: [String]
continuationKeywords =
[ behaviourallyS, getS, givenS, lambdaS, refinedS, resultS, toS, versionS
, excludingS, entailsS ]
-- | reserved keywords
casl_reserved_words :: [String]
casl_reserved_words =
casl_basic_reserved_words ++ casl_structured_reserved_words
-- | these formula words are legal in terms, but illegal in declarations
formula_words :: [String]
formula_words = [asS, defS, elseS, ifS, inS, whenS, falseS, notS, trueS]
-- | all reserved words
casl_reserved_fwords :: [String]
casl_reserved_fwords = formula_words ++ casl_reserved_words
-- * a single 'Token' parser taking lists of key symbols and words as parameter
{- | a simple 'Token' parser depending on reserved signs and words
(including a quoted char, dot-words or a single digit) -}
sid :: ([String], [String]) -> GenParser Char st Token
sid (kOps, kWords) = pToken (scanQuotedChar <|> scanDotWords
<|> scanDigit <|> reserved kOps scanAnySigns
<|> reserved kWords scanAnyWords <?> "simple-id")
-- * 'Token' lists parsers
-- | balanced mixfix components within braces
braceP :: GenParser Char st [Token] -> GenParser Char st [Token]
braceP p = oBraceT <:> p <++> single cBraceT
<|> try (oBracketT <:> single cBracketT)
-- | balanced mixfix components within square brackets
bracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
bracketP p = oBracketT <:> p <++> single cBracketT
{- | an 'sid' optionally followed by other mixfix components
(without no two consecutive 'sid's) -}
innerMix1 :: ([String], [String]) -> GenParser Char st [Token]
innerMix1 l = sid l <:> optionL (innerMix2 l)
-- | mixfix components not starting with a 'sid' (possibly places)
innerMix2 :: ([String], [String]) -> GenParser Char st [Token]
innerMix2 l = let p = innerList l in
flat (many1 (braceP p <|> bracketP p <|> many1 placeT))
<++> optionL (innerMix1 l)
-- | any mixfix components within braces or brackets
innerList :: ([String], [String]) -> GenParser Char st [Token]
innerList l = optionL (innerMix1 l <|> innerMix2 l <?> "token")
-- | mixfix components starting with a 'sid' (outside 'innerList')
topMix1 :: ([String], [String]) -> GenParser Char st [Token]
topMix1 l = sid l <:> optionL (topMix2 l)
{- | mixfix components starting with braces ('braceP')
that may follow 'sid' outside 'innerList'.
(Square brackets after a 'sid' will be taken as a compound list.) -}
topMix2 :: ([String], [String]) -> GenParser Char st [Token]
topMix2 l = flat (many1 (braceP $ innerList l)) <++> optionL (topMix1 l)
{- | mixfix components starting with square brackets ('bracketP')
that may follow a place ('placeT') (outside 'innerList') -}
topMix3 :: ([String], [String]) -> GenParser Char st [Token]
topMix3 l = let p = innerList l in
bracketP p <++> flat (many (braceP p))
<++> optionL (topMix1 l)
{- | any ('topMix1', 'topMix2', 'topMix3') mixfix components
that may follow a place ('placeT') at the top level -}
afterPlace :: ([String], [String]) -> GenParser Char st [Token]
afterPlace l = topMix1 l <|> topMix2 l <|> topMix3 l
-- | places possibly followed by other ('afterPlace') mixfix components
middle :: ([String], [String]) -> GenParser Char st [Token]
middle l = many1 placeT <++> optionL (afterPlace l)
{- | many (balanced, top-level) mixfix components ('afterPlace')
possibly interspersed with multiple places ('placeT') -}
tokStart :: ([String], [String]) -> GenParser Char st [Token]
tokStart l = afterPlace l <++> flat (many (middle l))
{- | any (balanced, top-level) mixfix components
possibly starting with places but no single 'placeT' only. -}
start :: ([String], [String]) -> GenParser Char st [Token]
start l = tokStart l <|> placeT <:> (tokStart l <|>
many1 placeT <++> optionL (tokStart l))
<?> "id"
-- * parser for mixfix and compound 'Id's
-- | parsing a compound list
comps :: ([String], [String]) -> GenParser Char st ([Id], Range)
comps keys = do
o <- oBracketT
(ts, ps) <- mixId keys keys `separatedBy` commaT
c <- cBracketT
return (ts, toRange o ps c)
{- | parse mixfix components ('start') and an optional compound list ('comps')
if the last token was no place. Accept possibly further places.
Key strings (second argument) within compound list may differ from
top-level key strings (first argument)!
-}
mixId :: ([String], [String]) -> ([String], [String]) -> GenParser Char st Id
mixId keys idKeys = do
l <- start keys
if isPlace (last l) then return (Id l [] nullRange) else do
(c, p) <- option ([], nullRange) (comps idKeys)
u <- many placeT
return (Id (l ++ u) c p)
-- | the Casl key strings (signs first) with additional keywords
casl_keys :: [String] -> ([String], [String])
casl_keys ks = (ks ++ casl_reserved_fops, ks ++ casl_reserved_fwords)
-- | Casl ids for operations and predicates
parseId :: [String] -> GenParser Char st Id
parseId ks = mixId (casl_keys ks) (casl_keys ks)
-- | disallow 'barS' within the top-level of constructor names
consId :: [String] -> GenParser Char st Id
consId ks = mixId (barS : ks ++ casl_reserved_fops,
ks ++ casl_reserved_fwords) $ casl_keys ks
{- | Casl sorts are simple words ('varId'),
but may have a compound list ('comps') -}
sortId :: [String] -> GenParser Char st Id
sortId ks =
do s <- varId ks
(c, p) <- option ([], nullRange) (comps $ casl_keys ks)
return (Id [s] c p)
-- * parser for simple 'Id's
-- | parse a simple word not in 'casl_reserved_fwords'
varId :: [String] -> GenParser Char st Token
varId ks = pToken (reserved (ks ++ casl_reserved_fwords) scanAnyWords)
-- | non-skipping version for simple ids
nonSkippingSimpleId :: GenParser Char st Token
nonSkippingSimpleId =
parseToken $ reserved casl_reserved_words scanAnyWords
-- | like 'varId'. 'Common.Id.SIMPLE_ID' for spec- and view names
simpleId :: GenParser Char st Token
simpleId = nonSkippingSimpleId << skipSmart
-- * parser for key 'Token's
-- | parse a question mark key sign ('quMark')
quMarkT :: GenParser Char st Token
quMarkT = pToken $ toKey quMark
-- | parse a 'colonS' possibly immediately followed by a 'quMark'
colonST :: GenParser Char st Token
colonST = pToken $ try $ string colonS << notFollowedBy
(satisfy $ \ c -> c /= '?' && isSignChar c)
-- | parse the product key sign ('prodS' or 'timesS')
crossT :: GenParser Char st Token
crossT = pToken (toKey prodS <|> toKey timesS) <?> show prodS