66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder

81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- HetCATS/HasCASL/ParseTerm.hs

81d182b21020b815887e9057959228546cf61b6bChristian Maeder $Id$

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder Authors: Christian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder Year: 2002

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder parser for HasCASL kind, types, terms and pattern/equations

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder-}

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedermodule ParseTerm where

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Id

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Keywords

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport Lexer

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Token

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HToken

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport As

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Parsec

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport AS_Annotation

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Anno_Parser(annotationL)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaedernoQuMark :: String -> GenParser Char st Token

ad270004874ce1d0697fb30d7309f180553bb315Christian MaedernoQuMark s = try $ asKey s << notFollowedBy (char '?')

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian MaedercolT, plusT, minusT, qColonT :: GenParser Char st Token

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercolT = noQuMark colonS

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederplusT = asKey plusS

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederminusT = asKey minusS

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederqColonT = asKey (colonS++quMark)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederquColon :: GenParser Char st (Partiality, Token)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederquColon = do c <- colT

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder return (Total, c)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|>

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder do c <- qColonT

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return (Partial, c)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-----------------------------------------------------------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- kind

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- universe is just a special className ("Type")

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederparseClass :: GenParser Char st Class

27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaederparseClass = fmap ClassName className

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder <|>

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do o <- oParenT

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder (cs, ps) <- parseClass `separatedBy` commaT

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder c <- cParenT

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return (Intersection cs (toPos o ps c))

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederextClass :: GenParser Char st ExtClass

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederextClass = do c <- parseClass

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do s <- plusT

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder return (ExtClass c CoVar (tokPos s))

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|>

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder do s <- minusT

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return (ExtClass c ContraVar (tokPos s))

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|> return (ExtClass c InVar nullPos)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprodClass :: GenParser Char st ProdClass

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederprodClass = do (cs, ps) <- extClass `separatedBy` crossT

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (ProdClass cs (map tokPos ps))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederkind :: GenParser Char st Kind

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederkind = kindOrClass [] []

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederkindOrClass, curriedKind :: [ProdClass] -> [Token] -> GenParser Char st Kind

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederkindOrClass os ps = do c@(ProdClass cs _) <- prodClass

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if let isClass (ExtClass _ InVar _) = True

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder isClass _ = False

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in length cs == 1 && isClass (head cs)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then curriedKind (os++[c]) ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|> return (Kind os ( (\ (ExtClass e _ _)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> e) (head cs))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (map tokPos ps))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else curriedKind (os++[c]) ps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian MaedercurriedKind os ps = do a <- asKey funS

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder kindOrClass os (ps++[a])

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder-----------------------------------------------------------------------------

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder-- type

07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder-----------------------------------------------------------------------------

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

bbcc77a6eb9554dd3092cabafae1e5ca74a054eeChristian MaedertypeToken :: GenParser Char st Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertypeToken = fmap TypeToken (pToken (scanWords <|> placeS <|>

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder reserved (hascasl_type_ops ++

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder formula_ops ++

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder hascasl_reserved_ops)

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder scanAnySigns))

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maederbraces :: GenParser Char st a -> ([a] -> [Pos] -> b)

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder -> GenParser Char st b

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maederbraces p c = bracketParser p oBraceT cBraceT commaT c

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-- [...] may contain types or ids

6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaederidToken :: Bool -> GenParser Char st Token

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederidToken b = pToken (scanQuotedChar <|> scanDotWords

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|> scanDigit <|> scanWords <|> placeS <|>

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder reserved ((if b then formula_ops else funS:formula_ops)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ++ hascasl_reserved_ops)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder scanAnySigns)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprimTypeOrId, typeOrId :: GenParser Char st Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederprimTypeOrId = fmap TypeToken (idToken True)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|> braces typeOrId (BracketType Braces)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|> brackets typeOrId (BracketType Squares)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder <|> bracketParser typeOrId oParenT cParenT commaT

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (BracketType Parens)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder

