{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |
-- Module      : OAlg.Entity.Sum.Definition
-- Description : definition of free sums over fibred symbols.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- definition of free 'Sum's over 'Fibred' symbols.
module OAlg.Entity.Sum.Definition
  (
    -- * Sum
    Sum(), smlc, smJoin, nSum, zSum, smMap

    -- * Form
  , SumForm(..), smfLength, smflc, lcsmf
  , smfMap, smfJoin, smfReduce

    -- * Linear Combination
  , LinearCombination(..), lcs, lcAggr, lcSort, lcSclFilter

  ) where

import Data.List (map,groupBy,(++),filter)
import Data.Foldable
import Data.Monoid hiding (Sum)

import OAlg.Prelude

import OAlg.Data.Canonical
import OAlg.Data.Reducible
import OAlg.Data.Constructable
import OAlg.Data.Singleton

import OAlg.Structure.Exception
import OAlg.Structure.Fibred.Definition
import OAlg.Structure.Additive.Definition
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Ring.Definition
import OAlg.Structure.Number
import OAlg.Structure.Vectorial

import OAlg.Hom.Definition
import OAlg.Hom.Fibred

--------------------------------------------------------------------------------
-- SumForm -

infixr 6 :+
infixr 9 :!

-- | form for a free sum over 'Fibred' symbols in @__a__@ with scalars in @__r__@.
--
-- __Definition__ Let @__r__@ be a 'Commutative' 'Semiring' and @__a__@ a 'Fibred' structure.
-- A 'SumForm' @a@ is 'valid' if and only if all scalars in @a@ are 'valid' and all symbols in @__a__@
-- are 'valid' and have the same @'root'@.
data SumForm r a
  = Zero (Root a)
  | S a
  | r :! SumForm r a
  | SumForm r a :+ SumForm r a

deriving instance (Fibred a, Entity r) => Show (SumForm r a)
deriving instance (Fibred a, Entity r) => Eq (SumForm r a)
deriving instance ( Fibred a, Entity r
                  , OrdRoot a, Ord r, Ord a
                  ) => Ord (SumForm r a)

--------------------------------------------------------------------------------
-- SumForm - Entity -

instance (Fibred a, Semiring r, Commutative r) => Validable (SumForm r a) where
  valid :: SumForm r a -> Statement
valid SumForm r a
sf = [Statement] -> Statement
And [ String -> Label
Label String
"root" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall f. Fibred f => f -> Root f
root SumForm r a
sf)
                 , String -> Label
Label String
"symbols" Label -> Statement -> Statement
:<=>: forall {a} {a}.
(Validable a, Validable a, Validable (Root a)) =>
SumForm a a -> Statement
vld SumForm r a
sf
                 ] where
    
    vld :: SumForm a a -> Statement
vld SumForm a a
sf = case SumForm a a
sf of
      Zero Root a
e   -> forall a. Validable a => a -> Statement
valid Root a
e
      S a
a      -> forall a. Validable a => a -> Statement
valid a
a
      a
r :! SumForm a a
a   -> forall a. Validable a => a -> Statement
valid a
r forall b. Boolean b => b -> b -> b
&& SumForm a a -> Statement
vld SumForm a a
a
      SumForm a a
a :+ SumForm a a
b   -> SumForm a a -> Statement
vld SumForm a a
a forall b. Boolean b => b -> b -> b
&& SumForm a a -> Statement
vld SumForm a a
b
      
instance (Fibred a, Semiring r, Commutative r) => Entity (SumForm r a)

--------------------------------------------------------------------------------
-- SumForm - Fibred -

instance (Fibred a, Semiring r, Commutative r) => Fibred (SumForm r a) where
  type Root (SumForm r a) = Root a
  root :: SumForm r a -> Root (SumForm r a)
root SumForm r a
sf = case SumForm r a
sf of
    Zero Root a
e -> Root a
e
    S a
a    -> forall f. Fibred f => f -> Root f
root a
a
    r
_ :! SumForm r a
a -> forall f. Fibred f => f -> Root f
root SumForm r a
a
    SumForm r a
a :+ SumForm r a
b -> let r :: Root (SumForm r a)
r = forall f. Fibred f => f -> Root f
root SumForm r a
a in if Root (SumForm r a)
r forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root SumForm r a
b then Root (SumForm r a)
r else forall a e. Exception e => e -> a
throw ArithmeticException
NotAddable
    
