{- |
Module      :  ./HasCASL/ParseItem.hs
Description :  parser for HasCASL basic Items
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

parser for HasCASL basic Items
-}

module HasCASL.ParseItem (basicItems, basicSpec) where

import Text.ParserCombinators.Parsec

import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.HToken
import HasCASL.ParseTerm

import Control.Monad
import qualified Control.Monad.Fail as Fail

-- * adapted item list parser (using 'itemAux')

hasCaslItemList :: String -> AParser st b
                -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList :: String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList kw :: String
kw ip :: AParser st b
ip constr :: [Annoted b] -> Range -> a
constr = do
    Token
p <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
kw
    [String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
forall st b a.
[String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList [String]
hasCaslStartKeywords [Token
p] AParser st b
ip [Annoted b] -> Range -> a
constr

hasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
               -> AParser st a
hasCaslItemAux :: [Token]
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemAux = [String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
forall st b a.
[String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList [String]
hasCaslStartKeywords

-- * parsing type items

commaTypeDecl :: TypePattern -> AParser st TypeItem
commaTypeDecl :: TypePattern -> AParser st TypeItem
commaTypeDecl s :: TypePattern
s = do
    Token
c <- AParser st Token
forall st. AParser st Token
anComma
    (is :: [TypePattern]
is, cs :: [Token]
cs) <- AParser st TypePattern
forall st. AParser st TypePattern
typePattern AParser st TypePattern
-> AParser st Token
-> GenParser Char (AnnoState st) ([TypePattern], [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 :: [TypePattern]
l = TypePattern
s TypePattern -> [TypePattern] -> [TypePattern]
forall a. a -> [a] -> [a]
: [TypePattern]
is
        p :: [Token]
p = Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs
    ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl ([TypePattern]
l, [Token]
p) AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl ([TypePattern]
l, [Token]
p)
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern]
l Kind
universe (Range -> TypeItem) -> Range -> TypeItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
p)

kindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl (l :: [TypePattern]
l, p :: [Token]
p) = do
    Token
t <- AParser st Token
forall st. AParser st Token
colT
    Kind
s <- AParser st Kind
forall st. AParser st Kind
kind
    let d :: TypeItem
d = [TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern]
l Kind
s (Range -> TypeItem) -> Range -> TypeItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
p [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
t]
    case [TypePattern]
l of
      [hd :: TypePattern
hd] -> TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
forall st.
TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef TypePattern
hd (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
s) [Token
t] AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> Kind -> [Token] -> AParser st TypeItem
forall st. TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef TypePattern
hd Kind
s [Token
t] AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return TypeItem
d
      _ -> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return TypeItem
d

isoDecl :: TypePattern -> AParser st TypeItem
isoDecl :: TypePattern -> AParser st TypeItem
isoDecl s :: TypePattern
s = do
    Token
e <- AParser st Token
forall st. AParser st Token
equalT
    (TypePattern, Token) -> AParser st TypeItem
forall st. (TypePattern, Token) -> AParser st TypeItem
subTypeDefn (TypePattern
s, Token
e) AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
        (l :: [TypePattern]
l, p :: [Token]
p) <- AParser st TypePattern
forall st. AParser st TypePattern
typePattern AParser st TypePattern
-> AParser st Token
-> GenParser Char (AnnoState st) ([TypePattern], [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
        TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeItem -> AParser st TypeItem)
-> TypeItem -> AParser st TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Range -> TypeItem
IsoDecl (TypePattern
s TypePattern -> [TypePattern] -> [TypePattern]
forall a. a -> [a] -> [a]
: [TypePattern]
l) (Range -> TypeItem) -> Range -> TypeItem
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]
p

vars :: AParser st Vars
vars :: AParser st Vars
vars = (Id -> Vars)
-> ParsecT String (AnnoState st) Identity Id -> AParser st Vars
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Vars
Var ParsecT String (AnnoState st) Identity Id
forall st. GenParser Char st Id
var AParser st Vars -> AParser st Vars -> AParser st Vars
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT
    (vs :: [Vars]
vs, ps :: [Token]
ps) <- AParser st Vars
forall st. AParser st Vars
vars AParser st Vars
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Vars], [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
    Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT
    Vars -> AParser st Vars
forall (m :: * -> *) a. Monad m => a -> m a
return (Vars -> AParser st Vars) -> Vars -> AParser st Vars
forall a b. (a -> b) -> a -> b
$ [Vars] -> Range -> Vars
VarTuple [Vars]
vs (Range -> Vars) -> Range -> Vars
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c

subTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
subTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
subTypeDefn (s :: TypePattern
s, e :: Token
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
    Vars
v <- AParser st Vars
forall st. AParser st Vars
vars
    Token
c <- CharParser (AnnoState st) Token
forall st. AParser st Token
colT
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    Token
d <- CharParser (AnnoState st) Token
forall st. AParser st Token
dotT -- or bar
    Term
f <- AParser st Term
forall st. AParser st Term
term
    [Annotation]
a2 <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    Token
p <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
    let qs :: Range
qs = Token -> [Token] -> Token -> Range
toRange Token
e [Token
o, Token
c, Token
d] Token
p
    TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeItem -> AParser st TypeItem)
-> TypeItem -> AParser st TypeItem
forall a b. (a -> b) -> a -> b
$ TypePattern -> Vars -> Type -> Annoted Term -> Range -> TypeItem
SubtypeDefn TypePattern
s Vars
v Type
t (Term -> Range -> [Annotation] -> [Annotation] -> Annoted Term
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted Term
f Range
qs [Annotation]
a [Annotation]
a2) Range
qs

subTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl (l :: [TypePattern]
l, p :: [Token]
p) = do
    Token
t <- AParser st Token
forall st. AParser st Token
lessT
    Type
s <- AParser st Type
forall st. AParser st Type
parseType
    TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeItem -> AParser st TypeItem)
-> TypeItem -> AParser st TypeItem
forall a b. (a -> b) -> a -> b
$ [TypePattern] -> Type -> Range -> TypeItem
SubtypeDecl [TypePattern]
l Type
s (Range -> TypeItem) -> Range -> TypeItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
p [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
t]

sortItem :: AParser st TypeItem
sortItem :: AParser st TypeItem
sortItem = do
    TypePattern
s <- AParser st TypePattern
forall st. AParser st TypePattern
typePattern
    ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl ([TypePattern
s], [])
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl ([TypePattern
s], [])
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> AParser st TypeItem
forall st. TypePattern -> AParser st TypeItem
commaTypeDecl TypePattern
s
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> AParser st TypeItem
forall st. TypePattern -> AParser st TypeItem
isoDecl TypePattern
s
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern
s] Kind
universe Range
nullRange)

sortItems :: AParser st SigItems
sortItems :: AParser st SigItems
sortItems = String
-> AParser st TypeItem
-> ([Annoted TypeItem] -> Range -> SigItems)
-> AParser st SigItems
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
sortS AParser st TypeItem
forall st. AParser st TypeItem
sortItem (Instance -> [Annoted TypeItem] -> Range -> SigItems
TypeItems Instance
Plain)

typeItem :: AParser st TypeItem
typeItem :: AParser st TypeItem
typeItem = do
    TypePattern
s <- AParser st TypePattern
forall st. AParser st TypePattern
typePattern
    ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl ([TypePattern
s], [])
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> Kind -> [Token] -> AParser st TypeItem
forall st. TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef TypePattern
s Kind
universe []
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
forall st.
TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef TypePattern
s Maybe Kind
forall a. Maybe a
Nothing []
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([TypePattern], [Token]) -> AParser st TypeItem
forall st. ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl ([TypePattern
s], [])
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> AParser st TypeItem
forall st. TypePattern -> AParser st TypeItem
commaTypeDecl TypePattern
s
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypePattern -> AParser st TypeItem
forall st. TypePattern -> AParser st TypeItem
isoDecl TypePattern
s
        AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypePattern] -> Kind -> Range -> TypeItem
