{- |
Module      :  ./HasCASL/ParseTerm.hs
Description :  parser for HasCASL kinds, types, terms, patterns and equations
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 kinds, types, terms, patterns and equations
-}

module HasCASL.ParseTerm where

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 Text.ParserCombinators.Parsec

import Data.List ((\\))
import qualified Data.Set as Set

-- * key sign tokens

-- | a colon not followed by a question mark
colT :: AParser st Token
colT :: AParser st Token
colT = String -> AParser st Token
forall st. String -> AParser st Token
asKey String
colonS

-- * parser for bracketed lists

-- | a generic bracket parser
bracketParser :: AParser st a -> AParser st Token -> AParser st Token
              -> AParser st Token -> ([a] -> Range -> b) -> AParser st b
bracketParser :: AParser st a
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([a] -> Range -> b)
-> AParser st b
bracketParser parser :: AParser st a
parser op :: AParser st Token
op cl :: AParser st Token
cl sep :: AParser st Token
sep k :: [a] -> Range -> b
k = do
    Token
o <- AParser st Token
op
    (ts :: [a]
ts, ps :: [Token]
ps) <- ([a], [Token])
-> ParsecT String (AnnoState st) Identity ([a], [Token])
-> ParsecT String (AnnoState st) Identity ([a], [Token])
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], []) (ParsecT String (AnnoState st) Identity ([a], [Token])
 -> ParsecT String (AnnoState st) Identity ([a], [Token]))
-> ParsecT String (AnnoState st) Identity ([a], [Token])
-> ParsecT String (AnnoState st) Identity ([a], [Token])
forall a b. (a -> b) -> a -> b
$ AParser st a
-> AParser st Token
-> ParsecT String (AnnoState st) Identity ([a], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy AParser st a
parser AParser st Token
sep
    Token
c <- AParser st Token
cl
    b -> AParser st b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> AParser st b) -> b -> AParser st b
forall a b. (a -> b) -> a -> b
$ [a] -> Range -> b
k [a]
ts (Range -> b) -> Range -> b
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c

-- | parser for square brackets
mkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets p :: AParser st a
p = AParser st a
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([a] -> Range -> b)
-> AParser st b
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 a
p AParser st Token
forall st. CharParser st Token
oBracketT AParser st Token
forall st. CharParser st Token
cBracketT AParser st Token
forall st. AParser st Token
anComma

-- | parser for braces
mkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces p :: AParser st a
p = AParser st a
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([a] -> Range -> b)
-> AParser st b
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 a
p AParser st Token
forall st. CharParser st Token
oBraceT AParser st Token
forall st. CharParser st Token
cBraceT AParser st Token
forall st. AParser st Token
anComma

-- * kinds

-- | parse a simple class name or the type universe as kind
parseClassId :: AParser st Kind
parseClassId :: AParser st Kind
parseClassId = (Id -> Kind)
-> ParsecT String (AnnoState st) Identity Id -> AParser st Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Kind
forall a. a -> AnyKind a
ClassKind ParsecT String (AnnoState st) Identity Id
forall st. GenParser Char st Id
classId

-- | do 'parseClassId' or a kind in parenthessis
parseSimpleKind :: AParser st Kind
parseSimpleKind :: AParser st Kind
parseSimpleKind = AParser st Kind
forall st. AParser st Kind
parseClassId AParser st Kind -> AParser st Kind -> AParser st Kind
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT CharParser (AnnoState st) Token
-> AParser st Kind -> AParser st Kind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Kind
forall st. AParser st Kind
kind AParser st Kind
-> CharParser (AnnoState st) Token -> AParser st Kind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT)

-- | do 'parseSimpleKind' and check for an optional 'Variance'
parseExtKind :: AParser st (Variance, Kind)
parseExtKind :: AParser st (Variance, Kind)
parseExtKind = ParsecT String (AnnoState st) Identity Variance
-> ParsecT String (AnnoState st) Identity Kind
-> AParser st (Variance, Kind)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT String (AnnoState st) Identity Variance
forall st. AParser st Variance
variance ParsecT String (AnnoState st) Identity Kind
forall st. AParser st Kind
parseSimpleKind

-- | parse a (right associative) function kind for a given argument kind
arrowKind :: (Variance, Kind) -> AParser st Kind
arrowKind :: (Variance, Kind) -> AParser st Kind
arrowKind (v :: Variance
v, k :: Kind
k) = do
    Token
a <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
funS
    Kind
k2 <- AParser st Kind
forall st. AParser st Kind
kind
    Kind -> AParser st Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> AParser st Kind) -> Kind -> AParser st Kind
forall a b. (a -> b) -> a -> b
$ Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v Kind
k Kind
k2 (Range -> Kind) -> Range -> Kind
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
a

-- | parse a function kind but reject an extended kind
kind :: AParser st Kind
kind :: AParser st Kind
kind = do
    k1 :: (Variance, Kind)
k1@(v :: Variance
v, k :: Kind
k) <- AParser st (Variance, Kind)
forall st. AParser st (Variance, Kind)
parseExtKind
    (Variance, Kind) -> AParser st Kind
forall st. (Variance, Kind) -> AParser st Kind
arrowKind (Variance, Kind)
k1 AParser st Kind -> AParser st Kind -> AParser st Kind
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> case Variance
v of
        NonVar -> Kind -> AParser st Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
k
        _ -> String -> AParser st Kind
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected "variance of kind"

-- | parse a function kind but accept an extended kind
extKind :: AParser st (Variance, Kind)
extKind :: AParser st (Variance, Kind)
extKind = do
    (Variance, Kind)
k1 <- AParser st (Variance, Kind)
forall st. AParser st (Variance, Kind)
parseExtKind
    do Kind
k <- (Variance, Kind) -> AParser st Kind
forall st. (Variance, Kind) -> AParser st Kind
arrowKind (Variance, Kind)
k1
       (Variance, Kind) -> AParser st (Variance, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variance
NonVar, Kind
k)
      AParser st (Variance, Kind)
-> AParser st (Variance, Kind) -> AParser st (Variance, Kind)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Variance, Kind) -> AParser st (Variance, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variance, Kind)
k1

-- * type variables

variance :: AParser st Variance
variance :: AParser st Variance
variance = let l :: [Variance]
l = [Variance
CoVar, Variance
ContraVar] in
    [AParser st Variance] -> AParser st Variance
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((Variance -> AParser st Variance)
-> [Variance] -> [AParser st Variance]
forall a b. (a -> b) -> [a] -> [b]
map ( \ v :: Variance
v -> String -> AParser st Token
forall st. String -> AParser st Token
asKey (Variance -> String
forall a. Show a => a -> String
show Variance
v) AParser st Token -> AParser st Variance -> AParser st Variance
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Variance -> AParser st Variance
forall (m :: * -> *) a. Monad m => a -> m a
return Variance
v) [Variance]
l) AParser st Variance -> AParser st Variance -> AParser st Variance
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Variance -> AParser st Variance
forall (m :: * -> *) a. Monad m => a -> m a
return Variance
NonVar

-- a (simple) type variable with a 'Variance'
extVar :: AParser st Id -> AParser st (Id, Variance)
extVar :: AParser st Id -> AParser st (Id, Variance)
extVar vp :: AParser st Id
vp = AParser st Id
-> ParsecT String (AnnoState st) Identity Variance
-> AParser st (Id, Variance)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair AParser st Id
vp ParsecT String (AnnoState st) Identity Variance
forall st. AParser st Variance
variance

