{- |

Module : ./CASL/SortItem.hs

Description : parser for SORT-ITEMs

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 SORT-ITEMs (sort and subsort declarations and definitions)

-}

{-

parse SORT-ITEM and "sort/sorts SORT-ITEM ; ... ; SORT-ITEM"

parse DATATYPE-DECL

http://www.cofi.info/Documents/CASL/Summary/

from 25 March 2001

C.2.1 Basic Specifications with Subsorts

-}

module CASL.SortItem

( sortItem

, datatype

, subSortDecl

, commaSortDecl

, isoDecl

, parseDatatype

) where

import CASL.AS_Basic_CASL

import CASL.Formula

import Common.AS_Annotation

import Common.AnnoState

import Common.Id

import Common.Keywords

import Common.Lexer

import Common.Parsec

import Common.Token

import Text.ParserCombinators.Parsec

-- * sortItem

commaSortDecl :: [String] -> Id -> AParser st (SORT_ITEM f)

commaSortDecl ks s =

do c <- anComma

(is, cs) <- sortId ks `separatedBy` anComma

let l = s : is

p = catRange (c : cs)

subSortDecl ks (l, p) <|> return (Sort_decl l p)

isoDecl :: TermParser f => [String] -> Id -> AParser st (SORT_ITEM f)

isoDecl ks s =

do e <- equalT

subSortDefn ks (s, tokPos e) <|> do

(l, p) <- sortId ks `separatedBy` equalT

return (Iso_decl (s : l) (catRange (e : p)))

subSortDefn :: TermParser f => [String] -> (Id, Range)

-> AParser st (SORT_ITEM f)

subSortDefn ks (s, e) =

do a <- annos

o <- oBraceT << addAnnos

v <- varId ks

c <- colonT

t <- sortId ks

d <- dotT

f <- formula ks

a2 <- annos

p <- cBraceT

return $ Subsort_defn s v t (Annoted f nullRange a a2)

(e `appRange` catRange [o, c, d, p])

subSortDecl :: [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)

subSortDecl ks (l, p) =

do t <- lessT

s <- sortId ks

return $ Subsort_decl l s (p `appRange` tokPos t)

sortItem :: TermParser f => [String] -> AParser st (SORT_ITEM f)

sortItem ks =

do s <- sortId ks

subSortDecl ks ([s], nullRange) <|> commaSortDecl ks s

<|> isoDecl ks s <|> return (Sort_decl [s] nullRange)

-- * typeItem

datatype :: [String] -> AParser st DATATYPE_DECL

datatype ks = do

s <- sortId ks

e <- asKey defnS

parseDatatype ks s e

parseDatatype :: [String] -> SORT -> Token -> AParser st DATATYPE_DECL

parseDatatype ks s e = do

a <- getAnnos

(Annoted v _ _ b : alts, ps) <- aAlternative ks `separatedBy` barT

return $ Datatype_decl s (Annoted v nullRange a b : alts)

$ catRange $ e : ps

aAlternative :: [String] -> AParser st (Annoted ALTERNATIVE)

aAlternative ks = do

a <- alternative ks

an <- lineAnnos

return (Annoted a nullRange [] an)

alternative :: [String] -> AParser st ALTERNATIVE

alternative ks =

do s <- pluralKeyword sortS

(ts, cs) <- sortId ks `separatedBy` anComma

return (Subsorts ts (catRange (s : cs)))

<|> (consId ks >>= optComps ks)

optComps :: [String] -> Id -> AParser st ALTERNATIVE

optComps ks i = do

o <- wrapAnnos oParenT

(cs, ps) <- component ks `separatedBy` anSemiOrComma

c <- addAnnos >> cParenT

optQuMarkAlt i (concat cs) $ toRange o ps c

<|> return (Alt_construct Total i [] nullRange)

optQuMarkAlt :: Id -> [COMPONENTS] -> Range -> AParser st ALTERNATIVE

optQuMarkAlt i cs qs = do

q <- try (addAnnos >> quMarkT)

return (Alt_construct Partial i cs (qs `appRange` tokPos q))

<|> return (Alt_construct Total i cs qs)

isSortId :: Id -> Bool

isSortId (Id is _ _) = case is of

[Token (c : _) _] -> caslLetters c

_ -> False

component :: [String] -> AParser st [COMPONENTS]

component ks =

do (is, cs) <- parseId ks `separatedBy` anComma

if all isSortId is then

compSort ks is cs <|> return (map Sort is)

else compSort ks is cs

compSort :: [String] -> [OP_NAME] -> [Token] -> AParser st [COMPONENTS]

compSort ks is cs =

do c <- anColon

(b, t, qs) <- opSort ks

let p = catRange (cs ++ [c]) `appRange` qs

return [Cons_select (if b then Partial else Total) is t p]