{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving, DeriveFunctor #-}
{-# 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 Control.Monad as M (Functor(..))

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.Oriented.Definition
import OAlg.Structure.Fibred.Definition
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive.Definition
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Ring.Definition
import OAlg.Structure.Distributive.Definition
import OAlg.Structure.Vectorial.Definition
import OAlg.Structure.Algebraic.Definition
import OAlg.Structure.Number.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
:<=>: Root a -> Statement
forall a. Validable a => a -> Statement
valid (SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
sf)
                 , String -> Label
Label String
"symbols" Label -> Statement -> Statement
:<=>: SumForm r a -> 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   -> Root a -> Statement
forall a. Validable a => a -> Statement
valid Root a
e
      S a
a      -> a -> Statement
forall a. Validable a => a -> Statement
valid a
a
      a
r :! SumForm a a
a   -> a -> Statement
forall a. Validable a => a -> Statement
valid a
r Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& 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 Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& SumForm a a -> Statement
vld SumForm a a
b
      
-- instance (Fibred a, Semiring r, Commutative r) => Entity (SumForm r a)

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

type instance Root (SumForm r a) = Root a

instance ShowRoot a => ShowRoot (SumForm r a)
instance EqRoot a => EqRoot (SumForm r a)
instance ValidableRoot a => ValidableRoot (SumForm r a)
instance TypeableRoot a => TypeableRoot (SumForm r a)

instance (Fibred a, Semiring r, Commutative r) => Fibred (SumForm r a) where

  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
Root (SumForm r a)
e
    S a
a    -> a -> Root a
forall f. Fibred f => f -> Root f
root a
a
    r
_ :! SumForm r a
a -> SumForm r a -> Root (SumForm r 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 = SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
a in if Root a
Root (SumForm r a)
r Root a -> Root a -> Bool
forall a. Eq a => a -> a -> Bool
== SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
b then Root (SumForm r a)
r else ArithmeticException -> Root a
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
_) = m
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
_)  = m
forall a. Monoid a => a
mempty
  foldMap a -> m
f (N
n:!SumForm N a
a)   = (a -> m) -> SumForm N a -> m
forall m a. Monoid m => (a -> m) -> SumForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f SumForm N a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> SumForm N a -> m
forall m a. Monoid m => (a -> m) -> SumForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (N -> N
forall a. Enum a => a -> a
pred N
n N -> SumForm N a -> SumForm N a
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) = (a -> m) -> SumForm N a -> m
forall m a. Monoid m => (a -> m) -> SumForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f SumForm N a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> SumForm N a -> m
forall m a. Monoid m => (a -> m) -> SumForm N a -> m
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 = (Root (SumForm r a) -> SumForm r a)
-> (r -> SumForm r a -> SumForm r a)
-> (SumForm r a -> SumForm r a -> SumForm r a)
-> (SumForm r a -> SumForm r a)
-> SumForm r (SumForm r a)
-> SumForm r a
forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum Root a -> SumForm r a
Root (SumForm r a) -> SumForm r a
forall r a. Root a -> SumForm r a
Zero r -> SumForm r a -> SumForm r a
forall r a. r -> SumForm r a -> SumForm r a
(:!) SumForm r a -> SumForm r a -> SumForm r a
forall r a. SumForm r a -> SumForm 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 = (Root x -> SumForm r y)
-> (r -> SumForm r y -> SumForm r y)
-> (SumForm r y -> SumForm r y -> SumForm r y)
-> (x -> SumForm r y)
-> SumForm r x
-> SumForm r y
forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (SumForm r y -> Root x -> SumForm r y
forall b a. b -> a -> b
const ( Root y -> SumForm r y
forall r a. Root a -> SumForm r a
Zero Root y
forall s. Singleton s => s
unit)) r -> SumForm r y -> SumForm r y
forall r a. r -> SumForm r a -> SumForm r a
(:!) SumForm r y -> SumForm r y -> SumForm r y
forall r a. SumForm r a -> SumForm r a -> SumForm r a
(:+) (y -> SumForm r y
forall r a. a -> SumForm r a
S (y -> SumForm r y) -> (x -> y) -> x -> SumForm r y
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. x -> y
f)

--------------------------------------------------------------------------------
-- 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  -> r -> N
forall {r} {y}. (Projectible y Z, Number r) => r -> y
nFloor r
r N -> N -> N
forall c. Multiplicative c => c -> c -> c
* SumForm r a -> N
forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
a
  SumForm r a
a :+ SumForm r a
b  -> SumForm r a -> N
forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
a N -> N -> N
forall a. Additive a => a -> a -> a
+ SumForm r a -> N
forall r a. Number r => SumForm r a -> N
smfLength SumForm r a
b
  where nFloor :: r -> y
nFloor r
r = Z -> y
forall a b. Projectible a b => b -> a
prj (Z -> y) -> Z -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Z, r) -> Z
forall a b. (a, b) -> a
fst ((Z, r) -> Z) -> (Z, r) -> Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction r
r

