{- |
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 :: [String] -> Id -> AParser st (SORT_ITEM f)
commaSortDecl ks :: [String]
ks s :: Id
s =
    do Token
c <- AParser st Token
forall st. AParser st Token
anComma
       (is :: [Id]
is, cs :: [Token]
cs) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks GenParser Char (AnnoState st) Id
-> AParser st Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
anComma
       let l :: [Id]
l = Id
s Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
is
           p :: Range
p = [Token] -> Range
catRange (Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs)
       [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
forall st f. [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
subSortDecl [String]
ks ([Id]
l, Range
p) AParser st (SORT_ITEM f)
-> AParser st (SORT_ITEM f) -> AParser st (SORT_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SORT_ITEM f -> AParser st (SORT_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> SORT_ITEM f
forall f. [Id] -> Range -> SORT_ITEM f
Sort_decl [Id]
l Range
p)

isoDecl :: TermParser f => [String] -> Id -> AParser st (SORT_ITEM f)
isoDecl :: [String] -> Id -> AParser st (SORT_ITEM f)
isoDecl ks :: [String]
ks s :: Id
s =
    do Token
e <- AParser st Token
forall st. AParser st Token
equalT
       [String] -> (Id, Range) -> AParser st (SORT_ITEM f)
forall f st.
TermParser f =>
[String] -> (Id, Range) -> AParser st (SORT_ITEM f)
subSortDefn [String]
ks (Id
s, Token -> Range
tokPos Token
e) AParser st (SORT_ITEM f)
-> AParser st (SORT_ITEM f) -> AParser st (SORT_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
           (l :: [Id]
l, p :: [Token]
p) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks GenParser Char (AnnoState st) Id
-> AParser st Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
equalT
           SORT_ITEM f -> AParser st (SORT_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> SORT_ITEM f
forall f. [Id] -> Range -> SORT_ITEM f
Iso_decl (Id
s Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
l) ([Token] -> Range
catRange (Token
e Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
p)))

subSortDefn :: TermParser f => [String] -> (Id, Range)
            -> AParser st (SORT_ITEM f)
subSortDefn :: [String] -> (Id, Range) -> AParser st (SORT_ITEM f)
subSortDefn ks :: [String]
ks (s :: Id
s, e :: Range
e) =
    do [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
       Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT CharParser (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addAnnos
       Token
v <- [String] -> CharParser (AnnoState st) Token
forall st. [String] -> GenParser Char st Token
varId [String]
ks
       Token
c <- CharParser (AnnoState st) Token
forall st. AParser st Token
colonT
       Id
t <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks
       Token
d <- CharParser (AnnoState st) Token
forall st. AParser st Token
dotT
       FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
ks
       [Annotation]
a2 <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
       Token
p <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
       SORT_ITEM f -> AParser st (SORT_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT_ITEM f -> AParser st (SORT_ITEM f))
-> SORT_ITEM f -> AParser st (SORT_ITEM f)
forall a b. (a -> b) -> a -> b
$ Id -> Token -> Id -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
forall f.
Id -> Token -> Id -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
Subsort_defn Id
s Token
v Id
t (FORMULA f
-> Range -> [Annotation] -> [Annotation] -> Annoted (FORMULA f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FORMULA f
f Range
nullRange [Annotation]
a [Annotation]
a2)
                  (Range
e Range -> Range -> Range
`appRange` [Token] -> Range
catRange [Token
o, Token
c, Token
d, Token
p])

subSortDecl :: [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
subSortDecl :: [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
subSortDecl ks :: [String]
ks (l :: [Id]
l, p :: Range
p) =
    do Token
t <- AParser st Token
forall st. AParser st Token
lessT
       Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks
       SORT_ITEM f -> AParser st (SORT_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT_ITEM f -> AParser st (SORT_ITEM f))
-> SORT_ITEM f -> AParser st (SORT_ITEM f)
forall a b. (a -> b) -> a -> b
$ [Id] -> Id -> Range -> SORT_ITEM f
forall f. [Id] -> Id -> Range -> SORT_ITEM f
Subsort_decl [Id]
l Id
s (Range
p Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
t)

sortItem :: TermParser f => [String] -> AParser st (SORT_ITEM f)
sortItem :: [String] -> AParser st (SORT_ITEM f)
sortItem ks :: [String]
ks =
    do Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks
       [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
forall st f. [String] -> ([Id], Range) -> AParser st (SORT_ITEM f)
subSortDecl [String]
ks ([Id
s], Range
nullRange) AParser st (SORT_ITEM f)
-> AParser st (SORT_ITEM f) -> AParser st (SORT_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> Id -> AParser st (SORT_ITEM f)
forall st f. [String] -> Id -> AParser st (SORT_ITEM f)
commaSortDecl [String]
ks Id
s
          AParser st (SORT_ITEM f)
-> AParser st (SORT_ITEM f) -> AParser st (SORT_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> Id -> AParser st (SORT_ITEM f)
forall f st.
TermParser f =>
[String] -> Id -> AParser st (SORT_ITEM f)
isoDecl [String]
ks Id
s AParser st (SORT_ITEM f)
-> AParser st (SORT_ITEM f) -> AParser st (SORT_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SORT_ITEM f -> AParser st (SORT_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> SORT_ITEM f
forall f. [Id] -> Range -> SORT_ITEM f
Sort_decl [Id
s] Range
nullRange)

-- * typeItem

datatype :: [String] -> AParser st DATATYPE_DECL
datatype :: [String] -> AParser st DATATYPE_DECL
datatype ks :: [String]
ks = do
    Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
defnS
    [String] -> Id -> Token -> AParser st DATATYPE_DECL
forall st. [String] -> Id -> Token -> AParser st DATATYPE_DECL
parseDatatype [String]
ks Id
s Token
e

parseDatatype :: [String] -> SORT -> Token -> AParser st DATATYPE_DECL
parseDatatype :: [String] -> Id -> Token -> AParser st DATATYPE_DECL
parseDatatype ks :: [String]
ks s :: Id
s e :: Token
e = do
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
getAnnos
    (Annoted v :: ALTERNATIVE
v _ _ b :: [Annotation]
b : alts :: [Annoted ALTERNATIVE]
alts, ps :: [Token]
ps) <- [String] -> AParser st (Annoted ALTERNATIVE)
forall st. [String] -> AParser st (Annoted ALTERNATIVE)
aAlternative [String]
ks AParser st (Annoted ALTERNATIVE)
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Annoted ALTERNATIVE], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
barT
    DATATYPE_DECL -> AParser st DATATYPE_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return (DATATYPE_DECL -> AParser st DATATYPE_DECL)
-> DATATYPE_DECL -> AParser st DATATYPE_DECL
forall a b. (a -> b) -> a -> b
$ Id -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl Id
s (ALTERNATIVE
-> Range -> [Annotation] -> [Annotation] -> Annoted ALTERNATIVE
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted ALTERNATIVE
v Range
nullRange [Annotation]
a [Annotation]
b Annoted ALTERNATIVE
-> [Annoted ALTERNATIVE] -> [Annoted ALTERNATIVE]
forall a. a -> [a] -> [a]
: [Annoted ALTERNATIVE]
alts)
      (Range -> DATATYPE_DECL) -> Range -> DATATYPE_DECL
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
e Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

aAlternative :: [String] -> AParser st (Annoted ALTERNATIVE)
aAlternative :: [String] -> AParser st (Annoted ALTERNATIVE)
aAlternative ks :: [String]
ks = do
    ALTERNATIVE
a <- [String] -> AParser st ALTERNATIVE
forall st. [String] -> AParser st ALTERNATIVE
alternative [String]
ks
    [Annotation]
an <- AParser st [Annotation]
forall st. AParser st [Annotation]
lineAnnos
    Annoted ALTERNATIVE -> AParser st (Annoted ALTERNATIVE)
forall (m :: * -> *) a. Monad m => a -> m a
return (ALTERNATIVE
-> Range -> [Annotation] -> [Annotation] -> Annoted ALTERNATIVE
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted ALTERNATIVE
a Range
nullRange [] [Annotation]
an)

alternative :: [String] -> AParser st ALTERNATIVE
alternative :: [String] -> AParser st ALTERNATIVE
alternative ks :: [String]
ks =
    do Token
s <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
sortS
       (ts :: [Id]
ts, cs :: [Token]
cs) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks GenParser Char (AnnoState st) Id
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. AParser st Token
anComma
       ALTERNATIVE -> AParser st ALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> ALTERNATIVE
Subsorts [Id]
ts ([Token] -> Range
catRange (Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs)))
    AParser st ALTERNATIVE
-> AParser st ALTERNATIVE -> AParser st ALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
consId [String]
ks GenParser Char (AnnoState st) Id
-> (Id -> AParser st ALTERNATIVE) -> AParser st ALTERNATIVE
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> Id -> AParser st ALTERNATIVE
forall st. [String] -> Id -> AParser st ALTERNATIVE
optComps [String]
ks)

optComps :: [String] -> Id -> AParser st ALTERNATIVE
optComps :: [String] -> Id -> AParser st ALTERNATIVE
optComps ks :: [String]
ks i :: Id
i = do
            Token
o <- AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos AParser st Token
forall st. CharParser st Token
oParenT
            (cs :: [[COMPONENTS]]
cs, ps :: [Token]
ps) <- [String] -> AParser st [COMPONENTS]
forall st. [String] -> AParser st [COMPONENTS]
component [String]
ks AParser st [COMPONENTS]
-> AParser st Token
-> GenParser Char (AnnoState st) ([[COMPONENTS]], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
anSemiOrComma
            Token
c <- AParser st ()
forall st. AParser st ()
addAnnos AParser st () -> AParser st Token -> AParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Token
forall st. CharParser st Token
cParenT
            Id -> [COMPONENTS] -> Range -> AParser st ALTERNATIVE
forall st. Id -> [COMPONENTS] -> Range -> AParser st ALTERNATIVE
optQuMarkAlt Id
i ([[COMPONENTS]] -> [COMPONENTS]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[COMPONENTS]]
cs) (Range -> AParser st ALTERNATIVE)
-> Range -> AParser st ALTERNATIVE
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c
         AParser st ALTERNATIVE
-> AParser st ALTERNATIVE -> AParser st ALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ALTERNATIVE -> AParser st ALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Total Id
i [] Range
nullRange)

optQuMarkAlt :: Id -> [COMPONENTS] -> Range -> AParser st ALTERNATIVE
optQuMarkAlt :: Id -> [COMPONENTS] -> Range -> AParser st ALTERNATIVE
optQuMarkAlt i :: Id
i cs :: [COMPONENTS]
cs qs :: Range
qs = do
    Token
q <- GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st ()
forall st. AParser st ()
addAnnos AParser st ()
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char (AnnoState st) Token
forall st. CharParser st Token
quMarkT)
    ALTERNATIVE -> AParser st ALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Partial Id
i [COMPONENTS]
cs (Range
qs Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
q))
  AParser st ALTERNATIVE
-> AParser st ALTERNATIVE -> AParser st ALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ALTERNATIVE -> AParser st ALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Id -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
Total Id
i [COMPONENTS]
cs Range
qs)

isSortId :: Id -> Bool
isSortId :: Id -> Bool
isSortId (Id is :: [Token]
is _ _) = case [Token]
is of
                       [Token (c :: Char
c : _) _] -> Char -> Bool
caslLetters Char
c
                       _ -> Bool
False

component :: [String] -> AParser st [COMPONENTS]
component :: [String] -> AParser st [COMPONENTS]
component ks :: [String]
ks =
    do (is :: [Id]
is, cs :: [Token]
cs) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
ks GenParser Char (AnnoState st) Id
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
anComma
       if (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
isSortId [Id]
is then
          [String] -> [Id] -> [Token] -> AParser st [COMPONENTS]
forall st. [String] -> [Id] -> [Token] -> AParser st [COMPONENTS]
compSort [String]
ks [Id]
is [Token]
cs AParser st [COMPONENTS]
-> AParser st [COMPONENTS] -> AParser st [COMPONENTS]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [COMPONENTS] -> AParser st [COMPONENTS]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Id -> COMPONENTS) -> [Id] -> [COMPONENTS]
forall a b. (a -> b) -> [a] -> [b]
map Id -> COMPONENTS
Sort [Id]
is)
          else [String] -> [Id] -> [Token] -> AParser st [COMPONENTS]
forall st. [String] -> [Id] -> [Token] -> AParser st [COMPONENTS]
compSort [String]
ks [Id]
is [Token]
cs

compSort :: [String] -> [OP_NAME] -> [Token] -> AParser st [COMPONENTS]
compSort :: [String] -> [Id] -> [Token] -> AParser st [COMPONENTS]
compSort ks :: [String]
ks is :: [Id]
is cs :: [Token]
cs =
    do Token
c <- AParser st Token
forall st. AParser st Token
anColon
       (b :: Bool
b, t :: Id
t, qs :: Range
qs) <- [String] -> GenParser Char (AnnoState st) (Bool, Id, Range)
forall st. [String] -> GenParser Char st (Bool, Id, Range)
opSort [String]
ks
       let p :: Range
p = [Token] -> Range
catRange ([Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]) Range -> Range -> Range
`appRange` Range
qs
       [COMPONENTS] -> AParser st [COMPONENTS]
forall (m :: * -> *) a. Monad m => a -> m a
return [OpKind -> [Id] -> Id -> Range -> COMPONENTS
Cons_select (if Bool
b then OpKind
Partial else OpKind
Total) [Id]
is Id
t Range
p]