6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedertypeOrId = do ts <- many1 primTypeOrId

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder let t = if length ts == 1 then head ts

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder else MixfixType ts

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder in

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder kindAnno t

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder <|>

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return(t)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederkindAnno :: Type -> GenParser Char st Type

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederkindAnno t = do c <- colT

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder k <- kind

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return (KindedType t k (tokPos c))

2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder

2ca4cb7c4970015237ff434081c2c5bc74284cadChristian MaederprimType, lazyType, mixType, prodType, funType :: GenParser Char st Type

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederprimType = typeToken

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|> bracketParser parseType oParenT cParenT commaT

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (BracketType Parens)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|> braces parseType (BracketType Braces)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|> brackets typeOrId (BracketType Squares)

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederlazyType = do q <- quMarkT

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder t <- primType

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return (LazyType t (tokPos q))

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder <|> primType

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaedermixType = do ts <- many1 lazyType

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder let t = if length ts == 1 then head ts else MixfixType ts

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder in kindAnno t

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder <|> return t

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaederprodType = do (ts, ps) <- mixType `separatedBy` crossT

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder return (if length ts == 1 then head ts

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder else ProductType ts (map tokPos ps))

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederfunType = do (ts, as) <- prodType `separatedBy` arrowT

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (makeFun ts as)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder where makeFun [t] [] = t

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder makeFun [t,r] [a] = FunType t (fst a) r [snd a]

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder makeFun (t:r) (a:b) = makeFun [t, makeFun r b] [a]

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder makeFun _ _ = error "makeFun got illegal argument"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

61091743da1a9ed6dfd5e077fdcc972553358962Christian MaederarrowT :: GenParser Char st (Arrow, Pos)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederarrowT = do a <- noQuMark funS

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder return (FunArr, tokPos a)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|>

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder do a <- asKey pFun

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (PFunArr, tokPos a)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|>

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder do a <- noQuMark contFun

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (ContFunArr, tokPos a)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder <|>

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do a <- asKey pContFun

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder return (PContFunArr, tokPos a)

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaederparseType :: GenParser Char st Type

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaederparseType = funType

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder-----------------------------------------------------------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- var decls, typevar decls, genVarDecls

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-----------------------------------------------------------------------------

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

405b95208385572f491e1e0207d8d14e31022fa6Christian MaedervarDecls :: GenParser Char st [VarDecl]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarDecls = do (vs, ps) <- var `separatedBy` commaT

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder varDeclType vs ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarDeclType :: [Var] -> [Token] -> GenParser Char st [VarDecl]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarDeclType vs ps = do c <- colT

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t <- parseType

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (makeVarDecls vs ps t (tokPos c))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermakeVarDecls :: [Var] -> [Token] -> Type -> Pos -> [VarDecl]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermakeVarDecls vs ps t q = zipWith (\ v p -> VarDecl v t Comma (tokPos p))

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarDeclDownSet :: [TypeVar] -> [Token] -> GenParser Char st [TypeVarDecl]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedervarDeclDownSet vs ps =

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder do l <- lessT

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder t <- parseType

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder return (makeTypeVarDecls vs ps (Downset t) (tokPos l))

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertypeVarDecls :: GenParser Char st [TypeVarDecl]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertypeVarDecls = do (vs, ps) <- typeVar `separatedBy` commaT

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do c <- colT

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t <- parseClass

341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder return (makeTypeVarDecls vs ps t (tokPos c))

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder <|> varDeclDownSet vs ps

6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder <|> return (makeTypeVarDecls vs ps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Universe nullPos) nullPos)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermakeTypeVarDecls :: [TypeVar] -> [Token] -> Class -> Pos -> [TypeVarDecl]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermakeTypeVarDecls vs ps cl q = zipWith (\ v p ->

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder TypeVarDecl v cl Comma (tokPos p))

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (init vs) ps

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder ++ [TypeVarDecl (last vs) cl Other q]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergenVarDecls:: GenParser Char st [GenVarDecl]

