about summary refs log tree commit diff
path: root/src/Typecheck.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Typecheck.hs')
-rw-r--r--src/Typecheck.hs63
1 files changed, 60 insertions, 3 deletions
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 ()
+  
+