885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose{- |

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseModule : $Header$

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseCopyright : (c) Christian Maeder and Uni Bremen 2002-2004

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseMaintainer : hets@tzi.de

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseStability : provisional

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosePortability : portable

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose parser for HasCASL kinds, types, terms, patterns and equations

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-}

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bosemodule HasCASL.ParseTerm where

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.AnnoState

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.Id

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.Keywords

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.Lexer

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport HasCASL.HToken

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport HasCASL.As

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Boseimport Common.Lib.Parsec

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- * key sign tokens

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | keywords for the variance of kinds

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseplusT, minusT :: AParser Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseplusT = asKey plusS

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseminusT = asKey minusS

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a keyword string not followed by a question mark

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosenoQuMark :: String -> AParser Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosenoQuMark s = try $ asKey s << notFollowedBy (char '?')

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a colon not followed by a question mark

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosecolT :: AParser Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosecolT = noQuMark colonS

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a colon immediately followed by a question mark

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseqColonT :: AParser Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseqColonT = asKey (colonS++quMark)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- * parser for bracketed lists

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a generic bracket parser

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosebracketParser :: AParser a -> AParser Token -> AParser Token -> AParser Token

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose -> ([a] -> [Pos] -> b) -> AParser b

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosebracketParser parser op cl sep k =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do o <- op

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose (ts, ps) <- option ([], []) (parser `separatedBy` sep)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose c <- cl

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (k ts (toPos o ps c))

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parser for square brackets

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemkBrackets :: AParser a -> ([a] -> [Pos] -> b) -> AParser b

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemkBrackets p c = bracketParser p oBracketT cBracketT anComma c

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parser for braces

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemkBraces :: AParser a -> ([a] -> [Pos] -> b) -> AParser b

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemkBraces p c = bracketParser p oBraceT cBraceT anComma c

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- * kinds

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parse a simple class name or the type universe as kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseClassId :: AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseClassId = fmap (\c -> if showId c "" == "Type"

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose then Universe [posOfId c]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose else ClassKind c MissingKind) classId

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | do 'parseClassId' or a downset or an intersection kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseSimpleKind :: AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseSimpleKind = parseClassId

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|>

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do o <- oParenT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose (cs, ps) <- kind `separatedBy` anComma

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose c <- cParenT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (if isSingle cs then head cs else

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose Intersection cs (toPos o ps c))

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|>

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do o <- oBraceT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose i <- pToken scanHCWords

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose d <- dotT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose j <- asKey (tokStr i)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose l <- lessT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose t <- parseType

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose p <- cBraceT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (Downset (Just i) t MissingKind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose (map tokPos [o,d,j,l,p]))

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | do 'parseSimpleKind' and check for an optional 'Variance'

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseExtKind :: AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseparseExtKind = do k <- parseSimpleKind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do s <- plusT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (ExtKind k CoVar [tokPos s])

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|>

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do m <- minusT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (ExtKind k ContraVar [tokPos m])

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|> return k

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parse a (right associative) function kind for a given argument kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosearrowKind :: Kind -> AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosearrowKind k1 =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do a <- asKey funS

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose k2 <- kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (FunKind k1 k2 $ [tokPos a])

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parse a function kind but reject an extended kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bosekind :: AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bosekind =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do k1 <- parseExtKind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose arrowKind k1 <|> case k1 of

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ExtKind _ CoVar _ -> unexpected "co-variance of kind"

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ExtKind _ ContraVar _ -> unexpected "contra-variance of kind"

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ExtKind k InVar _ -> return k

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose _ -> return k1

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | parse a function kind but accept an extended kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseextKind :: AParser Kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseextKind =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do k1 <- parseExtKind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose arrowKind k1 <|> return k1

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- * type variables

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- a (simple) type variable with a 'Variance'

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseextTypeVar :: AParser (TypeId, Variance, Pos)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BoseextTypeVar = do t <- typeVar

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do a <- plusT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (t, CoVar, tokPos a)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|>

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do a <- minusT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (t, ContraVar, tokPos a)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|> return (t, InVar, nullPos)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- several 'extTypeVar' with a 'Kind'

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosetypeVars :: AParser [TypeArg]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosetypeVars = do (ts, ps) <- extTypeVar `separatedBy` anComma

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do c <- colT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose if let isInVar(_, InVar, _) = True

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose isInVar(_,_,_) = False

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose in all isInVar ts then

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do k <- extKind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (makeTypeArgs ts ps [tokPos c] k)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose else do k <- kind

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return (makeTypeArgs ts ps [tokPos c] k)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|> typeDownset ts ps

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose <|> return (makeTypeArgs ts ps [] star)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- 'parseType' a 'Downset' starting with 'lessT'

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosetypeDownset :: [(TypeId, Variance, Pos)] -> [Token] -> AParser [TypeArg]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosetypeDownset vs ps =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose do l <- lessT

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose t <- parseType

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose return $ makeTypeArgs vs ps [tokPos l]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose (Downset Nothing t MissingKind [])

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | add the 'Kind' to all 'extTypeVar' and yield a 'TypeArg'

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemakeTypeArgs :: [(TypeId, Variance, Pos)] -> [Token]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose -> [Pos] -> Kind -> [TypeArg]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosemakeTypeArgs ts ps qs k =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose zipWith (mergeVariance Comma k) (init ts)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose (map ((:[]). tokPos) ps)

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose ++ [mergeVariance Other k (last ts) qs]

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose where mergeVariance c (ExtKind e InVar _) (t, v, p) q =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose TypeArg t (ExtKind e v [p]) c q

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose mergeVariance c e (t, _, _) p =

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose TypeArg t e c p

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a single 'TypeArg' (parsed by 'typeVars')

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosesingleTypeArg :: AParser TypeArg

