X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/64abbeaeddb1956b5c07a29cc6caea1a971101b5..880eb9d73e5ea9239698d8f6d294032b6e339310:/src/HM/Parser.hs?ds=sidebyside diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs index 556cbdb..f02a7cc 100644 --- a/src/HM/Parser.hs +++ b/src/HM/Parser.hs @@ -16,13 +16,12 @@ module HM.Parser , parseTerm ) where +import Data.Char (isAsciiLower, isAsciiUpper) import Data.Text as T hiding (map) import Data.Attoparsec.Text import Control.Applicative import HM.Term -import qualified Lambda.Parser.Fancy as Lambda -import qualified Lambda.Term as Lambda braced :: String -> String braced t = "(" ++ t ++ ")" @@ -31,9 +30,9 @@ instance Show Term where show (Var x) = x show (Lam x (NTTerm (Lam y t))) = show (Lam (x ++ " " ++ y) t) show (Lam x t) = braced $ "λ" ++ x ++ "." ++ show t - show (App a (NTTerm (App b c))) = show a ++ " " ++ (braced $ show (App b c)) + show (App a (NTTerm (App b c))) = show a ++ " " ++ braced ( show (App b c)) show (App t r) = show t ++ " " ++ show r - show (Let x e1 e2) = braced $ "let " ++ x ++ " = " ++ show e1 ++ " in " ++ show e2 + show (Let x e1 e2) = braced $ "LET " ++ x ++ " = " ++ show e1 ++ " IN " ++ show e2 instance Show TypedTerm where show (NTTerm t) = show t @@ -48,36 +47,126 @@ instance Show TypeScheme where show (TScheme t) = show t show (TSForAll x t) = braced $ "∀" ++ x ++ ": " ++ show t -tRead :: String -> Term -tRead = undefined +tRead :: String -> TypedTerm +tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of + (Right t) -> t + (Left e) -> error e -parseTerm :: Parser TypedTerm +parseTerm :: Parser Term parseTerm = parseLet <|> - (lambdaToHM <$> Lambda.parseTerm) + parseApp <|> + parseVar <|> + parseLambda -parseLet :: Parser TypedTerm -parseLet = do +parseTermNA :: Parser Term +parseTermNA = parseLet <|> + parseVar <|> + parseLambda + +parseTypeAndTermNA :: Parser TypedTerm +parseTypeAndTermNA = do + term <- parseTermNA + string " :: " + tp <- parseTypeScheme + return $! TTerm term tp + +parseTypeAndTerm :: Parser TypedTerm +parseTypeAndTerm = do + term <- parseTerm + string " :: " + tp <- parseTypeScheme + return $! TTerm term tp + +parseTypedTermNA :: Parser TypedTerm +parseTypedTermNA = parseBraces <|> + parseTypeAndTermNA <|> + (NTTerm <$> parseTerm) + +parseTypedTerm :: Parser TypedTerm +parseTypedTerm = parseBraces <|> + parseTypeAndTerm <|> + (NTTerm <$> parseTerm) + +parseType :: Parser Type +parseType = parsePrimitive <|> + parseTypeVar <|> + parseTypeFunction + +parsePrimitive :: Parser Type +parsePrimitive = do + x <- many1 $ satisfy isAsciiUpper + return $! Primitive x + +parseTypeVar :: Parser Type +parseTypeVar = do + x <- many1 $ satisfy isAsciiLower + return $! TypeVar x + +parseTypeFunction :: Parser Type +parseTypeFunction = do + a <- parseType + string " -> " + b <- parseType + return $! TypeFunction a b + +parseTypeScheme :: Parser TypeScheme +parseTypeScheme = parseForAll <|> + (TScheme <$> parseType) + +parseForAll :: Parser TypeScheme +parseForAll = do + string "FORALL " + (TypeVar x) <- parseTypeVar + string "." + t <- parseTypeScheme + return $! TSForAll x t + +parseBraces :: Parser TypedTerm +parseBraces = do char '(' - string "let " - (Lambda.Var x) <- Lambda.parseVar - string " = " - e1 <- lambdaToHM <$> Lambda.parseTerm - string " in " - e2 <- lambdaToHM <$> Lambda.parseTerm + t <- parseTypedTerm char ')' - return . NTTerm $ Let x e1 e2 + return t + +parseLet :: Parser Term +parseLet = do + string "LET " + (Var x) <- parseVar + string " = " + e1 <- parseTypedTerm + string " IN " + e2 <- parseTypedTerm + return $! Let x e1 e2 + +parseVar :: Parser Term +parseVar = do + x <- many1 $ satisfy isAsciiLower + return $! Var x + +parseLambda :: Parser Term +parseLambda = do + char '\\' <|> char 'λ' <|> char 'L' + vars <- sepBy1 parseVar (char ' ') + char '.' + t <- parseTypedTerm + let (NTTerm l) = createLambda vars t + return $! l + +parseApp :: Parser Term +parseApp = do + aps <- sepBy1 parseTypedTermNA (char ' ') + return $! createApp aps + +createLambda :: [Term] -> TypedTerm -> TypedTerm +createLambda (Var x : vs) t = NTTerm . Lam x $ createLambda vs t +createLambda [] t = t +createLambda _ _ = error "createLambda failed" + +createApp :: [TypedTerm] -> Term +createApp [t,ts] = App t ts +createApp (t:ts:tss) = createApp (NTTerm (App t ts) : tss) +createApp [] = error "empty createApp" -lambdaToHM :: Lambda.Term -> TypedTerm -lambdaToHM (Lambda.Var x) = NTTerm $ Var x -lambdaToHM (Lambda.App t u) = NTTerm $ App (lambdaToHM t) (lambdaToHM u) -lambdaToHM (Lambda.Lambda x t) = NTTerm $ Lam x (lambdaToHM t) -- | -- TODO prop> t == tRead (show (t :: Term)) - -{- -tRead :: String -> Term -tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of - (Right t) -> t - (Left e) -> error e --}