59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedergenVarDecls = do (vs, ps) <- var `separatedBy` commaT

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder if all isSimpleId vs then

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder fmap (map GenVarDecl) (varDeclType vs ps)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder <|> fmap (map GenTypeVarDecl)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (varDeclDownSet (map (\ (Id ts _ _)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -> head ts) vs) ps)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder else

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder fmap (map GenVarDecl) (varDeclType vs ps)

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder where isSimpleId (Id ts _ _) = null (tail ts) && head (tokStr (head ts))

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder `elem` caslLetters

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder

-----------------------------------------------------------------------------

-- typeArgs

-----------------------------------------------------------------------------

extTypeVar :: GenParser Char st (TypeVar, Variance, Pos)

extTypeVar = do t <- typeVar

do a <- plusT

return (t, CoVar, tokPos a)

<|>

do a <- plusT

return (t, ContraVar, tokPos a)

<|> return (t, InVar, nullPos)

typeArgs :: GenParser Char st [TypeArg]

typeArgs = do (ts, ps) <- extTypeVar `separatedBy` commaT

do c <- colT

if let isInVar(_, InVar, _) = True

isInVar(_,_,_) = False

in all isInVar ts then

do k <- extClass

return (makeTypeArgs ts ps (tokPos c) k)

else do k <- parseClass

return (makeTypeArgs ts ps (tokPos c)

(ExtClass k InVar nullPos))

<|>

do l <- lessT

t <- parseType

return (makeTypeArgs ts ps (tokPos l)

(ExtClass (Downset t) InVar nullPos))

<|> return (makeTypeArgs ts ps nullPos

(ExtClass (Universe nullPos) InVar nullPos))

where mergeVariance k e (t, InVar, _) p =

TypeArg t e k p

mergeVariance k (ExtClass c _ _) (t, v, ps) p =

TypeArg t (ExtClass c v ps) k p

makeTypeArgs ts ps q e =

zipWith (mergeVariance Comma e) (init ts)

(map tokPos ps)

++ [mergeVariance Other e (last ts) q]

-----------------------------------------------------------------------------

-- type pattern

-----------------------------------------------------------------------------

typePatternToken, primTypePatternOrId, typePatternOrId

:: GenParser Char st TypePattern

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

reserved (hascasl_type_ops ++

formula_ops ++

hascasl_reserved_ops)

scanAnySigns))

primTypePatternOrId = fmap TypePatternToken (idToken True)

<|> braces typePatternOrId (BracketTypePattern Braces)

<|> brackets typePatternOrId (BracketTypePattern Squares)

<|> bracketParser typePatternArgs oParenT cParenT semiT

(BracketTypePattern Parens)

typePatternOrId = do ts <- many1 primTypePatternOrId

return( if length ts == 1 then head ts

else MixfixTypePattern ts)

typePatternArgs, primTypePattern, typePattern :: GenParser Char st TypePattern

typePatternArgs = fmap TypePatternArgs typeArgs

primTypePattern = typePatternToken

<|> bracketParser typePatternArgs oParenT cParenT semiT

(BracketTypePattern Parens)

<|> braces typePattern (BracketTypePattern Braces)

<|> brackets typePatternOrId (BracketTypePattern Squares)

typePattern = do ts <- many1 primTypePattern

let t = if length ts == 1 then head ts

else MixfixTypePattern ts

in return t

-----------------------------------------------------------------------------

-- pattern

-----------------------------------------------------------------------------

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

-- thus [ ... ] may be a mixfix-pattern, a compound list,

-- or an instantiation with types

-- special pattern needed that don't contain "->" at the top-level

-- because "->" should be recognized in case-expressions

-- flag b allows "->" in patterns

tokenPattern :: Bool -> GenParser Char st Pattern

tokenPattern b = fmap PatternToken (idToken b)

primPattern :: Bool -> GenParser Char st Pattern

primPattern b = tokenPattern b

