From 81f620c2c7d7bbe1ce8b7e2a573bd643e6b22f5e Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 18 Jul 2018 14:44:20 +0200 Subject: [PATCH] infer --- ast.dcl | 1 + ast.icl | 3 +- infer.dcl | 11 ++++++ infer.icl | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ parse.dcl | 2 +- parse.icl | 72 +++++++++++++++++------------------ 6 files changed, 160 insertions(+), 39 deletions(-) create mode 100644 infer.dcl create mode 100644 infer.icl diff --git a/ast.dcl b/ast.dcl index a24b2df..a490153 100644 --- a/ast.dcl +++ b/ast.dcl @@ -9,6 +9,7 @@ definition module ast | Variable String | Apply Expression Expression | Lambda String Expression + | Let String Expression Expression | Code String | .. diff --git a/ast.icl b/ast.icl index 3f52921..8911114 100644 --- a/ast.icl +++ b/ast.icl @@ -15,7 +15,8 @@ where pretty (Literal v) = pretty v pretty (Variable v) = string v pretty (Apply a b) = parens (pretty a <+> pretty b) - pretty (Lambda a b) = string "\\" <-> string a <-> string "->" <-> pretty b + pretty (Lambda a b) = string "\\" <-> string a <+> string "->" <+> pretty b + pretty (Let v a b) = string "let" <+> string v <+> string "=" <+> pretty a <+> string "in" <+> pretty b pretty (Code b) = string "code" <+> string b instance Pretty Function diff --git a/infer.dcl b/infer.dcl new file mode 100644 index 0000000..1c1d294 --- /dev/null +++ b/infer.dcl @@ -0,0 +1,11 @@ +definition module infer + +from Data.Map import :: Map + +:: Type + = VarType String + | IntType + | BoolType + | CharType + | Arrow Type Type +:: Scheme = Forall [String] Type diff --git a/infer.icl b/infer.icl new file mode 100644 index 0000000..fadc684 --- /dev/null +++ b/infer.icl @@ -0,0 +1,110 @@ +implementation module infer + +import StdEnv + +import qualified Data.Map as DM +from Data.Map import instance Functor (Map k) +import qualified Data.Set as DS +import Data.Functor +import Data.Func +import Data.Either +import Data.List +import Data.Maybe +import Control.Applicative +import Control.Monad +import Control.Monad.Trans +import qualified Control.Monad.State as MS +import Control.Monad.RWST + +import ast + +:: TypeEnv :== 'DM'.Map String Scheme +:: Constraint :== (Type, Type) +:: Subst :== 'DM'.Map String Type +:: Unifier :== (Subst, [Constraint]) +:: Infer a :== RWST TypeEnv [Constraint] InferState (Either TypeError) a +:: InferState = { count :: Int } +:: Solve a :== 'MS'.StateT Unifier (Either TypeError) a +:: TypeError = UnboundVariable String + +nullSubst :: Subst +nullSubst = 'DM'.newMap + +uni :: Type Type -> Infer () +uni t1 t2 = tell [(t1, t2)] + +inEnv :: (String, Scheme) (Infer a) -> Infer a +inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m + +letters :: [String] +letters = map toString $ [1..] >>= flip replicateM ['a'..'z'] + +fresh :: Infer Type +fresh = get >>= \s=:{count}->put {s & count=count + 1} >>| pure (VarType $ letters !! count) + +lookupEnv :: String -> Infer Type +lookupEnv x = asks ('DM'.get x) + >>= maybe (liftT $ Left $ UnboundVariable x) instantiate + +class Substitutable a +where + apply :: Subst a -> a + ftv :: a -> 'DS'.Set String + +instance Substitutable Type +where + apply s t=:(VarType a) = maybe t id $ 'DM'.get a s + apply s (Arrow t1 t2) = Arrow (apply s t1) (apply s t2) + apply _ t = t + + ftv (VarType a) = 'DS'.singleton a + ftv (Arrow t1 t2) = 'DS'.union (ftv t1) (ftv t2) + ftv t = 'DS'.newSet + +instance Substitutable Scheme +where + apply s (Forall as t) = Forall as $ apply (foldr 'DM'.del s as) t + ftv (Forall as t) = 'DS'.difference (ftv t) ('DS'.fromList as) + +instance Substitutable [a] | Substitutable a +where + apply s ls = map (apply s) ls + ftv t = foldr ('DS'.union o ftv) 'DS'.newSet t + +instance Substitutable TypeEnv where + apply s env = fmap (apply s) env + ftv env = ftv $ 'DM'.elems env + +instantiate :: Scheme -> Infer Type +instantiate (Forall as t) = mapM (const fresh) as + >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t +generalize :: TypeEnv Type -> Scheme +generalize env t = Forall ('DS'.toList $ 'DS'.difference (ftv t) (ftv env)) t + +infer :: Expression -> Infer Type +infer (Literal v) = case v of + Int _ = pure IntType + Bool _ = pure BoolType + Char _ = pure CharType +infer (Variable s) = lookupEnv s +infer (Apply e1 e2) + = infer e1 + >>= \t1->infer e2 + >>= \t2->fresh + >>= \tv->uni t1 (Arrow t2 tv) + >>| pure tv +infer (Lambda s e) + = fresh + >>= \tv->inEnv (s, Forall [] tv) (infer e) + >>= \t-> pure (Arrow tv t) +infer (Let x e1 e2) + = ask + >>= \en->infer e1 + >>= \t1->inEnv (x, generalize en t1) (infer e2) +infer (Code c) = fresh >>= \v->pure case c of + "add" = Arrow v (Arrow v v) + "sub" = Arrow v (Arrow v v) + "mul" = Arrow v (Arrow v v) + "div" = Arrow v (Arrow v v) + "and" = Arrow v (Arrow v BoolType) + "or" = Arrow v (Arrow v BoolType) diff --git a/parse.dcl b/parse.dcl index 9ac10cd..e059278 100644 --- a/parse.dcl +++ b/parse.dcl @@ -9,5 +9,5 @@ from StdOverloaded import class zero instance zero ParseState -lex :: [Char] -> [Token] +lex :: [Char] -> [Token] parse :: [Token] ParseState -> Either [String] AST diff --git a/parse.icl b/parse.icl index e5927bd..4359629 100644 --- a/parse.icl +++ b/parse.icl @@ -22,33 +22,39 @@ import Data.Tuple derive consName Token, Value :: Expression | DelayedParse [Token] - :: Token = IntToken Int | BoolToken Bool | CharToken Char | IdentToken String | InfixrToken | InfixlToken | SemiColonToken | OpenBraceToken | CloseBraceToken | EqualsToken | CodeToken | LambdaToken - | ArrowToken + | ArrowToken | LetToken | InToken +:: ParseState = {tokens :: [Token], infixers :: [Infix]} +:: Infix = Infix String Fixity Int +:: Fixity = InfixL | InfixR +:: Parser a :== StateT ParseState (Either [String]) a + +instance < Infix where (<) (Infix _ _ s) (Infix _ _ t) = s < t +instance zero ParseState where zero = {tokens=[],infixers=[]} lex :: [Char] -> [Token] lex cs = lex` cs where - lex` [] = [] - lex` ['\n':cs] = lex` cs - lex` [c:cs] - | isSpace c = lex` cs - lex` [';':cs] = [SemiColonToken:lex` cs] - lex` ['=',c:cs] - | not (isIdent c) = [EqualsToken:lex` [c:cs]] - lex` ['(':cs] = [OpenBraceToken:lex` cs] - lex` [')':cs] = [CloseBraceToken:lex` cs] - lex` ['-','>':cs] = [ArrowToken:lex` cs] - lex` ['\\':cs] = [LambdaToken:lex` cs] - lex` ['\'',c,'\'':cs] = [CharToken c:lex` cs] - lex` ['T','r','u','e':cs] = [BoolToken True:lex` cs] - lex` ['c','o','d','e':cs] = [CodeToken:lex` cs] - lex` ['F','a','l','s','e':cs] = [BoolToken True:lex` cs] - lex` ['i','n','f','i','x','r':cs] = [InfixrToken:lex` cs] - lex` ['i','n','f','i','x','l':cs] = [InfixlToken:lex` cs] + lex` [] = [] + lex` ['\n':cs] = lex` cs + lex` [c:cs] | isSpace c = lex` cs + lex` [';':cs] = [SemiColonToken:lex` cs] + lex` ['=',c:cs] | not (isIdent c) = [EqualsToken:lex` [c:cs]] + lex` ['(':cs] = [OpenBraceToken:lex` cs] + lex` [')':cs] = [CloseBraceToken:lex` cs] + lex` ['->':cs] = [ArrowToken:lex` cs] + lex` ['\\':cs] = [LambdaToken:lex` cs] + lex` ['\'',c,'\'':cs] = [CharToken c:lex` cs] + lex` ['let':cs] | whiteOrEnd cs = [LetToken:lex` cs] + lex` ['in':cs] | whiteOrEnd cs = [InToken:lex` cs] + lex` ['code':cs] | whiteOrEnd cs = [CodeToken:lex` cs] + lex` ['False':cs] | whiteOrEnd cs = [BoolToken True:lex` cs] + lex` ['True':cs] | whiteOrEnd cs = [BoolToken True:lex` cs] + lex` ['infixr':cs] | whiteOrEnd cs = [InfixrToken:lex` cs] + lex` ['infixl':cs] | whiteOrEnd cs = [InfixlToken:lex` cs] lex` ['-',c:cs] | isDigit c = case lex` [c:cs] of @@ -66,21 +72,12 @@ where = [IdentToken $ toString [c:i]:lex` cs] = abort $ "Huh lexer failed on: " +++ toString (toInt c) +whiteOrEnd [] = True +whiteOrEnd [c:cs] = isSpace c + isIdent c = isAlpha c || elem c ['\'`'] isFunny = flip elem ['!@#$%^&*\|+-?/\'<>.:~='] -:: ParseState = - { tokens :: [Token] - , infixers :: [Infix] - } -:: Infix = Infix String Fixity Int -instance < Infix where (<) (Infix _ _ s) (Infix _ _ t) = s < t -:: Fixity = InfixL | InfixR - -:: Parser a :== StateT ParseState (Either [String]) a - -instance zero ParseState where zero = {tokens=[],infixers=[]} - () infixl 1 :: a (StateT b (Either (c a)) d) -> StateT b (Either (c a)) d | Semigroup (c a) & Applicative c () err p = StateT $ first (flip mappend (pure err)) o runStateT p @@ -131,6 +128,7 @@ where parseBasic //Bracketed = token OpenBraceToken *> parseBracketed <* token CloseBraceToken + <|> Let <$> (token LetToken *> parseIdent <* token EqualsToken) <*> (parseExpr <* token InToken) <*> parseExpr <|> Literal <$> Int <$> parseInt <|> Code <$> (token CodeToken *> parseIdent) <|> flip (foldr Lambda) <$> (token LambdaToken *> some parseIdent <* token ArrowToken) <*> parseExpr @@ -139,17 +137,14 @@ where parseBracketed :: Parser Expression parseBracketed //Curried prefix infix - = (\e op->Apply (Apply fpflip op) e) <$> parseIfx <*> parseExpr + = (\op->Lambda "_v" o Apply (Apply op (Variable "v"))) <$> parseIfx <*> parseExpr //Regular Prefix infix <|> parseIfx //Curried flipped prefix infix - <|> Apply <$> parseExpr <*> parseIfx + <|> (\e op->Lambda "_v" (Apply (Apply op e) (Variable "v"))) <$> parseExpr <*> parseIfx //Parse regular expression <|> parseExpr - fpflip :: Expression - fpflip = Lambda "x" $ Lambda "y" $ Lambda "z" $ Apply (Apply (Variable "x") (Variable "z")) (Variable "y") - parseWithIfx :: ([String] String -> Bool) -> Parser String parseWithIfx f = gets (\s->[i\\Infix i _ _<-s.infixers]) >>= flip parseIf parseIdent o f @@ -183,6 +178,8 @@ Start = ['id x = x;'] ++ ['const x y = x;'] ++ ['flip x y z = x z y;'] ++ + ['twice f = f . f;'] ++ + ['fix f x = let x = f x in x;'] ++ ['. infixr 9 f g x = f $ g x;'] ++ ['$ infixr 0 = id;'] ++ ['& infixr 0 = flip $;'] ++ @@ -192,5 +189,6 @@ Start = ['/ infixr 7 = code div;'] ++ ['&& infixl 3 = code and;'] ++ ['|| infixl 2 = code or;'] ++ - ['ap = f . g $ x;'] + ['ap = (1 +);'] ++ + ['ap = (+ 1);'] ) zero -- 2.20.1