{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# 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, prfReductionWith

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

  )

  where

import Control.Monad as M

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
:<=>: Orientation (Point a) -> Statement
forall a. Validable a => a -> Statement
valid (ProductForm r a -> Orientation (Point (ProductForm r a))
forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
pf)
                 , String -> Label
Label String
"symbols" Label -> Statement -> Statement
:<=>: ProductForm r a -> 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   -> Point a -> Statement
forall a. Validable a => a -> Statement
valid Point a
e
      P a
a     -> a -> Statement
forall a. Validable a => a -> Statement
valid a
a
      ProductForm a a
pf :^ a
r -> ProductForm a a -> Statement
vld ProductForm a a
pf Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& a -> Statement
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 Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& 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 = Point (Orientation Char) -> ProductForm r (Orientation Char)
forall r a. Point a -> ProductForm r a
One Char
Point (Orientation Char)
c
pf Int
i Char
c = Orientation Char -> ProductForm r (Orientation Char)
forall r a. a -> ProductForm r a
P (Char
cChar -> Char -> Orientation Char
forall p. p -> p -> Orientation p
:>Char
c) ProductForm r (Orientation Char)
-> ProductForm r (Orientation Char)
-> ProductForm r (Orientation Char)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* Int -> Char -> ProductForm r (Orientation Char)
forall r. Int -> Char -> ProductForm r (Orientation Char)
pf (Int
iInt -> Int -> Int
forall a. Abelian a => a -> a -> a
-Int
1) Char
c

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

type instance Point (ProductForm r a) = Point a

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

instance (Oriented a, Number r) => Oriented (ProductForm r a) where
  orientation :: ProductForm r a -> Orientation (Point (ProductForm r a))
orientation ProductForm r a
pf = case ProductForm r a
pf of
    One Point a
p    -> Point (Orientation (Point a)) -> Orientation (Point a)
forall c. Multiplicative c => Point c -> c
one Point a
Point (Orientation (Point a))
p
    P a
a      -> a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a
    ProductForm r a
f :^ r
r   -> ProductForm r a -> Orientation (Point (ProductForm r a))
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)
(^) = Orientation (Point a) -> r -> Orientation (Point a)
forall r.
Number r =>
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   -> ProductForm r a -> Orientation (Point (ProductForm r a))
forall q. Oriented q => q -> Orientation (Point q)
orientation ProductForm r a
f Orientation (Point a)
-> Orientation (Point a) -> Orientation (Point a)
forall c. Multiplicative c => c -> c -> c
* ProductForm r a -> Orientation (Point (ProductForm r a))
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
_)  = m
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) = m
forall a. Monoid a => a
mempty
  foldMap a -> m
f (ProductForm N a
p :^ N
n) = (a -> m) -> ProductForm N a -> m
forall m a. Monoid m => (a -> m) -> ProductForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ProductForm N a
p m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> ProductForm N a -> m
forall m a. Monoid m => (a -> m) -> ProductForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (ProductForm N a
p ProductForm N a -> N -> ProductForm N a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ N -> N
forall a. Enum a => a -> a
pred N
n)
  foldMap a -> m
f (ProductForm N a
p :* ProductForm N a
q) = (a -> m) -> ProductForm N a -> m
forall m a. Monoid m => (a -> m) -> ProductForm N a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ProductForm N a
p m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> ProductForm N a -> m
forall m a. Monoid m => (a -> m) -> ProductForm N a -> m
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) = (ProductForm r a -> ProductForm r a -> ProductForm r a)
-> ProductForm r a -> [ProductForm r a] -> ProductForm 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 ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
(:*) (Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
s) ([ProductForm r a] -> ProductForm r a)
-> [ProductForm r a] -> ProductForm r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (a -> ProductForm r a) -> [a] -> [ProductForm r a]
forall a b. (a -> b) -> [a] -> [b]
map a -> ProductForm r a
forall r a. a -> ProductForm r a
P [a]
fs

instance Embeddable a (ProductForm r a) where
  inj :: a -> ProductForm r a
