{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

-- |
-- Module      : OAlg.Structure.Additive.Proposition
-- Description : propositions on additive structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions on 'Additive' structures.
module OAlg.Structure.Additive.Proposition
  (
    -- * Additive
    relIsZero
  , prpAdd
  , prpAdd1, prpAdd2, prpAdd2_1, prpAdd2_2
  , prpAdd3, prpAdd4, prpAdd5, prpAdd6

    -- * Abelian
  , prpAbl, prpAbl1, prpAbl2
  , prpAbl3, prpAbl3_1, prpAbl3_2
  , prpAbl4, prpAbl5

    -- * X
    -- ** Additive
  , XAdd(..), Adbl2(..), Adbl3(..)
  , XStandardAdd(..)

    -- ** Abelian
  , XAbl(..)

    -- ** Total
  , xAddTtl

    -- ** Direction
  , xoAdd, xoRoot, xoAdbl2, xoAdbl3
  , xoAbl, xoFbr

    -- ** Orientation
  , xAddOrnt

     -- ** Stalk
  , xAddStalk, xStalkAdbl2, xStalkAdbl3

  )
  where

import Control.Monad
import Control.Applicative

import OAlg.Prelude

import OAlg.Data.Singleton
import OAlg.Data.Canonical

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Fibred

import OAlg.Structure.Additive.Definition

--------------------------------------------------------------------------------
-- relIsZero -

-- | relation of 'isZero'.
relIsZero :: Additive a => a -> Statement
relIsZero :: forall a. Additive a => a -> Statement
relIsZero a
a = String -> Label
Label String
"isZero" Label -> Statement -> Statement
:<=>: forall a. Additive a => a -> Bool
isZero a
a Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
a]

--------------------------------------------------------------------------------
-- prpAdd1 -

-- | validtiy of 'root' according to "OAlg.Structure.Additive.Definition#Add1".
prpAdd1 :: Additive a => p a -> X (Root a) -> Statement
prpAdd1 :: forall a (p :: * -> *).
Additive a =>
p a -> X (Root a) -> Statement
prpAdd1 p a
s X (Root a)
xr = String -> Label
Prp String
"Add1"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Root a)
xr (\Root a
r -> (forall f. Fibred f => f -> Root f
root (forall a (p :: * -> *). Additive a => p a -> Root a -> a
zero' p a
s Root a
r) forall a. Eq a => a -> a -> Bool
== Root a
r) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [])

--------------------------------------------------------------------------------
-- Adbl2 -

-- | predicate for two addable summands.
data Adbl2 a = Adbl2 a a deriving (Int -> Adbl2 a -> ShowS
forall a. Show a => Int -> Adbl2 a -> ShowS
forall a. Show a => [Adbl2 a] -> ShowS
forall a. Show a => Adbl2 a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Adbl2 a] -> ShowS
$cshowList :: forall a. Show a => [Adbl2 a] -> ShowS
show :: Adbl2 a -> String
$cshow :: forall a. Show a => Adbl2 a -> String
showsPrec :: Int -> Adbl2 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Adbl2 a -> ShowS
Show,Adbl2 a -> Adbl2 a -> Bool
forall a. Eq a => Adbl2 a -> Adbl2 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Adbl2 a -> Adbl2 a -> Bool
$c/= :: forall a. Eq a => Adbl2 a -> Adbl2 a -> Bool
== :: Adbl2 a -> Adbl2 a -> Bool
$c== :: forall a. Eq a => Adbl2 a -> Adbl2 a -> Bool
Eq,Adbl2 a -> Adbl2 a -> Bool
Adbl2 a -> Adbl2 a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Adbl2 a)
forall a. Ord a => Adbl2 a -> Adbl2 a -> Bool
forall a. Ord a => Adbl2 a -> Adbl2 a -> Ordering
forall a. Ord a => Adbl2 a -> Adbl2 a -> Adbl2 a
min :: Adbl2 a -> Adbl2 a -> Adbl2 a
$cmin :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Adbl2 a
max :: Adbl2 a -> Adbl2 a -> Adbl2 a
$cmax :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Adbl2 a
>= :: Adbl2 a -> Adbl2 a -> Bool
$c>= :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Bool
> :: Adbl2 a -> Adbl2 a -> Bool
$c> :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Bool
<= :: Adbl2 a -> Adbl2 a -> Bool
$c<= :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Bool
< :: Adbl2 a -> Adbl2 a -> Bool
$c< :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Bool
compare :: Adbl2 a -> Adbl2 a -> Ordering
$ccompare :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Ordering
Ord)

