Continue refactoring the core-to-core pipeline

[ghc-hetmet.git] / compiler / coreSyn / CoreLint.lhs

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 4893885..62fe897 100644 (file)
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -36,7 +36,6 @@ import BasicTypes
 import StaticFlags
 import ListSetOps
 import PrelNames
-import DynFlags
 import Outputable
 import FastString
 import Util
@@ -96,29 +95,11 @@ find an occurence of an Id, we fetch it from the in-scope set.
 
 
 \begin{code}
-lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
-
-lintCoreBindings dflags _whoDunnit _binds
-  | not (dopt Opt_DoCoreLinting dflags)
-  = return ()
-
-lintCoreBindings dflags whoDunnit binds
-  | isEmptyBag errs
-  = do { showPass dflags ("Core Linted result of " ++ whoDunnit)
-       ; unless (isEmptyBag warns || opt_NoDebugOutput) $ printDump $
-         (banner "warnings" $$ displayMessageBag warns)
-       ; return () }
-
-  | otherwise
-  = do { printDump (vcat [ banner "errors", displayMessageBag errs
-                        , ptext (sLit "*** Offending Program ***")
-                        , pprCoreBindings binds
-                        , ptext (sLit "*** End of Offense ***") ])
-
-       ; ghcExit dflags 1 }
+lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
+--   Returns (warnings, errors)
+lintCoreBindings binds
+  = initL (lint_binds binds)
   where
-    (warns, errs) = initL (lint_binds binds)
-
        -- Put all the top-level binders in scope at the start
        -- This is because transformation rules can bring something
        -- into use 'unexpectedly'
@@ -128,13 +109,6 @@ lintCoreBindings dflags whoDunnit binds
 
     lint_bind (Rec prs)                = mapM_ (lintSingleBinding TopLevel Recursive) prs
     lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
-
-    banner string = ptext (sLit "*** Core Lint")      <+> text string 
-                    <+> ptext (sLit ": in result of") <+> text whoDunnit 
-                    <+> ptext (sLit "***")
-
-displayMessageBag :: Bag Message -> SDoc
-displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
 \end{code}
 
 %************************************************************************
@@ -154,7 +128,7 @@ lintUnfolding :: SrcLoc
 
 lintUnfolding locn vars expr
   | isEmptyBag errs = Nothing
-  | otherwise       = Just (displayMessageBag errs)
+  | otherwise       = Just (pprMessageBag errs)
   where
     (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
                             addInScopeVars vars                   $
@@ -633,10 +607,9 @@ lintCoercion ty@(FunTy ty1 ty2)
        ; return (FunTy s1 s2, FunTy t1 t2) }
 
 lintCoercion ty@(TyConApp tc tys) 
-  | Just (ar, rule) <- isCoercionTyCon_maybe tc
+  | Just (ar, desc) <- isCoercionTyCon_maybe tc
   = do { unless (tys `lengthAtLeast` ar) (badCo ty)
-       ; (s,t)   <- rule lintType lintCoercion 
-                         True (take ar tys)
+       ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
        ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
        ; check_co_app ty (typeKind s) ss
        ; return (mkAppTys s ss, mkAppTys t ts) }
@@ -677,6 +650,70 @@ lintCoercion (ForAllTy tv ty)
 badCo :: Coercion -> LintM a
 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
 
+---------------
+lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
+-- Always called with correct number of coercion arguments
+-- First arg is just for error message
+lintCoTyConApp _ CoLeft  (co:_) = lintLR   fst             co 
+lintCoTyConApp _ CoRight (co:_) = lintLR   snd             co   
+lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3   co 
+lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3   co 
+lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co 
+
+lintCoTyConApp _ CoSym (co:_) 
+  = do { (ty1,ty2) <- lintCoercion co
+       ; return (ty2,ty1) }
+
+lintCoTyConApp co CoTrans (co1:co2:_) 
+  = do { (ty1a, ty1b) <- lintCoercion co1
+       ; (ty2a, ty2b) <- lintCoercion co2
+       ; checkL (ty1b `coreEqType` ty2a)
+                (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
+                    2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+       ; return (ty1a, ty2b) }
+
+lintCoTyConApp _ CoInst (co:arg_ty:_) 
+  = do { co_tys <- lintCoercion co
+       ; arg_kind  <- lintType arg_ty
+       ; case decompInst_maybe co_tys of
+          Just ((tv1,tv2), (ty1,ty2)) 
+            | arg_kind `isSubKind` tyVarKind tv1
+            -> return (substTyWith [tv1] [arg_ty] ty1, 
+                       substTyWith [tv2] [arg_ty] ty2) 
+            | otherwise
+            -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
+         Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
+
+lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs 
+                          , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
+  = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
+       ; sequence_ (zipWith checkKinds tvs tys1)
+       ; return (substTyWith tvs tys1 lhs_ty,
+                 substTyWith tvs tys2 rhs_ty) }
+
+lintCoTyConApp _ CoUnsafe (ty1:ty2:_) 
+  = do { _ <- lintType ty1
+       ; _ <- lintType ty2     -- Ignore kinds; it's unsafe!
+       ; return (ty1,ty2) } 
+
+lintCoTyConApp _ _ _ = panic "lintCoTyConApp"  -- Called with wrong number of coercion args
+
+----------
+lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
+lintLR sel co
+  = do { (ty1,ty2) <- lintCoercion co
+       ; case decompLR_maybe (ty1,ty2) of
+           Just res -> return (sel res)
+           Nothing  -> failWithL (ptext (sLit "Bad argument of left/right")) }
+
+----------
+lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
+lintCsel sel co
+  = do { (ty1,ty2) <- lintCoercion co
+       ; case decompCsel_maybe (ty1,ty2) of
+           Just res -> return (sel res)
+           Nothing  -> failWithL (ptext (sLit "Bad argument of csel")) }
+
 -------------------
 lintType :: OutType -> LintM Kind
 lintType (TyVarTy tv)