instance LengthN (SumForm N a) where
  lengthN :: SumForm N a -> N
lengthN = SumForm N a -> N
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
[LinearCombination r a] -> ShowS
LinearCombination r a -> String
(Int -> LinearCombination r a -> ShowS)
-> (LinearCombination r a -> String)
-> ([LinearCombination r a] -> ShowS)
-> Show (LinearCombination r a)
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
$cshowsPrec :: forall r a.
(Show r, Show a) =>
Int -> LinearCombination r a -> ShowS
showsPrec :: Int -> LinearCombination r a -> ShowS
$cshow :: forall r a. (Show r, Show a) => LinearCombination r a -> String
show :: LinearCombination r a -> String
$cshowList :: forall r a. (Show r, Show a) => [LinearCombination r a] -> ShowS
showList :: [LinearCombination r a] -> ShowS
Show,LinearCombination r a -> LinearCombination r a -> Bool
(LinearCombination r a -> LinearCombination r a -> Bool)
-> (LinearCombination r a -> LinearCombination r a -> Bool)
-> Eq (LinearCombination r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a.
(Eq r, Eq a) =>
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
/= :: LinearCombination r a -> LinearCombination r a -> Bool
Eq,LinearCombination r a -> Statement
(LinearCombination r a -> Statement)
-> Validable (LinearCombination r a)
forall a. (a -> Statement) -> Validable a
forall r a.
(Validable r, Validable a) =>
LinearCombination r a -> Statement
$cvalid :: forall r a.
(Validable r, Validable a) =>
LinearCombination r a -> Statement
valid :: LinearCombination r a -> Statement
Validable,(forall a b.
 (a -> b) -> LinearCombination r a -> LinearCombination r b)
-> (forall a b.
    a -> LinearCombination r b -> LinearCombination r a)
-> Functor (LinearCombination r)
forall a b. a -> LinearCombination r b -> LinearCombination r a
forall a b.
(a -> b) -> LinearCombination r a -> LinearCombination r b
forall r a b. a -> LinearCombination r b -> LinearCombination r a
forall r a b.
(a -> b) -> LinearCombination r a -> LinearCombination r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall r a b.
(a -> b) -> LinearCombination r a -> LinearCombination r b
fmap :: forall a b.
(a -> b) -> LinearCombination r a -> LinearCombination r b
$c<$ :: forall r a b. a -> LinearCombination r b -> LinearCombination r a
<$ :: forall a b. a -> LinearCombination r b -> LinearCombination r a
M.Functor)

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

instance ApplicativeG (LinearCombination r) (->) (->) where
  amapG :: forall x y.
(x -> y) -> LinearCombination r x -> LinearCombination r y
amapG = (x -> y) -> LinearCombination r x -> LinearCombination r y
forall x y.
(x -> y) -> LinearCombination r x -> LinearCombination r y
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
M.fmap
  
