-- | Validated values
--
-- 'Validated' is similar to 'Feldspar.Option.Option', with the difference that
-- 'Validated' does not guarantee that invalid values are not evaluated.
-- Therefore, 'Validated' should not be used to guard operations from illegal
-- use (e.g. array bounds checking).
--
-- Still, the operations try to defer evaluation of invalid values as much as
-- possible.

module Feldspar.Data.Validated where



-- Since there's no guarantee that invalid values are not evaluated, there is
-- no point in hiding the implementation. Having access to the implementation
-- means that it's possible to take shortcuts. For example, `fmap` could not
-- have been implemented without opening up the representation.



import Prelude ()

import Language.Syntactic

import Feldspar hiding (desugar, sugar)
import Feldspar.Representation



-- | A value that can be valid or invalid
data Validated a = Validated (Data Bool) a

instance Functor Validated
  where
    fmap :: (a -> b) -> Validated a -> Validated b
fmap a -> b
f (Validated Data Bool
valid a
a) = Data Bool -> b -> Validated b
forall a. Data Bool -> a -> Validated a
Validated Data Bool
valid (a -> b
f a
a)

instance Applicative Validated
  where
    pure :: a -> Validated a
pure  = Data Bool -> a -> Validated a
forall a. Data Bool -> a -> Validated a
Validated Data Bool
true
    <*> :: Validated (a -> b) -> Validated a -> Validated b
(<*>) = Validated (a -> b) -> Validated a -> Validated b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Validated
  where
    return :: a -> Validated a
return = a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    Validated Data Bool
valid a
a >>= :: Validated a -> (a -> Validated b) -> Validated b
>>= a -> Validated b
k = Data Bool -> b -> Validated b
forall a. Data Bool -> a -> Validated a
Validated (Data Bool
valid Data Bool -> Data Bool -> Data Bool
&& Data Bool
valid') b
b
      where
        Validated Data Bool
valid' b
b = a -> Validated b
k a
a

instance Syntax a => Syntactic (Validated a)
  where
    type Domain (Validated a)   = FeldDomain
    type Internal (Validated a) = (Bool, Internal a)
    desugar :: Validated a -> ASTF (Domain (Validated a)) (Internal (Validated a))
desugar (Validated Data Bool
valid a
a) = (Data Bool, a)
-> ASTF (Domain (Data Bool, a)) (Internal (Data Bool, a))
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar (Data Bool
valid,a
a)
    sugar :: ASTF (Domain (Validated a)) (Internal (Validated a)) -> Validated a
sugar = (Data Bool -> a -> Validated a) -> (Data Bool, a) -> Validated a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Data Bool -> a -> Validated a
forall a. Data Bool -> a -> Validated a
Validated ((Data Bool, a) -> Validated a)
-> (ASTF FeldDomain (Bool, Internal a) -> (Data Bool, a))
-> ASTF FeldDomain (Bool, Internal a)
-> Validated a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF FeldDomain (Bool, Internal a) -> (Data Bool, a)
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar

-- | Create a validated value. Note that the value may get evaluated even if the
-- condition is false.
validWhen :: Data Bool -> a -> Validated a
validWhen :: Data Bool -> a -> Validated a
validWhen = Data Bool -> a -> Validated a
forall a. Data Bool -> a -> Validated a
Validated

-- | Invalid value
invalid :: Syntax a => Validated a
invalid :: Validated a
invalid = Data Bool -> a -> Validated a
forall a. Data Bool -> a -> Validated a
Validated Data Bool
false a
forall a. Syntax a => a
example

-- | Deconstruct an 'Validated' value
validated :: Syntax b
    => b         -- ^ Invalid case
    -> (a -> b)  -- ^ Valid case
    -> Validated a
    -> b
validated :: b -> (a -> b) -> Validated a -> b
validated b
no a -> b
yes (Validated Data Bool
valid a
a) = Data Bool
valid Data Bool -> b -> b -> b
forall a. Syntax a => Data Bool -> a -> a -> a
? a -> b
yes a
a (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ b
no

-- | Deconstruct an 'Validated' value
caseValidated :: Syntax b
    => Validated a
    -> b         -- ^ Invalid case
    -> (a -> b)  -- ^ Valid case
    -> b
caseValidated :: Validated a -> b -> (a -> b) -> b
caseValidated Validated a
v b
no a -> b
yes = b -> (a -> b) -> Validated a -> b
forall b a. Syntax b => b -> (a -> b) -> Validated a -> b
validated b
no a -> b
yes Validated a
v

fromValidated :: Syntax a
    => Validated a
    -> a  -- ^ Value to return in case the first arg. is invalid
    -> a
fromValidated :: Validated a -> a -> a
fromValidated Validated a
v a
def = Validated a -> a -> (a -> a) -> a
forall b a. Syntax b => Validated a -> b -> (a -> b) -> b
caseValidated Validated a
v a
def a -> a
forall a. a -> a
id

-- | Deconstruct an 'Validated' value
validatedM :: MonadComp m
    => m ()         -- ^ Invalid case
    -> (a -> m ())  -- ^ Valid case
    -> Validated a
    -> m ()
validatedM :: m () -> (a -> m ()) -> Validated a -> m ()
validatedM m ()
no a -> m ()
yes (Validated Data Bool
valid a
a) = Data Bool -> m () -> m () -> m ()
forall (m :: * -> *).
MonadComp m =>
Data Bool -> m () -> m () -> m ()
iff Data Bool
valid (a -> m ()
yes a
a) m ()
no

-- | Deconstruct an 'Validated' value
caseValidatedM :: MonadComp m
    => Validated a
    -> m ()         -- ^ Invalid case
    -> (a -> m ())  -- ^ Valid case
    -> m ()
caseValidatedM :: Validated a -> m () -> (a -> m ()) -> m ()
caseValidatedM Validated a
v m ()
no a -> m ()
yes = m () -> (a -> m ()) -> Validated a -> m ()
forall (m :: * -> *) a.
MonadComp m =>
m () -> (a -> m ()) -> Validated a -> m ()
validatedM m ()
no a -> m ()
yes Validated a
v