content: {- |
  Module      :  ./CASL/OpItem.hs
  Description :  Parser for OP-ITEMs (operation declarations and definitions)
  Copyright   :  (c) Christian Maeder, Uni Bremen 2002-2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Parser for OP-ITEMs (operation declarations and definitions)
  -}
  
  {-
     parse OP-ITEM and "op/ops OP-ITEM ; ... ; OP-ITEM"
     parse PRED-ITEM and "op/ops PRED-ITEM ; ... ; PRED-ITEM"
  
     http://www.cofi.info/Documents/CASL/Summary/
     from 25 March 2001
  
     C.2.1 Basic Specifications with Subsorts
  -}
  
  module CASL.OpItem (opItem, opHead, predItem) where
  
  import Common.AnnoState
  import Common.Id
  import Common.Keywords
  import Common.Lexer
  import CASL.AS_Basic_CASL
  import Common.AS_Annotation
  import Text.ParserCombinators.Parsec
  import Common.Token
  import CASL.Formula
  import Data.List (sort)
  
  -- non-empty
  predHead :: [String] -> AParser st PRED_HEAD
  predHead ks =
      do o <- wrapAnnos oParenT
         (vs, ps) <- varDecls ks
         p <- addAnnos >> cParenT
         return $ Pred_head vs $ catRange (o : ps ++ [p])
  
  opHead :: [String] -> AParser st OP_HEAD
  opHead ks =
      do Pred_head vs ps <- predHead ks
         do
           c <- anColon
           (b, s, qs) <- opSort ks
           return $ Op_head (if b then Partial else Total) vs (Just s)
                (ps `appRange` tokPos c `appRange` qs)
          <|> return (Op_head Partial vs Nothing ps)
  
  opAttr :: TermParser f => [String] -> AParser st (OP_ATTR f, Token)
  opAttr ks = choice
    (map (\ (s, t) -> fmap (\ p -> (t, p)) $ asKey s)
      [(assocS, Assoc_op_attr), (commS, Comm_op_attr), (idemS, Idem_op_attr)])
    <|> do
      p <- asKey unitS
      t <- term ks
      return (Unit_op_attr t, p)
  
  opItem :: TermParser f => [String] -> AParser st (OP_ITEM f)
  opItem ks = do
      (os, cs) <- parseId ks `separatedBy` anComma
      case os of
        [o] -> do
            c <- anColon
            t@(Op_type k args s ps) <- opType ks
            case args of
              [] -> opBody ks o (Op_head k [] (Just s) $ appRange ps $ tokPos c)
                <|> opAttrs ks os t [c]  -- this always succeeds
              _ -> opAttrs ks os t [c]
          <|> (opHead ks >>= opBody ks o)
          -- require sort: <|> opBody ks o (Op_head Partial [] Nothing nullRange)
        _ -> do
          c <- anColon
          t <- opType ks
          opAttrs ks os t $ cs ++ [c]
  
  opBody :: TermParser f => [String] -> OP_NAME -> OP_HEAD
         -> AParser st (OP_ITEM f)
  opBody ks o h =
      do e <- equalT
         a <- annos
         t <- term ks
         return $ Op_defn o h (Annoted t nullRange a []) $ tokPos e
  
  opAttrs :: TermParser f => [String] -> [OP_NAME] -> OP_TYPE -> [Token]
          -> AParser st (OP_ITEM f)
  opAttrs ks os t c =
      do q <- anComma
         (as, cs) <- opAttr ks `separatedBy` anComma
         let ps = Range (sort (catPosAux (c ++ map snd as ++ (q : cs))))
         return (Op_decl os t (map fst as) ps)
     <|> return (Op_decl os t [] (catRange c))
  -- overlap "o:t" DEF-or DECL "o:t=e" or "o:t, assoc"
  
  -- * predicates
  
  predItem :: TermParser f => [String] -> AParser st (PRED_ITEM f)
  predItem ks =
      do (ps, cs) <- parseId ks `separatedBy` anComma
         if isSingle ps then
                  predBody ks (head ps) (Pred_head [] nullRange)
                  <|> (predHead ks >>= predBody ks (head ps))
                  <|> predTypeCont ks ps cs
           else predTypeCont ks ps cs
  
  predBody :: TermParser f => [String] -> PRED_NAME -> PRED_HEAD
           -> AParser st (PRED_ITEM f)
  predBody ks p h =
      do e <- asKey equivS
         a <- annos
         f <- formula ks
         return $ Pred_defn p h (Annoted f nullRange a []) $ tokPos e
  
  predTypeCont :: [String] -> [PRED_NAME] -> [Token] -> AParser st (PRED_ITEM f)
  predTypeCont ks ps cs =
      do c <- colonT
         t <- predType ks
         return $ Pred_decl ps t $ catRange (cs ++ [c])
  