9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaDescription : parser for HasCASL kinds, types, terms, patterns and equations

228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2002-2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova

228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaMaintainer : Christian.Maeder@dfki.de

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovaStability : provisional

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovaPortability : portable

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakovaparser for HasCASL kinds, types, terms, patterns and equations

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova-}

228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova

c208973c890b8f993297720fd0247bc7481d4304Christian Maedermodule HasCASL.ParseTerm where

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakova

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakovaimport Common.AnnoState

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakovaimport Common.Id

0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina Sojakovaimport Common.Keywords

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakovaimport Common.Lexer

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakovaimport Common.Token

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakovaimport HasCASL.HToken

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakovaimport HasCASL.As

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakovaimport HasCASL.AsUtils

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakovaimport Text.ParserCombinators.Parsec

0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina Sojakovaimport Data.List ((\\))

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakova-- * key sign tokens

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova-- | a colon not followed by a question mark

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovacolT :: AParser st Token

0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina SojakovacolT = asKey colonS

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa

c35969f341eb137848e9c0874503bed8c419cbd2Kristina Sojakova-- | a colon immediately followed by a question mark

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina SojakovaqColonT :: AParser st Token

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovaqColonT = asKey colonQuMark

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova-- * parser for bracketed lists

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina Sojakova-- | a generic bracket parser

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina SojakovabracketParser :: AParser st a -> AParser st Token -> AParser st Token

228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova -> AParser st Token -> ([a] -> Range -> b) -> AParser st b

0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina SojakovabracketParser parser op cl sep k = do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder o <- op

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova (ts, ps) <- option ([], []) $ separatedBy parser sep

22ade8eac560459be401bb34c010f0a981ec02bdKristina Sojakova c <- cl

3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova return $ k ts $ toPos o ps c

22ade8eac560459be401bb34c010f0a981ec02bdKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- | parser for square brackets

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovamkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovamkBrackets p c = bracketParser p oBracketT cBracketT anComma c

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- | parser for braces

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaedermkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaedermkBraces p c = bracketParser p oBraceT cBraceT anComma c

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- * kinds

99c3239092cab05eaca2f021e5edef2eab00ba01Christian Maeder

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | parse a simple class name or the type universe as kind

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaparseClassId :: AParser st Kind

4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescuparseClassId = fmap ClassKind classId

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | do 'parseClassId' or a kind in parenthessis

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaederparseSimpleKind :: AParser st Kind

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaparseSimpleKind = parseClassId <|> (oParenT >> kind << cParenT)

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- | do 'parseSimpleKind' and check for an optional 'Variance'

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaederparseExtKind :: AParser st (Variance, Kind)

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaparseExtKind = bind (,) variance parseSimpleKind

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | parse a (right associative) function kind for a given argument kind

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaederarrowKind :: (Variance, Kind) -> AParser st Kind

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaederarrowKind (v, k) = do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder a <- asKey funS

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder k2 <- kind

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova return $ FunKind v k k2 $ tokPos a

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | parse a function kind but reject an extended kind

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakovakind :: AParser st Kind

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakovakind = do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder k1@(v, k) <- parseExtKind

53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova arrowKind k1 <|> case v of

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova InVar -> return k

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa _ -> unexpected "variance of kind"

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova-- | parse a function kind but accept an extended kind

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovaextKind :: AParser st (Variance, Kind)

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovaextKind = do

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova k1 <- parseExtKind

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder do k <- arrowKind k1

f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova return (InVar, k)

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova <|> return k1

da16798d538221b43043890083523e5a04540f2eChristian Maeder

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova-- * type variables

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maedervariance :: AParser st Variance

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakovavariance = let l = [CoVar, ContraVar] in

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakova choice (map ( \ v -> asKey (show v) >> return v) l) <|> return InVar

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- a (simple) type variable with a 'Variance'

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaextVar :: AParser st Id -> AParser st (Id, Variance)

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaextVar vp = bind (,) vp variance

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- several 'extVar' with a 'Kind'

