{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Entity.Product.Definition
-- Description : definition of free products over oriented symbols
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- defintion of free products over 'Oriented' symbols with exponents in a 'Number'.
--
-- __Note__ On 'Oriented' structures the canonical injection 'inj' and projection
-- 'prj' are bijections between the 'valid' entities of 'Path' and @'Product' 'N'@.
-- This is not true betwenn 'Path' and @'ProductForm' 'N'@ as
--
-- >>> prj (P 3 :^ 2 :: ProductForm N Q) :: Path Q
-- Path () [3,3]
--
-- and
--
-- >>> prj (P 3 :* P 3 :: ProductForm N Q) :: Path Q
-- Path () [3,3]
--
-- both map to the same 'Path'! But
--
-- >>> let p = make (P 3) :: Product N Q in p * p == p ^ 2
-- True
module OAlg.Entity.Product.Definition
  (
    -- * Product
    Product(), prLength, prFactor, prFactors, prwrd
  , nProduct, zProduct
  , prdMapTotal, prFromOp
  
    -- * Word
  , Word(..), fromWord, prfwrd, wrdprf, wrdPrfGroup
  , nFactorize, nFactorize'

    -- * Form
  , ProductForm(..), prfLength, prfDepth, prfFactors
  , nProductForm, zProductForm
  , prfInverse, prfFromOp
  , prfMapTotal

    -- ** Reduction
  , prfReduce, prfReduceWith

    -- ** Operations
  , prfopr, prfopr', prfopl, prfopl'

  )

  where

import Control.Monad
import Control.Exception

import Data.List ((++),repeat,map,groupBy,zip)

import Data.Foldable hiding (product)
import Data.Monoid hiding (Product)

import OAlg.Prelude

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

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Ring
import OAlg.Structure.Number
import OAlg.Structure.Exponential

import OAlg.Hom

import OAlg.Entity.Sequence.Definition

infixr 7 :*
infixl 9 :^

--------------------------------------------------------------------------------
-- ProductForm -

-- | form for a free product over 'Oriented' symbols in @__a__@ with exponents in @__r__@.
--
--   __Definition__ Let @__r__@ be a 'Number'. A 'ProductForm' @pf@ is 'valid'
--  if and only if @'orientation' pf@ is 'valid' (see definition below) and all
--  its symbols @x@ - where @'P' x@ occurs in @pf@ - are 'valid'.
--
--  The 'orientation' of @pf@ is defined according:
--
-- @
--  orientation pf = case pf of
--    One p    -> one p
--    P a      -> orientation a
--    f :^ r   -> orientation f ^ r where (^) = power
--    f :* g   -> orientation f * orientation g
-- @
--
--  __Note__ 'Number' is required for @-1@, @0@ and @1@ are not degenerated as in @Z/2@ or
--  @Z/1@.
data ProductForm r a
  = One (Point a)
  | P a
  | ProductForm r a :^ r
  | ProductForm r a :* ProductForm r a

deriving instance (Oriented a, Entity r) => Show (ProductForm r a)
deriving instance (Oriented a, Entity r) => Eq (ProductForm r a)
deriving instance ( Oriented a, Entity r
                  , Ord a, OrdPoint a, Ord r
                  ) => Ord (ProductForm r a)

--------------------------------------------------------------------------------
-- ProductForm - Entity -

instance (Oriented a, Number r) => Validable (ProductForm r a) where
  valid :: ProductForm r a -> Statement
valid ProductForm r a
pf = [Statement] -> Statement
And [ String -> Label
Label String
"orientation" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
pf)
                 , String -> Label
Label String
"symbols" Label -> Statement -> Statement
:<=>: forall {a} {a}.
(Validable a, Validable a, Validable (Point a)) =>
ProductForm a a -> Statement
vld ProductForm r a
pf
                 ] where

    vld :: ProductForm a a -> Statement
vld ProductForm a a
pf = case ProductForm a a
pf of
      One Point a
e   -> forall a. Validable a => a -> Statement
valid Point a
e
      P a
a     -> forall a. Validable a => a -> Statement
valid a
a
      ProductForm a a
pf :^ a
r -> ProductForm a a -> Statement
vld ProductForm a a
pf forall b. Boolean b => b -> b -> b
&& forall a. Validable a => a -> Statement
valid a
r
      ProductForm a a
a :* ProductForm a a
b  -> ProductForm a a -> Statement
vld ProductForm a a
a forall b. Boolean b => b -> b -> b
&& ProductForm a a -> Statement
vld ProductForm a a
b
    
instance (Oriented a, Number r) => Entity (ProductForm r a)

pf :: Int -> Char -> ProductForm r (Orientation Char)
pf :: forall r. Int -> Char -> ProductForm r (Orientation Char)
pf Int
0 Char
c = forall r a. Point a -> ProductForm r a
One Char
c
pf Int
i Char
c = forall r a. a -> ProductForm r a
P (Char
cforall p. p -> p -> Orientation p
:>Char
c) forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall r. Int -> Char -> ProductForm r (Orientation Char)
pf (Int
iforall a. Abelian a => a -> a -> a
-Int
1) Char
c

--------------------------------------------------------------------------------
-- ProductForm - Oriented -

instance (Oriented a, Number r) => Oriented (ProductForm r a) where
  type Point (ProductForm r a) = Point a
  orientation :: ProductForm r a -> Orientation (Point (ProductForm r a))
orientation ProductForm r a
pf = case ProductForm r a
pf of
    One Point a
p    -> forall c. Multiplicative c => Point c -> c
one Point a
p
    P a
a      -> forall q. Oriented q => q -> Orientation (Point q)
orientation a
a
    ProductForm r a
f :^ r
r   -> forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
f Orientation (Point a) -> r -> Orientation (Point a)
^ r
r where ^ :: Orientation (Point a) -> r -> Orientation (Point a)
(^) = forall f r. (Real f, Number r) => f -> r -> f
power
    ProductForm r a
f :* ProductForm r a
g   -> forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
f forall c. Multiplicative c => c -> c -> c
* forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
g

--------------------------------------------------------------------------------
-- ProductForm - Foldable -

