{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}

-- |
-- Module      : OAlg.Data.Validable
-- Description : validable values
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- validable values @x@, which can be validated via @'OAlg.Control.Validate.validate' ('valid' x)@. 
module OAlg.Data.Validable
  ( -- * Validable
    Validable(..), rnfValid

  , Validable1(..), Validable2(..)

    -- * XStandard
  , XStandard(..), relXStandard
  )
  where

import Control.DeepSeq (NFData(..))

import Data.Ratio
import Data.Proxy

import OAlg.Category.Definition hiding ((.))

import OAlg.Data.Statement
import OAlg.Data.Either
import OAlg.Data.Number
import OAlg.Data.Opposite
import OAlg.Data.X

import OAlg.Structure.Definition

--------------------------------------------------------------------------------
-- XStandard -

-- | standard random variable for __@x@__.
--
--   __Property__ For all @x@ in the range of 'xStandard' holds: @'valid' x@.
class Validable x => XStandard x where
  xStandard :: X x

instance XStandard () where xStandard :: X ()
xStandard = forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance XStandard N where xStandard :: X N
xStandard = X N
xN
instance XStandard Z where xStandard :: X Z
xStandard = X Z
xZ
instance XStandard Q where xStandard :: X Q
xStandard = X Q
xQ

--------------------------------------------------------------------------------
-- xStandard' -

-- | the standard random variable associated to __@x@__. The type __@p x@__ serves
--   only as proxy and will be not evaluated.
xStandard' :: XStandard x => p x -> X x
xStandard' :: forall x (p :: * -> *). XStandard x => p x -> X x
xStandard' p x
_ = forall x. XStandard x => X x
xStandard

--------------------------------------------------------------------------------
-- relXStandard -

-- | validity of the standard random variable associated to __@x@__
--   (__@p x@__ just serves as proxy and will not be evaluated).
relXStandard :: XStandard x => p x -> Statement
relXStandard :: forall x (p :: * -> *). XStandard x => p x -> Statement
relXStandard p x
px = forall x. X x -> (x -> Statement) -> Statement
Forall (forall x (p :: * -> *). XStandard x => p x -> X x
xStandard' p x
px) forall a. Validable a => a -> Statement
valid where

--------------------------------------------------------------------------------
-- Validable -

-- | validation of a value of @__a__@.
class Validable a where
  valid :: a -> Statement

deriving instance Validable x => Validable (Op x)

instance Validable () where
  valid :: () -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid

instance Validable Bool where
  valid :: Bool -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid

instance Validable Valid where
  valid :: Valid -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid
  
instance Validable Char where
  valid :: Char -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid
  
instance Validable Int where
  valid :: Int -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid

instance Validable Integer where
  valid :: Integer -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid

instance Validable (Ratio Integer) where
  valid :: Ratio Integer -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid

instance Validable N where
  valid :: N -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid
  
instance Validable Z where
  valid :: Z -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid
  
instance Validable Q where
  valid :: Q -> Statement
valid = forall x. NFData x => x -> Statement
rnfValid  

instance Validable (Proxy x) where
  valid :: Proxy x -> Statement
valid Proxy x
Proxy = Statement
SValid

instance Validable (Struct s x) where
  valid :: Struct s x -> Statement
valid Struct s x
Struct = Statement
SValid

instance Validable a => Validable (Maybe a) where
  valid :: Maybe a -> Statement
valid (Just a
a)  = forall a. Validable a => a -> Statement
valid a
a
  valid (Maybe a
Nothing) = Statement
SValid
  
instance Validable a => Validable [a] where
  valid :: [a] -> Statement
valid []     = Statement
SValid
  valid (a
x:[a]
xs) = forall a. Validable a => a -> Statement
valid a
x Statement -> Statement -> Statement
:&& forall a. Validable a => a -> Statement
valid [a]
xs

instance (Validable a,Validable b) => Validable (Either a b) where
  valid :: Either a b -> Statement
valid (Left a
a)  = forall a. Validable a => a -> Statement
valid a
a
  valid (Right b
b) = forall a. Validable a => a -> Statement
valid b
b

