new good version works

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 | '_')*) ;

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)

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

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

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
+                        }

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