--------------------------------------------------------------------------------
-- SumFrom - Foldable -

instance Foldable (SumForm N) where
  foldMap :: forall m a. Monoid m => (a -> m) -> SumForm N a -> m
foldMap a -> m
_ (Zero Root a
_) = forall a. Monoid a => a
mempty
  foldMap a -> m
f (S a
a)    = a -> m
f a
a
  foldMap a -> m
_ (N
0:! SumForm N a
_)  = forall a. Monoid a => a
mempty
  foldMap a -> m
f (N
n:!SumForm N a
a)   = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f SumForm N a
a forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (forall a. Enum a => a -> a
pred N
n forall r a. r -> SumForm r a -> SumForm r a
:! SumForm N a
a)
  foldMap a -> m
f (SumForm N a
a :+ SumForm N a
b) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f SumForm N a
a forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f SumForm N a
b

--------------------------------------------------------------------------------
-- smfSum -

smfSum :: (Root x -> y) -> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum :: forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum Root x -> y
z r -> y -> y
(!) y -> y -> y
(+) x -> y
f SumForm r x
s = SumForm r x -> y
sm SumForm r x
s where
  sm :: SumForm r x -> y
sm (Zero Root x
e) = Root x -> y
z Root x
e
  sm (S x
x)    = x -> y
f x
x
  sm (r
r :! SumForm r x
a) = r
r r -> y -> y
! SumForm r x -> y
sm SumForm r x
a
  sm (SumForm r x
a :+ SumForm r x
b) = SumForm r x -> y
sm SumForm r x
a y -> y -> y
+ SumForm r x -> y
sm SumForm r x
b

--------------------------------------------------------------------------------
-- smfJoin -

-- | joining a sum form of sum forms.
smfJoin :: SumForm r (SumForm r a) -> SumForm r a
smfJoin :: forall r a. SumForm r (SumForm r a) -> SumForm r a
smfJoin = forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum forall r a. Root a -> SumForm r a
Zero forall r a. r -> SumForm r a -> SumForm r a
(:!) forall r a. SumForm r a -> SumForm r a -> SumForm r a
(:+) forall x. x -> x
id

--------------------------------------------------------------------------------
-- smfMap -

-- | mapping of sum forms.
smfMap :: Singleton (Root y) => (x -> y) -> SumForm r x -> SumForm r y
smfMap :: forall y x r.
Singleton (Root y) =>
(x -> y) -> SumForm r x -> SumForm r y
smfMap x -> y
f = forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (forall b a. b -> a -> b
const ( forall r a. Root a -> SumForm r a
Zero forall s. Singleton s => s
unit)) forall r a. r -> SumForm r a -> SumForm r a
(:!) forall r a. SumForm r a -> SumForm r a -> SumForm r a
(:+) (forall r a. a -> SumForm r a
S forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. x -> y
f)

--------------------------------------------------------------------------------
-- smfLength -

-- | the length of a sum form,
smfLength :: Number r => SumForm r a -> N
smfLength :: forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
s = case SumForm r a
s of
  Zero Root a
_  -> N
0
  S a
_     -> N
1
  r
r :! SumForm r a
a  -> forall {b} {r}. (Projectible b Z, Number r) => r -> b
nFloor r
r forall c. Multiplicative c => c -> c -> c
* forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
a
  SumForm r a
a :+ SumForm r a
b  -> forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
a forall a. Additive a => a -> a -> a
+ forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
b
  where nFloor :: r -> b
nFloor r
r = forall a b. Projectible a b => b -> a
prj forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r. Number r => r -> (Z, r)
zFloorFraction r
r

instance LengthN (SumForm N a) where
  lengthN :: SumForm N a -> N
lengthN = forall r a. Number r => SumForm r a -> N
smfLength

--------------------------------------------------------------------------------
-- LinearCombination -