instance Foldable (ProductForm N) where
  foldMap :: forall m a. Monoid m => (a -> m) -> ProductForm N a -> m
foldMap a -> m
_ (One Point a
_)  = forall a. Monoid a => a
mempty
  foldMap a -> m
f (P a
a)    = a -> m
f a
a
  foldMap a -> m
_ (ProductForm N a
_ :^ N
0) = forall a. Monoid a => a
mempty
  foldMap a -> m
f (ProductForm N a
p :^ N
n) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ProductForm N a
p forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (ProductForm N a
p forall r a. ProductForm r a -> r -> ProductForm r a
:^ forall a. Enum a => a -> a
pred N
n)
  foldMap a -> m
f (ProductForm N a
p :* ProductForm N a
q) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ProductForm N a
p forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ProductForm N a
q

--------------------------------------------------------------------------------
-- ProductForm - Canonical -

instance Embeddable (Path a) (ProductForm r a) where
  inj :: Path a -> ProductForm r a
inj (Path Point a
s [a]
fs) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
(:*) (forall r a. Point a -> ProductForm r a
One Point a
s) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall r a. a -> ProductForm r a
P [a]
fs

instance Embeddable a (ProductForm r a) where
  inj :: a -> ProductForm r a
inj = forall r a. a -> ProductForm r a
P
  
instance Oriented a => Projectible (Path a) (ProductForm N a) where
  prj :: ProductForm N a -> Path a
prj ProductForm N a
pf = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
start ProductForm N a
pf) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ProductForm N a
pf)

instance Integral r => Embeddable (ProductForm N a) (ProductForm r a) where
  inj :: ProductForm N a -> ProductForm r a
inj (One Point a
p)  = forall r a. Point a -> ProductForm r a
One Point a
p
  inj (P a
x)    = forall r a. a -> ProductForm r a
P a
x
  inj (ProductForm N a
x :^ N
n) = forall a b. Embeddable a b => a -> b
inj ProductForm N a
x forall r a. ProductForm r a -> r -> ProductForm r a
:^ (forall a. Additive a => N -> a -> a
ntimes N
n forall r. Semiring r => r
rOne)
  inj (ProductForm N a
x :* ProductForm N a
y) = forall a b. Embeddable a b => a -> b
inj ProductForm N a
x forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall a b. Embeddable a b => a -> b
inj ProductForm N a
y

instance Integral r => Projectible (ProductForm N a) (ProductForm r a) where
  prj :: ProductForm r a -> ProductForm N a
prj (One Point a
p)  = forall r a. Point a -> ProductForm r a
One Point a
p
  prj (P a
x)    = forall r a. a -> ProductForm r a
P a
x
  prj (ProductForm r a
x :^ r
r) = forall a b. Projectible a b => b -> a
prj ProductForm r a
x forall r a. ProductForm r a -> r -> ProductForm r a
:^ N
n where n :: N
n = forall a b. Projectible a b => b -> a
prj (forall r. Number r => r -> Z
zFloor r
r)
  prj (ProductForm r a
x :* ProductForm r a
y) = forall a b. Projectible a b => b -> a
prj ProductForm r a
x forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall a b. Projectible a b => b -> a
prj ProductForm r a
y
  
--------------------------------------------------------------------------------
-- prfopl -

-- | applicative operation from the left.
prfopl :: (t -> x -> x) -> ProductForm N t -> x -> x
prfopl :: forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) ProductForm N t
pf x
x = case ProductForm N t
pf of
  One Point t
_    -> x
x
  P t
t      -> t
t t -> x -> x
*> x
x
  ProductForm N t
_ :^ N
0   -> x
x
  ProductForm N t
a :^ N
n   -> forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) (ProductForm N t
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ forall a. Enum a => a -> a
pred N
n) (forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) ProductForm N t
a x
x)
  ProductForm N t
a :* ProductForm N t
b   -> forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) ProductForm N t
a (forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) ProductForm N t
b x
x)

--------------------------------------------------------------------------------
-- prfopl' -

-- | partially strict version of 'prfopl', i.e. every @n@-th application will be
-- reduced to head normal form.
--
-- Let @x' = 'prfopl'' n op p x@.
--
-- __Pre__ @0 '<' n@.
--
-- __Post__ @x' '==' 'prfopl' op p x@.
prfopl' :: N -> (t -> x -> x) -> ProductForm N t -> x -> x
prfopl' :: forall t x. N -> (t -> x -> x) -> ProductForm N t -> x -> x
prfopl' N
n t -> x -> x
op ProductForm N t
p x
x = forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> (x, N) -> (x, N)
op' ProductForm N t
p (x
x,N
0) where
  op' :: t -> (x, N) -> (x, N)
op' t
t (x
x,N
i) = if N
i forall a. Integral a => a -> a -> a
`mod` N
n forall a. Eq a => a -> a -> Bool
== N
0
    then x
x' seq :: forall a b. a -> b -> b
`seq` (x
x',N
0) else (x
x',N
iforall a. Additive a => a -> a -> a
+N
1) where x' :: x
x' = t
t t -> x -> x
`op` x
x


--------------------------------------------------------------------------------
-- prfopr -

-- | applicative operation from the right.
prfopr :: (x -> t -> x) -> x -> ProductForm N t -> x
prfopr :: forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) x
x ProductForm N t
pf = case ProductForm N t
pf of
  One Point t
_    -> x
x
  P t
t      -> x
x x -> t -> x
<* t
t
  ProductForm N t
_ :^ N
0   -> x
x
  ProductForm N t
a :^ N
n   -> forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) (forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) x
x ProductForm N t
a) (ProductForm N t
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ forall a. Enum a => a -> a
pred N
n)
  ProductForm N t
a :* ProductForm N t
b   -> forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) (forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) x
x ProductForm N t
a) ProductForm N t
b
  
--------------------------------------------------------------------------------
-- prfopr' -