-- several 'extVar' with a 'Kind'
typeVars :: AParser st [TypeArg]
typeVars :: AParser st [TypeArg]
typeVars = do
    (ts :: [(Id, Variance)]
ts, ps :: [Token]
ps) <- AParser st Id -> AParser st (Id, Variance)
forall st. AParser st Id -> AParser st (Id, Variance)
extVar AParser st Id
forall st. GenParser Char st Id
typeVar AParser st (Id, Variance)
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([(Id, Variance)], [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
    Bool -> [(Id, Variance)] -> [Token] -> AParser st [TypeArg]
forall st.
Bool -> [(Id, Variance)] -> [Token] -> AParser st [TypeArg]
typeKind Bool
False [(Id, Variance)]
ts [Token]
ps

allIsNonVar :: [(Id, Variance)] -> Bool
allIsNonVar :: [(Id, Variance)] -> Bool
allIsNonVar = ((Id, Variance) -> Bool) -> [(Id, Variance)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ( \ (_, v :: Variance
v) -> case Variance
v of
    NonVar -> Bool
True
    _ -> Bool
False)

-- 'parseType' a 'Downset' starting with 'lessT' (True means require kind)
typeKind :: Bool -> [(Id, Variance)] -> [Token]
         -> AParser st [TypeArg]
typeKind :: Bool -> [(Id, Variance)] -> [Token] -> AParser st [TypeArg]
typeKind b :: Bool
b vs :: [(Id, Variance)]
vs ps :: [Token]
ps = do
    Token
c <- AParser st Token
forall st. AParser st Token
colT
    if [(Id, Variance)] -> Bool
allIsNonVar [(Id, Variance)]
vs then do
        (v :: Variance
v, k :: Kind
k) <- AParser st (Variance, Kind)
forall st. AParser st (Variance, Kind)
extKind
        [TypeArg] -> AParser st [TypeArg]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeArg] -> AParser st [TypeArg])
-> [TypeArg] -> AParser st [TypeArg]
forall a b. (a -> b) -> a -> b
$ [(Id, Variance)]
-> [Token] -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs [(Id, Variance)]
vs [Token]
ps Variance
v (Kind -> VarKind
VarKind Kind
k) (Range -> [TypeArg]) -> Range -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
      else do
        Kind
k <- AParser st Kind
forall st. AParser st Kind
kind
        [TypeArg] -> AParser st [TypeArg]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeArg] -> AParser st [TypeArg])
-> [TypeArg] -> AParser st [TypeArg]
forall a b. (a -> b) -> a -> b
$ [(Id, Variance)]
-> [Token] -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs [(Id, Variance)]
vs [Token]
ps Variance
NonVar (Kind -> VarKind
VarKind Kind
k) (Range -> [TypeArg]) -> Range -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
  AParser st [TypeArg]
-> AParser st [TypeArg] -> AParser st [TypeArg]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
l <- AParser st Token
forall st. AParser st Token
lessT
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    [TypeArg] -> AParser st [TypeArg]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeArg] -> AParser st [TypeArg])
-> [TypeArg] -> AParser st [TypeArg]
forall a b. (a -> b) -> a -> b
$ [(Id, Variance)]
-> [Token] -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs [(Id, Variance)]
vs [Token]
ps Variance
NonVar (Type -> VarKind
Downset Type
t) (Range -> [TypeArg]) -> Range -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
l
  AParser st [TypeArg]
-> AParser st [TypeArg] -> AParser st [TypeArg]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> if Bool
b then String -> AParser st [TypeArg]
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected "missing kind" else
          [TypeArg] -> AParser st [TypeArg]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Id, Variance)]
-> [Token] -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs [(Id, Variance)]
vs [Token]
ps Variance
NonVar VarKind
MissingKind Range
nullRange)

-- | add the 'Kind' to all 'extVar' and yield a 'TypeArg'
makeTypeArgs :: [(Id, Variance)] -> [Token]
             -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs :: [(Id, Variance)]
-> [Token] -> Variance -> VarKind -> Range -> [TypeArg]
makeTypeArgs ts :: [(Id, Variance)]
ts ps :: [Token]
ps vv :: Variance
vv vk :: VarKind
vk qs :: Range
qs =
    ((Id, Variance) -> Range -> TypeArg)
-> [(Id, Variance)] -> [Range] -> [TypeArg]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SeparatorKind
-> Variance -> VarKind -> (Id, Variance) -> Range -> TypeArg
mergeVariance SeparatorKind
Comma Variance
vv VarKind
vk) ([(Id, Variance)] -> [(Id, Variance)]
forall a. [a] -> [a]
init [(Id, Variance)]
ts)
                ((Token -> Range) -> [Token] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Range
tokPos [Token]
ps)
                [TypeArg] -> [TypeArg] -> [TypeArg]
forall a. [a] -> [a] -> [a]
++ [SeparatorKind
-> Variance -> VarKind -> (Id, Variance) -> Range -> TypeArg
mergeVariance SeparatorKind
Other Variance
vv VarKind
vk ([(Id, Variance)] -> (Id, Variance)
forall a. [a] -> a
last [(Id, Variance)]
ts) Range
qs]
                where
    mergeVariance :: SeparatorKind
-> Variance -> VarKind -> (Id, Variance) -> Range -> TypeArg
mergeVariance c :: SeparatorKind
c v :: Variance
v k :: VarKind
k (t :: Id
t, NonVar) q :: Range
q = Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
t Variance
v VarKind
k RawKind
rStar 0 SeparatorKind
c Range
q
    mergeVariance c :: SeparatorKind
c _ k :: VarKind
k (t :: Id
t, v :: Variance
v) q :: Range
q = Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
t Variance
v VarKind
k RawKind
rStar 0 SeparatorKind
c Range
q

-- | a single 'TypeArg' (parsed by 'typeVars')
singleTypeArg :: AParser st TypeArg
singleTypeArg :: AParser st TypeArg
singleTypeArg = do
    [TypeArg]
as <- AParser st [TypeArg]
forall st. AParser st [TypeArg]
typeVars
    case [TypeArg]
as of
      [a :: TypeArg
a] -> TypeArg -> AParser st TypeArg
forall (m :: * -> *) a. Monad m => a -> m a
return TypeArg
a
      _ -> String -> AParser st TypeArg
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected "list of type arguments"

-- | a 'singleTypeArg' put in parentheses
parenTypeArg :: AParser st (TypeArg, [Token])
parenTypeArg :: AParser st (TypeArg, [Token])
parenTypeArg = do
    Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT
    TypeArg
a <- AParser st TypeArg
forall st. AParser st TypeArg
singleTypeArg
    Token
p <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT
    (TypeArg, [Token]) -> AParser st (TypeArg, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeArg
a, [Token
o, Token
p])

-- | a 'singleTypeArg' possibly put in parentheses
typeArg :: AParser st (TypeArg, [Token])
typeArg :: AParser st (TypeArg, [Token])
typeArg = do
    TypeArg