-- | list of symbols in @__a__@ together with a scalar in @__r__@.
--
-- __Note__ 'valid' linear combinations must not be sorted according to the second component!
newtype LinearCombination r a = LinearCombination [(r,a)] deriving (Int -> LinearCombination r a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a.
(Show r, Show a) =>
Int -> LinearCombination r a -> ShowS
forall r a. (Show r, Show a) => [LinearCombination r a] -> ShowS
forall r a. (Show r, Show a) => LinearCombination r a -> String
showList :: [LinearCombination r a] -> ShowS
$cshowList :: forall r a. (Show r, Show a) => [LinearCombination r a] -> ShowS
show :: LinearCombination r a -> String
$cshow :: forall r a. (Show r, Show a) => LinearCombination r a -> String
showsPrec :: Int -> LinearCombination r a -> ShowS
$cshowsPrec :: forall r a.
(Show r, Show a) =>
Int -> LinearCombination r a -> ShowS
Show,LinearCombination r a -> LinearCombination r a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a.
(Eq r, Eq a) =>
LinearCombination r a -> LinearCombination r a -> Bool
/= :: LinearCombination r a -> LinearCombination r a -> Bool
$c/= :: forall r a.
(Eq r, Eq a) =>
LinearCombination r a -> LinearCombination r a -> Bool
== :: LinearCombination r a -> LinearCombination r a -> Bool
$c== :: forall r a.
(Eq r, Eq a) =>
LinearCombination r a -> LinearCombination r a -> Bool
Eq,LinearCombination r a -> Statement
forall a. (a -> Statement) -> Validable a
forall r a.
(Validable r, Validable a) =>
LinearCombination r a -> Statement
valid :: LinearCombination r a -> Statement
$cvalid :: forall r a.
(Validable r, Validable a) =>
LinearCombination r a -> Statement
Validable)

instance (Entity a, Entity r) => Entity (LinearCombination r a)

--------------------------------------------------------------------------------
-- lcs -

-- | the underlying list of symbols with their scalar.
lcs :: LinearCombination r a -> [(r,a)]
lcs :: forall r a. LinearCombination r a -> [(r, a)]
lcs (LinearCombination [(r, a)]
as) = [(r, a)]
as

--------------------------------------------------------------------------------
-- lcAggr -

-- | aggregating linear combinations with same symbols.
lcAggr :: (Eq a, Semiring r) => LinearCombination r a -> LinearCombination r a
lcAggr :: forall a r.
(Eq a, Semiring r) =>
LinearCombination r a -> LinearCombination r a
lcAggr = forall r a. [(r, a)] -> LinearCombination r a
LinearCombination forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b. (a -> b) -> [a] -> [b]
map forall {b} {b}. (Distributive b, Total b) => [(b, b)] -> (b, b)
aggr forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy forall {a} {a} {a}. Eq a => (a, a) -> (a, a) -> Bool
(<=>) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. LinearCombination r a -> [(r, a)]
lcs where
  (a, a)
a <=> :: (a, a) -> (a, a) -> Bool
<=> (a, a)
b = forall a b. (a, b) -> b
snd (a, a)
a forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> b
snd (a, a)
b
  aggr :: [(b, b)] -> (b, b)
aggr as :: [(b, b)]
as@((b
_,b
a):[(b, b)]
_) = (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Additive a => a -> a -> a
(+) forall r. Semiring r => r
rZero forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(b, b)]
as,b
a)

--------------------------------------------------------------------------------
-- lcSort -

-- | sorting a linear combination according to its symbols.
lcSort :: Ord a => LinearCombination r a -> LinearCombination r a
lcSort :: forall a r. Ord a => LinearCombination r a -> LinearCombination r a
lcSort (LinearCombination [(r, a)]
as) = forall r a. [(r, a)] -> LinearCombination r a
LinearCombination (forall b a. Ord b => [(a, b)] -> [(a, b)]
sortSnd [(r, a)]
as)

--------------------------------------------------------------------------------
-- lcSclFilter -

-- | filtering a word according to the scalars.
lcSclFilter :: (r -> Bool) -> LinearCombination r a -> LinearCombination r a
lcSclFilter :: forall r a.
(r -> Bool) -> LinearCombination r a -> LinearCombination r a
lcSclFilter r -> Bool
p (LinearCombination [(r, a)]
ws) = forall r a. [(r, a)] -> LinearCombination r a
LinearCombination forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (r -> Bool
p forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b. (a, b) -> a
fst) [(r, a)]
ws

--------------------------------------------------------------------------------
-- smflc -

-- | transforming a sum form to its corresponding linear combination..
smflc :: Semiring r => SumForm r a -> LinearCombination r a
smflc :: forall r a. Semiring r => SumForm r a -> LinearCombination r a
smflc SumForm r a
sf = forall r a. [(r, a)] -> LinearCombination r a
LinearCombination (forall {a} {b}.
(Distributive a, Total a) =>
SumForm a b -> [(a, b)]
tow SumForm r a
sf) where
  tow :: SumForm a b -> [(a, b)]