-- | partially strict version of 'prfopr', i.e. every @n@-th application will be
-- reduced to head normal form.
--
-- Let @x' = 'prfopr'' n op x p@.
--
-- __Pre__ @0 '<' n@.
--
-- __Post__ @x' '==' 'prfopr' op x p@.
prfopr' :: N -> (x -> t -> x) -> x -> ProductForm N t -> x
prfopr' :: forall x t. N -> (x -> t -> x) -> x -> ProductForm N t -> x
prfopr' N
n x -> t -> x
op x
x ProductForm N t
p = forall a b. (a, b) -> a
fst forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr (x, N) -> t -> (x, N)
op' (x
x,N
0) ProductForm N t
p where
  op' :: (x, N) -> t -> (x, N)
op' (x
x,N
i) t
t = if N
i forall a. Integral a => a -> a -> a
`mod` N
n forall a. Eq a => a -> a -> Bool
== N
0
    then x
x' seq :: forall a b. a -> b -> b
`seq` (x
x',N
0) else (x
x',N
iforall a. Additive a => a -> a -> a
+N
1) where x' :: x
x' = x
x x -> t -> x
`op` t
t


--------------------------------------------------------------------------------
-- prfLength -

-- | length.
prfLength :: Number r => ProductForm r a -> N
prfLength :: forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
p = case ProductForm r a
p of
  One Point a
_  -> N
0
  P a
_    -> N
1
  ProductForm r a
f :^ r
r -> forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
f forall c. Multiplicative c => c -> c -> c
* forall {b} {r}. (Projectible b Z, Number r) => r -> b
nFloor r
r
  ProductForm r a
f :* ProductForm r a
g -> forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
f forall a. Additive a => a -> a -> a
+ forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
g
  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 (ProductForm N a) where
  lengthN :: ProductForm N a -> N
lengthN = forall r a. Number r => ProductForm r a -> N
prfLength
  
----------------------------------------
-- prfDepth -

-- | depth.
prfDepth :: ProductForm r a -> N
prfDepth :: forall r a. ProductForm r a -> N
prfDepth ProductForm r a
p = case ProductForm r a
p of
  One Point a
_  -> N
0
  P a
_    -> N
1
  ProductForm r a
f :^ r
_ -> forall r a. ProductForm r a -> N
prfDepth ProductForm r a
f forall a. Additive a => a -> a -> a
+ N
1
  ProductForm r a
f :* ProductForm r a
g -> forall a. Ord a => a -> a -> a
max (forall r a. ProductForm r a -> N
prfDepth ProductForm r a
f) (forall r a. ProductForm r a -> N
prfDepth ProductForm r a
g) forall a. Additive a => a -> a -> a
+ N
1

--------------------------------------------------------------------------------
-- Word -

-- | list of symbols in @__a__@ together with an exponent in @__r__@.
newtype Word r a = Word [(a,r)] deriving (Int -> Word r a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a. (Show a, Show r) => Int -> Word r a -> ShowS
forall r a. (Show a, Show r) => [Word r a] -> ShowS
forall r a. (Show a, Show r) => Word r a -> String
showList :: [Word r a] -> ShowS
$cshowList :: forall r a. (Show a, Show r) => [Word r a] -> ShowS
show :: Word r a -> String
$cshow :: forall r a. (Show a, Show r) => Word r a -> String
showsPrec :: Int -> Word r a -> ShowS
$cshowsPrec :: forall r a. (Show a, Show r) => Int -> Word r a -> ShowS
Show,Word r a -> Word r a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a. (Eq a, Eq r) => Word r a -> Word r a -> Bool
/= :: Word r a -> Word r a -> Bool
$c/= :: forall r a. (Eq a, Eq r) => Word r a -> Word r a -> Bool
== :: Word r a -> Word r a -> Bool
$c== :: forall r a. (Eq a, Eq r) => Word r a -> Word r a -> Bool
Eq,Word r a -> Statement
forall a. (a -> Statement) -> Validable a
forall r a. (Validable a, Validable r) => Word r a -> Statement
valid :: Word r a -> Statement
$cvalid :: forall r a. (Validable a, Validable r) => Word r a -> Statement
Validable)

--------------------------------------------------------------------------------
-- fromWord -

-- | the underlying list of @a@'s with their exponent.
fromWord :: Word r a -> [(a,r)]
fromWord :: forall r a. Word r a -> [(a, r)]
fromWord (Word [(a, r)]
ars) = [(a, r)]
ars

--------------------------------------------------------------------------------
-- wrdAggr -

-- | aggregating words.
wrdAggr :: (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr :: forall a r. (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr = forall r a. [(a, r)] -> Word r a
Word 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} {a}. (Distributive b, Total b) => [(a, b)] -> (a, 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} {b} {b}. Eq a => (a, b) -> (a, b) -> Bool
(<=>) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. Word r a -> [(a, r)]
fromWord where
  (a, b)
a <=> :: (a, b) -> (a, b) -> Bool
<=> (a, b)
b = forall a b. (a, b) -> a
fst (a, b)
a forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (a, b)
b
  aggr :: [(a, b)] -> (a, b)
aggr as :: [(a, b)]
as@((a
a,b
_):[(a, b)]
_) = (a
a,forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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) -> b
snd [(a, b)]
as)

--------------------------------------------------------------------------------
-- nFactorize -