inj = a -> ProductForm r a
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 = Point a -> [a] -> Path a
forall q. Point q -> [q] -> Path q
Path (ProductForm N a -> Point (ProductForm N a)
forall q. Oriented q => q -> Point q
start ProductForm N a
pf) (ProductForm N a -> [a]
forall a. ProductForm N a -> [a]
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)  = Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
p
  inj (P a
x)    = a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
x
  inj (ProductForm N a
x :^ N
n) = ProductForm N a -> ProductForm r a
forall a b. Embeddable a b => a -> b
inj ProductForm N a
x ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ (N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
n r
forall r. Semiring r => r
rOne)
  inj (ProductForm N a
x :* ProductForm N a
y) = ProductForm N a -> ProductForm r a
forall a b. Embeddable a b => a -> b
inj ProductForm N a
x ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm N 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)  = Point a -> ProductForm N a
forall r a. Point a -> ProductForm r a
One Point a
p
  prj (P a
x)    = a -> ProductForm N a
forall r a. a -> ProductForm r a
P a
x
  prj (ProductForm r a
x :^ r
r) = ProductForm r a -> ProductForm N a
forall a b. Projectible a b => b -> a
prj ProductForm r a
x ProductForm N a -> N -> ProductForm N a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ N
n where n :: N
n = Z -> N
forall a b. Projectible a b => b -> a
prj (r -> Z
forall r. Number r => r -> Z
zFloor r
r)
  prj (ProductForm r a
x :* ProductForm r a
y) = ProductForm r a -> ProductForm N a
forall a b. Projectible a b => b -> a
prj ProductForm r a
x ProductForm N a -> ProductForm N a -> ProductForm N a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a -> ProductForm N 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   -> (t -> x -> x) -> ProductForm N t -> x -> x
forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) (ProductForm N t
a ProductForm N t -> N -> ProductForm N t
forall r a. ProductForm r a -> r -> ProductForm r a
:^ N -> N
forall a. Enum a => a -> a
pred N
n) ((t -> x -> x) -> ProductForm N t -> x -> x
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   -> (t -> x -> x) -> ProductForm N t -> x -> x
forall t x. (t -> x -> x) -> ProductForm N t -> x -> x
prfopl t -> x -> x
(*>) ProductForm N t
a ((t -> x -> x) -> ProductForm N t -> x -> x
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 = (x, N) -> x
forall a b. (a, b) -> a
fst ((x, N) -> x) -> (x, N) -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (t -> (x, N) -> (x, N)) -> ProductForm N t -> (x, N) -> (x, N)
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 N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0
    then x
x' x -> (x, N) -> (x, N)
forall a b. a -> b -> b
`seq` (x
x',N
0) else (x
x',N
iN -> N -> N
forall 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   -> (x -> t -> x) -> x -> ProductForm N t -> x
forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) ((x -> t -> x) -> x -> ProductForm N 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 ProductForm N t -> N -> ProductForm N t
forall r a. ProductForm r a -> r -> ProductForm r a
:^ N -> N
forall a. Enum a => a -> a
pred N
n)
  ProductForm N t
a :* ProductForm N t
b   -> (x -> t -> x) -> x -> ProductForm N t -> x
forall b a. (b -> a -> b) -> b -> ProductForm N a -> b
prfopr x -> t -> x
(<*) ((x -> t -> x) -> x -> ProductForm N 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 = (x, N) -> x
forall a b. (a, b) -> a
fst ((x, N) -> x) -> (x, N) -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, N) -> t -> (x, N)) -> (x, N) -> ProductForm N t -> (x, N)
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 N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0
    then x
x' x -> (x, N) -> (x, N)
forall a b. a -> b -> b
`seq` (x
x',N
0) else (x
x',N
iN -> N -> N
forall 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 -> ProductForm r a -> N
forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
f N -> N -> N
forall c. Multiplicative c => c -> c -> c
* r -> N
forall {r} {y}. (Projectible y Z, Number r) => r -> y
nFloor r
r
  ProductForm r a
f :* ProductForm r a
g -> ProductForm r a -> N
forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
f N -> N -> N
forall a. Additive a => a -> a -> a
+ ProductForm r a -> N
forall r a. Number r => ProductForm r a -> N
prfLength ProductForm r a
g
  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 (ProductForm N a) where
  lengthN :: ProductForm N a -> N
lengthN = ProductForm N a -> N
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
_ -> ProductForm r a -> N
forall r a. ProductForm r a -> N
prfDepth ProductForm r a
f N -> N -> N
forall a. Additive a => a -> a -> a
+ N
1
  ProductForm r a
f :* ProductForm r a
g -> N -> N -> N
forall a. Ord a => a -> a -> a
max (ProductForm r a -> N
forall r a. ProductForm r a -> N
prfDepth ProductForm r a
f) (ProductForm r a -> N
forall r a. ProductForm r a -> N
prfDepth ProductForm r a
g) N -> N -> N
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
[Word r a] -> ShowS
Word r a -> String
(Int -> Word r a -> ShowS)
-> (Word r a -> String) -> ([Word r a] -> ShowS) -> Show (Word r a)
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
$cshowsPrec :: forall r a. (Show a, Show r) => Int -> Word r a -> ShowS
showsPrec :: Int -> Word r a -> ShowS
$cshow :: forall r a. (Show a, Show r) => Word r a -> String
show :: Word r a -> String
$cshowList :: forall r a. (Show a, Show r) => [Word r a] -> ShowS
showList :: [Word r a] -> ShowS
Show,Word r a -> Word r a -> Bool
(Word r a -> Word r a -> Bool)
-> (Word r a -> Word r a -> Bool) -> Eq (Word r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a. (Eq a, Eq r) => 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
/= :: Word r a -> Word r a -> Bool
Eq,Word r a -> Statement
(Word r a -> Statement) -> Validable (Word r a)
forall a. (a -> Statement) -> Validable a
forall r a. (Validable a, Validable r) => Word r a -> Statement
$cvalid :: forall r a. (Validable a, Validable r) => Word r a -> Statement
valid :: Word r a -> Statement
Validable,(forall a b. (a -> b) -> Word r a -> Word r b)
-> (forall a b. a -> Word r b -> Word r a) -> Functor (Word r)
forall a b. a -> Word r b -> Word r a
forall a b. (a -> b) -> Word r a -> Word r b
forall r a b. a -> Word r b -> Word r a
forall r a b. (a -> b) -> Word r a -> Word 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) -> Word r a -> Word r b
fmap :: forall a b. (a -> b) -> Word r a -> Word r b
$c<$ :: forall r a b. a -> Word r b -> Word r a
<$ :: forall a b. a -> Word r b -> Word r a
M.Functor)

instance ApplicativeG (Word r) (->) (->) where amapG :: forall x y. (x -> y) -> Word r x -> Word r y
amapG = (x -> y) -> Word r x -> Word r y
forall x y. (x -> y) -> Word r x -> Word r y
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
M.fmap
  
--------------------------------------------------------------------------------
-- 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 = [(a, r)] -> Word r a
forall r a. [(a, r)] -> Word r a
Word ([(a, r)] -> Word r a)
-> (Word r a -> [(a, r)]) -> Word r a -> Word 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
. ([(a, r)] -> (a, r)) -> [[(a, r)]] -> [(a, r)]
forall a b. (a -> b) -> [a] -> [b]
map [(a, r)] -> (a, r)
forall {b} {a}. (Distributive b, Total b) => [(a, b)] -> (a, b)
aggr ([[(a, r)]] -> [(a, r)])
-> (Word r a -> [[(a, r)]]) -> Word r a -> [(a, r)]
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
. ((a, r) -> (a, r) -> Bool) -> [(a, r)] -> [[(a, r)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (a, r) -> (a, r) -> Bool
forall {a} {b} {b}. Eq a => (a, b) -> (a, b) -> Bool
(<=>) ([(a, r)] -> [[(a, r)]])
-> (Word r a -> [(a, r)]) -> Word r a -> [[(a, r)]]
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
. Word r a -> [(a, r)]
forall r a. Word r a -> [(a, r)]
fromWord where
  (a, b)
a <=> :: (a, b) -> (a, b) -> Bool
<=> (a, b)
b = (a, b) -> a
forall a b. (a, b) -> a
fst (a, b)
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, b) -> a
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,(b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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
$ ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
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 = AlgebraicException -> Word N N
forall a e. Exception e => e -> a
throw (AlgebraicException -> Word N N) -> AlgebraicException -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
Undefined String
"nFactorize 0"
nFactorize N
n = Word N N -> Word N N
forall a r. (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr (Word N N -> Word N N) -> Word N N -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(N, N)] -> Word N N
forall r a. [(a, r)] -> Word r a
Word ([(N, N)] -> Word N N) -> [(N, N)] -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [N] -> N -> [(N, N)]
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 t -> t -> t
forall a. Integral a => a -> a -> a
`mod` t
p t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0
    then (t
p,b
1)(t, b) -> [(t, b)] -> [(t, b)]
forall a. a -> [a] -> [a]
:[t] -> t -> [(t, b)]
fct [t]
prms (t
n t -> t -> t
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    = AlgebraicException -> Word N N
forall a e. Exception e => e -> a
throw (AlgebraicException -> Word N N) -> AlgebraicException -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
Undefined String
"nFactorize 0"
nFactorize' N
pMax N
n = Word N N -> Word N N
forall a r. (Eq a, Semiring r) => Word r a -> Word r a
wrdAggr (Word N N -> Word N N) -> Word N N -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(N, N)] -> Word N N
forall r a. [(a, r)] -> Word r a
Word ([(N, N)] -> Word N N) -> [(N, N)] -> Word N N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [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 N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<  N
p      = []
                   | N
n N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
p N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 = (N
p,N
1)(N, N) -> [(N, N)] -> [(N, N)]
forall a. a -> [a] -> [a]
:[N] -> N -> [(N, N)]
fct [N]
ps (N
n N -> 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    -> Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
p
  P a
a      -> case Maybe r
forall r. Number r => Maybe r
minusOne of
    Just r
e -> a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
e
    Maybe r
_      -> ArithmeticException -> ProductForm r a
forall a e. Exception e => e -> a
throw ArithmeticException
NoMinusOne
  P a
a :^ r
z -> case Maybe r
forall r. Number r => Maybe r
minusOne of
    Just r
e -> a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ (r
er -> r -> r
forall c. Multiplicative c => c -> c -> c
*r
z)
    Maybe r
_      -> ArithmeticException -> ProductForm r a
forall a e. Exception e => e -> a
throw ArithmeticException
NoMinusOne
  ProductForm r a
a :^ r
z   -> ProductForm r a -> ProductForm r a
forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
a ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
z
  ProductForm r a
a :* ProductForm r a
b   -> ProductForm r a -> ProductForm r a
forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
b ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm 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)    = Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
Point (Op a)
p
prfFromOp (P (Op a
a)) = a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a
prfFromOp (ProductForm r (Op a)
fo :^ r
r)  = ProductForm r (Op a) -> ProductForm r a
forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
fo ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
prfFromOp (ProductForm r (Op a)
fo :* ProductForm r (Op a)
fg) = ProductForm r (Op a) -> ProductForm r a
forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
fg ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r (Op 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)  = Point (Op a) -> ProductForm r (Op a)
forall r a. Point a -> ProductForm r a
One Point a
Point (Op a)
p
prfToOp (P a
a)    = Op a -> ProductForm r (Op a)
forall r a. a -> ProductForm r a
P (a -> Op a
forall x. x -> Op x
Op a
a)
prfToOp (ProductForm r a
f :^ r
r) = ProductForm r a -> ProductForm r (Op a)
forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp ProductForm r a
f ProductForm r (Op a) -> r -> ProductForm r (Op a)
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
prfToOp (ProductForm r a
f :* ProductForm r a
g) = ProductForm r a -> ProductForm r (Op a)
forall r a. ProductForm r a -> ProductForm r (Op a)
prfToOp ProductForm r a
g ProductForm r (Op a)
-> ProductForm r (Op a) -> ProductForm r (Op a)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a -> ProductForm r (Op 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 = [(a, r)] -> Word r a
forall r a. [(a, r)] -> Word r a
Word (ProductForm r a -> [(a, r)]
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,r
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 ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ (r
yr -> r -> r
forall c. Multiplicative c => c -> c -> c
*r
z)) 
    ProductForm r a
a :^ r
z      -> [[(a, r)]] -> [(a, r)]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[(a, r)]] -> [(a, r)]) -> [[(a, r)]] -> [(a, r)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> [[(a, r)]] -> [[(a, r)]]
forall a. N -> [a] -> [a]
takeN N
n ([[(a, r)]] -> [[(a, r)]]) -> [[(a, r)]] -> [[(a, r)]]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(a, r)] -> [[(a, r)]]
forall a. a -> [a]
repeat ([(a, r)] -> [[(a, r)]]) -> [(a, r)] -> [[(a, r)]]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm r a -> [(a, r)]
tow (ProductForm r a -> [(a, r)]) -> ProductForm r a -> [(a, r)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ if r
z r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
forall r. Semiring r => r
rZero then ProductForm r a -> ProductForm r a
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 = Z -> N
forall a b. Projectible a b => b -> a
prj (Z -> N) -> Z -> N
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
z
    ProductForm r a
a :* ProductForm r a
b      -> ProductForm r a -> [(a, r)]
tow ProductForm r a
a [(a, r)] -> [(a, r)] -> [(a, r)]
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) = Point a -> [(a, r)] -> ProductForm r a
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 
    []      -> Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
p
    [(a
a,r
r)] -> if r
r r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
forall r. Semiring r => r
rOne then a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a else (a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a ProductForm r a -> r -> ProductForm r 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] ProductForm r a -> ProductForm r a -> ProductForm r a
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) = [(a, r)] -> Action RdcState [(a, r)]
forall {b} {a}.
(Distributive b, Total b, Eq a) =>
[(a, b)] -> Action RdcState [(a, b)]
rdcw [(a, r)]
ws Action RdcState [(a, r)]
-> ([(a, r)] -> Action RdcState (Word r a))
-> Action RdcState (Word r a)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Word r a -> Action RdcState (Word r a)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word r a -> Action RdcState (Word r a))
-> ([(a, r)] -> Word r a) -> [(a, r)] -> Action RdcState (Word 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
. [(a, r)] -> Word r a
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 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall r. Semiring r => r
rZero -> [(a, b)] -> Action RdcState [(a, b)]
forall a. a -> Action RdcState a
reducesTo [(a, b)]
ws Action RdcState [(a, b)]
-> ([(a, b)] -> Action RdcState [(a, b)])
-> Action RdcState [(a, b)]
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b     -> [(a, b)] -> Action RdcState [(a, b)]
forall a. a -> Action RdcState a
reducesTo ((a
a,b
rb -> b -> b
forall a. Additive a => a -> a -> a
+b
s)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
ws) Action RdcState [(a, b)]
-> ([(a, b)] -> Action RdcState [(a, b)])
-> Action RdcState [(a, b)]
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
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 Action RdcState [(a, b)]
-> ([(a, b)] -> Action RdcState [(a, b)])
-> Action RdcState [(a, b)]
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(a, b)] -> Action RdcState [(a, b)]
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, b)] -> Action RdcState [(a, b)])
-> ([(a, b)] -> [(a, b)]) -> [(a, b)] -> Action RdcState [(a, b)]
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
. ((a, b)
ar(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:)
    []                          -> [(a, b)] -> Action RdcState [(a, b)]
forall a. a -> Action RdcState 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
  = Point a -> Word r a -> ProductForm r a
forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf (ProductForm r a -> Point (ProductForm r a)
forall q. Oriented q => q -> Point q
end ProductForm r a
pf)
  (Word r a -> ProductForm r a) -> Word r a -> ProductForm r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Word r a -> Rdc (Word r a)) -> Word r a -> Word r a
