From 3c2cb1a713a023d90a15161b63392ac73f775357 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Fri, 24 Mar 2023 17:06:32 +0100 Subject: [PATCH] new good version works --- Grammar.cf | 12 +++++------ src/Main.hs | 3 ++- src/Renamer/Renamer.hs | 37 +++++++++++++++++++++------------- src/TypeChecker/TypeChecker.hs | 31 +++++++++++++++++++--------- test_program | 21 +++++++++---------- tests/Tests.hs | 2 +- 6 files changed, 63 insertions(+), 43 deletions(-) diff --git a/Grammar.cf b/Grammar.cf index b0a7a4c..51ff54b 100644 --- a/Grammar.cf +++ b/Grammar.cf @@ -43,11 +43,11 @@ Data. Data ::= "data" Type "where" "{" [Constructor] "}" ; -- * EXPRESSIONS ------------------------------------------------------------------------------- -EAnn. Exp5 ::= "(" Exp ":" Type ")" ; -EVar. Exp4 ::= LIdent ; -EInj. Exp4 ::= UIdent ; -ELit. Exp4 ::= Lit ; -EApp. Exp3 ::= Exp3 Exp4 ; +EAnn. Exp4 ::= "(" Exp ":" Type ")" ; +EVar. Exp3 ::= LIdent ; +EInj. Exp3 ::= UIdent ; +ELit. Exp3 ::= Lit ; +EApp. Exp2 ::= Exp2 Exp3 ; EAdd. Exp1 ::= Exp1 "+" Exp2 ; ELet. Exp ::= "let" Bind "in" Exp ; EAbs. Exp ::= "\\" LIdent "." Exp ; @@ -84,7 +84,7 @@ separator Ident " "; separator LIdent " "; separator TVar " " ; -coercions Exp 5 ; +coercions Exp 4 ; coercions Type 2 ; token UIdent (upper (letter | digit | '_')*) ; diff --git a/src/Main.hs b/src/Main.hs index d8ecdd6..7ae149b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -7,7 +7,8 @@ import GHC.IO.Handle.Text (hPutStrLn) import Grammar.ErrM (Err) import Grammar.Par (myLexer, pProgram) import Grammar.Print (printTree) -import Monomorphizer.Monomorphizer (monomorphize) + +-- import Monomorphizer.Monomorphizer (monomorphize) import Control.Monad (when) import Data.List.Extra (isSuffixOf) diff --git a/src/Renamer/Renamer.hs b/src/Renamer/Renamer.hs index c550a92..5576793 100644 --- a/src/Renamer/Renamer.hs +++ b/src/Renamer/Renamer.hs @@ -2,11 +2,15 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Use mapAndUnzipM" #-} module Renamer.Renamer (rename) where import Auxiliary (mapAccumM) import Control.Applicative (Applicative (liftA2)) +import Control.Monad (foldM) import Control.Monad.Except (ExceptT, MonadError, runExceptT, throwError) import Control.Monad.Identity (Identity, runIdentity) import Control.Monad.State ( @@ -102,7 +106,7 @@ type Names = Map LIdent LIdent renameExp :: Names -> Exp -> Rn (Names, Exp) renameExp old_names = \case EVar n -> pure (coerce old_names, EVar . fromMaybe n $ Map.lookup n old_names) - ECons n -> pure (old_names, ECons n) + EInj n -> pure (old_names, EInj n) ELit lit -> pure (old_names, ELit lit) EApp e1 e2 -> do (env1, e1') <- renameExp old_names e1 @@ -128,27 +132,32 @@ renameExp old_names = \case pure (new_names, EAnn e' t') ECase e injs -> do (new_names, e') <- renameExp old_names e - (new_names', injs') <- renameInjs new_names injs + (new_names', injs') <- renameBranches new_names injs pure (new_names', ECase e' injs') -renameInjs :: Names -> [Inj] -> Rn (Names, [Inj]) -renameInjs ns xs = do - (new_names, xs') <- unzip <$> mapM (renameInj ns) xs +renameBranches :: Names -> [Branch] -> Rn (Names, [Branch]) +renameBranches ns xs = do + (new_names, xs') <- unzip <$> mapM (renameBranch ns) xs if null new_names then return (mempty, xs') else return (head new_names, xs') -renameInj :: Names -> Inj -> Rn (Names, Inj) -renameInj ns (Inj init e) = do - (new_names, init') <- renameInit ns init +renameBranch :: Names -> Branch -> Rn (Names, Branch) +renameBranch ns (Branch init e) = do + (new_names, init') <- renamePattern ns init (new_names', e') <- renameExp new_names e - return (new_names', Inj init' e') + return (new_names', Branch init' e') -renameInit :: Names -> Init -> Rn (Names, Init) -renameInit ns i = case i of - InitConstructor cs vars -> do - (ns_new, vars') <- newNames ns (coerce vars) - return (ns_new, InitConstructor cs (coerce vars')) +renamePattern :: Names -> Pattern -> Rn (Names, Pattern) +renamePattern ns i = case i of + PInj cs ps -> do + (ns_new, ps) <- renamePatterns ns ps + return (ns_new, PInj cs ps) rest -> return (ns, rest) +renamePatterns :: Names -> [Pattern] -> Rn (Names, [Pattern]) +renamePatterns ns xs = do + (new_names, xs') <- unzip <$> mapM (renamePattern ns) xs + if null new_names then return (mempty, xs') else return (head new_names, xs') + renameTVars :: Type -> Rn Type renameTVars typ = case typ of TAll tvar t -> do diff --git a/src/TypeChecker/TypeChecker.hs b/src/TypeChecker/TypeChecker.hs index 5b22999..e10023c 100644 --- a/src/TypeChecker/TypeChecker.hs +++ b/src/TypeChecker/TypeChecker.hs @@ -528,7 +528,7 @@ insertConstr i t = checkCase :: T.Type -> [Branch] -> Infer (Subst, [T.Branch], T.Type) checkCase expT injs = do - (injTs, injs, returns) <- unzip3 <$> mapM checkBranch injs + (injTs, injs, returns) <- unzip3 <$> mapM inferBranch injs (sub1, _) <- foldM ( \(sub, acc) x -> @@ -549,22 +549,35 @@ checkCase expT injs = do | snd = type of expr -} inferBranch :: Branch -> Infer (T.Type, T.Branch, T.Type) -inferBranch (Branch it expr) = do - (initT, vars) <- inferPattern it - (e, exprT) <- withBindings vars (inferExp expr) - return (initT, T.Branch (it, initT) (e, exprT), exprT) +inferBranch (Branch pat expr) = do + newPat@(pat, branchT) <- inferPattern pat + newExp@(_, exprT) <- withPattern pat (inferExp expr) + return (branchT, T.Branch newPat newExp, exprT) + +-- return (initT, T.Branch (it, initT) (e, exprT), exprT) + +withPattern :: T.Pattern -> Infer a -> Infer 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 inferPattern :: Pattern -> Infer (T.Pattern, T.Type) inferPattern = \case - PLit lit -> return (T.PLit $ toNew lit, litType lit) + PLit lit -> let lt = litType lit in return (T.PLit (toNew lit, lt), lt) PInj constr patterns -> do t <- gets (M.lookup (coerce constr) . constructors) t <- maybeToRightM ("Constructor: " <> printTree constr <> " does not exist") t - (vs, ret) <- maybeToRightM (throwError "Partial pattern match not allowed") (unsnoc $ flattenType t) + (vs, ret) <- maybeToRightM "Partial pattern match not allowed" (unsnoc $ flattenType t) patterns <- mapM inferPattern patterns - undefined + zipWithM_ unify vs (map snd patterns) + return (T.PInj (coerce constr) (map fst patterns), ret) PCatch -> (T.PCatch,) <$> fresh - PVar x -> undefined + PVar x -> do + fr <- fresh + let pvar = T.PVar (coerce x, fr) + return (pvar, fr) flattenType :: T.Type -> [T.Type] flattenType (T.TFun a b) = flattenType a <> flattenType b diff --git a/test_program b/test_program index 28cd227..0543b88 100644 --- a/test_program +++ b/test_program @@ -12,7 +12,7 @@ hello_world = Cons 'h' (Cons 'e' (Cons 'l' (Cons 'l' (Cons 'o' (Cons ' ' (Cons ' length : List (a) -> Int ; length xs = case xs of { - Nil => 0 ; + Nil => 0, Cons x xs => length xs }; @@ -21,24 +21,21 @@ head xs = case xs of { Cons x xs => x }; -firstIsOne : List (Int) -> Bool () ; firstIsOne : List (Int) -> Bool () ; firstIsOne xs = case xs of { Cons x xs => case x of { - 1 => True ; + 0 => True , _ => case xs of { - Cons x xs => False ; + Cons x xs => False , _ => False } - }; + }, _ => False }; -firstIsOne :: [Int] -> Bool -firstIsOne xs = case xs of - (1 : xs) -> True - _ -> False +main = firstIsOne (Cons 1 Nil); -main = firstIsOne (Cons 'a' Nil) - -data a -> b where +deepPat xs = case xs of { + Cons 1 _ => True , + _ => False + } diff --git a/tests/Tests.hs b/tests/Tests.hs index 9c5649f..bba6216 100644 --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -61,7 +61,7 @@ infer_eid = describe "algoW used on EVar" $ do property $ \x -> do let env = Env 0 mempty mempty let t = T.TVar $ T.MkTVar "a" - let ctx = Ctx (M.singleton (Ident (x :: String)) t) + let ctx = Ctx (M.singleton (T.Ident (x :: String)) t) getTypeC env ctx (EVar (LIdent x)) `shouldBe` Right (T.TVar $ T.MkTVar "a") infer_eabs = describe "algoW used on EAbs" $ do