diff --git a/src/Main.hs b/src/Main.hs index cff33f7..6aa4dad 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -155,6 +155,7 @@ main' opts s = when check (removeDirectoryRecursive "output") createDirectory "output" createDirectory "output/logs" + when opts.logIL (writeFile "output/logs/tc.log" (printTree typechecked)) when opts.debug $ do printToErr "\n -- Compiler --" writeFile "output/llvm.ll" generatedCode diff --git a/src/TypeChecker/TypeCheckerHm.hs b/src/TypeChecker/TypeCheckerHm.hs index 6564b8b..7e50d06 100644 --- a/src/TypeChecker/TypeCheckerHm.hs +++ b/src/TypeChecker/TypeCheckerHm.hs @@ -2,7 +2,6 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QualifiedDo #-} -{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- | A module for type checking and inference using algorithm W, Hindley-Milner module TypeChecker.TypeCheckerHm where @@ -17,10 +16,8 @@ import Control.Monad.Writer import Data.Coerce (coerce) import Data.Function (on) import Data.List (foldl') -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 Grammar.Abs @@ -333,7 +330,7 @@ algoW = \case withBinding (coerce name) fr $ do (s1, e@(_, t0)) <- algoW (makeLambda e (coerce args)) env <- asks vars - let t' = generalize (apply s1 env) t0 + let t' = generalize (apply s1 (M.elems env)) t0 withBinding (coerce name) t' $ do (s2, (e1', t2)) <- algoW e1 let comp = s2 <> s1 @@ -355,6 +352,7 @@ checkCase _ [] = do return (nullSubst, [], fr) checkCase expT brnchs = do (subs, branchTs, injs, returns) <- unzip4 <$> mapM inferBranch brnchs + -- compose all probably wrong let sub0 = composeAll subs (sub1, _) <- foldM @@ -431,8 +429,7 @@ inferPattern = \case ) t let numArgs = typeLength t - 1 - let (vs, ret) = fromJust (unsnoc $ flattenType t) - patterns <- mapM inferPattern patterns + (pats, typs) <- mapAndUnzipM inferPattern patterns unless (length patterns == numArgs) ( catchableErr $ Aux.do @@ -443,10 +440,11 @@ inferPattern = \case " arguments but has been given " show (length patterns) ) - sub <- composeAll <$> zipWithM unify vs (map snd patterns) + fr <- fresh + sub <- unify t (foldr TFun fr typs) return - ( T.PInj (coerce constr) (apply sub patterns) - , apply sub ret + ( T.PInj (coerce constr) (apply sub $ zip pats typs) + , apply sub fr ) -- | Unify two types producing a new substitution @@ -485,15 +483,6 @@ unify t0 t1 = case (t0, t1) of "does not match with:" printTree name' quote $ printTree t' - (TEVar a, TEVar b) -> - if a == b - then return nullSubst - else catchableErr $ - Aux.do - "Can not unify" - quote $ printTree (TEVar a) - "with" - quote $ printTree (TEVar b) (a, b) -> do catchableErr $ Aux.do @@ -507,7 +496,6 @@ I.E. { a = a -> b } is an unsolvable constraint since there is no substitution where these are equal -} occurs :: TVar -> Type -> Infer Subst -occurs i t@(TEVar _) = return (singleton i t) occurs i t@(TVar _) = return (singleton i t) occurs i t | S.member i (free t) = @@ -526,7 +514,7 @@ occurs i t Type checks: let f = \x. x in (f True, f 'a') Does not type check: (\f. (f True, f 'a')) (\x. x) -} -generalize :: Map T.Ident Type -> Type -> Type +generalize :: [Type] -> Type -> Type generalize env t = go (S.toList $ free t S.\\ free env) (removeForalls t) where go :: [TVar] -> Type -> Type @@ -570,6 +558,7 @@ fresh = do return . TVar . MkTVar . LIdent $ letters !! n -- Is the left more general than the right +-- TODO: A bug might exist (<<=) :: Type -> Type -> Infer Bool (<<=) a b = case (a, b) of (TVar _, _) -> return True @@ -592,7 +581,6 @@ fresh = do where go :: [TVar] -> Type -> Type -> Infer Bool go tvars t1 t2 = do - -- probably not necessary freshies <- mapM (const fresh) tvars let sub = Subst . M.fromList $ zip tvars freshies let t1' = apply sub t1 @@ -638,7 +626,6 @@ instance FreeVars Type where free (TLit _) = mempty free (TFun a b) = free a `S.union` free b free (TData _ a) = free a - free (TEVar _) = S.empty instance FreeVars a => FreeVars [a] where free = let f acc x = acc `S.union` free x in foldl' f S.empty @@ -656,9 +643,6 @@ instance SubstType Type where Just _ -> apply sub t TFun a b -> TFun (apply sub a) (apply sub b) TData name a -> TData name (apply sub a) - TEVar (MkTEVar a) -> case find (MkTVar a) sub of - Nothing -> TEVar (MkTEVar $ coerce a) - Just t -> t instance FreeVars (Map T.Ident Type) where free :: Map T.Ident Type -> Set TVar diff --git a/test_program.crf b/test_program.crf index 06dfee3..13ea2cf 100644 --- a/test_program.crf +++ b/test_program.crf @@ -1,6 +1,34 @@ -main = sigma 0 10 +data Maybe a where + Nothing : Maybe a + Just : a -> Maybe a + +data Either a b where + Left : a -> Either a b + Right : b -> Either a b + +data List a where + Nil : List a + Cons : a -> List a -> List a + +data Foo a where + Foo : List a -> Foo a + +data Bar a where + Bar : Foo a -> Bar a + +test = \x . case x of + Left (Just (Bar (Foo (Cons 1 Nil)))) => 1 + _ => 0 + +main = 0 + +-- pattern1 = PInj (UIdent "Foo") [PInj (UIdent "Cons") [PLit (LInt 1), PEnum (UIdent "Nil")]] +-- env = Env { sigs = mempty, count = 0, nextChar = 'a', declaredBinds = mempty, takenTypeVars = mempty, injections = M.insert (T.Ident "Foo") (TFun list foo) $ M.insert (T.Ident "Nil") list $ M.singleton (T.Ident "Cons") (TFun a (TFun list list))} +-- list = TData (UIdent "List") [a] +-- foo = TData (UIdent "Foo") [a] +-- a = TVar $ MkTVar "a" +-- pattern2 = PInj (UIdent "Foo") [PInj (UIdent "Cons") [PLit (LInt 1),PEnum (UIdent "Nil")]] + +-- (snd . fst) <$> run' env initCtx (inferPattern pattern1) +-- (snd . fst) <$> run' env initCtx (inferPattern pattern2) -sigma : Int -> Int -> Int -sigma from to = case from == to of - True => from - False => to + sigma from (to - 1)