Base.hs 5.41 KB
Newer Older
André Pacak's avatar
temp  
André Pacak committed
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 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
module ADTypes.Base where

import Prelude hiding ((>=), (<=))
import qualified Data.Map as M
import Data.Maybe
import ADTypes.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 = 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 :: Monad m => Maybe a -> String -> m 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
77
lookupCotr (Bind c x ty) y = case ty of
André Pacak's avatar
temp  
André Pacak committed
78 79 80 81 82 83 84 85
  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


86 87 88 89
inferType :: Ctx -> TypeMap -> Term -> Infer Type
inferType _ _ (Zero _) = return Nat
inferType ctx tymap (Succ t _) = do
  checkType ctx tymap t Nat
André Pacak's avatar
temp  
André Pacak committed
90
  return Nat
91 92 93
inferType ctx tymap (Add t1 t2 _) = do
  checkType ctx tymap t1 Nat
  checkType ctx tymap t2 Nat
André Pacak's avatar
temp  
André Pacak committed
94
  return Nat
95 96 97
inferType ctx tymap (Mult t1 t2 _) = do
  checkType ctx tymap t1 Nat
  checkType ctx tymap t2 Nat
André Pacak's avatar
temp  
André Pacak committed
98
  return Nat
99 100 101 102
inferType _ _ (Tru _) = return Bool
inferType _ _ (Fls _) = return Bool
inferType ctx tymap (Not t _) = do
  checkType ctx tymap t Bool
André Pacak's avatar
temp  
André Pacak committed
103
  return Bool
104 105 106
inferType ctx tymap (And t1 t2 _) = do
  checkType ctx tymap t1 Bool
  checkType ctx tymap t2 Bool
André Pacak's avatar
temp  
André Pacak committed
107
  return Bool
108 109 110
inferType ctx tymap (Or t1 t2 _) = do
  checkType ctx tymap t1 Bool
  checkType ctx tymap t2 Bool
André Pacak's avatar
temp  
André Pacak committed
111
  return Bool
112 113 114
inferType ctx tymap (Var name _) = do
  ty <- lookupVar ctx name
  matchTypeVar tymap ty
115 116 117 118 119
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 ty
André Pacak's avatar
temp  
André Pacak committed
120
  return ty
121 122
inferType ctx tymap (App t1 t2 _) = do
  ty <- inferType ctx tymap t1
André Pacak's avatar
temp  
André Pacak committed
123
  (ty1, ty2) <- matchFun ty (show t1)
124
  checkType ctx tymap t2 ty1
André Pacak's avatar
temp  
André Pacak committed
125
  return ty2
126 127 128 129 130
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
André Pacak's avatar
temp  
André Pacak committed
131 132
  -- TODO find better solution
  -- PROBLEM we need to find the binding that contains the constructor
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148

  (adty, tys) <- lookupCotr tymap n
  if length ts == length tys
  then do
    -- check types accordingly to definition
    let subchecks = zipWith (\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
    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 -> Type -> Check
checkType ctx tymap p@(Lam name t _) ty = do
André Pacak's avatar
temp  
André Pacak committed
149
  (ty1, ty2) <- matchFun ty (show p)
150 151 152 153 154 155 156 157 158
  checkType (Bind ctx name ty1) tymap t ty2
checkType ctx tymap (If cond t1 t2 _) ty = do
  checkType ctx tymap cond Bool
  checkType ctx tymap t1 ty
  checkType ctx tymap t2 ty
checkType ctx tymap (Match m cases _) ty = do
  mty <- inferType ctx tymap m
  mty' <- matchTypeVar tymap mty
  (_, cotrs) <- matchADT mty' (show m)
André Pacak's avatar
temp  
André Pacak committed
159
  if length cases == length cotrs
160 161 162
  then do
    let casechecks = map (\c -> do
          tys <- liftMaybe (M.lookup (labelOfCase c) cotrs) "Could not find constructor" :: Infer [Type]
163
          if length (bindingsOfCase c) == length tys
164 165 166
          then do
              let ctx' = foldl (\r (b, bty) -> Bind r b bty) ctx (zip (bindingsOfCase c) tys)
              checkType ctx' tymap (termOfCase c) ty
167
          else fail "number of bindings does not match number of args of constructor"
168 169
          ) cases
    foldl (>>) (return ()) casechecks
170 171 172
  else fail $ "cases do not match number of constructors of" ++ show m
checkType ctx tymap t ty = do
  ty' <- inferType ctx tymap t
André Pacak's avatar
temp  
André Pacak committed
173
  matchType ty ty' (show t)