885386b7e3f1c3e74b354576b98a092b0835d64eSumit BosesingleTypeArg = do as <- typeVars

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose case as of

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose [a] -> return a

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose _ -> unexpected "list of type arguments"

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose

885386b7e3f1c3e74b354576b98a092b0835d64eSumit Bose-- | a 'singleTypArg' put in parentheses

parenTypeArg :: AParser (TypeArg, [Token])

parenTypeArg =

do o <- oParenT

a <- singleTypeArg

p <- cParenT

return (a, [o, p])

-- | a 'singleTypeArg' possibly put in parentheses

typeArg :: AParser (TypeArg, [Token])

typeArg =

do a <- singleTypeArg

return (a, [])

<|> parenTypeArg

-- | several 'typeArg's

typeArgs :: AParser ([TypeArg], [Token])

typeArgs =

do l <- many1 typeArg

return (map fst l, concatMap snd l)

-- | a 'singleTypeArg' put in parentheses as 'TypePattern'

typePatternArg :: AParser TypePattern

typePatternArg =

do (a, ps) <- parenTypeArg

return $ TypePatternArg a $ map tokPos ps

-- * parse special tokens

type TokenMode = [String]

-- | parse a 'Token' of an 'Id' (to be declared)

-- but exclude the signs in 'TokenMode'

aToken :: TokenMode -> AParser Token

aToken b = pToken (scanQuotedChar <|> scanDotWords

<|> scanDigit <|> scanHCWords <|> placeS <|>

reserved b scanHCSigns)

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

idToken :: AParser Token

idToken = aToken []

-- * type patterns

-- 'TypePatternToken's within 'BracketTypePattern's

-- may recusively be 'idToken's.

-- Parenthesis are only legal for a 'typePatternArg'.

primTypePatternOrId :: AParser TypePattern

primTypePatternOrId = fmap TypePatternToken idToken

<|> mkBraces typePatternOrId (BracketTypePattern Braces)

