utils/ext-core/Check.hs

   1 module Check where
   2
   3 import Monad
   4 import Core
   5 import Printer
   6 import List
   7 import Env
   8
   9 {- Checking is done in a simple error monad.  In addition to
  10    allowing errors to be captured, this makes it easy to guarantee
  11    that checking itself has been completed for an entire module. -}
  12
  13 data CheckResult a = OkC a | FailC String
  14
  15 instance Monad CheckResult where
  16   OkC a >>= k = k a
  17   FailC s >>= k = fail s
  18   return = OkC
  19   fail = FailC
  20
  21 require :: Bool -> String -> CheckResult ()
  22 require False s = fail s
  23 require True  _ = return ()
  24
  25 requireM :: CheckResult Bool -> String -> CheckResult ()
  26 requireM cond s =
  27   do b <- cond
  28      require b s
  29
  30 {- Environments. -}
  31 type Tvenv = Env Tvar Kind                    -- type variables  (local only)
  32 type Tcenv = Env Tcon Kind                    -- type constructors
  33 type Tsenv = Env Tcon ([Tvar],Ty)             -- type synonyms
  34 type Cenv = Env Dcon Ty                       -- data constructors
  35 type Venv = Env Var Ty                        -- values
  36 type Menv = Env Mname Envs                    -- modules
  37 data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
  38
  39 {- Extend an environment, checking for illegal shadowing of identifiers. -}
  40 extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
  41 extendM env (k,d) =
  42    case elookup env k of
  43      Just _ -> fail ("multiply-defined identifier: " ++ show k)
  44      Nothing -> return (eextend env (k,d))
  45
  46 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
  47 lookupM env k =
  48    case elookup env k of
  49      Just v -> return v
  50      Nothing -> fail ("undefined identifier: " ++ show k)
  51
  52 {- Main entry point. -}
  53 checkModule :: Menv -> Module -> CheckResult Menv
  54 checkModule globalEnv (Module mn tdefs vdefgs) =
  55   do (tcenv,tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
  56      cenv <- foldM (checkTdef tcenv) eempty tdefs
  57      (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) (eempty,eempty) vdefgs
  58      return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
  59   where
  60
  61     checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
  62     checkTdef0 (tcenv,tsenv) tdef = ch tdef
  63       where
  64         ch (Data (m,c) tbs _) =
  65             do require (m == mn) ("wrong module name in data type declaration:\n" ++ show tdef)
  66                tcenv' <- extendM tcenv (c,k)
  67                return (tcenv',tsenv)
  68             where k = foldr Karrow Klifted (map snd tbs)
  69         ch (Newtype (m,c) tbs rhs) =
  70             do require (m == mn) ("wrong module name in newtype declaration:\n" ++ show tdef)
  71                tcenv' <- extendM tcenv (c,k)
  72                tsenv' <- case rhs of
  73                            Nothing -> return tsenv
  74                            Just rep -> extendM tsenv (c,(map fst tbs,rep))
  75                return (tcenv', tsenv')
  76             where k = foldr Karrow Klifted (map snd tbs)
  77
  78     checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
  79     checkTdef tcenv cenv = ch
  80        where
  81          ch (Data (_,c) utbs cdefs) =
  82             do cbinds <- mapM checkCdef cdefs
  83                foldM extendM cenv cbinds
  84             where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
  85                     do require (m == mn) ("wrong module name in constructor declaration:\n" ++ show cdef)
  86                        tvenv <- foldM extendM eempty tbs
  87                        ks <- mapM (checkTy (tcenv,tvenv)) ts
  88                        mapM_ (\k -> require (baseKind k)
  89                                             ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
  90                                              "kind: " ++ show k) ) ks
  91                        return (dcon,t)
  92                     where tbs = utbs ++ etbs
  93                           t = foldr Tforall
  94                                   (foldr tArrow
  95                                           (foldl Tapp (Tcon (mn,c))
  96                                                  (map (Tvar . fst) utbs)) ts) tbs
  97          ch (tdef@(Newtype c tbs (Just t))) =
  98             do tvenv <- foldM extendM eempty tbs
  99                k <- checkTy (tcenv,tvenv) t
 100                require (k==Klifted) ("bad kind:\n" ++ show tdef)
 101                return cenv
 102          ch (tdef@(Newtype c tbs Nothing)) =
 103             {- should only occur for recursive Newtypes -}
 104             return cenv
 105
 106
 107     checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv)
 108     checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
 109       case vdefg of
 110         Rec vdefs ->
 111             do e_venv' <- foldM extendM e_venv e_vts
 112                l_venv' <- foldM extendM l_venv l_vts
 113                let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
 114                mapM_ (\ (vdef@(Vdef ((m,v),t,e))) ->
 115                             do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
 116                                k <- checkTy (tcenv,tvenv) t
 117                                require (k==Klifted) ("unlifted kind in:\n" ++ show vdef)
 118                                t' <- checkExp env' e
 119                                requireM (equalTy tsenv t t')
 120                                         ("declared type doesn't match expression type in:\n"  ++ show vdef ++ "\n" ++
 121                                          "declared type: " ++ show t ++ "\n" ++
 122                                          "expression type: " ++ show t')) vdefs
 123                return (e_venv',l_venv')
 124             where e_vts  = [ (v,t) | Vdef ((m,v),t,_) <- vdefs, m /= "" ]
 125                   l_vts  = [ (v,t) | Vdef (("",v),t,_) <- vdefs]
 126         Nonrec (vdef@(Vdef ((m,v),t,e))) ->
 127             do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
 128                k <- checkTy (tcenv,tvenv) t
 129                require (k /= Kopen) ("open kind in:\n" ++ show vdef)
 130                require ((not top_level) || (k /= Kunlifted)) ("top-level unlifted kind in:\n" ++ show vdef)
 131                t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
 132                requireM (equalTy tsenv t t')
 133                         ("declared type doesn't match expression type in:\n" ++ show vdef  ++ "\n"  ++
 134                          "declared type: " ++ show t ++ "\n" ++
 135                          "expression type: " ++ show t')
 136                if m == "" then
 137                  do l_venv' <- extendM l_venv (v,t)
 138                     return (e_venv,l_venv')
 139                 else
 140                  do e_venv' <- extendM e_venv (v,t)
 141                     return (e_venv',l_venv)
 142
 143     checkExp ::  (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
 144     checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
 145       where
 146         ch e0 =
 147           case e0 of
 148             Var qv ->
 149               qlookupM venv_ e_venv l_venv qv
 150             Dcon qc ->
 151               qlookupM cenv_ cenv eempty qc
 152             Lit l ->
 153               checkLit l
 154             Appt e t ->
 155               do t' <- ch e
 156                  k' <- checkTy (tcenv,tvenv) t
 157                  case t' of
 158                    Tforall (tv,k) t0 ->
 159                      do require (k' <= k)
 160                                 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
 161                                  "operator kind: " ++ show k ++ "\n" ++
 162                                  "operand kind: " ++ show k')
 163                         return (substl [tv] [t] t0)
 164                    _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
 165                                "operator type: " ++ show t')
 166             App e1 e2 ->
 167               do t1 <- ch e1
 168                  t2 <- ch e2
 169                  case t1 of
 170                    Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
 171                         do requireM (equalTy tsenv t2 t')
 172                                     ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
 173                                      "operator type: " ++ show t' ++ "\n" ++
 174                                      "operand type: " ++ show t2)
 175                            return t0
 176                    _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
 177                                "operator type: " ++ show t1)
 178             Lam (Tb tb) e ->
 179               do tvenv' <- extendM tvenv tb
 180                  t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
 181                  return (Tforall tb t)
 182             Lam (Vb (vb@(_,vt))) e ->
 183               do k <- checkTy (tcenv,tvenv) vt
 184                  require (baseKind k)
 185                          ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
 186                           "kind: " ++ show k)
 187                  l_venv' <- extendM l_venv vb
 188                  t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
 189                  require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
 190                  return (tArrow vt t)
 191             Let vdefg e ->
 192               do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg
 193                  checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
 194             Case e (v,t) alts ->
 195               do t' <- ch e
 196                  checkTy (tcenv,tvenv) t
 197                  requireM (equalTy tsenv t t')
 198                           ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
 199                            "declared type: " ++ show t ++ "\n" ++
 200                            "expression type: " ++ show t')
 201                  case (reverse alts) of
 202                    (Acon c _ _ _):as ->
 203                       let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
 204                                                                  ("duplicate alternative in case:\n" ++ show e0)
 205                                                          ok as (c:cs)
 206                           ok ((Alit _ _):_)      _  = fail ("invalid alternative in constructor case:\n" ++ show e0)
 207                           ok [Adefault _]        _  = return ()
 208                           ok (Adefault _:_)      _  = fail ("misplaced default alternative in case:\n" ++ show e0)
 209                           ok []                  _  = return ()
 210                       in ok as [c]
 211                    (Alit l _):as ->
 212                       let ok ((Acon _ _ _ _):_) _  = fail ("invalid alternative in literal case:\n" ++ show e0)
 213                           ok ((Alit l _):as)    ls = do require (notElem l ls)
 214                                                                 ("duplicate alternative in case:\n" ++ show e0)
 215                                                         ok as (l:ls)
 216                           ok [Adefault _]       _  = return ()
 217                           ok (Adefault _:_)     _  = fail ("misplaced default alternative in case:\n" ++ show e0)
 218                           ok []                 _  = fail ("missing default alternative in literal case:\n" ++ show e0)
 219                       in ok as [l]
 220                    [Adefault _] -> return ()
 221                    [] -> fail ("no alternatives in case:\n" ++ show e0)
 222                  l_venv' <- extendM l_venv (v,t)
 223                  t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
 224                  bs <- mapM (equalTy tsenv t) ts
 225                  require (and bs)
 226                          ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
 227                           "types: " ++ show (t:ts))
 228                  return t
 229             Coerce t e ->
 230               do ch e
 231                  checkTy (tcenv,tvenv) t
 232                  return t
 233             Note s e ->
 234               ch e
 235             External _ t ->
 236               do checkTy (tcenv,eempty) t {- external types must be closed -}
 237                  return t
 238
 239     checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
 240     checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
 241       where
 242         ch a0 =
 243           case a0 of
 244             Acon qc etbs vbs e ->
 245               do let uts = f t0
 246                        where f (Tapp t0 t) = f t0 ++ [t]
 247                              f _ = []
 248                  ct <- qlookupM cenv_ cenv eempty qc
 249                  let (tbs,ct_args0,ct_res0) = splitTy ct
 250                  {- get universals -}
 251                  let (utbs,etbs') = splitAt (length uts) tbs
 252                  let utvs = map fst utbs
 253                  {- check existentials -}
 254                  let (etvs,eks) = unzip etbs
 255                  let (etvs',eks') = unzip etbs'
 256                  require (eks == eks')
 257                          ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
 258                           "kinds declared in data constructor: " ++ show eks ++
 259                           "kinds declared in case alternative: " ++ show eks')
 260                  tvenv' <- foldM extendM tvenv etbs
 261                  {- check term variables -}
 262                  let vts = map snd vbs
 263                  mapM_ (\vt -> require ((not . isUtupleTy) vt)
 264                                        ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
 265                                         "pattern type: " ++ show vt)) vts
 266                  vks <- mapM (checkTy (tcenv,tvenv')) vts
 267                  mapM_ (\vk -> require (baseKind vk)
 268                                        ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
 269                                         "kind: " ++ show vk)) vks
 270                  let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
 271                  zipWithM_
 272                     (\ct_arg vt ->
 273                         requireM (equalTy tsenv ct_arg vt)
 274                                  ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
 275                                   "pattern variable type: " ++ show ct_arg ++ "\n" ++
 276                                   "constructor argument type: " ++ show vt)) ct_args vts
 277                  requireM (equalTy tsenv ct_res t0)
 278                           ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
 279                            "pattern constructor type: " ++ show ct_res ++ "\n" ++
 280                            "scrutinee type: " ++ show t0)
 281                  l_venv' <- foldM extendM l_venv vbs
 282                  t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
 283                  checkTy (tcenv,tvenv) t  {- check that existentials don't escape in result type -}
 284                  return t
 285             Alit l e ->
 286               do t <- checkLit l
 287                  requireM (equalTy tsenv t t0)
 288                          ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
 289                           "pattern type: " ++ show t ++ "\n" ++
 290                           "scrutinee type: " ++ show t0)
 291                  checkExp env e
 292             Adefault e ->
 293               checkExp env e
 294
 295     checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
 296     checkTy (tcenv,tvenv) = ch
 297      where
 298        ch (Tvar tv) = lookupM tvenv tv
 299        ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc
 300        ch (t@(Tapp t1 t2)) =
 301            do k1 <- ch t1
 302               k2 <- ch t2
 303               case k1 of
 304                  Karrow k11 k12 ->
 305                    do require (k2 <= k11)
 306                              ("kinds don't match in type application: " ++ show t ++ "\n" ++
 307                               "operator kind: " ++ show k11 ++ "\n" ++
 308                               "operand kind: " ++ show k2)
 309                       return k12
 310                  _ -> fail ("applied type has non-arrow kind: " ++ show t)
 311        ch (Tforall tb t) =
 312             do tvenv' <- extendM tvenv tb
 313                checkTy (tcenv,tvenv') t
 314
 315     {- Type equality modulo newtype synonyms. -}
 316     equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
 317     equalTy tsenv t1 t2 =
 318             do t1' <- expand t1
 319                t2' <- expand t2
 320                return (t1' == t2')
 321       where expand (Tvar v) = return (Tvar v)
 322             expand (Tcon qtc) = return (Tcon qtc)
 323             expand (Tapp t1 t2) =
 324               do t2' <- expand t2
 325                  expapp t1 [t2']
 326             expand (Tforall tb t) =
 327               do t' <- expand t
 328                  return (Tforall tb t')
 329             expapp (t@(Tcon (m,tc))) ts =
 330               do env <- mlookupM tsenv_ tsenv eempty m
 331                  case elookup env tc of
 332                     Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs)
 333                     _ -> return (foldl Tapp t ts)
 334             expapp (Tapp t1 t2) ts =
 335               do t2' <- expand t2
 336                  expapp t1 (t2':ts)
 337             expapp t ts =
 338               do t' <- expand t
 339                  return (foldl Tapp t' ts)
 340
 341
 342     mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname -> CheckResult (Env a b)
 343     mlookupM selector external_env local_env m =
 344       if m == "" then
 345         return local_env
 346       else if m == mn then
 347         return external_env
 348       else
 349         case elookup globalEnv m of
 350           Just env' -> return (selector env')
 351           Nothing -> fail ("undefined module name: " ++ show m)
 352
 353     qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> (Mname,a) -> CheckResult b
 354     qlookupM selector external_env local_env (m,k) =
 355       do env <- mlookupM selector external_env local_env m
 356          lookupM env k
 357
 358
 359 checkLit :: Lit -> CheckResult Ty
 360 checkLit lit =
 361   case lit of
 362     Lint _ t ->
 363           do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh])
 364                      ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
 365              return t
 366     Lrational _ t ->
 367           do {- require (elem t [tFloatzh,tDoublezh])
 368                      ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
 369              return t
 370     Lchar _ t ->
 371           do {- require (t == tCharzh)
 372                      ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)  -}
 373              return t
 374     Lstring _ t ->
 375           do {- require (t == tAddrzh)
 376                      ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)  -}
 377              return t
 378
 379 {- Utilities -}
 380
 381 {- Split off tbs, arguments and result of a (possibly abstracted)  arrow type -}
 382 splitTy :: Ty -> ([Tbind],[Ty],Ty)
 383 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
 384                 where (tbs,ts,tr) = splitTy t
 385 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
 386                 where (tbs,ts,tr) = splitTy t
 387 splitTy t = ([],[],t)
 388
 389
 390 {- Simultaneous substitution on types for type variables,
 391    renaming as neceessary to avoid capture.
 392    No checks for correct kindedness. -}
 393 substl :: [Tvar] -> [Ty] -> Ty -> Ty
 394 substl tvs ts t = f (zip tvs ts) t
 395   where
 396     f env t0 =
 397      case t0 of
 398        Tcon _ -> t0
 399        Tvar v -> case lookup v env of
 400                    Just t1 -> t1
 401                    Nothing -> t0
 402        Tapp t1 t2 -> Tapp (f env t1) (f env t2)
 403        Tforall (t,k) t1 ->
 404          if t `elem` free then
 405            Tforall (t',k) (f ((t,Tvar t'):env) t1)
 406          else
 407            Tforall (t,k) (f (filter ((/=t).fst) env) t1)
 408      where free = foldr union [] (map (freeTvars.snd) env)
 409            t' = freshTvar free
 410
 411 {- Return free tvars in a type -}
 412 freeTvars :: Ty -> [Tvar]
 413 freeTvars (Tcon _) = []
 414 freeTvars (Tvar v) = [v]
 415 freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
 416 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
 417
 418 {- Return any tvar *not* in the argument list. -}
 419 freshTvar :: [Tvar] -> Tvar
 420 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
 421