From 880eb9d73e5ea9239698d8f6d294032b6e339310 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Tom=C3=A1=C5=A1=20Musil?= Date: Sat, 22 Aug 2015 05:09:21 +0200 Subject: [PATCH 1/1] =?utf8?q?pr=C3=A1ce=20na=20parseru=20pro=20HM?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- src/HM.hs | 39 +++++++----- src/HM/Parser.hs | 145 ++++++++++++++++++++++++++++++++++++--------- src/Lambda/Parser/Fancy.hs | 5 +- 3 files changed, 144 insertions(+), 45 deletions(-) diff --git a/src/HM.hs b/src/HM.hs index 83bbe04..065ccbb 100644 --- a/src/HM.hs +++ b/src/HM.hs @@ -11,18 +11,27 @@ module HM ( -- * Types Type(..) - , Term + , TypeScheme(..) + , Term(..) + , TypedTerm(..) -- * Type inference , algW ) where +import Control.Monad.State + import HM.Term import HM.Parser type Substitution = TypeScheme -> TypeScheme +type VarS a = State Int a fresh :: TypeVarName fresh = undefined +--fresh = do +-- n <- get +-- "a" ++ show n + substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme substitute = undefined @@ -32,17 +41,17 @@ unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b -algW :: HMTerm -> Either String TypeScheme -algW (HMTerm (Var _) t) = Right t -algW (HMTerm (Lambda x t) (TScheme p)) = do - let v = TScheme (TypeVar fresh) - np = substitute v x t - unify p np -algW (HMTerm (App u v) t) = do - tu <- algW u - tv <- algW v - case tu of - (TScheme (TypeFunction a b)) -> do - unify a tv - return b - _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv +algW :: TypedTerm -> Either String TypeScheme +algW (TTerm (Var _) t) = Right t +--algW (TTerm (Lam x t) (TScheme p)) = do +-- let v = TScheme (TypeVar fresh) +-- np = substitute v x t +-- unify p np +--algW (TTerm (App u v) t) = do +-- tu <- algW u +-- tv <- algW v +-- case tu of +-- (TScheme (TypeFunction a b)) -> do +-- unify a tv +-- return b +-- _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv 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 --} diff --git a/src/Lambda/Parser/Fancy.hs b/src/Lambda/Parser/Fancy.hs index 9a1deb3..3ad5728 100644 --- a/src/Lambda/Parser/Fancy.hs +++ b/src/Lambda/Parser/Fancy.hs @@ -22,6 +22,7 @@ module Lambda.Parser.Fancy , parseVar ) where +import Data.Char (isAsciiLower) import Data.Text as T hiding (map) import Data.Attoparsec.Text import Control.Applicative @@ -56,12 +57,12 @@ tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of parseVar :: Parser Term parseVar = do - x <- many1 (letter <|> digit) + x <- many1 $ satisfy isAsciiLower return $! Var x parseLambda :: Parser Term parseLambda = do - char '\\' <|> char 'λ' + char '\\' <|> char 'λ' <|> char 'L' vars <- sepBy1 parseVar (char ' ') char '.' t <- parseTerm -- 2.4.2