2eb5f647dafdbb3a16675dd47256f9641ea234ebKristina SojakovatypeVars :: AParser st [TypeArg]

2eb5f647dafdbb3a16675dd47256f9641ea234ebKristina SojakovatypeVars = do

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova (ts, ps) <- extVar typeVar `separatedBy` anComma

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova typeKind ts ps

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaallIsInVar :: [(Id, Variance)] -> Bool

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina SojakovaallIsInVar = all ( \ (_, v) -> case v of

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova InVar -> True

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova _ -> False)

2eb5f647dafdbb3a16675dd47256f9641ea234ebKristina Sojakova

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova-- 'parseType' a 'Downset' starting with 'lessT'

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina SojakovatypeKind :: [(Id, Variance)] -> [Token]

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova -> AParser st [TypeArg]

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina SojakovatypeKind vs ps = do

2eb5f647dafdbb3a16675dd47256f9641ea234ebKristina Sojakova c <- colT

2eb5f647dafdbb3a16675dd47256f9641ea234ebKristina Sojakova if allIsInVar vs then do

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova (v, k) <- extKind

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder return $ makeTypeArgs vs ps v (VarKind k) $ tokPos c

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder else do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder k <- kind

99c3239092cab05eaca2f021e5edef2eab00ba01Christian Maeder return $ makeTypeArgs vs ps InVar (VarKind k) $ tokPos c

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder <|> do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder l <- lessT

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa t <- parseType

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova return $ makeTypeArgs vs ps InVar (Downset t) $ tokPos l

da16798d538221b43043890083523e5a04540f2eChristian Maeder <|> return (makeTypeArgs vs ps InVar MissingKind nullRange)

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova-- | add the 'Kind' to all 'extVar' and yield a 'TypeArg'

f20841e0b3d9311fd39f2615e43538214f720dd5Kristina SojakovamakeTypeArgs :: [(Id, Variance)] -> [Token]

f20841e0b3d9311fd39f2615e43538214f720dd5Kristina Sojakova -> Variance -> VarKind -> Range -> [TypeArg]

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina SojakovamakeTypeArgs ts ps vv vk qs =

88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder zipWith (mergeVariance Comma vv vk) (init ts)

88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder (map tokPos ps)

b9e7c27252b02c6e444fb5555dcf191dfaf3065bKristina Sojakova ++ [mergeVariance Other vv vk (last ts) qs]

da16798d538221b43043890083523e5a04540f2eChristian Maeder where

53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova mergeVariance c v k (t, InVar) q = TypeArg t v k rStar 0 c q

e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina Sojakova mergeVariance c _ k (t, v) q = TypeArg t v k rStar 0 c q

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | a single 'TypeArg' (parsed by 'typeVars')

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovasingleTypeArg :: AParser st TypeArg

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovasingleTypeArg = do

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder as <- typeVars

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder case as of

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova [a] -> return a

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova _ -> unexpected "list of type arguments"

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | a 'singleTypeArg' put in parentheses

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaparenTypeArg :: AParser st (TypeArg, [Token])

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovaparenTypeArg = do

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova o <- oParenT

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder a <- singleTypeArg

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova p <- cParenT

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova return (a, [o, p])

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa-- | a 'singleTypeArg' possibly put in parentheses

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovatypeArg :: AParser st (TypeArg, [Token])

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina SojakovatypeArg = do

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova a <- singleTypeArg

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova return (a, [])

f5e136145332e265f82919a1c36d5bf35e568251Christian Maeder <|> parenTypeArg

85ae7717e4102529f83a3e487d0a308a56dc8fc7Kristina Sojakova

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian Maeder-- | a 'singleTypeArg' put in parentheses as 'TypePattern'

66c6e29ddfa36396c7ebfc02d01d8d7e6c26976cChristian MaedertypePatternArg :: AParser st TypePattern

typePatternArg = do

(a, ps) <- parenTypeArg

return $ TypePatternArg a $ catPos 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 b = pToken $ scanQuotedChar <|> scanDigit <|> scanHCWords <|> placeS

<|> reserved b scanHCSigns