shfAdbl2 :: Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 :: forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 (Adbl2 a
a a
b) = forall f. Root f -> [f] -> Sheaf f
Sheaf (forall f. Fibred f => f -> Root f
root a
a) [a
a,a
b]

instance Fibred a => Validable (Adbl2 a) where
  valid :: Adbl2 a -> Statement
valid = forall a. Validable a => a -> Statement
valid forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2

type instance Dual (Adbl2 a) = Adbl2 (Op a)

instance FibredOriented a => Dualisable (Adbl2 a) where
  toDual :: Adbl2 a -> Dual (Adbl2 a)
toDual Adbl2 a
ab = case forall x. Dualisable x => x -> Dual x
toDual (forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 Adbl2 a
ab) of
    Sheaf Root (Op a)
_ [Op a
a',Op a
b'] -> forall a. a -> a -> Adbl2 a
Adbl2 Op a
a' Op a
b'
    Dual (Sheaf a)
_               -> forall a. HasCallStack => String -> a
error String
implementation

  fromDual :: Dual (Adbl2 a) -> Adbl2 a
fromDual Dual (Adbl2 a)
ab' = case forall x. Dualisable x => Dual x -> x
fromDual (forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 Dual (Adbl2 a)
ab') of
    Sheaf Root a
_ [a
a,a
b] -> forall a. a -> a -> Adbl2 a
Adbl2 a
a a
b
    Sheaf a
_             -> forall a. HasCallStack => String -> a
error String
implementation
  

--------------------------------------------------------------------------------
-- Adbl3 -

-- | predicate for three addable summands.
data Adbl3 a = Adbl3 a a a deriving (Int -> Adbl3 a -> ShowS
forall a. Show a => Int -> Adbl3 a -> ShowS
forall a. Show a => [Adbl3 a] -> ShowS
forall a. Show a => Adbl3 a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Adbl3 a] -> ShowS
$cshowList :: forall a. Show a => [Adbl3 a] -> ShowS
show :: Adbl3 a -> String
$cshow :: forall a. Show a => Adbl3 a -> String
showsPrec :: Int -> Adbl3 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Adbl3 a -> ShowS
Show,Adbl3 a -> Adbl3 a -> Bool
forall a. Eq a => Adbl3 a -> Adbl3 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Adbl3 a -> Adbl3 a -> Bool
$c/= :: forall a. Eq a => Adbl3 a -> Adbl3 a -> Bool
== :: Adbl3 a -> Adbl3 a -> Bool
$c== :: forall a. Eq a => Adbl3 a -> Adbl3 a -> Bool
Eq,Adbl3 a -> Adbl3 a -> Bool
Adbl3 a -> Adbl3 a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Adbl3 a)
forall a. Ord a => Adbl3 a -> Adbl3 a -> Bool
forall a. Ord a => Adbl3 a -> Adbl3 a -> Ordering
forall a. Ord a => Adbl3 a -> Adbl3 a -> Adbl3 a
min :: Adbl3 a -> Adbl3 a -> Adbl3 a
$cmin :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Adbl3 a
max :: Adbl3 a -> Adbl3 a -> Adbl3 a
$cmax :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Adbl3 a
>= :: Adbl3 a -> Adbl3 a -> Bool
$c>= :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Bool
> :: Adbl3 a -> Adbl3 a -> Bool
$c> :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Bool
<= :: Adbl3 a -> Adbl3 a -> Bool
$c<= :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Bool
< :: Adbl3 a -> Adbl3 a -> Bool
$c< :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Bool
compare :: Adbl3 a -> Adbl3 a -> Ordering
$ccompare :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Ordering
Ord)