-- | factorization of a natural number to powers of primes.
--   For @0@ there will be thrown 'Undefined'.
nFactorize :: N -> Word N N
nFactorize :: N -> Word N N
nFactorize N
0 = forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
Undefined String
"nFactorize 0"
nFactorize N
n = forall a r. (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. [(a, r)] -> Word r a
Word forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall {t} {b}. (Integral t, Num t, Num b) => [t] -> t -> [(t, b)]
fct [N]
primes N
n where
  fct :: [t] -> t -> [(t, b)]
fct [t]
_ t
1   = []
  fct prms :: [t]
prms@(t
p:[t]
prms') t
n = if t
n forall a. Integral a => a -> a -> a
`mod` t
p forall a. Eq a => a -> a -> Bool
== t
0
    then (t
p,b
1)forall a. a -> [a] -> [a]
:[t] -> t -> [(t, b)]
fct [t]
prms (t
n forall a. Integral a => a -> a -> a
`div` t
p)
    else [t] -> t -> [(t, b)]
fct [t]
prms' t
n

-- | factorization of a natural number to powers of primes smaller then the given bound.
--   For @0@ there will be thrown 'Undefined'.
nFactorize' 
  :: N -- ^ bound for the primes
  -> N -- ^ a natural number
  -> Word N N
nFactorize' :: N -> N -> Word N N
nFactorize' N
_ N
0    = forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
Undefined String
"nFactorize 0"
nFactorize' N
pMax N
n = forall a r. (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. [(a, r)] -> Word r a
Word forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [N] -> N -> [(N, N)]
fct [N]
primes N
n where
  fct :: [N] -> N -> [(N, N)]
fct [N]
_ N
1 = []
  fct ps :: [N]
ps@(N
p:[N]
ps') N
n | N
pMax forall a. Ord a => a -> a -> Bool
<  N
p      = []
                   | N
n forall a. Integral a => a -> a -> a
`mod` N
p forall a. Eq a => a -> a -> Bool
== N
0 = (N
p,N
1)forall a. a -> [a] -> [a]
:[N] -> N -> [(N, N)]
fct [N]
ps (N
n forall a. Integral a => a -> a -> a
`div` N
p)
                   | Bool
otherwise      = [N] -> N -> [(N, N)]
fct [N]
ps' N
n
                   
--------------------------------------------------------------------------------
-- prfInverse -

-- | formal inverse
--
--  Let @p@ in @'ProductForm' r a@ then:
--
--   __Pre__ If @p@ contains a factor @'P' a@ then @'minusOne' '/=' 'Nothing'@.
--
--   __Post__ the formal inverse.
prfInverse :: Number r => ProductForm r a -> ProductForm r a
prfInverse :: forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
p = case ProductForm r a
p of
  One Point a
p    -> forall r a. Point a -> ProductForm r a
One Point a
p
  P a
a      -> case forall r. Number r => Maybe r
minusOne of
    Just r
e -> forall r a. a -> ProductForm r a
P a
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
e
    Maybe r
_      -> forall a e. Exception e => e -> a
throw ArithmeticException
NoMinusOne
  P a
a :^ r
z -> case forall r. Number r => Maybe r
minusOne of
    Just r
e -> forall r a. a -> ProductForm r a
P a
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ (r
eforall c. Multiplicative c => c -> c -> c
*r
z)
    Maybe r
_      -> forall a e. Exception e => e -> a
throw ArithmeticException
NoMinusOne
  ProductForm r a
a :^ r
z   -> forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
z
  ProductForm r a
a :* ProductForm r a
b   -> forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
b forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
a

--------------------------------------------------------------------------------
-- prfFromOp -

-- | from 'Op' symbols.
prfFromOp :: ProductForm r (Op a) -> ProductForm r a
prfFromOp :: forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp (One Point (Op a)
p)    = forall r a. Point a -> ProductForm r a
One Point (Op a)
p
prfFromOp (P (Op a
a)) = forall r a. a -> ProductForm r a
P a
a
prfFromOp (ProductForm r (Op a)
fo :^ r
r)  = forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
fo forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
prfFromOp (ProductForm r (Op a)
fo :* ProductForm r (Op a)
fg) = forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
fg forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
fo

--------------------------------------------------------------------------------
-- prpToOp -

-- | to 'Op' symbols.
prfToOp :: ProductForm r a -> ProductForm r (Op a)
prfToOp :: forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp (One Point a
p)  = forall r a. Point a -> ProductForm r a
One Point a
p
prfToOp (P a
a)    = forall r a. a -> ProductForm r a
P (forall x. x -> Op x
Op a
a)
prfToOp (ProductForm r a
f :^ r
r) = forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp ProductForm r a
f forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
prfToOp (ProductForm r a
f :* ProductForm r a
g) = forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp ProductForm r a
g forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp ProductForm r a
f

--------------------------------------------------------------------------------
-- prfwrd -

-- | transforming a 'ProductForm' to its corresponding 'Word'.
prfwrd :: Integral r => ProductForm r a -> Word r a
prfwrd :: forall r a. Integral r => ProductForm r a -> Word r a
prfwrd ProductForm r a
pf = forall r a. [(a, r)] -> Word r a
Word (forall {r} {a}. Number r => ProductForm r a -> [(a, r)]
tow ProductForm r a
pf) where
  tow :: ProductForm r a -> [(a, r)]
tow ProductForm r a
pf = case ProductForm r a
pf of
    One Point a
_       -> []
    P a
a         -> [(a
a,forall r. Semiring r => r
rOne)]
    P a
a :^ r
z    -> [(a
a,r
z)]
    ProductForm r a
a :^ r
y :^ r
z -> ProductForm r a -> [(a, r)]
tow (ProductForm r a
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ (r
yforall c. Multiplicative c => c -> c -> c
*r
z)) 
    ProductForm r a
a :^ r
z      -> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. N -> [a] -> [a]
takeN N
n forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ProductForm r a -> [(a, r)]
tow forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ if r
z forall a. Ord a => a -> a -> Bool
< forall r. Semiring r => r
rZero then forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
a else ProductForm r a
a
      where n :: N
n = 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
z
    ProductForm r a
a :* ProductForm r a
b      -> ProductForm r a -> [(a, r)]
tow ProductForm r a
a forall a. [a] -> [a] -> [a]
++ ProductForm r a -> [(a, r)]
tow ProductForm r a
b

--------------------------------------------------------------------------------
-- wrdprf -

-- | transforming a 'Word' to it corresponding 'ProductForm'.
--
-- __Note__ the 'Point' is needed for empty 'Word's.
wrdprf :: Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf :: forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf Point a
p (Word [(a, r)]
ws) = forall {r} {a}.
(Distributive r, Total r) =>
Point a -> [(a, r)] -> ProductForm r a
prf Point a
p [(a, r)]
ws where
  prf :: Point a -> [(a, r)] -> ProductForm r a
prf Point a
p [(a, r)]
ws = case [(a, r)]
ws of 
    []      -> forall r a. Point a -> ProductForm r a
One Point a
p
    [(a
a,r
r)] -> if r
r forall a. Eq a => a -> a -> Bool
== forall r. Semiring r => r
rOne then forall r a. a -> ProductForm r a
P a
a else (forall r a. a -> ProductForm r a
P a
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r)
    (a, r)
w:[(a, r)]
ws    -> Point a -> [(a, r)] -> ProductForm r a
prf Point a
p [(a, r)
w] forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* Point a -> [(a, r)] -> ProductForm r a
prf Point a
p [(a, r)]
ws

--------------------------------------------------------------------------------
-- wrdPrfGroup -

-- | reducing a 'Word' by adding the exponents of consecutive equal symbols and
-- eliminating symbols with zero exponents.
wrdPrfGroup :: (Eq a, Semiring r) => Word r a -> Rdc (Word r a)
wrdPrfGroup :: forall a r. (Eq a, Semiring r) => Word r a -> Rdc (Word r a)
wrdPrfGroup (Word [(a, r)]
ws) = forall {b} {a}.
(Distributive b, Total b, Eq a) =>
[(a, b)] -> Action RdcState [(a, b)]
rdcw [(a, r)]
ws forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. [(a, r)] -> Word r a
Word where
  rdcw :: [(a, b)] -> Action RdcState [(a, b)]
rdcw [(a, b)]
ws = case [(a, b)]
ws of
    (a
_,b
r):[(a, b)]
ws       | b
r forall a. Eq a => a -> a -> Bool
== forall r. Semiring r => r
rZero -> forall x. x -> Rdc x
reducesTo [(a, b)]
ws forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(a, b)] -> Action RdcState [(a, b)]
rdcw 
    (a
a,b
r):(a
b,b
s):[(a, b)]
ws | a
a forall a. Eq a => a -> a -> Bool
== a
b     -> forall x. x -> Rdc x
reducesTo ((a
a,b
rforall a. Additive a => a -> a -> a
+b
s)forall a. a -> [a] -> [a]
:[(a, b)]
ws) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(a, b)] -> Action RdcState [(a, b)]
rdcw
    (a, b)
ar:[(a, b)]
ws                       -> [(a, b)] -> Action RdcState [(a, b)]
rdcw [(a, b)]
ws forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((a, b)
arforall a. a -> [a] -> [a]
:)
    []                          -> forall (m :: * -> *) a. Monad m => a -> m a
return [(a, b)]
ws         
  
--------------------------------------------------------------------------------
-- prfReduceWith -

-- | reduces a product form by the given reduction rules for words until no more
--   reductions are applicable.
prfReduceWith :: (Oriented a, Integral r)
  => (Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
prfReduceWith :: forall a r.
(Oriented a, Integral r) =>
(Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
prfReduceWith Word r a -> Rdc (Word r a)
rel ProductForm r a
pf
  = forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf (forall q. Oriented q => q -> Point q
end ProductForm r a
pf)
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. (x -> Rdc x) -> x -> x
reduceWith (forall a r. (Eq a, Semiring r) => Word r a -> Rdc (Word r a)
wrdPrfGroup forall x. (x -> Rdc x) -> (x -> Rdc x) -> x -> Rdc x
>>>= Word r a -> Rdc (Word r a)
rel)
  forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Integral r => ProductForm r a -> Word r a
prfwrd ProductForm r a
pf

--------------------------------------------------------------------------------
-- prfFactors -

-- | list of elementary factors.
prfFactors :: ProductForm N a -> [a]
prfFactors :: forall a. ProductForm N a -> [a]
prfFactors = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

-- | gets the @n@-the symbol.
prfLookup :: ProductForm N a -> N -> Maybe a
prfLookup :: forall a. ProductForm N a -> N -> Maybe a
prfLookup ProductForm N a
p = forall {t} {a}.
(Additive t, Ord t) =>
t -> [(a, t)] -> t -> Maybe a
lookup N
0 (forall r a. Word r a -> [(a, r)]
fromWord forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r a. Integral r => ProductForm r a -> Word r a
prfwrd ProductForm N a
p) where
  lookup :: t -> [(a, t)] -> t -> Maybe a
lookup t
_ [] t
_         = forall a. Maybe a
Nothing
  lookup t
l ((a
a,t
e):[(a, t)]
ws) t
i = if t
i forall a. Ord a => a -> a -> Bool
< t
l' then forall a. a -> Maybe a
Just a
a else t -> [(a, t)] -> t -> Maybe a
lookup t
l' [(a, t)]
ws t
i where l' :: t
l' = t
lforall a. Additive a => a -> a -> a
+t
e 
  
instance Sequence (ProductForm N) N x where
  list :: forall (p :: * -> *). p N -> ProductForm N x -> [(x, N)]
list p N
_ ProductForm N x
pf = forall a. ProductForm N a -> [a]
prfFactors ProductForm N x
pf forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]
  ?? :: ProductForm N x -> N -> Maybe x
(??) = forall a. ProductForm N a -> N -> Maybe a
prfLookup
  
--------------------------------------------------------------------------------
-- prfReduce -

-- | reducing a 'ProductForm'  according to @'prfReduceWith' 'return'@.
prfReduce :: (Oriented a, Integral r) => ProductForm r a -> ProductForm r a
prfReduce :: forall a r.
(Oriented a, Integral r) =>
ProductForm r a -> ProductForm r a
prfReduce = forall a r.
(Oriented a, Integral r) =>
(Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
prfReduceWith forall (m :: * -> *) a. Monad m => a -> m a
return

instance (Oriented a, Integral r) => Reducible (ProductForm r a) where
  reduce :: ProductForm r a -> ProductForm r a
reduce = forall a r.
(Oriented a, Integral r) =>
ProductForm r a -> ProductForm r a
prfReduce


--------------------------------------------------------------------------------
-- Product -

-- | free product over 'Oriented' symbols in @__a__@ with exponents in a 'Integral' @__r__@.
--
-- __Definition__ A 'Product' @p@ is 'valid' if and only if its underlying
-- 'ProductForm' @pf@ is 'valid' and @pf@ is reduced, i.e. @pf == 'reduce' pf@.
newtype Product r a = Product (ProductForm r a) deriving (Int -> Product r a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a. (Oriented a, Entity r) => Int -> Product r a -> ShowS
forall r a. (Oriented a, Entity r) => [Product r a] -> ShowS
forall r a. (Oriented a, Entity r) => Product r a -> String
showList :: [Product r a] -> ShowS
$cshowList :: forall r a. (Oriented a, Entity r) => [Product r a] -> ShowS
show :: Product r a -> String
$cshow :: forall r a. (Oriented a, Entity r) => Product r a -> String
showsPrec :: Int -> Product r a -> ShowS
$cshowsPrec :: forall r a. (Oriented a, Entity r) => Int -> Product r a -> ShowS
Show,Product r a -> Product r a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a.
(Oriented a, Entity r) =>
Product r a -> Product r a -> Bool
/= :: Product r a -> Product r a -> Bool
$c/= :: forall r a.
(Oriented a, Entity r) =>
Product r a -> Product r a -> Bool
== :: Product r a -> Product r a -> Bool
$c== :: forall r a.
(Oriented a, Entity r) =>
Product r a -> Product r a -> Bool
Eq,Product r a -> Product r a -> Bool
Product r a -> Product r a -> Ordering
Product r a -> Product r a -> Product 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}.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Eq (Product r a)
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Bool
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Ordering
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Product r a
min :: Product r a -> Product r a -> Product r a
$cmin :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Product r a
max :: Product r a -> Product r a -> Product r a
$cmax :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Product r a
>= :: Product r a -> Product r a -> Bool
$c>= :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Bool
> :: Product r a -> Product r a -> Bool
$c> :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Bool
<= :: Product r a -> Product r a -> Bool
$c<= :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Bool
< :: Product r a -> Product r a -> Bool
$c< :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Bool
compare :: Product r a -> Product r a -> Ordering
$ccompare :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Entity r) =>
Product r a -> Product r a -> Ordering
Ord)

instance (Oriented a, Integral r) => Validable (Product r a) where
  valid :: Product r a -> Statement
valid (Product ProductForm r a
pf) = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid ProductForm r a
pf
                           , String -> Label
Label String
"reduced"
                             Label -> Statement -> Statement
:<=>: (forall e. Reducible e => e -> e
reduce ProductForm r a
pf forall a. Eq a => a -> a -> Bool
== ProductForm r a
pf) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"pf"String -> String -> Parameter
:=forall a. Show a => a -> String
show ProductForm r a
pf]
                           ]