<|> braces pattern (BracketPattern Braces)

<|> brackets pattern (BracketPattern Squares)

<|> bracketParser patterns oParenT cParenT semiT

(BracketPattern Parens)

patterns :: GenParser Char st Pattern

patterns = do (ts, ps) <- pattern `separatedBy` commaT

let tp = if length ts == 1 then head ts

else TuplePattern ts (map tokPos ps)

in return tp

mixPattern :: Bool -> GenParser Char st Pattern

mixPattern b =

do l <- many1 $ primPattern b

let p = if length l == 1 then head l else MixfixPattern l

in typedPattern p <|> return p

typedPattern :: Pattern -> GenParser Char st Pattern

typedPattern p = do { c <- colT

; t <- parseType

; return (TypedPattern p t [tokPos c])

}

asPattern :: Bool -> GenParser Char st Pattern

asPattern b =

do v <- mixPattern b

do c <- asT

t <- mixPattern b

return (AsPattern v t [tokPos c])

<|> return v

-- True allows "->" in patterns

pattern :: GenParser Char st Pattern

pattern = asPattern True

-----------------------------------------------------------------------------

-- instOpName

-----------------------------------------------------------------------------

-- places may follow instantiation lists

instOpName :: GenParser Char st InstOpName

instOpName = do i@(Id is cs ps) <- uninstOpName

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

else do l <- many (brackets parseType Types)

u <- many placeT

return (InstOpName (Id (is++u) cs ps) l)

-----------------------------------------------------------------------------

-- typeScheme

-----------------------------------------------------------------------------

typeScheme :: GenParser Char st TypeScheme

typeScheme = do f <- forallT

(ts, cs) <- typeVarDecls `separatedBy` semiT

d <- dotT

t <- typeScheme

return (TypeScheme (concat ts) t (toPos f cs d))

<|> fmap SimpleTypeScheme parseType

-----------------------------------------------------------------------------

-- term

-----------------------------------------------------------------------------

tToken :: GenParser Char st Token