a <- AParser st TypeArg
forall st. AParser st TypeArg
singleTypeArg
    (TypeArg, [Token]) -> AParser st (TypeArg, [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeArg
a, [])
  AParser st (TypeArg, [Token])
-> AParser st (TypeArg, [Token]) -> AParser st (TypeArg, [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st (TypeArg, [Token])
forall st. AParser st (TypeArg, [Token])
parenTypeArg

-- | a 'singleTypeArg' put in parentheses as 'TypePattern'
typePatternArg :: AParser st TypePattern
typePatternArg :: AParser st TypePattern
typePatternArg = do
    (a :: TypeArg
a, ps :: [Token]
ps) <- AParser st (TypeArg, [Token])
forall st. AParser st (TypeArg, [Token])
parenTypeArg
    TypePattern -> AParser st TypePattern
forall (m :: * -> *) a. Monad m => a -> m a
return (TypePattern -> AParser st TypePattern)
-> TypePattern -> AParser st TypePattern
forall a b. (a -> b) -> a -> b
$ TypeArg -> Range -> TypePattern
TypePatternArg TypeArg
a (Range -> TypePattern) -> Range -> TypePattern
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps

-- * parse special identifier tokens

type TokenMode = [String]

{- | parse a 'Token' of an 'Id' (to be declared)
but exclude the signs in 'TokenMode' -}
aToken :: TokenMode -> AParser st Token
aToken :: TokenMode -> AParser st Token
aToken b :: TokenMode
b = CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String -> AParser st Token)
-> CharParser (AnnoState st) String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
forall st. CharParser st String
scanQuotedChar CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanDigit CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanHCWords CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
placeS
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st.
TokenMode -> CharParser st String -> CharParser st String
reserved TokenMode
b CharParser (AnnoState st) String
forall st. CharParser st String
scanHCSigns

-- | just 'aToken' only excluding basic HasCASL keywords
idToken :: AParser st Token
idToken :: AParser st Token
idToken = TokenMode -> AParser st Token
forall st. TokenMode -> AParser st Token
aToken [] 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
<|> CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
pToken CharParser (AnnoState st) String
forall st. CharParser st String
scanDotWords

-- * type patterns

{- 'TypePatternToken's within 'BracketTypePattern's
may recusively be 'idToken's.
Parenthesis are only legal for a 'typePatternArg'. -}
primTypePatternOrId :: AParser st TypePattern
primTypePatternOrId :: AParser st TypePattern
primTypePatternOrId = (Token -> TypePattern)
-> ParsecT String (AnnoState st) Identity Token
-> AParser st TypePattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> TypePattern
TypePatternToken ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
idToken
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
-> ([TypePattern] -> Range -> TypePattern)
-> AParser st TypePattern
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st TypePattern
forall st. AParser st TypePattern
typePatternOrId (BracketKind -> [TypePattern] -> Range -> TypePattern
BracketTypePattern BracketKind
Braces)
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
-> ([TypePattern] -> Range -> TypePattern)
-> AParser st TypePattern
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st TypePattern
forall st. AParser st TypePattern
typePatternOrId (BracketKind -> [TypePattern] -> Range -> TypePattern
BracketTypePattern BracketKind
Squares)
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
forall st. AParser st TypePattern
typePatternArg

-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
mixTypePattern :: AParser st TypePattern -> AParser st TypePattern
mixTypePattern :: AParser st TypePattern -> AParser st TypePattern
mixTypePattern p :: AParser st TypePattern
p = do
    [TypePattern]
ts <- AParser st TypePattern
-> ParsecT String (AnnoState st) Identity [TypePattern]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 AParser st TypePattern
p
    TypePattern -> AParser st TypePattern
forall (m :: * -> *) a. Monad m => a -> m a
return (TypePattern -> AParser st TypePattern)
-> TypePattern -> AParser st TypePattern
forall a b. (a -> b) -> a -> b
$ case [TypePattern]
ts of
       [hd :: TypePattern
hd] -> TypePattern
hd
       _ -> [TypePattern] -> TypePattern
MixfixTypePattern [TypePattern]
ts

-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
typePatternOrId :: AParser st TypePattern
typePatternOrId :: AParser st TypePattern
typePatternOrId = AParser st TypePattern -> AParser st TypePattern
forall st. AParser st TypePattern -> AParser st TypePattern
mixTypePattern AParser st TypePattern
forall st. AParser st TypePattern
primTypePatternOrId

{- | those (top-level) 'Token's (less than 'idToken')
that may appear in 'TypePattern's as 'TypePatternToken'. -}
typePatternToken :: AParser st TypePattern
typePatternToken :: AParser st TypePattern
typePatternToken = (Token -> TypePattern)
-> ParsecT String (AnnoState st) Identity Token
-> AParser st TypePattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> TypePattern
TypePatternToken (ParsecT String (AnnoState st) Identity Token
 -> AParser st TypePattern)
-> ParsecT String (AnnoState st) Identity Token
-> AParser st TypePattern
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String
 -> ParsecT String (AnnoState st) Identity Token)
-> CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
forall st. CharParser st String
scanHCWords CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
placeS
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st.
TokenMode -> CharParser st String -> CharParser st String
reserved TokenMode
hascasl_reserved_tops CharParser (AnnoState st) String
forall st. CharParser st String
scanHCSigns

{- | a 'typePatternToken' or something in braces (a 'typePattern'),
in square brackets (a 'typePatternOrId' covering compound lists)
or parenthesis ('typePatternArg') -}
primTypePattern :: AParser st TypePattern
primTypePattern :: AParser st TypePattern
primTypePattern = AParser st TypePattern
forall st. AParser st TypePattern
typePatternToken
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
-> ([TypePattern] -> Range -> TypePattern)
-> AParser st TypePattern
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st TypePattern
forall st. AParser st TypePattern
typePatternOrId (BracketKind -> [TypePattern] -> Range -> TypePattern
BracketTypePattern BracketKind
Squares)
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
-> ([TypePattern] -> Range -> TypePattern)
-> AParser st TypePattern
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st TypePattern
forall st. AParser st TypePattern
typePattern (BracketKind -> [TypePattern] -> Range -> TypePattern
BracketTypePattern BracketKind
Braces)
    AParser st TypePattern
-> AParser st TypePattern -> AParser st TypePattern
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st TypePattern
forall st. AParser st TypePattern
typePatternArg

-- several 'primTypePatter's possibly yielding a 'MixfixTypePattern'
typePattern :: AParser st TypePattern
typePattern :: AParser st TypePattern
typePattern = AParser st TypePattern -> AParser st TypePattern
forall st. AParser st TypePattern -> AParser st TypePattern
mixTypePattern AParser st TypePattern
forall st. AParser st TypePattern
primTypePattern

{- * types
a parsed type may also be interpreted as a kind (by the mixfix analysis) -}

-- | type tokens with some symbols removed
typeToken :: AParser st Type
typeToken :: AParser st Type
typeToken = (Token -> Type)
-> ParsecT String (AnnoState st) Identity Token -> AParser st Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Type
TypeToken (ParsecT String (AnnoState st) Identity Token -> AParser st Type)
-> ParsecT String (AnnoState st) Identity Token -> AParser st Type
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String
 -> ParsecT String (AnnoState st) Identity Token)
-> CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ CharParser (AnnoState st) String
forall st. CharParser st String
scanHCWords CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
placeS CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    TokenMode
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st.
TokenMode -> CharParser st String -> CharParser st String
reserved (TokenMode
hascasl_reserved_tops TokenMode -> TokenMode -> TokenMode
forall a. [a] -> [a] -> [a]
++ TokenMode
hascasl_type_ops)
    CharParser (AnnoState st) String
forall st. CharParser st String
scanHCSigns

{- | 'TypeToken's within 'BracketType's may recusively be
'idToken's. Parenthesis may group a mixfix type
or may be interpreted as a kind later on in a GEN-VAR-DECL. -}
primTypeOrId :: AParser st Type
primTypeOrId :: AParser st Type
primTypeOrId = (Token -> Type)
-> ParsecT String (AnnoState st) Identity Token -> AParser st Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Type
TypeToken ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
idToken
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type -> ([Type] -> Range -> Type) -> AParser st Type
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st Type
forall st. AParser st Type
typeOrId (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Squares)
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type -> ([Type] -> Range -> Type) -> AParser st Type
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st Type
forall st. AParser st Type
typeOrId (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Braces)
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ([Type] -> Range -> Type)
-> AParser st Type
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 Type
forall st. AParser st Type
typeOrId ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
oParenT ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
cParenT ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
anComma (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Parens)

mkMixfixType :: AParser st Type -> AParser st Type
mkMixfixType :: AParser st Type -> AParser st Type
mkMixfixType p :: AParser st Type
p = do
    [Type]
ts <- AParser st Type -> ParsecT String (AnnoState st) Identity [Type]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 AParser st Type
p
    Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> AParser st Type) -> Type -> AParser st Type
forall a b. (a -> b) -> a -> b
$ case [Type]
ts of
              [hd :: Type
hd] -> Type
hd
              _ -> [Type] -> Type
MixfixType [Type]
ts

mkKindedMixType :: AParser st Type -> AParser st Type
mkKindedMixType :: AParser st Type -> AParser st Type
mkKindedMixType p :: AParser st Type
p = do
    Type
t <- AParser st Type -> AParser st Type
forall st. AParser st Type -> AParser st Type
mkMixfixType AParser st Type
p
    Type -> AParser st Type
forall st. Type -> AParser st Type
kindAnno Type
t AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

{- | several 'primTypeOrId's possibly yielding a 'MixfixType'
and possibly followed by a 'kindAnno'. -}
typeOrId :: AParser st Type
typeOrId :: AParser st Type
typeOrId = AParser st Type -> AParser st Type
forall st. AParser st Type -> AParser st Type
mkKindedMixType AParser st Type
forall st. AParser st Type
primTypeOrId

-- | a 'Kind' annotation starting with 'colT'.
kindAnno :: Type -> AParser st Type
kindAnno :: Type -> AParser st Type
kindAnno t :: Type
t = do
    Token
c <- AParser st Token
forall st. AParser st Token
colT
    Kind