deriving instance Foldable (Product N)
deriving instance LengthN (Product N a)

---------------------------------------
-- Product - Constructable -

instance Exposable (Product r a) where
  type Form (Product r a) = ProductForm r a
  form :: Product r a -> Form (Product r a)
form (Product ProductForm r a
p) = ProductForm r a
p

instance (Oriented a, Integral r) => Constructable (Product r a) where
  make :: Form (Product r a) -> Product r a
make = forall r a. ProductForm r a -> Product r a
Product forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall e. Reducible e => e -> e
reduce

--------------------------------------------------------------------------------
-- Product - Sequence -

instance Sequence (Product N) N a where
  list :: forall (p :: * -> *). p N -> Product N a -> [(a, N)]
list p N
f = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict (forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list p N
f)
  ?? :: Product N a -> N -> Maybe a
(??) = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
(??)
  
----------------------------------------
-- Product - Canonical -

instance (Oriented a, Integral r) => Embeddable a (Product r a) where
  inj :: a -> Product r a
inj a
a = forall x. Constructable x => Form x -> x
make forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. Embeddable a b => a -> b
inj a
a

instance (Oriented a, Integral r) => Embeddable (Path a) (Product r a) where
  inj :: Path a -> Product r a
inj Path a
p = forall x. Constructable x => Form x -> x
make forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. Embeddable a b => a -> b
inj Path a
p

