{-# LANGUAGE RebindableSyntax #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.YAP.PowerSeries.General
-- Copyright   :  (c) Ross Paterson 2021
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  [email protected]
-- Stability   :  provisional
-- Portability :  portable
--
-- An example instance of the algebraic classes: formal power series
-- generalized to arbitrary exponents.
--
-----------------------------------------------------------------------------

module Data.YAP.PowerSeries.General (
    -- * General power series
    PowerSeries,
    -- * Construction
    term,
    constant,
    identity,
    fromTerms,
    fromCoefficients,
    -- * Queries
    order,
    terms,
    -- * Special cases
    LaurentSeries,
    laurentSeries,
    LeviCivitaField,
    ) where

import Prelude.YAP
import Data.YAP.Algebra

-- | A formal series of the form
--
-- \[
-- \sum_{e \in I} a_e x^e
-- \]
--
-- such that the set of indices \(e\) for which \(a_e\) is non-zero is
-- /left-finite/: for any \(i\), the set of indices \(e < i\) for which
-- \(a_e\) is non-zero is finite.
--
-- Addition of indices is required to preserve the ordering.
newtype PowerSeries i a = PS [(i, a)]

instance AdditiveFunctor (PowerSeries i) where
    mapAdditive :: forall a b.
(AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> PowerSeries i a -> PowerSeries i b
mapAdditive a -> b
f (PS [(i, a)]
as) = [(i, b)] -> PowerSeries i b
forall i a. [(i, a)] -> PowerSeries i a
PS (((i, a) -> (i, b)) -> [(i, a)] -> [(i, b)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> (i, a) -> (i, b)
forall a b. (a -> b) -> (i, a) -> (i, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) [(i, a)]
as)

-- | fails for equal series
instance (Eq i, Eq a) => Eq (PowerSeries i a) where
    PS [(i, a)]
xs == :: PowerSeries i a -> PowerSeries i a -> Bool
== PS [(i, a)]
ys = ([(i, a)]
xs [(i, a)] -> [(i, a)] -> [(i, a)]
forall a. [a] -> [a] -> [a]
++ [(i, a)]
forall {a}. a
padding) [(i, a)] -> [(i, a)] -> Bool
forall a. Eq a => a -> a -> Bool
== ([(i, a)]
ys [(i, a)] -> [(i, a)] -> [(i, a)]
forall a. [a] -> [a] -> [a]
++ [(i, a)]
forall {a}. a
padding)
      where
        padding :: a
padding = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"comparison of equal series"

-- | treats the indeterminate as a positive infinitesimal
instance (Ord i, Ord a, AdditiveMonoid a) => Ord (PowerSeries i a) where
    compare :: PowerSeries i a -> PowerSeries i a -> Ordering
compare (PS [(i, a)]
xs) (PS [(i, a)]
ys) = [(i, a)] -> [(i, a)] -> Ordering
forall i a.
(Ord i, Ord a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> Ordering
comp [(i, a)]
xs [(i, a)]
ys

comp :: (Ord i, Ord a, AdditiveMonoid a) => [(i, a)] -> [(i, a)] -> Ordering
comp :: forall i a.
(Ord i, Ord a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> Ordering
comp [] [] = [Char] -> Ordering
forall a. HasCallStack => [Char] -> a
error [Char]
"comparison of equal series"
comp ((i
_, a
vx):[(i, a)]
_) [] = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
vx a
forall a. AdditiveMonoid a => a
zero
comp [] ((i
_, a
vy):[(i, a)]
_) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
forall a. AdditiveMonoid a => a
zero a
vy
comp ((i
ix, a
vx):[(i, a)]
xs) ((i
iy, a
vy):[(i, a)]
ys) = case i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
ix i
iy of
    Ordering
LT -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
vx a
forall a. AdditiveMonoid a => a
zero
    Ordering
EQ -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
vx a
vy Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> [(i, a)] -> [(i, a)] -> Ordering
forall i a.
(Ord i, Ord a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> Ordering
comp [(i, a)]
xs [(i, a)]
ys
    Ordering
GT -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
forall a. AdditiveMonoid a => a
zero a
vy

instance (Show i, Show a, Eq a, AdditiveMonoid a) =>
        Show (PowerSeries i a) where
    showsPrec :: Int -> PowerSeries i a -> ShowS
showsPrec Int
p PowerSeries i a
xs =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Char] -> ShowS
showString [Char]
"fromTerms " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(i, a)] -> ShowS
forall a. Show a => a -> ShowS
shows (PowerSeries i a -> [(i, a)]
forall a i. (Eq a, AdditiveMonoid a) => PowerSeries i a -> [(i, a)]
terms PowerSeries i a
xs)

-- | Construct a power series from a list in ascending order of index
--
-- prop> fromTerms ts = sum [term i a | (i, a) <- ts]
fromTerms :: (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms :: forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS ([(i, a)] -> PowerSeries i a)
-> ([(i, a)] -> [(i, a)]) -> [(i, a)] -> PowerSeries i a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(i, a)] -> [(i, a)]
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)]
dropZeroes

dropZeroes :: (Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)]
dropZeroes :: forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)]
dropZeroes [(i, a)]
xs = [(i
i, a
v) | (i
i, a
v) <- [(i, a)]
xs, a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
forall a. AdditiveMonoid a => a
zero]