forall x. (x -> Rdc x) -> x -> x
reduceWith (Word r a -> Rdc (Word r a)
forall a r. (Eq a, Semiring r) => Word r a -> Rdc (Word r a)
wrdPrfGroup (Word r a -> Rdc (Word r a))
-> (Word r a -> Rdc (Word r a)) -> Word r a -> Rdc (Word r a)
forall x. (x -> Rdc x) -> (x -> Rdc x) -> x -> Rdc x
>>>= Word r a -> Rdc (Word r a)
rel)
  (Word r a -> Word r a) -> Word r a -> Word r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm r a -> Word r a
forall r a. Integral r => ProductForm r a -> Word r a
prfwrd ProductForm r a
pf

--------------------------------------------------------------------------------
-- prfReduce' -

-- | reduces a product form by the given reduction rule and aggregates it.
prfReductionWith :: (Oriented a, Integral r)
  => (Word r a -> Rdc (Word r a)) -> ProductForm r a -> Rdc (ProductForm r a)
prfReductionWith :: forall a r.
(Oriented a, Integral r) =>
(Word r a -> Rdc (Word r a))
-> ProductForm r a -> Rdc (ProductForm r a)
prfReductionWith Word r a -> Rdc (Word r a)
rel ProductForm r a
pf = (Word r a -> Rdc (Word r a)
rel (Word r a -> Rdc (Word r a)) -> Word r a -> Rdc (Word r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm r a -> Word r a
forall r a. Integral r => ProductForm r a -> Word r a
prfwrd ProductForm r a
pf) Rdc (Word r a) -> (Word r a -> Rdc (Word r a)) -> Rdc (Word r a)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Word r a -> Rdc (Word r a)
forall a r. (Eq a, Semiring r) => Word r a -> Rdc (Word r a)
wrdPrfGroup Rdc (Word r a)
-> (Word r a -> Action RdcState (ProductForm r a))
-> Action RdcState (ProductForm r a)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductForm r a -> Action RdcState (ProductForm r a)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductForm r a -> Action RdcState (ProductForm r a))
-> (Word r a -> ProductForm r a)
-> Word r a
-> Action RdcState (ProductForm 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
. Point a -> Word r a -> ProductForm r a
forall r a. Semiring r => Point a -> Word r a -> ProductForm r a
wrdprf (ProductForm r a -> Point (ProductForm r a)
forall q. Oriented q => q -> Point q
end ProductForm r a
pf)

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

-- | list of elementary factors.
prfFactors :: ProductForm N a -> [a]
prfFactors :: forall a. ProductForm N a -> [a]
prfFactors = ProductForm N a -> [a]
forall a. ProductForm N a -> [a]
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 = N -> [(a, N)] -> N -> Maybe a
forall {t} {a}.
(Additive t, Ord t) =>
t -> [(a, t)] -> t -> Maybe a
lookup N
0 (Word N a -> [(a, N)]
forall r a. Word r a -> [(a, r)]
fromWord (Word N a -> [(a, N)]) -> Word N a -> [(a, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm N a -> Word N a
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
_         = Maybe a
forall a. Maybe a
Nothing
  lookup t
l ((a
a,t
e):[(a, t)]
ws) t
i = if t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
l' then a -> Maybe a
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
lt -> t -> t
forall 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 = ProductForm N x -> [x]
forall a. ProductForm N a -> [a]
prfFactors ProductForm N x
pf [x] -> [N] -> [(x, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]
  ?? :: ProductForm N x -> N -> Maybe x
(??) = 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 = (Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
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)
forall a. a -> Action RdcState a
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 = ProductForm r a -> ProductForm r a
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
[Product r a] -> ShowS
Product r a -> String
(Int -> Product r a -> ShowS)
-> (Product r a -> String)
-> ([Product r a] -> ShowS)
-> Show (Product r a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Int -> Product r a -> ShowS
forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
[Product r a] -> ShowS
forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Product r a -> String
$cshowsPrec :: forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Int -> Product r a -> ShowS
showsPrec :: Int -> Product r a -> ShowS
$cshow :: forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Product r a -> String
show :: Product r a -> String
$cshowList :: forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
[Product r a] -> ShowS
showList :: [Product r a] -> ShowS
Show,Product r a -> Product r a -> Bool
(Product r a -> Product r a -> Bool)
-> (Product r a -> Product r a -> Bool) -> Eq (Product r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Product r a -> Product r a -> Bool
$c== :: forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Product r a -> Product r a -> Bool
== :: Product r a -> Product r a -> Bool
$c/= :: forall r a.
(Oriented a, Show r, Eq r, Validable r, Typeable r) =>
Product r a -> Product r a -> Bool
/= :: Product r a -> Product r a -> Bool
Eq,Eq (Product r a)
Eq (Product r a) =>
(Product r a -> Product r a -> Ordering)
-> (Product r a -> Product r a -> Bool)
-> (Product r a -> Product r a -> Bool)
-> (Product r a -> Product r a -> Bool)
-> (Product r a -> Product r a -> Bool)
-> (Product r a -> Product r a -> Product r a)
-> (Product r a -> Product r a -> Product r a)
-> Ord (Product r a)
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, Show r, Validable r,
 Typeable r) =>
Eq (Product r a)
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Bool
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Ordering
forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Product r a
$ccompare :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Ordering
compare :: Product r a -> Product r a -> Ordering
$c< :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable 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, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Bool
>= :: Product r a -> Product r a -> Bool
$cmax :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Product r a
max :: Product r a -> Product r a -> Product r a
$cmin :: forall r a.
(Oriented a, OrdPoint a, Ord a, Ord r, Show r, Validable r,
 Typeable r) =>
Product r a -> Product r a -> Product r a
min :: Product r a -> Product r a -> Product r a
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 [ ProductForm r a -> Statement
forall a. Validable a => a -> Statement
valid ProductForm r a
pf
                           , String -> Label
Label String
"reduced"
                             Label -> Statement -> Statement
:<=>: (ProductForm r a -> ProductForm r a
forall e. Reducible e => e -> e
reduce ProductForm r a
pf ProductForm r a -> ProductForm r a -> Bool
forall a. Eq a => a -> a -> Bool
== ProductForm r a
pf) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"pf"String -> String -> Parameter
:=ProductForm r a -> String
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) = Form (Product r a)
ProductForm r a
p

instance (Oriented a, Integral r) => Constructable (Product r a) where
  make :: Form (Product r a) -> Product r a
make = ProductForm r a -> Product r a
forall r a. ProductForm r a -> Product r a
Product (ProductForm r a -> Product r a)
-> (ProductForm r a -> ProductForm r a)
-> ProductForm r a
-> Product 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
. ProductForm r a -> ProductForm r a
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 = (Form (Product N a) -> [(a, N)]) -> Product N a -> [(a, N)]
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict (p N -> ProductForm N a -> [(a, N)]
forall (p :: * -> *). p N -> ProductForm N a -> [(a, N)]
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
(??) = (Form (Product N a) -> N -> Maybe a) -> Product N a -> N -> Maybe a
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Product N a) -> N -> Maybe a
ProductForm N a -> N -> Maybe a
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
(??)
  
----------------------------------------
-- Product - Canonical -

instance (Oriented a, Integral r) => Projectible (Product r a) (Path a) where
  prj :: Path a -> Product r a
prj (Path Point a
p [a]
as) = Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a -> Product r a) -> ProductForm r a -> Product r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (a -> ProductForm r a -> ProductForm r a)
-> ProductForm r a -> [a] -> ProductForm 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 -> ProductForm r a -> ProductForm r a
forall {a} {r}. a -> ProductForm r a -> ProductForm r a
(*) (Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
p) [a]
as where a
c * :: a -> ProductForm r a -> ProductForm r a
* ProductForm r a
p = a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
c  ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a
p

instance (Oriented a, Total a, Integral r) => Projectible (Product r a) (Word r a) where
  prj :: Word r a -> Product r a
prj (Word [(a, r)]
as) = Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a -> Product r a) -> ProductForm r a -> Product r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((a, r) -> ProductForm r a -> ProductForm r a)
-> ProductForm r a -> [(a, r)] -> ProductForm 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, r) -> ProductForm r a -> ProductForm r a
forall {a} {r}. (a, r) -> ProductForm r a -> ProductForm r a
(*^) (Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One (Point a -> ProductForm r a) -> Point a -> ProductForm r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point a
forall s. Singleton s => s
unit) [(a, r)]
as where (a
a,r
e) *^ :: (a, r) -> ProductForm r a -> ProductForm r a
*^ ProductForm r a
p = a -> ProductForm r a
forall r a. a -> ProductForm r a
P a
a ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
e ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a
p
  
instance (Oriented a, Integral r) => Embeddable a (Product r a) where
  inj :: a -> Product r a
inj a
a = Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a -> Product r a) -> ProductForm r a -> Product r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ a -> ProductForm r a
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 = Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a -> Product r a) -> ProductForm r a -> Product r a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Path a -> ProductForm r a
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 = (Form (Product N a) -> Path a) -> Product N a -> Path a
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Product N a) -> Path a
ProductForm N a -> Path a
forall a b. Projectible a b => b -> a
prj
  
