4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederDescription : parser for HasCASL kinds, types, terms, patterns and equations

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2005

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : Christian.Maeder@dfki.de

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederparser for HasCASL kinds, types, terms, patterns and equations

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maedermodule HasCASL.ParseTerm where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maederimport Common.AnnoState

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maederimport Common.Id

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Keywords

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Lexer

4954b30d3c209d7dee4e43016cee8189daf646e8Christian Maederimport Common.Token

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maederimport HasCASL.HToken

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport HasCASL.As

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport HasCASL.AsUtils

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Text.ParserCombinators.Parsec

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Data.List ((\\))

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-- * key sign tokens

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | a colon not followed by a question mark

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedercolT :: AParser st Token

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaedercolT = asKey colonS

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- * parser for bracketed lists

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder-- | a generic bracket parser

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederbracketParser :: AParser st a -> AParser st Token -> AParser st Token

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder -> AParser st Token -> ([a] -> Range -> b) -> AParser st b

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaederbracketParser parser op cl sep k = do

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder o <- op

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder (ts, ps) <- option ([], []) $ separatedBy parser sep

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder c <- cl

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder return $ k ts $ toPos o ps c

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder-- | parser for square brackets

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian MaedermkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian MaedermkBrackets p c = bracketParser p oBracketT cBracketT anComma c

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder-- | parser for braces

0f894093b1d435fd222074706d7fdadb9725cfdfChristian MaedermkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b

df638d53c2d5fe5e80b943a58609c8936848ed82Christian MaedermkBraces p c = bracketParser p oBraceT cBraceT anComma c

51281dddda866c0cda9fca22bf6bc4eea7128112Christian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder-- * kinds

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

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

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaederparseClassId :: AParser st Kind

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaederparseClassId = fmap ClassKind classId

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder-- | do 'parseClassId' or a kind in parenthessis

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederparseSimpleKind :: AParser st Kind

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederparseSimpleKind = parseClassId <|> (oParenT >> kind << cParenT)

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- | do 'parseSimpleKind' and check for an optional 'Variance'

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederparseExtKind :: AParser st (Variance, Kind)

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian MaederparseExtKind = bind (,) variance parseSimpleKind

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | parse a (right associative) function kind for a given argument kind

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian MaederarrowKind :: (Variance, Kind) -> AParser st Kind

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian MaederarrowKind (v, k) = do

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder a <- asKey funS

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder k2 <- kind

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder return $ FunKind v k k2 $ tokPos a

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder-- | parse a function kind but reject an extended kind

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederkind :: AParser st Kind

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederkind = do

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder k1@(v, k) <- parseExtKind

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder arrowKind k1 <|> case v of

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder InVar -> return k

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder _ -> unexpected "variance of kind"

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder-- | parse a function kind but accept an extended kind

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederextKind :: AParser st (Variance, Kind)

628310b42327ad76ce471caf0dde6563d6fa6307Christian MaederextKind = do

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder k1 <- parseExtKind

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder do k <- arrowKind k1

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder return (InVar, k)

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder <|> return k1

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- * type variables

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maedervariance :: AParser st Variance

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maedervariance = let l = [CoVar, ContraVar] in

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder choice (map ( \ v -> asKey (show v) >> return v) l) <|> return InVar

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder-- a (simple) type variable with a 'Variance'

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian MaederextVar :: AParser st Id -> AParser st (Id, Variance)

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederextVar vp = bind (,) vp variance

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- several 'extVar' with a 'Kind'

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaedertypeVars :: AParser st [TypeArg]

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian MaedertypeVars = do

ac07a6558423dae7adc488ed9092cd8e9450a29dChristian Maeder (ts, ps) <- extVar typeVar `separatedBy` anComma

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder typeKind ts ps

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederallIsInVar :: [(Id, Variance)] -> Bool

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian MaederallIsInVar = all ( \ (_, v) -> case v of

b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder InVar -> True

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder _ -> False)

b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- 'parseType' a 'Downset' starting with 'lessT'

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian MaedertypeKind :: [(Id, Variance)] -> [Token]

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder -> AParser st [TypeArg]

53301de22afd7190981b363b57c48df86fcb50f7Christian MaedertypeKind vs ps = do

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder c <- colT

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if allIsInVar vs then do

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (v, k) <- extKind

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder return $ makeTypeArgs vs ps v (VarKind k) $ tokPos c

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else do

k <- kind

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

<|> do

l <- lessT

t <- parseType

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

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

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

makeTypeArgs :: [(Id, Variance)] -> [Token]

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

makeTypeArgs ts ps vv vk qs =

zipWith (mergeVariance Comma vv vk) (init ts)

(map tokPos ps)

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

where

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

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

-- | a single 'TypeArg' (parsed by 'typeVars')

singleTypeArg :: AParser st TypeArg

singleTypeArg = do

as <- typeVars

case as of

[a] -> return a

_ -> unexpected "list of type arguments"

-- | a 'singleTypeArg' put in parentheses

parenTypeArg :: AParser st (TypeArg, [Token])

parenTypeArg = do

o <- oParenT

a <- singleTypeArg

p <- cParenT

return (a, [o, p])

-- | a 'singleTypeArg' possibly put in parentheses

typeArg :: AParser st (TypeArg, [Token])

typeArg = do

a <- singleTypeArg

return (a, [])

<|> parenTypeArg

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

typePatternArg :: 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

return $ case ts of

[hd] -> hd

_ -> MixfixType ts

mkKindedMixType :: AParser st Type -> AParser st Type

mkKindedMixType p = do

t <- mkMixfixType p

kindAnno t <|> return t

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

-- and possibly followed by a 'kindAnno'.

typeOrId :: AParser st Type

typeOrId = mkKindedMixType 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 >> mkMixfixType primType) <|> primType

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

mixType :: AParser st Type

mixType = mkKindedMixType 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

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

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

-- a single underscore serves as wildcard pattern

-- | 'tokenPattern' or 'BracketTerm'

primPattern :: TokenMode -> AParser st Term

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 Term

mixPattern = fmap mkMixfixTerm . many1 . asPattern

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

typedPattern :: TokenMode -> AParser st Term

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 Term

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 Term

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 [Term]

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)

parsePolyId :: AParser st PolyId

parsePolyId = do

l <- try ite <|> start hcKeys

if isPlace (last l)

then return $ PolyId (Id l [] nullRange) [] nullRange else do

(cs, ps) <- option ([], nullRange) (try $ comps hcKeys)

(tys, qs) <- option ([], nullRange) $

bracketParser typeVars oBracketT cBracketT semiT (,)

u <- many placeT

return $ PolyId (Id (l ++ u) cs ps) (concat tys) qs

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

qualOpName :: AParser st Term

qualOpName = do

(v, b) <- opBrand

i <- parsePolyId

c <- colonST

t <- typeScheme

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

-- | a qualified predicate

qualPredName :: AParser st Term

qualPredName = do

v <- asKey predS

i <- parsePolyId

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

lamDecls :: AParser st [Term]

lamDecls = try ((do

(vs, _) <- separatedBy varDecls anSemi

lookAhead lamDot

return $ map QualVar $ concat vs) <?> "VAR-DECL") <|> lamPattern

-- | a 'LambdaTerm'

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

lambdaTerm b = do

l <- asKey lamS

pl <- lamDecls

(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