tow SumForm a b
sf = case SumForm a b
sf of
    Zero Root b
_        -> []
    S b
a           -> [(forall r. Semiring r => r
rOne,b
a)]
    a
r :! SumForm a b
a        -> forall a b. (a -> b) -> [a] -> [b]
map (\(a
s,b
a) -> (a
rforall c. Multiplicative c => c -> c -> c
*a
s,b
a)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ SumForm a b -> [(a, b)]
tow SumForm a b
a
    S b
a :+ SumForm a b
b      -> (forall r. Semiring r => r
rOne,b
a)forall a. a -> [a] -> [a]
:SumForm a b -> [(a, b)]
tow SumForm a b
b
    a
r :! S b
a :+ SumForm a b
b -> (a
r,b
a)forall a. a -> [a] -> [a]
:SumForm a b -> [(a, b)]
tow SumForm a b
b
    SumForm a b
a :+ SumForm a b
b        -> SumForm a b -> [(a, b)]
tow SumForm a b
a forall a. [a] -> [a] -> [a]
++ SumForm a b -> [(a, b)]
tow SumForm a b
b
                   
--------------------------------------------------------------------------------
-- lcsmf -

-- | transforming a word to its corresponding sum form.
lcsmf :: Semiring r => Root a -> LinearCombination r a -> SumForm r a
lcsmf :: forall r a.
Semiring r =>
Root a -> LinearCombination r a -> SumForm r a
lcsmf Root a
e (LinearCombination [(r, a)]
ws) = forall {r} {a}.
(Distributive r, Total r) =>
Root a -> [(r, a)] -> SumForm r a
smf Root a
e [(r, a)]
ws where
  smf :: Root a -> [(r, a)] -> SumForm r a
smf Root a
e [(r, a)]
ws = case [(r, a)]
ws of
    []      -> forall r a. Root a -> SumForm r a
Zero Root a
e
    [(r
r,a
a)] -> if r
r forall a. Eq a => a -> a -> Bool
== forall r. Semiring r => r
rOne then forall r a. a -> SumForm r a
S a
a else (r
r forall r a. r -> SumForm r a -> SumForm r a
:! forall r a. a -> SumForm r a
S a
a)
    (r, a)
w:[(r, a)]
ws    -> Root a -> [(r, a)] -> SumForm r a
smf Root a
e [(r, a)
w] forall r a. SumForm r a -> SumForm r a -> SumForm r a
:+ Root a -> [(r, a)] -> SumForm r a
smf Root a
e [(r, a)]
ws

--------------------------------------------------------------------------------
-- smfReduce -

-- | reducing a sum form to its canonical form,
smfReduce :: (Fibred a, Ord a, Semiring r, Commutative r) => SumForm r a -> SumForm r a
smfReduce :: forall a r.
(Fibred a, Ord a, Semiring r, Commutative r) =>
SumForm r a -> SumForm r a
smfReduce SumForm r a
sf = forall r a.
Semiring r =>
Root a -> LinearCombination r a -> SumForm r a
lcsmf (forall f. Fibred f => f -> Root f
root SumForm r a
sf) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a.
(r -> Bool) -> LinearCombination r a -> LinearCombination r a
lcSclFilter (forall b. Boolean b => b -> b
not forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. Additive a => a -> Bool
isZero) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a r.
(Eq a, Semiring r) =>
LinearCombination r a -> LinearCombination r a
lcAggr forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a r. Ord a => LinearCombination r a -> LinearCombination r a
lcSort forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Semiring r => SumForm r a -> LinearCombination r a
smflc SumForm r a
sf

instance (Fibred a, Ord a, Semiring r, Commutative r) => Reducible (SumForm r a) where
  reduce :: SumForm r a -> SumForm r a
reduce = forall a r.
(Fibred a, Ord a, Semiring r, Commutative r) =>
SumForm r a -> SumForm r a
smfReduce

--------------------------------------------------------------------------------
-- Sum -

-- | free sum over 'Fibred' symbols in @__a__@ with scalars in @__r__@.
--
-- __Definition__ A 'Sum' @s@ is 'valid' if and only if its underlying 'SumForm' @s'@ is 'valid' and
-- @s'@ is reduced, i.e. @s' '==' 'reduce' s'@.
newtype Sum r a = Sum (SumForm r a) deriving (Int -> Sum r a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a. (Fibred a, Entity r) => Int -> Sum r a -> ShowS
forall r a. (Fibred a, Entity r) => [Sum r a] -> ShowS
forall r a. (Fibred a, Entity r) => Sum r a -> String
showList :: [Sum r a] -> ShowS
$cshowList :: forall r a. (Fibred a, Entity r) => [Sum r a] -> ShowS
show :: Sum r a -> String
$cshow :: forall r a. (Fibred a, Entity r) => Sum r a -> String
showsPrec :: Int -> Sum r a -> ShowS
$cshowsPrec :: forall r a. (Fibred a, Entity r) => Int -> Sum r a -> ShowS
Show,Sum r a -> Sum r a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a. (Fibred a, Entity r) => Sum r a -> Sum r a -> Bool
/= :: Sum r a -> Sum r a -> Bool
$c/= :: forall r a. (Fibred a, Entity r) => Sum r a -> Sum r a -> Bool
== :: Sum r a -> Sum r a -> Bool
$c== :: forall r a. (Fibred a, Entity r) => Sum r a -> Sum r a -> Bool
Eq,Sum r a -> Sum r a -> Bool
Sum r a -> Sum r a -> Ordering
Sum r a -> Sum r a -> Sum r 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 {r} {a}.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Eq (Sum r a)
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Bool
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Ordering
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Sum r a
min :: Sum r a -> Sum r a -> Sum r a
$cmin :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Sum r a
max :: Sum r a -> Sum r a -> Sum r a
$cmax :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Sum r a
>= :: Sum r a -> Sum r a -> Bool
$c>= :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Bool
> :: Sum r a -> Sum r a -> Bool
$c> :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Bool
<= :: Sum r a -> Sum r a -> Bool
$c<= :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Bool
< :: Sum r a -> Sum r a -> Bool
$c< :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Bool
compare :: Sum r a -> Sum r a -> Ordering
$ccompare :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Entity r) =>
Sum r a -> Sum r a -> Ordering
Ord,Sum r a -> Statement
forall a. (a -> Statement) -> Validable a
forall r a.
(Distributive r, Total r, Commutative r, Fibred a) =>
Sum r a -> Statement
valid :: Sum r a -> Statement
$cvalid :: forall r a.
(Distributive r, Total r, Commutative r, Fibred a) =>
Sum r a -> Statement
Validable)