k <- AParser st Kind
forall st. AParser st Kind
kind
    Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> AParser st Type) -> Type -> AParser st Type
forall a b. (a -> b) -> a -> b
$ Type -> Set Kind -> Range -> Type
KindedType Type
t (Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k) (Range -> Type) -> Range -> Type
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c

-- | a typeToken' or a 'BracketType'. Square brackets may contain 'typeOrId'.
primType :: AParser st Type
primType :: AParser st Type
primType = AParser st Type
forall st. AParser st Type
typeToken
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type -> ([Type] -> Range -> Type) -> AParser st Type
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st Type
forall st. AParser st Type
typeOrId (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Squares)
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type -> ([Type] -> Range -> Type) -> AParser st Type
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st Type
forall st. AParser st Type
parseType (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Braces)
    AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([Type] -> Range -> Type)
-> AParser st Type
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 Type
forall st. AParser st Type
parseType 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
anComma (BracketKind -> [Type] -> Range -> Type
BracketType BracketKind
Parens)

-- | a 'primType' possibly preceded by 'quMarkT'
lazyType :: AParser st Type
lazyType :: AParser st Type
lazyType = (Type -> Type) -> AParser st Type -> AParser st Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
mkLazyType (GenParser Char (AnnoState st) Token
forall st. CharParser st Token
quMarkT GenParser Char (AnnoState st) Token
-> AParser st Type -> AParser st Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st Type -> AParser st Type
forall st. AParser st Type -> AParser st Type
mkMixfixType AParser st Type
forall st. AParser st Type
primType) AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Type
forall st. AParser st Type
primType

-- | several 'lazyType's (as 'MixfixType') possibly followed by 'kindAnno'
mixType :: AParser st Type
mixType :: AParser st Type
mixType = AParser st Type -> AParser st Type
forall st. AParser st Type -> AParser st Type
mkKindedMixType AParser st Type
forall st. AParser st Type
lazyType

