Fix variants typing, add wellformedness for commands

2 files changed, 63 insertions, 6 deletions

diff --git a/src/Syntax.hs b/src/Syntax.hs
index bbd8cbe..f5d9c2d 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -17,7 +17,7 @@ data Expr = Var Idnt
           | Mult Expr Expr
           | Neg Expr
           | Deref Expr
-          | Match Expr [(Idnt, Expr)]
+          | Match Expr [(Idnt, Idnt, Expr)] -- Variant,Binder, Expression
           | Proj Idnt Expr 
            deriving(Eq,Show)
 data Com = Skip
@@ -26,9 +26,9 @@ data Com = Skip
          | While Expr Com
          | Asgn Idnt Expr
          | Decl Idnt Expr Com
-         | Alloc Idnt Expr
+         | Alloc Idnt Expr Com
          | Save Idnt Expr
-         | SMatch Expr [(Idnt, Expr)]
+         | SMatch Expr [(Idnt, Idnt, Com)]
            deriving(Eq,Show)
          
 data FuncDecl = Func Idnt [Idnt] [(Idnt,Expr)] Com Expr
diff --git a/src/Typecheck.hs b/src/Typecheck.hs
index 2ed189d..d8c0187 100644
--- a/src/Typecheck.hs
+++ b/src/Typecheck.hs
@@ -2,7 +2,9 @@
 module Typecheck
 (inferExpr,
  checkExpr,
- Environment)
+ wellFormed,
+ Environment,
+ )
   where
 import Syntax
 --import Control.Monad
@@ -32,6 +34,13 @@ envlookup name env expr = case lookup name env of
   Just t -> return t
   Nothing -> throwError $ "Variable "++ name ++ "not defined in expr" ++ show expr
 
+insert :: Idnt -> Typ -> Environment -> TypeDict
+insert v t l = (v,t):l
+
+subset ::Show a=> [Idnt] -> [Idnt]-> a -> Error ()
+subset [] _ _= return ()
+subset (x:xs) l a= if x `elem` l then subset xs l a else throwError $ "Case "++ show x ++ "not checked in case/match" ++ show a
+
 inferExpr :: Expr -> Environment -> Error Typ
 inferExpr e@(Var name) env = envlookup name env e
 inferExpr (IntLit _) _ = return TInt
@@ -61,8 +70,10 @@ inferExpr (Deref e1) env = do
 inferExpr c@(Match e cases) env = do
   varType <- inferExpr e env
   variants <- assertVar varType e
-  -- TODO ensure variants and cases cover the same names
-  caseTypes <- mapM (\(v,e) ->(v,) <$> inferExpr e env) cases
+  caseTypes <- mapM (\(v,bind,e) ->(v,) <$> do
+                        tt <- envlookup v variants e
+                        inferExpr e (insert bind tt env)) cases
+  subset (map fst variants) (map (\(_,v,_)->v) cases) c
   ret <- allSame caseTypes
   return $ snd ret
   where
@@ -99,3 +110,49 @@ checkExpr e env t = do
   if t == t' then return ()
     else throwError $ "Expected type of expression " ++
          show e ++ " to be"++ show t  ++" instead got" ++ show t'
+
+bool = TVariant [("True",TRecord []),("False", TRecord [])]
+  
+cenvlookup :: Idnt -> TypeDict -> Com -> Error Typ
+cenvlookup name env c = case lookup name env of
+  Just t -> return t
+  Nothing -> throwError $ "Variable "++ name ++ "not defined in expr" ++ show c
+
+wellFormed :: Com ->Environment -> Error ()
+wellFormed Skip _= return ()
+wellFormed (Seq s1 s2) env = do
+  wellFormed s1 env
+  wellFormed s2 env
+wellFormed (If e c1 c2) env = do
+  checkExpr e env bool
+  wellFormed c1 env
+  wellFormed c2 env
+wellFormed (While e c) env = do
+  checkExpr e env bool
+  wellFormed c env
+wellFormed c@(Asgn v e) env = do
+  vt <- cenvlookup v env c
+  et <- inferExpr e env
+  if vt==et then return ()
+    else throwError $ "Variable " ++ show v ++ "::" ++ show vt ++ " was assigned expression " ++ show e ++ "::" ++ show et
+wellFormed (Decl v e c) env= do
+  et <- inferExpr e env
+  wellFormed c (insert v et env)
+wellFormed (Alloc v e c) env = do
+  et <- inferExpr e env
+  wellFormed c (insert v (TPtr et) env)
+wellFormed c@(Save v e) env = do
+  vt <- cenvlookup v env c
+  et <- inferExpr e env
+  if vt==TPtr et then return ()
+    else throwError $ "Expression" ++ show e ++ "::" ++ show et ++ " was saved to pointer "++show v ++ " of type" ++ show vt
+wellFormed c@(SMatch e cases) env = do
+  varType <- inferExpr e env
+  variants <- assertVar varType e
+  mapM (\(v,bind,c) -> do
+                        tt <- envlookup v variants e
+                        wellFormed c (insert bind tt env)) cases
+  subset (map fst variants) (map (\(_,v,_)->v) cases) c
+  return ()
+  
+