shfAdbl3 :: Fibred a => Adbl3 a -> Sheaf a
shfAdbl3 :: forall a. Fibred a => Adbl3 a -> Sheaf a
shfAdbl3 (Adbl3 a
a a
b a
c) = forall f. Root f -> [f] -> Sheaf f
Sheaf (forall f. Fibred f => f -> Root f
root a
a) [a
a,a
b,a
c]

instance Fibred a => Validable (Adbl3 a) where
  valid :: Adbl3 a -> Statement
valid = forall a. Validable a => a -> Statement
valid forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Fibred a => Adbl3 a -> Sheaf a
shfAdbl3

type instance Dual (Adbl3 a) = Adbl3 (Op a)

instance FibredOriented a => Dualisable (Adbl3 a) where
  toDual :: Adbl3 a -> Dual (Adbl3 a)
toDual Adbl3 a
abc = case forall x. Dualisable x => x -> Dual x
toDual (forall a. Fibred a => Adbl3 a -> Sheaf a
shfAdbl3 Adbl3 a
abc) of
    Sheaf Root (Op a)
_ [Op a
a',Op a
b',Op a
c'] -> forall a. a -> a -> a -> Adbl3 a
Adbl3 Op a
a' Op a
b' Op a
c'
    Dual (Sheaf a)
_                  -> forall a. HasCallStack => String -> a
error String
implementation
  fromDual :: Dual (Adbl3 a) -> Adbl3 a
fromDual Dual (Adbl3 a)
abc' = case forall x. Dualisable x => Dual x -> x
fromDual (forall a. Fibred a => Adbl3 a -> Sheaf a
shfAdbl3 Dual (Adbl3 a)
abc') of
    Sheaf Root a
_ [a
a,a
b,a
c] -> forall a. a -> a -> a -> Adbl3 a
Adbl3 a
a a
b a
c
    Sheaf a
_               -> forall a. HasCallStack => String -> a
error String
implementation

--------------------------------------------------------------------------------
-- prpAdd2_1 -

-- | validity of '+' for two addable summands according to
--   "OAlg.Structure.Additive.Definition#Add2_1".
prpAdd2_1 :: Additive a => Adbl2 a -> Statement
prpAdd2_1 :: forall a. Additive a => Adbl2 a -> Statement
prpAdd2_1 a :: Adbl2 a
a@(Adbl2 a
f a
g) = String -> Label
Prp String
"Add2_1"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
fg
            , (forall f. Fibred f => f -> Root f
root a
fg forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root a
f)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show Adbl2 a
a]
            ]
  where fg :: a
fg = a
f forall a. Additive a => a -> a -> a
+ a
g


--------------------------------------------------------------------------------
-- prpAdd2_2 -

-- | validity of '+' for two not addable summands according to
--   "OAlg.Structure.Additive.Definition#Add2_2".
prpAdd2_2 :: Additive a => a -> a -> Statement
prpAdd2_2 :: forall a. Additive a => a -> a -> Statement
prpAdd2_2 a
f a
g = String -> Label
Prp String
"Add2_2"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement -> Statement
Not Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid
            , Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nab
            ]
  where vfg :: Statement
vfg = forall a. Validable a => a -> Statement
valid (a
f forall a. Additive a => a -> a -> a
+ a
g)
        nab :: ArithmeticException -> Statement
nab ArithmeticException
NotAddable = Statement
SValid
        nab ArithmeticException
_          = Statement
SInvalid
        
--------------------------------------------------------------------------------
-- prpAdd2 -

-- | validtiy of two summands according to "OAlg.Structure.Additive.Definition#Add2".
prpAdd2 :: Additive a => X (a,a) -> Statement
prpAdd2 :: forall a. Additive a => X (a, a) -> Statement
prpAdd2 X (a, a)
xfg = String -> Label
Prp String
"Add2"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (a, a)
xfg (\(a
f,a
g)
                    -> let fg :: Adbl2 a
fg = forall a. a -> a -> Adbl2 a
Adbl2 a
f a
g
                        in [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Adbl2 a
fg       Statement -> Statement -> Statement
|~> forall a. Additive a => Adbl2 a -> Statement
prpAdd2_1 Adbl2 a
fg
                               , Statement -> Statement
Not (forall a. Validable a => a -> Statement
valid Adbl2 a
fg) Statement -> Statement -> Statement
|~> forall a. Additive a => a -> a -> Statement
prpAdd2_2 a
f a
g
                               ]
                   )

