variant type errorlist, continue after failure and type argument elimination transformation

haskell/src/SumTypes/ContinueAfterCheckFail.hs

@@ -6,6 +6,7 @@ module SumTypes.ContinueAfterCheckFail where
 
 import Prelude hiding (Monad(..), (>=), (<=), lookup)
 import GHC.Exts (Constraint)
+import qualified Data.Map as Map
 
 import SumTypes.Language
 import Util.ErrorMessages
@@ -42,6 +43,8 @@ instance WithTop () where
 instance (WithTop a, WithTop b) => WithTop (a, b) where
   top = (top, top)
 
+instance (WithTop v) => WithTop (Map.Map Name v) where
+  top = Map.empty
 
 -- Had to define an own monad type class.
 -- It is not possible otherwise to get the type constraint WithTop a.
@@ -85,6 +88,14 @@ matchSum :: Type -> String -> Infer (Type, Type)
 matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
 matchSum ty err = fail [sumError ty err]
 
+matchVariant :: Type -> String -> Infer (Map.Map Name Type)
+matchVariant (Variant types) _ = return types
+matchVariant ty err = fail [variantError ty err]
+
+liftMaybe :: WithTop a => Maybe a -> String -> Infer a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail [err]
+
 lookup :: Ctx -> Name -> Infer Type
 lookup Empty x = fail ["Unbound variable " ++ show x]
 lookup (Bind c x t) y | x == y = return t
@@ -132,6 +143,19 @@ checkType ctx p@(Case e n1 t1 n2 t2 _) ty = do
   (ty1, ty2) <- matchSum ety (show e)
   checkType (Bind ctx n1 ty1) t1 ty
   checkType (Bind ctx n2 ty2) t2 ty
+checkType ctx p@(Tag n t _) ty = do
+  types <- matchVariant ty (show p)
+  lty <- liftMaybe (Map.lookup n types) "Label not contained in Variant"
+  checkType ctx t lty
+checkType ctx p@(Match m cases _) ty = do
+  ety <- inferType ctx m
+  types <- matchVariant ety (show m)
+  let subchecks =
+        map (\(l, x, t) -> do
+          lty <- liftMaybe (Map.lookup l types) "Could not find labeled type"
+          checkType (Bind ctx x lty) t ty
+        ) cases
+  foldl (>>) (return ()) subchecks
 checkType ctx t ty = do
   ty' <- inferType ctx t
   matchType ty ty' (show t)

haskell/src/SumTypes/EliminateTypeArgumentOfCheck.hs

@@ -6,6 +6,7 @@ module SumTypes.EliminateTypeArgumentOfCheck where
 
 import Prelude hiding (Monad(..), (>=), (<=), lookup)
 import GHC.Exts (Constraint)
+import qualified Data.Map as Map
 
 import SumTypes.Language
 import Util.ErrorMessages
@@ -42,6 +43,9 @@ instance WithTop () where
 instance (WithTop a, WithTop b) => WithTop (a, b) where
   top = (top, top)
 
+instance (WithTop v) => WithTop (Map.Map Name v) where
+  top = Map.empty
+
 -- Had to define an own monad type class.
 -- It is not possible otherwise to get the type constraint WithTop a.
 -- We use the extension ConstraintKinds to support this.
@@ -76,13 +80,21 @@ matchFun :: Type -> String -> Infer (Type, Type)
 matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
 matchFun ty err = fail [funError ty err]
 
+matchType :: Type -> Type -> String -> Check
+matchType ty1 ty2 _ | ty1 >= ty2 = return ()
+matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
+
 matchSum :: Type -> String -> Infer (Type, Type)
 matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
 matchSum ty err = fail [sumError ty err]
 
-matchType :: Type -> Type -> String -> Check
-matchType ty1 ty2 _ | ty1 >= ty2 = return ()
-matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
+matchVariant :: Type -> String -> Infer (Map.Map Name Type)
+matchVariant (Variant types) _ = return types
+matchVariant ty err = fail [variantError ty err]
+
+liftMaybe :: WithTop a => Maybe a -> String -> Infer a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail [err]
 
 lookup :: Ctx -> Name -> Infer Type
 lookup Empty x = fail ["Unbound variable " ++ show x]
@@ -136,7 +148,22 @@ checkType ctx p@(Case e n1 t1 n2 t2 _) = do
   ty <- requiredType ctx p
   checkType (Bind ctx n1 ty1) t1
   checkType (Bind ctx n2 ty2) t2
-
+checkType ctx p@(Tag n t _) = do
+  ty <- requiredType ctx p
+  types <- matchVariant ty (show p)
+  let lty = Map.lookup n types
+  lty <- liftMaybe (Map.lookup n types) "Label not contained in Variant"
+  checkType ctx t
+checkType ctx p@(Match m cases _) = do
+  ety <- inferType ctx m
+  types <- matchVariant ety (show m)
+  ty <- requiredType ctx p
+  let subchecks =
+        map (\(l, x, t) -> do
+          lty <- liftMaybe (Map.lookup l types) "Could not find labeled type"
+          checkType (Bind ctx x lty) t
+        ) cases
+  foldl (>>) (return ()) subchecks
 checkType ctx t = do
   ty <- requiredType ctx t
   ty' <- inferType ctx t
@@ -183,4 +210,11 @@ requiredType ctx t = case parent t of
     (ty1, ty2) <- matchSum ety (show e)
     ty <- requiredType ctx' p
     return ty
+  Just p@(Tag n t' _) | t == t' -> do
+    ty <- requiredType ctx p
+    types <- matchVariant ty (show p)
+    liftMaybe (Map.lookup n types) "Label not contained in Variant"
+  Just p@(Match m cases _) -> do
+    ty <- requiredType ctx p
+    return ty
   _ -> fail ["Could not determine required type"]

haskell/src/SumTypes/ErrorList.hs

@@ -2,6 +2,7 @@ module SumTypes.ErrorList where
 
 import Prelude hiding (lookup, Ord)
 import Data.List(find)
+import qualified Data.Map as Map
 
 import SumTypes.Language
 import Util.ErrorMessages
@@ -44,6 +45,14 @@ matchSum :: Type -> String -> Infer (Type, Type)
 matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
 matchSum ty err = fail $ sumError ty err
 
+matchVariant :: Type -> String -> Infer (Map.Map Name Type)
+matchVariant (Variant types) _ = return types
+matchVariant ty err = fail $ variantError ty err
+
+liftMaybe :: Monad m => Maybe a -> String -> m a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail err
+
 lookup :: Ctx -> Name -> Infer Type
 lookup Empty x = fail $ "Unbound variable " ++ show x
 lookup (Bind c x t) y | x == y = return t
@@ -91,6 +100,19 @@ checkType ctx p@(Case e n1 t1 n2 t2 _) ty = do
   (ty1, ty2) <- matchSum ety (show e)
   checkType (Bind ctx n1 ty1) t1 ty
   checkType (Bind ctx n2 ty2) t2 ty
+checkType ctx p@(Tag n t _) ty = do
+  types <- matchVariant ty (show p)
+  let lty = Map.lookup n types
+  (maybe (fail "") (checkType ctx t) lty)
+checkType ctx p@(Match m cases _) ty = do
+  ety <- inferType ctx m
+  types <- matchVariant ety (show m)
+  let subchecks =
+        map (\(l, x, t) -> do
+          lty <- liftMaybe (Map.lookup l types) "Could not find labeled type"
+          checkType (Bind ctx x lty) t ty
+        ) cases
+  foldl (>>) (return ()) subchecks
 checkType ctx t ty = do
   ty' <- inferType ctx t
   matchType ty ty' (show t)