content: {- |
  Module      :  ./CoCASL/Parse_AS.hs
  Description :  Parser for CoCASL
  Copyright   :  (c) Christian Maeder, Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  hausmann@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Parser for CoCASL
  -}
  
  module CoCASL.Parse_AS where
  
  import Common.AnnoState
  import Common.AS_Annotation
  import Common.Id
  import Common.Keywords
  import Common.Lexer
  import Common.Token
  import CoCASL.AS_CoCASL
  import Text.ParserCombinators.Parsec
  import CASL.Formula
  import CASL.Parse_AS_Basic (sigItems)
  import CASL.AS_Basic_CASL
  
  cocasl_reserved_words :: [String]
  cocasl_reserved_words = [diamondS]
  
  parseSen :: AParser st (FORMULA C_FORMULA)
  parseSen = formula cocasl_reserved_words
  
  cocaslFormula :: AParser st C_FORMULA
  cocaslFormula = do
      o <- oBracketT
      m <- modality []
      c <- cBracketT
      f <- formula cocasl_reserved_words
      return (BoxOrDiamond True m f $ toRange o [] c)
    <|> do
      o <- asKey lessS
      m <- modality [greaterS] -- do not consume matching ">"!
      c <- asKey greaterS
      f <- formula cocasl_reserved_words
      return (BoxOrDiamond False m f $ toRange o [] c)
  
  modality :: [String] -> AParser st MODALITY
  modality ks = do
      t <- term (prodS : ks ++ cocasl_reserved_words)
              -- put the term in parens if you need to use "*"
      option () (asKey prodS >> return ())
         -- presence of "*" is not stored yet!
      return $ case t of
        Mixfix_token tok -> Simple_mod tok
        _ -> Term_mod t
  
  instance TermParser C_FORMULA where
    termParser = aToTermParser cocaslFormula
  
  cBasic :: AParser st C_BASIC_ITEM
  cBasic = do
      f <- asKey cofreeS
      ti <- coSigItems
      return (codatatypeToCofreetype ti (tokPos f))
    <|> do
      g <- asKey cogeneratedS
      do t <- sigItems cocasl_reserved_words
         return (CoSort_gen [Annoted t nullRange [] []] $ tokPos g)
        <|> do
          o <- oBraceT
          is <- annosParser (sigItems cocasl_reserved_words)
          c <- cBraceT
          return (CoSort_gen is (toRange g [o] c))
  
  coSigItems :: AParser st C_SIG_ITEM
  coSigItems =
    itemList cocasl_reserved_words cotypeS codatatype CoDatatype_items
  
  codatatype :: [String] -> AParser st CODATATYPE_DECL
  codatatype ks = do
      s <- sortId ks
      addAnnos
      e <- asKey defnS
      addAnnos
      a <- getAnnos
      (Annoted v _ _ b : as, ps) <- acoAlternative ks `separatedBy` barT
      return $ CoDatatype_decl s (Annoted v nullRange a b : as)
        $ catRange $ e : ps
  
  acoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
  acoAlternative ks = do
      a <- coalternative ks
      an <- annos
      return (Annoted a nullRange [] an)
  
  coalternative :: [String] -> AParser st COALTERNATIVE
  coalternative ks = do
      s <- pluralKeyword sortS
      (ts, cs) <- sortId ks `separatedBy` anComma
      return (CoSubsorts ts $ catRange $ s : cs)
    <|> do
      i <- consId ks
      cocomp ks (Just i)
    <|> cocomp ks Nothing
  
  cocomp :: [String] -> Maybe OP_NAME -> AParser st COALTERNATIVE
  cocomp ks i = do
      o <- oParenT
      (cs, ps) <- cocomponent ks `separatedBy` anSemi
      c <- cParenT
      let qs = toRange o ps c
      do q <- quMarkT
         return (Co_construct Partial i cs (qs `appRange` tokPos q))
        <|> return (Co_construct Total i cs qs)
    <|> return (Co_construct Total i [] nullRange)
  
  cocomponent :: [String] -> AParser st COCOMPONENTS
  cocomponent ks = do
      (is, cs) <- parseId ks `separatedBy` anComma
      c <- colonST
      t <- opType ks
      return $ CoSelect is t $ catRange $ cs ++ [c]
  
  instance AParsable C_SIG_ITEM where
    aparser = coSigItems
  
  instance AParsable C_BASIC_ITEM where
    aparser = cBasic
  
  codatatypeToCofreetype :: C_SIG_ITEM -> Range -> C_BASIC_ITEM
  codatatypeToCofreetype d pos = case d of
      CoDatatype_items ts ps -> CoFree_datatype ts (pos `appRange` ps)
  