content: {- |
  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 = [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
  