From f77793a132361a80f9736dc10d9e8c93168ff203 Mon Sep 17 00:00:00 2001 From: sebastian Date: Mon, 15 May 2023 23:40:15 +0200 Subject: [PATCH] Added proper error message to monomorphizer; made subst a monoid --- src/Main.hs | 2 +- src/Monomorphizer/Monomorphizer.hs | 74 +++++++++++++++--------------- src/TypeChecker/TypeCheckerHm.hs | 40 +++++++--------- src/TypeChecker/TypeCheckerIr.hs | 57 ++++++++++++----------- 4 files changed, 83 insertions(+), 90 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 7447747..cff33f7 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -144,7 +144,7 @@ main' opts s = when opts.logIL (printToErr "\n-- Lambda Lifter --" >> log lifted) - let monomorphized = monomorphize lifted + monomorphized <- fromErr $ monomorphize lifted when opts.logIL (printToErr "\n -- Monomorphizer --" >> log monomorphized) diff --git a/src/Monomorphizer/Monomorphizer.hs b/src/Monomorphizer/Monomorphizer.hs index 47ddbcc..c537a1e 100644 --- a/src/Monomorphizer/Monomorphizer.hs +++ b/src/Monomorphizer/Monomorphizer.hs @@ -28,7 +28,7 @@ module Monomorphizer.Monomorphizer (monomorphize, morphExp, morphBind) where import Control.Monad.Reader (MonadReader (ask, local), - Reader, asks, runReader) + ReaderT, asks, runReaderT) import Control.Monad.State (MonadState, StateT (runStateT), gets, modify) @@ -38,22 +38,20 @@ import Grammar.Print (printTree) import Monomorphizer.DataTypeRemover (removeDataTypes) import qualified Monomorphizer.MonomorphizerIr as O import qualified Monomorphizer.MorbIr as M --- import TypeChecker.TypeCheckerIr (Ident (Ident)) import LambdaLifterIr (Ident (..)) --- import TypeChecker.TypeCheckerIr qualified as T import qualified LambdaLifterIr as L import Data.Maybe (fromJust, catMaybes) import Data.Tuple.Extra (secondM) -import Debug.Trace (trace) -import Test.QuickCheck.State (State(expected)) +import Control.Monad.Except (throwError, Except, runExcept, MonadError) +import Data.List (foldl') {- | EnvM is the monad containing the read-only state as well as the output state containing monomorphized functions and to-be monomorphized data type declarations. -} -newtype EnvM a = EnvM (StateT Output (Reader Env) a) - deriving (Functor, Applicative, Monad, MonadState Output, MonadReader Env) +newtype EnvM a = EnvM (StateT Output (ReaderT Env (Except String)) a) + deriving (Functor, Applicative, Monad, MonadState Output, MonadReader Env, MonadError String) type Output = Map.Map Ident Outputted @@ -106,25 +104,26 @@ isConsMarked ident = gets (Map.member ident) -- | Finds main bind. getMain :: EnvM L.Bind -getMain = asks (\env -> case Map.lookup (Ident "main") (input env) of - Just mainBind -> mainBind - Nothing -> error "main not found in monomorphizer!" - ) +getMain = do + env <- ask + case Map.lookup (Ident "main") (input env) of + Just mainBind -> return mainBind + Nothing -> throwError "main not found in monomorphizer!" {- | Makes a kv pair list of polymorphic to monomorphic mappings, throws runtime error when encountering different structures between the two arguments. Debug: First argument is the name of the bind. -} -mapTypes :: Ident -> L.Type -> M.Type -> [(Ident, M.Type)] -mapTypes _ident (L.TLit _) (M.TLit _) = [] -mapTypes _ident (L.TVar (L.MkTVar i1)) tm = [(i1, tm)] +mapTypes :: Ident -> L.Type -> M.Type -> EnvM [(Ident, M.Type)] +mapTypes _ident (L.TLit _) (M.TLit _) = return [] +mapTypes _ident (L.TVar (L.MkTVar i1)) tm = return [(i1, tm)] mapTypes ident (L.TFun pt1 pt2) (M.TFun mt1 mt2) = - mapTypes ident pt1 mt1 - ++ mapTypes ident pt2 mt2 + (++) <$> mapTypes ident pt1 mt1 <*> mapTypes ident pt2 mt2 mapTypes ident (L.TData tIdent pTs) (M.TData mIdent mTs) = if tIdent /= mIdent - then error "the data type names of monomorphic and polymorphic data types does not match" - else foldl (\xs (p, m) -> mapTypes ident p m ++ xs) [] (zip pTs mTs) + then throwError "the data type names of monomorphic and polymorphic data types does not match" + else foldl' (\xs (p, m) -> do x <- mapTypes ident p m; (++x) <$> xs) (return []) (zip pTs mTs) +-- This is a proper callstack error as a previous phase has a bug. mapTypes ident t1 t2 = error $ "in bind: '" ++ printTree ident ++ "', " ++ "structure of types not the same: '" ++ printTree t1 ++ "', '" ++ printTree t2 ++ "'" @@ -166,11 +165,12 @@ morphBind expectedType b@(L.Bind (ident, btype) args (exp, expt)) = do -- The "new name" is used to find out if it is already marked or not. let name' = newFuncName expectedType b bindMarked <- isBindMarked name' + mt <- mapTypes ident btype expectedType local ( \env -> env { locals = Set.fromList (map fst args) - , polys = Map.fromList (mapTypes ident btype expectedType) + , polys = Map.fromList mt } ) $ do @@ -196,11 +196,12 @@ morphBind expectedType b@(L.BindC cxt (ident, btype) args (exp, expt)) = do -- The "new name" is used to find out if it is already marked or not. let name' = newFuncName expectedType b bindMarked <- isBindMarked name' + mt <- mapTypes ident btype expectedType local ( \env -> env { locals = Set.fromList (map fst args) - , polys = Map.fromList (mapTypes ident btype expectedType) + , polys = Map.fromList mt } ) $ do @@ -234,8 +235,7 @@ morphArg (ident, t) = do -- | Gets the data bind from the name of a constructor. getInputData :: Ident -> EnvM (Maybe L.Data) getInputData ident = do - env <- ask - return $ Map.lookup ident (dataDefs env) + asks (Map.lookup ident . dataDefs) {- | Monomorphize a constructor using it's global name. Constructors may appear as expressions in the tree, or as patterns in case-expressions. @@ -248,12 +248,13 @@ morphCons expectedType ident newIdent = do -- closures can have unbound variables Nothing -> pure () Just d -> do - modify (\output -> Map.insert newIdent (Data expectedType d) output) + modify (Map.insert newIdent (Data expectedType d)) -- | Converts literals from input to output tree. convertLit :: L.Lit -> M.Lit convertLit (L.LInt v) = M.LInt v convertLit (L.LChar v) = M.LChar v +convertLit l = error $ "Unexpected lit in monomorphizer: '" ++ printTree l ++ "'" -- | Monomorphizes an expression, given an expected type. @@ -292,7 +293,7 @@ morphExp expectedType exp = case exp of else do bind <- getInputBind ident case bind of - Nothing -> error $ "unbound variable: '" ++ printTree ident ++ "'" + Nothing -> throwError $ "unbound variable: '" ++ printTree ident ++ "'" Just bind' -> do -- New bind to process newBindName <- morphBind expectedType bind' @@ -356,8 +357,7 @@ morphPattern p expectedType = case p of -- Exampel: List a => a -> List a convertConsTypeToDataType :: M.Type -> [M.Type] -> M.Type -convertConsTypeToDataType inner (t:ts) = convertConsTypeToDataType (M.TFun t inner) ts -convertConsTypeToDataType inner [] = inner +convertConsTypeToDataType = foldl (flip M.TFun) -- | Creates a new identifier for a function with an assigned type. @@ -381,28 +381,26 @@ newName t (Ident str) = Ident $ str ++ "$" ++ newName' t newName' (M.TData (Ident str) ts) = str ++ foldl (\s t -> s ++ "." ++ newName' t) "" ts -- | Monomorphization step. -monomorphize :: L.Program -> O.Program -monomorphize (L.Program defs) = - removeDataTypes $ - M.Program - ( getDefsFromOutput - (runEnvM Map.empty (createEnv defs) monomorphize') - ) +monomorphize :: L.Program -> Either String O.Program +monomorphize (L.Program defs) = do + op <- runEnvM Map.empty (createEnv defs) monomorphize' + let prg = getDefsFromOutput op + return . removeDataTypes $ M.Program prg where monomorphize' :: EnvM () monomorphize' = do mainBind <- getMain case mainBind of - (L.BindC _ _ _ _) -> error "main should not be a BindC node" + (L.BindC {}) -> error "main should not be a BindC node" main@(L.Bind _ _ (_, mainType)) -> case getMonoFromMono mainType of - Nothing -> error "main should be monomorphic" + Nothing -> throwError "main should be monomorphic" Just mainTypeMono -> do morphBind mainTypeMono main return () -- | Runs and gives the output binds. -runEnvM :: Output -> Env -> EnvM () -> Output -runEnvM o env (EnvM stateM) = snd $ runReader (runStateT stateM o) env +runEnvM :: Output -> Env -> EnvM () -> Either String Output +runEnvM o env (EnvM stateM) = snd <$> runExcept (runReaderT (runStateT stateM o) env) -- | Creates the environment based on the input binds. createEnv :: [L.Def] -> Env @@ -485,7 +483,7 @@ createNewData ((consIdent, consType, polyData) : input) o = getDataType :: M.Type -> M.Type getDataType (M.TFun _t1 t2) = getDataType t2 getDataType tData@(M.TData _ _) = tData -getDataType _ = error "???" +getDataType _ = error "Bug in previous phase of compilation" addLocal :: Ident -> Env -> Env diff --git a/src/TypeChecker/TypeCheckerHm.hs b/src/TypeChecker/TypeCheckerHm.hs index f17e589..6564b8b 100644 --- a/src/TypeChecker/TypeCheckerHm.hs +++ b/src/TypeChecker/TypeCheckerHm.hs @@ -16,7 +16,7 @@ import Control.Monad.State import Control.Monad.Writer import Data.Coerce (coerce) import Data.Function (on) -import Data.List (foldl', nub) +import Data.List (foldl') import Data.List.Extra (unsnoc) import Data.Map (Map) import Data.Map qualified as M @@ -28,14 +28,6 @@ import Grammar.Print (printTree) import TypeChecker.TypeCheckerIr (T, T') import TypeChecker.TypeCheckerIr qualified as T -{- -TODO -Prettifying the types of generated variables does only need to be done when -presenting the types to the user, i.e, when the user has made a mistake. -For succesfully typed programs the types only need to match. - --} - -- | Type check a program typecheck :: Program -> Either String (T.Program' Type, [Warning]) typecheck = onLeft msg . run . checkPrg @@ -245,7 +237,7 @@ algoW = \case "does not match inferred type" quote $ printTree t' ) - let comp = sub1 `compose` sub0 + let comp = sub1 <> sub0 return (comp, (apply comp e', t)) -- \| ------------------ @@ -309,7 +301,7 @@ algoW = \case (s2, (e1', t1)) <- algoW e1 s3 <- exprErr (unify t0 int) err s4 <- exprErr (unify t1 int) err - let comp = s4 `compose` s3 `compose` s2 `compose` s1 + let comp = s4 <> s3 <> s2 <> s1 return ( comp , apply comp (T.EAdd (e0', t0) (e1', t1), int) @@ -327,7 +319,7 @@ algoW = \case (s1, (e1', t1)) <- algoW e1 s2 <- unify (apply s1 t0) (TFun t1 fr) let t = apply s2 fr - let comp = s2 `compose` s1 `compose` s0 + let comp = s2 <> s1 <> s0 return (comp, apply comp (T.EApp (e0', t0) (e1', t1), t)) -- \| Γ ⊢ e₀ : τ, S₀ S₀Γ, x : S̅₀Γ̅(τ) ⊢ e₁ : τ', S₁ @@ -344,7 +336,7 @@ algoW = \case let t' = generalize (apply s1 env) t0 withBinding (coerce name) t' $ do (s2, (e1', t2)) <- algoW e1 - let comp = s2 `compose` s1 + let comp = s2 <> s1 return ( comp , apply @@ -354,7 +346,7 @@ algoW = \case ECase caseExpr injs -> do (sub, (e', t)) <- algoW caseExpr (subst, injs, ret_t) <- checkCase t injs - let comp = subst `compose` sub + let comp = subst <> sub return (comp, apply comp (T.ECase (e', t) injs, ret_t)) checkCase :: Type -> [Branch] -> Infer (Subst, [T.Branch' Type], Type) @@ -367,18 +359,18 @@ checkCase expT brnchs = do (sub1, _) <- foldM ( \(sub, acc) x -> - (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc + (\a -> (a <> sub, a `apply` acc)) <$> unify x acc ) (nullSubst, expT) branchTs (sub2, returns_type) <- foldM ( \(sub, acc) x -> - (\a -> (a `compose` sub, a `apply` acc)) <$> unify x acc + (\a -> (a <> sub, a `apply` acc)) <$> unify x acc ) (nullSubst, head returns) (tail returns) - let comp = sub2 `compose` sub1 `compose` sub0 + let comp = sub2 <> sub1 <> sub0 return (comp, apply comp injs, apply comp returns_type) inferBranch :: Branch -> Infer (Subst, Type, T.Branch' Type, Type) @@ -463,7 +455,7 @@ unify t0 t1 = case (t0, t1) of (TFun a b, TFun c d) -> do s1 <- unify a c s2 <- unify (apply s1 b) (apply s1 d) - return $ s2 `compose` s1 + return $ s2 <> s1 (TVar a, t@(TData _ _)) -> return $ singleton a t (t@(TData _ _), TVar b) -> return $ singleton b t (TVar a, t) -> occurs a t @@ -575,7 +567,7 @@ fresh :: Infer Type fresh = do n <- gets count modify (\st -> st{count = succ (count st)}) - return $ TVar $ MkTVar $ LIdent $ show n + return . TVar . MkTVar . LIdent $ letters !! n -- Is the left more general than the right (<<=) :: Type -> Type -> Infer Bool @@ -730,13 +722,15 @@ instance SubstType (T T.Ident Type) where nullSubst :: Subst nullSubst = mempty --- | Compose two substitution sets +{- | Compose two substitution sets +The monoid instance of Subst uses this definition +-} compose :: Subst -> Subst -> Subst compose m1@(Subst m1') (Subst m2) = Subst $ M.map (apply m1) m2 `M.union` m1' -- | Compose a list of substitution sets into one composeAll :: [Subst] -> Subst -composeAll = foldl' compose nullSubst +composeAll = mconcat {- | Convert a function with arguments to its pointfree version > makeLambda (add x y = x + y) = add = \x. \y. x + y @@ -914,5 +908,5 @@ uncatchableErr msg = throwError $ Error msg False quote :: String -> String quote s = "'" ++ s ++ "'" -letters :: [T.Ident] -letters = map T.Ident $ [1 ..] >>= flip replicateM ['a' .. 'z'] +letters :: [String] +letters = [1 ..] >>= flip replicateM ['a' .. 'z'] diff --git a/src/TypeChecker/TypeCheckerIr.hs b/src/TypeChecker/TypeCheckerIr.hs index b7b1ef0..8dc0e57 100644 --- a/src/TypeChecker/TypeCheckerIr.hs +++ b/src/TypeChecker/TypeCheckerIr.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} module TypeChecker.TypeCheckerIr ( @@ -6,10 +6,10 @@ module TypeChecker.TypeCheckerIr ( module TypeChecker.TypeCheckerIr, ) where -import Data.String (IsString) -import Grammar.Abs (Lit (..)) -import Grammar.Print -import Prelude +import Data.String (IsString) +import Grammar.Abs (Lit (..)) +import Grammar.Print +import Prelude newtype Program' t = Program [Def' t] deriving (Eq, Ord, Show, Functor) @@ -58,8 +58,7 @@ newtype TVar = MkTVar Ident deriving (Eq, Ord, Show) type T' a t = (a t, t) -type T a t = (a, t) - +type T a t = (a, t) data Bind' t = Bind (T Ident t) [T Ident t] (T' Exp' t) deriving (Eq, Ord, Show, Functor) @@ -74,12 +73,13 @@ instance Print t => Print (Program' t) where prt i (Program sc) = prt i sc instance Print t => Print (Bind' t) where - prt i (Bind sig parms rhs) = concatD - [ prtSig sig - , prt i parms - , doc $ showString "=" - , prt i rhs - ] + prt i (Bind sig parms rhs) = + concatD + [ prtSig sig + , prt i parms + , doc $ showString "=" + , prt i rhs + ] prtSig :: Print t => T Ident t -> Doc prtSig (x, t) = @@ -93,17 +93,18 @@ instance (Print a, Print t) => Print (T a t) where prt i (x, t) = noT where noT = prt i x - withT = concatD - [ doc $ showString "(" - , prt i x - , doc $ showString ":" - , prt 0 t - , doc $ showString ")" - ] + withT = + concatD + [ doc $ showString "(" + , prt i x + , doc $ showString ":" + , prt 0 t + , doc $ showString ")" + ] instance Print t => Print [Bind' t] where - prt _ [] = concatD [] - prt i [x] = concatD [prt i x] + prt _ [] = concatD [] + prt i [x] = concatD [prt i x] prt i (x : xs) = concatD [prt i x, doc (showString ";"), prt i xs] instance Print t => Print (Exp' t) where @@ -121,13 +122,13 @@ instance Print t => Print (Branch' t) where prt i (Branch (pattern_, t) exp) = prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_, doc (showString " : "), prt 0 t, doc (showString ")"), doc (showString "=>"), prt 0 exp]) instance Print t => Print [Branch' t] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] instance Print t => Print (Def' t) where prt i = \case - DBind bind -> prPrec i 0 (concatD [prt 0 bind]) + DBind bind -> prPrec i 0 (concatD [prt 0 bind]) DData data_ -> prPrec i 0 (concatD [prt 0 data_]) instance Print t => Print (Data' t) where @@ -152,12 +153,12 @@ instance Print t => Print (Pattern' t) where PInj uident patterns -> prPrec i 0 (concatD [prt 0 uident, prt 1 patterns]) instance Print t => Print [Def' t] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x : xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] instance Print [Type] where - prt _ [] = concatD [] + prt _ [] = concatD [] prt _ (x : xs) = concatD [prt 0 x, doc (showString " "), prt 0 xs] instance Print Type where