tToken = pToken(scanFloat <|> scanString

<|> scanQuotedChar <|> scanDotWords <|> scanTermWords

<|> reserved hascasl_reserved_ops scanAnySigns

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

termToken :: GenParser Char st Term

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

-- flag if within brackets: True allows "in"-Terms

primTerm :: Bool -> GenParser Char st Term

primTerm b = termToken

<|> braces term (BracketTerm Braces)

<|> brackets term (BracketTerm Squares)

<|> parenTerm

<|> forallTerm b

<|> exTerm b

<|> lambdaTerm b

<|> caseTerm b

<|> letTerm b

parenTerm :: GenParser Char st Term

parenTerm = do o <- oParenT

varTerm o

<|>

qualOpName o

<|>

qualPredName o

<|>

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

p <- cParenT

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

partialTypeScheme :: GenParser Char st (Token, TypeScheme)

partialTypeScheme = do q <- qColonT

t <- parseType

return (q, SimpleTypeScheme

(FunType (TupleType [] [tokPos q])

PFunArr t [tokPos q]))

<|> bind (,) colT typeScheme

varTerm :: Token -> GenParser Char st Term

varTerm o = do v <- asKey varS

i <- var

c <- colT

t <- parseType

p <- cParenT

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

qualOpName :: Token -> GenParser Char st Term

qualOpName o = do { v <- asKey opS

; i <- instOpName

; (c, t) <- partialTypeScheme

; p <- cParenT

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

}

predTypeScheme :: TypeScheme -> TypeScheme

predTypeScheme (SimpleTypeScheme t) = SimpleTypeScheme (predType t)

predTypeScheme (TypeScheme vs t ps) = TypeScheme vs (predTypeScheme t) ps

predType :: Type -> Type

predType t = FunType t PFunArr (TupleType [] []) []

qualPredName :: Token -> GenParser Char st Term

qualPredName o = do { v <- asKey predS

; i <- instOpName

; c <- colT

; t <- typeScheme

; p <- cParenT

; return (QualOp i (predTypeScheme t)

(toPos o [v, c] p))

}

typeQual :: Bool -> GenParser Char st (TypeQual, Token)

typeQual b =

do q <- colT

return (OfType, q)

<|>

if b then

do q <- asT

return (AsType, q)

<|>

do q <- asKey inS

return (InType, q)

else

do q <- asT

return (AsType, q)

typedTerm :: Term -> Bool -> GenParser Char st Term

typedTerm f b =

do (q, p) <- typeQual b

t <- parseType

return (TypedTerm f q t (tokPos p))

mixTerm :: Bool -> GenParser Char st Term

mixTerm b =

do ts <- many1 $ primTerm b

let t = if length ts == 1 then head ts else MixfixTerm ts

in typedTerm t b <|> return t

term :: GenParser Char st Term

term = mixTerm True

-----------------------------------------------------------------------------

-- quantified term

-----------------------------------------------------------------------------

forallTerm :: Bool -> GenParser Char st Term

forallTerm b =

do f <- forallT

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

d <- dotT

t <- mixTerm b

return (QuantifiedTerm Universal (concat vs) t

(toPos f ps d))

exQuant :: GenParser Char st (Quantifier, Id.Token)

exQuant =

do { q <- asKey (existsS++exMark)

; return (Unique, q)

}

<|>

do { q <- asKey existsS

; return (Existential, q)

}

exTerm :: Bool -> GenParser Char st Term

exTerm b =

do { (q, p) <- exQuant

; (vs, ps) <- varDecls `separatedBy` semiT

; d <- dotT

; f <- mixTerm b

; return (QuantifiedTerm q (map GenVarDecl (concat vs)) f

(toPos p ps d))

}

lamDot :: GenParser Char st (Partiality, Token)

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

return (Total,d)

<|>

do d <- dotT

return (Partial,d)

lambdaTerm :: Bool -> GenParser Char st Term

lambdaTerm b =

do l <- asKey lamS

pl <- lamPattern

(k, d) <- lamDot

t <- mixTerm b

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

lamPattern :: GenParser Char st [Pattern]

lamPattern = do (vs, ps) <- varDecls `separatedBy` semiT

return [PatternVars (concat vs) (map tokPos ps)]

<|>

many (bracketParser patterns oParenT cParenT semiT

(BracketPattern Parens))

-----------------------------------------------------------------------------

-- case-term

-----------------------------------------------------------------------------

-- b1 allows "->", b2 allows "in"-Terms

patternTermPair :: Bool -> Bool -> String -> GenParser Char st ProgEq

patternTermPair b1 b2 sep =

do p <- asPattern b1

s <- asKey sep

t <- mixTerm b2

return (ProgEq p t (tokPos s))

caseTerm :: Bool -> GenParser Char st Term

caseTerm b =

do c <- asKey caseS

t <- term

o <- asKey ofS

(ts, ps) <- patternTermPair False b funS `separatedBy` barT

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

-----------------------------------------------------------------------------

-- annos and lookahead after ";"

-----------------------------------------------------------------------------

-- skip to leading annotation and read many

annos :: GenParser Char st [Annotation]

annos = skip >> many (annotationL << skip)

tryItemEnd :: [String] -> GenParser Char st ()

tryItemEnd l =

try (do { c <- lookAhead (annos >>

(single (oneOf "\"([{")

<|> placeS

<|> scanAnySigns

<|> many scanLPD))

; if null c || c `elem` l then return () else unexpected c

})

-- "axiom/axioms ... ; exists ... " is not supported

startKeyword :: [String]

startKeyword = dotS:cDot: hascasl_reserved_words

-----------------------------------------------------------------------------

-- let-term

-----------------------------------------------------------------------------

letTerm :: Bool -> GenParser Char st Term

letTerm b =

do l <- asKey letS

(es, ps) <- patternTermPair True False equalS `separatedBy` semiT

i <- asKey inS

t <- mixTerm b

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