ParseTerm.hs revision 36ba2cb9632b54226ad1defaac537fbb0b2f224c
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maedermodule ParseTerm where
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport Id -- (Token(Token), Id(Id), showTok)
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederimport Lexer -- ((<:>), (<++>), flat, scanFloat, scanString, single, toKey)
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian Maederimport ParseType
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder-- ----------------------------------------------
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder-- parse decls (of bindings)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- ----------------------------------------------
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian MaedervarId = parseId
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maedercolon = toKey [colonChar]
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian MaederpartialColon = makeToken (keySign
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder (char colonChar <:> option "" (string partialSuffix)))
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaedervarDecl :: Parser Decl
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian MaedervarDecl = do { (is, cs) <- separatedBy varId comma
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder ; t <- funType
1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder ; return (Decl is t (map tokPos (cs ++ [c])))
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedervarDecls :: Parser ([Decl], [Pos])
cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian MaedervarDecls = do { (ds, cs) <- separatedBy varDecl semi
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder ; return (ds, map tokPos cs)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaederparseDecls = varDecls
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ----------------------------------------------
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- no-bracket-token, literal or place (for terms)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ----------------------------------------------
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederexEqual = string "=e="
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maederkeyword :: Show a => a -> Parser (a, Pos)
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maederkeyword a = do {t <- toKey (show a)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder ; return (a, tokPos t)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederasOp = keyword AsType
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederinOp = keyword InType
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederofOp = keyword OfType
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersimpleTerm :: Parser Term
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersimpleTerm = fmap SimpleTerm (makeToken(scanFloat <|> scanString <|>
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder otherToken <|> scanTermWords <|>
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder try exEqual <|> scanTermSigns)
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederstartTerm :: Parser Term
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederstartTerm = parenTerm <|> braceTerm <|> sBrktTerm <|> simpleTerm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederrestTerm :: Parser Term
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederrestTerm = startTerm <|> typedTerm
25612a7b3ce708909298d5426406592473880a20Christian MaedermixTerm = do { l <- startTerm <:> many restTerm <++> option [] (single quantTerm)
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder ; if length l == 1 then return (head l)
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder else return (MixTerm l)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder } <|> quantTerm
25612a7b3ce708909298d5426406592473880a20Christian MaedertypedTerm :: Parser Term
25612a7b3ce708909298d5426406592473880a20Christian MaedertypedTerm = do { (c, p) <- try (ofOp <|> asOp <|> inOp) <?> "type"
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder ; t <- funType
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; return (TypeInfo c t [p])
18b709ce961d68328da768318dcc70067f066d86Christian Maederterms :: Parser ([Term], [Pos])
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederterms = do { (ts, ps) <- separatedBy mixTerm comma
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; return (ts, map tokPos ps)
b814fecd0a2dbdeae62402903783d08e4206b4d2Christian MaederisColon c = showTok c == [colonChar]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederparsePartialType c = if isColon c then funType else fmap PartialType sortId
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederqualName = do { (w, p) <- try (keyword VarQ <|> keyword OpQ <|> keyword PredQ)
18b709ce961d68328da768318dcc70067f066d86Christian Maeder <?> "qualifier"
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder ; i <- parseId
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; c <- partialColon `checkWith` \c -> w == OpQ
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder || showTok c == [colonChar]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ; t <- parsePartialType c
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder ; return (Qualified (QualId w i t [p, tokPos c]))
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederparenTerm = do { o <- oParen
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder ; (ts, ps) <- fmap (\t -> ([t], [])) qualName <|> terms
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ; c <- cParen
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder ; return (Application Parens ts (tokPos o : ps ++ [tokPos c]))
797f811e57952d59e73b8cd03b667eef276db972Christian MaederbraceTerm = do { o <- oBrace
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder ; (ts, ps) <- option ([], []) terms
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; c <- cBrace
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; return (Application Braces ts (tokPos o : ps ++ [tokPos c]))
18b709ce961d68328da768318dcc70067f066d86Christian MaedersBrktTerm = do { o <- opBrkt
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; (ts, ps) <- option ([], []) terms
18b709ce961d68328da768318dcc70067f066d86Christian Maeder ; c <- clBrkt
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ; return (Application Squares ts (tokPos o : ps ++ [tokPos c]))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederquant = try (keyword ExistsUnique <|> keyword Exists <|> keyword Forall
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder <|> keyword LambdaPartial) <?> "quantifier"
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedergetDot = makeToken (keySign (oneOf (dotChar:middleDotStr)
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder <:> option "" (string totalSuffix)))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisLambda (LambdaPartial) = True
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisLambda (LambdaTotal) = True
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederisLambda _ = False
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederquantTerm = do { (q, p) <- quant
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder ; (vs, ps) <- varDecls
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ; d <- getDot `checkWith` \d -> length (showTok d) == 1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder || isLambda q
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ; t <- mixTerm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ; let qu = if length (showTok d) > 1 then LambdaTotal else q
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder in return (Binding qu vs t (p:ps ++ [tokPos d]))
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederparseTerm = mixTerm