<|> mkBrackets typePatternOrId (BracketTypePattern Squares)

<|> typePatternArg

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

typePatternOrId :: AParser TypePattern

typePatternOrId = do ts <- many1 primTypePatternOrId

return( if isSingle ts then head ts

else MixfixTypePattern ts)

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

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

typePatternToken :: AParser TypePattern

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

reserved [lessS, equalS] scanHCSigns))

-- | a 'typePatternToken' or something in braces (a 'typePattern'),

-- in square brackets (a 'typePatternOrId' covering compound lists)

-- or parenthesis ('typePatternArg')

primTypePattern :: AParser TypePattern

primTypePattern = typePatternToken

<|> typePatternArg

<|> mkBraces typePattern (BracketTypePattern Braces)

<|> mkBrackets typePatternOrId (BracketTypePattern Squares)

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

typePattern :: AParser TypePattern

typePattern = do ts <- many1 primTypePattern

let t = if isSingle ts then head ts

else MixfixTypePattern ts

in return t

-- * types

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

-- | type tokens with some symbols removed

typeToken :: AParser Type

typeToken = fmap TypeToken (pToken (scanHCWords <|> placeS <|>

reserved (lessS : equalS : barS :

hascasl_type_ops

++ hascasl_reserved_ops)

scanHCSigns))

-- | 'TypeToken's within 'BracketType's may recusively be

-- 'idToken's. Parenthesis may group a mixfix type

-- or may be interpreted as 'Intersection' later in a GEN-VAR-DECL.

primTypeOrId :: AParser Type

primTypeOrId = fmap TypeToken idToken

<|> mkBraces typeOrId (BracketType Braces)

<|> mkBrackets typeOrId (BracketType Squares)

<|> bracketParser typeOrId oParenT cParenT anComma

(BracketType Parens)

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

-- and possibly followed by a 'kindAnno'.

typeOrId :: AParser Type

typeOrId = do ts <- many1 primTypeOrId

let t = if isSingle ts then head ts

else MixfixType ts

in

kindAnno t

<|>

return(t)

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

kindAnno :: Type -> AParser 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 Type

primType = typeToken

<|> bracketParser parseType oParenT cParenT anComma

(BracketType Parens)

<|> mkBraces parseType (BracketType Braces)

<|> mkBrackets typeOrId (BracketType Squares)

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

lazyType :: AParser Type

lazyType = do q <- quMarkT

t <- primType

return (LazyType t [tokPos q])

<|> primType

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

mixType :: AParser Type

mixType = do ts <- many1 lazyType

let t = if isSingle ts then head ts else MixfixType ts

in kindAnno t

<|> return t

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

prodType :: AParser Type

prodType = do (ts, ps) <- mixType `separatedBy` crossT

return (if isSingle ts then head ts

else ProductType ts (map tokPos ps))

-- | a (right associativ) function type

parseType :: AParser Type

parseType =

do t1 <- prodType

do a <- arrowT

t2 <- parseType

return $ FunType t1 (fst a) t2 [snd a]

<|> return t1

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

arrowT :: AParser (Arrow, Pos)

arrowT = do a <- noQuMark funS

return (FunArr, tokPos a)

<|>

do a <- asKey pFun

return (PFunArr, tokPos a)

<|>

do a <- noQuMark contFun

return (ContFunArr, tokPos a)

<|>

do a <- asKey pContFun

return (PContFunArr, tokPos a)

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

typeScheme :: AParser 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 ++ ps)

<|> fmap simpleTypeScheme parseType

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

partialTypeScheme :: AParser (Token, TypeScheme)

partialTypeScheme = do q <- qColonT

t <- parseType

return (q, simpleTypeScheme

(FunType (BracketType Parens [] [tokPos q])

PFunArr t [tokPos q]))

<|> bind (,) colT typeScheme

-- * varDecls and genVarDecls

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

varDecls :: AParser [VarDecl]

varDecls = do (vs, ps) <- var `separatedBy` anComma