--------------------------------------------------------------------------------
-- 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 = [(r, a)] -> LinearCombination r a
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination ([(r, a)] -> LinearCombination r a)
-> (LinearCombination r a -> [(r, a)])
-> LinearCombination r a
-> LinearCombination r a
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
. ([(r, a)] -> (r, a)) -> [[(r, a)]] -> [(r, a)]
forall a b. (a -> b) -> [a] -> [b]
map [(r, a)] -> (r, a)
forall {b} {b}. (Distributive b, Total b) => [(b, b)] -> (b, b)
aggr ([[(r, a)]] -> [(r, a)])
-> (LinearCombination r a -> [[(r, a)]])
-> LinearCombination r a
-> [(r, a)]
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
. ((r, a) -> (r, a) -> Bool) -> [(r, a)] -> [[(r, a)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (r, a) -> (r, a) -> Bool
forall {a} {a} {a}. Eq a => (a, a) -> (a, a) -> Bool
(<=>) ([(r, a)] -> [[(r, a)]])
-> (LinearCombination r a -> [(r, a)])
-> LinearCombination r a
-> [[(r, a)]]
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
. LinearCombination r a -> [(r, a)]
forall r a. LinearCombination r a -> [(r, a)]
lcs where
  (a, a)
a <=> :: (a, a) -> (a, a) -> Bool
<=> (a, a)
b = (a, a) -> a
forall a b. (a, b) -> b
snd (a, a)
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, a) -> a
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)]
_) = ((b -> b -> b) -> b -> [b] -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr b -> b -> b
forall a. Additive a => a -> a -> a
(+) b
forall r. Semiring r => r
rZero ([b] -> b) -> [b] -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, b) -> b
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) = [(r, a)] -> LinearCombination r a
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination ([(r, a)] -> [(r, a)]
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) = [(r, a)] -> LinearCombination r a
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination ([(r, a)] -> LinearCombination r a)
-> [(r, a)] -> LinearCombination r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, a) -> Bool) -> [(r, a)] -> [(r, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (r -> Bool
p (r -> Bool) -> ((r, a) -> r) -> (r, a) -> Bool
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
. (r, a) -> r
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 = [(r, a)] -> LinearCombination r a
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination (SumForm r a -> [(r, a)]
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           -> [(a
forall r. Semiring r => r
rOne,b
a)]
    a
r :! SumForm a b
a        -> ((a, b) -> (a, b)) -> [(a, b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
s,b
a) -> (a
ra -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
s,b
a)) ([(a, b)] -> [(a, b)]) -> [(a, b)] -> [(a, b)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SumForm a b -> [(a, b)]
tow SumForm a b
a
    S b
a :+ SumForm a b
b      -> (a
forall r. Semiring r => r
rOne,b
a)(a, b) -> [(a, b)] -> [(a, b)]
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)(a, b) -> [(a, b)] -> [(a, b)]
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 [(a, b)] -> [(a, b)] -> [(a, b)]
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) = Root a -> [(r, a)] -> SumForm r a
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
    []      -> Root a -> SumForm r a
forall r a. Root a -> SumForm r a
Zero Root a
e
    [(r
r,a
a)] -> if r
r r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
forall r. Semiring r => r
rOne then a -> SumForm r a
forall r a. a -> SumForm r a
S a
a else (r
r r -> SumForm r a -> SumForm r a
forall r a. r -> SumForm r a -> SumForm r a
:! 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] SumForm r a -> SumForm r a -> SumForm r a
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 = Root a -> LinearCombination r a -> SumForm r a
forall r a.
Semiring r =>
Root a -> LinearCombination r a -> SumForm r a
lcsmf (SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
sf) (LinearCombination r a -> SumForm r a)
-> LinearCombination r a -> SumForm r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (r -> Bool) -> LinearCombination r a -> LinearCombination r a
forall r a.
(r -> Bool) -> LinearCombination r a -> LinearCombination r a
lcSclFilter (Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> (r -> Bool) -> r -> Bool
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
. r -> Bool
forall a. Additive a => a -> Bool
isZero) (LinearCombination r a -> LinearCombination r a)
-> LinearCombination r a -> LinearCombination r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination r a -> LinearCombination r a
forall a r.
(Eq a, Semiring r) =>
LinearCombination r a -> LinearCombination r a
lcAggr (LinearCombination r a -> LinearCombination r a)
-> LinearCombination r a -> LinearCombination r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination r a -> LinearCombination r a
forall a r. Ord a => LinearCombination r a -> LinearCombination r a
lcSort (LinearCombination r a -> LinearCombination r a)
-> LinearCombination r a -> LinearCombination r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SumForm r a -> LinearCombination r a
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 = SumForm r a -> SumForm r a
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
[Sum r a] -> ShowS
Sum r a -> String
(Int -> Sum r a -> ShowS)
-> (Sum r a -> String) -> ([Sum r a] -> ShowS) -> Show (Sum r a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Int -> Sum r a -> ShowS
forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
[Sum r a] -> ShowS
forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Sum r a -> String
$cshowsPrec :: forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Int -> Sum r a -> ShowS
showsPrec :: Int -> Sum r a -> ShowS
$cshow :: forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Sum r a -> String
show :: Sum r a -> String
$cshowList :: forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
[Sum r a] -> ShowS
showList :: [Sum r a] -> ShowS
Show,Sum r a -> Sum r a -> Bool
(Sum r a -> Sum r a -> Bool)
-> (Sum r a -> Sum r a -> Bool) -> Eq (Sum r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Sum r a -> Sum r a -> Bool
$c== :: forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Sum r a -> Sum r a -> Bool
== :: Sum r a -> Sum r a -> Bool
$c/= :: forall r a.
(Fibred a, Show r, Eq r, Validable r, Typeable r) =>
Sum r a -> Sum r a -> Bool
/= :: Sum r a -> Sum r a -> Bool
Eq,Eq (Sum r a)
Eq (Sum r a) =>
(Sum r a -> Sum r a -> Ordering)
-> (Sum r a -> Sum r a -> Bool)
-> (Sum r a -> Sum r a -> Bool)
-> (Sum r a -> Sum r a -> Bool)
-> (Sum r a -> Sum r a -> Bool)
-> (Sum r a -> Sum r a -> Sum r a)
-> (Sum r a -> Sum r a -> Sum r a)
-> Ord (Sum r a)
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, Show r, Validable r,
 Typeable r) =>
Eq (Sum r a)
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Bool
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Ordering
forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Sum r a
$ccompare :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Ordering
compare :: Sum r a -> Sum r a -> Ordering
$c< :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Bool
>= :: Sum r a -> Sum r a -> Bool
$cmax :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Sum r a
max :: Sum r a -> Sum r a -> Sum r a
$cmin :: forall r a.
(Fibred a, OrdRoot a, Ord r, Ord a, Show r, Validable r,
 Typeable r) =>
Sum r a -> Sum r a -> Sum r a
min :: Sum r a -> Sum r a -> Sum r a
Ord,Sum r a -> Statement
(Sum r a -> Statement) -> Validable (Sum r a)
forall a. (a -> Statement) -> Validable a
forall r a.
(Distributive r, Total r, Commutative r, Fibred a) =>
Sum r a -> Statement
$cvalid :: forall r a.
(Distributive r, Total r, Commutative r, Fibred a) =>
Sum r a -> Statement
valid :: 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) = Form (Sum r 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 = SumForm r a -> Sum r a
forall r a. SumForm r a -> Sum r a
Sum (SumForm r a -> Sum r a)
-> (SumForm r a -> SumForm r a) -> SumForm r a -> Sum r a
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
. SumForm r a -> SumForm r a
forall e. Reducible e => e -> e
reduce
  
--------------------------------------------------------------------------------
-- Sum - Abelian -

type instance Root (Sum r a) = Root a

instance ShowRoot a => ShowRoot (Sum r a)
instance EqRoot a => EqRoot (Sum r a)
instance ValidableRoot a => ValidableRoot (Sum r a)
instance TypeableRoot a => TypeableRoot (Sum r a)

instance (Fibred a, Semiring r, Commutative r) => Fibred (Sum r a) where
  root :: Sum r a -> Root (Sum r a)
root (Sum SumForm r a
sf) = SumForm r a -> Root (SumForm r a)
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 = SumForm r a -> Sum r a
forall r a. SumForm r a -> Sum r a
Sum (Root a -> SumForm r a
forall r a. Root a -> SumForm r a
Zero Root a
Root (Sum r a)
e)
  Sum SumForm r a
a + :: Sum r a -> Sum r a -> Sum r a
+ Sum SumForm r a
b | SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
a Root a -> Root a -> Bool
forall a. Eq a => a -> a -> Bool
== SumForm r a -> Root (SumForm r a)
forall f. Fibred f => f -> Root f
root SumForm r a
b = Form (Sum r a) -> Sum r a
forall x. Constructable x => Form x -> x
make (SumForm r a
a SumForm r a -> SumForm r a -> SumForm r a
forall r a. SumForm r a -> SumForm r a -> SumForm r a
:+ SumForm r a
b)
                | Bool
otherwise        = ArithmeticException -> Sum r a
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) = Form (Sum r a) -> Sum r a
forall x. Constructable x => Form x -> x
make (N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
n r
forall r. Semiring r => r
rOne r -> SumForm r a -> SumForm r a
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)   = Form (Sum r a) -> Sum r a
forall x. Constructable x => Form x -> x
make (r -> r
forall a. Abelian a => a -> a
negate r
forall r. Semiring r => r
rOne r -> SumForm r a -> SumForm r a
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) = Form (Sum r a) -> Sum r a
forall x. Constructable x => Form x -> x
make (Z -> r -> r
forall a. Abelian a => Z -> a -> a
ztimes Z
z r
forall r. Semiring r => r
rOne r -> SumForm r a -> SumForm r a
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) = Form (Sum r a) -> Sum r a
forall x. Constructable x => Form x -> x
make (r
Scalar (Sum r a)
r r -> SumForm r a -> SumForm r a
forall r a. r -> SumForm r a -> SumForm r a
:! SumForm r a
a)

--------------------------------------------------------------------------------
-- Canonical -

instance (Fibred a, Ord a, Semiring r, Commutative r) => Projectible (Sum r a) (Sheaf a) where
  prj :: Sheaf a -> Sum r a
prj (Sheaf Root a
r [a]
as) = Form (Sum r a) -> Sum r a
SumForm r a -> Sum r a
forall x. Constructable x => Form x -> x
make (SumForm r a -> Sum r a) -> SumForm r a -> Sum r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (a -> SumForm r a -> SumForm r a)
-> SumForm r a -> [a] -> SumForm r a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> SumForm r a -> SumForm r a
forall {a} {r}. a -> SumForm r a -> SumForm r a
(+) (Root a -> SumForm r a
forall r a. Root a -> SumForm r a
Zero Root a
r) [a]
as where a
a + :: a -> SumForm r a -> SumForm r a
+ SumForm r a
s = a -> SumForm r a
forall r a. a -> SumForm r a
S a
a SumForm r a -> SumForm r a -> SumForm r a
forall r a. SumForm r a -> SumForm r a -> SumForm r a
:+ SumForm r a
s

instance ( Fibred a, Ord a, Scalar a ~ r
         , Semiring r, Commutative r
         ) => Projectible (Sum r a) (VectorSheaf a) where
  prj :: VectorSheaf a -> Sum r a
prj (VectorSheaf Root a
r [(Scalar a, a)]
as) = Form (Sum r a) -> Sum r a
SumForm r a -> Sum r a
forall x. Constructable x => Form x -> x
make (SumForm r a -> Sum r a) -> SumForm r a -> Sum r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((r, a) -> SumForm r a -> SumForm r a)
-> SumForm r a -> [(r, a)] -> SumForm r a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (r, a) -> SumForm r a -> SumForm r a
forall {r} {a}. (r, a) -> SumForm r a -> SumForm r a
(+!) (Root a -> SumForm r a
forall r a. Root a -> SumForm r a
Zero Root a
r) [(r, a)]
[(Scalar a, a)]
as where (r
x,a
a) +! :: (r, a) -> SumForm r a -> SumForm r a
+! SumForm r a
v = r
x r -> SumForm r a -> SumForm r a
forall r a. r -> SumForm r a -> SumForm r a
:! a -> SumForm r a
forall r a. a -> SumForm r a
S a
a SumForm r a -> SumForm r a -> SumForm r a
forall r a. SumForm r a -> SumForm r a -> SumForm r a
:+ SumForm r a
v
  
--------------------------------------------------------------------------------
-- 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 = (Form (Sum r a) -> LinearCombination r a)
-> Sum r a -> LinearCombination r a
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Sum r a) -> LinearCombination r a
SumForm r a -> LinearCombination r a
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 = Form (Sum r a) -> Sum r a
SumForm r a -> Sum r a
forall x. Constructable x => Form x -> x
make (SumForm r a -> Sum r a)
-> (Sum r (Sum r a) -> SumForm r a) -> Sum r (Sum r a) -> Sum r a
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
. SumForm r (SumForm r a) -> SumForm r a
forall r a. SumForm r (SumForm r a) -> SumForm r a
smfJoin (SumForm r (SumForm r a) -> SumForm r a)
-> (Sum r (Sum r a) -> SumForm r (SumForm r a))
-> Sum r (Sum r a)
-> SumForm r a
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
. (Form (Sum r (Sum r a)) -> SumForm r (SumForm r a))
-> Sum r (Sum r a) -> SumForm r (SumForm r a)
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict ((Root (Sum r a) -> SumForm r (SumForm r a))
-> (r -> SumForm r (SumForm r a) -> SumForm r (SumForm r a))
-> (SumForm r (SumForm r a)
    -> SumForm r (SumForm r a) -> SumForm r (SumForm r a))
-> (Sum r a -> SumForm r (SumForm r a))
-> SumForm r (Sum r a)
-> SumForm r (SumForm r a)
forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum Root (Sum r a) -> SumForm r (SumForm r a)
Root (SumForm r a) -> SumForm r (SumForm r a)
forall r a. Root a -> SumForm r a
Zero r -> SumForm r (SumForm r a) -> SumForm r (SumForm r a)
forall r a. r -> SumForm r a -> SumForm r a
(:!) SumForm r (SumForm r a)
-> SumForm r (SumForm r a) -> SumForm r (SumForm r a)
forall r a. SumForm r a -> SumForm r a -> SumForm r a
(:+) (SumForm r a -> SumForm r (SumForm r a)
forall r a. a -> SumForm r a
S (SumForm r a -> SumForm r (SumForm r a))
-> (Sum r a -> SumForm r a) -> Sum r a -> SumForm r (SumForm r a)
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
. Sum r a -> Form (Sum r a)
Sum r a -> SumForm r a
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) = Form (Sum r y) -> Sum r y
forall x. Constructable x => Form x -> x
make ((x -> y) -> SumForm r x -> SumForm r y
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 :: (HomFibred h,Additive x) => h a x -> Sum N a -> x
nSum :: forall (h :: * -> * -> *) x a.
(HomFibred h, Additive x) =>
h a x -> Sum N a -> x
nSum h a x
h = (Form (Sum N a) -> x) -> Sum N a -> x
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict ((Root a -> x)
-> (N -> x -> x) -> (x -> x -> x) -> (a -> x) -> SumForm N a -> x
forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (Root x -> x
forall a. Additive a => Root a -> a
zero (Root x -> x) -> (Root a -> Root x) -> Root a -> x
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
. h a x -> Root a -> Root x
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h a x
h) N -> x -> x
forall a. Additive a => N -> a -> a
ntimes x -> x -> x
forall a. Additive a => a -> a -> a
(+) (h a x -> a -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a x
h))

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

-- | additive homomorphism for sums over 'Z'.
zSum :: (HomFibred h,Abelian x) => h a x -> Sum Z a -> x
zSum :: forall (h :: * -> * -> *) x a.
(HomFibred h, Abelian x) =>
h a x -> Sum Z a -> x
zSum h a x
h = (Form (Sum Z a) -> x) -> Sum Z a -> x
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict ((Root a -> x)
-> (Z -> x -> x) -> (x -> x -> x) -> (a -> x) -> SumForm Z a -> x
forall x y r.
(Root x -> y)
-> (r -> y -> y) -> (y -> y -> y) -> (x -> y) -> SumForm r x -> y
smfSum (Root x -> x
forall a. Additive a => Root a -> a
zero (Root x -> x) -> (Root a -> Root x) -> Root a -> x
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
. h a x -> Root a -> Root x
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h a x
h) Z -> x -> x
forall a. Abelian a => Z -> a -> a
ztimes x -> x -> x
forall a. Additive a => a -> a -> a
(+) (h a x -> a -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a x
h))

--------------------------------------------------------------------------------
-- Sum - Algebra -

type instance Point (SumForm r a) = Point a

instance ShowPoint a => ShowPoint (SumForm r a)
instance EqPoint a => EqPoint (SumForm r a)
instance ValidablePoint a => ValidablePoint (SumForm r a)
instance TypeablePoint a => TypeablePoint (SumForm r a)

instance (Semiring r, Commutative r, FibredOriented m) => Oriented (SumForm r m) where
  orientation :: SumForm r m -> Orientation (Point (SumForm r m))
orientation = SumForm r m -> Orientation (Point (SumForm r m))
SumForm r m -> Root (SumForm r m)
forall f. Fibred f => f -> Root f
root

type instance Point (Sum r a) = Point a

instance ShowPoint a => ShowPoint (Sum r a)
instance EqPoint a => EqPoint (Sum r a)
instance ValidablePoint a => ValidablePoint (Sum r a)
instance TypeablePoint a => TypeablePoint (Sum r a)

instance (Semiring r, Commutative r, FibredOriented m) => Oriented (Sum r m) where
  orientation :: Sum r m -> Orientation (Point (Sum r m))
orientation = Sum r m -> Orientation (Point (Sum r m))
Sum r m -> Root (Sum r m)
forall f. Fibred f => f -> Root f
root

instance (Semiring r, Commutative r, Multiplicative m, FibredOriented m, Ord m)
  => Multiplicative (Sum r m) where
  one :: Point (Sum r m) -> Sum r m
one = Form (Sum r m) -> Sum r m
SumForm r m -> Sum r m
forall x. Constructable x => Form x -> x
make (SumForm r m -> Sum r m)
-> (Point m -> SumForm r m) -> Point m -> Sum r m
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
. m -> SumForm r m
forall r a. a -> SumForm r a
S (m -> SumForm r m) -> (Point m -> m) -> Point m -> SumForm r m
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
. Point m -> m
forall c. Multiplicative c => Point c -> c
one

  Sum SumForm r m
f * :: Sum r m -> Sum r m -> Sum r m
* Sum SumForm r m
g 
    | SumForm r m -> Point (SumForm r m)
forall q. Oriented q => q -> Point q
end SumForm r m
g Point m -> Point m -> Bool
forall a. Eq a => a -> a -> Bool
/= SumForm r m -> Point (SumForm r m)
forall q. Oriented q => q -> Point q
start SumForm r m
f = ArithmeticException -> Sum r m
forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable
    | Bool
otherwise = Form (Sum r m) -> Sum r m
SumForm r m -> Sum r m
forall x. Constructable x => Form x -> x
make
                (SumForm r m -> Sum r m) -> SumForm r m -> Sum r m
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Root m -> LinearCombination r m -> SumForm r m
forall r a.
Semiring r =>
Root a -> LinearCombination r a -> SumForm r a
lcsmf (SumForm r m -> Point (SumForm r m)
forall q. Oriented q => q -> Point q
start SumForm r m
g Point m -> Point m -> Orientation (Point m)
forall p. p -> p -> Orientation p
:> SumForm r m -> Point (SumForm r m)
forall q. Oriented q => q -> Point q
end SumForm r m
f)
                (LinearCombination r m -> SumForm r m)
-> LinearCombination r m -> SumForm r m
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(r, m)] -> LinearCombination r m
forall r a. [(r, a)] -> LinearCombination r a
LinearCombination
                ([(r, m)] -> LinearCombination r m)
-> [(r, m)] -> LinearCombination r m
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(r
rr -> r -> r
forall c. Multiplicative c => c -> c -> c
*r
s,m
am -> m -> m
forall c. Multiplicative c => c -> c -> c
*m
b) | (r
r,m
a) <- [(r, m)]
as, (r
s,m
b) <- [(r, m)]
bs]
      where LinearCombination [(r, m)]
as = SumForm r m -> LinearCombination r m
forall r a. Semiring r => SumForm r a -> LinearCombination r a
smflc SumForm r m
f
            LinearCombination [(r, m)]
bs = SumForm r m -> LinearCombination r m
forall r a. Semiring r => SumForm r a -> LinearCombination r a
smflc SumForm r m
g

instance (Semiring r, Commutative r, FibredOriented m) => FibredOriented (SumForm r m)
instance (Semiring r, Commutative r, FibredOriented m) => FibredOriented (Sum r m)

instance (Semiring r, Commutative r, Multiplicative m, FibredOriented m, Ord m)
  => Distributive (Sum r m)

instance (Semiring r, Commutative r, Multiplicative m, FibredOriented m, Ord m)
  => Algebraic (Sum r m)