-- | 'mixType' possibly interspersed with 'crossT'
prodType :: AParser st Type
prodType :: AParser st Type
prodType = do
    (ts :: [Type]
ts, ps :: [Token]
ps) <- AParser st Type
forall st. AParser st Type
mixType AParser st Type
-> GenParser Char (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` GenParser Char (AnnoState st) Token
forall st. CharParser st Token
crossT
    Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> AParser st Type) -> Type -> AParser st Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Range -> Type
mkProductTypeWithRange [Type]
ts (Range -> Type) -> Range -> Type
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange [Token]
ps

-- | a (right associativ) function type
parseType :: AParser st Type
parseType :: AParser st Type
parseType = do
    Type
t1 <- AParser st Type
forall st. AParser st Type
prodType
    do Id
a <- AParser st Id
forall st. AParser st Id
arrowT AParser st Id -> String -> AParser st Id
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> String -> String
forall a. Show a => a -> String
show String
funS
       Type
t2 <- AParser st Type
forall st. AParser st Type
parseType
       Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> AParser st Type) -> Type -> AParser st Type
forall a b. (a -> b) -> a -> b
$ Type -> [Type] -> Type
mkTypeAppl
           (Id -> RawKind -> Int -> Type
TypeName Id
a (Kind -> RawKind
toRaw (Kind -> RawKind) -> Kind -> RawKind
forall a b. (a -> b) -> a -> b
$ Range -> Kind
funKindWithRange (Range -> Kind) -> Range -> Kind
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
a) 0) [Type
t1, Type
t2]
      AParser st Type -> AParser st Type -> AParser st Type
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Type -> AParser st Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t1

-- | parse one of the four possible 'Arrow's
arrowT :: AParser st Id
arrowT :: AParser st Id
arrowT = let l :: [Arrow]
l = [Arrow
FunArr, Arrow
PFunArr, Arrow
ContFunArr, Arrow
PContFunArr] in
    [AParser st Id] -> AParser st Id
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st Id] -> AParser st Id)
-> [AParser st Id] -> AParser st Id
forall a b. (a -> b) -> a -> b
$ (Arrow -> AParser st Id) -> [Arrow] -> [AParser st Id]
forall a b. (a -> b) -> [a] -> [b]
map ( \ a :: Arrow
a -> do
           Token
t <- 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
$ Arrow -> String
forall a. Show a => a -> String
show Arrow
a
           Id -> AParser st Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> AParser st Id) -> Id -> AParser st Id
forall a b. (a -> b) -> a -> b
$ [Token] -> Id
mkId [Token
placeTok, Token
t, Token
placeTok]) [Arrow]
l

-- | parse a 'TypeScheme' using 'forallT', 'typeVars', 'dotT' and 'parseType'
typeScheme :: PolyId -> AParser st TypeScheme
typeScheme :: PolyId -> AParser st TypeScheme
typeScheme (PolyId _ tys :: [TypeArg]
tys ps :: Range
ps) = if [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tys then do
    Token
f <- AParser st Token
forall st. AParser st Token
forallT
    (ts :: [[TypeArg]]
ts, cs :: [Token]
cs) <- AParser st [TypeArg]
forall st. AParser st [TypeArg]
typeVars AParser st [TypeArg]
-> AParser st Token
-> GenParser Char (AnnoState st) ([[TypeArg]], [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
    Token
d <- AParser st Token
forall st. AParser st Token
dotT
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    TypeScheme -> AParser st TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeScheme -> AParser st TypeScheme)
-> TypeScheme -> AParser st TypeScheme
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme ([[TypeArg]] -> [TypeArg]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TypeArg]]
ts) Type
t (Range -> TypeScheme) -> Range -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
f [Token]
cs Token
d
  AParser st TypeScheme
-> AParser st TypeScheme -> AParser st TypeScheme
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Type -> TypeScheme) -> AParser st Type -> AParser st TypeScheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> TypeScheme
simpleTypeScheme AParser st Type
forall st. AParser st Type
parseType
  else do
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    TypeScheme -> AParser st TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeScheme -> AParser st TypeScheme)
-> TypeScheme -> AParser st TypeScheme
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
tys Type
t Range
ps

-- * varDecls and genVarDecls

-- | comma separated 'var' with 'varDeclType'
varDecls :: AParser st [VarDecl]
varDecls :: AParser st [VarDecl]
varDecls = do
   (vs :: [Id]
vs, ps :: [Token]
ps) <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
var 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 [VarDecl]
forall st. [Id] -> [Token] -> AParser st [VarDecl]
varDeclType [Id]
vs [Token]
ps

-- | a type ('parseType') following a colon
varDeclType :: [Id] -> [Token] -> AParser st [VarDecl]
varDeclType :: [Id] -> [Token] -> AParser st [VarDecl]
varDeclType vs :: [Id]
vs ps :: [Token]
ps = 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
    [VarDecl] -> AParser st [VarDecl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([VarDecl] -> AParser st [VarDecl])
-> [VarDecl] -> AParser st [VarDecl]
forall a b. (a -> b) -> a -> b
$ [Id] -> [Token] -> Type -> Range -> [VarDecl]
makeVarDecls [Id]
vs [Token]
ps Type
t (Range -> [VarDecl]) -> Range -> [VarDecl]
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c

-- | attach the 'Type' to every 'Var'
makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]
makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]
makeVarDecls vs :: [Id]
vs ps :: [Token]
ps t :: Type
t q :: Range
q = (Id -> Token -> VarDecl) -> [Id] -> [Token] -> [VarDecl]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ( \ v :: Id
v -> Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v Type
t SeparatorKind
Comma (Range -> VarDecl) -> (Token -> Range) -> Token -> VarDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Range
tokPos)
    ([Id] -> [Id]
forall a. [a] -> [a]
init [Id]
vs) [Token]
ps [VarDecl] -> [VarDecl] -> [VarDecl]
forall a. [a] -> [a] -> [a]
++ [Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl ([Id] -> Id
forall a. [a] -> a
last [Id]
vs) Type
t SeparatorKind
Other Range
q]

{- | either like 'varDecls' or declared type variables.
A 'GenVarDecl' may later become a 'GenTypeVarDecl'. -}
genVarDecls :: AParser st [GenVarDecl]
genVarDecls :: AParser st [GenVarDecl]
genVarDecls = ([GenVarDecl] -> [GenVarDecl])
-> AParser st [GenVarDecl] -> AParser st [GenVarDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((GenVarDecl -> GenVarDecl) -> [GenVarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map ( \ g :: GenVarDecl
g -> case GenVarDecl
g of
    GenTypeVarDecl (TypeArg i :: Id
i v :: Variance
v MissingKind _ n :: Int
n s :: SeparatorKind
s ps :: Range
ps) ->
        TypeArg -> GenVarDecl
GenTypeVarDecl (Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (Kind -> VarKind
VarKind Kind
universe)
                                              RawKind
rStar Int
n SeparatorKind
s Range
ps)
    _ -> GenVarDecl
g)) (AParser st [GenVarDecl] -> AParser st [GenVarDecl])
-> AParser st [GenVarDecl] -> AParser st [GenVarDecl]
forall a b. (a -> b) -> a -> b
$ do
    (vs :: [(Id, Variance)]
vs, ps :: [Token]
ps) <- AParser st Id -> AParser st (Id, Variance)
forall st. AParser st Id -> AParser st (Id, Variance)
extVar AParser st Id
forall st. GenParser Char st Id
var AParser st (Id, Variance)
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([(Id, Variance)], [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 other :: ParsecT String (AnnoState st) Identity [GenVarDecl]
other = ([TypeArg] -> [GenVarDecl])
-> ParsecT String (AnnoState st) Identity [TypeArg]
-> ParsecT String (AnnoState st) Identity [GenVarDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TypeArg -> GenVarDecl) -> [TypeArg] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> GenVarDecl
GenTypeVarDecl) (Bool
-> [(Id, Variance)]
-> [Token]
-> ParsecT String (AnnoState st) Identity [TypeArg]
forall st.
Bool -> [(Id, Variance)] -> [Token] -> AParser st [TypeArg]
typeKind Bool
True [(Id, Variance)]
vs [Token]
ps)
    if [(Id, Variance)] -> Bool
allIsNonVar [(Id, Variance)]
vs then ([VarDecl] -> [GenVarDecl])
-> ParsecT String (AnnoState st) Identity [VarDecl]
-> AParser st [GenVarDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl)
        ([Id] -> [Token] -> ParsecT String (AnnoState st) Identity [VarDecl]
forall st. [Id] -> [Token] -> AParser st [VarDecl]
varDeclType (((Id, Variance) -> Id) -> [(Id, Variance)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, Variance) -> Id
forall a b. (a, b) -> a
fst [(Id, Variance)]
vs) [Token]
ps) AParser st [GenVarDecl]
-> AParser st [GenVarDecl] -> AParser st [GenVarDecl]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st [GenVarDecl]
forall st. ParsecT String (AnnoState st) Identity [GenVarDecl]
other
      else AParser st [GenVarDecl]
forall st. ParsecT String (AnnoState st) Identity [GenVarDecl]
other

-- * patterns

{- | different legal 'TermToken's possibly excluding 'funS' or
'equalS' for case or let patterns resp. -}
tokenPattern :: TokenMode -> AParser st Term
tokenPattern :: TokenMode -> AParser st Term
tokenPattern b :: TokenMode
b = (Token -> Term)
-> ParsecT String (AnnoState st) Identity Token -> AParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Term
TermToken (TokenMode -> ParsecT String (AnnoState st) Identity Token
forall st. TokenMode -> AParser st Token
aToken TokenMode
b ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity Token
forall st. CharParser st String -> CharParser st Token
pToken (String -> CharParser (AnnoState st) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "_"))
-- a single underscore serves as wildcard pattern

-- | 'tokenPattern' or 'BracketTerm'
primPattern :: TokenMode -> AParser st Term
primPattern :: TokenMode -> AParser st Term
primPattern b :: TokenMode
b = TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
tokenPattern TokenMode
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term -> ([Term] -> Range -> Term) -> AParser st Term
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st Term
forall st. AParser st Term
pattern (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Squares)
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term -> ([Term] -> Range -> Term) -> AParser st Term
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st Term
forall st. AParser st Term
pattern (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Braces)
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([Term] -> Range -> Term)
-> AParser st Term
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 Term
forall st. AParser st Term
pattern AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
forall st. AParser st Term
varTerm AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
forall st. AParser st Term
qualOpName)
          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
anComma (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Parens)

mkMixfixTerm :: [Term] -> Term
mkMixfixTerm :: [Term] -> Term
mkMixfixTerm ts :: [Term]
ts = case [Term]
ts of
    [hd :: Term
hd] -> Term
hd
    _ -> [Term] -> Term
MixfixTerm [Term]
ts

-- | several 'typedPattern'
mixPattern :: TokenMode -> AParser st Term
mixPattern :: TokenMode -> AParser st Term
mixPattern = ([Term] -> Term)
-> ParsecT String (AnnoState st) Identity [Term] -> AParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Term] -> Term
mkMixfixTerm (ParsecT String (AnnoState st) Identity [Term] -> AParser st Term)
-> (TokenMode -> ParsecT String (AnnoState st) Identity [Term])
-> TokenMode
-> AParser st Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st Term -> ParsecT String (AnnoState st) Identity [Term]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (AParser st Term -> ParsecT String (AnnoState st) Identity [Term])
-> (TokenMode -> AParser st Term)
-> TokenMode
-> ParsecT String (AnnoState st) Identity [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
asPattern

-- | a possibly typed ('parseType') pattern
typedPattern :: TokenMode -> AParser st Term
typedPattern :: TokenMode -> AParser st Term
typedPattern b :: TokenMode
b = do
    Term
t <- TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
primPattern TokenMode
b
    do Token
c <- AParser st Token
forall st. AParser st Token
colT
       Type
ty <- AParser st Type
forall st. AParser st Type
parseType
       Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
MixfixTerm [Term
t, TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
OfType Type
ty (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c]
      AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- | top-level pattern (possibly 'AsPattern')
asPattern :: TokenMode -> AParser st Term
asPattern :: TokenMode -> AParser st Term
asPattern b :: TokenMode
b = do
    Term
v <- TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
typedPattern TokenMode
b
    case Term
v of
      TermToken tt :: Token
tt -> if Token -> Bool
isPlace Token
tt then Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v else do
          Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
asP
          Term
t <- TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
typedPattern TokenMode
b
          Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term -> Range -> Term
AsPattern (Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl ([Token] -> Id
mkId [Token
tt]) ([Type] -> Type
MixfixType [])
                              SeparatorKind
Other (Range -> VarDecl) -> Range -> VarDecl
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c) Term
t (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
        AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
      _ -> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | an unrestricted 'asPattern'
pattern :: AParser st Term
pattern :: AParser st Term
pattern = TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
mixPattern []

myChoice :: [(AParser st Token, a)] -> AParser st (a, Token)
myChoice :: [(AParser st Token, a)] -> AParser st (a, Token)
myChoice = [AParser st (a, Token)] -> AParser st (a, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st (a, Token)] -> AParser st (a, Token))
-> ([(AParser st Token, a)] -> [AParser st (a, Token)])
-> [(AParser st Token, a)]
-> AParser st (a, Token)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((AParser st Token, a) -> AParser st (a, Token))
-> [(AParser st Token, a)] -> [AParser st (a, Token)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (p :: AParser st Token
p, a :: a
a) -> do
   Token
t <- AParser st Token
p
   (a, Token) -> AParser st (a, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, Token
t))

-- | a 'Total' or 'Partial' lambda dot
lamDot :: AParser st (Partiality, Token)
lamDot :: AParser st (Partiality, Token)
lamDot = [(AParser st Token, Partiality)] -> AParser st (Partiality, Token)
forall st a. [(AParser st Token, a)] -> AParser st (a, Token)
myChoice [ ([AParser st Token] -> AParser st Token
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st Token] -> AParser st Token)
-> [AParser st Token] -> AParser st Token
forall a b. (a -> b) -> a -> b
$ (String -> AParser st Token) -> TokenMode -> [AParser st Token]
forall a b. (a -> b) -> [a] -> [b]
map (String -> AParser st Token
forall st. String -> AParser st Token
asKey (String -> AParser st Token)
-> (String -> String) -> String -> AParser st Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
exMark)) [String
dotS, String
cDot], Partiality
Total)
                  , (AParser st Token
forall st. AParser st Token
dotT, Partiality
Partial)]

-- | patterns between 'lamS' and 'lamDot'
lamPattern :: AParser st [Term]
lamPattern :: AParser st [Term]
lamPattern =
    (ParsecT String (AnnoState st) Identity (Partiality, Token)
-> ParsecT String (AnnoState st) Identity (Partiality, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead ParsecT String (AnnoState st) Identity (Partiality, Token)
forall st. AParser st (Partiality, Token)
lamDot ParsecT String (AnnoState st) Identity (Partiality, Token)
-> AParser st [Term] -> AParser st [Term]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Term] -> AParser st [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return []) AParser st [Term] -> AParser st [Term] -> AParser st [Term]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
typedPattern [] AParser st Term -> AParser st [Term] -> AParser st [Term]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> AParser st [Term]
forall st. AParser st [Term]
lamPattern

-- * terms

{- | 'Token's that may occur in 'Term's including literals
   'scanFloat', 'scanString' but excluding 'ifS', 'whenS' and 'elseS'
   to allow a quantifier after 'whenS'. In case-terms also 'barS' will
   be excluded on the top-level. -}

tToken :: TokenMode -> AParser st Token
tToken :: TokenMode -> AParser st Token
tToken b :: TokenMode
b = CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String
forall st. CharParser st String
scanFloat
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanString
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanQuotedChar CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
scanDotWords
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st.
TokenMode -> CharParser st String -> CharParser st String
reserved [String
ifS, String
whenS, String
elseS] CharParser (AnnoState st) String
forall st. CharParser st String
scanHCWords
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall st.
TokenMode -> CharParser st String -> CharParser st String
reserved TokenMode
b CharParser (AnnoState st) String
forall st. CharParser st String
scanHCSigns
    CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CharParser (AnnoState st) String
forall st. CharParser st String
placeS CharParser (AnnoState st) String
-> String -> CharParser (AnnoState st) String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "id/literal")

-- | 'tToken' as 'Term' plus 'exEqual' and 'equalS'
termToken :: TokenMode -> AParser st Term
termToken :: TokenMode -> AParser st Term
termToken b :: TokenMode
b = (Token -> Term)
-> ParsecT String (AnnoState st) Identity Token -> AParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Term
TermToken (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
exEqual ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
equalS ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> TokenMode -> ParsecT String (AnnoState st) Identity Token
forall st. TokenMode -> AParser st Token
tToken TokenMode
b)

-- | 'termToken' plus 'BracketTerm's
primTerm :: TokenMode -> AParser st Term
primTerm :: TokenMode -> AParser st Term
primTerm b :: TokenMode
b = TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
termToken TokenMode
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term -> ([Term] -> Range -> Term) -> AParser st Term
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBraces AParser st Term
forall st. AParser st Term
term (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Braces)
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term -> ([Term] -> Range -> Term) -> AParser st Term
forall st a b. AParser st a -> ([a] -> Range -> b) -> AParser st b
mkBrackets AParser st Term
forall st. AParser st Term
term (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Squares)
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([Term] -> Range -> Term)
-> AParser st Term
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 Term
forall st. AParser st Term
termInParens 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
anComma (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Parens)

-- | how the keyword 'inS' should be treated
data InMode = NoIn   -- ^ next 'inS' belongs to 'letS'
            | WithIn -- ^ 'inS' is the element test

-- | all 'Term's that start with a unique keyword
baseTerm :: (InMode, TokenMode) -> AParser st Term
baseTerm :: (InMode, TokenMode) -> AParser st Term
baseTerm b :: (InMode, TokenMode)
b = (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
ifTerm (InMode, TokenMode)
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
whenTerm (InMode, TokenMode)
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
exTerm (InMode, TokenMode)
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
lambdaTerm (InMode, TokenMode)
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
caseTerm (InMode, TokenMode)
b
    AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
letTerm (InMode, TokenMode)
b

-- | 'whenS' possibly followed by an 'elseS'
whenTerm :: (InMode, TokenMode) -> AParser st Term
whenTerm :: (InMode, TokenMode) -> AParser st Term
whenTerm b :: (InMode, TokenMode)
b = do
    Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
whenS
    Term
c <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    let l1 :: [Term]
l1 = [Token -> Term
TermToken Token
i, Term
c]
    do Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
elseS
       Term
e <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
       Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
MixfixTerm ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
l1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Token -> Term
TermToken Token
t, Term
e]
      AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> Term
MixfixTerm [Term]
l1)

{- | 'ifS' possibly followed by 'thenS' and 'elseS'
yielding a 'MixfixTerm' -}
ifTerm :: (InMode, TokenMode) -> AParser st Term
ifTerm :: (InMode, TokenMode) -> AParser st Term
ifTerm b :: (InMode, TokenMode)
b = do
    Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ifS
    Term
c <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    let l1 :: [Term]
l1 = [Token -> Term
TermToken Token
i, Term
c]
    do Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
thenS
       Term
e <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
       let l2 :: [Term]
l2 = [Term]
l1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Token -> Term
TermToken Token
t, Term
e]
       do Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
elseS
          Term
f <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
          Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
MixfixTerm ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
l2 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Token -> Term
TermToken Token
s, Term
f]
         AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> Term
MixfixTerm [Term]
l2)
      AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> Term
MixfixTerm [Term]
l1)

-- | unrestricted terms including qualified names
termInParens :: AParser st Term
termInParens :: AParser st Term
termInParens = AParser st Term
forall st. AParser st Term
term AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
forall st. AParser st Term
varTerm AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
forall st. AParser st Term
qualOpName AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Term
forall st. AParser st Term
qualPredName

-- | a qualified 'var'
varTerm :: AParser st Term
varTerm :: AParser st Term
varTerm = do
    Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
varS
    Id
i <- GenParser Char (AnnoState st) Id
forall st. GenParser Char st Id
var
    Token
c <- AParser st Token
forall st. CharParser st Token
colonST
    Type
t <- AParser st Type
forall st. AParser st Type
parseType
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
i Type
t SeparatorKind
Other (Range -> VarDecl) -> Range -> VarDecl
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
v [] Token
c

-- | 'opS' or 'functS'
opBrand :: AParser st (Token, OpBrand)
opBrand :: AParser st (Token, OpBrand)
opBrand = ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity OpBrand
-> AParser st (Token, OpBrand)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
opS) (OpBrand -> ParsecT String (AnnoState st) Identity OpBrand
forall (m :: * -> *) a. Monad m => a -> m a
return OpBrand
Op)
    AParser st (Token, OpBrand)
-> AParser st (Token, OpBrand) -> AParser st (Token, OpBrand)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity OpBrand
-> AParser st (Token, OpBrand)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
functS) (OpBrand -> ParsecT String (AnnoState st) Identity OpBrand
forall (m :: * -> *) a. Monad m => a -> m a
return OpBrand
Fun)

parsePolyId :: AParser st PolyId
parsePolyId :: AParser st PolyId
parsePolyId = do
    [Token]
l <- GenParser Char (AnnoState st) [Token]
-> GenParser Char (AnnoState st) [Token]
forall tok st a. GenParser tok st a -> GenParser tok st a
try GenParser Char (AnnoState st) [Token]
forall st. GenParser Char st [Token]
ite 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
<|> (TokenMode, TokenMode) -> GenParser Char (AnnoState st) [Token]
forall st. (TokenMode, TokenMode) -> GenParser Char st [Token]
start (TokenMode, TokenMode)
hcKeys
    if Token -> Bool
isPlace ([Token] -> Token
forall a. [a] -> a
last [Token]
l)
      then PolyId -> AParser st PolyId
forall (m :: * -> *) a. Monad m => a -> m a
return (PolyId -> AParser st PolyId) -> PolyId -> AParser st PolyId
forall a b. (a -> b) -> a -> b
$ Id -> [TypeArg] -> Range -> PolyId
PolyId ([Token] -> [Id] -> Range -> Id
Id [Token]
l [] Range
nullRange) [] Range
nullRange else do
        (cs :: [Id]
cs, ps :: Range
ps) <- ([Id], Range)
-> ParsecT String (AnnoState st) Identity ([Id], Range)
-> ParsecT String (AnnoState st) Identity ([Id], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) (ParsecT String (AnnoState st) Identity ([Id], Range)
-> ParsecT String (AnnoState st) Identity ([Id], Range)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String (AnnoState st) Identity ([Id], Range)
 -> ParsecT String (AnnoState st) Identity ([Id], Range))
-> ParsecT String (AnnoState st) Identity ([Id], Range)
-> ParsecT String (AnnoState st) Identity ([Id], Range)
forall a b. (a -> b) -> a -> b
$ (TokenMode, TokenMode)
-> ParsecT String (AnnoState st) Identity ([Id], Range)
forall st.
(TokenMode, TokenMode) -> GenParser Char st ([Id], Range)
comps (TokenMode, TokenMode)
hcKeys)
        (tys :: [[TypeArg]]
tys, qs :: Range
qs) <- ([[TypeArg]], Range)
-> ParsecT String (AnnoState st) Identity ([[TypeArg]], Range)
-> ParsecT String (AnnoState st) Identity ([[TypeArg]], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) (ParsecT String (AnnoState st) Identity ([[TypeArg]], Range)
 -> ParsecT String (AnnoState st) Identity ([[TypeArg]], Range))
-> ParsecT String (AnnoState st) Identity ([[TypeArg]], Range)
-> ParsecT String (AnnoState st) Identity ([[TypeArg]], Range)
forall a b. (a -> b) -> a -> b
$
                AParser st [TypeArg]
-> AParser st Token
-> AParser st Token
-> AParser st Token
-> ([[TypeArg]] -> Range -> ([[TypeArg]], Range))
-> ParsecT String (AnnoState st) Identity ([[TypeArg]], 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 [TypeArg]
forall st. AParser st [TypeArg]
typeVars AParser st Token
forall st. CharParser st Token
oBracketT AParser st Token
forall st. CharParser st Token
cBracketT AParser st Token
forall st. CharParser st Token
semiT (,)
        [Token]
u <- AParser st Token -> GenParser Char (AnnoState st) [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many AParser st Token
forall st. CharParser st Token
placeT
        PolyId -> AParser st PolyId
forall (m :: * -> *) a. Monad m => a -> m a
return (PolyId -> AParser st PolyId) -> PolyId -> AParser st PolyId
forall a b. (a -> b) -> a -> b
$ Id -> [TypeArg] -> Range -> PolyId
PolyId ([Token] -> [Id] -> Range -> Id
Id ([Token]
l [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
u) [Id]
cs Range
ps) ([[TypeArg]] -> [TypeArg]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TypeArg]]
tys) Range
qs

-- | a qualified operation (with 'opBrand')
qualOpName :: AParser st Term
qualOpName :: AParser st Term
qualOpName = do
    (v :: Token
v, b :: OpBrand
b) <- AParser st (Token, OpBrand)
forall st. AParser st (Token, OpBrand)
opBrand
    PolyId
i <- AParser st PolyId
forall st. AParser st PolyId
parsePolyId
    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
i
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
b PolyId
i TypeScheme
t [] InstKind
Infer (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
v [] Token
c

-- | a qualified predicate
qualPredName :: AParser st Term
qualPredName :: AParser st Term
qualPredName = do
    Token
v <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
predS
    PolyId
i <- AParser st PolyId
forall st. AParser st PolyId
parsePolyId
    Token
c <- AParser st Token
forall st. AParser st Token
colT
    TypeScheme
t <- PolyId -> AParser st TypeScheme
forall st. PolyId -> AParser st TypeScheme
typeScheme PolyId
i
    let p :: Range
p = Token -> [Token] -> Token -> Range
toRange Token
v [] Token
c
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Pred PolyId
i (Range -> TypeScheme -> TypeScheme
predTypeScheme Range
p TypeScheme
t) [] InstKind
Infer Range
p

{- | a qualifier expecting a further 'Type'.
'inS' is rejected for 'NoIn' -}
typeQual :: InMode -> AParser st (TypeQual, Token)
typeQual :: InMode -> AParser st (TypeQual, Token)
typeQual m :: InMode
m = [(AParser st Token, TypeQual)] -> AParser st (TypeQual, Token)
forall st a. [(AParser st Token, a)] -> AParser st (a, Token)
myChoice ([(AParser st Token, TypeQual)] -> AParser st (TypeQual, Token))
-> [(AParser st Token, TypeQual)] -> AParser st (TypeQual, Token)
forall a b. (a -> b) -> a -> b
$ (AParser st Token
forall st. AParser st Token
colT, TypeQual
OfType) (AParser st Token, TypeQual)
-> [(AParser st Token, TypeQual)] -> [(AParser st Token, TypeQual)]
forall a. a -> [a] -> [a]
: (AParser st Token
forall st. AParser st Token
asT, TypeQual
AsType) (AParser st Token, TypeQual)
-> [(AParser st Token, TypeQual)] -> [(AParser st Token, TypeQual)]
forall a. a -> [a] -> [a]
: case InMode
m of
    NoIn -> []
    WithIn -> [(String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS, TypeQual
InType)]

-- | a qualifier plus a subsequent type as mixfix term component
qualAndType :: InMode -> AParser st Term
qualAndType :: InMode -> AParser st Term
qualAndType i :: InMode
i = do
  (q :: TypeQual
q, p :: Token
p) <- InMode -> AParser st (TypeQual, Token)
forall st. InMode -> AParser st (TypeQual, Token)
typeQual InMode
i
  Type
ty <- AParser st Type
forall st. AParser st Type
parseType
  Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
q Type
ty (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
p

-- | a possibly type qualified ('typeQual') 'primTerm' or a 'baseTerm'
typedTerm :: (InMode, TokenMode) -> AParser st Term
typedTerm :: (InMode, TokenMode) -> AParser st Term
typedTerm (i :: InMode
i, b :: TokenMode
b) = do
    Term
t <- TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
primTerm TokenMode
b
    [Term]
tys <- AParser st Term -> ParsecT String (AnnoState st) Identity [Term]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (AParser st Term -> ParsecT String (AnnoState st) Identity [Term])
-> AParser st Term -> ParsecT String (AnnoState st) Identity [Term]
forall a b. (a -> b) -> a -> b
$ InMode -> AParser st Term
forall st. InMode -> AParser st Term
qualAndType InMode
i
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
tys then Term
t else [Term] -> Term
MixfixTerm ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Term
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
tys
  AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
baseTerm (InMode
i, TokenMode
b)

-- | several 'typedTerm's yielding a 'MixfixTerm'
mixTerm :: (InMode, TokenMode) -> AParser st Term
mixTerm :: (InMode, TokenMode) -> AParser st Term
mixTerm = ([Term] -> Term)
-> ParsecT String (AnnoState st) Identity [Term] -> AParser st Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Term] -> Term
mkMixfixTerm (ParsecT String (AnnoState st) Identity [Term] -> AParser st Term)
-> ((InMode, TokenMode)
    -> ParsecT String (AnnoState st) Identity [Term])
-> (InMode, TokenMode)
-> AParser st Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st Term -> ParsecT String (AnnoState st) Identity [Term]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (AParser st Term -> ParsecT String (AnnoState st) Identity [Term])
-> ((InMode, TokenMode) -> AParser st Term)
-> (InMode, TokenMode)
-> ParsecT String (AnnoState st) Identity [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
typedTerm

-- | keywords that start a new item
hasCaslStartKeywords :: [String]
hasCaslStartKeywords :: TokenMode
hasCaslStartKeywords =
    String
dotS String -> TokenMode -> TokenMode
forall a. a -> [a] -> [a]
: String
cDot String -> TokenMode -> TokenMode
forall a. a -> [a] -> [a]
: (TokenMode
hascasl_reserved_words TokenMode -> TokenMode -> TokenMode
forall a. Eq a => [a] -> [a] -> [a]
\\ [String
existsS, String
letS, String
caseS])

-- | a 'mixTerm' followed by 'whereS' and equations separated by 'optSemi'
whereTerm :: (InMode, TokenMode) -> AParser st Term
whereTerm :: (InMode, TokenMode) -> AParser st Term
whereTerm b :: (InMode, TokenMode)
b = do
    Term
t <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    do Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
whereS
       (es :: [ProgEq]
es, ps :: [Token]
ps, _ans :: [[Annotation]]
_ans) <- TokenMode
-> AParser st ProgEq
-> AParser st ([ProgEq], [Token], [[Annotation]])
forall st a.
TokenMode
-> AParser st a -> AParser st ([a], [Token], [[Annotation]])
itemAux TokenMode
hasCaslStartKeywords (AParser st ProgEq
 -> AParser st ([ProgEq], [Token], [[Annotation]]))
-> AParser st ProgEq
-> AParser st ([ProgEq], [Token], [[Annotation]])
forall a b. (a -> b) -> a -> b
$
         TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
forall st.
TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
patternTermPair [String
equalS] (InMode, TokenMode)
b String
equalS
         -- ignore collected annotations
       Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
Where [ProgEq]
es Term
t (Range -> Term) -> Range -> Term
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]
ps
      AParser st Term -> AParser st Term -> AParser st Term
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- | a 'whereTerm' called with ('WithIn', [])
term :: AParser st Term
term :: AParser st Term
term = (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
whereTerm (InMode
WithIn, [])

-- | a 'Universal', 'Unique' or 'Existential' 'QuantifiedTerm'
exQuant :: AParser st (Token, Quantifier)
exQuant :: AParser st (Token, Quantifier)
exQuant = [AParser st (Token, Quantifier)] -> AParser st (Token, Quantifier)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([AParser st (Token, Quantifier)]
 -> AParser st (Token, Quantifier))
-> [AParser st (Token, Quantifier)]
-> AParser st (Token, Quantifier)
forall a b. (a -> b) -> a -> b
$ ((Quantifier, String) -> AParser st (Token, Quantifier))
-> [(Quantifier, String)] -> [AParser st (Token, Quantifier)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: Quantifier
v, s :: String
s) -> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Quantifier
-> AParser st (Token, Quantifier)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
s) (ParsecT String (AnnoState st) Identity Quantifier
 -> AParser st (Token, Quantifier))
-> ParsecT String (AnnoState st) Identity Quantifier
-> AParser st (Token, Quantifier)
forall a b. (a -> b) -> a -> b
$ Quantifier -> ParsecT String (AnnoState st) Identity Quantifier
forall (m :: * -> *) a. Monad m => a -> m a
return Quantifier
v)
  [ (Quantifier
Universal, String
forallS)
  , (Quantifier
Unique, String
existsS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
exMark)
  , (Quantifier
Existential, String
existsS) ]

-- | a (possibly unique) existential 'QuantifiedTerm'
exTerm :: (InMode, TokenMode) -> AParser st Term
exTerm :: (InMode, TokenMode) -> AParser st Term
exTerm b :: (InMode, TokenMode)
b = do
    (p :: Token
p, q :: Quantifier
q) <- AParser st (Token, Quantifier)
forall st. AParser st (Token, Quantifier)
exQuant
    (vs :: [[VarDecl]]
vs, ps :: [Token]
ps) <- AParser st [VarDecl]
forall st. AParser st [VarDecl]
varDecls AParser st [VarDecl]
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([[VarDecl]], [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
anSemi
    Token
d <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
dotT
    Term
f <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
q ((VarDecl -> GenVarDecl) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> GenVarDecl
GenVarDecl ([VarDecl] -> [GenVarDecl]) -> [VarDecl] -> [GenVarDecl]
forall a b. (a -> b) -> a -> b
$ [[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
vs) Term
f (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
p [Token]
ps Token
d

lamDecls :: AParser st [Term]
lamDecls :: AParser st [Term]
lamDecls = AParser st [Term] -> AParser st [Term]
forall tok st a. GenParser tok st a -> GenParser tok st a
try ((do
    (vs :: [[VarDecl]]
vs, _) <- GenParser Char (AnnoState st) [VarDecl]
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([[VarDecl]], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy GenParser Char (AnnoState st) [VarDecl]
forall st. AParser st [VarDecl]
varDecls GenParser Char (AnnoState st) Token
forall st. AParser st Token
anSemi
    ParsecT String (AnnoState st) Identity (Partiality, Token)
-> ParsecT String (AnnoState st) Identity (Partiality, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead ParsecT String (AnnoState st) Identity (Partiality, Token)
forall st. AParser st (Partiality, Token)
lamDot
    [Term] -> AParser st [Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> AParser st [Term]) -> [Term] -> AParser st [Term]
forall a b. (a -> b) -> a -> b
$ case [[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
vs of
      [VarDecl (Id [t :: Token
t] [] _) ty :: Type
ty _ ps :: Range
ps] ->
          -- this may be a constant constructor
          [[Term] -> Term
MixfixTerm [Token -> Term
TermToken Token
t, TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
OfType Type
ty Range
ps]]
      vss :: [VarDecl]
vss -> (VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
vss) AParser st [Term] -> String -> AParser st [Term]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "VAR-DECL") AParser st [Term] -> AParser st [Term] -> AParser st [Term]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st [Term]
forall st. AParser st [Term]
lamPattern

-- | a 'LambdaTerm'
lambdaTerm :: (InMode, TokenMode) -> AParser st Term
lambdaTerm :: (InMode, TokenMode) -> AParser st Term
lambdaTerm b :: (InMode, TokenMode)
b = do
    Token
l <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
lamS
    [Term]
pl <- AParser st [Term]
forall st. AParser st [Term]
lamDecls
    (k :: Partiality
k, d :: Token
d) <- AParser st (Partiality, Token)
forall st. AParser st (Partiality, Token)
lamDot
    Term
t <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm (if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
pl then [BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Parens [] Range
nullRange]
                         else [Term]
pl) Partiality
k Term
t (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
l [] Token
d

-- | a 'CaseTerm' with 'funS' excluded in 'patternTermPair'
caseTerm :: (InMode, TokenMode) -> AParser st Term
caseTerm :: (InMode, TokenMode) -> AParser st Term
caseTerm (i :: InMode
i, _) = do
    Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
caseS
    Term
t <- AParser st Term
forall st. AParser st Term
term
    Token
o <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ofS
    (ts :: [ProgEq]
ts, ps :: [Token]
ps) <- TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
forall st.
TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
patternTermPair [String
funS] (InMode
i, [String
barS]) String
funS AParser st ProgEq
-> AParser st Token
-> GenParser Char (AnnoState st) ([ProgEq], [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
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ Term -> [ProgEq] -> Range -> Term
CaseTerm Term
t [ProgEq]
ts (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Token
o Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

{- | a 'LetTerm' with 'equalS' excluded in 'patternTermPair'
(called with 'NoIn') -}
letTerm :: (InMode, TokenMode) -> AParser st Term
letTerm :: (InMode, TokenMode) -> AParser st Term
letTerm b :: (InMode, TokenMode)
b = do
    Token
l <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
letS
    (es :: [ProgEq]
es, ps :: [Token]
ps) <- TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
forall st.
TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
patternTermPair [String
equalS] (InMode
NoIn, []) String
equalS AParser st ProgEq
-> AParser st Token
-> GenParser Char (AnnoState st) ([ProgEq], [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
    Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS
    Term
t <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b
    Term -> AParser st Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> AParser st Term) -> Term -> AParser st Term
forall a b. (a -> b) -> a -> b
$ LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
Let [ProgEq]
es Term
t (Range -> Term) -> Range -> Term
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
l [Token]
ps Token
i

-- | a customizable pattern equation
patternTermPair :: TokenMode -> (InMode, TokenMode) -> String
                -> AParser st ProgEq
patternTermPair :: TokenMode -> (InMode, TokenMode) -> String -> AParser st ProgEq
patternTermPair b1 :: TokenMode
b1 b2 :: (InMode, TokenMode)
b2 sep :: String
sep = do
    Term
p <- TokenMode -> AParser st Term
forall st. TokenMode -> AParser st Term
mixPattern TokenMode
b1
    Token
s <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
sep
    Term
t <- (InMode, TokenMode) -> AParser st Term
forall st. (InMode, TokenMode) -> AParser st Term
mixTerm (InMode, TokenMode)
b2
    ProgEq -> AParser st ProgEq
forall (m :: * -> *) a. Monad m => a -> m a
return (ProgEq -> AParser st ProgEq) -> ProgEq -> AParser st ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
p Term
t (Range -> ProgEq) -> Range -> ProgEq
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
s