...
 
Commits (2)
{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module SumTypes.ContinueAfterCheckFail where module SumTypes.ContinueAfterCheckFail where
import Prelude hiding (Monad(..), (>=), (<=), lookup) import Prelude hiding ((>=), (<=), lookup, fail)
import GHC.Exts (Constraint)
import qualified Data.Map as Map import qualified Data.Map as Map
import Control.Monad.Writer.Lazy (Writer)
import qualified Control.Monad.Writer.Lazy as Writer
import SumTypes.Language import SumTypes.Language
import Util.ErrorMessages import Util.ErrorMessages
import Util.PartialOrd import Util.PartialOrd
-- is needed because we use the RebindableSyntax extension
ifThenElse :: Bool -> a -> a -> a
ifThenElse True thn _ = thn
ifThenElse False _ els = els
type Error = [String] type Error = [String]
data Infer a = Inferred a | NotInferred Error
type Infer a = Writer Error a
type Check = Infer () 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
class WithTop a where class WithTop a where
top :: a top :: a
...@@ -46,30 +30,10 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where ...@@ -46,30 +30,10 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where
instance (WithTop v) => WithTop (Map.Map Name v) where instance (WithTop v) => WithTop (Map.Map Name v) where
top = Map.empty top = Map.empty
-- Had to define an own monad type class. fail :: WithTop a => Error -> Infer a
-- It is not possible otherwise to get the type constraint WithTop a. fail msg = do
-- We use the extension ConstraintKinds to support this. Writer.tell msg
-- Could not find a simpler solution for this problem. return top
-- The restricted monad problem is common.
class RMonad m where
type RMonadCtx m a :: Constraint
return :: RMonadCtx m a => a -> m a
(>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
(>>) :: (RMonadCtx m a, RMonadCtx m b) => m a -> m b -> m b
m >> k = m >>= \_ -> k
fail :: [String] -> m a
instance RMonad Infer where
type RMonadCtx Infer a = WithTop a
return = Inferred
(Inferred ty) >>= f = f ty
NotInferred err1 >>= f =
-- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
case f top of
Inferred _ -> fail err1
NotInferred err2 -> fail $ err1 ++ err2
fail = NotInferred
-- matching functions that extract the inner types if possible -- matching functions that extract the inner types if possible
matchNat :: Type -> String -> Check matchNat :: Type -> String -> Check
......
...@@ -9,12 +9,13 @@ import SumTypes.Base as B ...@@ -9,12 +9,13 @@ import SumTypes.Base as B
import SumTypes.SharedSpecs import SumTypes.SharedSpecs
import SumTypes.ContinueAfterCheckFail as C import SumTypes.ContinueAfterCheckFail as C
import SumTypes.Language import SumTypes.Language
import Control.Monad.Writer.Lazy (Writer, runWriter)
instance ConvertToBInfer (Writer C.Error) where
instance ConvertToBInfer C.Infer where convert m =
convert (C.Inferred ty) = B.Inferred ty case runWriter m of
convert (C.NotInferred err) = B.NotInferred $ head err (t,[]) -> Inferred t
(t,err) -> NotInferred (head err)
main :: IO () main :: IO ()
main = hspec spec main = hspec spec
......