ErrorList.hs 4.48 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
module FORecursiveTypes.ErrorList where

import Prelude hiding ((>=), (<=), lookup)
import Data.List(find)
-- import Data.Map
import qualified Data.Map as Map

import FORecursiveTypes.Language
import Util.ErrorMessages

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

instance Monad Infer where
  return = Inferred
  (Inferred ty) >>= f = f ty
  (NotInferred err) >>= _ = NotInferred err
  fail msg = NotInferred [msg]

-- matching functions that extract the inner types if possible
-- one problem is that we do not get as good error messages, because term is not known in these functions
matchNat :: Type -> String -> Check
matchNat Nat _ = return ()
matchNat ty err = fail $ natError 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

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

57 58 59 60
lookupTypeVar :: TypeMap -> Name -> Infer Type
lookupTypeVar Empty x = fail $ "Unbound type variable " ++ show x
lookupTypeVar (Bind c x t) y
  | x == y = return t
André Pacak's avatar
André Pacak committed
61
  | otherwise = lookupTypeVar c y
62

63
matchTypeVar :: TypeMap -> Type -> Infer Type
64
matchTypeVar tymap (TypeVar x) = lookupTypeVar tymap x
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
matchTypeVar _ ty = return ty

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
  | otherwise = lookup c y

inferType :: Ctx -> TypeMap -> Term -> Infer Type
inferType _ _ (Unit _) = return UnitT
inferType _ _ (Zero _) = return Nat
inferType ctx tymap (Succ t _) = do
  checkType ctx tymap t Nat
  return Nat
inferType ctx tymap (Add t1 t2 _) = do
  checkType ctx tymap t1 Nat
  checkType ctx tymap t2 Nat
  return Nat
inferType ctx tymap (Mult t1 t2 _) = do
  checkType ctx tymap t1 Nat
  checkType ctx tymap t2 Nat
  return Nat
inferType ctx _ (Var name _) = lookup 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
96
  checkType ctx tymap term ty
97 98 99 100 101 102 103
  return ty
inferType ctx tymap (App t1 t2 _) = do
  ty <- inferType ctx tymap t1
  rty <- matchTypeVar tymap ty
  (ty1, ty2) <- matchFun rty (show t1)
  checkType ctx tymap t2 ty1
  return ty2
104
inferType ctx tymap (LetType n ty t _) = inferType ctx (Bind tymap n ty) t
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
inferType _ _ t = fail $ "Cannot infer type of term " ++ show t

checkType :: Ctx -> TypeMap -> Term -> Type -> Check
checkType ctx tymap p@(Lam name t _) ty = do
  rty <- matchTypeVar tymap ty
  (ty1, ty2) <- matchFun rty (show p)
  checkType (Bind ctx name ty1) tymap t ty2
checkType ctx tymap p@(InL t _) ty = do
  rty <- matchTypeVar tymap ty
  (ty1, ty2) <- matchSum rty (show p)
  checkType ctx tymap t ty1
checkType ctx tymap p@(InR t _) ty = do
  rty <- matchTypeVar tymap ty
  (ty1, ty2) <- matchSum rty (show p)
  checkType ctx tymap t ty2
checkType ctx tymap p@(Case e n1 t1 n2 t2 _) ty = do
  ety <- inferType ctx tymap e
  rty <- matchTypeVar tymap ety
  (ty1, ty2) <- matchSum rty (show e)
  checkType (Bind ctx n1 ty1) tymap t1 ty
  checkType (Bind ctx n2 ty2) tymap t2 ty
checkType ctx tymap p@(Tag n t _) ty = do
  rty <- matchTypeVar tymap ty
  types <- matchVariant rty (show p)
  let lty = Map.lookup n types
  (maybe (fail "") (checkType ctx tymap t) lty)
checkType ctx tymap p@(Match m cases _) ty = do
  ety <- inferType ctx tymap m
  rty <- matchTypeVar tymap ety
  types <- matchVariant rty (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) tymap t ty
        ) cases
  foldl (>>) (return ()) subchecks

checkType ctx tymap t ty = do
  ty' <- inferType ctx tymap t
  matchType ty ty' (show t)