TypeDecl [TypePattern
s] Kind
universe Range
nullRange)

typeItemList :: [Token] -> Instance -> AParser st SigItems
typeItemList :: [Token] -> Instance -> AParser st SigItems
typeItemList ps :: [Token]
ps = [Token]
-> AParser st TypeItem
-> ([Annoted TypeItem] -> Range -> SigItems)
-> AParser st SigItems
forall st b a.
[Token]
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemAux [Token]
ps AParser st TypeItem
forall st. AParser st TypeItem
typeItem (([Annoted TypeItem] -> Range -> SigItems) -> AParser st SigItems)
-> (Instance -> [Annoted TypeItem] -> Range -> SigItems)
-> Instance
-> AParser st SigItems
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instance -> [Annoted TypeItem] -> Range -> SigItems
TypeItems

typeItems :: AParser st SigItems
typeItems :: AParser st SigItems
typeItems = do
    Token
p <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
typeS
    do Token
q <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
instanceS
       [Token] -> Instance -> AParser st SigItems
forall st. [Token] -> Instance -> AParser st SigItems
typeItemList [Token
p, Token
q] Instance
Instance
      AParser st SigItems -> AParser st SigItems -> AParser st SigItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Token] -> Instance -> AParser st SigItems
forall st. [Token] -> Instance -> AParser st SigItems
typeItemList [Token
p] Instance
Plain

pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef t :: TypePattern
t k :: Maybe Kind
k l :: [Token]
l = do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
assignS
    Type
p <- AParser st Type
forall st. AParser st Type
parseType
    TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeItem -> AParser st TypeItem)
-> TypeItem -> AParser st TypeItem
forall a b. (a -> b) -> a -> b
$ TypePattern -> Maybe Kind -> TypeScheme -> Range -> TypeItem
AliasType TypePattern
t Maybe Kind
k (Type -> TypeScheme
simpleTypeScheme Type
p) (Range -> TypeItem) -> Range -> TypeItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
l [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]

-- * parsing datatypes

component :: AParser st [Component]
component :: AParser st [Component]
component = AParser st [Component] -> AParser st [Component]
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do
    (is :: [Id]
is, cs :: [Token]
cs) <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
opId 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
    [Id] -> [Token] -> AParser st [Component]
forall st. [Id] -> [Token] -> AParser st [Component]
compType [Id]
is [Token]
cs) AParser st [Component]
-> AParser st [Component] -> AParser st [Component]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    [Component] -> AParser st [Component]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type -> Component
NoSelector Type
t]

concatFst :: [[a]] -> Range -> ([a], Range)
concatFst :: [[a]] -> Range -> ([a], Range)
concatFst as :: [[a]]
as ps :: Range
ps = ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
as, Range
ps)

tupleComponent :: AParser st ([Component], Range)
tupleComponent :: AParser st ([Component], Range)
tupleComponent = AParser st [Component]
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([[Component]] -> Range -> ([Component], Range))
-> AParser st ([Component], Range)
forall st a b.
AParser st a
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([a] -> Range -> b)
-> AParser st b
bracketParser AParser st [Component]
forall st. AParser st [Component]
component AParser st Token
forall st. CharParser st Token
oParenT AParser st Token
forall st. CharParser st Token
cParenT AParser st Token
forall st. AParser st Token
anSemi [[Component]] -> Range -> ([Component], Range)
forall a. [[a]] -> Range -> ([a], Range)
concatFst

altComponent :: AParser st ([Component], Range)
altComponent :: AParser st ([Component], Range)
altComponent = AParser st ([Component], Range)
forall st. AParser st ([Component], Range)
tupleComponent AParser st ([Component], Range)
-> AParser st ([Component], Range)
-> AParser st ([Component], Range)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Id
i <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
typeVar
    let t :: Type
t = case Id
i of
          Id [tok :: Token
tok] [] _ -> Token -> Type
TypeToken Token
tok
          _ -> String -> Type
forall a. HasCallStack => String -> a
error "altComponent"
    ([Component], Range) -> AParser st ([Component], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type -> Component
NoSelector Type
t], Range
nullRange)

compType :: [Id] -> [Token] -> AParser st [Component]
compType :: [Id] -> [Token] -> AParser st [Component]
compType is :: [Id]
is cs :: [Token]
cs = do
    Token