-- | just 'aToken' only excluding basic HasCASL keywords

idToken :: AParser st Token

idToken = aToken [] <|> pToken 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 = fmap TypePatternToken idToken

<|> mkBraces typePatternOrId (BracketTypePattern Braces)

<|> mkBrackets typePatternOrId (BracketTypePattern Squares)

<|> typePatternArg

-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'

mixTypePattern :: AParser st TypePattern -> AParser st TypePattern

mixTypePattern p = do

ts <- many1 p

return $ case ts of

[hd] -> hd

_ -> MixfixTypePattern ts

-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'

typePatternOrId :: AParser st TypePattern

typePatternOrId = mixTypePattern primTypePatternOrId

-- | those (top-level) 'Token's (less than 'idToken')

-- that may appear in 'TypePattern's as 'TypePatternToken'.

typePatternToken :: AParser st TypePattern

typePatternToken = fmap TypePatternToken $ pToken $ scanHCWords <|> placeS

<|> reserved [assignS, lessS, equalS] 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 = typePatternToken

<|> mkBrackets typePatternOrId (BracketTypePattern Squares)

<|> mkBraces typePattern (BracketTypePattern Braces)

<|> typePatternArg

-- several 'primTypePatter's possibly yielding a 'MixfixTypePattern'

typePattern :: AParser st TypePattern

typePattern = mixTypePattern 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 = fmap TypeToken $ pToken $ scanHCWords <|> placeS <|>

reserved (assignS : lessS : equalS : barS : hascasl_type_ops) 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 = fmap TypeToken idToken

<|> mkBrackets typeOrId (BracketType Squares)

<|> mkBraces typeOrId (BracketType Braces)

<|> bracketParser typeOrId oParenT cParenT anComma (BracketType Parens)

mkMixfixType :: AParser st Type -> AParser st Type

mkMixfixType p = do

ts <- many1 p

let t = case ts of

[hd] -> hd

_ -> MixfixType ts

kindAnno t <|> return t

-- | several 'primTypeOrId's possibly yielding a 'MixfixType'

-- and possibly followed by a 'kindAnno'.

typeOrId :: AParser st Type

typeOrId = mkMixfixType primTypeOrId

-- | a 'Kind' annotation starting with 'colT'.

kindAnno :: Type -> AParser st Type

kindAnno t = do

c <- colT

k <- kind

return $ KindedType t k $ tokPos c

-- | a typeToken' or a 'BracketType'. Square brackets may contain 'typeOrId'.

primType :: AParser st Type

primType = typeToken

<|> mkBrackets typeOrId (BracketType Squares)

<|> mkBraces parseType (BracketType Braces)

<|> bracketParser parseType oParenT cParenT anComma (BracketType Parens)

-- | a 'primType' possibly preceded by 'quMarkT'

lazyType :: AParser st Type

lazyType = fmap mkLazyType (quMarkT >> primType) <|> primType

-- | several 'lazyType's (as 'MixfixType') possibly followed by 'kindAnno'

mixType :: AParser st Type

mixType = mkMixfixType lazyType

-- | 'mixType' possibly interspersed with 'crossT'

prodType :: AParser st Type

prodType = do

(ts, ps) <- mixType `separatedBy` crossT

return $ mkProductTypeWithRange ts $ catPos ps

-- | a (right associativ) function type

parseType :: AParser st Type

parseType = do

t1 <- prodType

do a <- arrowT <?> funS

t2 <- parseType

return $ mkTypeAppl

(TypeName a (toRaw $ funKindWithRange $ posOfId a) 0) [t1, t2]

<|> return t1

-- | parse one of the four possible 'Arrow's

arrowT :: AParser st Id

arrowT = let l = [FunArr, PFunArr, ContFunArr, PContFunArr] in

choice $ map ( \ a -> do

t <- asKey $ show a

return $ mkId [placeTok, t, placeTok]) l

-- | parse a 'TypeScheme' using 'forallT', 'typeVars', 'dotT' and 'parseType'

typeScheme :: AParser st TypeScheme

typeScheme = do

f <- forallT

(ts, cs) <- typeVars `separatedBy` anSemi