instance (Validable a,Validable b) => Validable (a,b) where
  valid :: (a, b) -> Statement
valid (a
a,b
b) = [Statement] -> Statement
And [forall a. Validable a => a -> Statement
valid a
a,forall a. Validable a => a -> Statement
valid b
b]

instance (Validable a,Validable b,Validable c) => Validable (a,b,c) where
  valid :: (a, b, c) -> Statement
valid (a
a,b
b,c
c) = [Statement] -> Statement
And [forall a. Validable a => a -> Statement
valid a
a,forall a. Validable a => a -> Statement
valid b
b,forall a. Validable a => a -> Statement
valid c
c]
  
instance (Validable a,Validable b,Validable c,Validable d) => Validable (a,b,c,d) where
  valid :: (a, b, c, d) -> Statement
valid (a
a,b
b,c
c,d
d) = [Statement] -> Statement
And [forall a. Validable a => a -> Statement
valid a
a,forall a. Validable a => a -> Statement
valid b
b,forall a. Validable a => a -> Statement
valid c
c,forall a. Validable a => a -> Statement
valid d
d]

instance (Validable a,Validable b,Validable c,Validable d,Validable e)
  => Validable (a,b,c,d,e) where
  valid :: (a, b, c, d, e) -> Statement
valid (a
a,b
b,c
c,d
d,e
e) = [Statement] -> Statement
And [forall a. Validable a => a -> Statement
valid a
a,forall a. Validable a => a -> Statement
valid b
b,forall a. Validable a => a -> Statement
valid c
c,forall a. Validable a => a -> Statement
valid d
d,forall a. Validable a => a -> Statement
valid e
e]

instance Validable a => Validable (X a) where
  valid :: X a -> Statement
valid X a
xa = forall x. X x -> (x -> Statement) -> Statement
Forall X a
xa forall a. Validable a => a -> Statement
valid

instance (XStandard x, Validable y) => Validable (x -> y) where
  valid :: (x -> y) -> Statement
valid x -> y
f = forall x. X x -> (x -> Statement) -> Statement
Forall forall x. XStandard x => X x
xStandard (forall a. Validable a => a -> Statement
valid forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> y
f)

--------------------------------------------------------------------------------
-- rnfValid -

-- | validation of being reducible to normal form.
rnfValid :: NFData x => x -> Statement
rnfValid :: forall x. NFData x => x -> Statement
rnfValid x
x = ((forall a. NFData a => a -> ()
rnf x
x forall a. Eq a => a -> a -> Bool
== ()) Bool -> Message -> Statement
:?> Message
MInvalid)

--------------------------------------------------------------------------------
-- Validable1 -

-- | validation of a value of @p x@.
class Validable1 p where
  valid1 :: p x -> Statement
  default valid1 :: Validable (p x) => p x -> Statement
  valid1 = forall a. Validable a => a -> Statement
valid

instance Validable1 Proxy
instance Validable1 (Struct s)

--------------------------------------------------------------------------------
-- Validable2 -

-- | validation of a value of @h x y@.
class Validable2 h where
  valid2 :: h x y -> Statement
  default valid2 :: Validable (h x y) => h x y -> Statement
  valid2 = forall a. Validable a => a -> Statement
valid

instance Validable2 h => Validable2 (Op2 h) where
  valid2 :: forall x y. Op2 h x y -> Statement
valid2 (Op2 h y x
h) = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h y x
h

instance (Validable2 f, Validable2 g) => Validable2 (Either2 f g) where
  valid2 :: forall x y. Either2 f g x y -> Statement
valid2 (Left2 f x y
f)  = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 f x y
f
  valid2 (Right2 g x y
g) = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 g x y
g

instance Validable2 m => Validable2 (Forget t m) where
  valid2 :: forall x y. Forget t m x y -> Statement
valid2 (Forget m x y
m) = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 m x y
m

instance Validable2 m => Validable (Forget t m x y) where
  valid :: Forget t m x y -> Statement
valid = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2