--------------------------------------------------------------------------------
-- prpAdd3 -

-- | validtiy of two adable summands according to "OAlg.Structure.Additive.Definition#Add3".
prpAdd3 :: Additive a => X (Adbl2 a) -> Statement
prpAdd3 :: forall a. Additive a => X (Adbl2 a) -> Statement
prpAdd3 X (Adbl2 a)
xfg = String -> Label
Prp String
"Add3"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Adbl2 a)
xfg (\a :: Adbl2 a
a@(Adbl2 a
f a
g) -> (a
f forall a. Additive a => a -> a -> a
+ a
g forall a. Eq a => a -> a -> Bool
== a
g forall a. Additive a => a -> a -> a
+ a
f)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show Adbl2 a
a])

--------------------------------------------------------------------------------
-- prpAdd4 -

-- | validtiy according to "OAlg.Structure.Additive.Definition#Add4".
prpAdd4 :: Additive a => X a -> Statement
prpAdd4 :: forall a. Additive a => X a -> Statement
prpAdd4 X a
xa = String -> Label
Prp String
"Add4"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X a
xa (\a
f -> (a
f forall a. Additive a => a -> a -> a
+ forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
f) forall a. Eq a => a -> a -> Bool
== a
f)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f])

--------------------------------------------------------------------------------
-- prpAdd5 -

-- | validtiy of three adable summands according to "OAlg.Structure.Additive.Definition#Add5".
prpAdd5 :: Additive a => X (Adbl3 a) -> Statement
prpAdd5 :: forall a. Additive a => X (Adbl3 a) -> Statement
prpAdd5 X (Adbl3 a)
xfgh = String -> Label
Prp String
"Add5"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Adbl3 a)
xfgh (\a :: Adbl3 a
a@(Adbl3 a
f a
g a
h)
                     -> ((a
f forall a. Additive a => a -> a -> a
+ a
g) forall a. Additive a => a -> a -> a
+ a
h forall a. Eq a => a -> a -> Bool
== a
f forall a. Additive a => a -> a -> a
+ (a
g forall a. Additive a => a -> a -> a
+ a
h))
                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show Adbl3 a
a]
                    )

--------------------------------------------------------------------------------
-- prpAdd6 -

-- | validity of 'ntimes' according to "OAlg.Structure.Additive.Definition#Add6".
prpAdd6 :: Additive a => X N -> X a -> Statement
prpAdd6 :: forall a. Additive a => X N -> X a -> Statement
prpAdd6 X N
xn X a
xa = String -> Label
Prp String
"Add6"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (N, a)
xnf (\(N
n,a
f)
                    -> [Statement] -> Statement
And [ (forall a. Additive a => N -> a -> a
ntimes N
0 a
f forall a. Eq a => a -> a -> Bool
== forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
f))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f]
                           , (forall a. Additive a => N -> a -> a
ntimes (N
nforall a. Additive a => a -> a -> a
+N
1) a
f forall a. Eq a => a -> a -> Bool
== a
f forall a. Additive a => a -> a -> a
+ forall a. Additive a => N -> a -> a
ntimes N
n a
f)
                             Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"n"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n,String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f]
                           ]
                   )
  where xnf :: X (N, a)
xnf = forall a b. X a -> X b -> X (a, b)
xTupple2 X N
xn X a
xa

--------------------------------------------------------------------------------
-- XAdd -

-- | random variable for validating 'Additive' structures.
data XAdd a = XAdd (X N) (X (Root a)) (X a) (X (Adbl2 a)) (X (Adbl3 a))

instance Additive a => Validable (XAdd a) where
  valid :: XAdd a -> Statement
