Commit 22a29a8d authored by Sven Keidel's avatar Sven Keidel

use writer monad to avoid rebindable syntax

parent 658a5352
{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module SumTypes.ContinueAfterCheckFail where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Prelude hiding ((>=), (<=), lookup, fail)
import qualified Data.Map as Map
import Control.Monad.Writer.Lazy (Writer)
import qualified Control.Monad.Writer.Lazy as Writer
import SumTypes.Language
import Util.ErrorMessages
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]
data Infer a = Inferred a | NotInferred Error
type Infer a = Writer Error a
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
top :: a
......@@ -46,30 +30,10 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where
instance (WithTop v) => WithTop (Map.Map Name v) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
-- We use the extension ConstraintKinds to support this.
-- Could not find a simpler solution for this problem.
-- 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
fail :: WithTop a => Error -> Infer a
fail msg = do
Writer.tell msg
return top
-- matching functions that extract the inner types if possible
matchNat :: Type -> String -> Check
......
......@@ -9,12 +9,13 @@ import SumTypes.Base as B
import SumTypes.SharedSpecs
import SumTypes.ContinueAfterCheckFail as C
import SumTypes.Language
import Control.Monad.Writer.Lazy (Writer, runWriter)
instance ConvertToBInfer C.Infer where
convert (C.Inferred ty) = B.Inferred ty
convert (C.NotInferred err) = B.NotInferred $ head err
instance ConvertToBInfer (Writer C.Error) where
convert m =
case runWriter m of
(t,[]) -> Inferred t
(t,err) -> NotInferred (head err)
main :: IO ()
main = hspec spec
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment