{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# 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
  , ValidableDual1

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

    -- * XStandard

  , XStandard(..), relXStandard
  , XStd, xStd, xStdStruct
  , XStandardDual1

    -- * Extensional Equality

  , EqualExt, EqE
  , equalExt
  )
  where

import Control.Monad (return)
import Control.DeepSeq (NFData(..))

import Data.Kind
import Data.Ratio

import OAlg.Category.Applicative
import OAlg.Category.Definition
import OAlg.Data.Identity

import OAlg.Data.Proxy
import OAlg.Data.Boolean.Definition
import OAlg.Data.Statement.Definition
import OAlg.Data.Dualisable
import OAlg.Data.Maybe
import OAlg.Data.Either
import OAlg.Data.Equal
import OAlg.Data.EqualExtensional
import OAlg.Data.Show
import OAlg.Data.Ord
import OAlg.Data.Number
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 XStandard x where
  xStandard :: X x

instance XStandard () where xStandard :: X ()
xStandard = () -> X ()
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance XStandard Int where xStandard :: X Int
xStandard = X Int
xInt
instance XStandard Integer where xStandard :: X Integer
xStandard = X Integer
xInteger
instance XStandard x => XStandard (Id x) where xStandard :: X (Id x)
xStandard = (x -> Id x) -> X x -> X (Id x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Id x
forall x. x -> Id x
Id X x
forall x. XStandard x => X x
xStandard

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
_ = X 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 :: (Validable x, XStandard x) => p x -> Statement
relXStandard :: forall x (p :: * -> *).
(Validable x, XStandard x) =>
p x -> Statement
relXStandard p x
px = X x -> (x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (p x -> X x
forall x (p :: * -> *). XStandard x => p x -> X x
xStandard' p x
px) x -> Statement
forall a. Validable a => a -> Statement
valid where

--------------------------------------------------------------------------------

-- XStd -


-- | type representing the class of 'XStandard' structures.

data XStd

type instance Structure XStd x = (XStandard x)

--------------------------------------------------------------------------------

-- xStd -


-- | the associated standard random variable.

xStdStruct :: Struct XStd x -> X x
xStdStruct :: forall x. Struct XStd x -> X x
xStdStruct Struct XStd x
Struct = X x
forall x. XStandard x => X x
xStandard

-- | the associated standard random variable for the 'domain'.

xStd :: (Morphism m, Transformable (ObjectClass m) XStd) => m x y -> X x
xStd :: forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) XStd) =>
m x y -> X x
xStd m x y
m = Struct XStd x -> X x
forall x. Struct XStd x -> X x
xStdStruct (Struct (ObjectClass m) x -> Struct XStd x
forall x. Struct (ObjectClass m) x -> Struct XStd x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (m x y -> Struct (ObjectClass m) x
forall x y. m x y -> Struct (ObjectClass m) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
m))

--------------------------------------------------------------------------------

-- XStandardDual1 -


-- | helper class to avoid undecidable instances.

class XStandard (Dual1 d x) => XStandardDual1 d x

--------------------------------------------------------------------------------

-- Validable -


-- | validation of a value of @__a__@.

class Validable a where
  valid :: a -> Statement

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

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

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

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

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

instance Validable x => Validable (Id x) where valid :: Id x -> Statement
valid (Id x
x) = x -> Statement
forall a. Validable a => a -> Statement
valid x
x

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

instance Validable x => Validable (Closure x) where
  valid :: Closure x -> Statement
valid Closure x
x' = case Closure x
x' of
    It x
x -> x -> Statement
forall a. Validable a => a -> Statement
valid x
x
    Closure x
_    -> Statement
SValid


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 (Struct2 m x y) where
  valid :: Struct2 m x y -> Statement
valid Struct2 m x y
Struct2 = Statement
SValid

instance Validable a => Validable (Maybe a) where
  valid :: Maybe a -> Statement