instance (Fibred a, Semiring r, Commutative r) => Entity (Sum r a)

--------------------------------------------------------------------------------
-- Sum - Constructable -

instance Exposable (Sum r a) where
  type Form (Sum r a) = SumForm r a
  form :: Sum r a -> Form (Sum r a)
form (Sum SumForm r a
a) = SumForm r a
a

instance (Fibred a, Ord a, Semiring r, Commutative r) => Constructable (Sum r a) where
  make :: Form (Sum r a) -> Sum r a
make = forall r a. SumForm r a -> Sum r a
Sum forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall e. Reducible e => e -> e
reduce
  
--------------------------------------------------------------------------------
-- Sum - Abelian -

instance (Fibred a, Semiring r, Commutative r) => Fibred (Sum r a) where
  type Root (Sum r a) = Root a
  root :: Sum r a -> Root (Sum r a)
root (Sum SumForm r a
sf) = forall f. Fibred f => f -> Root f
root SumForm r a
sf
  
instance (Fibred a, Ord a, Semiring r, Commutative r) => Additive (Sum r a) where
  zero :: Root (Sum r a) -> Sum r a
zero Root (Sum r a)
e = forall r a. SumForm r a -> Sum r a
Sum (forall r a. Root a -> SumForm r a
Zero Root (Sum r a)
e)
  Sum SumForm r a
a + :: Sum r a -> Sum r a -> Sum r a
+ Sum SumForm r a
b | forall f. Fibred f => f -> Root f
root SumForm r a
a forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root SumForm r a
b = forall x. Constructable x => Form x -> x
make (SumForm r a
a forall r a. SumForm r a -> SumForm r a -> SumForm r a
:+ SumForm r a
b)
                | Bool
otherwise        = forall a e. Exception e => e -> a
throw ArithmeticException
NotAddable

  ntimes :: N -> Sum r a -> Sum r a
ntimes N
n (Sum SumForm r a
a) = forall x. Constructable x => Form x -> x
make (forall a. Additive a => N -> a -> a
ntimes N
n forall r. Semiring r => r
rOne forall r a. r -> SumForm r a -> SumForm r a
:! SumForm r a
a) 

