diff --git a/language.cabal b/language.cabal index 7b21b60..f803c1b 100644 --- a/language.cabal +++ b/language.cabal @@ -15,7 +15,6 @@ extra-doc-files: CHANGELOG.md extra-source-files: Grammar.cf - common warnings ghc-options: -Wdefault @@ -51,6 +50,34 @@ executable language , either , extra , array - , unification-fd default-language: GHC2021 + +test-suite test + hs-source-dirs: tests, src + main-is: Main.hs + type: exitcode-stdio-1.0 + + other-modules: + Grammar.Abs + Grammar.Lex + Grammar.Par + Grammar.Print + Grammar.Skel + Grammar.ErrM + Auxiliary + Renamer.RenamerM + TypeChecker.AlgoW + TypeChecker.HM + TypeChecker.HMIr + + build-depends: + base >=4.16 + , mtl + , containers + , either + , array + , extra + , hspec + + default-language: GHC2021 diff --git a/src/Main.hs b/src/Main.hs index 1a73e95..58811fe 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -12,8 +12,7 @@ import System.Exit (exitFailure, exitSuccess) import TypeChecker.AlgoW (typecheck) main :: IO () -main = - getArgs >>= \case +main = getArgs >>= \case [] -> print "Required file path missing" (x : _) -> do file <- readFile x diff --git a/src/Renamer/RenamerM.hs b/src/Renamer/RenamerM.hs index 215290c..5fb1fa2 100644 --- a/src/Renamer/RenamerM.hs +++ b/src/Renamer/RenamerM.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} module Renamer.RenamerM where diff --git a/src/TypeChecker/AlgoW.hs b/src/TypeChecker/AlgoW.hs index 3492908..de931d1 100644 --- a/src/TypeChecker/AlgoW.hs +++ b/src/TypeChecker/AlgoW.hs @@ -120,12 +120,11 @@ w = \case return (s3 `compose` s2 `compose` s1, t, T.EApp t e0' e1') ELet name e0 e1 -> do (s1, t1, e0') <- w e0 - applySt s1 $ do - env <- asks vars - let t' = generalize (apply s1 env) t1 - withBinding name t' $ do - (s2, t2, e1') <- w e1 - return (s2 `compose` s1, t2, T.ELet t2 name e0' e1' ) + env <- asks vars + let t' = generalize (apply s1 env) t1 + withBinding name t' $ do + (s2, t2, e1') <- w e1 + return (s2 `compose` s1, t2, T.ELet t2 name e0' e1' ) -- | Unify two types producing a new substitution (constraint) unify :: Type -> Type -> Infer Subst diff --git a/src/TypeChecker/Unification.hs b/src/TypeChecker/Unification.hs deleted file mode 100644 index 226e1e9..0000000 --- a/src/TypeChecker/Unification.hs +++ /dev/null @@ -1,261 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternSynonyms #-} - -module TypeChecker.Unification where - -import Control.Arrow ((>>>)) -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State -import Control.Unification hiding (applyBindings, (=:=)) -import qualified Control.Unification as U -import Control.Unification.IntVar -import Data.Foldable (fold) -import Data.Functor.Fixedpoint -import Data.Functor.Identity -import Data.Map (Map) -import qualified Data.Map as M -import Data.Maybe (fromJust, fromMaybe) -import Data.Set (Set, (\\)) -import qualified Data.Set as S -import Debug.Trace (trace) -import GHC.Generics (Generic1) -import Renamer.Renamer -import qualified Renamer.RenamerIr as R -import Renamer.RenamerIr (Const (..), Ident (..), RBind (..), - RExp (..), RProgram (..)) - -type Ctx = Map Ident UPolytype - -type TypeError = String - -data TypeT a = TPolyT Ident | TMonoT Ident | TArrowT a a - deriving (Functor, Foldable, Traversable, Generic1, Unifiable) - -instance Show a => Show (TypeT a) where - show (TPolyT (Ident i)) = i - show (TMonoT (Ident i)) = i - show (TArrowT a b) = show a ++ " -> " ++ show b - -type Infer = StateT (Map Ident UPolytype) (ReaderT Ctx (ExceptT TypeError (IntBindingT TypeT Identity))) - -type Type = Fix TypeT - -type UType = UTerm TypeT IntVar - -data Poly t = Forall [Ident] t - deriving (Eq, Functor) - -instance Show t => Show (Poly t) where - show (Forall is t) = unwords (map (\(Ident x) -> "forall " ++ x ++ ".") is) ++ " " ++ show t - -type Polytype = Poly Type - -type UPolytype = Poly UType - -pattern TPoly :: Ident -> Type -pattern TPoly v = Fix (TPolyT v) - -pattern TMono :: Ident -> Type -pattern TMono v = Fix (TMonoT v) - -pattern TArrow :: Type -> Type -> Type -pattern TArrow t1 t2 = Fix (TArrowT t1 t2) - -pattern UTMono :: Ident -> UType -pattern UTMono v = UTerm (TMonoT v) - -pattern UTArrow :: UType -> UType -> UType -pattern UTArrow t1 t2 = UTerm (TArrowT t1 t2) - -pattern UTPoly :: Ident -> UType -pattern UTPoly v = UTerm (TPolyT v) - -data TType = TTPoly Ident | TTMono Ident | TTArrow TType TType - deriving (Show) - -newtype Program = Program [Bind] - deriving (Show) - -data Bind = Bind Ident Exp Polytype - deriving (Show) - -data Exp - = EAnn Exp Polytype - | EBound Ident Polytype - | EFree Ident Polytype - | EConst Const Polytype - | EApp Exp Exp Polytype - | EAdd Exp Exp Polytype - | EAbs Ident Exp Polytype - deriving (Show) - -data TExp - = TAnn TExp UType - | TFree Ident UType - | TBound Ident UType - | TConst Const UType - | TApp TExp TExp UType - | TAdd TExp TExp UType - | TAbs Ident TExp UType - deriving (Show) - ----------------------------------------------------------- -typecheck :: RProgram -> Either TypeError Program -typecheck = undefined - -run :: Infer (UType, TExp) -> Either TypeError Polytype -run = fmap fst - >>> (>>= applyBindings) - >>> (>>= (generalize >>> fmap fromUPolytype)) - >>> flip evalStateT mempty - >>> flip runReaderT mempty - >>> runExceptT - >>> evalIntBindingT - >>> runIdentity - -infer :: RExp -> Infer (UType, TExp) -infer = \case - (RConst (CInt i)) -> return (UTMono "Int", TConst (CInt i) (UTMono "Int")) - (RConst (CStr str)) -> return (UTMono "String", TConst (CStr str) (UTMono "String")) - (RAdd e1 e2) -> do - (t1, e1') <- infer e2 - (t2, e2') <- infer e1 - t1 =:= UTMono "Int" - t2 =:= UTMono "Int" - return (UTMono "Int", TAdd e1' e2' (UTMono "Int")) - -- type is not used, probably wrong - (RAnn e t) -> do - (t', e') <- infer e - check e t' - return (t', TAnn e' t') - (RApp e1 e2) -> do - (f, e1') <- infer e1 - (arg, e2') <- infer e2 - res <- fresh - f =:= UTArrow arg res - return (res, TApp e1' e2' res) - (RAbs _ i e) -> do - arg <- fresh - withBinding i (Forall [] arg) $ do - (res, e') <- infer e - return (UTArrow arg res, TAbs i e' (UTArrow arg res)) - (RFree i) -> do - t <- lookupSigsT i - return (t, TFree i t) - (RBound _ i) -> do - t <- lookupVarT i - return (t, TBound i t) - -check :: RExp -> UType -> Infer () -check expr t = do - (t', _) <- infer expr - t =:= t' - return () - -lookupVarT :: Ident -> Infer UType -lookupVarT x@(Ident i) = do - ctx <- ask - maybe (throwError $ "Var - Unbound variable: " <> i) instantiate (M.lookup x ctx) - -lookupSigsT :: Ident -> Infer UType -lookupSigsT x@(Ident i) = do - ctx <- ask - case M.lookup x ctx of - Nothing -> trace (show ctx) (throwError $ "Sigs - Unbound variable: " <> i) - Just ut -> return $ fromPolytype ut - -insertSigs :: MonadState (Map Ident UPolytype) m => Ident -> UPolytype -> m () -insertSigs x ty = modify (M.insert x ty) - -fromPolytype :: UPolytype -> UType -fromPolytype (Forall ids ut) = ut - -ucata :: Functor t => (v -> a) -> (t a -> a) -> UTerm t v -> a -ucata f _ (UVar v) = f v -ucata f g (UTerm t) = g (fmap (ucata f g) t) - -withBinding :: MonadReader Ctx m => Ident -> UPolytype -> m a -> m a -withBinding x ty = local (M.insert x ty) - -deriving instance Ord IntVar - -class FreeVars a where - freeVars :: a -> Infer (Set (Either Ident IntVar)) - -instance FreeVars UType where - freeVars ut = do - fuvs <- fmap (S.fromList . map Right) . lift . lift . lift $ getFreeVars ut - let ftvs = - ucata - (const S.empty) - (\case TMonoT x -> S.singleton (Left x); f -> fold f) - ut - return $ fuvs `S.union` ftvs - -instance FreeVars UPolytype where - freeVars (Forall xs ut) = (\\ (S.fromList (map Left xs))) <$> freeVars ut - -instance FreeVars Ctx where - freeVars = fmap S.unions . mapM freeVars . M.elems - -fresh :: Infer UType -fresh = UVar <$> lift (lift (lift freeVar)) - -instance Fallible TypeT IntVar TypeError where - occursFailure iv ut = "Infinite" - mismatchFailure iv ut = "Mismatch" - -(=:=) :: UType -> UType -> Infer UType -(=:=) s t = lift . lift $ s U.=:= t - -applyBindings :: UType -> Infer UType -applyBindings = lift . lift . U.applyBindings - -instantiate :: UPolytype -> Infer UType -instantiate (Forall xs uty) = do - xs' <- mapM (const fresh) xs - return $ substU (M.fromList (zip (map Left xs) xs')) uty - -substU :: Map (Either Ident IntVar) UType -> UType -> UType -substU m = - ucata - (\v -> fromMaybe (UVar v) (M.lookup (Right v) m)) - ( \case - TPolyT v -> fromMaybe (UTPoly v) (M.lookup (Left v) m) - f -> UTerm f - ) - -skolemize :: UPolytype -> Infer UType -skolemize (Forall xs uty) = do - xs' <- mapM (const fresh) xs - return $ substU (M.fromList (zip (map Left xs) (map toSkolem xs'))) uty - where - toSkolem (UVar v) = UTPoly (mkVarName "s" v) - -mkVarName :: String -> IntVar -> Ident -mkVarName nm (IntVar v) = Ident $ nm ++ show (v + (maxBound :: Int) + 1) - --- | Used in let bindings to generalize functions declared there -generalize :: UType -> Infer UPolytype -generalize uty = do - uty' <- applyBindings uty - ctx <- ask - tmfvs <- freeVars uty' - ctxfvs <- freeVars ctx - let fvs = S.toList $ tmfvs \\ ctxfvs - xs = map (either id (mkVarName "a")) fvs - return $ Forall xs (substU (M.fromList (zip fvs (map UTPoly xs))) uty') - -fromUPolytype :: UPolytype -> Polytype -fromUPolytype = fmap (fromJust . freeze) - -inf = RAbs 0 "x" (RApp (RBound 0 "x") (RBound 0 "x")) - -one = RConst (CInt 1) - -lambda = RAbs 0 "f" (RAbs 1 "x" (RApp (RBound 0 "f") (RBound 1 "x"))) - -fn = RAbs 0 "x" (RBound 0 "x") diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 index 0000000..7432800 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Main where + +import Grammar.Abs +import System.Exit (exitFailure) +import Test.Hspec +import TypeChecker.AlgoW + +main :: IO () +main = do + print "RUNNING TESTS BROTHER" + exitFailure + -- hspec $ do + -- describe "the algorithm W" $ do + -- it "infers EInt as type Int" $ do + -- fmap fst (run (inferExp (EInt 1))) `shouldBe` Right (TMono "Int") + -- it "throws an exception if a variable is inferred with an empty env" $ do + -- run (inferExp (EId "x")) `shouldBe` Left "Unbound variable: x" + -- it "throws an exception if the annotated type does not match the inferred type" $ do + -- fmap fst (run (inferExp (EAnn (EInt 3) (TPol "a")))) `shouldBe` Right (TMono "bad")