valid (Just a
a)  = a -> Statement
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) = a -> Statement
forall a. Validable a => a -> Statement
valid a
x Statement -> Statement -> Statement
:&& [a] -> 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)  = a -> Statement
forall a. Validable a => a -> Statement
valid a
a
  valid (Right b
b) = b -> Statement
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 [a -> Statement
forall a. Validable a => a -> Statement
valid a
a,b -> Statement
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 [a -> Statement
forall a. Validable a => a -> Statement
valid a
a,b -> Statement
forall a. Validable a => a -> Statement
valid b
b,c -> Statement
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 [a -> Statement
forall a. Validable a => a -> Statement
valid a
a,b -> Statement
forall a. Validable a => a -> Statement
valid b
b,c -> Statement
forall a. Validable a => a -> Statement
valid c
c,d -> Statement
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 [a -> Statement
forall a. Validable a => a -> Statement
valid a
a,b -> Statement
forall a. Validable a => a -> Statement
valid b
b,c -> Statement
forall a. Validable a => a -> Statement
valid c
c,d -> Statement
forall a. Validable a => a -> Statement
valid d
d,e -> Statement
forall a. Validable a => a -> Statement
valid e
e]

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

instance (XStandard x, Validable y) => Validable (x -> y) where
  valid :: (x -> y) -> Statement
valid x -> y
f = X x -> (x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X x
forall x. XStandard x => X x
xStandard (y -> Statement
forall a. Validable a => a -> Statement
valid (y -> Statement) -> (x -> y) -> x -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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 = ((x -> ()
forall a. NFData a => a -> ()
rnf x
x () -> () -> Bool
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 = p x -> Statement
forall a. Validable a => a -> Statement
valid

instance Validable1 Proxy
instance Validable1 (Struct s)

instance (Validable (a x), Validable (b x)) => Validable (Either1 a b x) where
  valid :: Either1 a b x -> Statement
valid (Left1 a x
a) = a x -> Statement
forall a. Validable a => a -> Statement
valid a x
a
  valid (Right1 b x
b) = b x -> Statement
forall a. Validable a => a -> Statement
valid b x
b

--------------------------------------------------------------------------------

-- ValidableDual1 -


-- | helper class to avoid undecidable instances.

class Validable (Dual1 d x) => ValidableDual1 d x

--------------------------------------------------------------------------------

-- 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 = h x y -> Statement
forall a. Validable a => a -> Statement
valid

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)  = f x y -> Statement
forall x y. f x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 f x y
f
  valid2 (Right2 g x y
g) = g x y -> Statement
forall x y. g x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 g x y
g

instance Validable2 (Struct2 m)

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

    
--------------------------------------------------------------------------------

-- EqE -


-- | type representing extensional equality.

data EqE

type instance Structure EqE x = (Show x, Eq x, XStandard x)

instance Transformable EqE Type where tau :: forall x. Struct EqE x -> Struct (*) x
tau Struct EqE x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType EqE

--------------------------------------------------------------------------------

-- EqualExt -


-- | category of extensional equality.

type EqualExt = Sub EqE (->)

instance EqExt EqualExt where
  Sub x -> y
f .=. :: forall x y. EqualExt x y -> EqualExt x y -> Statement
.=. Sub x -> y
g = X x -> (x -> y) -> (x -> y) -> Statement
forall x y.
(Show x, Eq y) =>
X x -> (x -> y) -> (x -> y) -> Statement
prpEqualExt X x
forall x. XStandard x => X x
xStandard x -> y
f x -> y
g

--------------------------------------------------------------------------------

-- equalExt -


-- | embedding 'amapG' of a 'Applicative1' to 'EqualExt'.

equalExtS :: Applicative1 c t => Homomorphous EqE (t x) (t y) -> c x y -> EqualExt (t x) (t y)
equalExtS :: forall (c :: * -> * -> *) (t :: * -> *) x y.
Applicative1 c t =>
Homomorphous EqE (t x) (t y) -> c x y -> EqualExt (t x) (t y)
equalExtS (Struct EqE (t x)
Struct:>:Struct EqE (t y)
Struct) c x y
f = (t x -> t y) -> Sub EqE (->) (t x) (t y)
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub (c x y -> t x -> t y
forall x y. c x y -> t x -> t y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG c x y
f)

-- | embedding 'amapG' of a 'Applicative1' to 'EqualExt'.

equalExt :: (Morphism c, Applicative1 c t, TransformableG t (ObjectClass c) EqE)
  => c x y -> EqualExt (t x) (t y)
equalExt :: forall (c :: * -> * -> *) (t :: * -> *) x y.
(Morphism c, Applicative1 c t,
 TransformableG t (ObjectClass c) EqE) =>
c x y -> EqualExt (t x) (t y)
equalExt c x y
f = Homomorphous EqE (t x) (t y) -> c x y -> EqualExt (t x) (t y)
forall (c :: * -> * -> *) (t :: * -> *) x y.
Applicative1 c t =>
Homomorphous EqE (t x) (t y) -> c x y -> EqualExt (t x) (t y)
equalExtS (Struct (ObjectClass c) x -> Struct EqE (t x)
forall x. Struct (ObjectClass c) x -> Struct EqE (t x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (c x y -> Struct (ObjectClass c) x
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f)Struct EqE (t x)
-> Struct EqE (t y) -> Homomorphous EqE (t x) (t y)
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>:Struct (ObjectClass c) y -> Struct EqE (t y)
forall x. Struct (ObjectClass c) x -> Struct EqE (t x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (c x y -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f)) c x y
f

--------------------------------------------------------------------------------

-- Inv2 - Validable


instance (Category c, EqExt c) => Validable (Inv2 c x y) where
  valid :: Inv2 c x y -> Statement
valid (Inv2 c x y
f c y x
f') = String -> Label
Label String
"Inv2" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (c y x
f' c y x -> c x y -> c x x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f c x x -> c x x -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) x
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f))
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (c x y
f c x y -> c y x -> c y y
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
f' c y y -> c y y -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. Struct (ObjectClass c) y -> c y y
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f))
        ]
    
instance (Category c, EqExt c) => Validable2 (Inv2 c)