----------------------------------------
-- Product - Structure -

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

type instance Point (Product r a) = Point a

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

instance (Oriented a, Integral r) => Oriented (Product r a) where
  orientation :: Product r a -> Orientation (Point (Product r a))
orientation = (Form (Product r a) -> Orientation (Point a))
-> Product r a -> Orientation (Point a)
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Product r a) -> Orientation (Point a)
ProductForm r a -> Orientation (Point (ProductForm r a))
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                 = Form (Product r a) -> Product r a
forall x. Constructable x => Form x -> x
make (Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
Point (Product r a)
p)
  
  Product ProductForm r a
f * :: Product r a -> Product r a -> Product r a
* Product ProductForm r a
g | ProductForm r a -> Point (ProductForm r a)
forall q. Oriented q => q -> Point q
start ProductForm r a
f Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== ProductForm r a -> Point (ProductForm r a)
forall q. Oriented q => q -> Point q
end ProductForm r a
g = Form (Product r a) -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a
f ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm r a
g)
                        | Bool
otherwise        = ArithmeticException -> Product r a
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 Product r a -> Exponent (Product r a) -> Product r a
forall f. Exponential f => f -> Exponent f -> f
^ r
Exponent (Product r a)
r where r :: r
r = N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
n r
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 = Product r a -> Solver (Product r a)
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (Product r a -> Solver (Product r a))
-> (Product r a -> Product r a)
-> Product r a
-> Solver (Product 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
. Product r a -> Product r a
forall c. Invertible c => c -> c
invert 
  invert :: Product r a -> Product r a
invert (Product ProductForm r a
p) = Form (Product r a) -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a
p ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r -> r
forall a. Abelian a => a -> a
negate r
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
    | Bool -> Bool
forall b. Boolean b => b -> b
not (r -> r
forall r. Number r => r -> r
abs r
Exponent (Product r a)
r r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
forall r. Semiring r => r
rOne Bool -> Bool -> Bool
forall a. Logical a => a -> a -> a
|| Product r a -> Bool
forall q. Oriented q => q -> Bool
isEndo Product r a
p) = ArithmeticException -> Product r a
forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential
    | Bool
otherwise                       = Form (Product r a) -> Product r a
forall x. Constructable x => Form x -> x
make (ProductForm r a
pf ProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
Exponent (Product r a)
r)

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

-- | the list of primary factors.
prFactors :: Product N a -> [a]
prFactors :: forall a. Product N a -> [a]
prFactors = Product N a -> [a]
forall a. Product N a -> [a]
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 = (Form (Product N a) -> N) -> Product N a -> N
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (Product N a) -> N
ProductForm N a -> N
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) = [(a, r)] -> Word r a
forall r a. [(a, r)] -> Word r a
Word (ProductForm r a -> [(a, r)]
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,b
forall r. Semiring r => r
rOne)]
    P a