instance Oriented a => Projectible (Path a) (Product N a) where
  prj :: Product N a -> Path a
prj = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall a b. Projectible a b => b -> a
prj
  
----------------------------------------
-- Product - Structure -

instance (Oriented a, Integral r) => Entity (Product r a)

instance (Oriented a, Integral r) => Oriented (Product r a) where
  type Point (Product r a) = Point a
  orientation :: Product r a -> Orientation (Point (Product r a))
orientation = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall q. Oriented q => q -> Orientation (Point q)
orientation

instance (Oriented a, Integral r) => Multiplicative (Product r a) where
  one :: Point (Product r a) -> Product r a
one Point (Product r a)
p                 = forall x. Constructable x => Form x -> x
make (forall r a. Point a -> ProductForm r a
One Point (Product r a)
p)
  
  Product ProductForm r a
f * :: Product r a -> Product r a -> Product r a
* Product ProductForm r a
g | forall q. Oriented q => q -> Point q
start ProductForm r a
f forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end ProductForm r a
g = forall x. Constructable x => Form x -> x
make (ProductForm r a
f forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a
g)
                        | Bool
otherwise        = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

  npower :: Product r a -> N -> Product r a
npower Product r a
p N
n = Product r a
p forall f. Exponential f => f -> Exponent f -> f
^ r
r where r :: r
r = forall a. Additive a => N -> a -> a
ntimes N
n forall r. Semiring r => r
rOne

instance (Oriented a, Integral r, Ring r) => Invertible (Product r a) where
  tryToInvert :: Product r a -> Solver (Product r a)
tryToInvert = forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Invertible c => c -> c
invert 
  invert :: Product r a -> Product r a
invert (Product ProductForm r a
p) = forall x. Constructable x => Form x -> x
make (ProductForm r a
p forall r a. ProductForm r a -> r -> ProductForm r a
:^ forall a. Abelian a => a -> a
negate forall r. Semiring r => r
rOne)

instance (Oriented a, Integral r, Ring r) => Cayleyan (Product r a)

instance (Oriented a, Integral r) => Exponential (Product r a) where
  type Exponent (Product r a) = r
  p :: Product r a
p@(Product ProductForm r a
pf) ^ :: Product r a -> Exponent (Product r a) -> Product r a
^ Exponent (Product r a)
r
    | forall b. Boolean b => b -> b
