added PEnum

Grammar.cf

@@ -66,26 +66,28 @@ LChar. Lit ::= Char ;
 
 Branch. Branch ::= Pattern "=>" Exp ;
 
-PVar.   Pattern ::= LIdent ;
+PVar.   Pattern1 ::= LIdent ;
-PLit.   Pattern ::= Lit ;
+PLit.   Pattern1 ::= Lit ;
-PInj.   Pattern ::= UIdent [Pattern] ;
+PCatch. Pattern1 ::= "_" ;
-PCatch. Pattern ::= "_" ;
+PEnum. Pattern1 ::= UIdent ;
+PInj.   Pattern ::= UIdent [Pattern1] ;
 
 -------------------------------------------------------------------------------
 -- * AUX
 -------------------------------------------------------------------------------
 
-separator Def ";" ;
+terminator Def ";" ;
 separator nonempty Constructor "" ;
 separator Type " " ;
-separator Pattern " " ;
+separator nonempty Pattern1 " " ;
-separator Branch "," ;
+terminator Branch ";" ;
 separator Ident " ";
 separator LIdent " ";
 separator TVar " " ;
 
 coercions Exp 4 ;
 coercions Type 2 ;
+coercions Pattern 1 ;
 
 token UIdent (upper (letter | digit | '_')*) ;
 token LIdent (lower (letter | digit | '_')*) ;

sample-programs/basic-9

@@ -0,0 +1,14 @@
+data List (a) where {
+  Nil  : List (a)
+  Cons : a -> List (a) -> List (a)
+};
+
+test xs = case xs of {
+    Cons Nil _ => 0 ;
+};
+
+
+
+List a /= List (List a)
+
+a /= List a

src/TypeChecker/TypeChecker.hs

@@ -562,6 +562,7 @@ withPattern p ma = case p of
     T.PInj _ ps -> foldl' (flip withPattern) ma ps
     T.PLit _ -> ma
     T.PCatch -> ma
+    T.PEnum _ -> ma
 
 inferPattern :: Pattern -> Infer (T.Pattern, T.Type)
 inferPattern = \case
@@ -574,6 +575,10 @@ inferPattern = \case
         zipWithM_ unify vs (map snd patterns)
         return (T.PInj (coerce constr) (map fst patterns), ret)
     PCatch -> (T.PCatch,) <$> fresh
+    PEnum p -> do
+        t <- gets (M.lookup (coerce p) . constructors)
+        t <- maybeToRightM ("Constructor: " <> printTree p <> " does not exist") t
+        return (T.PEnum $ coerce p, t)
     PVar x -> do
         fr <- fresh
         let pvar = T.PVar (coerce x, fr)

src/TypeChecker/TypeCheckerIr.hs

@@ -64,7 +64,7 @@ type ExpT = (Exp, Type)
 data Branch = Branch (Pattern, Type) ExpT
     deriving (C.Eq, C.Ord, C.Read, C.Show)
 
-data Pattern = PVar Id | PLit (Lit, Type) | PInj Ident [Pattern] | PCatch
+data Pattern = PVar Id | PLit (Lit, Type) | PInj Ident [Pattern] | PCatch | PEnum Ident
     deriving (C.Eq, C.Ord, C.Show, C.Read)
 
 data Def = DBind Bind | DData Data

test_program

@@ -12,30 +12,32 @@ 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
+    Cons x xs => length xs;
 };
 
 head : List (a) -> a ;
 head xs = case xs of {
-    Cons x xs => x
+    Cons x xs => x;
 };
 
 firstIsOne : List (Int) -> Bool () ;
 firstIsOne xs = case xs of {
     Cons x xs => case x of {
-            0 => True ,
+            0 => True;
             _ => case xs of {
-                    Cons x xs => False ,
+                    Cons x xs => False;
-                    _ => False
+                    _ => False;
-                }
+                };
-            },
+            };
-    _ => False
+    _ => False;
     };
 
 main = firstIsOne (Cons 1 Nil);
 
 deepPat xs = case xs of {
-    Cons 1 _ => True ,
+    Cons (Nil) _ => True;
-    _        => False
+    _                 => False;
-                        }
+                        };
+
+