Add extract for safely extracting final element from union

This commit is contained in:
Eric Easley 2016-11-15 22:54:41 -08:00
parent d5393e72aa
commit 4260466929
6 changed files with 24 additions and 24 deletions

View File

@ -57,11 +57,10 @@ exitSuccess' = send ExitSuccess
--------------------------------------------------------------------------------
runTeletype :: Eff '[Teletype] w -> IO w
runTeletype (Val x) = return x
runTeletype (E u q) = case decomp u of
Right (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ())
Right GetLine -> getLine >>= \s -> runTeletype (qApp q s)
Right ExitSuccess -> exitSuccess
Left _ -> error "This cannot happen"
runTeletype (E u q) = case extract u of
(PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ())
GetLine -> getLine >>= \s -> runTeletype (qApp q s)
ExitSuccess -> exitSuccess
--------------------------------------------------------------------------------
-- Pure Interpreter --

View File

@ -30,11 +30,10 @@ exitSuccess' = send ExitSuccess
--------------------------------------------------------------------------------
runTeletype :: Eff '[Teletype] w -> IO w
runTeletype (Val x) = return x
runTeletype (E u q) = case decomp u of
Right (PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ())
Right GetLine -> getLine >>= \s -> runTeletype (qApp q s)
Right ExitSuccess -> exitSuccess
Left _ -> error "This cannot happen"
runTeletype (E u q) = case extract u of
(PutStrLn msg) -> putStrLn msg >> runTeletype (qApp q ())
GetLine -> getLine >>= \s -> runTeletype (qApp q s)
ExitSuccess -> exitSuccess
--------------------------------------------------------------------------------
-- Pure Interpreter --
@ -44,8 +43,7 @@ runTeletypePure inputs req = reverse (go inputs req [])
where go :: [String] -> Eff '[Teletype] w -> [String] -> [String]
go _ (Val _) acc = acc
go [] _ acc = acc
go (x:xs) (E u q) acc = case decomp u of
Right (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc)
Right GetLine -> go xs (qApp q x) acc
Right ExitSuccess -> go xs (Val ()) acc
Left _ -> go xs (Val ()) acc
go (x:xs) (E u q) acc = case extract u of
(PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc)
GetLine -> go xs (qApp q x) acc
ExitSuccess -> go xs (Val ()) acc

View File

@ -44,6 +44,7 @@ module Control.Monad.Freer.Internal (
decomp,
tsingleton,
extract,
qApp,
qComp,
@ -137,9 +138,8 @@ run _ = error "Internal:run - This (E) should never happen"
-- This is useful for plugging in traditional transformer stacks.
runM :: Monad m => Eff '[m] w -> m w
runM (Val x) = return x
runM (E u q) = case decomp u of
Right mb -> mb >>= runM . qApp q
Left _ -> error "Internal:runM - This (Left) should never happen"
runM (E u q) = case extract u of
mb -> mb >>= runM . qApp q
-- the other case is unreachable since Union [] a cannot be
-- constructed. Therefore, run is a total function if its argument

View File

@ -38,6 +38,5 @@ trace = send . Trace
-- | An IO handler for Trace effects
runTrace :: Eff '[Trace] w -> IO w
runTrace (Val x) = return x
runTrace (E u q) = case decomp u of
Right (Trace s) -> putStrLn s >> runTrace (qApp q ())
Left _ -> error "runTrace:Left - This should never happen"
runTrace (E u q) = case extract u of
Trace s -> putStrLn s >> runTrace (qApp q ())

View File

@ -46,8 +46,12 @@ decomp :: Union (t ': r) v -> Either (Union r v) (t v)
decomp (UNow x) = Right x
decomp (UNext v) = Left v
{-# INLINE extract #-}
extract :: Union '[t] v -> t v
extract (UNow x) = x
{-# INLINE weaken #-}
weaken :: Union r w -> Union (any ': r) w
weaken :: Union (t ': r) w -> Union (any ': t ': r) w
weaken = UNext
class (Member' t r (FindElem t r)) => Member t r where

View File

@ -10,7 +10,7 @@ module Data.Open.Union.Internal where
data Union (r :: [ * -> * ]) v where
UNow :: t v -> Union (t ': r) v
UNext :: Union r v -> Union (any ': r) v
UNext :: Union (t ': r) v -> Union (any ': t ': r) v
data Nat = S Nat | Z
data P (n :: Nat) = P
@ -25,7 +25,7 @@ instance (r ~ (t ': r')) => Member' t r 'Z where
prj' _ (UNow x) = Just x
prj' _ _ = Nothing
instance (r ~ (t' ': r'), Member' t r' n) => Member' t r ('S n) where
instance (r ~ (t' ': r' : rs'), Member' t (r' : rs') n) => Member' t r ('S n) where
inj' _ = UNext . inj' (P::P n)
prj' _ (UNow _) = Nothing
prj' _ (UNext x) = prj' (P::P n) x