not (forall r. Number r => r -> r
abs Exponent (Product r a)
r forall a. Eq a => a -> a -> Bool
== forall r. Semiring r => r
rOne forall b. Boolean b => b -> b -> b
|| forall q. Oriented q => q -> Bool
isEndo Product r a
p) = forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential
    | Bool
otherwise                       = forall x. Constructable x => Form x -> x
make (ProductForm r a
pf forall r a. ProductForm r a -> r -> ProductForm r a
:^ Exponent (Product r a)
r)

--------------------------------------------------------------------------------
-- prFactors -

-- | the list of primary factors.
prFactors :: Product N a -> [a]
prFactors :: forall a. Product N a -> [a]
prFactors = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

--------------------------------------------------------------------------------
-- prLength -

-- | number of primary factors where where all simple factors are expanded according to there exponent.
prLength :: Product N a -> N
prLength :: forall a. Product N a -> N
prLength = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. Number r => ProductForm r a -> N
prfLength

--------------------------------------------------------------------------------
-- prwrd -

-- | restriction of 'prfwrd'.
prwrd :: (Integral r, Oriented a) => Product r a -> Word r a
prwrd :: forall r a. (Integral r, Oriented a) => Product r a -> Word r a
prwrd (Product ProductForm r a
pf) = forall r a. [(a, r)] -> Word r a
Word (forall {b} {a}.
(Distributive b, Total b, Oriented a) =>
ProductForm b a -> [(a, b)]
prfwrd ProductForm r a
pf) where
  -- we use here the property that pf is reduced.
  prfwrd :: ProductForm b a -> [(a, b)]
prfwrd ProductForm b a
pf = case ProductForm b a
pf of
    One Point a
_          -> []
    P a
a            -> [(a
a,forall r. Semiring r => r
rOne)]
    P a
a :^ b
r       -> [(a
a,b
r)]
    P a
a :* ProductForm b a
pf      -> (a
a,forall r. Semiring r => r
rOne)forall a. a -> [a] -> [a]
:ProductForm b a -> [(a, b)]
prfwrd ProductForm b a
pf
    P a
a :^ b
r :* ProductForm b a
pf -> (a
a,b
r)forall a. a -> [a] -> [a]
:ProductForm b a -> [(a, b)]
prfwrd ProductForm b a
pf
    ProductForm b a
pf             -> forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
InvalidData forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ProductForm b a
pf

--------------------------------------------------------------------------------
-- prFactor -

-- | the @n@-th primary factor where all simple factors are expanded according to there
--   exponent. 
prFactor :: Product N a -> N -> a
prFactor :: forall a. Product N a -> N -> a
prFactor = forall (s :: * -> *) i x. Sequence s i x => s x -> i -> x
(?)

--------------------------------------------------------------------------------
-- prd -

-- | evaluates the /product/ according to the given exponential and multiplication.
prd :: (Multiplicative x, Oriented a, p ~ Point a, q ~ Point x, Number r)
   => (x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
prd :: forall x a p q r.
(Multiplicative x, Oriented a, p ~ Point a, q ~ Point x,
 Number r) =>
(x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
prd x -> r -> x
(^) p -> q
q a -> x
x ProductForm r a
pf = case ProductForm r a
pf of
  One Point a
p  -> forall c. Multiplicative c => Point c -> c
one (p -> q
q Point a
p)
  P a
a    -> a -> x
x a
a
  ProductForm r a
a :^ r
r -> forall x a p q r.
(Multiplicative x, Oriented a, p ~ Point a, q ~ Point x,
 Number r) =>
(x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
prd x -> r -> x
(^) p -> q
q a -> x
x ProductForm r a
a x -> r -> x
^ r
r
  ProductForm r a
a :* ProductForm r a
b -> forall x a p q r.
(Multiplicative x, Oriented a, p ~ Point a, q ~ Point x,
 Number r) =>
(x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
prd x -> r -> x
(^) p -> q
q a -> x
x ProductForm r a
a forall c. Multiplicative c => c -> c -> c
* forall x a p q r.
(Multiplicative x, Oriented a, p ~ Point a, q ~ Point x,
 Number r) =>
(x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
prd x -> r -> x
(^) p -> q
q a -> x
x ProductForm r a
b

--------------------------------------------------------------------------------
-- prdMapTotal -

-- | mapping a product.
prdMapTotal :: (Singleton (Point y), Oriented y, Integral r)
  => (x -> y) -> Product r x -> Product r y
prdMapTotal :: forall y r x.
(Singleton (Point y), Oriented y, Integral r) =>
(x -> y) -> Product r x -> Product r y
prdMapTotal x -> y
f (Product ProductForm r x
p) = forall x. Constructable x => Form x -> x
make forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ProductForm r x -> ProductForm r y
f' ProductForm r x
p where
  f' :: ProductForm r x -> ProductForm r y
f' (One Point x
_)  = forall r a. Point a -> ProductForm r a
One forall s. Singleton s => s
unit
  f' (P x
x)    = forall r a. a -> ProductForm r a
P (x -> y
f x
x)
  f' (ProductForm r x
x :^ r
r) = ProductForm r x -> ProductForm r y
f' ProductForm r x
x forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
  f' (ProductForm r x
x :* ProductForm r x
y) = ProductForm r x -> ProductForm r y
f' ProductForm r x
x forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r x -> ProductForm r y
f' ProductForm r x
y
  

--------------------------------------------------------------------------------
-- prfMapTotal -

-- | mapping a product form
prfMapTotal :: Singleton (Point y)
  => (x -> ProductForm r y) -> ProductForm r x -> ProductForm r y
prfMapTotal :: forall y x r.
Singleton (Point y) =>
(x -> ProductForm r y) -> ProductForm r x -> ProductForm r y
prfMapTotal x -> ProductForm r y
f ProductForm r x
pf = case ProductForm r x
pf of
  One Point x
_  -> forall r a. Point a -> ProductForm r a
One forall s. Singleton s => s
unit
  P x
x    -> x -> ProductForm r y
f x
x
  ProductForm r x
x :^ r
r -> forall y x r.
Singleton (Point y) =>
(x -> ProductForm r y) -> ProductForm r x -> ProductForm r y
prfMapTotal x -> ProductForm r y
f ProductForm r x
x forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
  ProductForm r x
x :* ProductForm r x
y -> forall y x r.
Singleton (Point y) =>
(x -> ProductForm r y) -> ProductForm r x -> ProductForm r y
prfMapTotal x -> ProductForm r y
f ProductForm r x
x forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall y x r.
Singleton (Point y) =>
(x -> ProductForm r y) -> ProductForm r x -> ProductForm r y
prfMapTotal x -> ProductForm r y
f ProductForm r x
y

----------------------------------------
-- nProductForm -


nProductFormOrt :: (Hom Ort h, Multiplicative x)
  => Struct Ort a -> h a x -> ProductForm N a -> x
-- nProductFormOrt Struct f = prd npower (pmap f) (f$)
nProductFormOrt :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
Struct Ort a -> h a x -> ProductForm N a -> x
nProductFormOrt Struct Ort a
Struct h a x
h = forall {c} {h :: * -> * -> *} {a}.
(Multiplicative c, HomOriented h) =>
h a c -> ProductForm N a -> c
prd h a x
h where
  prd :: h a c -> ProductForm N a -> c
prd h a c
h ProductForm N a
f = case ProductForm N a
f of
    One Point a
p  -> forall c. Multiplicative c => Point c -> c
one (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a c
h Point a
p)
    P a
a    -> forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a c
h a
a
    ProductForm N a
a :^ N
n -> h a c -> ProductForm N a -> c
prd h a c
h ProductForm N a
a forall c. Multiplicative c => c -> N -> c
`npower` N
n
    ProductForm N a
a :* ProductForm N a
b -> h a c -> ProductForm N a -> c
prd h a c
h ProductForm N a
a forall c. Multiplicative c => c -> c -> c
* h a c -> ProductForm N a -> c
prd h a c
h ProductForm N a
b
    
-- | mapping a product form with exponents in t'N' into a 'Multiplicative' structure
-- applying a homomorphism between 'Oriented' structures.
nProductForm :: (Hom Ort h, Multiplicative x)
  => h a x -> ProductForm N a -> x
nProductForm :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
h a x -> ProductForm N a -> x
nProductForm h a x
f = forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
Struct Ort a -> h a x -> ProductForm N a -> x
nProductFormOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a x
f) h a x
f


