From 0d30cb80e02daae74c62206ace6667deb26d38a8 Mon Sep 17 00:00:00 2001 From: sebastian Date: Thu, 6 Apr 2023 14:19:54 +0200 Subject: [PATCH] removed pretty printing of tvars --- src/TypeChecker/TypeCheckerHm.hs | 123 ++++++++++++++++--------------- 1 file changed, 62 insertions(+), 61 deletions(-) diff --git a/src/TypeChecker/TypeCheckerHm.hs b/src/TypeChecker/TypeCheckerHm.hs index bac1d44..826caa1 100644 --- a/src/TypeChecker/TypeCheckerHm.hs +++ b/src/TypeChecker/TypeCheckerHm.hs @@ -1,31 +1,31 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedRecordDot #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE QualifiedDo #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QualifiedDo #-} -- | A module for type checking and inference using algorithm W, Hindley-Milner module TypeChecker.TypeCheckerHm where -import Auxiliary (int, litType, maybeToRightM, unzip4) -import qualified Auxiliary as Aux -import Control.Monad.Except -import Control.Monad.Identity (Identity, runIdentity) -import Control.Monad.Reader -import Control.Monad.State -import Control.Monad.Writer -import Data.Coerce (coerce) -import Data.Function (on) -import Data.List (foldl', nub, sortOn) -import Data.List.Extra (unsnoc) -import Data.Map (Map) -import qualified Data.Map as M -import Data.Maybe (fromJust) -import Data.Set (Set) -import qualified Data.Set as S -import Debug.Trace (trace) -import Grammar.Abs -import Grammar.Print (printTree) -import qualified TypeChecker.TypeCheckerIr as T +import Auxiliary (int, litType, maybeToRightM, unzip4) +import Auxiliary qualified as Aux +import Control.Monad.Except +import Control.Monad.Identity (Identity, runIdentity) +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Writer +import Data.Coerce (coerce) +import Data.Function (on) +import Data.List (foldl', nub, sortOn) +import Data.List.Extra (unsnoc) +import Data.Map (Map) +import Data.Map qualified as M +import Data.Maybe (fromJust) +import Data.Set (Set) +import Data.Set qualified as S +import Debug.Trace (trace) +import Grammar.Abs +import Grammar.Print (printTree) +import TypeChecker.TypeCheckerIr qualified as T {- TODO @@ -40,16 +40,17 @@ typecheck :: Program -> Either String (T.Program' Type, [Warning]) typecheck = onLeft msg . run . checkPrg where onLeft :: (Error -> String) -> Either Error a -> Either String a - onLeft f (Left x) = Left $ f x + onLeft f (Left x) = Left $ f x onLeft _ (Right x) = Right x checkPrg :: Program -> Infer (T.Program' Type) checkPrg (Program bs) = do preRun bs - sgs <- gets sigs + -- sgs <- gets sigs bs <- map snd . sortOn fst <$> bindCount bs bs <- checkDef bs - return . prettify sgs . T.Program $ bs + -- return . prettify sgs . T.Program $ bs + return . T.Program $ bs -- | Send the map of user declared signatures to not rename stuff the user defined prettify :: Map T.Ident (Maybe Type) -> T.Program' Type -> T.Program' Type @@ -126,7 +127,7 @@ preRun (x : xs) = case x of s <- gets sigs case M.lookup (coerce n) s of Nothing -> insertSig (coerce n) Nothing >> preRun xs - Just _ -> preRun xs + Just _ -> preRun xs DData d@(Data t _) -> collect (collectTVars t) >> checkData d >> preRun xs where -- Check if function body / signature has been declared already @@ -148,11 +149,11 @@ checkDef (x : xs) = case x of T.Data t $ map (\(Inj name typ) -> T.Inj (coerce name) typ) injs freeOrdered :: Type -> [T.Ident] -freeOrdered (TVar (MkTVar a)) = return (coerce a) +freeOrdered (TVar (MkTVar a)) = return (coerce a) freeOrdered (TAll (MkTVar bound) t) = return (coerce bound) ++ freeOrdered t -freeOrdered (TFun a b) = freeOrdered a ++ freeOrdered b -freeOrdered (TData _ a) = concatMap freeOrdered a -freeOrdered _ = mempty +freeOrdered (TFun a b) = freeOrdered a ++ freeOrdered b +freeOrdered (TData _ a) = concatMap freeOrdered a +freeOrdered _ = mempty checkBind :: Bind -> Infer (T.Bind' Type) checkBind (Bind name args e) = do @@ -226,11 +227,11 @@ checkInj (Inj c inj_typ) name tvars toTVar :: Type -> Either Error TVar toTVar = \case TVar tvar -> pure tvar - _ -> uncatchableErr "Not a type variable" + _ -> uncatchableErr "Not a type variable" returnType :: Type -> Type returnType (TFun _ t2) = returnType t2 -returnType a = a +returnType a = a inferExp :: Exp -> Infer (T.ExpT' Type) inferExp e = do @@ -243,7 +244,7 @@ class CollectTVars a where instance CollectTVars Exp where collectTVars (EAnn e t) = collectTVars t `S.union` collectTVars e - collectTVars _ = S.empty + collectTVars _ = S.empty instance CollectTVars Type where collectTVars (TVar (MkTVar i)) = S.singleton (coerce i) @@ -562,12 +563,12 @@ generalize :: Map T.Ident Type -> Type -> Type generalize env t = go (S.toList $ free t S.\\ free env) (removeForalls t) where go :: [T.Ident] -> Type -> Type - go [] t = t + go [] t = t go (x : xs) t = TAll (MkTVar (coerce x)) (go xs t) removeForalls :: Type -> Type - removeForalls (TAll _ t) = removeForalls t + removeForalls (TAll _ t) = removeForalls t removeForalls (TFun t1 t2) = TFun (removeForalls t1) (removeForalls t2) - removeForalls t = t + removeForalls t = t {- | Instantiate a polymorphic type. The free type variables are substituted with fresh ones. @@ -615,28 +616,28 @@ currently this is not the case, the TAll pattern match is incorrectly implemente skipForalls :: Type -> Type skipForalls = \case - TAll _ t -> t - t -> t + TAll _ t -> skipForalls t + t -> t foralls :: Type -> [T.Ident] foralls (TAll (MkTVar a) t) = coerce a : foralls t -foralls _ = [] +foralls _ = [] mkForall :: Type -> Type mkForall t = case map (TAll . MkTVar . coerce) $ S.toList $ free t of [] -> t (x : xs) -> - let f acc [] = acc + let f acc [] = acc f acc (x : xs) = f (x acc) xs (y : ys) = reverse $ x : xs in f (y t) ys skolemize :: Type -> Type skolemize (TVar (MkTVar a)) = TEVar $ MkTEVar a -skolemize (TAll x t) = TAll x (skolemize t) -skolemize (TFun t1 t2) = (TFun `on` skolemize) t1 t2 -skolemize (TData n ts) = TData n (map skolemize ts) -skolemize t = t +skolemize (TAll x t) = TAll x (skolemize t) +skolemize (TFun t1 t2) = (TFun `on` skolemize) t1 t2 +skolemize (TData n ts) = TData n (map skolemize ts) +skolemize t = t -- | A class for substitutions class SubstType t where @@ -670,10 +671,10 @@ instance SubstType Type where TLit _ -> t TVar (MkTVar a) -> case M.lookup (coerce a) sub of Nothing -> TVar (MkTVar $ coerce a) - Just t -> t + Just t -> t TAll (MkTVar i) t -> case M.lookup (coerce i) sub of Nothing -> TAll (MkTVar i) (apply sub t) - Just _ -> apply sub t + Just _ -> apply sub t TFun a b -> TFun (apply sub a) (apply sub b) TData name a -> TData name (apply sub a) TEVar (MkTEVar _) -> t @@ -718,10 +719,10 @@ instance SubstType (T.Branch' Type) where instance SubstType (T.Pattern' Type) where apply s = \case T.PVar (iden, t) -> T.PVar (iden, apply s t) - T.PLit (lit, t) -> T.PLit (lit, apply s t) - T.PInj i ps -> T.PInj i $ apply s ps - T.PCatch -> T.PCatch - T.PEnum i -> T.PEnum i + T.PLit (lit, t) -> T.PLit (lit, apply s t) + T.PInj i ps -> T.PInj i $ apply s ps + T.PCatch -> T.PCatch + T.PEnum i -> T.PEnum i instance SubstType (T.Pattern' Type, Type) where apply s (p, t) = (apply s p, apply s t) @@ -763,10 +764,10 @@ withBindings xs = withPattern :: (Monad m, MonadReader Ctx m) => T.Pattern' Type -> m a -> m a withPattern p ma = case p of T.PVar (x, t) -> withBinding x t ma - T.PInj _ ps -> foldl' (flip withPattern) ma ps - T.PLit _ -> ma - T.PCatch -> ma - T.PEnum _ -> ma + T.PInj _ ps -> foldl' (flip withPattern) ma ps + T.PLit _ -> ma + T.PCatch -> ma + T.PEnum _ -> ma -- | Insert a function signature into the environment insertSig :: T.Ident -> Maybe Type -> Infer () @@ -791,11 +792,11 @@ existInj n = gets (M.lookup n . injections) flattenType :: Type -> [Type] flattenType (TFun a b) = flattenType a <> flattenType b -flattenType a = [a] +flattenType a = [a] typeLength :: Type -> Int typeLength (TFun _ b) = 1 + typeLength b -typeLength _ = 1 +typeLength _ = 1 {- | Catch an error if possible and add the given expression as addition to the error message @@ -878,11 +879,11 @@ newtype Ctx = Ctx {vars :: Map T.Ident Type} deriving (Show) data Env = Env - { count :: Int - , nextChar :: Char - , sigs :: Map T.Ident (Maybe Type) + { count :: Int + , nextChar :: Char + , sigs :: Map T.Ident (Maybe Type) , takenTypeVars :: Set T.Ident - , injections :: Map T.Ident Type + , injections :: Map T.Ident Type , declaredBinds :: Set T.Ident } deriving (Show)