ParseTerm.hs revision 72909c6c1cfe9702f5910d0a135c8b55729c7917
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuModule : $Header$
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuDescription : parser for HasCASL kinds, types, terms, patterns and equations
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuMaintainer : Christian.Maeder@dfki.de
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuStability : provisional
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuPortability : portable
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuparser for HasCASL kinds, types, terms, patterns and equations
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuimport qualified Data.Set as Set
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * key sign tokens
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a colon not followed by a question mark
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiucolT :: AParser st Token
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiucolT = asKey colonS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * parser for bracketed lists
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a generic bracket parser
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiubracketParser :: AParser st a -> AParser st Token -> AParser st Token
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -> AParser st Token -> ([a] -> Range -> b) -> AParser st b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiubracketParser parser op cl sep k = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (ts, ps) <- option ([], []) $ separatedBy parser sep
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ k ts $ toPos o ps c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parser for square brackets
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkBrackets p c = bracketParser p oBracketT cBracketT anComma c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parser for braces
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkBraces p c = bracketParser p oBraceT cBraceT anComma c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a simple class name or the type universe as kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseClassId :: AParser st Kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseClassId = fmap ClassKind classId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | do 'parseClassId' or a kind in parenthessis
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseSimpleKind :: AParser st Kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseSimpleKind = parseClassId <|> (oParenT >> kind << cParenT)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | do 'parseSimpleKind' and check for an optional 'Variance'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseExtKind :: AParser st (Variance, Kind)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseExtKind = bind (,) variance parseSimpleKind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a (right associative) function kind for a given argument kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuarrowKind :: (Variance, Kind) -> AParser st Kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuarrowKind (v, k) = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu a <- asKey funS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ FunKind v k k2 $ tokPos a
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a function kind but reject an extended kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiukind :: AParser st Kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu k1@(v, k) <- parseExtKind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu arrowKind k1 <|> case v of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu InVar -> return k
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu _ -> unexpected "variance of kind"
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a function kind but accept an extended kind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuextKind :: AParser st (Variance, Kind)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu k1 <- parseExtKind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do k <- arrowKind k1
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return (InVar, k)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * type variables
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuvariance :: AParser st Variance
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuvariance = let l = [CoVar, ContraVar] in
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu choice (map ( \ v -> asKey (show v) >> return v) l) <|> return InVar
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- a (simple) type variable with a 'Variance'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuextVar :: AParser st Id -> AParser st (Id, Variance)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuextVar vp = bind (,) vp variance
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- several 'extVar' with a 'Kind'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeVars :: AParser st [TypeArg]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (ts, ps) <- extVar typeVar `separatedBy` anComma
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuallIsInVar :: [(Id, Variance)] -> Bool
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuallIsInVar = all ( \ (_, v) -> case v of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- 'parseType' a 'Downset' starting with 'lessT'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeKind :: [(Id, Variance)] -> [Token]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -> AParser st [TypeArg]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeKind vs ps = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu if allIsInVar vs then do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (v, k) <- extKind
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ makeTypeArgs vs ps v (VarKind k) $ tokPos c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ makeTypeArgs vs ps InVar (VarKind k) $ tokPos c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ makeTypeArgs vs ps InVar (Downset t) $ tokPos l
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> return (makeTypeArgs vs ps InVar MissingKind nullRange)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | add the 'Kind' to all 'extVar' and yield a 'TypeArg'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumakeTypeArgs :: [(Id, Variance)] -> [Token]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -> Variance -> VarKind -> Range -> [TypeArg]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumakeTypeArgs ts ps vv vk qs =
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu zipWith (mergeVariance Comma vv vk) (init ts)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (map tokPos ps)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu ++ [mergeVariance Other vv vk (last ts) qs]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu mergeVariance c v k (t, InVar) q = TypeArg t v k rStar 0 c q
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu mergeVariance c _ k (t, v) q = TypeArg t v k rStar 0 c q
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a single 'TypeArg' (parsed by 'typeVars')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiusingleTypeArg :: AParser st TypeArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiusingleTypeArg = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu [a] -> return a
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu _ -> unexpected "list of type arguments"
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'singleTypeArg' put in parentheses
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparenTypeArg :: AParser st (TypeArg, [Token])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparenTypeArg = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu a <- singleTypeArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return (a, [o, p])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'singleTypeArg' possibly put in parentheses
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeArg :: AParser st (TypeArg, [Token])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu a <- singleTypeArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> parenTypeArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'singleTypeArg' put in parentheses as 'TypePattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternArg :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternArg = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (a, ps) <- parenTypeArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ TypePatternArg a $ catPos ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * parse special identifier tokens
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiutype TokenMode = [String]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a 'Token' of an 'Id' (to be declared)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- but exclude the signs in 'TokenMode'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuaToken :: TokenMode -> AParser st Token
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuaToken b = pToken $ scanQuotedChar <|> scanDigit <|> scanHCWords <|> placeS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> reserved b scanHCSigns
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | just 'aToken' only excluding basic HasCASL keywords
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuidToken :: AParser st Token
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuidToken = aToken [] <|> pToken scanDotWords
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * type patterns
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- 'TypePatternToken's within 'BracketTypePattern's
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- may recusively be 'idToken's.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- Parenthesis are only legal for a 'typePatternArg'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypePatternOrId :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypePatternOrId = fmap TypePatternToken idToken
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces typePatternOrId (BracketTypePattern Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets typePatternOrId (BracketTypePattern Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> typePatternArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixTypePattern :: AParser st TypePattern -> AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixTypePattern p = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ case ts of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu _ -> MixfixTypePattern ts
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternOrId :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternOrId = mixTypePattern primTypePatternOrId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | those (top-level) 'Token's (less than 'idToken')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- that may appear in 'TypePattern's as 'TypePatternToken'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternToken :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePatternToken = fmap TypePatternToken $ pToken $ scanHCWords <|> placeS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> reserved [assignS, lessS, equalS] scanHCSigns
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'typePatternToken' or something in braces (a 'typePattern'),
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- in square brackets (a 'typePatternOrId' covering compound lists)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- or parenthesis ('typePatternArg')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypePattern :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypePattern = typePatternToken
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets typePatternOrId (BracketTypePattern Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces typePattern (BracketTypePattern Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> typePatternArg
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- several 'primTypePatter's possibly yielding a 'MixfixTypePattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePattern :: AParser st TypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypePattern = mixTypePattern primTypePattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- a parsed type may also be interpreted as a kind (by the mixfix analysis)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | type tokens with some symbols removed
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeToken :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeToken = fmap TypeToken $ pToken $ scanHCWords <|> placeS <|>
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu reserved (assignS : lessS : equalS : barS : hascasl_type_ops) scanHCSigns
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'TypeToken's within 'BracketType's may recusively be
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- 'idToken's. Parenthesis may group a mixfix type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- or may be interpreted as a kind later on in a GEN-VAR-DECL.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypeOrId :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTypeOrId = fmap TypeToken idToken
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets typeOrId (BracketType Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces typeOrId (BracketType Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bracketParser typeOrId oParenT cParenT anComma (BracketType Parens)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkMixfixType :: AParser st Type -> AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkMixfixType p = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ case ts of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu _ -> MixfixType ts
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkKindedMixType :: AParser st Type -> AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkKindedMixType p = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- mkMixfixType p
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu kindAnno t <|> return t
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | several 'primTypeOrId's possibly yielding a 'MixfixType'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- and possibly followed by a 'kindAnno'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeOrId :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeOrId = mkKindedMixType primTypeOrId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'Kind' annotation starting with 'colT'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiukindAnno :: Type -> AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ KindedType t (Set.singleton k) $ tokPos c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a typeToken' or a 'BracketType'. Square brackets may contain 'typeOrId'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimType :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimType = typeToken
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets typeOrId (BracketType Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces parseType (BracketType Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bracketParser parseType oParenT cParenT anComma (BracketType Parens)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'primType' possibly preceded by 'quMarkT'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulazyType :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulazyType = fmap mkLazyType (quMarkT >> mkMixfixType primType) <|> primType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | several 'lazyType's (as 'MixfixType') possibly followed by 'kindAnno'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixType :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixType = mkKindedMixType lazyType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'mixType' possibly interspersed with 'crossT'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprodType :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (ts, ps) <- mixType `separatedBy` crossT
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ mkProductTypeWithRange ts $ catPos ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a (right associativ) function type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparseType :: AParser st Type
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do a <- arrowT <?> funS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t2 <- parseType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ mkTypeAppl
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (TypeName a (toRaw $ funKindWithRange $ posOfId a) 0) [t1, t2]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse one of the four possible 'Arrow's
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuarrowT :: AParser st Id
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuarrowT = let l = [FunArr, PFunArr, ContFunArr, PContFunArr] in
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu choice $ map ( \ a -> do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- asKey $ show a
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ mkId [placeTok, t, placeTok]) l
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | parse a 'TypeScheme' using 'forallT', 'typeVars', 'dotT' and 'parseType'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeScheme :: PolyId -> AParser st TypeScheme
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeScheme (PolyId _ tys ps) = if null tys then do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (ts, cs) <- typeVars `separatedBy` anSemi
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ TypeScheme (concat ts) t $ toPos f cs d
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> fmap simpleTypeScheme parseType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ TypeScheme tys t ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- * varDecls and genVarDecls
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | comma separated 'var' with 'varDeclType'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuvarDecls :: AParser st [VarDecl]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (vs, ps) <- var `separatedBy` anComma
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu varDeclType vs ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a type ('parseType') following a colon
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuvarDeclType :: [Id] -> [Token] -> AParser st [VarDecl]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuvarDeclType vs ps = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ makeVarDecls vs ps t $ tokPos c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | attach the 'Type' to every 'Var'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumakeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumakeVarDecls vs ps t q = zipWith ( \ v p -> VarDecl v t Comma $ tokPos p)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (init vs) ps ++ [VarDecl (last vs) t Other q]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | either like 'varDecls' or declared type variables.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- A 'GenVarDecl' may later become a 'GenTypeVarDecl'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiugenVarDecls:: AParser st [GenVarDecl]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiugenVarDecls = fmap (map ( \ g -> case g of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu GenTypeVarDecl (TypeArg i v MissingKind _ n s ps) ->
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu GenTypeVarDecl (TypeArg i v (VarKind universe)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (vs, ps) <- extVar var `separatedBy` anComma
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu let other = fmap (map GenTypeVarDecl) (typeKind vs ps)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu if allIsInVar vs then fmap (map GenVarDecl)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (varDeclType (map ( \ (i, _) -> i) vs) ps) <|> other
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu{- | different legal 'TermToken's possibly excluding 'funS' or
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu'equalS' for case or let patterns resp. -}
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutokenPattern :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutokenPattern b = fmap TermToken (aToken b <|> pToken (string "_"))
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- a single underscore serves as wildcard pattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'tokenPattern' or 'BracketTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimPattern :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimPattern b = tokenPattern b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets pattern (BracketTerm Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces pattern (BracketTerm Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bracketParser (pattern <|> varTerm <|> qualOpName)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu oParenT cParenT anComma (BracketTerm Parens)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkMixfixTerm :: [Term] -> Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumkMixfixTerm ts = case ts of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu _ -> MixfixTerm ts
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | several 'typedPattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixPattern :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixPattern = fmap mkMixfixTerm . many1 . asPattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a possibly typed ('parseType') pattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypedPattern :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypedPattern b = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- primPattern b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu ty <- parseType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ MixfixTerm [t, MixTypeTerm OfType ty $ tokPos c]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | top-level pattern (possibly 'AsPattern')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuasPattern :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuasPattern b = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu v <- typedPattern b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu TermToken tt -> if isPlace tt then return v else do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- typedPattern b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ AsPattern (VarDecl (mkId [tt]) (MixfixType [])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu Other $ tokPos c) t $ tokPos c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | an unrestricted 'asPattern'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiupattern :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiupattern = mixPattern []
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumyChoice :: [(AParser st Token, a)] -> AParser st (a, Token)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumyChoice = choice . map ( \ (p, a) -> do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'Total' or 'Partial' lambda dot
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulamDot :: AParser st (Partiality, Token)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulamDot = myChoice [ (choice $ map (asKey . (++ exMark)) [dotS, cDot], Total)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu , (dotT, Partial)]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | patterns between 'lamS' and 'lamDot'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulamPattern :: AParser st [Term]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (lookAhead lamDot >> return []) <|> bind (:) (typedPattern []) lamPattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu{- | 'Token's that may occur in 'Term's including literals
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu 'scanFloat', 'scanString' but excluding 'ifS', 'whenS' and 'elseS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu to allow a quantifier after 'whenS'. In case-terms also 'barS' will
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu be excluded on the top-level. -}
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutToken :: TokenMode -> AParser st Token
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutToken b = pToken (scanFloat
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> scanQuotedChar <|> scanDotWords
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> reserved [ifS, whenS, elseS] scanHCWords
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> reserved b scanHCSigns
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> placeS <?> "id/literal")
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'tToken' as 'Term' plus 'exEqual' and 'equalS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutermToken :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutermToken b = fmap TermToken (asKey exEqual <|> asKey equalS <|> tToken b)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'termToken' plus 'BracketTerm's
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTerm :: TokenMode -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuprimTerm b = termToken b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBraces term (BracketTerm Braces)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> mkBrackets term (BracketTerm Squares)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bracketParser termInParens oParenT cParenT anComma (BracketTerm Parens)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | how the keyword 'inS' should be treated
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiudata InMode = NoIn -- ^ next 'inS' belongs to 'letS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu | WithIn -- ^ 'inS' is the element test
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | all 'Term's that start with a unique keyword
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiubaseTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiubaseTerm b = ifTerm b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> forallTerm b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> lambdaTerm b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'whenS' possibly followed by an 'elseS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuwhenTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu i <- asKey whenS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu let l1 = [TermToken i, c]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do t <- asKey elseS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ MixfixTerm $ l1 ++ [TermToken t, e]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> return (MixfixTerm l1)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'ifS' possibly followed by 'thenS' and 'elseS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- yielding a 'MixfixTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuifTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu let l1 = [TermToken i, c]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do t <- asKey thenS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu let l2 = l1 ++ [TermToken t, e]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do s <- asKey elseS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ MixfixTerm $ l2 ++ [TermToken s, f]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> return (MixfixTerm l2)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> return (MixfixTerm l1)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | unrestricted terms including qualified names
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutermInParens :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutermInParens = term <|> varTerm <|> qualOpName <|> qualPredName
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a qualified 'var'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuvarTerm :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu v <- asKey varS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ QualVar $ VarDecl i t Other $ toPos v [] c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'opS' or 'functS'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuopBrand :: AParser st (Token, OpBrand)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuopBrand = bind (,) (asKey opS) (return Op)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bind (,) (asKey functS) (return Fun)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparsePolyId :: AParser st PolyId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuparsePolyId = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu l <- try ite <|> start hcKeys
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu if isPlace (last l)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu then return $ PolyId (Id l [] nullRange) [] nullRange else do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (cs, ps) <- option ([], nullRange) (try $ comps hcKeys)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (tys, qs) <- option ([], nullRange) $
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu bracketParser typeVars oBracketT cBracketT semiT (,)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu u <- many placeT
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ PolyId (Id (l ++ u) cs ps) (concat tys) qs
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a qualified operation (with 'opBrand')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuqualOpName :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (v, b) <- opBrand
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu i <- parsePolyId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- typeScheme i
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ QualOp b i t [] Infer $ toPos v [] c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a qualified predicate
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuqualPredName :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuqualPredName = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu v <- asKey predS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu i <- parsePolyId
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- typeScheme i
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu let p = toPos v [] c
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ QualOp Pred i (predTypeScheme p t) [] Infer p
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a qualifier expecting a further 'Type'.
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- 'inS' is rejected for 'NoIn'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeQual :: InMode -> AParser st (TypeQual, Token)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypeQual m = myChoice $ (colT, OfType) : (asT, AsType) : case m of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu WithIn -> [(asKey inS, InType)]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a possibly type qualified ('typeQual') 'primTerm' or a 'baseTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypedTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiutypedTerm (i, b) = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- primTerm b
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do (q, p) <- typeQual i
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu ty <- parseType
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ MixfixTerm [t, MixTypeTerm q ty $ tokPos p]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> baseTerm (i, b)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | several 'typedTerm's yielding a 'MixfixTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiumixTerm = fmap mkMixfixTerm . many1 . typedTerm
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | keywords that start a new item
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuhasCaslStartKeywords :: [String]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuhasCaslStartKeywords =
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu dotS : cDot : (hascasl_reserved_words \\ [existsS, letS, caseS])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'mixTerm' followed by 'whereS' and equations separated by 'optSemi'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuwhereTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuwhereTerm b = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu do p <- asKey whereS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (es, ps, _ans) <- itemAux hasCaslStartKeywords $
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu patternTermPair [equalS] b equalS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -- ignore collected annotations
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ LetTerm Where es t $ catPos $ p : ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'whereTerm' called with ('WithIn', [])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuterm :: AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiuterm = whereTerm (WithIn, [])
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'Universal' 'QuantifiedTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuforallTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuforallTerm b = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (vs, ps) <- genVarDecls `separatedBy` anSemi
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ QuantifiedTerm Universal (concat vs) t $ toPos f ps d
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | 'Unique' or 'Existential'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuexQuant :: AParser st (Token, Quantifier)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuexQuant = bind (,) (asKey (existsS++exMark)) (return Unique)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu <|> bind (,) (asKey existsS) (return Existential)
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a (possibly unique) existential 'QuantifiedTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuexTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (p, q) <- exQuant <?> existsS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (vs, ps) <- varDecls `separatedBy` anSemi
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ QuantifiedTerm q (map GenVarDecl (concat vs)) f $ toPos p ps d
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulamDecls :: AParser st [Term]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulamDecls = try ((do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (vs, _) <- separatedBy varDecls anSemi
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu lookAhead lamDot
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ case concat vs of
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu [(VarDecl (Id [t] [] _) ty _ ps)] ->
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -- this may be a constant constructor
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu [MixfixTerm [TermToken t, MixTypeTerm OfType ty ps]]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu vss -> map QualVar vss) <?> "VAR-DECL") <|> lamPattern
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'LambdaTerm'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulambdaTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiulambdaTerm b = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu l <- asKey lamS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (k, d) <- lamDot
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ LambdaTerm (if null pl then [BracketTerm Parens [] nullRange]
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu else pl) k t $ toPos l [] d
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'CaseTerm' with 'funS' excluded in 'patternTermPair'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiucaseTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiucaseTerm (i, _) = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu c <- asKey caseS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (ts, ps) <- patternTermPair [funS] (i, [barS]) funS `separatedBy` barT
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ CaseTerm t ts $ catPos $ c : o : ps
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a 'LetTerm' with 'equalS' excluded in 'patternTermPair'
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- (called with 'NoIn')
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiuletTerm :: (InMode, TokenMode) -> AParser st Term
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu l <- asKey letS
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu (es, ps) <- patternTermPair [equalS] (NoIn, []) equalS `separatedBy` anSemi
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ LetTerm Let es t $ toPos l ps i
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu-- | a customizable pattern equation
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiupatternTermPair :: TokenMode -> (InMode, TokenMode) -> String
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu -> AParser st ProgEq
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae BungiupatternTermPair b1 b2 sep = do
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu p <- mixPattern b1
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu t <- mixTerm b2
d8cee46da48576e19b83a24f68c13e95f49d286cFrancisc Nicolae Bungiu return $ ProgEq p t $ tokPos s