a :^ b
r       -> [(a
a,b
r)]
    P a
a :* ProductForm b a
pf      -> (a
a,b
forall r. Semiring r => r
rOne)(a, b) -> [(a, b)] -> [(a, b)]
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)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:ProductForm b a -> [(a, b)]
prfwrd ProductForm b a
pf
    ProductForm b a
pf             -> AlgebraicException -> [(a, b)]
forall a e. Exception e => e -> a
throw (AlgebraicException -> [(a, b)]) -> AlgebraicException -> [(a, b)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
InvalidData (String -> AlgebraicException) -> String -> AlgebraicException
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm b a -> String
forall a. Show a => a -> String
show (ProductForm b a -> String) -> ProductForm b a -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 = Product N a -> N -> a
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  -> Point x -> x
forall c. Multiplicative c => Point c -> c
one (p -> q
q p
Point a
p)
  P a
a    -> a -> x
x a
a
  ProductForm r a
a :^ r
r -> (x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
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 -> (x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
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 -> x -> x
forall c. Multiplicative c => c -> c -> c
* (x -> r -> x) -> (p -> q) -> (a -> x) -> ProductForm r a -> x
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) = Form (Product r y) -> Product r y
ProductForm r y -> Product r y
forall x. Constructable x => Form x -> x
make (ProductForm r y -> Product r y) -> ProductForm r y -> Product r y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ProductForm r x -> ProductForm r y
f' ProductForm r x
p where
  f' :: ProductForm r x -> ProductForm r y
f' (One Point x
_)  = Point y -> ProductForm r y
forall r a. Point a -> ProductForm r a
One Point y
forall s. Singleton s => s
unit
  f' (P x
x)    = y -> ProductForm r y
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 ProductForm r y -> r -> ProductForm r y
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 ProductForm r y -> ProductForm r y -> ProductForm r y
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
_  -> Point y -> ProductForm r y
forall r a. Point a -> ProductForm r a
One Point y
forall s. Singleton s => s
unit
  P x
