compiler: finish type well-formedness (#59)

cogent/src/Cogent/TypeCheck.hs

@@ -33,7 +33,7 @@ import Control.Arrow (first, second)
 import Control.Lens
 import Control.Monad.Except
 import Control.Monad.State
-import Control.Monad.Writer
+import Control.Monad.Writer hiding (censor)
 import Data.Either (lefts)
 import Data.List (nub, (\\))
 import qualified Data.Map as M
@@ -45,24 +45,26 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<>), (<$>))
 
 tc :: [(SourcePos, TopLevel LocType LocPatn LocExpr)]
    -> IO ((Either () [TopLevel RawType TypedPatn TypedExpr], [ContextualisedEW]), TCState)
-tc = ((first . second) adjustErrors <$>) . flip runStateT (TCS M.empty knownTypes M.empty) . runWriterT . runExceptT . typecheck
+tc = ((first . second) adjustErrors <$>) . flip runStateT (TCS M.empty knownTypes M.empty) . (failError <$>) . runWriterT . runExceptT . typecheck
   where
     knownTypes = map (, ([] , Nothing)) $ words "U8 U16 U32 U64 String Bool"
     adjustErrors = (if __cogent_freverse_tc_errors then reverse else id) . adjustContexts
     adjustContexts = map (first noConstraints)
     noConstraints = if __cogent_ftc_ctx_constraints then id else filter (not . isCtxConstraint)
+    failError (Right _, ews) | or (map isWarnAsError ews), Flag_Werror <- __cogent_warning_switch = (Left (), ews)
+    failError x = x
+
+typecheck :: [(SourcePos, TopLevel LocType LocPatn LocExpr)]
+          -> ExceptT () (WriterT [ContextualisedEW] TC) [TopLevel RawType TypedPatn TypedExpr]
+typecheck = censor warnsToErrors . mapM (uncurry checkOne)
+  where
     warnsToErrors = case __cogent_warning_switch of
                       Flag_w -> filter (not . isWarn)
                       Flag_Wwarn -> id
                       Flag_Werror -> map warnToError
-    isWarn (_, Right _) = True; isWarn _ = False
     warnToError (c,Right w) = (c, Left $ TypeWarningAsError w)
     warnToError ew = ew
 
-typecheck :: [(SourcePos, TopLevel LocType LocPatn LocExpr)]
-          -> ExceptT () (WriterT [ContextualisedEW] TC) [TopLevel RawType TypedPatn TypedExpr]
-typecheck = mapM (uncurry checkOne)
-
 -- TODO: Check for prior definition
 checkOne :: SourcePos -> TopLevel LocType LocPatn LocExpr
          -> ExceptT () (WriterT [ContextualisedEW] TC) (TopLevel RawType TypedPatn TypedExpr)

cogent/src/Cogent/TypeCheck/Base.hs

@@ -104,6 +104,14 @@ isCtxConstraint _ = False
 -- high-level context at the end of the list
 type ContextualisedEW = ([ErrorContext], TypeEW)
 
+isWarn :: ContextualisedEW -> Bool
+isWarn (_, Right _) = True
+isWarn _ = False
+
+isWarnAsError :: ContextualisedEW -> Bool
+isWarnAsError (_, Left (TypeWarningAsError _)) = True
+isWarnAsError _ = False
+
 data TypeFragment a = F a
                     | FRecord [(FieldName, (a, Taken))]
                     | FVariant (M.Map TagName ([a], Taken))
@@ -235,10 +243,6 @@ warnToConstraint f w | f = SemiSat w
 --           Flag_Werror -> Unsat (TypeWarningAsError w)
 --   | otherwise = Sat
 
-isWarnAsError :: ContextualisedEW -> Bool
-isWarnAsError (_, Left (TypeWarningAsError _)) = True
-isWarnAsError _ = False
-
 data TCState = TCS { _knownFuns    :: M.Map FunName (Polytype TCType)
                    , _knownTypes   :: TypeDict
                    , _knownConsts  :: M.Map VarName (TCType, SourcePos)

cogent/src/Cogent/TypeCheck/Post.hs

@@ -38,16 +38,6 @@ import Text.PrettyPrint.ANSI.Leijen as P hiding ((<>), (<$>))
 
 type Post a = ExceptT () (WriterT [ContextualisedEW] TC) a
 
--- NOTE: The `ExceptT` on `WriterT` monad stack works in a way which,
--- if an error has been thrown, then later operations like `tell` or
--- `censor` will not fire. Although that is the right definition for
--- Monad, it doesn't serve our purposes here. Thus this `censor` function,
--- which sort of work around the problem. Still, it doesn't change the
--- way `>>=` works in general. As a consequence, if an error has been
--- thrown, it still doesn't contiune logging more errors. / zilinc
-censor :: ([ContextualisedEW] -> [ContextualisedEW]) -> Post a -> Post a
-censor f m = ExceptT . WriterT $ do (a, w) <- runWriterT $ runExceptT m; return (a, f w)
-
 postT :: [ErrorContext] -> TCType -> Post RawType
 postT ctx t = do
   d <- use knownTypes

cogent/src/Cogent/TypeCheck/Util.hs

@@ -8,8 +8,10 @@ import Cogent.Compiler
 -- import Cogent.TypeCheck.Base
 import Cogent.PrettyPrint
 
-import Control.Monad.IO.Class
+import Control.Monad.Except
+-- import Control.Monad.IO.Class
 -- import Control.Monad.State.Class
+import Control.Monad.Writer
 -- import Data.Function ((&))
 -- import System.IO
 import Text.PrettyPrint.ANSI.Leijen as L hiding (indent)
@@ -20,3 +22,15 @@ traceTC s | Just ws <- __cogent_ddump_tc_filter, s `notElem` ws = const $ return
 
 traceTC' :: MonadIO m => String -> String -> m ()
 traceTC' s = traceTC s . text
+
+-- NOTE: The `ExceptT` on `WriterT` monad stack works in a way which,
+-- if an error has been thrown, then later operations like `tell` or
+-- `censor` will not fire. Although that is the right definition for
+-- Monad, it doesn't serve our purposes here. Thus this `censor` function,
+-- which sort of work around the problem. Still, it doesn't change the
+-- way `>>=` works in general. As a consequence, if an error has been
+-- thrown, it still doesn't contiune logging more errors. / zilinc
+censor :: (Monad m) => (w -> w) -> ExceptT e (WriterT w m) a -> ExceptT e (WriterT w m) a
+censor f m = ExceptT . WriterT $ do (a, w) <- runWriterT $ runExceptT m; return (a, f w)
+
+