instance (Fibred a, Ord a, Ring r, Commutative r) => Abelian (Sum r a) where
  negate :: Sum r a -> Sum r a
negate (Sum SumForm r a
a)   = forall x. Constructable x => Form x -> x
make (forall a. Abelian a => a -> a
negate forall r. Semiring r => r
rOne forall r a. r -> SumForm r a -> SumForm r a
:! SumForm r a
a) 
  ztimes :: Z -> Sum r a -> Sum r a
ztimes Z
z (Sum SumForm r a
a) = forall x. Constructable x => Form x -> x
make (forall a. Abelian a => Z -> a -> a
ztimes Z
z forall r. Semiring r => r
rOne forall r a. r -> SumForm r a -> SumForm r a
:! SumForm r a
a)

instance (Fibred a, Ord a, Semiring r, Commutative r) => Vectorial (Sum r a) where
  type Scalar (Sum r a) = r
  Scalar (Sum r a)
r ! :: Scalar (Sum r a) -> Sum r a -> Sum r a
! (Sum SumForm r a
a) = forall x. Constructable x => Form x -> x
make (Scalar (Sum r a)
r forall r a. r -> SumForm r a -> SumForm r a
:! SumForm r a
a)
  
--------------------------------------------------------------------------------
-- smlc -

-- | the associated linear combination.
--
-- __Note__ The associated linear combination of a sum is sorted according to the second component!
smlc :: Semiring r => Sum r a -> LinearCombination r a
smlc :: forall r a. Semiring r => Sum r a -> LinearCombination r a
smlc = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. Semiring r => SumForm r a -> LinearCombination r a
smflc

--------------------------------------------------------------------------------
-- smJoin -

-- | joining a sum of sums.
smJoin :: (Semiring r, Commutative r, Fibred a, Ord a) => Sum r (Sum r a) -> Sum r a
smJoin :: forall r a.
(Semiring r, Commutative r, Fibred a, Ord a) =>
Sum r (Sum r a) -> Sum r a
smJoin = forall x. Constructable x => Form x -> x
make forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. SumForm r (SumForm r a) -> SumForm r a
smfJoin forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x y. Exposable x => (Form x -> y) -> x -> y
restrict (forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum forall r a. Root a -> SumForm r a
Zero forall r a. r -> SumForm r a -> SumForm r a
(:!) forall r a. SumForm r a -> SumForm r a -> SumForm r a
(:+) (forall r a. a -> SumForm r a
S forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Exposable x => x -> Form x
form))

--------------------------------------------------------------------------------
-- smMap -

-- | additive homomorphism to a totally defined sum.
smMap :: (Singleton (Root y), Fibred y, Ord y, Semiring r, Commutative r)
  => (x -> y) -> Sum r x -> Sum r y
smMap :: forall y r x.
(Singleton (Root y), Fibred y, Ord y, Semiring r, Commutative r) =>
(x -> y) -> Sum r x -> Sum r y
smMap x -> y
f (Sum SumForm r x
s) = forall x. Constructable x => Form x -> x
make (forall y x r.
Singleton (Root y) =>
(x -> y) -> SumForm r x -> SumForm r y
smfMap x -> y
f SumForm r x
s)

--------------------------------------------------------------------------------
-- nSum -

-- | additive homomorphism for sums over 'N'.
nSum :: (Hom Fbr h,Additive x) => h a x -> Sum N a -> x
nSum :: forall (h :: * -> * -> *) x a.
(Hom Fbr h, Additive x) =>
h a x -> Sum N a -> x
nSum h a x
h = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict (forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (forall a. Additive a => Root a -> a
zero forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap h a x
h) forall a. Additive a => N -> a -> a
ntimes forall a. Additive a => a -> a -> a
(+) (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a x
h))

--------------------------------------------------------------------------------
-- zSum -

-- | additive homomorphism for sums over 'Z'.
zSum :: (Hom Fbr h,Abelian x) => h a x -> Sum Z a -> x
zSum :: forall (h :: * -> * -> *) x a.
(Hom Fbr h, Abelian x) =>
h a x -> Sum Z a -> x
zSum h a x
h = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict (forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (forall a. Additive a => Root a -> a
zero forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap h a x
h) forall a. Abelian a => Z -> a -> a
ztimes forall a. Additive a => a -> a -> a
(+) (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a x
h))