{- |
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"
-}

{- http://www.cofi.info/Documents/CASL/Summary/
   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

import Text.ParserCombinators.Parsec

-- * Casl keyword lists

-- | reserved signs
casl_reserved_ops :: [String]
casl_reserved_ops :: [String]
casl_reserved_ops = [String
colonS, String
colonQuMark, String
defnS, String
dotS, String
cDot, String
mapsTo]

-- | these formula signs are legal in terms, but illegal in declarations
formula_ops :: [String]
formula_ops :: [String]
formula_ops = [String
equalS, String
implS, String
equivS, String
lOr, String
lAnd, String
negS]

-- | all reseverd signs
casl_reserved_fops :: [String]
casl_reserved_fops :: [String]
casl_reserved_fops = [String]
formula_ops [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_ops

-- | reserved keywords
casl_basic_reserved_words :: [String]
casl_basic_reserved_words :: [String]
casl_basic_reserved_words =
    [String
axiomS, String
axiomS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
cogeneratedS, String
cotypeS, String
cotypeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS,
     String
esortS, String
esortS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
etypeS, String
etypeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS,
     String
existsS, String
forallS, String
freeS, String
generatedS,
     String
opS, String
opS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
predS, String
predS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS,
     String
sortS, String
sortS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
typeS, String
typeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
varS, String
varS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS]

-- | reserved keywords
casl_structured_reserved_words :: [String]
casl_structured_reserved_words :: [String]
casl_structured_reserved_words = String
libraryS String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
    [String]
continuationKeywords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
otherStartKeywords
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
criticalKeywords

-- | keywords terminating a basic spec or starting a new library item
criticalKeywords :: [String]
criticalKeywords :: [String]
criticalKeywords = [String]
terminatingKeywords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
startingKeywords

-- | keywords terminating a basic spec
terminatingKeywords :: [String]
terminatingKeywords :: [String]
terminatingKeywords =
    [ String
andS, String
endS, String
extractS, String
fitS, String
forgetS, String
hideS, String
keepS, String
rejectS, String
removeS, 
      String
revealS, String
selectS, String
thenS, String
withS, String
withinS, String
ofS, String
forS, String
toS, String
intersectS]

-- | keywords starting a library item
startingKeywords :: [String]
startingKeywords :: [String]
startingKeywords =
    [ String
archS, String
fromS, String
logicS, String
newlogicS, String
refinementS, String
specS, String
unitS, String
viewS
    , String
ontologyS, String
alignmentS, String
networkS, String
equivalenceS, String
newcomorphismS
    , String
interpretationS, String
entailmentS ]

-- | keywords that may follow a defining equal sign
otherStartKeywords :: [String]
otherStartKeywords :: [String]
otherStartKeywords =
    [String
closedS, String
cofreeS, String
freeS, String
localS, String
unitS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sS, String
combineS]

-- | other intermediate keywords
continuationKeywords :: [String]
continuationKeywords :: [String]
continuationKeywords =
    [ String
behaviourallyS, String
getS, String
givenS, String
lambdaS, String
refinedS, String
resultS, String
toS, String
versionS
    , String
excludingS, String
entailsS ]

-- | reserved keywords
casl_reserved_words :: [String]
casl_reserved_words :: [String]
casl_reserved_words =
   [String]
casl_basic_reserved_words [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_structured_reserved_words

-- | these formula words are legal in terms, but illegal in declarations
formula_words :: [String]
formula_words :: [String]
formula_words = [String
asS, String
defS, String
elseS, String
ifS, String
inS, String
whenS, String
falseS, String
notS, String
trueS]

-- | all reserved words
casl_reserved_fwords :: [String]
casl_reserved_fwords :: [String]
casl_reserved_fwords = [String]
formula_words [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
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 :: ([String], [String]) -> GenParser Char st Token
sid (kOps :: [String]
kOps, kWords :: [String]
kWords) = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String
forall st. CharParser st String
scanQuotedChar CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st String
forall st. CharParser st String
scanDotWords
                CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st String
forall st. CharParser st String
scanDigit CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
kOps CharParser st String
forall st. CharParser st String
scanAnySigns
                CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
kWords CharParser st String
forall st. CharParser st String
scanAnyWords CharParser st String -> String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "simple-id")

-- * 'Token' lists parsers

-- | balanced mixfix components within braces
braceP :: GenParser Char st [Token] -> GenParser Char st [Token]
braceP :: GenParser Char st [Token] -> GenParser Char st [Token]
braceP p :: GenParser Char st [Token]
p = CharParser st Token
forall st. CharParser st Token
oBraceT CharParser st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> GenParser Char st [Token]
p GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> CharParser st Token -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single CharParser st Token
forall st. CharParser st Token
cBraceT
           GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st Token
forall st. CharParser st Token
oBracketT CharParser st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> CharParser st Token -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single CharParser st Token
forall st. CharParser st Token
cBracketT)
-- | balanced mixfix components within square brackets
bracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
bracketP :: GenParser Char st [Token] -> GenParser Char st [Token]
bracketP p :: GenParser Char st [Token]
p = CharParser st Token
forall st. CharParser st Token
oBracketT CharParser st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> GenParser Char st [Token]
p GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> CharParser st Token -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single CharParser st Token
forall st. CharParser st Token
cBracketT

{- | an 'sid' optionally followed by other mixfix components
   (without no two consecutive 'sid's) -}
innerMix1 :: ([String], [String]) -> GenParser Char st [Token]
innerMix1 :: ([String], [String]) -> GenParser Char st [Token]
innerMix1 l :: ([String], [String])
l = ([String], [String]) -> GenParser Char st Token
forall st. ([String], [String]) -> GenParser Char st Token
sid ([String], [String])
l GenParser Char st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerMix2 ([String], [String])
l)

-- | mixfix components not starting with a 'sid' (possibly places)
innerMix2 :: ([String], [String]) -> GenParser Char st [Token]
innerMix2 :: ([String], [String]) -> GenParser Char st [Token]
innerMix2 l :: ([String], [String])
l = let p :: GenParser Char st [Token]
p = ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerList ([String], [String])
l in
                  ParsecT String st Identity [[Token]] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (GenParser Char st [Token] -> ParsecT String st Identity [[Token]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (GenParser Char st [Token] -> GenParser Char st [Token]
forall st. GenParser Char st [Token] -> GenParser Char st [Token]
braceP GenParser Char st [Token]
forall st. GenParser Char st [Token]
p GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char st [Token] -> GenParser Char st [Token]
forall st. GenParser Char st [Token] -> GenParser Char st [Token]
bracketP GenParser Char st [Token]
forall st. GenParser Char st [Token]
p GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String st Identity Token -> GenParser Char st [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String st Identity Token
forall st. CharParser st Token
placeT))
                           GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerMix1 ([String], [String])
l)

-- | any mixfix components within braces or brackets
innerList :: ([String], [String]) -> GenParser Char st [Token]
innerList :: ([String], [String]) -> GenParser Char st [Token]
innerList l :: ([String], [String])
l = GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerMix1 ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerMix2 ([String], [String])
l GenParser Char st [Token] -> String -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "token")

-- | mixfix components starting with a 'sid' (outside 'innerList')
topMix1 :: ([String], [String]) -> GenParser Char st [Token]
topMix1 :: ([String], [String]) -> GenParser Char st [Token]
topMix1 l :: ([String], [String])
l = ([String], [String]) -> GenParser Char st Token
forall st. ([String], [String]) -> GenParser Char st Token
sid ([String], [String])
l GenParser Char st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix2 ([String], [String])
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 :: ([String], [String]) -> GenParser Char st [Token]
topMix2 l :: ([String], [String])
l = ParsecT String st Identity [[Token]] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (GenParser Char st [Token] -> ParsecT String st Identity [[Token]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (GenParser Char st [Token] -> GenParser Char st [Token]
forall st. GenParser Char st [Token] -> GenParser Char st [Token]
braceP (GenParser Char st [Token] -> GenParser Char st [Token])
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall a b. (a -> b) -> a -> b
$ ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerList ([String], [String])
l)) GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix1 ([String], [String])
l)

{- | mixfix components starting with square brackets ('bracketP')
   that may follow a place ('placeT') (outside 'innerList') -}
topMix3 :: ([String], [String]) -> GenParser Char st [Token]
topMix3 :: ([String], [String]) -> GenParser Char st [Token]
topMix3 l :: ([String], [String])
l = let p :: GenParser Char st [Token]
p = ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
innerList ([String], [String])
l in
                GenParser Char st [Token] -> GenParser Char st [Token]
forall st. GenParser Char st [Token] -> GenParser Char st [Token]
bracketP GenParser Char st [Token]
forall st. GenParser Char st [Token]
p GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> ParsecT String st Identity [[Token]] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (GenParser Char st [Token] -> ParsecT String st Identity [[Token]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (GenParser Char st [Token] -> GenParser Char st [Token]
forall st. GenParser Char st [Token] -> GenParser Char st [Token]
braceP GenParser Char st [Token]
forall st. GenParser Char st [Token]
p))
                             GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix1 ([String], [String])
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 :: ([String], [String]) -> GenParser Char st [Token]
afterPlace l :: ([String], [String])
l = ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix1 ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix2 ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
topMix3 ([String], [String])
l

-- | places possibly followed by other ('afterPlace') mixfix components
middle :: ([String], [String]) -> GenParser Char st [Token]
middle :: ([String], [String]) -> GenParser Char st [Token]
middle l :: ([String], [String])
l = ParsecT String st Identity Token -> GenParser Char st [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String st Identity Token
forall st. CharParser st Token
placeT GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
afterPlace ([String], [String])
l)

{- | many (balanced, top-level) mixfix components ('afterPlace')
   possibly interspersed with multiple places ('placeT') -}
tokStart :: ([String], [String]) -> GenParser Char st [Token]
tokStart :: ([String], [String]) -> GenParser Char st [Token]
tokStart l :: ([String], [String])
l = ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
afterPlace ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> ParsecT String st Identity [[Token]] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (GenParser Char st [Token] -> ParsecT String st Identity [[Token]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
middle ([String], [String])
l))

{- | any (balanced, top-level) mixfix components
   possibly starting with places but no single 'placeT' only. -}
start :: ([String], [String]) -> GenParser Char st [Token]
start :: ([String], [String]) -> GenParser Char st [Token]
start l :: ([String], [String])
l = ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
tokStart ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser st Token
forall st. CharParser st Token
placeT CharParser st Token
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
tokStart ([String], [String])
l GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                                 CharParser st Token -> GenParser Char st [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 CharParser st Token
forall st. CharParser st Token
placeT GenParser Char st [Token]
-> GenParser Char st [Token] -> GenParser Char st [Token]
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> GenParser Char st [Token] -> GenParser Char st [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
tokStart ([String], [String])
l))
                                     GenParser Char st [Token] -> String -> GenParser Char st [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "id"

-- * parser for mixfix and compound 'Id's

-- | parsing a compound list
comps :: ([String], [String]) -> GenParser Char st ([Id], Range)
comps :: ([String], [String]) -> GenParser Char st ([Id], Range)
comps keys :: ([String], [String])
keys = do
  Token
o <- CharParser st Token
forall st. CharParser st Token
oBracketT
  (ts :: [Id]
ts, ps :: [Token]
ps) <- ([String], [String])
-> ([String], [String]) -> GenParser Char st Id
forall st.
([String], [String])
-> ([String], [String]) -> GenParser Char st Id
mixId ([String], [String])
keys ([String], [String])
keys GenParser Char st Id
-> CharParser st Token -> GenParser Char st ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser st Token
forall st. CharParser st Token
commaT
  Token
c <- CharParser st Token
forall st. CharParser st Token
cBracketT
  ([Id], Range) -> GenParser Char st ([Id], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id]
ts, Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
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 :: ([String], [String])
-> ([String], [String]) -> GenParser Char st Id
mixId keys :: ([String], [String])
keys idKeys :: ([String], [String])
idKeys = do
  [Token]
l <- ([String], [String]) -> GenParser Char st [Token]
forall st. ([String], [String]) -> GenParser Char st [Token]
start ([String], [String])
keys
  if Token -> Bool
isPlace ([Token] -> Token
forall a. [a] -> a
last [Token]
l) then Id -> GenParser Char st Id
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> [Id] -> Range -> Id
Id [Token]
l [] Range
nullRange) else do
    (c :: [Id]
c, p :: Range
p) <- ([Id], Range)
-> ParsecT String st Identity ([Id], Range)
-> ParsecT String st Identity ([Id], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) (([String], [String]) -> ParsecT String st Identity ([Id], Range)
forall st. ([String], [String]) -> GenParser Char st ([Id], Range)
comps ([String], [String])
idKeys)
    [Token]
u <- ParsecT String st Identity Token -> GenParser Char st [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String st Identity Token
forall st. CharParser st Token
placeT
    Id -> GenParser Char st Id
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> [Id] -> Range -> Id
Id ([Token]
l [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
u) [Id]
c Range
p)

-- | the Casl key strings (signs first) with additional keywords
casl_keys :: [String] -> ([String], [String])
casl_keys :: [String] -> ([String], [String])
casl_keys ks :: [String]
ks = ([String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fops, [String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fwords)

-- | Casl ids for operations and predicates
parseId :: [String] -> GenParser Char st Id
parseId :: [String] -> GenParser Char st Id
parseId ks :: [String]
ks = ([String], [String])
-> ([String], [String]) -> GenParser Char st Id
forall st.
([String], [String])
-> ([String], [String]) -> GenParser Char st Id
mixId ([String] -> ([String], [String])
casl_keys [String]
ks) ([String] -> ([String], [String])
casl_keys [String]
ks)

-- | disallow 'barS' within the top-level of constructor names
consId :: [String] -> GenParser Char st Id
consId :: [String] -> GenParser Char st Id
consId ks :: [String]
ks = ([String], [String])
-> ([String], [String]) -> GenParser Char st Id
forall st.
([String], [String])
-> ([String], [String]) -> GenParser Char st Id
mixId (String
barS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fops,
                   [String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fwords) (([String], [String]) -> GenParser Char st Id)
-> ([String], [String]) -> GenParser Char st Id
forall a b. (a -> b) -> a -> b
$ [String] -> ([String], [String])
casl_keys [String]
ks

{- | Casl sorts are simple words ('varId'),
   but may have a compound list ('comps') -}
sortId :: [String] -> GenParser Char st Id
sortId :: [String] -> GenParser Char st Id
sortId ks :: [String]
ks =
    do Token
s <- [String] -> GenParser Char st Token
forall st. [String] -> GenParser Char st Token
varId [String]
ks
       (c :: [Id]
c, p :: Range
p) <- ([Id], Range)
-> ParsecT String st Identity ([Id], Range)
-> ParsecT String st Identity ([Id], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) (([String], [String]) -> ParsecT String st Identity ([Id], Range)
forall st. ([String], [String]) -> GenParser Char st ([Id], Range)
comps (([String], [String]) -> ParsecT String st Identity ([Id], Range))
-> ([String], [String]) -> ParsecT String st Identity ([Id], Range)
forall a b. (a -> b) -> a -> b
$ [String] -> ([String], [String])
casl_keys [String]
ks)
       Id -> GenParser Char st Id
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> [Id] -> Range -> Id
Id [Token
s] [Id]
c Range
p)

-- * parser for simple 'Id's

-- | parse a simple word not in 'casl_reserved_fwords'
varId :: [String] -> GenParser Char st Token
varId :: [String] -> GenParser Char st Token
varId ks :: [String]
ks = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken ([String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved ([String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
casl_reserved_fwords) CharParser st String
forall st. CharParser st String
scanAnyWords)

-- | non-skipping version for simple ids
nonSkippingSimpleId :: GenParser Char st Token
nonSkippingSimpleId :: GenParser Char st Token
nonSkippingSimpleId =
  CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
parseToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ [String] -> CharParser st String -> CharParser st String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
casl_reserved_words CharParser st String
forall st. CharParser st String
scanAnyWords

-- | like 'varId'.  'Common.Id.SIMPLE_ID' for spec- and view names
simpleId :: GenParser Char st Token
simpleId :: GenParser Char st Token
simpleId = GenParser Char st Token
forall st. CharParser st Token
nonSkippingSimpleId GenParser Char st Token
-> ParsecT String st Identity () -> GenParser Char st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String st Identity ()
forall st. CharParser st ()
skipSmart

-- * parser for key 'Token's

-- | parse a question mark key sign ('quMark')
quMarkT :: GenParser Char st Token
quMarkT :: GenParser Char st Token
quMarkT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
quMark

-- | parse a 'colonS' possibly immediately followed by a 'quMark'
colonST :: GenParser Char st Token
colonST :: GenParser Char st Token
colonST = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ CharParser st String -> CharParser st String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (CharParser st String -> CharParser st String)
-> CharParser st String -> CharParser st String
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
colonS CharParser st String
-> ParsecT String st Identity () -> CharParser st String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String st Identity Char -> ParsecT String st Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy
    ((Char -> Bool) -> ParsecT String st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String st Identity Char)
-> (Char -> Bool) -> ParsecT String st Identity Char
forall a b. (a -> b) -> a -> b
$ \ c :: Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '?' Bool -> Bool -> Bool
&& Char -> Bool
isSignChar Char
c)

-- | parse the product key sign ('prodS' or 'timesS')
crossT :: GenParser Char st Token
crossT :: GenParser Char st Token
crossT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (String -> CharParser st String
forall st. String -> CharParser st String
toKey String
prodS CharParser st String
-> CharParser st String -> CharParser st String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser st String
forall st. String -> CharParser st String
toKey String
timesS) GenParser Char st Token -> String -> GenParser Char st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String -> String
forall a. Show a => a -> String
show String
prodS