d <- dotT

t <- typeScheme

return $ case t of

TypeScheme ots q ps -> TypeScheme (concat ts ++ ots) q

$ toPos f cs d `appRange` ps

<|> fmap simpleTypeScheme parseType

data TypeOrTypeScheme = PartialType Type | TotalTypeScheme TypeScheme

-- a 'TypeOrTypescheme' for a possibly partial constant (given by 'qColonT')

typeOrTypeScheme :: AParser st (Token, TypeOrTypeScheme)

typeOrTypeScheme = do

q <- qColonT

t <- parseType

return (q, PartialType t)

<|> do

q <- colT

s <- typeScheme

return (q, TotalTypeScheme s)

toPartialTypeScheme :: TypeOrTypeScheme -> TypeScheme

toPartialTypeScheme ts = case ts of

PartialType t -> simpleTypeScheme $ mkLazyType t

TotalTypeScheme s -> s

partialTypeScheme :: AParser st (Token, TypeScheme)

partialTypeScheme = do

(c, ts) <- typeOrTypeScheme

return (c, toPartialTypeScheme ts)

-- * varDecls and genVarDecls

-- | comma separated 'var' with 'varDeclType'

varDecls :: AParser st [VarDecl]

varDecls = do

(vs, ps) <- var `separatedBy` anComma

varDeclType vs ps

-- | a type ('parseType') following a colon

varDeclType :: [Id] -> [Token] -> AParser st [VarDecl]

varDeclType vs ps = do

c <- colonST

t <- parseType

return $ makeVarDecls vs ps t $ tokPos c

-- | attach the 'Type' to every 'Var'

makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]

makeVarDecls vs ps t q = zipWith ( \ v p -> VarDecl v t Comma $ tokPos p)

(init vs) ps ++ [VarDecl (last vs) t Other q]

-- | either like 'varDecls' or declared type variables.

-- A 'GenVarDecl' may later become a 'GenTypeVarDecl'.

genVarDecls:: AParser st [GenVarDecl]

genVarDecls = fmap (map ( \ g -> case g of

GenTypeVarDecl (TypeArg i v MissingKind _ n s ps) ->

GenTypeVarDecl (TypeArg i v (VarKind universe)

rStar n s ps)

_ -> g)) $ do

(vs, ps) <- extVar var `separatedBy` anComma

let other = fmap (map GenTypeVarDecl) (typeKind vs ps)

if allIsInVar vs then fmap (map GenVarDecl)

(varDeclType (map ( \ (i, _) -> i) vs) ps) <|> other

else other

-- * patterns

{- | different legal 'TermToken's possibly excluding 'funS' or

'equalS' for case or let patterns resp. -}

tokenPattern :: TokenMode -> AParser st Pattern

tokenPattern b = fmap TermToken (aToken b <|> pToken (string "_"))

-- a single underscore serves as wildcard pattern

-- | 'tokenPattern' or 'BracketTerm'

primPattern :: TokenMode -> AParser st Pattern

primPattern b = tokenPattern b

<|> mkBrackets pattern (BracketTerm Squares)

<|> mkBraces pattern (BracketTerm Braces)

<|> bracketParser (pattern <|> varTerm <|> qualOpName)

oParenT cParenT anComma (BracketTerm Parens)

mkMixfixTerm :: [Term] -> Term

mkMixfixTerm ts = case ts of

[hd] -> hd

_ -> MixfixTerm ts

-- | several 'typedPattern'

mixPattern :: TokenMode -> AParser st Pattern

mixPattern = fmap mkMixfixTerm . many1 . asPattern

-- | a possibly typed ('parseType') pattern

typedPattern :: TokenMode -> AParser st Pattern

typedPattern b = do

t <- primPattern b

do c <- colT

ty <- parseType

return $ MixfixTerm [t, MixTypeTerm OfType ty $ tokPos c]

<|> return t

-- | top-level pattern (possibly 'AsPattern')

asPattern :: TokenMode -> AParser st Pattern

asPattern b = do

v <- typedPattern b

case v of

TermToken tt -> if isPlace tt then return v else do