x    -> x -> ProductForm r y
f x
x
  ProductForm r x
x :^ r
r -> (x -> ProductForm r y) -> ProductForm r x -> ProductForm r 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 ProductForm r y -> r -> ProductForm r y
forall r a. ProductForm r a -> r -> ProductForm r a
:^ r
r
  ProductForm r x
x :* ProductForm r x
y -> (x -> ProductForm r y) -> ProductForm r x -> ProductForm r 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 ProductForm r y -> ProductForm r y -> ProductForm r y
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* (x -> ProductForm r y) -> ProductForm r x -> ProductForm r 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
y

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

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


nProductOrt :: (HomOriented h, Multiplicative x)
  => Struct Ort a -> h a x -> Product N a -> x
nProductOrt :: forall (h :: * -> * -> *) x a.
(HomOriented h, Multiplicative x) =>
Struct Ort a -> h a x -> Product N a -> x
nProductOrt Struct Ort a
Struct = (Form (Product N a) -> x) -> Product N a -> x
(ProductForm N a -> x) -> Product N a -> x
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict ((ProductForm N a -> x) -> Product N a -> x)
-> (h a x -> ProductForm N a -> x) -> h a x -> Product N 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 -> ProductForm N a -> x
forall (h :: * -> * -> *) x a.
(HomOriented 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 :: (HomOriented h, Multiplicative x)
  => h a x -> Product N a -> x
nProduct :: forall (h :: * -> * -> *) x a.
(HomOriented h, Multiplicative x) =>
h a x -> Product N a -> x
nProduct h a x
h = Struct Ort a -> h a x -> Product N a -> x
forall (h :: * -> * -> *) x a.
(HomOriented h, Multiplicative x) =>
Struct Ort a -> h a x -> Product N a -> x
nProductOrt (Struct (ObjectClass h) a -> Struct Ort a
forall x. Struct (ObjectClass h) x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) a -> Struct Ort a)
-> Struct (ObjectClass h) a -> Struct Ort a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h a x -> Struct (ObjectClass h) a
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a x
h) h a x
h 

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

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


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

