6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Christian Maeder, Uni Bremen 2002-2004

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : maeder@tzi.de

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : portable

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parse SORT-ITEM and "sort/sorts SORT-ITEM ; ... ; SORT-ITEM"

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann parse DATATYPE-DECL

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann http://www.cofi.info/Documents/CASL/Summary/

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann from 25 March 2001

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann C.2.1 Basic Specifications with Subsorts

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule CASL.SortItem (sortItem, datatype) where

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AnnoState

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Id

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Keywords

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Lexer

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.AS_Basic_CASL

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AS_Annotation

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Text.ParserCombinators.Parsec

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Token

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport CASL.Formula

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- ------------------------------------------------------------------------

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- sortItem

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- ------------------------------------------------------------------------

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncommaSortDecl :: [String] -> Id -> AParser st (SORT_ITEM f)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanncommaSortDecl ks s =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann do c <- anComma

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

let l = s : is

p = catPos (c:cs)

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

isoDecl :: AParsable 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) (catPos (e:p))))

subSortDefn :: AParsable 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` catPos [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 :: AParsable 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

a <- getAnnos

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

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

(catPos (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 (catPos (s:cs)))

<|>

do i <- consId ks

do o <- wrapAnnos oParenT

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

c <- addAnnos >> cParenT

let qs = toPos o ps c

do q <- try (addAnnos >> quMarkT)

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

<|> return (Alt_construct Total i cs qs)

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

isSortId :: Id -> Bool

isSortId (Id is _ _) = case is of

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

_ -> False

component :: [String] -> AParser st COMPONENTS

component ks =

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

if isSingle is && isSortId (head is) then

compSort ks is cs <|> return (Sort (head 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 = catPos (cs++[c]) `appRange` qs

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