c <- asKey asP

t <- typedPattern b

return $ AsPattern (VarDecl (mkId [tt]) (MixfixType [])

Other $ tokPos c) t $ tokPos c

<|> return v

_ -> return v

-- | an unrestricted 'asPattern'

pattern :: AParser st Pattern

pattern = mixPattern []

myChoice :: [(AParser st Token, a)] -> AParser st (a, Token)

myChoice = choice . map ( \ (p, a) -> do

t <- p

return (a, t))

-- | a 'Total' or 'Partial' lambda dot

lamDot :: AParser st (Partiality, Token)

lamDot = myChoice [ (choice $ map (asKey . (++ exMark)) [dotS, cDot], Total)

, (dotT, Partial)]

-- | patterns between 'lamS' and 'lamDot'

lamPattern :: AParser st [Pattern]

lamPattern =

(lookAhead lamDot >> return []) <|> bind (:) (typedPattern []) 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 b = pToken (scanFloat

<|> scanString

<|> scanQuotedChar <|> scanDotWords

<|> reserved [ifS, whenS, elseS] scanHCWords

<|> reserved b scanHCSigns

<|> placeS <?> "id/literal")

-- | 'tToken' as 'Term' plus 'exEqual' and 'equalS'

termToken :: TokenMode -> AParser st Term

termToken b = fmap TermToken (asKey exEqual <|> asKey equalS <|> tToken b)

-- | 'termToken' plus 'BracketTerm's

primTerm :: TokenMode -> AParser st Term

primTerm b = termToken b

<|> mkBraces term (BracketTerm Braces)

<|> mkBrackets term (BracketTerm Squares)