valid (XAdd X N
xn X (Root a)
xr X a
xa X (Adbl2 a)
xa2 X (Adbl3 a)
xa3)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid X N
xn
          , forall a. Validable a => a -> Statement
valid X (Root a)
xr
          , forall a. Validable a => a -> Statement
valid X a
xa
          , forall a. Validable a => a -> Statement
valid X (Adbl2 a)
xa2
          , forall a. Validable a => a -> Statement
valid X (Adbl3 a)
xa3
          ]

--------------------------------------------------------------------------------
-- XStandardAdd -

-- | standard random variable for 'Additive' structures.
class XStandardAdd a where
  xStandardAdd :: XAdd a

--------------------------------------------------------------------------------
-- prpAdd -

-- | validity of the 'Additive' structure of @__a__@.
--
-- __Note__ For a good choice of @'X' 'N'@ see the note of 'prpAdd6'.
prpAdd :: Additive a => XAdd a -> Statement
prpAdd :: forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd X N
xn X (Root a)
xr X a
xa X (Adbl2 a)
xa2 X (Adbl3 a)
xa3) = String -> Label
Prp String
"Add"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a (p :: * -> *).
Additive a =>
p a -> X (Root a) -> Statement
prpAdd1 X a
xa X (Root a)
xr
            , forall a. Additive a => X (a, a) -> Statement
prpAdd2 X (a, a)
xfg
            , forall a. Additive a => X (Adbl2 a) -> Statement
prpAdd3 X (Adbl2 a)
xa2
            , forall a. Additive a => X a -> Statement
prpAdd4 X a
xa
            , forall a. Additive a => X (Adbl3 a) -> Statement
prpAdd5 X (Adbl3 a)
xa3
            , forall a. Additive a => X N -> X a -> Statement
prpAdd6 X N
xn X a
xa
            ]
  where xfg :: X (a, a)
xfg = forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xa X a
xa forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Adbl2 a
f a
g) -> (a
f,a
g)) X (Adbl2 a)
xa2


--------------------------------------------------------------------------------
-- xAddTtl -

-- | random variable for total 'Additive' structures.
xAddTtl :: Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl :: forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn X a
xa = forall a.
X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
XAdd X N
xn X (Root a)
xr X a
xa X (Adbl2 a)
xa2 X (Adbl3 a)
xa3 where
  xr :: X (Root a)
xr  = forall (m :: * -> *) a. Monad m => a -> m a
return forall s. Singleton s => s
unit
  xa2 :: X (Adbl2 a)
xa2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. a -> a -> Adbl2 a
Adbl2) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xa X a
xa
  xa3 :: X (Adbl3 a)
xa3 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall a. a -> a -> a -> Adbl3 a
Adbl3) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X a
xa X a
xa X a
xa

instance XStandardAdd N where
  xStandardAdd :: XAdd N
xStandardAdd = forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
1000

instance XStandardAdd Z where
  xStandardAdd :: XAdd Z
xStandardAdd = forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
1000

instance XStandardAdd Q where
  xStandardAdd :: XAdd Q
xStandardAdd = forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
1000

--------------------------------------------------------------------------------
-- xStalkAdbl2 -

-- | random variable of two addable summands rooted at the given root.
xStalkAdbl2 :: Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 :: forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk a
xs Root a
r = do
  Sheaf Root a
_ [a
a,a
b] <- forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs N
2 Root a
r
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> a -> Adbl2 a
Adbl2 a
a a
b

--------------------------------------------------------------------------------
-- xStalkAdbl3 -

-- | random variable of three addable summands rooted in the given root.
xStalkAdbl3 :: Additive a => XStalk a -> Root a -> X (Adbl3 a)
xStalkAdbl3 :: forall a. Additive a => XStalk a -> Root a -> X (Adbl3 a)
xStalkAdbl3 XStalk a
xs Root a
r = do
  Sheaf Root a
_ [a
a,a
b,a
c] <- forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs N
3 Root a
r
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> a -> a -> Adbl3 a
Adbl3 a
a a
b a
c

