eliminating type argument of check (harder to do because of complex program slice)

haskell/src/ADTypes/ContinueAfterFail.hs

@@ -182,10 +182,10 @@ inferType ctx tymap (Cotr n ts p) = do
   if length ts == length tys
   then do
     -- check types accordingly to definition
-    let subchecks = zipWith (\t ty -> do
+    let subchecks = map (\(t, ty) -> do
           ty' <- matchTypeVar tymap ty
           checkType ctx tymap t ty'
-          ) ts tys -- basically a map over the [(Term, Type)] and apply check ctx
+          ) (zip ts tys) -- basically a map over the [(Term, Type)] and apply check ctx
     foldl (>>) (return ()) subchecks
     return adty
   else fail ["Expected number of arguments violated for " ++ show (Cotr n ts p)]

haskell/src/ADTypes/EliminateTypeArgumentOfCheck.hs

+
+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RebindableSyntax #-}
+module ADTypes.EliminateTypeArgumentOfCheck where
+
+import Prelude hiding (Monad(..), (>=), (<=), lookup)
+import GHC.Exts (Constraint)
+import qualified Data.Map as M
+import Data.Maybe
+import Data.List(find)
+import ADTypes.Language
+import Util.ErrorMessages
+import Util.PartialOrd
+
+-- is needed because we use the RebindableSyntax extension
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True thn _ = thn
+ifThenElse False _ els = els
+
+type Error = [String]
+
+data Infer a
+  = Inferred a
+  | NotInferred Error deriving (Eq, Show)
+
+type Check = Infer ()
+
+instance Functor Infer where
+  fmap _ (NotInferred err) = NotInferred err
+  fmap f (Inferred ty) = Inferred $ f ty
+
+instance Applicative Infer where
+  pure = Inferred
+  (NotInferred err) <*> _ = NotInferred err
+  (Inferred a) <*> something = fmap a something
+
+class WithTop a where
+  top :: a
+
+instance WithTop Type where
+  top = AnyType
+
+instance WithTop () where
+  top = ()
+
+instance WithTop Char where
+  top = '_'
+
+instance (WithTop a, WithTop b) => WithTop (a, b) where
+  top = (top, top)
+
+instance (WithTop a) => WithTop [a] where
+  top = [top]
+
+instance (WithTop v) => WithTop (M.Map Name v) where
+  top = M.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.
+-- Could not find a simpler solution for this problem.
+-- The restricted monad problem is common.
+class RMonad m where
+  type RMonadCtx m a :: Constraint
+  return :: RMonadCtx m a => a -> m a
+  (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
+  (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a ->  m b -> m b
+  m >> k = m >>= \_ -> k
+  fail :: [String] -> m a
+
+instance RMonad Infer where
+  type RMonadCtx Infer a = WithTop a
+  return = Inferred
+  (Inferred ty) >>= f = f ty
+  NotInferred err1 >>= f =
+    -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
+    case f top of
+      Inferred _ -> fail err1
+      NotInferred err2 -> fail $ err1 ++ err2
+  fail = NotInferred
+
+-- matching functions that extract the inner types if possible
+matchNat :: Type -> String -> Check
+matchNat Nat _ = return ()
+matchNat ty err = fail [natError ty err]
+
+matchBool :: Type -> String -> Check
+matchBool Bool _ = return ()
+matchBool ty err = fail [boolError ty err]
+
+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]
+
+
+matchADT :: Type -> String -> Infer (Name, M.Map Name [Type])
+matchADT (ADT n cotrs) _ = return (n, cotrs)
+matchADT ty err = fail [sumError ty err]
+
+liftMaybe :: WithTop a => Maybe a -> String -> Infer a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail [err]
+
+lookupVar :: Ctx -> Name -> Infer Type
+lookupVar Empty x = fail ["Unbound variable " ++ show x]
+lookupVar (Bind c x t) y
+  | x == y = return t
+  | otherwise = lookupVar c y
+
+lookupTypeVar :: TypeMap -> Name -> Infer Type
+lookupTypeVar Empty x = fail ["Unbound type variable " ++ show x]
+lookupTypeVar (Bind c x t) y
+  | x == y = return t
+  | otherwise = lookupTypeVar c y
+
+matchTypeVar :: TypeMap -> Type -> Infer Type
+matchTypeVar tymap (TypeVar x) = lookupTypeVar tymap x
+matchTypeVar _ ty = return ty
+
+lookupCotr :: TypeMap -> Name -> Infer (Type, [Type])
+lookupCotr Empty x = fail ["Unbound constructor " ++ show x]
+lookupCotr (Bind c x ty) y = case ty of
+  t@(ADT n cotrs) ->
+    let mayCotr = M.lookup y cotrs in
+    if isJust mayCotr
+    then return (t, fromJust mayCotr)
+    else lookupCotr c y
+  _ -> lookupCotr c y
+
+
+inferType :: Ctx -> TypeMap -> Term -> Infer Type
+inferType _ _ (Zero _) = return Nat
+inferType ctx tymap (Succ t _) = do
+  checkType ctx tymap t
+  return Nat
+inferType ctx tymap (Add t1 t2 _) = do
+  checkType ctx tymap t1
+  checkType ctx tymap t2
+  return Nat
+inferType ctx tymap (Mult t1 t2 _) = do
+  checkType ctx tymap t1
+  checkType ctx tymap t2
+  return Nat
+inferType _ _ (Tru _) = return Bool
+inferType _ _ (Fls _) = return Bool
+inferType ctx tymap (Not t _) = do
+  checkType ctx tymap t
+  return Bool
+inferType ctx tymap (And t1 t2 _) = do
+  checkType ctx tymap t1
+  checkType ctx tymap t2
+  return Bool
+inferType ctx tymap (Or t1 t2 _) = do
+  checkType ctx tymap t1
+  checkType ctx tymap t2
+  return Bool
+inferType ctx _ (Var name _) = lookupVar ctx name
+inferType ctx tymap (Let name t body _) = do
+  tyt <- inferType ctx tymap t
+  inferType (Bind ctx name tyt) tymap body
+inferType ctx tymap (Anno term ty _) = do
+  checkType ctx tymap term
+  return ty
+inferType ctx tymap (App t1 t2 _) = do
+  ty <- inferType ctx tymap t1
+  (ty1, ty2) <- matchFun ty (show t1)
+  checkType ctx tymap t2
+  return ty2
+inferType ctx tymap (LetData n adty t _) =
+  -- TODO check that n is not already bound
+  -- TODO check that elements in n are not bound
+  inferType ctx (Bind tymap n adty) t
+inferType ctx tymap (Cotr n ts p) = do
+  -- TODO find better solution
+  -- PROBLEM we need to find the binding that contains the constructor
+  (adty, tys) <- lookupCotr tymap n
+  if length ts == length tys
+  then do
+    -- check types accordingly to definition
+    let subchecks = map (\(t, ty) -> do
+          ty' <- matchTypeVar tymap ty
+          checkType ctx tymap t
+          ) (zip ts tys) -- basically a map over the [(Term, Type)] and apply check ctx
+    foldl (>>) (return ()) subchecks
+    return adty
+  else fail ["Expected number of arguments violated for " ++ show (Cotr n ts p)]
+inferType _ _ t = fail ["Cannot infer type of term " ++ show t]
+
+checkType :: Ctx -> TypeMap -> Term -> Check
+checkType ctx tymap p@(Lam name t _) = do
+  ty <- requiredType ctx tymap p
+  (ty1, ty2) <- matchFun ty (show p)
+  checkType (Bind ctx name ty1) tymap t
+checkType ctx tymap p@(If cond t1 t2 _) = do
+  ty <- requiredType ctx tymap p
+  checkType ctx tymap cond
+  checkType ctx tymap t1
+  checkType ctx tymap t2
+checkType ctx tymap p@(Match m cases _) = do
+  ty <- requiredType ctx tymap p
+  mty <- inferType ctx tymap m
+  mty' <- matchTypeVar tymap mty
+  (_, cotrs) <- matchADT mty' (show m)
+  if length cases == length cotrs
+  then do
+    let casechecks = map (\c -> do
+          tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
+          if length (bindingsOfCase c) == length tys
+          then
+            if not (null (bindingsOfCase c))
+            then do
+              let bindchecks = map (\(b, bty) ->
+                    checkType (Bind ctx b bty) tymap (termOfCase c)
+                    ) $ zip (bindingsOfCase c) tys
+              foldl (>>) (return ()) bindchecks
+            else checkType ctx tymap (termOfCase c)
+          else fail ["number of bindings does not match number of args of constructor"]
+          ) cases
+    foldl (>>) (return ()) casechecks
+  else fail ["cases do not match number of constructors of" ++ show m]
+checkType ctx tymap t = do
+  ty <- requiredType ctx tymap t
+  ty' <- inferType ctx tymap t
+  matchType ty ty' (show t)
+
+requiredType :: Ctx -> TypeMap -> Term -> Infer Type
+requiredType ctx tymap term = case parent term of
+  Just (Succ t _) | term == t -> return Nat
+  Just (Add t1 t2 _) | term == t1 -> return Nat
+  Just (Add t1 t2 _) | term == t2 -> return Nat
+  Just (Mult t1 t2 _) | term == t1 -> return Nat
+  Just (Mult t1 t2 _) | term == t2 -> return Nat
+  Just (Not t _) | term == t -> return Bool
+  Just (And t1 t2 _) | term == t1 -> return Bool
+  Just (And t1 t2 _) | term == t2 -> return Bool
+  Just (Or t1 t2 _) | term == t1 -> return Bool
+  Just (Or t1 t2 _) | term == t2 -> return Bool
+  Just (Anno t ty _) | term == t -> return ty
+  Just (App t1 t2 _) | term == t2 -> do
+    ty <- inferType ctx tymap t1
+    (ty1, ty2) <- matchFun ty (show t1)
+    return ty1
+  Just (Cotr n ts p) -> do
+    (adty, tys) <- lookupCotr tymap n
+    if length ts == length tys
+    then do
+      -- check types accordingly to definition
+      let maybePair = find (\(t, ty) -> term == t) (zip ts tys)
+      let maybeType = fmap (\(t, ty) -> ty) maybePair
+      ty <- liftMaybe maybeType "Could not determine type belonging to term"
+      matchTypeVar tymap ty
+    else fail ["Expected number of arguments violated for " ++ show (Cotr n ts p)]
+  Just p@(Lam name t _) | term == t -> do
+    let (Bind ctx' _ _) = ctx
+    ty <- requiredType ctx' tymap p
+    (ty1, ty2) <- matchFun ty (show p)
+    return ty2
+  Just p@(If cond t1 t2 _) | term == cond -> return Bool
+  Just p@(If cond t1 t2 _) | term == t1 -> requiredType ctx tymap p
+  Just p@(If cond t1 t2 _) | term == t2 -> requiredType ctx tymap p
+  Just p@(Match m cases _) -> do
+    mty <- inferType ctx tymap m
+    mty' <- matchTypeVar tymap mty
+    (_, cotrs) <- matchADT mty' (show m)
+    if length cases == length cotrs
+    then do
+      -- throw away ctx extension if bindingsOfCase c != null
+      -- let x = find (\c -> term == termOfCase c) cases
+      let (Bind ctx' _ _) = ctx
+      requiredType ctx' tymap p
+    else fail ["cases do not match number of constructors of" ++ show m]
+  _ -> fail ["Could not determine required type"]

haskell/test/ADTypes/EliminateTypeArgumentOfCheckSpec.hs

+{-# LANGUAGE FlexibleInstances #-}
+module ADTypes.EliminateTypeArgumentOfCheckSpec where
+
+import Prelude hiding (lookup,(*), (**))
+import Test.Hspec
+
+import ADTypes.Base as B
+import ADTypes.SharedSpecs
+import ADTypes.EliminateTypeArgumentOfCheck as E
+import ADTypes.Language
+
+
+instance ConvertToBInfer E.Infer where
+  convert (E.Inferred ty) = B.Inferred ty
+  convert (E.NotInferred err) = B.NotInferred $ head err
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = sharedSpec $ E.inferType Empty Empty