c <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
colonST
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    let makeComps :: [Id] -> [Token] -> [Component]
makeComps l1 :: [Id]
l1 l2 :: [Token]
l2 = case ([Id]
l1, [Token]
l2) of
          ([a :: Id
a], [b :: Token
b]) -> [Id -> Partiality -> Type -> SeparatorKind -> Range -> Component
Selector Id
a Partiality
Total Type
t SeparatorKind
Other (Range -> Component) -> Range -> Component
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
b]
          (a :: Id
a : r :: [Id]
r, b :: Token
b : s :: [Token]
s) -> Id -> Partiality -> Type -> SeparatorKind -> Range -> Component
Selector Id
a Partiality
Total Type
t SeparatorKind
Comma (Token -> Range
tokPos Token
b) Component -> [Component] -> [Component]
forall a. a -> [a] -> [a]
: [Id] -> [Token] -> [Component]
makeComps [Id]
r [Token]
s
          _ -> String -> [Component]
forall a. HasCallStack => String -> a
error "makeComps: empty selector list"
    [Component] -> AParser st [Component]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Component] -> AParser st [Component])
-> [Component] -> AParser st [Component]
forall a b. (a -> b) -> a -> b
$ [Id] -> [Token] -> [Component]
makeComps [Id]
is ([Token] -> [Component]) -> [Token] -> [Component]
forall a b. (a -> b) -> a -> b
$ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]

alternative :: AParser st Alternative
alternative :: AParser st Alternative
alternative = do
    Token
s <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
sortS CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
typeS
    (ts :: [Type]
ts, cs :: [Token]
cs) <- AParser st Type
forall st. AParser st Type
parseType AParser st Type
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Type], [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 (Alternative -> AParser st Alternative)
-> Alternative -> AParser st Alternative
forall a b. (a -> b) -> a -> b
$ [Type] -> Range -> Alternative
Subtype [Type]
ts (Range -> Alternative) -> Range -> Alternative
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ 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
<|> do
    Id
i <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
hconsId
    [([Component], Range)]
cps <- ParsecT String (AnnoState st) Identity ([Component], Range)
-> ParsecT String (AnnoState st) Identity [([Component], Range)]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String (AnnoState st) Identity ([Component], Range)
forall st. AParser st ([Component], Range)
altComponent
    let ps :: Range
ps = (([Component], Range) -> Range) -> [([Component], Range)] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange ([Component], Range) -> Range
forall a b. (a, b) -> b
snd [([Component], Range)]
cps
        cs :: [[Component]]
cs = (([Component], Range) -> [Component])
-> [([Component], Range)] -> [[Component]]
forall a b. (a -> b) -> [a] -> [b]
map ([Component], Range) -> [Component]
forall a b. (a, b) -> a
fst [([Component], Range)]
cps
    do Token
q <- CharParser (AnnoState st) Token
forall st. CharParser st Token
quMarkT
       Alternative -> AParser st Alternative
forall (m :: * -> *) a. Monad m => a -> m a
return (Alternative -> AParser st Alternative)
-> Alternative -> AParser st Alternative
forall a b. (a -> b) -> a -> b
$ Id -> [[Component]] -> Partiality -> Range -> Alternative
Constructor Id
i [[Component]]
cs Partiality
Partial (Range -> Alternative) -> Range -> Alternative
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
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 (Id -> [[Component]] -> Partiality -> Range -> Alternative
Constructor Id
i [[Component]]
cs Partiality
Total Range
ps)

dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef t :: TypePattern
t k :: Kind
k l :: [Token]
l = do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
defnS
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    let aAlternative :: ParsecT String (AnnoState st) Identity (Annoted Alternative)
aAlternative = (Alternative -> [Annotation] -> Annoted Alternative)
-> ParsecT String (AnnoState st) Identity Alternative
-> ParsecT String (AnnoState st) Identity [Annotation]
-> ParsecT String (AnnoState st) Identity (Annoted Alternative)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ i :: Alternative
i -> Alternative
-> Range -> [Annotation] -> [Annotation] -> Annoted Alternative
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted Alternative
i Range
nullRange [])
          ParsecT String (AnnoState st) Identity Alternative