--------------------------------------------------------------------------------
-- xAddStalk -

-- | random variable for 'Additive' structure.
xAddStalk :: Additive a => XStalk a -> X N -> XAdd a
xAddStalk :: forall a. Additive a => XStalk a -> X N -> XAdd a
xAddStalk xs :: XStalk a
xs@(XStalk X (Root a)
xr Root a -> X a
_) X N
xn = forall a.
X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
XAdd X N
xn X (Root a)
xr X a
xa X (Adbl2 a)
xa2 X (Adbl3 a)
xa3 where
  xa :: X a
xa  = do
    Sheaf Root a
_ [a
s] <- forall a. Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf XStalk a
xs N
1
    forall (m :: * -> *) a. Monad m => a -> m a
return a
s
  xa2 :: X (Adbl2 a)
xa2 = X (Root a)
xr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk a
xs
  xa3 :: X (Adbl3 a)
xa3 = X (Root a)
xr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Additive a => XStalk a -> Root a -> X (Adbl3 a)
xStalkAdbl3 XStalk a
xs


--------------------------------------------------------------------------------
-- xAddOrnt -

-- | random variable for the 'Additive' structure of @'Orientation' __p__@.
xAddOrnt :: Entity p => X N -> X p -> XAdd (Orientation p)
xAddOrnt :: forall p. Entity p => X N -> X p -> XAdd (Orientation p)
xAddOrnt X N
xn X p
xp = forall a. Additive a => XStalk a -> X N -> XAdd a
xAddStalk (forall p. X p -> XStalk (Orientation p)
xStalkOrnt X p
xp) X N
xn

instance (Entity p, XStandard p) => XStandardAdd (Orientation p) where
  xStandardAdd :: XAdd (Orientation p)
xStandardAdd = forall p. Entity p => X N -> X p -> XAdd (Orientation p)
xAddOrnt X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
1000

--------------------------------------------------------------------------------
-- prpAbl1 -

-- | validity according to "OAlg.Structure.Additive.Definition#Abl1".
prpAbl1 :: Abelian a => X a -> Statement
prpAbl1 :: forall a. Abelian a => X a -> Statement
prpAbl1 X a
xf = String -> Label
Prp String
"Abl1"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X a
xf (\a
f -> (forall f. Fibred f => f -> Root f
root (forall a. Abelian a => a -> a
negate a
f) forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root a
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f]) 

--------------------------------------------------------------------------------
-- prpAbl2 -

-- | validity according to "OAlg.Structure.Additive.Definition#Abl2".
prpAbl2 :: Abelian a => X a -> Statement
prpAbl2 :: forall a. Abelian a => X a -> Statement
prpAbl2 X a
xf = String -> Label
Prp String
"Abl2"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X a
xf (\a
f -> (a
f forall a. Additive a => a -> a -> a
+ forall a. Abelian a => a -> a
negate a
f forall a. Eq a => a -> a -> Bool
== forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root a
f))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f])

--------------------------------------------------------------------------------
-- prpAbl3_1 -

-- | validity of '-' for two addable summands according to
--   "OAlg.Structure.Additive.Definition#Abl3_1".
prpAbl3_1 :: Abelian a => Adbl2 a -> Statement
prpAbl3_1 :: forall a. Abelian a => Adbl2 a -> Statement
prpAbl3_1 a :: Adbl2 a
a@(Adbl2 a
f a
g) = String -> Label
Prp String
"Adbl3_1"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
fg
            , (forall f. Fibred f => f -> Root f
root a
fg forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root a
f)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show Adbl2 a
a]
            ]
  where fg :: a
fg = a
f forall a. Abelian a => a -> a -> a
- a
g

--------------------------------------------------------------------------------
-- prpAbl3_2 -

-- | validity of '-' for two not addable summands according to
--   "OAlg.Structure.Additive.Definition#Abl3_2".
prpAbl3_2 :: Abelian a => a -> a -> Statement
prpAbl3_2 :: forall a. Abelian a => a -> a -> Statement
prpAbl3_2 a
f a
g = String -> Label
Prp String
"Abl3_2"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement -> Statement
Not Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid
            , Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nab
            ]
  where vfg :: Statement
