{- |
Module      :  ./CASL/SymbolParser.hs
Description :  Parser for symbols in translations and reductions
Copyright   :  (c) Christian Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Parsing symbols for translations and reductions
-}

module CASL.SymbolParser
  ( symbItems
  , symbItem
  , symbMapItems
  , opOrPredType
  , symbKind
  ) where

import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.ToDoc ()

import Common.AnnoState
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Token

import Text.ParserCombinators.Parsec

-- | parsing a possibly qualified identifier
symb :: [String] -> SYMB_KIND -> AParser st SYMB
symb ks k = parseId ks >>= \ i -> case k of
    Sorts_kind -> return $ Symb_id i
    _ -> case k of
        Ops_kind -> do
             c <- colonST
             o <- opType ks
             return $ Qual_id i (O_type o) $ tokPos c
        Preds_kind -> do
             c <- colonT
             p <- predType ks
             return $ Qual_id i (P_type p) $ tokPos c
        _ -> do
             c <- colonST
             t <- opOrPredType ks
             return (Qual_id i t $ tokPos c)
     <|> return (Symb_id i)

-- | parsing a type for an operation or a predicate
opOrPredType :: [String] -> AParser st TYPE
opOrPredType ks =
    do (b, s, p) <- opSort ks
       if b then return (O_type (Op_type Partial [] s p))
         else do
           c <- crossT
           (ts, ps) <- sortId ks `separatedBy` crossT
           fmap O_type (opFunSort ks (s : ts) (c : ps))
              <|> return (P_type $ Pred_type (s : ts) $ catRange $ c : ps)
         <|> fmap O_type (opFunSort ks [s] [])
         <|> return (A_type s)
    <|> fmap P_type predUnitType

-- | parsing one symbol or a mapping of one to second symbol
symbMap :: [String] -> SYMB_KIND -> AParser st SYMB_OR_MAP
symbMap ks k =
    do s <- symb ks k
       do
         f <- asKey mapsTo
         k2 <- option Implicit $ fmap fst symbKind
         case joinSymbKinds k k2 of
           Nothing -> fail $ "contradicting symbol kinds '"
             ++ showDoc k "' and '" ++ showDoc k2 "'"
           Just k3 -> do
             t <- symb ks k3
             return (Symb_map s t $ tokPos f)
        <|> return (Symb s)

joinSymbKinds :: SYMB_KIND -> SYMB_KIND -> Maybe SYMB_KIND
joinSymbKinds k1 k2 = case k1 of
  Implicit -> Just k2
  _ -> if k2 == Implicit || k1 == k2 then Just k1 else Nothing

-- | parse a kind keyword
symbKind :: AParser st (SYMB_KIND, Token)
symbKind =
  choice (map (\ (v, s) -> do
    q <- pluralKeyword s
    return (v, q))
  [(Sorts_kind, sortS), (Ops_kind, opS), (Preds_kind, predS)])
  <?> "kind"

{- | Parse a possible kinded list of comma separated CASL symbols.
     The argument is a list of keywords to avoid as identifiers. -}
symbItems :: [String] -> AParser st SYMB_ITEMS
symbItems ks =
    do (is, ps) <- symbs ks Implicit
       return (Symb_items Implicit is $ catRange ps)
    <|>
    do (k, p) <- symbKind
       (is, ps) <- symbs ks k
       return (Symb_items k is $ catRange $ p : ps)

-- | Parse a possible kinded CASL symbol.
symbItem :: [String] -> AParser st SYMB_ITEMS
symbItem ks = do
    i <- symb ks Implicit
    return $ Symb_items Implicit [i] $ getRange i
  <|> do
    (k, p) <- symbKind
    i <- symb ks k
    return $ Symb_items k [i] $ catRange [p]

-- | parse a comma separated list of symbols
symbs :: [String] -> SYMB_KIND -> AParser st ([SYMB], [Token])
symbs ks k =
    do s <- symb ks k
       do
         c <- commaT `followedWith` parseId ks
         (is, ps) <- symbs ks k
         return (s : is, c : ps)
        <|> return ([s], [])

-- | parse a possible kinded list of CASL symbol mappings
symbMapItems :: [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems ks =
    do (is, ps) <- symbMaps ks Implicit
       return (Symb_map_items Implicit is $ catRange ps)
    <|>
    do (k, p) <- symbKind
       (is, ps) <- symbMaps ks k
       return (Symb_map_items k is $ catRange $ p : ps)

-- | parse a comma separated list of symbol mappings
symbMaps :: [String] -> SYMB_KIND -> AParser st ([SYMB_OR_MAP], [Token])
symbMaps ks k =
    do s <- symbMap ks k
       do
         c <- commaT `followedWith` parseId ks
         (is, ps) <- symbMaps ks k
         return (s : is, c : ps)
        <|> return ([s], [])