446N/A{- |

4744N/AModule : $Header$

446N/ADescription : Parser for symbols in translations and reductions

446N/ACopyright : (c) Christian Maeder, Uni Bremen 2002-2006

446N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

446N/A

446N/AMaintainer : Christian.Maeder@dfki.de

446N/AStability : provisional

446N/APortability : portable

446N/A

446N/AParsing symbols for translations and reductions

446N/A-}

446N/A

446N/Amodule CASL.SymbolParser where

446N/A

446N/Aimport Common.Id

446N/Aimport Common.Keywords

446N/Aimport Common.Lexer

446N/Aimport CASL.AS_Basic_CASL

446N/Aimport Text.ParserCombinators.Parsec

873N/Aimport Common.Token

446N/Aimport CASL.Formula

446N/A

446N/A-- | parsing a possibly qualified identifier

446N/Asymb :: [String] -> GenParser Char st SYMB

5073N/Asymb ks =

5508N/A do i <- parseId ks

446N/A do c <- colonST

446N/A t <- opOrPredType ks

446N/A return (Qual_id i t $ tokPos c)

4744N/A <|> return (Symb_id i)

4744N/A

4744N/A-- | parsing a type for an operation or a predicate

4744N/AopOrPredType :: [String] -> GenParser Char st TYPE

4744N/AopOrPredType ks =

4744N/A do (b, s, p) <- opSort ks

4744N/A if b then return (O_type (Op_type Partial [] s p))

4744N/A else do c <- crossT

4744N/A (ts, ps) <- sortId ks `separatedBy` crossT

4744N/A fmap O_type (opFunSort ks (s:ts) (c:ps))

4744N/A <|> return (P_type $ Pred_type (s:ts)

4744N/A $ catPos $ c:ps)

4744N/A <|> fmap O_type (opFunSort ks [s] [])

4744N/A <|> return (A_type s)

4744N/A <|> fmap P_type predUnitType

4744N/A

4744N/A-- | parsing one symbol or a mapping of one to second symbol

4744N/AsymbMap :: [String] -> GenParser Char st SYMB_OR_MAP

4744N/AsymbMap ks =

4744N/A do s <- symb ks

4744N/A do f <- pToken $ toKey mapsTo

4744N/A t <- symb ks

5073N/A return (Symb_map s t $ tokPos f)

4744N/A <|> return (Symb s)

5073N/A

4744N/A-- | parse a kind keyword

4744N/AsymbKind :: GenParser Char st (SYMB_KIND, Token)

4744N/AsymbKind = try(

4744N/A do q <- pluralKeyword opS

4744N/A return (Ops_kind, q)

957N/A <|>

4744N/A do q <- pluralKeyword predS

4744N/A return (Preds_kind, q)

4744N/A <|>

4744N/A do q <- pluralKeyword sortS

4744N/A return (Sorts_kind, q)) <?> "kind"

4744N/A

4744N/A-- | parse a possible kinded list of comma separated symbols

4744N/AsymbItems :: [String] -> GenParser Char st SYMB_ITEMS

4744N/AsymbItems ks =

4744N/A do (is, ps) <- symbs ks

4744N/A return (Symb_items Implicit is $ catPos ps)

4744N/A <|>

4744N/A do (k, p) <- symbKind

4744N/A (is, ps) <- symbs ks

4744N/A return (Symb_items k is $ catPos $ p:ps)

4744N/A

4744N/A-- | parse a comma separated list of symbols

4744N/Asymbs :: [String] -> GenParser Char st ([SYMB], [Token])

4744N/Asymbs ks =

4744N/A do s <- symb ks

4744N/A do c <- commaT `followedWith` symb ks

4744N/A (is, ps) <- symbs ks

4744N/A return (s:is, c:ps)

4744N/A <|> return ([s], [])

4744N/A

4744N/A-- | parse a possible kinded list of symbol mappings

4744N/AsymbMapItems :: [String] -> GenParser Char st SYMB_MAP_ITEMS

4744N/AsymbMapItems ks =

4744N/A do s <- symbMap ks

4744N/A return (Symb_map_items Implicit [s] nullRange)

4744N/A <|>

4744N/A do (k, p) <- symbKind

4744N/A (is, ps) <- symbMaps ks

4744N/A return (Symb_map_items k is $ catPos $ p:ps)

4744N/A

4744N/A-- | parse a comma separated list of symbol mappings

4744N/AsymbMaps :: [String] -> GenParser Char st ([SYMB_OR_MAP], [Token])

4744N/AsymbMaps ks =

4744N/A do s <- symbMap ks

4744N/A do c <- commaT `followedWith` symb ks

4744N/A (is, ps) <- symbMaps ks

4744N/A return (s:is, c:ps)

4618N/A <|> return ([s], [])

4744N/A