nProductOrt :: (Hom Ort h, Multiplicative x)
  => Struct Ort a -> h a x -> Product N a -> x
nProductOrt :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
Struct Ort a -> h a x -> Product N a -> x
nProductOrt Struct Ort a
Struct = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
h a x -> ProductForm N a -> x
nProductForm

--------------------------------------------------------------------------------
-- nProduct -

-- | mapping a product with exponents in t'N' into a 'Multiplicative' structure
--   applying a homomorphism between 'Oriented' structures.
nProduct :: (Hom Ort h, Multiplicative x)
  => h a x -> Product N a -> x
nProduct :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
h a x -> Product N a -> x
nProduct h a x
h = forall (h :: * -> * -> *) x a.
(Hom Ort h, Multiplicative x) =>
Struct Ort a -> h a x -> Product N a -> x
nProductOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a x
h) h a x
h 

--------------------------------------------------------------------------------
-- zProductForm -

zProductFormOrt :: (Hom Ort h , Cayleyan x)
  => Struct Ort a -> h a x -> ProductForm Z a -> x
zProductFormOrt :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
Struct Ort a -> h a x -> ProductForm Z a -> x
zProductFormOrt Struct Ort a
Struct h a x
h = forall {c} {h :: * -> * -> *} {a}.
(HomOriented h, Invertible c) =>
h a c -> ProductForm Z a -> c
prd h a x
h where
  prd :: h a c -> ProductForm Z a -> c
prd h a c
h ProductForm Z a
f = case ProductForm Z a
f of
    One Point a
p  -> forall c. Multiplicative c => Point c -> c
one (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a c
h Point a
p)
    P a
a    -> forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a c
h a
a
    ProductForm Z a
a :^ Z
z -> h a c -> ProductForm Z a -> c
prd h a c
h ProductForm Z a
a forall c. Invertible c => c -> Z -> c
`zpower` Z
z
    ProductForm Z a
a :* ProductForm Z a
b -> h a c -> ProductForm Z a -> c
prd h a c
h ProductForm Z a
a forall c. Multiplicative c => c -> c -> c
* h a c -> ProductForm Z a -> c
prd h a c
h ProductForm Z a
b


-- | mapping a product form with exponents in 'Z' into a 'Cayleyan' structure
-- applying a homomorphism between 'Oriented' structures.
zProductForm :: (Hom Ort h , Cayleyan x)
                 => h a x -> ProductForm Z a -> x
zProductForm :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> ProductForm Z a -> x
zProductForm h a x
f = forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
Struct Ort a -> h a x -> ProductForm Z a -> x
zProductFormOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a x
f) h a x
f

--------------------------------------------------------------------------------
-- zProduct -
zProductOrt :: (Hom Ort h, Cayleyan x)
  => Struct Ort a -> h a x -> Product Z a -> x
zProductOrt :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
Struct Ort a -> h a x -> Product Z a -> x
zProductOrt Struct Ort a
Struct = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> ProductForm Z a -> x
zProductForm

-- | mapping a product with exponents in 'Z' into a 'Cayleyan' structure
--   applying a homomorphism between 'Oriented' structures.
zProduct :: (Hom Ort h, Cayleyan x)
  => h a x -> Product Z a -> x
zProduct :: forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct h a x
h = forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
Struct Ort a -> h a x -> Product Z a -> x
zProductOrt (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a x
h) h a x
h


--------------------------------------------------------------------------------
-- prFromOp -

-- | from 'Op' symbols.
--
-- __Property__ For every 'Oriented' structure @__a__@ and 'Integral' @__r__@ the resulting
-- map 'prFromOp' is a __contravariant__ homomorphisms between 'Multiplicative' structures.
prFromOp :: Product r (Op a) -> Product r a
prFromOp :: forall r a. Product r (Op a) -> Product r a
prFromOp (Product ProductForm r (Op a)
f) = forall r a. ProductForm r a -> Product r a
Product (forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
f)