forall st. AParser st Alternative
alternative ParsecT String (AnnoState st) Identity [Annotation]
forall st. AParser st [Annotation]
annos
    (Annoted v :: Alternative
v _ _ b :: [Annotation]
b : as :: [Annoted Alternative]
as, ps :: [Token]
ps) <- ParsecT String (AnnoState st) Identity (Annoted Alternative)
forall st.
ParsecT String (AnnoState st) Identity (Annoted Alternative)
aAlternative ParsecT String (AnnoState st) Identity (Annoted Alternative)
-> AParser 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` AParser st Token
forall st. AParser st Token
barT
    let aa :: [Annoted Alternative]
aa = 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]
as
        qs :: Range
qs = [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
l [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps
    do Token
d <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
derivingS
       (cs :: [Id]
cs, cps :: [Token]
cps) <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
classId 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
       TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeItem -> AParser st TypeItem)
-> TypeItem -> AParser st TypeItem
forall a b. (a -> b) -> a -> b
$ DatatypeDecl -> TypeItem
Datatype (DatatypeDecl -> TypeItem) -> DatatypeDecl -> TypeItem
forall a b. (a -> b) -> a -> b
$ TypePattern
-> Kind -> [Annoted Alternative] -> [Id] -> Range -> DatatypeDecl
DatatypeDecl TypePattern
t Kind
k [Annoted Alternative]
aa [Id]
cs
         (Range -> DatatypeDecl) -> Range -> DatatypeDecl
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
qs (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange (Token -> Range
tokPos Token
d) (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
cps
      AParser st TypeItem -> AParser st TypeItem -> AParser st TypeItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TypeItem -> AParser st TypeItem
forall (m :: * -> *) a. Monad m => a -> m a
return (DatatypeDecl -> TypeItem
Datatype (TypePattern
-> Kind -> [Annoted Alternative] -> [Id] -> Range -> DatatypeDecl
DatatypeDecl TypePattern
t Kind
k [Annoted Alternative]
aa [] Range
qs))

dataItem :: AParser st DatatypeDecl
dataItem :: AParser st DatatypeDecl
dataItem = do
     TypePattern
t <- AParser st TypePattern
forall st. AParser st TypePattern
typePattern
     do Token
c <- AParser st Token
forall st. AParser st Token
colT
        Kind
k <- AParser st Kind
forall st. AParser st Kind
kind
        Datatype d :: DatatypeDecl
d <- TypePattern -> Kind -> [Token] -> AParser st TypeItem
forall st. TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef TypePattern
t Kind
k [Token
c]
        DatatypeDecl -> AParser st DatatypeDecl
forall (m :: * -> *) a. Monad m => a -> m a
return DatatypeDecl
d
       AParser st DatatypeDecl
-> AParser st DatatypeDecl -> AParser st DatatypeDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
         Datatype d :: DatatypeDecl
d <- TypePattern -> Kind -> [Token] -> AParser st TypeItem
forall st. TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef TypePattern
t Kind
universe []
         DatatypeDecl -> AParser st DatatypeDecl
forall (m :: * -> *) a. Monad m => a -> m a
return DatatypeDecl
d

dataItems :: AParser st BasicItem
dataItems :: AParser st BasicItem
dataItems = String
-> AParser st DatatypeDecl
-> ([Annoted DatatypeDecl] -> Range -> BasicItem)
-> AParser st BasicItem
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
typeS AParser st DatatypeDecl
forall st. AParser st DatatypeDecl
dataItem [Annoted DatatypeDecl] -> Range -> BasicItem
FreeDatatype

-- * parse class items

classDecl :: AParser st ClassDecl
classDecl :: AParser st ClassDecl
classDecl = do
    (is :: [Id]
is, cs :: [Token]
cs) <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
classId 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
    (ps :: [Token]
ps, k :: Kind
k) <- ([Token], Kind)
-> ParsecT String (AnnoState st) Identity ([Token], Kind)
-> ParsecT String (AnnoState st) Identity ([Token], Kind)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Kind
universe) (ParsecT String (AnnoState st) Identity ([Token], Kind)
 -> ParsecT String (AnnoState st) Identity ([Token], Kind))
-> ParsecT String (AnnoState st) Identity ([Token], Kind)
-> ParsecT String (AnnoState st) Identity ([Token], Kind)
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity [Token]
-> ParsecT String (AnnoState st) Identity Kind
-> ParsecT String (AnnoState st) Identity ([Token], Kind)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (GenParser Char (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single (GenParser Char (AnnoState st) Token
 -> ParsecT String (AnnoState st) Identity [Token])
-> GenParser Char (AnnoState st) Token
-> ParsecT String (AnnoState st) Identity [Token]
forall a b. (a -> b) -> a -> b
$ GenParser Char (AnnoState st) Token
forall st. AParser st Token
lessT GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT) ParsecT String (AnnoState st) Identity Kind
forall st. AParser st Kind
kind
    ClassDecl -> AParser st ClassDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassDecl -> AParser st ClassDecl)
-> ClassDecl -> AParser st ClassDecl
forall a b. (a -> b) -> a -> b
$ [Id] -> Kind -> Range -> ClassDecl
ClassDecl [Id]
is Kind
k (Range -> ClassDecl) -> Range -> ClassDecl
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
ps

classItem :: AParser st ClassItem
classItem :: AParser st ClassItem
classItem = do
    ClassDecl
c <- AParser st ClassDecl
forall st. AParser st ClassDecl
classDecl
    do Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT
       [Annoted BasicItem]
is <- AParser st BasicItem -> AParser st [Annoted BasicItem]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser AParser st BasicItem
forall st. AParser st BasicItem
basicItems
       Token
p <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT
       ClassItem -> AParser st ClassItem
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassItem -> AParser st ClassItem)
-> ClassItem -> AParser st ClassItem
forall a b. (a -> b) -> a -> b
$ ClassDecl -> [Annoted BasicItem] -> Range -> ClassItem
ClassItem ClassDecl
c [Annoted BasicItem]
is (Range -> ClassItem) -> Range -> ClassItem
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
p
      AParser st ClassItem
-> AParser st ClassItem -> AParser st ClassItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ClassItem -> AParser st ClassItem
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassDecl -> [Annoted BasicItem] -> Range -> ClassItem
ClassItem ClassDecl
c [] Range
nullRange)

classItemList :: [Token] -> Instance -> AParser st BasicItem
classItemList :: [Token] -> Instance -> AParser st BasicItem
classItemList ps :: [Token]
ps = [Token]
-> AParser st ClassItem
-> ([Annoted ClassItem] -> Range -> BasicItem)
-> AParser st BasicItem
forall st b a.
[Token]
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemAux [Token]
ps AParser st ClassItem
forall st. AParser st ClassItem
classItem (([Annoted ClassItem] -> Range -> BasicItem)
 -> AParser st BasicItem)
-> (Instance -> [Annoted ClassItem] -> Range -> BasicItem)
-> Instance
-> AParser st BasicItem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instance -> [Annoted ClassItem] -> Range -> BasicItem
ClassItems

classItems :: AParser st BasicItem
classItems :: AParser st BasicItem
classItems = do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey (String
classS String -> String -> String
forall a. [a] -> [a] -> [a]
++ "es") AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKey String
classS AParser st Token -> String -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String
classS
    do Token
q <- String -> AParser st Token
forall st. String -> CharParser st Token
pluralKeyword String
instanceS
       [Token] -> Instance -> AParser st BasicItem
forall st. [Token] -> Instance -> AParser st BasicItem
classItemList [Token
p, Token
q] Instance
Instance
      AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Token] -> Instance -> AParser st BasicItem
forall st. [Token] -> Instance -> AParser st BasicItem
classItemList [Token
p] Instance
Plain

-- * parse op items

opAttr :: AParser st OpAttr
opAttr :: AParser st OpAttr
opAttr = let l :: [BinOpAttr]
l = [BinOpAttr
Assoc, BinOpAttr
Comm, BinOpAttr
Idem] in
    [AParser st OpAttr] -> AParser st OpAttr
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((BinOpAttr -> AParser st OpAttr)
-> [BinOpAttr] -> [AParser st OpAttr]
forall a b. (a -> b) -> [a] -> [b]
map ( \ a :: BinOpAttr
a -> do
      Token
b <- String -> AParser st Token
forall st. String -> AParser st Token
asKey (String -> AParser st Token) -> String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ BinOpAttr -> String
forall a. Show a => a -> String
show BinOpAttr
a
      OpAttr -> AParser st OpAttr
forall (m :: * -> *) a. Monad m => a -> m a
return (OpAttr -> AParser st OpAttr) -> OpAttr -> AParser st OpAttr
forall a b. (a -> b) -> a -> b
$ BinOpAttr -> Range -> OpAttr
BinOpAttr BinOpAttr
a (Range -> OpAttr) -> Range -> OpAttr
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
b) [BinOpAttr]
l)
    AParser st OpAttr -> AParser st OpAttr -> AParser st OpAttr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
unitS
    Term
t <- AParser st Term
forall st. AParser st Term
term
    OpAttr -> AParser st OpAttr
forall (m :: * -> *) a. Monad m => a -> m a
return (OpAttr -> AParser st OpAttr) -> OpAttr -> AParser st OpAttr
forall a b. (a -> b) -> a -> b
$ Term -> Range -> OpAttr
UnitOpAttr Term
t (Range -> OpAttr) -> Range -> OpAttr
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
a

multiTypeScheme :: [PolyId] -> AParser st TypeScheme
multiTypeScheme :: [PolyId] -> AParser st TypeScheme
multiTypeScheme os :: [PolyId]
os = case [PolyId]
os of
    p :: PolyId
p : r :: [PolyId]
r -> if [PolyId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PolyId]
r Bool -> Bool -> Bool
|| (PolyId -> Bool) -> [PolyId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ( \ (PolyId _ tys :: [TypeArg]
tys _) -> [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tys) [PolyId]
os
      then PolyId -> AParser st TypeScheme
forall st. PolyId -> AParser st TypeScheme
typeScheme PolyId
p
      else String -> AParser st TypeScheme
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> AParser st TypeScheme)
-> String -> AParser st TypeScheme
forall a b. (a -> b) -> a -> b
$ "instantiation list in identifier list: "
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Id] -> String
forall a. Show a => a -> String
show ((PolyId -> Id) -> [PolyId] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (PolyId i :: Id
i _ _) -> Id
i) [PolyId]
os)
    _ -> String -> AParser st TypeScheme
forall a. HasCallStack => String -> a
error "HasCASL.ParseItem.opDecl"

opDecl :: [PolyId] -> [Token] -> AParser st OpItem
opDecl :: [PolyId] -> [Token] -> AParser st OpItem
opDecl os :: [PolyId]
os ps :: [Token]
ps = do
    Token
c <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
colonST
    TypeScheme
t <- [PolyId] -> AParser st TypeScheme
forall st. [PolyId] -> AParser st TypeScheme
multiTypeScheme [PolyId]
os
    [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
forall st.
[PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
opAttrs [PolyId]
os [Token]
ps Token
c TypeScheme
t AParser st OpItem -> AParser st OpItem -> AParser st OpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId]
os TypeScheme
t [] (Range -> OpItem) -> Range -> OpItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c])

opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
opAttrs os :: [PolyId]
os ps :: [Token]
ps c :: Token
c t :: TypeScheme
t = do
    Token
d <- AParser st Token
forall st. AParser st Token
anComma
    (attrs :: [OpAttr]
attrs, cs :: [Token]
cs) <- AParser st OpAttr
forall st. AParser st OpAttr
opAttr AParser st OpAttr
-> AParser st Token
-> GenParser Char (AnnoState st) ([OpAttr], [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
    OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return (OpItem -> AParser st OpItem) -> OpItem -> AParser st OpItem
forall a b. (a -> b) -> a -> b
$ [PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId]
os TypeScheme
t [OpAttr]
attrs (Range -> OpItem) -> Range -> OpItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c, Token
d] [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
cs

opArg :: AParser st ([VarDecl], Range)
opArg :: AParser st ([VarDecl], Range)
opArg = AParser st [VarDecl]
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([[VarDecl]] -> Range -> ([VarDecl], Range))
-> AParser st ([VarDecl], Range)
forall st a b.
AParser st a
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([a] -> Range -> b)
-> AParser st b
bracketParser AParser st [VarDecl]
forall st. AParser st [VarDecl]
varDecls AParser st Token
forall st. CharParser st Token
oParenT AParser st Token
forall st. CharParser st Token
cParenT AParser st Token
forall st. AParser st Token
anSemi [[VarDecl]] -> Range -> ([VarDecl], Range)
forall a. [[a]] -> Range -> ([a], Range)
concatFst

opArgs :: AParser st ([[VarDecl]], Range)
opArgs :: AParser st ([[VarDecl]], Range)
opArgs = do
    [([VarDecl], Range)]
cps <- ParsecT String (AnnoState st) Identity ([VarDecl], Range)
-> ParsecT String (AnnoState st) Identity [([VarDecl], Range)]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String (AnnoState st) Identity ([VarDecl], Range)
forall st. AParser st ([VarDecl], Range)
opArg
    ([[VarDecl]], Range) -> AParser st ([[VarDecl]], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ((([VarDecl], Range) -> [VarDecl])
-> [([VarDecl], Range)] -> [[VarDecl]]
forall a b. (a -> b) -> [a] -> [b]
map ([VarDecl], Range) -> [VarDecl]
forall a b. (a, b) -> a
fst [([VarDecl], Range)]
cps, (([VarDecl], Range) -> Range) -> [([VarDecl], Range)] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange ([VarDecl], Range) -> Range
forall a b. (a, b) -> b
snd [([VarDecl], Range)]
cps)

opDeclOrDefn :: PolyId -> AParser st OpItem
opDeclOrDefn :: PolyId -> AParser st OpItem
opDeclOrDefn o :: PolyId
o = do
    Token
c <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
colonST
    TypeScheme
t <- PolyId -> AParser st TypeScheme
forall st. PolyId -> AParser st TypeScheme
typeScheme PolyId
o
    [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
forall st.
[PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
opAttrs [PolyId
o] [] Token
c TypeScheme
t AParser st OpItem -> AParser st OpItem -> AParser st OpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PolyId
-> [[VarDecl]] -> Range -> Token -> TypeScheme -> AParser st OpItem
forall st.
PolyId
-> [[VarDecl]] -> Range -> Token -> TypeScheme -> AParser st OpItem
opTerm PolyId
o [] Range
nullRange Token
c TypeScheme
t
        AParser st OpItem -> AParser st OpItem -> AParser st OpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId
o] TypeScheme
t [] (Range -> OpItem) -> Range -> OpItem
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c)
  AParser st OpItem -> AParser st OpItem -> AParser st OpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (args :: [[VarDecl]]
args, ps :: Range
ps) <- AParser st ([[VarDecl]], Range)
forall st. AParser st ([[VarDecl]], Range)
opArgs
    Token
c <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
colonST
    TypeScheme
t <- (Type -> TypeScheme)
-> ParsecT String (AnnoState st) Identity Type
-> AParser st TypeScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> TypeScheme
simpleTypeScheme ParsecT String (AnnoState st) Identity Type
forall st. AParser st Type
parseType
    PolyId
-> [[VarDecl]] -> Range -> Token -> TypeScheme -> AParser st OpItem
forall st.
PolyId
-> [[VarDecl]] -> Range -> Token -> TypeScheme -> AParser st OpItem
opTerm PolyId
o [[VarDecl]]
args Range
ps Token
c TypeScheme
t

opTerm :: PolyId -> [[VarDecl]] -> Range -> Token -> TypeScheme
       -> AParser st OpItem
opTerm :: PolyId
-> [[VarDecl]] -> Range -> Token -> TypeScheme -> AParser st OpItem
opTerm o :: PolyId
o as :: [[VarDecl]]
as ps :: Range
ps c :: Token
c sc :: TypeScheme
sc = do
    Token
e <- AParser st Token
forall st. AParser st Token
equalT
    Term
f <- AParser st Term
forall st. AParser st Term
term
    OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return (OpItem -> AParser st OpItem) -> OpItem -> AParser st OpItem
forall a b. (a -> b) -> a -> b
$ PolyId -> [[VarDecl]] -> TypeScheme -> Term -> Range -> OpItem
OpDefn PolyId
o [[VarDecl]]
as TypeScheme
sc Term
f (Range -> OpItem) -> Range -> OpItem
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 -> [Token] -> Token -> Range
toRange Token
c [] Token
e

opItem :: AParser st OpItem
opItem :: AParser st OpItem
opItem = do
    (os :: [PolyId]
os, ps :: [Token]
ps) <- AParser st PolyId
forall st. AParser st PolyId
parsePolyId AParser st PolyId
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([PolyId], [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 [PolyId]
os of
      [hd :: PolyId
hd] -> PolyId -> AParser st OpItem
forall st. PolyId -> AParser st OpItem
opDeclOrDefn PolyId
hd
      _ -> [PolyId] -> [Token] -> AParser st OpItem
forall st. [PolyId] -> [Token] -> AParser st OpItem
opDecl [PolyId]
os [Token]
ps

opItems :: AParser st SigItems
opItems :: AParser st SigItems
opItems = String
-> AParser st OpItem
-> ([Annoted OpItem] -> Range -> SigItems)
-> AParser st SigItems
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
opS AParser st OpItem
forall st. AParser st OpItem
opItem (OpBrand -> [Annoted OpItem] -> Range -> SigItems
OpItems OpBrand
Op)
    AParser st SigItems -> AParser st SigItems -> AParser st SigItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String
-> AParser st OpItem
-> ([Annoted OpItem] -> Range -> SigItems)
-> AParser st SigItems
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
functS AParser st OpItem
forall st. AParser st OpItem
opItem (OpBrand -> [Annoted OpItem] -> Range -> SigItems
OpItems OpBrand
Fun)

-- * parse pred items as op items

predDecl :: [PolyId] -> [Token] -> AParser st OpItem
predDecl :: [PolyId] -> [Token] -> AParser st OpItem
predDecl os :: [PolyId]
os ps :: [Token]
ps = do
    Token
c <- AParser st Token
forall st. AParser st Token
colT
    TypeScheme
t <- [PolyId] -> AParser st TypeScheme
forall st. [PolyId] -> AParser st TypeScheme
multiTypeScheme [PolyId]
os
    let p :: Range
p = [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
ps [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]
    OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return (OpItem -> AParser st OpItem) -> OpItem -> AParser st OpItem
forall a b. (a -> b) -> a -> b
$ [PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId]
os (Range -> TypeScheme -> TypeScheme
predTypeScheme Range
p TypeScheme
t) [] Range
p

predDefn :: PolyId -> AParser st OpItem
predDefn :: PolyId -> AParser st OpItem
predDefn o :: PolyId
o = do
    (args :: [VarDecl]
args, ps :: Range
ps) <- AParser st ([VarDecl], Range)
forall st. AParser st ([VarDecl], Range)
opArg
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
equivS
    Term
f <- AParser st Term
forall st. AParser st Term
term
    let p :: Range
p = Range -> Range -> Range
appRange Range
ps (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e
    OpItem -> AParser st OpItem
forall (m :: * -> *) a. Monad m => a -> m a
return (OpItem -> AParser st OpItem) -> OpItem -> AParser st OpItem
forall a b. (a -> b) -> a -> b
$ PolyId -> [[VarDecl]] -> TypeScheme -> Term -> Range -> OpItem
OpDefn PolyId
o [[VarDecl]
args]
        (Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkLazyType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Range -> Type
unitTypeWithRange Range
p) Term
f Range
p

predItem :: AParser st OpItem
predItem :: AParser st OpItem
predItem = do
    (os :: [PolyId]
os, ps :: [Token]
ps) <- AParser st PolyId
forall st. AParser st PolyId
parsePolyId AParser st PolyId
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([PolyId], [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
    let d :: AParser st OpItem
d = [PolyId] -> [Token] -> AParser st OpItem
forall st. [PolyId] -> [Token] -> AParser st OpItem
predDecl [PolyId]
os [Token]
ps
    case [PolyId]
os of
      [hd :: PolyId
hd] -> AParser st OpItem
forall st. AParser st OpItem
d AParser st OpItem -> AParser st OpItem -> AParser st OpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PolyId -> AParser st OpItem
forall st. PolyId -> AParser st OpItem
predDefn PolyId
hd
      _ -> AParser st OpItem
forall st. AParser st OpItem
d

predItems :: AParser st SigItems
predItems :: AParser st SigItems
predItems = String
-> AParser st OpItem
-> ([Annoted OpItem] -> Range -> SigItems)
-> AParser st SigItems
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
predS AParser st OpItem
forall st. AParser st OpItem
predItem (OpBrand -> [Annoted OpItem] -> Range -> SigItems
OpItems OpBrand
Pred)

-- * other items

sigItems :: AParser st SigItems
sigItems :: AParser st SigItems
sigItems = AParser st SigItems
forall st. AParser st SigItems
sortItems AParser st SigItems -> AParser st SigItems -> AParser st SigItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st SigItems
forall st. AParser st SigItems
opItems AParser st SigItems -> AParser st SigItems -> AParser st SigItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st SigItems
forall st. AParser st SigItems
predItems AParser st SigItems -> AParser st SigItems -> AParser st SigItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st SigItems
forall st. AParser st SigItems
typeItems

generatedItems :: AParser st BasicItem
generatedItems :: AParser st BasicItem
generatedItems = do
    Token
g <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
generatedS
    do FreeDatatype ds :: [Annoted DatatypeDecl]
ds ps :: Range
ps <- AParser st BasicItem
forall st. AParser st BasicItem
dataItems
       BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted SigItems] -> Range -> BasicItem
GenItems [SigItems
-> Range -> [Annotation] -> [Annotation] -> Annoted SigItems
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted (Instance -> [Annoted TypeItem] -> Range -> SigItems
TypeItems Instance
Plain ((Annoted DatatypeDecl -> Annoted TypeItem)
-> [Annoted DatatypeDecl] -> [Annoted TypeItem]
forall a b. (a -> b) -> [a] -> [b]
map ( \ d :: Annoted DatatypeDecl
d -> TypeItem
-> Range -> [Annotation] -> [Annotation] -> Annoted TypeItem
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted
            (DatatypeDecl -> TypeItem
Datatype (DatatypeDecl -> TypeItem) -> DatatypeDecl -> TypeItem
forall a b. (a -> b) -> a -> b
$ Annoted DatatypeDecl -> DatatypeDecl
forall a. Annoted a -> a
item Annoted DatatypeDecl
d) Range
nullRange (Annoted DatatypeDecl -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted DatatypeDecl
d) (Annoted DatatypeDecl -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted DatatypeDecl
d)) [Annoted DatatypeDecl]
ds) Range
ps)
                          Range
nullRange [] []] (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
g
      AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
        Token
o <- AParser st Token
forall st. CharParser st Token
oBraceT
        [Annoted SigItems]
is <- AParser st SigItems -> AParser st [Annoted SigItems]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser AParser st SigItems
forall st. AParser st SigItems
sigItems
        Token
c <- AParser st Token
forall st. CharParser st Token
cBraceT
        BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted SigItems] -> Range -> BasicItem
GenItems [Annoted SigItems]
is (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
g [Token
o] Token
c

genVarItems :: AParser st ([GenVarDecl], [Token])
genVarItems :: AParser st ([GenVarDecl], [Token])
genVarItems = do
    [GenVarDecl]
vs <- AParser st [GenVarDecl]
forall st. AParser st [GenVarDecl]
genVarDecls
    do Token
s <- AParser st Token
forall st. AParser st Token
trySemi AParser st Token
-> ParsecT String (AnnoState st) Identity () -> AParser st Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity ()
forall st. AParser st ()
addLineAnnos
       do [String] -> ParsecT String (AnnoState st) Identity ()
forall st. [String] -> AParser st ()
tryItemEnd [String]
hasCaslStartKeywords
          ([GenVarDecl], [Token]) -> AParser st ([GenVarDecl], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([GenVarDecl]
vs, [Token
s])
         AParser st ([GenVarDecl], [Token])
-> AParser st ([GenVarDecl], [Token])
-> AParser st ([GenVarDecl], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
            (ws :: [GenVarDecl]
ws, ts :: [Token]
ts) <- AParser st ([GenVarDecl], [Token])
forall st. AParser st ([GenVarDecl], [Token])
genVarItems
            ([GenVarDecl], [Token]) -> AParser st ([GenVarDecl], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([GenVarDecl]
vs [GenVarDecl] -> [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a] -> [a]
++ [GenVarDecl]
ws, Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts)
      AParser st ([GenVarDecl], [Token])
-> AParser st ([GenVarDecl], [Token])
-> AParser st ([GenVarDecl], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([GenVarDecl], [Token]) -> AParser st ([GenVarDecl], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([GenVarDecl]
vs, [])

freeDatatype :: AParser st BasicItem
freeDatatype :: AParser st BasicItem
freeDatatype = do
    Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
freeS
    FreeDatatype ds :: [Annoted DatatypeDecl]
ds ps :: Range
ps <- AParser st BasicItem
forall st. AParser st BasicItem
dataItems
    BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [Annoted DatatypeDecl] -> Range -> BasicItem
FreeDatatype [Annoted DatatypeDecl]
ds (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange (Token -> Range
tokPos Token
f) Range
ps

progItems :: AParser st BasicItem
progItems :: AParser st BasicItem
progItems = String
-> AParser st ProgEq
-> ([Annoted ProgEq] -> Range -> BasicItem)
-> AParser st BasicItem
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
programS
    ([String] -> (InMode, [String]) -> String -> AParser st ProgEq
forall st.
[String] -> (InMode, [String]) -> String -> AParser st ProgEq
patternTermPair [String
equalS] (InMode
WithIn, []) String
equalS) [Annoted ProgEq] -> Range -> BasicItem
ProgItems

axiomItems :: AParser st BasicItem
axiomItems :: AParser st BasicItem
axiomItems = String
-> AParser st Term
-> ([Annoted Term] -> Range -> BasicItem)
-> AParser st BasicItem
forall st b a.
String
-> AParser st b -> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList String
axiomS AParser st Term
forall st. AParser st Term
term (([Annoted Term] -> Range -> BasicItem) -> AParser st BasicItem)
-> ([Annoted Term] -> Range -> BasicItem) -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [Annoted Term] -> Range -> BasicItem
AxiomItems []

forallItem :: AParser st BasicItem
forallItem :: AParser st BasicItem
forallItem = do
    Token
f <- AParser st Token
forall st. AParser st Token
forallT
    (vs :: [[GenVarDecl]]
vs, ps :: [Token]
ps) <- AParser st [GenVarDecl]
forall st. AParser st [GenVarDecl]
genVarDecls AParser st [GenVarDecl]
-> AParser st Token
-> GenParser Char (AnnoState st) ([[GenVarDecl]], [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
anSemi
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    AxiomItems _ (Annoted ft :: Term
ft qs :: Range
qs as :: [Annotation]
as rs :: [Annotation]
rs : fs :: [Annoted Term]
fs) ds :: Range
ds <- AParser st BasicItem
forall st. AParser st BasicItem
dotFormulae
    let aft :: Annoted Term
aft = Term -> Range -> [Annotation] -> [Annotation] -> Annoted Term
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted Term
ft Range
qs ([Annotation]
a [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ [Annotation]
as) [Annotation]
rs
    BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [Annoted Term] -> Range -> BasicItem
AxiomItems ([[GenVarDecl]] -> [GenVarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[GenVarDecl]]
vs) (Annoted Term
aft Annoted Term -> [Annoted Term] -> [Annoted Term]
forall a. a -> [a] -> [a]
: [Annoted Term]
fs) (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange ([Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
f Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps) Range
ds

genVarItem :: AParser st BasicItem
genVarItem :: AParser st BasicItem
genVarItem = do
    Token
v <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
varS
    (vs :: [GenVarDecl]
vs, ps :: [Token]
ps) <- AParser st ([GenVarDecl], [Token])
forall st. AParser st ([GenVarDecl], [Token])
genVarItems
    BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> Range -> BasicItem
GenVarItems [GenVarDecl]
vs (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
v Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

dotFormulae :: AParser st BasicItem
dotFormulae :: AParser st BasicItem
dotFormulae = do
    Token
d <- AParser st Token
forall st. AParser st Token
dotT
    (fs :: [Annoted Term]
fs, ds :: [Token]
ds) <- AParser st Term -> AParser st (Annoted Term)
forall st a. AParser st a -> AParser st (Annoted a)
allAnnoParser AParser st Term
forall st. AParser st Term
term AParser st (Annoted Term)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted Term], [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
dotT
    let ps :: Range
ps = [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
d Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ds
        lst :: Annoted Term
lst = [Annoted Term] -> Annoted Term
forall a. [a] -> a
last [Annoted Term]
fs
    if [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Annotation] -> Bool) -> [Annotation] -> Bool
forall a b. (a -> b) -> a -> b
$ Annoted Term -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted Term
lst then do
        (m :: [Token]
m, an :: [Annotation]
an) <- AParser st ([Token], [Annotation])
forall st. AParser st ([Token], [Annotation])
optSemi
        BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [Annoted Term] -> Range -> BasicItem
AxiomItems [] ([Annoted Term] -> [Annoted Term]
forall a. [a] -> [a]
init [Annoted Term]
fs [Annoted Term] -> [Annoted Term] -> [Annoted Term]
forall a. [a] -> [a] -> [a]
++ [Annoted Term -> [Annotation] -> Annoted Term
forall a. Annoted a -> [Annotation] -> Annoted a
appendAnno Annoted Term
lst [Annotation]
an]) (Range -> BasicItem) -> Range -> BasicItem
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
catRange [Token]
m
       else BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return (BasicItem -> AParser st BasicItem)
-> BasicItem -> AParser st BasicItem
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [Annoted Term] -> Range -> BasicItem
AxiomItems [] [Annoted Term]
fs Range
ps

internalItems :: AParser st BasicItem
internalItems :: AParser st BasicItem
internalItems = do
    Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
internalS
    Token
o <- AParser st Token
forall st. CharParser st Token
oBraceT
    [Annoted BasicItem]
is <- AParser st BasicItem -> AParser st [Annoted BasicItem]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser AParser st BasicItem
forall st. AParser st BasicItem
basicItems
    Token
p <- AParser st Token
forall st. CharParser st Token
cBraceT
    BasicItem -> AParser st BasicItem
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted BasicItem] -> Range -> BasicItem
Internal [Annoted BasicItem]
is (Range -> BasicItem) -> Range -> BasicItem
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
i [Token
o] Token
p)

basicItems :: AParser st BasicItem
basicItems :: AParser st BasicItem
basicItems = (SigItems -> BasicItem)
-> ParsecT String (AnnoState st) Identity SigItems
-> AParser st BasicItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SigItems -> BasicItem
SigItems ParsecT String (AnnoState st) Identity SigItems
forall st. AParser st SigItems
sigItems
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
classItems
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
progItems
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
generatedItems
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
freeDatatype
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
genVarItem
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
forallItem
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
dotFormulae
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
axiomItems
    AParser st BasicItem
-> AParser st BasicItem -> AParser st BasicItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st BasicItem
forall st. AParser st BasicItem
internalItems

basicSpec :: AParser st BasicSpec
basicSpec :: AParser st BasicSpec
basicSpec = ([Annoted BasicItem] -> BasicSpec)
-> ParsecT String (AnnoState st) Identity [Annoted BasicItem]
-> AParser st BasicSpec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted BasicItem] -> BasicSpec
BasicSpec (AParser st BasicItem
-> ParsecT String (AnnoState st) Identity [Annoted BasicItem]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser AParser st BasicItem
forall st. AParser st BasicItem
basicItems)