vfg = forall a. Validable a => a -> Statement
valid (a
f forall a. Abelian a => a -> a -> a
- a
g)
        nab :: ArithmeticException -> Statement
nab ArithmeticException
NotAddable = Statement
SValid
        nab ArithmeticException
_          = Statement
SInvalid

--------------------------------------------------------------------------------
-- prpAbl3 -

-- | validity of two summands according to "OAlg.Structure.Additive.Definition#Abl3".
prpAbl3 :: Abelian a => X (a,a) -> Statement
prpAbl3 :: forall a. Abelian a => X (a, a) -> Statement
prpAbl3 X (a, a)
xfg = String -> Label
Prp String
"Abl3"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (a, a)
xfg (\(a
f,a
g)
                    -> let fg :: Adbl2 a
fg = forall a. a -> a -> Adbl2 a
Adbl2 a
f a
g
                       in [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Adbl2 a
fg       Statement -> Statement -> Statement
|~> forall a. Abelian a => Adbl2 a -> Statement
prpAbl3_1 Adbl2 a
fg
                              , Statement -> Statement
Not (forall a. Validable a => a -> Statement
valid Adbl2 a
fg) Statement -> Statement -> Statement
|~> forall a. Abelian a => a -> a -> Statement
prpAbl3_2 a
f a
g
                              ]
                   )

--------------------------------------------------------------------------------
-- prpAbl4 -

-- | validity of two summands according to "OAlg.Structure.Additive.Definition#Abl4".
prpAbl4 :: Abelian a => X (Adbl2 a) -> Statement
prpAbl4 :: forall a. Abelian a => X (Adbl2 a) -> Statement
prpAbl4 X (Adbl2 a)
xfg = String -> Label
Prp String
"Abl4"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Adbl2 a)
xfg (\a :: Adbl2 a
a@(Adbl2 a
f a
g)
                    -> (a
f forall a. Abelian a => a -> a -> a
- a
g forall a. Eq a => a -> a -> Bool
== a
f forall a. Additive a => a -> a -> a
+ forall a. Abelian a => a -> a
negate a
g)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=forall a. Show a => a -> String
show Adbl2 a
a]
                   )

--------------------------------------------------------------------------------
-- prpAbl5 -

-- | validity of two summands according to "OAlg.Structure.Additive.Definition#Abl5".
prpAbl5 :: Abelian a => X Z -> X a -> Statement
prpAbl5 :: forall a. Abelian a => X Z -> X a -> Statement
prpAbl5 X Z
xz X a
xf = String -> Label
Prp String
"Abl5"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Z, a)
xzf (\zf :: (Z, a)
zf@(Z
z,a
f)
                    -> ( forall a. Abelian a => Z -> a -> a
ztimes Z
z a
f forall a. Eq a => a -> a -> Bool
== if Z
0 forall a. Ord a => a -> a -> Bool
<= Z
z
                                         then forall a. Additive a => N -> a -> a
ntimes (forall a b. Projectible a b => b -> a
prj Z
z) a
f
                                         else forall a. Abelian a => a -> a
negate (forall a. Additive a => N -> a -> a
ntimes (forall a b. Projectible a b => b -> a
prj Z
z) a
f)
                       )Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(z,f)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Z, a)
zf]
                   )
  where xzf :: X (Z, a)
xzf = forall a b. X a -> X b -> X (a, b)
xTupple2 X Z
xz X a
xf

--------------------------------------------------------------------------------
-- XAbl -

-- | random variable for validating 'Abelian' structures. 
data XAbl a = XAbl (X Z) (X a) (X (Adbl2 a))

instance Additive a => Validable (XAbl a) where
  valid :: XAbl a -> Statement
valid (XAbl X Z
xz X a
xa X (Adbl2 a)
xa2)
    = String -> Label
Label String
"XAbl" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid X Z
xz forall b. Boolean b => b -> b -> b
&& forall a. Validable a => a -> Statement
valid X a
xa forall b. Boolean b => b -> b -> b
&& forall a. Validable a => a -> Statement
valid X (Adbl2 a)
xa2