varDeclType vs ps

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

varDeclType :: [Var] -> [Token] -> AParser [VarDecl]

varDeclType vs ps = do c <- colT

t <- parseType

return (makeVarDecls vs ps t (tokPos c))

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

makeVarDecls :: [Var] -> [Token] -> Type -> Pos -> [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 type variables with a 'typeDownset'.

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

genVarDecls:: AParser [GenVarDecl]

genVarDecls = do (vs, ps) <- var `separatedBy` anComma

fmap (map GenVarDecl) (varDeclType vs ps)

<|> fmap (map GenTypeVarDecl)

(typeDownset (map toExtTypeVar vs) ps)

where toExtTypeVar v@(Id ts cs qs) =

let s = last ts

n = Id (init ts) cs qs

p = tokPos s in

if tokStr s == plusS then

(n, CoVar, p)

else if tokStr s == minusS then

(n, ContraVar, p)

else (v, InVar, nullPos)

-- * patterns

-- | different legal 'PatternToken's (in- or excluding 'funS')

tokenPattern :: TokenMode -> AParser Pattern

tokenPattern b = fmap PatternToken (aToken b)

-- | 'tokenPattern' or 'BracketPattern'

primPattern :: TokenMode -> AParser Pattern

primPattern b = tokenPattern b

<|> mkBraces pattern (BracketPattern Braces)

<|> mkBrackets pattern (BracketPattern Squares)

<|> bracketParser pattern oParenT cParenT anComma

(BracketPattern Parens)

-- | several 'primPattern' possibly with a 'typeAnno'

mixPattern :: TokenMode -> AParser Pattern

mixPattern b =

do l <- many1 $ primPattern b

let p = if isSingle l then head l else MixfixPattern l

in typeAnno p <|> return p

-- | a type ('parseType') preceded by 'colT'

typeAnno :: Pattern -> AParser Pattern

typeAnno p =

do c <- colT

t <- parseType

return $ TypedPattern p t [tokPos c]

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

asPattern :: TokenMode -> AParser Pattern

asPattern b =

do v <- mixPattern b

do c <- asKey asP

t <- mixPattern b

case v of PatternToken _ -> return (AsPattern v t [tokPos c])

_ -> unexpected "complex pattern before '@'"

<|> return v

-- | an unrestricted 'asPattern'

pattern :: AParser Pattern

pattern = asPattern []

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

lamDot :: AParser (Partiality, Token)

lamDot = do d <- asKey (dotS++exMark) <|> asKey (cDot++exMark)

return (Total,d)

<|>

do d <- dotT

return (Partial,d)

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

lamPattern :: AParser [Pattern]

lamPattern =

do lookAhead lamDot

return []

<|> do p <- pattern

ps <- lamPattern

return (p : ps)

-- * terms

-- | an 'uninstOpId' possibly followed by types ('parseType') in brackets

-- and further places ('placeT')

instOpId :: AParser InstOpId

instOpId = do i@(Id is cs ps) <- uninstOpId

if isPlace (last is) then return (InstOpId i [] [])

else do (ts, qs) <- option ([], [])

(mkBrackets parseType (,))

u <- many placeT

return (InstOpId (Id (is++u) cs ps) ts qs)

-- | 'Token's that may occur in 'Term's including literals

-- ('scanFloat', 'scanString') excluding 'ifS' and 'barS'

tToken :: AParser Token

tToken = pToken(scanFloat <|> scanString

<|> scanQuotedChar <|> scanDotWords

<|> reserved [ifS] scanHCWords

<|> reserved [barS] scanHCSigns

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

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

termToken :: AParser Term

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

-- | 'termToken' plus 'BracketTerm's or 'parenTerm'

primTerm :: AParser Term

primTerm = termToken

<|> mkBraces term (BracketTerm Braces)

<|> mkBrackets term (BracketTerm Squares)

<|> parenTerm

-- | 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 -> AParser Term

baseTerm b = ifTerm b

<|> forallTerm b

<|> exTerm b

<|> lambdaTerm b

<|> caseTerm b

<|> letTerm b

-- | 'ifS' possibly followed by 'thenS' (for if-then-else)

-- yielding a 'MixfixTerm'.

ifTerm :: InMode -> AParser Term

ifTerm b =

do i <- asKey ifS

c <- mixTerm b

do t <- asKey thenS

e <- mixTerm b

return (MixfixTerm [TermToken i, c, TermToken t, e])

<|> return (MixfixTerm [TermToken i, c])

-- | a 'Term' in parentheses, may be a qualified name or a tuple

-- ('BracketTerm')

parenTerm :: AParser Term

parenTerm = do o <- oParenT

varTerm o

<|>

qualOpName o

<|>

qualPredName o

<|>

do (ts, ps) <- option ([],[]) (term `separatedBy` anComma)

p <- cParenT

return (BracketTerm Parens ts (toPos o ps p))

-- | a qualified 'var'

varTerm :: Token -> AParser Term

varTerm o = do v <- asKey varS

i <- var

c <- colT

t <- parseType

p <- cParenT

return (QualVar i t (toPos o [v, c] p))

-- | 'opS' or 'functS'

opBrand :: AParser (Token, OpBrand)

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

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

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

qualOpName :: Token -> AParser Term

qualOpName o =

do (v, b) <- opBrand

i <- instOpId

(c, t) <- partialTypeScheme

p <- cParenT

return $ QualOp b i t (toPos o [v, c] p)

-- | a qualified predicate

qualPredName :: Token -> AParser Term

qualPredName o =

do v <- asKey predS

i <- instOpId

c <- colT

t <- typeScheme

p <- cParenT

return $ QualOp Pred i (predTypeScheme t) (toPos o [v, c] p)

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

-- 'inS' is rejected for 'NoIn'

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

typeQual m =

do q <- colT

return (OfType, q)

<|>

do q <- asT

return (AsType, q)

<|>

case m of

NoIn -> pzero

WithIn ->

do q <- asKey inS

return (InType, q)

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

typedTerm :: InMode -> AParser Term

typedTerm b =

do t <- primTerm

do (q, p) <- typeQual b

ty <- parseType

return (TypedTerm t q ty [tokPos p])

<|> return t

<|> baseTerm b

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

mixTerm :: InMode -> AParser Term

mixTerm b =

do ts <- many1 $ typedTerm b

return $ if isSingle ts then head ts else MixfixTerm ts

-- | a 'mixTerm' called with 'WithIn'

term :: AParser Term

term = mixTerm WithIn

-- | a 'Universal' 'QuantifiedTerm'

forallTerm :: InMode -> AParser 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 (Token, Quantifier)

exQuant =

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

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

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

exTerm :: InMode -> AParser Term

exTerm b =

do (p, q) <- exQuant

(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 -> AParser Term

lambdaTerm b =

do l <- asKey lamS

pl <- lamPattern

(k, d) <- lamDot

t <- mixTerm b

return (LambdaTerm pl k t (toPos l [] d))

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

caseTerm :: InMode -> AParser Term

caseTerm b =

do c <- asKey caseS

t <- term

o <- asKey ofS

(ts, ps) <- patternTermPair ([funS]) b funS

`separatedBy` barT

return (CaseTerm t ts (map tokPos (c:o:ps)))

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

-- (called with 'NoIn')

letTerm :: InMode -> AParser Term

letTerm b =

do l <- asKey letS

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

`separatedBy` anSemi

i <- asKey inS

t <- mixTerm b

return (LetTerm es t (toPos l ps i))

-- | a customizable pattern equation

patternTermPair :: TokenMode -> InMode -> String -> AParser ProgEq

patternTermPair b1 b2 sep =

do p <- asPattern b1

s <- asKey sep

t <- mixTerm b2

return (ProgEq p t (tokPos s))