{-# 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.Definition
import OAlg.Structure.FibredOriented

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
:<=>: a -> Bool
forall a. Additive a => a -> Bool
isZero a
a Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a -> String
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
:<=>: X (Root a) -> (Root a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Root a)
xr (\Root a
r -> (a -> Root a
forall f. Fibred f => f -> Root f
root (p a -> Root a -> a
forall a (p :: * -> *). Additive a => p a -> Root a -> a
zero' p a
s Root a
r) Root a -> Root a -> Bool
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
[Adbl2 a] -> ShowS
Adbl2 a -> String
(Int -> Adbl2 a -> ShowS)
-> (Adbl2 a -> String) -> ([Adbl2 a] -> ShowS) -> Show (Adbl2 a)
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
$cshowsPrec :: forall a. Show a => Int -> Adbl2 a -> ShowS
showsPrec :: Int -> Adbl2 a -> ShowS
$cshow :: forall a. Show a => Adbl2 a -> String
show :: Adbl2 a -> String
$cshowList :: forall a. Show a => [Adbl2 a] -> ShowS
showList :: [Adbl2 a] -> ShowS
Show,Adbl2 a -> Adbl2 a -> Bool
(Adbl2 a -> Adbl2 a -> Bool)
-> (Adbl2 a -> Adbl2 a -> Bool) -> Eq (Adbl2 a)
forall a. Eq a => Adbl2 a -> Adbl2 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Adbl2 a -> Adbl2 a -> Bool
Eq,Eq (Adbl2 a)
Eq (Adbl2 a) =>
(Adbl2 a -> Adbl2 a -> Ordering)
-> (Adbl2 a -> Adbl2 a -> Bool)
-> (Adbl2 a -> Adbl2 a -> Bool)
-> (Adbl2 a -> Adbl2 a -> Bool)
-> (Adbl2 a -> Adbl2 a -> Bool)
-> (Adbl2 a -> Adbl2 a -> Adbl2 a)
-> (Adbl2 a -> Adbl2 a -> Adbl2 a)
-> Ord (Adbl2 a)
Adbl2 a -> Adbl2 a -> Bool
Adbl2 a -> Adbl2 a -> Ordering
Adbl2 a -> Adbl2 a -> Adbl2 a
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
$ccompare :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Ordering
compare :: Adbl2 a -> Adbl2 a -> Ordering
$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
>= :: Adbl2 a -> Adbl2 a -> Bool
$cmax :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Adbl2 a
max :: Adbl2 a -> Adbl2 a -> Adbl2 a
$cmin :: forall a. Ord a => Adbl2 a -> Adbl2 a -> Adbl2 a
min :: Adbl2 a -> Adbl2 a -> Adbl2 a
Ord)

shfAdbl2 :: Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 :: forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 (Adbl2 a
a a
b) = Root a -> [a] -> Sheaf a
forall f. Root f -> [f] -> Sheaf f
Sheaf (a -> Root a
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 = Sheaf a -> Statement
forall a. Validable a => a -> Statement
valid (Sheaf a -> Statement)
-> (Adbl2 a -> Sheaf a) -> Adbl2 a -> 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
. Adbl2 a -> Sheaf a
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 Sheaf a -> Dual (Sheaf a)
forall x. Dualisable x => x -> Dual x
toDual (Adbl2 a -> Sheaf a
forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 Adbl2 a
ab) of
    Sheaf Root (Op a)
_ [Op a
a',Op a
b'] -> Op a -> Op a -> Adbl2 (Op a)
forall a. a -> a -> Adbl2 a
Adbl2 Op a
a' Op a
b'
    Dual (Sheaf a)
_               -> String -> Adbl2 (Op a)
forall a. HasCallStack => String -> a
error String
implementation

  fromDual :: Dual (Adbl2 a) -> Adbl2 a
fromDual Dual (Adbl2 a)
ab' = case Dual (Sheaf a) -> Sheaf a
forall x. Dualisable x => Dual x -> x
fromDual (Adbl2 (Op a) -> Sheaf (Op a)
forall a. Fibred a => Adbl2 a -> Sheaf a
shfAdbl2 Dual (Adbl2 a)
Adbl2 (Op a)
ab') of
    Sheaf Root a
_ [a
a,a
b] -> a -> a -> Adbl2 a
forall a. a -> a -> Adbl2 a
Adbl2 a
a a
b
    Sheaf a
_             -> String -> Adbl2 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
[Adbl3 a] -> ShowS
Adbl3 a -> String
(Int -> Adbl3 a -> ShowS)
-> (Adbl3 a -> String) -> ([Adbl3 a] -> ShowS) -> Show (Adbl3 a)
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
$cshowsPrec :: forall a. Show a => Int -> Adbl3 a -> ShowS
showsPrec :: Int -> Adbl3 a -> ShowS
$cshow :: forall a. Show a => Adbl3 a -> String
show :: Adbl3 a -> String
$cshowList :: forall a. Show a => [Adbl3 a] -> ShowS
showList :: [Adbl3 a] -> ShowS
Show,Adbl3 a -> Adbl3 a -> Bool
(Adbl3 a -> Adbl3 a -> Bool)
-> (Adbl3 a -> Adbl3 a -> Bool) -> Eq (Adbl3 a)
forall a. Eq a => Adbl3 a -> Adbl3 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Adbl3 a -> Adbl3 a -> Bool
Eq,Eq (Adbl3 a)
Eq (Adbl3 a) =>
(Adbl3 a -> Adbl3 a -> Ordering)
-> (Adbl3 a -> Adbl3 a -> Bool)
-> (Adbl3 a -> Adbl3 a -> Bool)
-> (Adbl3 a -> Adbl3 a -> Bool)
-> (Adbl3 a -> Adbl3 a -> Bool)
-> (Adbl3 a -> Adbl3 a -> Adbl3 a)
-> (Adbl3 a -> Adbl3 a -> Adbl3 a)
-> Ord (Adbl3 a)
Adbl3 a -> Adbl3 a -> Bool
Adbl3 a -> Adbl3 a -> Ordering
Adbl3 a -> Adbl3 a -> Adbl3 a
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
$ccompare :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Ordering
compare :: Adbl3 a -> Adbl3 a -> Ordering
$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
>= :: Adbl3 a -> Adbl3 a -> Bool
$cmax :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Adbl3 a
max :: Adbl3 a -> Adbl3 a -> Adbl3 a
$cmin :: forall a. Ord a => Adbl3 a -> Adbl3 a -> Adbl3 a
min :: Adbl3 a -> Adbl3 a -> Adbl3 a
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) = Root a -> [a] -> Sheaf a
forall f. Root f -> [f] -> Sheaf f
Sheaf (a -> Root a
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 = Sheaf a -> Statement
forall a. Validable a => a -> Statement
valid (Sheaf a -> Statement)
-> (Adbl3 a -> Sheaf a) -> Adbl3 a -> 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
. Adbl3 a -> Sheaf a
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 Sheaf a -> Dual (Sheaf a)
forall x. Dualisable x => x -> Dual x
toDual (Adbl3 a -> Sheaf a
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'] -> Op a -> Op a -> Op a -> Adbl3 (Op a)
forall a. a -> a -> a -> Adbl3 a
Adbl3 Op a
a' Op a
b' Op a
c'
    Dual (Sheaf a)
_                  -> String -> Adbl3 (Op a)
forall a. HasCallStack => String -> a
error String
implementation
  fromDual :: Dual (Adbl3 a) -> Adbl3 a
fromDual Dual (Adbl3 a)
abc' = case Dual (Sheaf a) -> Sheaf a
forall x. Dualisable x => Dual x -> x
fromDual (Adbl3 (Op a) -> Sheaf (Op a)
forall a. Fibred a => Adbl3 a -> Sheaf a
shfAdbl3 Dual (Adbl3 a)
Adbl3 (Op a)
abc') of
    Sheaf Root a
_ [a
a,a
b,a
c] -> a -> a -> a -> Adbl3 a
forall a. a -> a -> a -> Adbl3 a
Adbl3 a
a a
b a
c
    Sheaf a
_               -> String -> Adbl3 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 [ a -> Statement
forall a. Validable a => a -> Statement
valid a
fg
            , (a -> Root a
forall f. Fibred f => f -> Root f
root a
fg Root a -> Root a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Root a
forall f. Fibred f => f -> Root f
root a
f)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Adbl2 a -> String
forall a. Show a => a -> String
show Adbl2 a
a]
            ]
  where fg :: a
fg = a
f a -> a -> a
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 Statement -> (SomeException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid
            , Statement
vfg Statement -> (ArithmeticException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nab
            ]
  where vfg :: Statement
vfg = a -> Statement
forall a. Validable a => a -> Statement
valid (a
f a -> a -> a
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
:<=>: X (a, a) -> ((a, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (a, a)
xfg (\(a
f,a
g)
                    -> let fg :: Adbl2 a
fg = a -> a -> Adbl2 a
forall a. a -> a -> Adbl2 a
Adbl2 a
f a
g
                        in [Statement] -> Statement
And [ Adbl2 a -> Statement
forall a. Validable a => a -> Statement
valid Adbl2 a
fg       Statement -> Statement -> Statement
|~> Adbl2 a -> Statement
forall a. Additive a => Adbl2 a -> Statement
prpAdd2_1 Adbl2 a
fg
                               , Statement -> Statement
Not (Adbl2 a -> Statement
forall a. Validable a => a -> Statement
valid Adbl2 a
fg) Statement -> Statement -> Statement
|~> a -> a -> 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
:<=>: X (Adbl2 a) -> (Adbl2 a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Adbl2 a)
xfg (\a :: Adbl2 a
a@(Adbl2 a
f a
g) -> (a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ a
g a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
g a -> a -> a
forall a. Additive a => a -> a -> a
+ a
f)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Adbl2 a -> String
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
:<=>: X a -> (a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X a
xa (\a
f -> (a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
forall f. Fibred f => f -> Root f
root a
f) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
f)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=a -> String
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
:<=>: X (Adbl3 a) -> (Adbl3 a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Adbl3 a)
xfgh (\a :: Adbl3 a
a@(Adbl3 a
f a
g a
h)
                     -> ((a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ a
g) a -> a -> a
forall a. Additive a => a -> a -> a
+ a
h a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ (a
g a -> a -> a
forall a. Additive a => a -> a -> a
+ a
h))
                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Adbl3 a -> String
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
:<=>: X (N, a) -> ((N, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (N, a)
xnf (\(N
n,a
f)
                    -> [Statement] -> Statement
And [ (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes N
0 a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
forall f. Fibred f => f -> Root f
root a
f))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
f]
                           , (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes (N
nN -> N -> N
forall a. Additive a => a -> a -> a
+N
1) a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ N -> 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
:=N -> String
forall a. Show a => a -> String
show N
n,String
"f"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
f]
                           ]
                   )
  where xnf :: X (N, a)
xnf = X N -> X a -> X (N, a)
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 [ X N -> Statement
forall a. Validable a => a -> Statement
valid X N
xn
          , X (Root a) -> Statement
forall a. Validable a => a -> Statement
valid X (Root a)
xr
          , X a -> Statement
forall a. Validable a => a -> Statement
valid X a
xa
          , X (Adbl2 a) -> Statement
forall a. Validable a => a -> Statement
valid X (Adbl2 a)
xa2
          , X (Adbl3 a) -> Statement
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

instance (FibredOriented x, XStandardAdd x) => XStandardAdd (Op x) where
  xStandardAdd :: XAdd (Op x)
xStandardAdd = X N
-> X (Root (Op x))
-> X (Op x)
-> X (Adbl2 (Op x))
-> X (Adbl3 (Op x))
-> XAdd (Op x)
forall a.
X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
XAdd X N
xn X (Root x)
X (Root (Op x))
xr' X (Op x)
xa' X (Adbl2 (Op x))
xa2' X (Adbl3 (Op x))
xa3' where
    XAdd X N
xn X (Root x)
xr X x
xa X (Adbl2 x)
xa2 X (Adbl3 x)
xa3 = XAdd x
forall a. XStandardAdd a => XAdd a
xStandardAdd
    xr' :: X (Root x)
xr' = X (Root x)
xr
    xa' :: X (Op x)
xa'  = (x -> Op x) -> X x -> X (Op x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Op x
forall x. x -> Op x
Op X x
xa
    xa2' :: X (Adbl2 (Op x))
xa2' = (Adbl2 x -> Adbl2 (Op x)) -> X (Adbl2 x) -> X (Adbl2 (Op x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Adbl2 x
a x
b) -> Op x -> Op x -> Adbl2 (Op x)
forall a. a -> a -> Adbl2 a
Adbl2 (x -> Op x
forall x. x -> Op x
Op x
a) (x -> Op x
forall x. x -> Op x
Op x
b)) X (Adbl2 x)
xa2
    xa3' :: X (Adbl3 (Op x))
xa3' = (Adbl3 x -> Adbl3 (Op x)) -> X (Adbl3 x) -> X (Adbl3 (Op x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Adbl3 x
a x
b x
c) -> Op x -> Op x -> Op x -> Adbl3 (Op x)
forall a. a -> a -> a -> Adbl3 a
Adbl3 (x -> Op x
forall x. x -> Op x
Op x
a) (x -> Op x
forall x. x -> Op x
Op x
b) (x -> Op x
forall x. x -> Op x
Op x
c)) X (Adbl3 x)
xa3
  
instance XStandardAdd x => XStandardAdd (Id x) where
  xStandardAdd :: XAdd (Id x)
xStandardAdd = X N
-> X (Root (Id x))
-> X (Id x)
-> X (Adbl2 (Id x))
-> X (Adbl3 (Id x))
-> XAdd (Id x)
forall a.
X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
XAdd X N
xn X (Root x)
X (Root (Id x))
xr X (Id x)
xa' X (Adbl2 (Id x))
xa2' X (Adbl3 (Id x))
xa3' where
    XAdd X N
xn X (Root x)
xr X x
xa X (Adbl2 x)
xa2 X (Adbl3 x)
xa3 = XAdd x
forall a. XStandardAdd a => XAdd a
xStandardAdd
    xa' :: X (Id x)
xa'  = (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
xa
    xa2' :: X (Adbl2 (Id x))
xa2' = (Adbl2 x -> Adbl2 (Id x)) -> X (Adbl2 x) -> X (Adbl2 (Id x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Adbl2 x
a x
b) -> Id x -> Id x -> Adbl2 (Id x)
forall a. a -> a -> Adbl2 a
Adbl2 (x -> Id x
forall x. x -> Id x
Id x
a) (x -> Id x
forall x. x -> Id x
Id x
b)) X (Adbl2 x)
xa2
    xa3' :: X (Adbl3 (Id x))
xa3' = (Adbl3 x -> Adbl3 (Id x)) -> X (Adbl3 x) -> X (Adbl3 (Id x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Adbl3 x
a x
b x
c) -> Id x -> Id x -> Id x -> Adbl3 (Id x)
forall a. a -> a -> a -> Adbl3 a
Adbl3 (x -> Id x
forall x. x -> Id x
Id x
a) (x -> Id x
forall x. x -> Id x
Id x
b) (x -> Id x
forall x. x -> Id x
Id x
c)) X (Adbl3 x)
xa3
  
--------------------------------------------------------------------------------
-- 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 [ X a -> X (Root a) -> Statement
forall a (p :: * -> *).
Additive a =>
p a -> X (Root a) -> Statement
prpAdd1 X a
xa X (Root a)
xr
            , X (a, a) -> Statement
forall a. Additive a => X (a, a) -> Statement
prpAdd2 X (a, a)
xfg
            , X (Adbl2 a) -> Statement
forall a. Additive a => X (Adbl2 a) -> Statement
prpAdd3 X (Adbl2 a)
xa2
            , X a -> Statement
forall a. Additive a => X a -> Statement
prpAdd4 X a
xa
            , X (Adbl3 a) -> Statement
forall a. Additive a => X (Adbl3 a) -> Statement
prpAdd5 X (Adbl3 a)
xa3
            , X N -> X a -> Statement
forall a. Additive a => X N -> X a -> Statement
prpAdd6 X N
xn X a
xa
            ]
  where xfg :: X (a, a)
xfg = X a -> X a -> X (a, a)
forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xa X a
xa X (a, a) -> X (a, a) -> X (a, a)
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Adbl2 a -> (a, a)) -> X (Adbl2 a) -> X (a, a)
forall a b. (a -> b) -> X a -> X b
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 = X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
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  = Root a -> X (Root a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Root a
forall s. Singleton s => s
unit
  xa2 :: X (Adbl2 a)
xa2 = ((a, a) -> Adbl2 a) -> X (a, a) -> X (Adbl2 a)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a -> Adbl2 a) -> (a, a) -> Adbl2 a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Adbl2 a
forall a. a -> a -> Adbl2 a
Adbl2) (X (a, a) -> X (Adbl2 a)) -> X (a, a) -> X (Adbl2 a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X a -> X a -> X (a, a)
forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xa X a
xa
  xa3 :: X (Adbl3 a)
xa3 = ((a, a, a) -> Adbl3 a) -> X (a, a, a) -> X (Adbl3 a)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a -> a -> Adbl3 a) -> (a, a, a) -> Adbl3 a
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 a -> a -> a -> Adbl3 a
forall a. a -> a -> a -> Adbl3 a
Adbl3) (X (a, a, a) -> X (Adbl3 a)) -> X (a, a, a) -> X (Adbl3 a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X a -> X a -> X a -> X (a, a, a)
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 = X N -> X N -> XAdd N
forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn X N
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 = X N -> X Z -> XAdd Z
forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn X Z
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 = X N -> X Q -> XAdd Q
forall a. Singleton (Root a) => X N -> X a -> XAdd a
xAddTtl X N
xn X Q
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] <- XStalk a -> N -> Root a -> X (Sheaf a)
forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs N
2 Root a
r
  Adbl2 a -> X (Adbl2 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Adbl2 a -> X (Adbl2 a)) -> Adbl2 a -> X (Adbl2 a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ a -> a -> Adbl2 a
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] <- XStalk a -> N -> Root a -> X (Sheaf a)
forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs N
3 Root a
r
  Adbl3 a -> X (Adbl3 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Adbl3 a -> X (Adbl3 a)) -> Adbl3 a -> X (Adbl3 a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ a -> a -> a -> Adbl3 a
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 = X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
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] <- XStalk a -> N -> X (Sheaf a)
forall a. Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf XStalk a
xs N
1
    a -> X a
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return a
s
  xa2 :: X (Adbl2 a)
xa2 = X (Root a)
xr X (Root a) -> (Root a -> X (Adbl2 a)) -> X (Adbl2 a)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XStalk a -> Root a -> X (Adbl2 a)
forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk a
xs
  xa3 :: X (Adbl3 a)
xa3 = X (Root a)
xr X (Root a) -> (Root a -> X (Adbl3 a)) -> X (Adbl3 a)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XStalk a -> Root a -> X (Adbl3 a)
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 = XStalk (Orientation p) -> X N -> XAdd (Orientation p)
forall a. Additive a => XStalk a -> X N -> XAdd a
xAddStalk (X p -> XStalk (Orientation p)
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 = X N -> X p -> XAdd (Orientation p)
forall p. Entity p => X N -> X p -> XAdd (Orientation p)
xAddOrnt X N
xn X p
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
:<=>: X a -> (a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X a
xf (\a
f -> (a -> Root a
forall f. Fibred f => f -> Root f
root (a -> a
forall a. Abelian a => a -> a
negate a
f) Root a -> Root a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Root a
forall f. Fibred f => f -> Root f
root a
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=a -> String
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
:<=>: X a -> (a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X a
xf (\a
f -> (a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ a -> a
forall a. Abelian a => a -> a
negate a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Root a -> a
forall a. Additive a => Root a -> a
zero (a -> Root a
forall f. Fibred f => f -> Root f
root a
f))Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=a -> String
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 [ a -> Statement
forall a. Validable a => a -> Statement
valid a
fg
            , (a -> Root a
forall f. Fibred f => f -> Root f
root a
fg Root a -> Root a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Root a
forall f. Fibred f => f -> Root f
root a
f)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Adbl2 a -> String
forall a. Show a => a -> String
show Adbl2 a
a]
            ]
  where fg :: a
fg = a
f a -> a -> a
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 Statement -> (SomeException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid
            , Statement
vfg Statement -> (ArithmeticException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nab
            ]
  where vfg :: Statement
vfg = a -> Statement
forall a. Validable a => a -> Statement
valid (a
f a -> a -> a
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
:<=>: X (a, a) -> ((a, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (a, a)
xfg (\(a
f,a
g)
                    -> let fg :: Adbl2 a
fg = a -> a -> Adbl2 a
forall a. a -> a -> Adbl2 a
Adbl2 a
f a
g
                       in [Statement] -> Statement
And [ Adbl2 a -> Statement
forall a. Validable a => a -> Statement
valid Adbl2 a
fg       Statement -> Statement -> Statement
|~> Adbl2 a -> Statement
forall a. Abelian a => Adbl2 a -> Statement
prpAbl3_1 Adbl2 a
fg
                              , Statement -> Statement
Not (Adbl2 a -> Statement
forall a. Validable a => a -> Statement
valid Adbl2 a
fg) Statement -> Statement -> Statement
|~> a -> a -> 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
:<=>: X (Adbl2 a) -> (Adbl2 a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Adbl2 a)
xfg (\a :: Adbl2 a
a@(Adbl2 a
f a
g)
                    -> (a
f a -> a -> a
forall a. Abelian a => a -> a -> a
- a
g a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
f a -> a -> a
forall a. Additive a => a -> a -> a
+ a -> a
forall a. Abelian a => a -> a
negate a
g)Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Adbl2 a -> String
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
:<=>: X (Z, a) -> ((Z, a) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Z, a)
xzf (\zf :: (Z, a)
zf@(Z
z,a
f)
                    -> ( Z -> a -> a
forall a. Abelian a => Z -> a -> a
ztimes Z
z a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== if Z
0 Z -> Z -> Bool
forall a. Ord a => a -> a -> Bool
<= Z
z
                                         then N -> a -> a
forall a. Additive a => N -> a -> a
ntimes (Z -> N
forall a b. Projectible a b => b -> a
prj Z
z) a
f
                                         else a -> a
forall a. Abelian a => a -> a
negate (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes (Z -> N
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
:=(Z, a) -> String
forall a. Show a => a -> String
show (Z, a)
zf]
                   )
  where xzf :: X (Z, a)
xzf = X Z -> X a -> X (Z, a)
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
:<=>: X Z -> Statement
forall a. Validable a => a -> Statement
valid X Z
xz Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& X a -> Statement
forall a. Validable a => a -> Statement
valid X a
xa Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& X (Adbl2 a) -> Statement
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 [ X a -> Statement
forall a. Abelian a => X a -> Statement
prpAbl1 X a
xf
            , X a -> Statement
forall a. Abelian a => X a -> Statement
prpAbl2 X a
xf
            , X (a, a) -> Statement
forall a. Abelian a => X (a, a) -> Statement
prpAbl3 X (a, a)
xfg
            , X (Adbl2 a) -> Statement
forall a. Abelian a => X (Adbl2 a) -> Statement
prpAbl4 X (Adbl2 a)
xa2
            , X Z -> X a -> Statement
forall a. Abelian a => X Z -> X a -> Statement
prpAbl5 X Z
xz X a
xf
            ]
  where xfg :: X (a, a)
xfg = X a -> X a -> X (a, a)
forall a b. X a -> X b -> X (a, b)
xTupple2 X a
xf X a
xf X (a, a) -> X (a, a) -> X (a, a)
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Adbl2 a -> (a, a)) -> X (Adbl2 a) -> X (a, a)
forall a b. (a -> b) -> X a -> X b
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 = XOrtOrientation a -> X (Orientation (Point a))
XOrtOrientation a -> X (Root a)
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 <- XOrtOrientation a -> X (Root a)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  a
a <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
b <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  Adbl2 a -> X (Adbl2 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> a -> Adbl2 a
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 <- XOrtOrientation a -> X (Root a)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  a
a <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
b <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  a
c <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo Orientation (Point a)
r
  Adbl3 a -> X (Adbl3 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> a -> a -> Adbl3 a
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 = X N -> X (Root a) -> X a -> X (Adbl2 a) -> X (Adbl3 a) -> XAdd a
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 = XOrtOrientation a -> X (Root a)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation a
xo
  xa :: X a
xa = XOrtOrientation a -> X a
forall f. XOrtOrientation f -> XFbr f
xoFbr XOrtOrientation a
xo
  xa2 :: X (Adbl2 a)
xa2 = XOrtOrientation a -> X (Adbl2 a)
forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation a
xo
  xa3 :: X (Adbl3 a)
xa3 = XOrtOrientation a -> X (Adbl3 a)
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 = X Z -> X a -> X (Adbl2 a) -> XAbl a
forall a. X Z -> X a -> X (Adbl2 a) -> XAbl a
XAbl X Z
xz X a
xa X (Adbl2 a)
xa2 where
  xa :: X a
xa = XOrtOrientation a -> X a
forall f. XOrtOrientation f -> XFbr f
xoFbr XOrtOrientation a
xo
  xa2 :: X (Adbl2 a)
xa2 = XOrtOrientation a -> X (Adbl2 a)
forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation a
xo