--------------------------------------------------------------------------------
-- prpAbl -

-- | validity of the 'Abelian' structure of __@a@__.
prpAbl :: Abelian a => XAbl a -> Statement
prpAbl :: forall a. Abelian a => XAbl a -> Statement
prpAbl (XAbl X Z
xz X a
xf X (Adbl2 a)
xa2) = String -> Label
Prp String
"Abl"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a. Abelian a => X a -> Statement
prpAbl1 X a
xf
            , forall a. Abelian a => X a -> Statement
prpAbl2 X a
xf
            , forall a. Abelian a => X (a, a) -> Statement
prpAbl3 X (a, a)
xfg
            , forall a. Abelian a => X (Adbl2 a) -> Statement
prpAbl4 X (Adbl2 a)
xa2
            , forall a. Abelian a => X Z -> X a -> Statement
prpAbl5 X Z
xz X a
xf
            ]
  where xfg :: X (a, a)
xfg = forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xf X a
xf forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Adbl2 a
f a
g) -> (a
f,a
g)) X (Adbl2 a)
xa2


--------------------------------------------------------------------------------
-- xoRoot -

-- | the induced random variables for roots.
xoRoot :: FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot :: forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot = forall q. XOrtOrientation q -> X (Orientation (Point q))
xoOrientation

--------------------------------------------------------------------------------
-- xoAdbl2 -

-- | the induced random variable for two addable summands.
xoAdbl2 :: FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 :: forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation a
xo = do
  Orientation (Point a)
r <- forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  a
a <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
b <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> a -> Adbl2 a
Adbl2 a
a a
b)

--------------------------------------------------------------------------------
-- xoAdbl3 -

-- | the induced random variable for three addable summands.
xoAdbl3 :: FibredOriented a => XOrtOrientation a -> X (Adbl3 a)
xoAdbl3 :: forall a. FibredOriented a => XOrtOrientation a -> X (Adbl3 a)
xoAdbl3 XOrtOrientation a
xo = do
  Orientation (Point a)
r <- forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  a
a <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
b <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
c <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> a -> a -> Adbl3 a
Adbl3 a
a a
b a
c)

--------------------------------------------------------------------------------
-- xoAdd -

-- | the induced random variable for 'Additive' structures with the given random variable to
-- validate 'ntimes'.
xoAdd :: FibredOriented a => X N -> XOrtOrientation a -> XAdd a
xoAdd :: forall a. FibredOriented a => X N -> XOrtOrientation a -> XAdd a
xoAdd X N
xn XOrtOrientation a
xo = forall a.
X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
XAdd X N
xn X (Root a)
xr XFbr a
xa X (Adbl2 a)
xa2 X (Adbl3 a)
xa3 where
  xr :: X (Root a)
xr = forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  xa :: XFbr a
xa = forall f. XOrtOrientation f -> XFbr f
xoFbr XOrtOrientation a
xo
  xa2 :: X (Adbl2 a)
xa2 = forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation a
xo
  xa3 :: X (Adbl3 a)
xa3 = forall a. FibredOriented a => XOrtOrientation a -> X (Adbl3 a)
xoAdbl3 XOrtOrientation a
xo

--------------------------------------------------------------------------------
-- xodAbl -

-- | the induced random variable for 'Abelian' structures with the given random variable to
-- validate 'ztimes'.
xoAbl :: FibredOriented a => X Z -> XOrtOrientation a -> XAbl a
xoAbl :: forall a. FibredOriented a => X Z -> XOrtOrientation a -> XAbl a
xoAbl X Z
xz XOrtOrientation a
xo = forall a. X Z -> X a -> X (Adbl2 a) -> XAbl a
XAbl X Z
xz XFbr a
xa X (Adbl2 a)
xa2 where
  xa :: XFbr a
xa = forall f. XOrtOrientation f -> XFbr f
xoFbr XOrtOrientation a
xo
  xa2 :: X (Adbl2 a)
xa2 = forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation a
xo