<|> bracketParser termInParens oParenT cParenT anComma (BracketTerm 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 b = ifTerm b

<|> whenTerm b

<|> forallTerm b

<|> exTerm b

<|> lambdaTerm b

<|> caseTerm b

<|> letTerm b

-- | 'whenS' possibly followed by an 'elseS'

whenTerm :: (InMode, TokenMode) -> AParser st Term

whenTerm b = do

i <- asKey whenS

c <- mixTerm b

let l1 = [TermToken i, c]

do t <- asKey elseS

e <- mixTerm b

return $ MixfixTerm $ l1 ++ [TermToken t, e]

<|> return (MixfixTerm l1)

-- | 'ifS' possibly followed by 'thenS' and 'elseS'

-- yielding a 'MixfixTerm'

ifTerm :: (InMode, TokenMode) -> AParser st Term

ifTerm b = do

i <- asKey ifS

c <- mixTerm b

let l1 = [TermToken i, c]

do t <- asKey thenS

e <- mixTerm b

let l2 = l1 ++ [TermToken t, e]

do s <- asKey elseS

f <- mixTerm b

return $ MixfixTerm $ l2 ++ [TermToken s, f]

<|> return (MixfixTerm l2)

<|> return (MixfixTerm l1)

-- | unrestricted terms including qualified names

termInParens :: AParser st Term

termInParens = term <|> varTerm <|> qualOpName <|> qualPredName

-- | a qualified 'var'

varTerm :: AParser st Term

varTerm = do

v <- asKey varS

i <- var

c <- colonST

t <- parseType

return $ QualVar $ VarDecl i t Other $ toPos v [] c

-- | 'opS' or 'functS'

opBrand :: AParser st (Token, OpBrand)

opBrand = bind (,) (asKey opS) (return Op)

<|> bind (,) (asKey functS) (return Fun)

-- | a qualified operation (with 'opBrand')

qualOpName :: AParser st Term

qualOpName = do

(v, b) <- opBrand

i <- opId

(c, t) <- partialTypeScheme

return $ QualOp b i t [] $ toPos v [] c

-- | a qualified predicate

qualPredName :: AParser st Term

qualPredName = do

v <- asKey predS

i <- opId

c <- colT

t <- typeScheme

let p = toPos v [] c

return $ QualOp Pred i (predTypeScheme p t) [] p

-- | a qualifier expecting a further 'Type'.

-- 'inS' is rejected for 'NoIn'

typeQual :: InMode -> AParser st (TypeQual, Token)

typeQual m = myChoice $ [(colT, OfType), (asT, AsType)] ++ case m of

NoIn -> []

WithIn -> [(asKey inS, InType)]

-- | a possibly type qualified ('typeQual') 'primTerm' or a 'baseTerm'

typedTerm :: (InMode, TokenMode) -> AParser st Term

typedTerm (i, b) = do

t <- primTerm b

do (q, p) <- typeQual i

ty <- parseType

return $ MixfixTerm [t, MixTypeTerm q ty $ tokPos p]

<|> return t

<|> baseTerm (i, b)

-- | several 'typedTerm's yielding a 'MixfixTerm'

mixTerm :: (InMode, TokenMode) -> AParser st Term

mixTerm = fmap mkMixfixTerm . many1 . typedTerm

-- | keywords that start a new item

hasCaslStartKeywords :: [String]

hasCaslStartKeywords =

dotS : cDot : (hascasl_reserved_words \\ [existsS, letS, caseS])

-- | a 'mixTerm' followed by 'whereS' and equations separated by 'optSemi'

whereTerm :: (InMode, TokenMode) -> AParser st Term

whereTerm b = do

t <- mixTerm b

do p <- asKey whereS

(es, ps, _ans) <- itemAux hasCaslStartKeywords $

patternTermPair [equalS] b equalS

-- ignore collected annotations

return $ LetTerm Where es t $ catPos $ p : ps

<|> return t

-- | a 'whereTerm' called with ('WithIn', [])

term :: AParser st Term

term = whereTerm (WithIn, [])

-- | a 'Universal' 'QuantifiedTerm'

forallTerm :: (InMode, TokenMode) -> AParser st Term

forallTerm b = do

f <- forallT

(vs, ps) <- genVarDecls `separatedBy` anSemi

addAnnos

d <- dotT

t <- mixTerm b

return $ QuantifiedTerm Universal (concat vs) t $ toPos f ps d

-- | 'Unique' or 'Existential'

exQuant :: AParser st (Token, Quantifier)

exQuant = bind (,) (asKey (existsS++exMark)) (return Unique)

<|> bind (,) (asKey existsS) (return Existential)

-- | a (possibly unique) existential 'QuantifiedTerm'

exTerm :: (InMode, TokenMode) -> AParser st Term

exTerm b = do

(p, q) <- exQuant <?> existsS

(vs, ps) <- varDecls `separatedBy` anSemi

d <- dotT

f <- mixTerm b

return $ QuantifiedTerm q (map GenVarDecl (concat vs)) f $ toPos p ps d

-- | a 'LambdaTerm'

lambdaTerm :: (InMode, TokenMode) -> AParser st Term

lambdaTerm b = do

l <- asKey lamS

pl <- lamPattern

(k, d) <- lamDot

t <- mixTerm b

return $ LambdaTerm (if null pl then [BracketTerm Parens [] nullRange]

else pl) k t $ toPos l [] d

-- | a 'CaseTerm' with 'funS' excluded in 'patternTermPair'

caseTerm :: (InMode, TokenMode) -> AParser st Term

caseTerm (i, _) = do

c <- asKey caseS

t <- term

o <- asKey ofS

(ts, ps) <- patternTermPair [funS] (i, [barS]) funS `separatedBy` barT

return $ CaseTerm t ts $ catPos $ c : o : ps

-- | a 'LetTerm' with 'equalS' excluded in 'patternTermPair'

-- (called with 'NoIn')

letTerm :: (InMode, TokenMode) -> AParser st Term

letTerm b = do

l <- asKey letS

(es, ps) <- patternTermPair [equalS] (NoIn, []) equalS `separatedBy` anSemi

i <- asKey inS

t <- mixTerm b

return $ LetTerm Let es t $ toPos l ps i

-- | a customizable pattern equation

patternTermPair :: TokenMode -> (InMode, TokenMode) -> String

-> AParser st ProgEq

patternTermPair b1 b2 sep = do

p <- mixPattern b1

s <- asKey sep

t <- mixTerm b2

return $ ProgEq p t $ tokPos s