-- | @'term' i a@ is a series consisting of the term \(a x^i\).
--
-- prop> term i a * term j b = term (i+j) (a*b)
term :: (Eq a, AdditiveMonoid a) => i -> a -> PowerSeries i a
term :: forall a i. (Eq a, AdditiveMonoid a) => i -> a -> PowerSeries i a
term i
i a
a
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS []
  | Bool
otherwise = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS [(i
i, a
a)]

-- | Identity function, i.e. the indeterminate \(x\)
--
-- prop> identity = term 1 1
identity :: (Semiring i, Semiring a) => PowerSeries i a
identity :: forall i a. (Semiring i, Semiring a) => PowerSeries i a
identity = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS [(i
forall a. Semiring a => a
one, a
forall a. Semiring a => a
one)]

-- | Power series representing a constant value \(c\)
--
-- prop> constant a = term 0 a
constant :: (AdditiveMonoid i, Eq a, AdditiveMonoid a) => a -> PowerSeries i a
constant :: forall i a.
(AdditiveMonoid i, Eq a, AdditiveMonoid a) =>
a -> PowerSeries i a
constant = i -> a -> PowerSeries i a
forall a i. (Eq a, AdditiveMonoid a) => i -> a -> PowerSeries i a
term i
forall a. AdditiveMonoid a => a
zero

-- | Power series formed from a list of coefficients of indices 0, 1, ...
-- If the list is finite, the remaining coefficients are zero.
fromCoefficients :: (Semiring i, Eq a, AdditiveMonoid a) =>
    [a] -> PowerSeries i a
fromCoefficients :: forall i a.
(Semiring i, Eq a, AdditiveMonoid a) =>
[a] -> PowerSeries i a
fromCoefficients = [(i, a)] -> PowerSeries i a
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms ([(i, a)] -> PowerSeries i a)
-> ([a] -> [(i, a)]) -> [a] -> PowerSeries i a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> [a] -> [(i, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((i -> i) -> i -> [i]
forall a. (a -> a) -> a -> [a]
iterate (i -> i -> i
forall a. AdditiveMonoid a => a -> a -> a
+i
forall a. Semiring a => a
one) i
forall a. AdditiveMonoid a => a
zero)

-- | A formal power series with integer indices, of which finitely many
-- are negative.
type LaurentSeries = PowerSeries Integer

-- | A Laurent series with coefficients starting from the given index
laurentSeries :: (Eq a, AdditiveMonoid a) => Integer -> [a] -> LaurentSeries a
laurentSeries :: forall a.
(Eq a, AdditiveMonoid a) =>
Integer -> [a] -> LaurentSeries a
laurentSeries Integer
i0 = [(Integer, a)] -> PowerSeries Integer a
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms ([(Integer, a)] -> PowerSeries Integer a)
-> ([a] -> [(Integer, a)]) -> [a] -> PowerSeries Integer a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> [a] -> [(Integer, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
i0..]

-- | The Levi-Civita field.
type LeviCivitaField = PowerSeries Rational

-- | The smallest exponent with a non-zero coefficient (undefined on 'zero')
order :: (Eq a, AdditiveMonoid a) => PowerSeries i a -> i
order :: forall a i. (Eq a, AdditiveMonoid a) => PowerSeries i a -> i
order (PS [(i, a)]
as) = case [(i, a)] -> [(i, a)]
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)]
dropZeroes [(i, a)]
as of
    [] -> [Char] -> i
forall a. HasCallStack => [Char] -> a
error [Char]
"order of a zero series"
    (i
i, a
_):[(i, a)]
_ -> i
i

-- | Indices with non-zero coefficients, in ascending order
terms :: (Eq a, AdditiveMonoid a) => PowerSeries i a -> [(i, a)]
terms :: forall a i. (Eq a, AdditiveMonoid a) => PowerSeries i a -> [(i, a)]
terms (PS [(i, a)]
as) = [(i, a)] -> [(i, a)]
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)]
dropZeroes [(i, a)]
as [(i, a)] -> [(i, a)] -> [(i, a)]
forall a. [a] -> [a] -> [a]
++ [Char] -> [(i, a)]
forall a. HasCallStack => [Char] -> a
error [Char]
"terms of a zero series"