--------------------------------------------------------------------------------
-- zProduct -
zProductOrt :: (HomOriented h, Cayleyan x)
  => Struct Ort a -> h a x -> Product Z a -> x
zProductOrt :: forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
Struct Ort a -> h a x -> Product Z a -> x
zProductOrt Struct Ort a
Struct = (Form (Product Z a) -> x) -> Product Z a -> x
(ProductForm Z a -> x) -> Product Z a -> x
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict ((ProductForm Z a -> x) -> Product Z a -> x)
-> (h a x -> ProductForm Z a -> x) -> h a x -> Product Z 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 -> ProductForm Z a -> x
forall (h :: * -> * -> *) x a.
(HomOriented 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 :: (HomOriented h, Cayleyan x)
  => h a x -> Product Z a -> x
zProduct :: forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct h a x
h = Struct Ort a -> h a x -> Product Z a -> x
forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
Struct Ort a -> h a x -> Product Z a -> x
zProductOrt (Struct (ObjectClass h) a -> Struct Ort a
forall x. Struct (ObjectClass h) x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct (ObjectClass h) a -> Struct Ort a)
-> Struct (ObjectClass h) a -> Struct Ort a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h a x -> Struct (ObjectClass h) a
forall x y. h x y -> Struct (ObjectClass h) x
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) = ProductForm r a -> Product r a
forall r a. ProductForm r a -> Product r a
Product (ProductForm r (Op a) -> ProductForm r a
forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp ProductForm r (Op a)
f)