{- |
Module      :  ./CASL/OpItem.hs
Description :  Parser for OP-ITEMs (operation declarations and definitions)
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 OP-ITEMs (operation declarations and definitions)
-}

{-
   parse OP-ITEM and "op/ops OP-ITEM ; ... ; OP-ITEM"
   parse PRED-ITEM and "op/ops PRED-ITEM ; ... ; PRED-ITEM"

   http://www.cofi.info/Documents/CASL/Summary/
   from 25 March 2001

   C.2.1 Basic Specifications with Subsorts
-}

module CASL.OpItem (opItem, opHead, predItem) where

import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import CASL.AS_Basic_CASL
import Common.AS_Annotation
import Text.ParserCombinators.Parsec
import Common.Token
import CASL.Formula
import Data.List (sort)

-- non-empty
predHead :: [String] -> AParser st PRED_HEAD
predHead :: [String] -> AParser st PRED_HEAD
predHead ks :: [String]
ks =
    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
       (vs :: [VAR_DECL]
vs, ps :: [Token]
ps) <- [String] -> AParser st ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
varDecls [String]
ks
       Token
p <- 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
       PRED_HEAD -> AParser st PRED_HEAD
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_HEAD -> AParser st PRED_HEAD)
-> PRED_HEAD -> AParser st PRED_HEAD
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> Range -> PRED_HEAD
Pred_head [VAR_DECL]
vs (Range -> PRED_HEAD) -> Range -> PRED_HEAD
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange (Token
o Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
p])

opHead :: [String] -> AParser st OP_HEAD
opHead :: [String] -> AParser st OP_HEAD
opHead ks :: [String]
ks =
    do Pred_head vs :: [VAR_DECL]
vs ps :: Range
ps <- [String] -> AParser st PRED_HEAD
forall st. [String] -> AParser st PRED_HEAD
predHead [String]
ks
       do
         Token
c <- AParser st Token
forall st. AParser st Token
anColon
         (b :: Bool
b, s :: Id
s, qs :: Range
qs) <- [String] -> GenParser Char (AnnoState st) (Bool, Id, Range)
forall st. [String] -> GenParser Char st (Bool, Id, Range)
opSort [String]
ks
         OP_HEAD -> AParser st OP_HEAD
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_HEAD -> AParser st OP_HEAD) -> OP_HEAD -> AParser st OP_HEAD
forall a b. (a -> b) -> a -> b
$ OpKind -> [VAR_DECL] -> Maybe Id -> Range -> OP_HEAD
Op_head (if Bool
b then OpKind
Partial else OpKind
Total) [VAR_DECL]
vs (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s)
              (Range
ps Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
c Range -> Range -> Range
`appRange` Range
qs)
        AParser st OP_HEAD -> AParser st OP_HEAD -> AParser st OP_HEAD
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> OP_HEAD -> AParser st OP_HEAD
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> [VAR_DECL] -> Maybe Id -> Range -> OP_HEAD
Op_head OpKind
Partial [VAR_DECL]
vs Maybe Id
forall a. Maybe a
Nothing Range
ps)

opAttr :: TermParser f => [String] -> AParser st (OP_ATTR f, Token)
opAttr :: [String] -> AParser st (OP_ATTR f, Token)
opAttr ks :: [String]
ks = [AParser st (OP_ATTR f, Token)] -> AParser st (OP_ATTR f, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice
  (((String, OP_ATTR f) -> AParser st (OP_ATTR f, Token))
-> [(String, OP_ATTR f)] -> [AParser st (OP_ATTR f, Token)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, t :: OP_ATTR f
t) -> (Token -> (OP_ATTR f, Token))
-> ParsecT String (AnnoState st) Identity Token
-> AParser st (OP_ATTR f, Token)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ p :: Token
p -> (OP_ATTR f
t, Token
p)) (ParsecT String (AnnoState st) Identity Token
 -> AParser st (OP_ATTR f, Token))
-> ParsecT String (AnnoState st) Identity Token
-> AParser st (OP_ATTR f, Token)
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
s)
    [(String
assocS, OP_ATTR f
forall f. OP_ATTR f
Assoc_op_attr), (String
commS, OP_ATTR f
forall f. OP_ATTR f
Comm_op_attr), (String
idemS, OP_ATTR f
forall f. OP_ATTR f
Idem_op_attr)])
  AParser st (OP_ATTR f, Token)