-- | Pointwise addition
instance (Ord i, Eq a, AdditiveMonoid a) =>
        AdditiveMonoid (PowerSeries i a) where
    PS [(i, a)]
xs + :: PowerSeries i a -> PowerSeries i a -> PowerSeries i a
+ PS [(i, a)]
ys = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS ([(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i, a)]
xs [(i, a)]
ys)
    zero :: PowerSeries i a
zero = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS []
    atimes :: forall b. ToInteger b => b -> PowerSeries i a -> PowerSeries i a
atimes b
n PowerSeries i a
xs
      | b
n b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. AdditiveMonoid a => a
zero = PowerSeries i a
forall a. AdditiveMonoid a => a
zero
      | Bool
otherwise = (a -> a) -> PowerSeries i a -> PowerSeries i a
forall a b.
(AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> PowerSeries i a -> PowerSeries i b
forall (f :: * -> *) a b.
(AdditiveFunctor f, AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> f a -> f b
mapAdditive (b -> a -> a
forall b. ToInteger b => b -> a -> a
forall a b. (AdditiveMonoid a, ToInteger b) => b -> a -> a
atimes b
n) PowerSeries i a
xs

add :: (Ord i, Eq a, AdditiveMonoid a) => [(i, a)] -> [(i, a)] -> [(i, a)]
add :: forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [] [(i, a)]
ys = [(i, a)]
ys
add [(i, a)]
xs [] = [(i, a)]
xs
add xs :: [(i, a)]
xs@((i
ix, a
vx):[(i, a)]
xs') ys :: [(i, a)]
ys@((i
iy, a
vy):[(i, a)]
ys') = case i -> i -> Ordering
forall a. Ord a => a -> a -> Ordering
compare i
ix i
iy of
    Ordering
LT -> (i
ix, a
vx)(i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
:[(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i, a)]
xs' [(i, a)]
ys
    Ordering
EQ
      | a
vxy a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero -> [(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i, a)]
xs' [(i, a)]
ys'
      | Bool
otherwise -> (i
ix, a
vxy)(i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
:[(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i, a)]
xs' [(i, a)]
ys'
      where
        vxy :: a
vxy = a
vx a -> a -> a
forall a. AdditiveMonoid a => a -> a -> a
+ a
vy
    Ordering
GT -> (i
iy, a
vy)(i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
:[(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i, a)]
xs [(i, a)]
ys'

instance (Ord i, Eq a, AbelianGroup a) =>
        AbelianGroup (PowerSeries i a) where
    negate :: PowerSeries i a -> PowerSeries i a
negate = (a -> a) -> PowerSeries i a -> PowerSeries i a
forall a b.
(AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> PowerSeries i a -> PowerSeries i b
forall (f :: * -> *) a b.
(AdditiveFunctor f, AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> f a -> f b
mapAdditive a -> a
forall a. AbelianGroup a => a -> a
negate
    gtimes :: forall b.
(AbelianGroup b, ToInteger b) =>
b -> PowerSeries i a -> PowerSeries i a
gtimes b
n PowerSeries i a
xs
      | b
n b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. AdditiveMonoid a => a
zero = PowerSeries i a
forall a. AdditiveMonoid a => a
zero
      | Bool
otherwise = (a -> a) -> PowerSeries i a -> PowerSeries i a
forall a b.
(AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> PowerSeries i a -> PowerSeries i b
forall (f :: * -> *) a b.
(AdditiveFunctor f, AdditiveMonoid a, AdditiveMonoid b) =>
(a -> b) -> f a -> f b
mapAdditive (b -> a -> a
forall b. (AbelianGroup b, ToInteger b) => b -> a -> a
forall a b.
(AbelianGroup a, AbelianGroup b, ToInteger b) =>
b -> a -> a
gtimes b
n) PowerSeries i a
xs

-- | Discrete convolution
instance (Ord i, AdditiveMonoid i, Eq a, Semiring a) =>
        Semiring (PowerSeries i a) where
    PS [(i, a)]
xs * :: PowerSeries i a -> PowerSeries i a -> PowerSeries i a
* PS [(i, a)]
ys = [(i, a)] -> PowerSeries i a
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms ([(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, AdditiveMonoid i, Eq a, Semiring a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
mul [(i, a)]
xs [(i, a)]
ys)
    one :: PowerSeries i a
one = [(i, a)] -> PowerSeries i a
forall i a. [(i, a)] -> PowerSeries i a
PS [(i
forall a. AdditiveMonoid a => a
zero, a
forall a. Semiring a => a
one)]
    fromNatural :: Natural -> PowerSeries i a
fromNatural Natural
n = a -> PowerSeries i a
forall i a.
(AdditiveMonoid i, Eq a, AdditiveMonoid a) =>
a -> PowerSeries i a
constant (Natural -> a
forall a. Semiring a => Natural -> a
fromNatural Natural
n)

mul :: (Ord i, AdditiveMonoid i, Eq a, Semiring a) => [(i, a)] -> [(i, a)] -> [(i, a)]
mul :: forall i a.
(Ord i, AdditiveMonoid i, Eq a, Semiring a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
mul ((i
ix, a
vx):[(i, a)]
xs') ys :: [(i, a)]
ys@((i
iy, a
vy):[(i, a)]
ys') =
    (i
ix i -> i -> i
forall a. AdditiveMonoid a => a -> a -> a
+ i
iy, a
vxa -> a -> a
forall a. Semiring a => a -> a -> a
*a
vy) (i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
:
        [(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, Eq a, AdditiveMonoid a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
add [(i
ix i -> i -> i
forall a. AdditiveMonoid a => a -> a -> a
+ i
iy', a
vx a -> a -> a
forall a. Semiring a => a -> a -> a
* a
vy') | (i
iy', a
vy') <- [(i, a)]
ys'] ([(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, AdditiveMonoid i, Eq a, Semiring a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
mul [(i, a)]
xs' [(i, a)]
ys)
mul [(i, a)]
_ [(i, a)]
_ = []

instance (Ord i, AdditiveMonoid i, Eq a, Ring a) => Ring (PowerSeries i a) where
    fromInteger :: Integer -> PowerSeries i a
fromInteger Integer
n = a -> PowerSeries i a
forall i a.
(AdditiveMonoid i, Eq a, AdditiveMonoid a) =>
a -> PowerSeries i a
constant (Integer -> a
forall a. Ring a => Integer -> a
fromInteger Integer
n)

instance (Ord i, AdditiveMonoid i, Eq a, FromRational a) =>
        FromRational (PowerSeries i a) where
    fromRational :: Rational -> PowerSeries i a
fromRational Rational
x = a -> PowerSeries i a
forall i a.
(AdditiveMonoid i, Eq a, AdditiveMonoid a) =>
a -> PowerSeries i a
constant (Rational -> a
forall a. FromRational a => Rational -> a
fromRational Rational
x)

instance (Ord i, AbelianGroup i, Eq a, Field a) =>
        DivisionSemiring (PowerSeries i a) where
    recip :: PowerSeries i a -> PowerSeries i a
recip (PS [(i, a)]
xs) = [(i, a)] -> PowerSeries i a
forall a i. (Eq a, AdditiveMonoid a) => [(i, a)] -> PowerSeries i a
fromTerms ([(i, a)] -> [(i, a)]
forall i a.
(Ord i, AbelianGroup i, Eq a, Field a) =>
[(i, a)] -> [(i, a)]
inv [(i, a)]
xs)

inv :: (Ord i, AbelianGroup i, Eq a, Field a) => [(i, a)] -> [(i, a)]
inv :: forall i a.
(Ord i, AbelianGroup i, Eq a, Field a) =>
[(i, a)] -> [(i, a)]
inv [] = [Char] -> [(i, a)]
forall a. HasCallStack => [Char] -> a
error [Char]
"inv of zero"
inv ((i
ix, a
vx):[(i, a)]
xs) = [(i, a)]
ys
  where
    ys :: [(i, a)]
ys = (i -> i
forall a. AbelianGroup a => a -> a
negate i
ix, a -> a
forall a. DivisionSemiring a => a -> a
recip a
vx) (i, a) -> [(i, a)] -> [(i, a)]
forall a. a -> [a] -> [a]
:
        [(i
iz i -> i -> i
forall a. AbelianGroup a => a -> a -> a
- i
ix, a -> a
forall a. AbelianGroup a => a -> a
negate (a
vz a -> a -> a
forall a. Semifield a => a -> a -> a
/ a
vx)) | (i
iz, a
vz) <- [(i, a)] -> [(i, a)] -> [(i, a)]
forall i a.
(Ord i, AdditiveMonoid i, Eq a, Semiring a) =>
[(i, a)] -> [(i, a)] -> [(i, a)]
mul [(i, a)]
xs [(i, a)]
ys]

instance (Ord i, AbelianGroup i, Eq a, Field a) => Semifield (PowerSeries i a)

instance (Ord i, AbelianGroup i, Eq a, Field a) =>
        DivisionRing (PowerSeries i a)

instance (Ord i, AbelianGroup i, Eq a, Field a) => Field (PowerSeries i a)