-> AParser st (OP_ATTR f, Token) -> AParser st (OP_ATTR f, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
p <- String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
unitS
    TERM f
t <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
ks
    (OP_ATTR f, Token) -> AParser st (OP_ATTR f, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> OP_ATTR f
forall f. TERM f -> OP_ATTR f
Unit_op_attr TERM f
t, Token
p)

opItem :: TermParser f => [String] -> AParser st (OP_ITEM f)
opItem :: [String] -> AParser st (OP_ITEM f)
opItem ks :: [String]
ks = do
    (os :: [Id]
os, 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
    case [Id]
os of
      [o :: Id
o] -> do
          Token
c <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
anColon
          t :: OP_TYPE
t@(Op_type k :: OpKind
k args :: [Id]
args s :: Id
s ps :: Range
ps) <- [String] -> AParser st OP_TYPE
forall st. [String] -> AParser st OP_TYPE
opType [String]
ks
          case [Id]
args of
            [] -> [String] -> Id -> OP_HEAD -> AParser st (OP_ITEM f)
forall f st.
TermParser f =>
[String] -> Id -> OP_HEAD -> AParser st (OP_ITEM f)
opBody [String]
ks Id
o (OpKind -> [VAR_DECL] -> Maybe Id -> Range -> OP_HEAD
Op_head OpKind
k [] (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
s) (Range -> OP_HEAD) -> Range -> OP_HEAD
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
ps (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c)
              AParser st (OP_ITEM f)
-> AParser st (OP_ITEM f) -> AParser st (OP_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
forall f st.
TermParser f =>
[String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
opAttrs [String]
ks [Id]
os OP_TYPE
t [Token
c]  -- this always succeeds
            _ -> [String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
forall f st.
TermParser f =>
[String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
opAttrs [String]
ks [Id]
os OP_TYPE
t [Token
c]
        AParser st (OP_ITEM f)
-> AParser st (OP_ITEM f) -> AParser st (OP_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String] -> AParser st OP_HEAD
forall st. [String] -> AParser st OP_HEAD
opHead [String]
ks AParser st OP_HEAD
-> (OP_HEAD -> AParser st (OP_ITEM f)) -> AParser st (OP_ITEM f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> Id -> OP_HEAD -> AParser st (OP_ITEM f)
forall f st.
TermParser f =>
[String] -> Id -> OP_HEAD -> AParser st (OP_ITEM f)
opBody [String]
ks Id
o)
        -- require sort: <|> opBody ks o (Op_head Partial [] Nothing nullRange)
      _ -> do
        Token
c <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
anColon
        OP_TYPE
t <- [String] -> AParser st OP_TYPE
forall st. [String] -> AParser st OP_TYPE
opType [String]
ks
        [String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
forall f st.
TermParser f =>
[String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
opAttrs [String]
ks [Id]
os OP_TYPE
t ([Token] -> AParser st (OP_ITEM f))
-> [Token] -> AParser st (OP_ITEM f)
forall a b. (a -> b) -> a -> b
$ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]

opBody :: TermParser f => [String] -> OP_NAME -> OP_HEAD
       -> AParser st (OP_ITEM f)
opBody :: [String] -> Id -> OP_HEAD -> AParser st (OP_ITEM f)
opBody ks :: [String]
ks o :: Id
o h :: OP_HEAD
h =
    do Token
e <- AParser st Token
forall st. AParser st Token
equalT
       [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
       TERM f
t <- [String] -> AParser st (TERM f)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
ks
       OP_ITEM f -> AParser st (OP_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_ITEM f -> AParser st (OP_ITEM f))
-> OP_ITEM f -> AParser st (OP_ITEM f)
forall a b. (a -> b) -> a -> b
$ Id -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
forall f. Id -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
Op_defn Id
o OP_HEAD
h (TERM f -> Range -> [Annotation] -> [Annotation] -> Annoted (TERM f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted TERM f
t Range
nullRange [Annotation]
a []) (Range -> OP_ITEM f) -> Range -> OP_ITEM f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e

opAttrs :: TermParser f => [String] -> [OP_NAME] -> OP_TYPE -> [Token]
        -> AParser st (OP_ITEM f)
opAttrs :: [String] -> [Id] -> OP_TYPE -> [Token] -> AParser st (OP_ITEM f)
opAttrs ks :: [String]
ks os :: [Id]
os t :: OP_TYPE
t c :: [Token]
c =
    do Token
q <- AParser st Token
forall st. AParser st Token
anComma
       (as :: [(OP_ATTR f, Token)]
as, cs :: [Token]
cs) <- [String] -> AParser st (OP_ATTR f, Token)
forall f st.
TermParser f =>
[String] -> AParser st (OP_ATTR f, Token)
opAttr [String]
ks AParser st (OP_ATTR f, Token)
-> AParser st Token
-> GenParser Char (AnnoState st) ([(OP_ATTR f, Token)], [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 ps :: Range
ps = [Pos] -> Range
Range ([Pos] -> [Pos]
forall a. Ord a => [a] -> [a]
sort ([Token] -> [Pos]
catPosAux ([Token]
c [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ ((OP_ATTR f, Token) -> Token) -> [(OP_ATTR f, Token)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ATTR f, Token) -> Token
forall a b. (a, b) -> b
snd [(OP_ATTR f, Token)]
as [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ (Token
q Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs))))
       OP_ITEM f -> AParser st (OP_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [Id]
os OP_TYPE
t (((OP_ATTR f, Token) -> OP_ATTR f)
-> [(OP_ATTR f, Token)] -> [OP_ATTR f]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ATTR f, Token) -> OP_ATTR f
forall a b. (a, b) -> a
fst [(OP_ATTR f, Token)]
as) Range
ps)
   AParser st (OP_ITEM f)
-> AParser st (OP_ITEM f) -> AParser st (OP_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> OP_ITEM f -> AParser st (OP_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [Id]
os OP_TYPE
t [] ([Token] -> Range
catRange [Token]
c))
-- overlap "o:t" DEF-or DECL "o:t=e" or "o:t, assoc"

-- * predicates

predItem :: TermParser f => [String] -> AParser st (PRED_ITEM f)
predItem :: [String] -> AParser st (PRED_ITEM f)
predItem ks :: [String]
ks =
    do (ps :: [Id]
ps, 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
forall a. [a] -> Bool
isSingle [Id]
ps then
                [String] -> Id -> PRED_HEAD -> AParser st (PRED_ITEM f)
forall f st.
TermParser f =>
[String] -> Id -> PRED_HEAD -> AParser st (PRED_ITEM f)
predBody [String]
ks ([Id] -> Id
forall a. [a] -> a
head [Id]
ps) ([VAR_DECL] -> Range -> PRED_HEAD
Pred_head [] Range
nullRange)
                AParser st (PRED_ITEM f)
-> AParser st (PRED_ITEM f) -> AParser st (PRED_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([String] -> AParser st PRED_HEAD
forall st. [String] -> AParser st PRED_HEAD
predHead [String]
ks AParser st PRED_HEAD
-> (PRED_HEAD -> AParser st (PRED_ITEM f))
-> AParser st (PRED_ITEM f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [String] -> Id -> PRED_HEAD -> AParser st (PRED_ITEM f)
forall f st.
TermParser f =>
[String] -> Id -> PRED_HEAD -> AParser st (PRED_ITEM f)
predBody [String]
ks ([Id] -> Id
forall a. [a] -> a
head [Id]
ps))
                AParser st (PRED_ITEM f)
-> AParser st (PRED_ITEM f) -> AParser st (PRED_ITEM f)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> [Id] -> [Token] -> AParser st (PRED_ITEM f)
forall st f.
[String] -> [Id] -> [Token] -> AParser st (PRED_ITEM f)
predTypeCont [String]
ks [Id]
ps [Token]
cs
         else [String] -> [Id] -> [Token] -> AParser st (PRED_ITEM f)
forall st f.
[String] -> [Id] -> [Token] -> AParser st (PRED_ITEM f)
predTypeCont [String]
ks [Id]
ps [Token]
cs

predBody :: TermParser f => [String] -> PRED_NAME -> PRED_HEAD
         -> AParser st (PRED_ITEM f)
predBody :: [String] -> Id -> PRED_HEAD -> AParser st (PRED_ITEM f)
predBody ks :: [String]
ks p :: Id
p h :: PRED_HEAD
h =
    do Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
equivS
       [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
       FORMULA f
f <- [String] -> AParser st (FORMULA f)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
ks
       PRED_ITEM f -> AParser st (PRED_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_ITEM f -> AParser st (PRED_ITEM f))
-> PRED_ITEM f -> AParser st (PRED_ITEM f)
forall a b. (a -> b) -> a -> b
$ Id -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
forall f.
Id -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
Pred_defn Id
p PRED_HEAD
h (FORMULA f
-> Range -> [Annotation] -> [Annotation] -> Annoted (FORMULA f)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FORMULA f
f Range
nullRange [Annotation]
a []) (Range -> PRED_ITEM f) -> Range -> PRED_ITEM f
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e

predTypeCont :: [String] -> [PRED_NAME] -> [Token] -> AParser st (PRED_ITEM f)
predTypeCont :: [String] -> [Id] -> [Token] -> AParser st (PRED_ITEM f)
predTypeCont ks :: [String]
ks ps :: [Id]
ps cs :: [Token]
cs =
    do Token
c <- AParser st Token
forall st. AParser st Token
colonT
       PRED_TYPE
t <- [String] -> AParser st PRED_TYPE
forall st. [String] -> AParser st PRED_TYPE
predType [String]
ks
       PRED_ITEM f -> AParser st (PRED_ITEM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_ITEM f -> AParser st (PRED_ITEM f))
-> PRED_ITEM f -> AParser st (PRED_ITEM f)
forall a b. (a -> b) -> a -> b
$ [Id] -> PRED_TYPE -> Range -> PRED_ITEM f
forall f. [Id] -> PRED_TYPE -> Range -> PRED_ITEM f
Pred_decl [Id]
ps PRED_TYPE
t (Range -> PRED_ITEM f) -> Range -> PRED_ITEM f
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c])