{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Algebra.Ring.LinearRecurrentSequence where

import Algebra.Field.Finite (FiniteField)
import Algebra.Prelude.Core
import Algebra.Ring.Euclidean.Quotient (Quotient, quotientBy, reifyQuotient, representative)
import Algebra.Ring.Fraction.Decomp
import Algebra.Ring.Polynomial.Factorise (clearDenom, factorHensel, factorise)
import Algebra.Ring.Polynomial.Univariate
import Control.Lens (ifoldMap)
import Control.Monad.Random
import Control.Monad.Trans.Writer.CPS (Writer, runWriter, tell)
import qualified Data.DList as DL
import Data.Functor ((<&>))
import qualified Data.IntMap.Strict as IM
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Monoid (Any (Any))
import Data.Reflection (Reifies (reflect))
import Data.Semigroup (Semigroup)
import qualified Data.Sized as S
import qualified Data.Sized as SV
import qualified Data.Vector as V
import qualified Numeric.Field.Fraction as F
import qualified Numeric.Ring.Class as AC
import Unsafe.Coerce (unsafeCoerce)

data Power = P Natural | Np
  deriving (Power -> Power -> Bool
(Power -> Power -> Bool) -> (Power -> Power -> Bool) -> Eq Power
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Power -> Power -> Bool
$c/= :: Power -> Power -> Bool
== :: Power -> Power -> Bool
$c== :: Power -> Power -> Bool
Eq, Eq Power
Eq Power
-> (Power -> Power -> Ordering)
-> (Power -> Power -> Bool)
-> (Power -> Power -> Bool)
-> (Power -> Power -> Bool)
-> (Power -> Power -> Bool)
-> (Power -> Power -> Power)
-> (Power -> Power -> Power)
-> Ord Power
Power -> Power -> Bool
Power -> Power -> Ordering
Power -> Power -> Power
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
min :: Power -> Power -> Power
$cmin :: Power -> Power -> Power
max :: Power -> Power -> Power
$cmax :: Power -> Power -> Power
>= :: Power -> Power -> Bool
$c>= :: Power -> Power -> Bool
> :: Power -> Power -> Bool
$c> :: Power -> Power -> Bool
<= :: Power -> Power -> Bool
$c<= :: Power -> Power -> Bool
< :: Power -> Power -> Bool
$c< :: Power -> Power -> Bool
compare :: Power -> Power -> Ordering
$ccompare :: Power -> Power -> Ordering
$cp1Ord :: Eq Power
Ord)

instance Show Power where
  showsPrec :: Int -> Power -> ShowS
showsPrec Int
_ (P Natural
n) = Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
n
  showsPrec Int
_ Power
Np = String -> ShowS
showString String
"n"

data GeneralTerm k where
  Const :: k -> GeneralTerm k
  N :: GeneralTerm k
  (:^) :: GeneralTerm k -> Power -> GeneralTerm k
  (:+) :: GeneralTerm k -> GeneralTerm k -> GeneralTerm k
  (:*) :: GeneralTerm k -> GeneralTerm k -> GeneralTerm k
  (:-) :: GeneralTerm k -> GeneralTerm k -> GeneralTerm k
  Lift ::
    Reifies s (Unipol k) =>
    Proxy s ->
    GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))) ->
    GeneralTerm k

deriving via Add (GeneralTerm k) instance Additive k => Semigroup (GeneralTerm k)

deriving via Add (GeneralTerm k) instance Rig k => Monoid (GeneralTerm k)

instance Additive (GeneralTerm k) where
  + :: GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(+) = GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:+)

instance Rig k => Monoidal (GeneralTerm k) where
  zero :: GeneralTerm k
zero = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall m. Monoidal m => m
zero

instance Abelian k => Abelian (GeneralTerm k)

instance Ring k => Group (GeneralTerm k) where
  (-) = GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:-)

instance Ring k => Semiring (GeneralTerm k)

instance Multiplicative (GeneralTerm k) where
  * :: GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(*) = GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*)

instance
  {-# OVERLAPPABLE #-}
  Semiring k =>
  LeftModule k (GeneralTerm k)
  where
  .* :: k -> GeneralTerm k -> GeneralTerm k
(.*) = GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*) (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> (k -> GeneralTerm k) -> k -> GeneralTerm k -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const

instance
  {-# OVERLAPPABLE #-}
  Semiring k =>
  RightModule k (GeneralTerm k)
  where
  *. :: GeneralTerm k -> k -> GeneralTerm k
(*.) = (k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k -> k -> GeneralTerm k
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((k -> GeneralTerm k -> GeneralTerm k)
 -> GeneralTerm k -> k -> GeneralTerm k)
-> (k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k
-> k
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall a b c. (a -> b -> c) -> b -> a -> c
flip GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*) (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> (k -> GeneralTerm k) -> k -> GeneralTerm k -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const

instance
  {-# OVERLAPPABLE #-}
  Semiring k =>
  LeftModule (Scalar k) (GeneralTerm k)
  where
  .* :: Scalar k -> GeneralTerm k -> GeneralTerm k
(.*) = GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*) (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> (Scalar k -> GeneralTerm k)
-> Scalar k
-> GeneralTerm k
-> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k)
-> (Scalar k -> k) -> Scalar k -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scalar k -> k
forall r. Scalar r -> r
runScalar

instance Unital k => Unital (GeneralTerm k) where
  one :: GeneralTerm k
one = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall r. Unital r => r
one

instance
  {-# OVERLAPPABLE #-}
  Semiring k =>
  RightModule (Scalar k) (GeneralTerm k)
  where
  *. :: GeneralTerm k -> Scalar k -> GeneralTerm k
(*.) = (Scalar k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k -> Scalar k -> GeneralTerm k
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Scalar k -> GeneralTerm k -> GeneralTerm k)
 -> GeneralTerm k -> Scalar k -> GeneralTerm k)
-> (Scalar k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k
-> Scalar k
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall a b c. (a -> b -> c) -> b -> a -> c
flip GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*) (GeneralTerm k -> GeneralTerm k -> GeneralTerm k)
-> (Scalar k -> GeneralTerm k)
-> Scalar k
-> GeneralTerm k
-> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k)
-> (Scalar k -> k) -> Scalar k -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scalar k -> k
forall r. Scalar r -> r
runScalar

instance Ring k => LeftModule Integer (GeneralTerm k) where
  Integer
c .* :: Integer -> GeneralTerm k -> GeneralTerm k
.* GeneralTerm k
a = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (Integer -> k
forall r. Ring r => Integer -> r
fromInteger' Integer
c) GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* GeneralTerm k
a

instance Ring k => RightModule Integer (GeneralTerm k) where
  GeneralTerm k
a *. :: GeneralTerm k -> Integer -> GeneralTerm k
*. Integer
c = GeneralTerm k
a GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (Integer -> k
forall r. Ring r => Integer -> r
fromInteger' Integer
c)

instance Rig k => LeftModule Natural (GeneralTerm k) where
  Natural
c .* :: Natural -> GeneralTerm k -> GeneralTerm k
.* GeneralTerm k
a = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (Natural -> k
forall r. Rig r => Natural -> r
fromNatural Natural
c) GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* GeneralTerm k
a

instance Rig k => RightModule Natural (GeneralTerm k) where
  GeneralTerm k
a *. :: GeneralTerm k -> Natural -> GeneralTerm k
*. Natural
c = GeneralTerm k
a GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (Natural -> k
forall r. Rig r => Natural -> r
fromNatural Natural
c)

instance Ring k => Rig (GeneralTerm k) where
  fromNatural :: Natural -> GeneralTerm k
fromNatural = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> (Natural -> k) -> Natural -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> k
forall r. Rig r => Natural -> r
fromNatural

instance Ring k => Ring (GeneralTerm k) where
  fromInteger :: Integer -> GeneralTerm k
fromInteger = k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> (Integer -> k) -> Integer -> GeneralTerm k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> k
forall r. Ring r => Integer -> r
fromInteger'

showsGTWith :: (CoeffRing k, Field k) => (Int -> k -> ShowSCoeff) -> Int -> GeneralTerm k -> ShowS
showsGTWith :: (Int -> k -> ShowSCoeff) -> Int -> GeneralTerm k -> ShowS
showsGTWith = (Int -> k -> ShowSCoeff) -> Int -> GeneralTerm k -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop
  where
    loop ::
      (CoeffRing a, Field a) =>
      (Int -> a -> ShowSCoeff) ->
      Int ->
      GeneralTerm a ->
      ShowS
    loop :: (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
_ (Const a
a) = case Int -> a -> ShowSCoeff
showsElt Int
11 a
a of
      ShowSCoeff
Vanished -> String -> ShowS
showString String
"0"
      ShowSCoeff
i -> ShowSCoeff -> ShowS
showsCoeffAsTerm ShowSCoeff
i
    loop Int -> a -> ShowSCoeff
_ Int
_ GeneralTerm a
N = String -> ShowS
showString String
"n"
    loop Int -> a -> ShowSCoeff
showsElt Int
d (GeneralTerm a
gt' :^ Power
po) =
      Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
11 GeneralTerm a
gt' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ^ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Power -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
8 Power
po
    loop Int -> a -> ShowSCoeff
showsElt Int
d (GeneralTerm a
gt' :+ GeneralTerm a
gt_a) =
      Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
6 GeneralTerm a
gt'
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" + "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
6 GeneralTerm a
gt_a
    loop Int -> a -> ShowSCoeff
showsElt Int
d (GeneralTerm a
gt' :* GeneralTerm a
gt_a) =
      Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
7) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
7 GeneralTerm a
gt'
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" * "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
7 GeneralTerm a
gt_a
    loop Int -> a -> ShowSCoeff
showsElt Int
d (GeneralTerm a
gt' :- GeneralTerm a
gt_a) =
      Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
6 GeneralTerm a
gt'
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" - "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop Int -> a -> ShowSCoeff
showsElt Int
6 GeneralTerm a
gt_a
    loop Int -> a -> ShowSCoeff
showsElt Int
d (Lift (Proxy s
s :: Proxy s) GeneralTerm (WrapDecidableUnits (Quotient s (Unipol a)))
gt') =
      let f :: Unipol a
f = Proxy s -> Unipol a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s
       in (Int -> WrapDecidableUnits (Quotient s (Unipol a)) -> ShowSCoeff)
-> Int
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol a)))
-> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
loop
            ( \Int
d' ->
                ShowS -> ShowSCoeff
Positive
                  (ShowS -> ShowSCoeff)
-> (WrapDecidableUnits (Quotient s (Unipol a)) -> ShowS)
-> WrapDecidableUnits (Quotient s (Unipol a))
-> ShowSCoeff
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> (Int -> Coefficient (Unipol a) -> ShowSCoeff)
-> Sized (Arity (Unipol a)) String
-> Int
-> Unipol a
-> ShowS
forall poly.
IsOrderedPolynomial poly =>
Bool
-> (Int -> Coefficient poly -> ShowSCoeff)
-> Sized (Arity poly) String
-> Int
-> poly
-> ShowS
showsPolynomialWith'
                    Bool
True
                    Int -> a -> ShowSCoeff
Int -> Coefficient (Unipol a) -> ShowSCoeff
showsElt
                    ( String -> Sized Vector 1 String
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton (String -> Sized Vector 1 String)
-> String -> Sized Vector 1 String
forall a b. (a -> b) -> a -> b
$
                        String
"Root(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Bool
-> (Int -> Coefficient (Unipol a) -> ShowSCoeff)
-> Sized (Arity (Unipol a)) String
-> Int
-> Unipol a
-> String
forall poly.
IsOrderedPolynomial poly =>
Bool
-> (Int -> Coefficient poly -> ShowSCoeff)
-> Sized (Arity poly) String
-> Int
-> poly
-> String
showPolynomialWith' Bool
True Int -> a -> ShowSCoeff
Int -> Coefficient (Unipol a) -> ShowSCoeff
showsElt (String -> Sized Vector 1 String
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton String
"x") Int
10 Unipol a
f String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
                    )
                    Int
d'
                  (Unipol a -> ShowS)
-> (WrapDecidableUnits (Quotient s (Unipol a)) -> Unipol a)
-> WrapDecidableUnits (Quotient s (Unipol a))
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quotient s (Unipol a) -> Unipol a
forall k (r :: k) a. Quotient r a -> a
representative
                  (Quotient s (Unipol a) -> Unipol a)
-> (WrapDecidableUnits (Quotient s (Unipol a))
    -> Quotient s (Unipol a))
-> WrapDecidableUnits (Quotient s (Unipol a))
-> Unipol a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapDecidableUnits (Quotient s (Unipol a)) -> Quotient s (Unipol a)
forall k. WrapDecidableUnits k -> k
runWrapDecidableUnits
            )
            Int
d
            GeneralTerm (WrapDecidableUnits (Quotient s (Unipol a)))
gt'

instance (Show k, Field k, CoeffRing k, PrettyCoeff k) => Show (GeneralTerm k) where
  showsPrec :: Int -> GeneralTerm k -> ShowS
showsPrec = (Int -> k -> ShowSCoeff) -> Int -> GeneralTerm k -> ShowS
forall a.
(CoeffRing a, Field a) =>
(Int -> a -> ShowSCoeff) -> Int -> GeneralTerm a -> ShowS
showsGTWith Int -> k -> ShowSCoeff
forall r. PrettyCoeff r => Int -> r -> ShowSCoeff
showsCoeff

infixl 6 :+, :-

infixl 7 :*

infixr 8 :^

data RecurrenceCoeff a = RC {RecurrenceCoeff a -> a
recCoefficient :: a, RecurrenceCoeff a -> a
initialValue :: a}
  deriving (Int -> RecurrenceCoeff a -> ShowS
[RecurrenceCoeff a] -> ShowS
RecurrenceCoeff a -> String
(Int -> RecurrenceCoeff a -> ShowS)
-> (RecurrenceCoeff a -> String)
-> ([RecurrenceCoeff a] -> ShowS)
-> Show (RecurrenceCoeff a)
forall a. Show a => Int -> RecurrenceCoeff a -> ShowS
forall a. Show a => [RecurrenceCoeff a] -> ShowS
forall a. Show a => RecurrenceCoeff a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RecurrenceCoeff a] -> ShowS
$cshowList :: forall a. Show a => [RecurrenceCoeff a] -> ShowS
show :: RecurrenceCoeff a -> String
$cshow :: forall a. Show a => RecurrenceCoeff a -> String
showsPrec :: Int -> RecurrenceCoeff a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RecurrenceCoeff a -> ShowS
Show, RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
(RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> Eq (RecurrenceCoeff a)
forall a. Eq a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c/= :: forall a. Eq a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
== :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c== :: forall a. Eq a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
Eq, Eq (RecurrenceCoeff a)
Eq (RecurrenceCoeff a)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Ordering)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> Bool)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a)
-> (RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a)
-> Ord (RecurrenceCoeff a)
RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
RecurrenceCoeff a -> RecurrenceCoeff a -> Ordering
RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff 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 a. Ord a => Eq (RecurrenceCoeff a)
forall a. Ord a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
forall a.
Ord a =>
RecurrenceCoeff a -> RecurrenceCoeff a -> Ordering
forall a.
Ord a =>
RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a
min :: RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a
$cmin :: forall a.
Ord a =>
RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a
max :: RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a
$cmax :: forall a.
Ord a =>
RecurrenceCoeff a -> RecurrenceCoeff a -> RecurrenceCoeff a
>= :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c>= :: forall a. Ord a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
> :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c> :: forall a. Ord a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
<= :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c<= :: forall a. Ord a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
< :: RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
$c< :: forall a. Ord a => RecurrenceCoeff a -> RecurrenceCoeff a -> Bool
compare :: RecurrenceCoeff a -> RecurrenceCoeff a -> Ordering
$ccompare :: forall a.
Ord a =>
RecurrenceCoeff a -> RecurrenceCoeff a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (RecurrenceCoeff a)
Ord)

data Recurrence a where
  Recurrence ::
    { ()
recCoefficients_ :: Sized n a
    , ()
initialValues_ :: Sized n a
    , Recurrence a -> a
constant :: a
    } ->
    Recurrence a

recurrenceSize :: Recurrence a -> Int
{-# INLINE recurrenceSize #-}
recurrenceSize :: Recurrence a -> Int
recurrenceSize Recurrence {a
Sized n a
constant :: a
initialValues_ :: Sized n a
recCoefficients_ :: Sized n a
constant :: forall a. Recurrence a -> a
initialValues_ :: ()
recCoefficients_ :: ()
..} = Vector a -> Int
forall a. Vector a -> Int
V.length (Vector a -> Int) -> Vector a -> Int
forall a b. (a -> b) -> a -> b
$ Sized n a -> Vector a
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
S.unsized Sized n a
recCoefficients_

recCoefficients :: Recurrence a -> Vector a
recCoefficients :: Recurrence a -> Vector a
recCoefficients Recurrence {a
Sized n a
constant :: a
initialValues_ :: Sized n a
recCoefficients_ :: Sized n a
constant :: forall a. Recurrence a -> a
initialValues_ :: ()
recCoefficients_ :: ()
..} = Sized n a -> Vector a
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
S.unsized Sized n a
recCoefficients_

initialValues :: Recurrence a -> Vector a
initialValues :: Recurrence a -> Vector a
initialValues Recurrence {a
Sized n a
constant :: a
initialValues_ :: Sized n a
recCoefficients_ :: Sized n a
constant :: forall a. Recurrence a -> a
initialValues_ :: ()
recCoefficients_ :: ()
..} = Sized n a -> Vector a
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
S.unsized Sized n a
initialValues_

{- | Generating function for the sequence defined by
the n-ary linear recurrence formula:
\[
  a_{n + k} = c_0 a_n + c_1 a_1 + \cdots + c_{k - 1} a_{n + k - 1}.
\]
Where initial values \(a_0, \ldots, a_{k - 1}\) are given.

Fibonacci \(a0 = 0, a1 = 1, a(n+2) = an + a(n+1)\):

>>> generatingFunction $ Recurrence (1 :< 1 :< Nil) (0 :< (1 :: Rational) :< Nil) 0
-x / x^2 + x - 1

Tribonacci:

>>> generatingFunction $ Recurrence (1 :< 1 :< 1 :< Nil) (0 :< 1 :< (1 :: Rational) :< Nil) 0
-x / x^3 + x^2 + x - 1
-}
generatingFunction ::
  forall k.
  (Field k, CoeffRing k) =>
  Recurrence k ->
  Fraction (Unipol k)
generatingFunction :: Recurrence k -> Fraction (Unipol k)
generatingFunction Recurrence k
recs =
  let den :: Unipol k
den =
        Add (Unipol k) -> Unipol k
forall a. Add a -> a
runAdd
          ((Int -> k -> Add (Unipol k)) -> Vector k -> Add (Unipol k)
forall i (f :: * -> *) m a.
(FoldableWithIndex i f, Monoid m) =>
(i -> a -> m) -> f a -> m
ifoldMap (\Int
i k
ci -> Unipol k -> Add (Unipol k)
forall a. a -> Add a
Add (Unipol k -> Add (Unipol k)) -> Unipol k -> Add (Unipol k)
forall a b. (a -> b) -> a -> b
$ k
ci k -> Unipol k -> Unipol k
forall r m. Module (Scalar r) m => r -> m -> m
.*. IsLabel "x" (Unipol k)
Unipol k
#x Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
k Int -> Int -> Int
forall r. Group r => r -> r -> r
- Int
i)) Vector k
coeffs)
          Unipol k -> Unipol k -> Unipol k
forall r. Group r => r -> r -> r
- Unipol k
1
      ok :: Unipol k
ok = Vector (Unipol k) -> Unipol k
forall a. Num a => Vector a -> a
V.sum (Vector (Unipol k) -> Unipol k) -> Vector (Unipol k) -> Unipol k
forall a b. (a -> b) -> a -> b
$
        Int -> (Int -> Unipol k) -> Vector (Unipol k)
forall a. Int -> (Int -> a) -> Vector a
V.generate (Int
k Int -> Int -> Int
forall r. Group r => r -> r -> r
- Int
1) ((Int -> Unipol k) -> Vector (Unipol k))
-> (Int -> Unipol k) -> Vector (Unipol k)
forall a b. (a -> b) -> a -> b
$ \Int
i ->
          Vector k -> k
forall (f :: * -> *) m. (Foldable f, Monoidal m) => f m -> m
sum ((k -> k -> k) -> Vector k -> Vector k -> Vector k
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith k -> k -> k
forall r. Multiplicative r => r -> r -> r
(*) (Int -> Vector k -> Vector k
forall a. Int -> Vector a -> Vector a
V.drop (Int
i Int -> Int -> Int
forall r. Additive r => r -> r -> r
+ Int
1) Vector k
coeffs) Vector k
inis)
            k -> Unipol k -> Unipol k
forall r m. Module (Scalar r) m => r -> m -> m
.*. IsLabel "x" (Unipol k)
Unipol k
#x Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
k Int -> Int -> Int
forall r. Group r => r -> r -> r
- Int
1 Int -> Int -> Int
forall r. Group r => r -> r -> r
- Int
i)
      num :: Unipol k
num = Unipol k
ok Unipol k -> Unipol k -> Unipol k
forall r. Group r => r -> r -> r
- Add (Unipol k) -> Unipol k
forall a. Add a -> a
runAdd ((Int -> k -> Add (Unipol k)) -> Vector k -> Add (Unipol k)
forall i (f :: * -> *) m a.
(FoldableWithIndex i f, Monoid m) =>
(i -> a -> m) -> f a -> m
ifoldMap (\Int
i k
ci -> Unipol k -> Add (Unipol k)
forall a. a -> Add a
Add (Unipol k -> Add (Unipol k)) -> Unipol k -> Add (Unipol k)
forall a b. (a -> b) -> a -> b
$ k
ci k -> Unipol k -> Unipol k
forall r m. Module (Scalar r) m => r -> m -> m
.*. IsLabel "x" (Unipol k)
Unipol k
#x Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) Vector k
inis)
   in (Unipol k
num Unipol k -> Unipol k -> Fraction (Unipol k)
forall d. GCDDomain d => d -> d -> Fraction d
F.% Unipol k
1 Fraction (Unipol k) -> Fraction (Unipol k) -> Fraction (Unipol k)
forall r. Additive r => r -> r -> r
+ (Recurrence k -> k
forall a. Recurrence a -> a
constant Recurrence k
recs k -> Unipol k -> Unipol k
forall r m. Module (Scalar r) m => r -> m -> m
.*. IsLabel "x" (Unipol k)
Unipol k
#x Unipol k -> Natural -> Unipol k
forall r. Unital r => r -> Natural -> r
^ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k) Unipol k -> Unipol k -> Fraction (Unipol k)
forall d. GCDDomain d => d -> d -> Fraction d
F.% (IsLabel "x" (Unipol k)
Unipol k
#x Unipol k -> Unipol k -> Unipol k
forall r. Group r => r -> r -> r
- Unipol k
1)) Fraction (Unipol k) -> Fraction (Unipol k) -> Fraction (Unipol k)
forall r. Division r => r -> r -> r
/ (Unipol k
den Unipol k -> Unipol k -> Fraction (Unipol k)
forall d. GCDDomain d => d -> d -> Fraction d
F.% Unipol k
1)
  where
    k :: Int
k = Recurrence k -> Int
forall a. Recurrence a -> Int
recurrenceSize Recurrence k
recs
    coeffs :: Vector k
coeffs = Recurrence k -> Vector k
forall a. Recurrence a -> Vector a
recCoefficients Recurrence k
recs
    inis :: Vector k
inis = Recurrence k -> Vector k
forall a. Recurrence a -> Vector a
initialValues Recurrence k
recs

{- | Solves ternary linear recurrent sequence (e.g. Fibonacci).

* Example: Fibonacci sequence

>>> fib <- evalRandIO $ solveTernaryRecurrence (1 :< 1 :< Nil) (0 :< 1 :< Nil) 0
>>> fib
((2 / 5)*Root(x^2 + x - 1) + (1 / 5)) * (Root(x^2 + x - 1) + 1) ^ n + (-(2 / 5)*Root(x^2 + x - 1) - (1 / 5)) * (-Root(x^2 + x - 1)) ^ n

>>> map (evalGeneralTerm fib) [0..12]
[0,1,1,2,3,5,8,13,21,34,55,89,144]
-}
solveTernaryRecurrence ::
  (MonadRandom m) =>
  -- | Recurrence coefficients
  Sized 2 Rational ->
  -- | Initial values
  Sized 2 Rational ->
  -- | Constant term
  Rational ->
  m (GeneralTerm Rational)
solveTernaryRecurrence :: Sized 2 Rational
-> Sized 2 Rational -> Rational -> m (GeneralTerm Rational)
solveTernaryRecurrence Sized 2 Rational
coes Sized 2 Rational
iniVals Rational
c =
  Recurrence Rational -> m (GeneralTerm Rational)
forall (m :: * -> *).
MonadRandom m =>
Recurrence Rational -> m (GeneralTerm Rational)
solveRationalRecurrence (Sized 2 Rational
-> Sized 2 Rational -> Rational -> Recurrence Rational
forall (n :: Nat) a. Sized n a -> Sized n a -> a -> Recurrence a
Recurrence Sized 2 Rational
coes Sized 2 Rational
iniVals Rational
c)

{- |
Solves general (n+1)-ary linear recurrent sequence.

** Example1: Tribonacci sequence defined by:
T_{n+3} = T_n + T_{n+1} + T_{n+2}
T_0 = 0, T_1 = 0, T_2 = 1

>>> trib <- evalRandIO $ solveRationalRecurrence $ Recurrence (1 :< 1 :< 1 :< Nil) (0 :< 0 :< 1 :< Nil) 0
>>> trib
((5 / 22)*Root(x^3 + x^2 + x - 1)^2 + (1 / 22)*Root(x^3 + x^2 + x - 1) + (1 / 11)) * (Root(x^3 + x^2 + x - 1)^2 + Root(x^3 + x^2 + x - 1) + 1) ^ n + (-(5 / 22)*Root(x^3 + x^2 + x - 1) - (2 / 11)*Root(1*x^2 + Root(x^3 + x^2 + x - 1) + 1*x + Root(x^3 + x^2 + x - 1)^2 + Root(x^3 + x^2 + x - 1) + 1) + -(5 / 22)*Root(x^3 + x^2 + x - 1)^2 - (5 / 22)*Root(x^3 + x^2 + x - 1) - (3 / 22)) * (-Root(x^3 + x^2 + x - 1)*Root(1*x^2 + Root(x^3 + x^2 + x - 1) + 1*x + Root(x^3 + x^2 + x - 1)^2 + Root(x^3 + x^2 + x - 1) + 1) + -Root(x^3 + x^2 + x - 1)^2 - Root(x^3 + x^2 + x - 1)) ^ n + ((5 / 22)*Root(x^3 + x^2 + x - 1) + (2 / 11)*Root(1*x^2 + Root(x^3 + x^2 + x - 1) + 1*x + Root(x^3 + x^2 + x - 1)^2 + Root(x^3 + x^2 + x - 1) + 1) + (2 / 11)*Root(x^3 + x^2 + x - 1) + (1 / 22)) * (Root(x^3 + x^2 + x - 1)*Root(1*x^2 + Root(x^3 + x^2 + x - 1) + 1*x + Root(x^3 + x^2 + x - 1)^2 + Root(x^3 + x^2 + x - 1) + 1)) ^ n
>>> map (evalGeneralTerm trib) [0..12]
[0,0,1,1,2,4,7,13,24,44,81,149,274]

** Example2: Tetrabonacci sequence defined by:
T_{n+4} = T_n + T_{n+1} + T_{n+2} + T_{n+3}
T_0 = 0, T_1 = 0, T_2 = 0, T_3 = 1

>>> tet <- evalRandIO $ solveRationalRecurrence $ Recurrence (1 :< 1 :< 1 :< 1 :< Nil) (0 :< 0 :< 0 :< 1 :< Nil) 0
>>> tet
>>> map (evalGeneralTerm tet) [0..12]
[0,0,0,1,1,2,4,8,15,29,56,108,208]
-}
solveRationalRecurrence ::
  (MonadRandom m) =>
  -- | Recurrence coefficients
  Recurrence Rational ->
  m (GeneralTerm Rational)
solveRationalRecurrence :: Recurrence Rational -> m (GeneralTerm Rational)
solveRationalRecurrence = (Unipol Rational
 -> m (Rational, NonEmpty (Unipol Rational, Natural)))
-> Recurrence Rational -> m (GeneralTerm Rational)
forall (m :: * -> *) k.
(Functor m, CoeffRing k, Field k) =>
(Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Recurrence k -> m (GeneralTerm k)
solveRecurrenceWith ((Unipol Rational
  -> m (Rational, NonEmpty (Unipol Rational, Natural)))
 -> Recurrence Rational -> m (GeneralTerm Rational))
-> (Unipol Rational
    -> m (Rational, NonEmpty (Unipol Rational, Natural)))
-> Recurrence Rational
-> m (GeneralTerm Rational)
forall a b. (a -> b) -> a -> b
$ \Unipol Rational
g -> do
  let (Integer
c, Unipol Integer
g') = Unipol Rational -> (Integer, Unipol Integer)
forall a.
(CoeffRing a, Euclidean a) =>
Unipol (Fraction a) -> (a, Unipol a)
clearDenom Unipol Rational
g
  (Integer
lc, IntMap (Set (Unipol Integer))
facs) <- Unipol Integer -> m (Integer, IntMap (Set (Unipol Integer)))
forall (m :: * -> *).
MonadRandom m =>
Unipol Integer -> m (Integer, IntMap (Set (Unipol Integer)))
factorHensel Unipol Integer
g'
  let (Mult Rational
lc', DList (Unipol Rational, Natural)
fs') =
        (Int
 -> Set (Unipol Integer)
 -> (Mult Rational, DList (Unipol Rational, Natural)))
-> IntMap (Set (Unipol Integer))
-> (Mult Rational, DList (Unipol Rational, Natural))
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
          ( \Int
d ->
              (Unipol Integer
 -> (Mult Rational, DList (Unipol Rational, Natural)))
-> Set (Unipol Integer)
-> (Mult Rational, DList (Unipol Rational, Natural))
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
                ( \((Integer -> Rational) -> Unipol Integer -> Unipol Rational
forall b a. DecidableZero b => (a -> b) -> Unipol a -> Unipol b
mapCoeffUnipol (Integer -> Integer -> Rational
forall d. GCDDomain d => d -> d -> Fraction d
F.% Integer
1) -> Unipol Rational
f0) ->
                    let lc0 :: Coefficient (Unipol Rational)
lc0 = Unipol Rational -> Coefficient (Unipol Rational)
forall poly. IsOrderedPolynomial poly => poly -> Coefficient poly
leadingCoeff Unipol Rational
f0
                        f' :: Unipol Rational
f' = Unipol Rational -> Unipol Rational
forall poly.
(Field (Coefficient poly), IsOrderedPolynomial poly) =>
poly -> poly
monoize Unipol Rational
f0
                     in (Rational -> Mult Rational
forall a. a -> Mult a
Mult Rational
Coefficient (Unipol Rational)
lc0, (Unipol Rational, Natural) -> DList (Unipol Rational, Natural)
forall a. a -> DList a
DL.singleton (Unipol Rational
f', Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
d))
                )
          )
          IntMap (Set (Unipol Integer))
facs
  (Rational, NonEmpty (Unipol Rational, Natural))
-> m (Rational, NonEmpty (Unipol Rational, Natural))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Rational
forall r. Num r => Integer -> r
fromInteger Integer
lc Rational -> Rational -> Rational
forall r. Multiplicative r => r -> r -> r
* Rational
lc' Rational -> Rational -> Rational
forall r. Multiplicative r => r -> r -> r
* (Integer
1 Integer -> Integer -> Rational
forall d. GCDDomain d => d -> d -> Fraction d
F.% Integer
c), [(Unipol Rational, Natural)] -> NonEmpty (Unipol Rational, Natural)
forall a. [a] -> NonEmpty a
NE.fromList ([(Unipol Rational, Natural)]
 -> NonEmpty (Unipol Rational, Natural))
-> [(Unipol Rational, Natural)]
-> NonEmpty (Unipol Rational, Natural)
forall a b. (a -> b) -> a -> b
$ DList (Unipol Rational, Natural) -> [(Unipol Rational, Natural)]
forall a. DList a -> [a]
DL.toList DList (Unipol Rational, Natural)
fs')

{- |
Solves linear recurrent sequence over finite fields.

** Example1: Fibonacci sequence over F_{17}.
>>> import Numeric.Field.Prime
>>> :set -XDataKinds
>>> fibF17 <- evalRandIO $ solveFiniteFieldRecurrence $ Recurrence (1 :< 1 :< Nil) (0 :< (1 :: F 17) :< Nil) 0
>>> fibF17
(14*Root(x^2 + x + 16) + 7) * (Root(x^2 + x + 16) + 1) ^ n + (3*Root(x^2 + x + 16) + 10) * (16*Root(x^2 + x + 16)) ^ n

>>> map (evalGeneralTerm  fibF17) [0..20]
[0,1,1,2,3,5,8,13,4,0,4,4,8,12,3,15,1,16,0,16,16]

** Example2: Tetrabonacci over F_{17}
>>> tetF17 <- evalRandIO $ solveFiniteFieldRecurrence $ Recurrence ((1 :: F 17) :< 1 :< 1 :< 1 :< Nil) (0 :< 0 :< 0 :< 1 :< Nil) 0
>>> map (evalGeneralTerm tetF17) [0..20]
[0,0,0,1,1,2,4,8,15,12,5,6,4,10,8,11,16,11,12,16,4]

** Example3: Twekaed tribonacci over GF_{5^3}

T_{n+3} = T_n + T_{n+1} + T_{n+2}
T_0 = 1, T_1 = ξ, T_2 = ξ^2,
where ξ is a primitive element of GF_{5^3}.

>>> triGF53 <- evalRandIO $ solveFiniteFieldRecurrence $ Recurrence (1 :< (1 :: GF 5 3) :< 1 :< Nil) ( 1 :< primitive :< (primitive ^ 2) :< Nil) 0
>>> triGF53
<ξ^2 + ξ + 1> * <3*ξ + 2> ^ n + <ξ^2 + ξ + 1> * <4*ξ^2> ^ n + <3*ξ^2 + 3*ξ + 4> * <ξ^2 + 2*ξ + 4> ^ n

>>> map (evalGeneralTerm  triGF53) [0..20]
[1,<ξ>,<ξ^2>,<ξ^2 + ξ + 1>,<2*ξ^2 + 2*ξ + 1>,<4*ξ^2 + 3*ξ + 2>,<2*ξ^2 + ξ + 4>,<3*ξ^2 + ξ + 2>,<4*ξ^2 + 3>,<4*ξ^2 + 2*ξ + 4>,<ξ^2 + 3*ξ + 4>,<4*ξ^2 + 1>,<4*ξ^2 + 4>,<4*ξ^2 + 3*ξ + 4>,<2*ξ^2 + 3*ξ + 4>,<ξ + 2>,<ξ^2 + 2*ξ>,<3*ξ^2 + ξ + 1>,<4*ξ^2 + 4*ξ + 3>,<3*ξ^2 + 2*ξ + 4>,<2*ξ + 3>]
-}
solveFiniteFieldRecurrence ::
  (MonadRandom m, CoeffRing k, FiniteField k, Random k) =>
  -- | Recurrence coefficients
  Recurrence k ->
  m (GeneralTerm k)
solveFiniteFieldRecurrence :: Recurrence k -> m (GeneralTerm k)
solveFiniteFieldRecurrence = (Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Recurrence k -> m (GeneralTerm k)
forall (m :: * -> *) k.
(Functor m, CoeffRing k, Field k) =>
(Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Recurrence k -> m (GeneralTerm k)
solveRecurrenceWith ((Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
 -> Recurrence k -> m (GeneralTerm k))
-> (Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Recurrence k
-> m (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ \Unipol k
g0 -> do
  let g :: Unipol k
g = Unipol k -> Unipol k
forall poly.
(Field (Coefficient poly), IsOrderedPolynomial poly) =>
poly -> poly
monoize Unipol k
g0
      lc :: Coefficient (Unipol k)
lc = Unipol k -> Coefficient (Unipol k)
forall poly. IsOrderedPolynomial poly => poly -> Coefficient poly
leadingCoeff Unipol k
g
  [(Unipol k, Natural)]
facs <- Unipol k -> m [(Unipol k, Natural)]
forall (m :: * -> *) k.
(MonadRandom m, CoeffRing k, FiniteField k, Random k) =>
Unipol k -> m [(Unipol k, Natural)]
factorise Unipol k
g
  (k, NonEmpty (Unipol k, Natural))
-> m (k, NonEmpty (Unipol k, Natural))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (k
Coefficient (Unipol k)
lc, [(Unipol k, Natural)] -> NonEmpty (Unipol k, Natural)
forall a. [a] -> NonEmpty a
NE.fromList [(Unipol k, Natural)]
facs)

solveRecurrenceWith ::
  (Functor m, CoeffRing k, Field k) =>
  -- | Factorisation function; must return content and monic square-free factorisation over k.
  (Unipol k -> m (k, NonEmpty (Unipol k, Natural))) ->
  -- | Recurrence coefficients
  Recurrence k ->
  m (GeneralTerm k)
solveRecurrenceWith :: (Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Recurrence k -> m (GeneralTerm k)
solveRecurrenceWith Unipol k -> m (k, NonEmpty (Unipol k, Natural))
factor Recurrence k
recurr =
  let f :: Fraction (Unipol k)
f = Recurrence k -> Fraction (Unipol k)
forall k.
(Field k, CoeffRing k) =>
Recurrence k -> Fraction (Unipol k)
generatingFunction Recurrence k
recurr
   in (Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Fraction (Unipol k) -> m (PartialFractionDecomp k)
forall k (m :: * -> *).
(Field k, CoeffRing k, Functor m) =>
(Unipol k -> m (k, NonEmpty (Unipol k, Natural)))
-> Fraction (Unipol k) -> m (PartialFractionDecomp k)
partialFractionDecomposition Unipol k -> m (k, NonEmpty (Unipol k, Natural))
factor Fraction (Unipol k)
f m (PartialFractionDecomp k)
-> (PartialFractionDecomp k -> GeneralTerm k) -> m (GeneralTerm k)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \PartialFraction {NonEmpty (Unipol k, IntMap (Unipol k))
Unipol k
partialFracs :: forall k.
PartialFractionDecomp k -> NonEmpty (Unipol k, IntMap (Unipol k))
residualPoly :: forall k. PartialFractionDecomp k -> Unipol k
partialFracs :: NonEmpty (Unipol k, IntMap (Unipol k))
residualPoly :: Unipol k
..} ->
        GeneralTerm k -> GeneralTerm k
forall k. (Field k, CoeffRing k) => GeneralTerm k -> GeneralTerm k
reduceGeneralTerm (GeneralTerm k -> GeneralTerm k) -> GeneralTerm k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          ((Unipol k, IntMap (Unipol k)) -> GeneralTerm k)
-> NonEmpty (Unipol k, IntMap (Unipol k)) -> GeneralTerm k
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
            ( \(Unipol k
h, IntMap (Unipol k)
powDens) ->
                if Unipol k -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' Unipol k
h Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
                  then
                    (Int -> Unipol k -> GeneralTerm k)
-> IntMap (Unipol k) -> GeneralTerm k
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
                      ( \Int
n Unipol k
q ->
                          k -> Natural -> k -> GeneralTerm k
forall k.
(CoeffRing k, Field k) =>
k -> Natural -> k -> GeneralTerm k
linearInverse (k -> k
forall r. Group r => r -> r
negate (k -> k) -> k -> k
forall a b. (a -> b) -> a -> b
$ Unipol k -> Coefficient (Unipol k)
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol k
h) (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) (Unipol k -> Coefficient (Unipol k)
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol k
q)
                      )
                      IntMap (Unipol k)
powDens
                  else --

                    (Int -> Unipol k -> GeneralTerm k)
-> IntMap (Unipol k) -> GeneralTerm k
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
                      ( \Int
mul Unipol k
q ->
                          Natural -> Fraction (Unipol k) -> GeneralTerm k
forall k.
(CoeffRing k, Field k) =>
Natural -> Fraction (Unipol k) -> GeneralTerm k
unliftQuadInverse (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
mul) (Unipol k
q Unipol k -> Unipol k -> Fraction (Unipol k)
forall d. GCDDomain d => d -> d -> Fraction d
F.% Unipol k
h)
                      )
                      IntMap (Unipol k)
powDens
            )
            NonEmpty (Unipol k, IntMap (Unipol k))
partialFracs

-- | Unsafe wrapper to treat 'DecidableUnits' as if it is a field.
newtype WrapDecidableUnits k = WrapDecidableUnits {WrapDecidableUnits k -> k
runWrapDecidableUnits :: k}
  deriving newtype
    ( WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
(WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> Eq (WrapDecidableUnits k)
forall k.
Eq k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c/= :: forall k.
Eq k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
== :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c== :: forall k.
Eq k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
Eq
    , Eq (WrapDecidableUnits k)
Eq (WrapDecidableUnits k)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Ordering)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> (WrapDecidableUnits k
    -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (WrapDecidableUnits k
    -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> Ord (WrapDecidableUnits k)
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
WrapDecidableUnits k -> WrapDecidableUnits k -> Ordering
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
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 k. Ord k => Eq (WrapDecidableUnits k)
forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Ordering
forall k.
Ord k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
min :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$cmin :: forall k.
Ord k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
max :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$cmax :: forall k.
Ord k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
>= :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c>= :: forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
> :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c> :: forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
<= :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c<= :: forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
< :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$c< :: forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
compare :: WrapDecidableUnits k -> WrapDecidableUnits k -> Ordering
$ccompare :: forall k.
Ord k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Ordering
$cp1Ord :: forall k. Ord k => Eq (WrapDecidableUnits k)
Ord
    , Int -> WrapDecidableUnits k -> ShowS
[WrapDecidableUnits k] -> ShowS
WrapDecidableUnits k -> String
(Int -> WrapDecidableUnits k -> ShowS)
-> (WrapDecidableUnits k -> String)
-> ([WrapDecidableUnits k] -> ShowS)
-> Show (WrapDecidableUnits k)
forall k. Show k => Int -> WrapDecidableUnits k -> ShowS
forall k. Show k => [WrapDecidableUnits k] -> ShowS
forall k. Show k => WrapDecidableUnits k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WrapDecidableUnits k] -> ShowS
$cshowList :: forall k. Show k => [WrapDecidableUnits k] -> ShowS
show :: WrapDecidableUnits k -> String
$cshow :: forall k. Show k => WrapDecidableUnits k -> String
showsPrec :: Int -> WrapDecidableUnits k -> ShowS
$cshowsPrec :: forall k. Show k => Int -> WrapDecidableUnits k -> ShowS
Show
    , Int -> WrapDecidableUnits k -> Int
WrapDecidableUnits k -> Int
(Int -> WrapDecidableUnits k -> Int)
-> (WrapDecidableUnits k -> Int) -> Hashable (WrapDecidableUnits k)
forall k. Hashable k => Int -> WrapDecidableUnits k -> Int
forall k. Hashable k => WrapDecidableUnits k -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: WrapDecidableUnits k -> Int
$chash :: forall k. Hashable k => WrapDecidableUnits k -> Int
hashWithSalt :: Int -> WrapDecidableUnits k -> Int
$chashWithSalt :: forall k. Hashable k => Int -> WrapDecidableUnits k -> Int
Hashable
    , Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
(WrapDecidableUnits k
 -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (Natural -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (forall (f :: * -> *) a.
    Foldable1 f =>
    (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k)
-> Additive (WrapDecidableUnits k)
forall k.
Additive k =>
Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
forall k.
Additive k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
forall k (f :: * -> *) a.
(Additive k, Foldable1 f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall r.
(r -> r -> r)
-> (Natural -> r -> r)
-> (forall (f :: * -> *) a. Foldable1 f => (a -> r) -> f a -> r)
-> Additive r
forall (f :: * -> *) a.
Foldable1 f =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
sumWith1 :: (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
$csumWith1 :: forall k (f :: * -> *) a.
(Additive k, Foldable1 f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
sinnum1p :: Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
$csinnum1p :: forall k.
Additive k =>
Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
+ :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$c+ :: forall k.
Additive k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
Additive
    , RightModule Natural (WrapDecidableUnits k)
LeftModule Natural (WrapDecidableUnits k)
WrapDecidableUnits k
Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
LeftModule Natural (WrapDecidableUnits k)
-> RightModule Natural (WrapDecidableUnits k)
-> WrapDecidableUnits k
-> (Natural -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (forall (f :: * -> *) a.
    Foldable f =>
    (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k)
-> Monoidal (WrapDecidableUnits k)
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall k. Monoidal k => RightModule Natural (WrapDecidableUnits k)
forall k. Monoidal k => LeftModule Natural (WrapDecidableUnits k)
forall k. Monoidal k => WrapDecidableUnits k
forall k.
Monoidal k =>
Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
forall k (f :: * -> *) a.
(Monoidal k, Foldable f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall m.
LeftModule Natural m
-> RightModule Natural m
-> m
-> (Natural -> m -> m)
-> (forall (f :: * -> *) a. Foldable f => (a -> m) -> f a -> m)
-> Monoidal m
forall (f :: * -> *) a.
Foldable f =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
sumWith :: (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
$csumWith :: forall k (f :: * -> *) a.
(Monoidal k, Foldable f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
sinnum :: Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
$csinnum :: forall k.
Monoidal k =>
Natural -> WrapDecidableUnits k -> WrapDecidableUnits k
zero :: WrapDecidableUnits k
$czero :: forall k. Monoidal k => WrapDecidableUnits k
$cp2Monoidal :: forall k. Monoidal k => RightModule Natural (WrapDecidableUnits k)
$cp1Monoidal :: forall k. Monoidal k => LeftModule Natural (WrapDecidableUnits k)
Monoidal
    , RightModule Integer (WrapDecidableUnits k)
Monoidal (WrapDecidableUnits k)
LeftModule Integer (WrapDecidableUnits k)
n -> WrapDecidableUnits k -> WrapDecidableUnits k
LeftModule Integer (WrapDecidableUnits k)
-> RightModule Integer (WrapDecidableUnits k)
-> Monoidal (WrapDecidableUnits k)
-> (WrapDecidableUnits k
    -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (WrapDecidableUnits k -> WrapDecidableUnits k)
-> (WrapDecidableUnits k
    -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (forall n.
    Integral n =>
    n -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> Group (WrapDecidableUnits k)
WrapDecidableUnits k -> WrapDecidableUnits k
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
forall n.
Integral n =>
n -> WrapDecidableUnits k -> WrapDecidableUnits k
forall r.
LeftModule Integer r
-> RightModule Integer r
-> Monoidal r
-> (r -> r -> r)
-> (r -> r)
-> (r -> r -> r)
-> (forall n. Integral n => n -> r -> r)
-> Group r
forall k. Group k => RightModule Integer (WrapDecidableUnits k)
forall k. Group k => Monoidal (WrapDecidableUnits k)
forall k. Group k => LeftModule Integer (WrapDecidableUnits k)
forall k. Group k => WrapDecidableUnits k -> WrapDecidableUnits k
forall k.
Group k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
forall k n.
(Group k, Integral n) =>
n -> WrapDecidableUnits k -> WrapDecidableUnits k
times :: n -> WrapDecidableUnits k -> WrapDecidableUnits k
$ctimes :: forall k n.
(Group k, Integral n) =>
n -> WrapDecidableUnits k -> WrapDecidableUnits k
subtract :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$csubtract :: forall k.
Group k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
negate :: WrapDecidableUnits k -> WrapDecidableUnits k
$cnegate :: forall k. Group k => WrapDecidableUnits k -> WrapDecidableUnits k
- :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$c- :: forall k.
Group k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$cp3Group :: forall k. Group k => Monoidal (WrapDecidableUnits k)
$cp2Group :: forall k. Group k => RightModule Integer (WrapDecidableUnits k)
$cp1Group :: forall k. Group k => LeftModule Integer (WrapDecidableUnits k)
Group
    , WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
(WrapDecidableUnits k
 -> WrapDecidableUnits k -> WrapDecidableUnits k)
-> (WrapDecidableUnits k -> Natural -> WrapDecidableUnits k)
-> (forall (f :: * -> *) a.
    Foldable1 f =>
    (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k)
-> Multiplicative (WrapDecidableUnits k)
forall k.
Multiplicative k =>
WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
forall k.
Multiplicative k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
forall k (f :: * -> *) a.
(Multiplicative k, Foldable1 f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall r.
(r -> r -> r)
-> (r -> Natural -> r)
-> (forall (f :: * -> *) a. Foldable1 f => (a -> r) -> f a -> r)
-> Multiplicative r
forall (f :: * -> *) a.
Foldable1 f =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
productWith1 :: (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
$cproductWith1 :: forall k (f :: * -> *) a.
(Multiplicative k, Foldable1 f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
pow1p :: WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
$cpow1p :: forall k.
Multiplicative k =>
WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
* :: WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
$c* :: forall k.
Multiplicative k =>
WrapDecidableUnits k
-> WrapDecidableUnits k -> WrapDecidableUnits k
Multiplicative
    , Additive (WrapDecidableUnits k)
Additive (WrapDecidableUnits k) -> Abelian (WrapDecidableUnits k)
forall k. Additive k => Additive (WrapDecidableUnits k)
forall r. Additive r -> Abelian r
Abelian
    , Multiplicative (WrapDecidableUnits k)
Additive (WrapDecidableUnits k)
Abelian (WrapDecidableUnits k)
Additive (WrapDecidableUnits k)
-> Abelian (WrapDecidableUnits k)
-> Multiplicative (WrapDecidableUnits k)
-> Semiring (WrapDecidableUnits k)
forall k.
(Additive k, Multiplicative k) =>
Multiplicative (WrapDecidableUnits k)
forall k.
(Additive k, Multiplicative k) =>
Additive (WrapDecidableUnits k)
forall k.
(Additive k, Multiplicative k) =>
Abelian (WrapDecidableUnits k)
forall r. Additive r -> Abelian r -> Multiplicative r -> Semiring r
$cp3Semiring :: forall k.
(Additive k, Multiplicative k) =>
Multiplicative (WrapDecidableUnits k)
$cp2Semiring :: forall k.
(Additive k, Multiplicative k) =>
Abelian (WrapDecidableUnits k)
$cp1Semiring :: forall k.
(Additive k, Multiplicative k) =>
Additive (WrapDecidableUnits k)
Semiring
    , Multiplicative (WrapDecidableUnits k)
WrapDecidableUnits k
Multiplicative (WrapDecidableUnits k)
-> WrapDecidableUnits k
-> (WrapDecidableUnits k -> Natural -> WrapDecidableUnits k)
-> (forall (f :: * -> *) a.
    Foldable f =>
    (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k)
-> Unital (WrapDecidableUnits k)
WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall k. Unital k => Multiplicative (WrapDecidableUnits k)
forall k. Unital k => WrapDecidableUnits k
forall k.
Unital k =>
WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
forall k (f :: * -> *) a.
(Unital k, Foldable f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
forall r.
Multiplicative r
-> r
-> (r -> Natural -> r)
-> (forall (f :: * -> *) a. Foldable f => (a -> r) -> f a -> r)
-> Unital r
forall (f :: * -> *) a.
Foldable f =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
productWith :: (a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
$cproductWith :: forall k (f :: * -> *) a.
(Unital k, Foldable f) =>
(a -> WrapDecidableUnits k) -> f a -> WrapDecidableUnits k
pow :: WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
$cpow :: forall k.
Unital k =>
WrapDecidableUnits k -> Natural -> WrapDecidableUnits k
one :: WrapDecidableUnits k
$cone :: forall k. Unital k => WrapDecidableUnits k
$cp1Unital :: forall k. Unital k => Multiplicative (WrapDecidableUnits k)
Unital
    , Unital (WrapDecidableUnits k)
Semiring (WrapDecidableUnits k)
Monoidal (WrapDecidableUnits k)
Natural -> WrapDecidableUnits k
Semiring (WrapDecidableUnits k)
-> Unital (WrapDecidableUnits k)
-> Monoidal (WrapDecidableUnits k)
-> (Natural -> WrapDecidableUnits k)
-> Rig (WrapDecidableUnits k)
forall k. Rig k => Unital (WrapDecidableUnits k)
forall k. Rig k => Semiring (WrapDecidableUnits k)
forall k. Rig k => Monoidal (WrapDecidableUnits k)
forall k. Rig k => Natural -> WrapDecidableUnits k
forall r.
Semiring r -> Unital r -> Monoidal r -> (Natural -> r) -> Rig r
fromNatural :: Natural -> WrapDecidableUnits k
$cfromNatural :: forall k. Rig k => Natural -> WrapDecidableUnits k
$cp3Rig :: forall k. Rig k => Monoidal (WrapDecidableUnits k)
$cp2Rig :: forall k. Rig k => Unital (WrapDecidableUnits k)
$cp1Rig :: forall k. Rig k => Semiring (WrapDecidableUnits k)
Rig
    , Rng (WrapDecidableUnits k)
Rig (WrapDecidableUnits k)
Integer -> WrapDecidableUnits k
Rig (WrapDecidableUnits k)
-> Rng (WrapDecidableUnits k)
-> (Integer -> WrapDecidableUnits k)
-> Ring (WrapDecidableUnits k)
forall k. Ring k => Rng (WrapDecidableUnits k)
forall k. Ring k => Rig (WrapDecidableUnits k)
forall k. Ring k => Integer -> WrapDecidableUnits k
forall r. Rig r -> Rng r -> (Integer -> r) -> Ring r
fromInteger :: Integer -> WrapDecidableUnits k
$cfromInteger :: forall k. Ring k => Integer -> WrapDecidableUnits k
$cp2Ring :: forall k. Ring k => Rng (WrapDecidableUnits k)
$cp1Ring :: forall k. Ring k => Rig (WrapDecidableUnits k)
Ring
    , Monoidal (WrapDecidableUnits k)
Monoidal (WrapDecidableUnits k)
-> (WrapDecidableUnits k -> Bool)
-> DecidableZero (WrapDecidableUnits k)
WrapDecidableUnits k -> Bool
forall k. DecidableZero k => Monoidal (WrapDecidableUnits k)
forall k. DecidableZero k => WrapDecidableUnits k -> Bool
forall r. Monoidal r -> (r -> Bool) -> DecidableZero r
isZero :: WrapDecidableUnits k -> Bool
$cisZero :: forall k. DecidableZero k => WrapDecidableUnits k -> Bool
$cp1DecidableZero :: forall k. DecidableZero k => Monoidal (WrapDecidableUnits k)
DecidableZero
    , Unital (WrapDecidableUnits k)
Unital (WrapDecidableUnits k)
-> (WrapDecidableUnits k -> WrapDecidableUnits k -> Bool)
-> DecidableAssociates (WrapDecidableUnits k)
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
forall k. DecidableAssociates k => Unital (WrapDecidableUnits k)
forall k.
DecidableAssociates k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
forall r. Unital r -> (r -> r -> Bool) -> DecidableAssociates r
isAssociate :: WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$cisAssociate :: forall k.
DecidableAssociates k =>
WrapDecidableUnits k -> WrapDecidableUnits k -> Bool
$cp1DecidableAssociates :: forall k. DecidableAssociates k => Unital (WrapDecidableUnits k)
DecidableAssociates
    , Unital (WrapDecidableUnits k)
Unital (WrapDecidableUnits k)
-> (WrapDecidableUnits k -> Maybe (WrapDecidableUnits k))
-> (WrapDecidableUnits k -> Bool)
-> (forall n.
    Integral n =>
    WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k))
-> DecidableUnits (WrapDecidableUnits k)
WrapDecidableUnits k -> Bool
WrapDecidableUnits k -> Maybe (WrapDecidableUnits k)
WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k)
forall n.
Integral n =>
WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k)
forall k. DecidableUnits k => Unital (WrapDecidableUnits k)
forall k. DecidableUnits k => WrapDecidableUnits k -> Bool
forall k.
DecidableUnits k =>
WrapDecidableUnits k -> Maybe (WrapDecidableUnits k)
forall k n.
(DecidableUnits k, Integral n) =>
WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k)
forall r.
Unital r
-> (r -> Maybe r)
-> (r -> Bool)
-> (forall n. Integral n => r -> n -> Maybe r)
-> DecidableUnits r
^? :: WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k)
$c^? :: forall k n.
(DecidableUnits k, Integral n) =>
WrapDecidableUnits k -> n -> Maybe (WrapDecidableUnits k)
isUnit :: WrapDecidableUnits k -> Bool
$cisUnit :: forall k. DecidableUnits k => WrapDecidableUnits k -> Bool
recipUnit :: WrapDecidableUnits k -> Maybe (WrapDecidableUnits k)
$crecipUnit :: forall k.
DecidableUnits k =>
WrapDecidableUnits k -> Maybe (WrapDecidableUnits k)
$cp1DecidableUnits :: forall k. DecidableUnits k => Unital (WrapDecidableUnits k)
DecidableUnits
    , Multiplicative (WrapDecidableUnits k)
Multiplicative (WrapDecidableUnits k)
-> Commutative (WrapDecidableUnits k)
forall r. Multiplicative r -> Commutative r
forall k. Multiplicative k => Multiplicative (WrapDecidableUnits k)
Commutative
    , Semiring (WrapDecidableUnits k)
Monoidal (WrapDecidableUnits k)
Monoidal (WrapDecidableUnits k)
-> Semiring (WrapDecidableUnits k)
-> ZeroProductSemiring (WrapDecidableUnits k)
forall r. Monoidal r -> Semiring r -> ZeroProductSemiring r
forall k.
(Monoidal k, Multiplicative k) =>
Semiring (WrapDecidableUnits k)
forall k.
(Monoidal k, Multiplicative k) =>
Monoidal (WrapDecidableUnits k)
$cp2ZeroProductSemiring :: forall k.
(Monoidal k, Multiplicative k) =>
Semiring (WrapDecidableUnits k)
$cp1ZeroProductSemiring :: forall k.
(Monoidal k, Multiplicative k) =>
Monoidal (WrapDecidableUnits k)
ZeroProductSemiring
    , Show (WrapDecidableUnits k)
Show (WrapDecidableUnits k)
-> (Int -> WrapDecidableUnits k -> ShowSCoeff)
-> PrettyCoeff (WrapDecidableUnits k)
Int -> WrapDecidableUnits k -> ShowSCoeff
forall r. Show r -> (Int -> r -> ShowSCoeff) -> PrettyCoeff r
forall k. PrettyCoeff k => Show (WrapDecidableUnits k)
forall k.
PrettyCoeff k =>
Int -> WrapDecidableUnits k -> ShowSCoeff
showsCoeff :: Int -> WrapDecidableUnits k -> ShowSCoeff
$cshowsCoeff :: forall k.
PrettyCoeff k =>
Int -> WrapDecidableUnits k -> ShowSCoeff
$cp1PrettyCoeff :: forall k. PrettyCoeff k => Show (WrapDecidableUnits k)
PrettyCoeff
    )

instance DecidableUnits k => Division (WrapDecidableUnits k) where
  recip :: WrapDecidableUnits k -> WrapDecidableUnits k
recip = WrapDecidableUnits k
-> Maybe (WrapDecidableUnits k) -> WrapDecidableUnits k
forall a. a -> Maybe a -> a
fromMaybe (String -> WrapDecidableUnits k
forall a. HasCallStack => String -> a
error String
"WrapDecidableUnits: Inverting non-units!") (Maybe (WrapDecidableUnits k) -> WrapDecidableUnits k)
-> (WrapDecidableUnits k -> Maybe (WrapDecidableUnits k))
-> WrapDecidableUnits k
-> WrapDecidableUnits k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapDecidableUnits k -> Maybe (WrapDecidableUnits k)
forall r. DecidableUnits r => r -> Maybe r
recipUnit

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  Euclidean (WrapDecidableUnits k)

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  PID (WrapDecidableUnits k)

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  UFD (WrapDecidableUnits k)

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  GCDDomain (WrapDecidableUnits k)

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  UnitNormalForm (WrapDecidableUnits k)

instance
  ( DecidableAssociates k
  , Ring k
  , DecidableZero k
  , DecidableUnits k
  ) =>
  IntegralDomain (WrapDecidableUnits k)

deriving newtype instance
  LeftModule c k => LeftModule c (WrapDecidableUnits k)

deriving newtype instance
  RightModule c k => RightModule c (WrapDecidableUnits k)

unliftQuadInverse ::
  forall k.
  (CoeffRing k, Field k) =>
  -- | Multiplicity
  Natural ->
  -- | Formal fraction with square-free denominator of degree >= 2.
  Fraction (Unipol k) ->
  GeneralTerm k
unliftQuadInverse :: Natural -> Fraction (Unipol k) -> GeneralTerm k
unliftQuadInverse Natural
n Fraction (Unipol k)
f
  | Unipol k -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' (Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
denominator Fraction (Unipol k)
f) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
    Unipol k
-> (forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
-> GeneralTerm k
forall a r.
Euclidean a =>
a -> (forall s. Reifies s a => Proxy s -> r) -> r
reifyQuotient (Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
denominator Fraction (Unipol k)
f) ((forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
 -> GeneralTerm k)
-> (forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ \(Proxy s
den :: Proxy r) ->
      let root :: WrapDecidableUnits (Quotient s (Unipol k))
root = Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den IsLabel "x" (Unipol k)
Unipol k
#x
          g :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
g = (k -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall b a. DecidableZero b => (a -> b) -> Unipol a -> Unipol b
mapCoeffUnipol (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> (k -> Quotient s (Unipol k))
-> k
-> WrapDecidableUnits (Quotient s (Unipol k))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den (Unipol k -> Quotient s (Unipol k))
-> (k -> Unipol k) -> k -> Quotient s (Unipol k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff) (Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. (a -> b) -> a -> b
$ Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
denominator Fraction (Unipol k)
f
          h :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
h = (k -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall b a. DecidableZero b => (a -> b) -> Unipol a -> Unipol b
mapCoeffUnipol (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> (k -> Quotient s (Unipol k))
-> k
-> WrapDecidableUnits (Quotient s (Unipol k))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den (Unipol k -> Quotient s (Unipol k))
-> (k -> Unipol k) -> k -> Quotient s (Unipol k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff) (Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. (a -> b) -> a -> b
$ Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
numerator Fraction (Unipol k)
f
          rootg :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg = IsLabel "x" (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
#x Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall r. Group r => r -> r -> r
- Coefficient (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff Coefficient (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
WrapDecidableUnits (Quotient s (Unipol k))
root
          (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
root'g, Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
_) = Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
g Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
    Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall r.
(CoeffRing r, Field r) =>
Unipol r -> Unipol r -> (Unipol r, Unipol r)
`divModUnipol` Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg
          PartialFraction {NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
partialFracs :: NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
residualPoly :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
partialFracs :: forall k.
PartialFractionDecomp k -> NonEmpty (Unipol k, IntMap (Unipol k))
residualPoly :: forall k. PartialFractionDecomp k -> Unipol k
..} =
            Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
-> PartialFractionDecomp
     (WrapDecidableUnits (Quotient s (Unipol k)))
forall k.
(CoeffRing k, Field k) =>
Unipol k -> NonEmpty (Unipol k, Natural) -> PartialFractionDecomp k
partialFractionDecompositionWith Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
h ((Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg, Natural
n) (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
-> [(Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)]
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
forall a. a -> [a] -> NonEmpty a
:| [(Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
root'g, Natural
n)])
       in Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
den (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
            ((Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
  IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
 -> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
      IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
              ( \(Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z, IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
im) ->
                  let c :: WrapDecidableUnits (Quotient s (Unipol k))
c = WrapDecidableUnits (Quotient s (Unipol k))
-> WrapDecidableUnits (Quotient s (Unipol k))
forall r. Group r => r -> r
negate (WrapDecidableUnits (Quotient s (Unipol k))
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> WrapDecidableUnits (Quotient s (Unipol k))
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Coefficient
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z
                   in (Int
 -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
                        ( \Int
l Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
p ->
                            WrapDecidableUnits (Quotient s (Unipol k))
-> Natural
-> WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k.
(CoeffRing k, Field k) =>
k -> Natural -> k -> GeneralTerm k
linearInverse WrapDecidableUnits (Quotient s (Unipol k))
c (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l Natural -> Natural -> Natural
forall r. Multiplicative r => r -> r -> r
* Natural
n) (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Coefficient
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
p)
                        )
                        IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
im
              )
              NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
partialFracs
  | Bool
otherwise =
    Unipol k
-> (forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
-> GeneralTerm k
forall a r.
Euclidean a =>
a -> (forall s. Reifies s a => Proxy s -> r) -> r
reifyQuotient (Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
denominator Fraction (Unipol k)
f) ((forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
 -> GeneralTerm k)
-> (forall s. Reifies s (Unipol k) => Proxy s -> GeneralTerm k)
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ \(Proxy s
den :: Proxy r) ->
      let root :: WrapDecidableUnits (Quotient s (Unipol k))
root = Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den IsLabel "x" (Unipol k)
Unipol k
#x
          g :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
g = (k -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall b a. DecidableZero b => (a -> b) -> Unipol a -> Unipol b
mapCoeffUnipol (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> (k -> Quotient s (Unipol k))
-> k
-> WrapDecidableUnits (Quotient s (Unipol k))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den (Unipol k -> Quotient s (Unipol k))
-> (k -> Unipol k) -> k -> Quotient s (Unipol k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff) (Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. (a -> b) -> a -> b
$ Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
denominator Fraction (Unipol k)
f
          h :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
h = (k -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall b a. DecidableZero b => (a -> b) -> Unipol a -> Unipol b
mapCoeffUnipol (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> (k -> Quotient s (Unipol k))
-> k
-> WrapDecidableUnits (Quotient s (Unipol k))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
den (Unipol k -> Quotient s (Unipol k))
-> (k -> Unipol k) -> k -> Quotient s (Unipol k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff) (Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol k -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. (a -> b) -> a -> b
$ Fraction (Unipol k) -> Unipol k
forall t. Fraction t -> t
numerator Fraction (Unipol k)
f
          rootg :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg = IsLabel "x" (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
#x Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall r. Group r => r -> r -> r
- Coefficient (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff Coefficient (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
WrapDecidableUnits (Quotient s (Unipol k))
root
          (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
root'g, Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
_) = Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
g Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
    Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall r.
(CoeffRing r, Field r) =>
Unipol r -> Unipol r -> (Unipol r, Unipol r)
`divModUnipol` Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg
          PartialFraction {NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
partialFracs :: NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
residualPoly :: Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
partialFracs :: forall k.
PartialFractionDecomp k -> NonEmpty (Unipol k, IntMap (Unipol k))
residualPoly :: forall k. PartialFractionDecomp k -> Unipol k
..} =
            Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
-> PartialFractionDecomp
     (WrapDecidableUnits (Quotient s (Unipol k)))
forall k.
(CoeffRing k, Field k) =>
Unipol k -> NonEmpty (Unipol k, Natural) -> PartialFractionDecomp k
partialFractionDecompositionWith Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
h ((Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
rootg, Natural
1) (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
-> [(Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)]
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))), Natural)
forall a. a -> [a] -> NonEmpty a
:| [(Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
root'g, Natural
1)])
       in Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
den (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
            ((Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
  IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
 -> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> NonEmpty
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
      IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
              ( \(Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z, IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
im) ->
                  if Unipol (WrapDecidableUnits (Quotient s (Unipol k))) -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
                    then
                      let c :: WrapDecidableUnits (Quotient s (Unipol k))
c = WrapDecidableUnits (Quotient s (Unipol k))
-> WrapDecidableUnits (Quotient s (Unipol k))
forall r. Group r => r -> r
negate (WrapDecidableUnits (Quotient s (Unipol k))
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> WrapDecidableUnits (Quotient s (Unipol k))
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Coefficient
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z
                       in (Int
 -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
                            ( \Int
l Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
p ->
                                WrapDecidableUnits (Quotient s (Unipol k))
-> Natural
-> WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k.
(CoeffRing k, Field k) =>
k -> Natural -> k -> GeneralTerm k
linearInverse WrapDecidableUnits (Quotient s (Unipol k))
c (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l Natural -> Natural -> Natural
forall r. Multiplicative r => r -> r -> r
* Natural
n) (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Coefficient
     (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
p)
                            )
                            IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
im
                    else
                      (Int
 -> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall m a. Monoid m => (Int -> a -> m) -> IntMap a -> m
IM.foldMapWithKey
                        ( \Int
l Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
u ->
                            -- Because a denominator is square-free,
                            -- we can just recurse to extension field.
                            Natural
-> Fraction (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k.
(CoeffRing k, Field k) =>
Natural -> Fraction (Unipol k) -> GeneralTerm k
unliftQuadInverse
                              (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l Natural -> Natural -> Natural
forall r. Multiplicative r => r -> r -> r
* Natural
n)
                              (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
u Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
-> Fraction (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
forall d. GCDDomain d => d -> d -> Fraction d
F.% Unipol (WrapDecidableUnits (Quotient s (Unipol k)))
z)
                        )
                        IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k))))
im
              )
              NonEmpty
  (Unipol (WrapDecidableUnits (Quotient s (Unipol k))),
   IntMap (Unipol (WrapDecidableUnits (Quotient s (Unipol k)))))
partialFracs

linearInverse ::
  (CoeffRing k, Field k) =>
  -- | alpha for X - alpha
  k ->
  -- | power
  Natural ->
  -- | coefficient
  k ->
  GeneralTerm k
linearInverse :: k -> Natural -> k -> GeneralTerm k
linearInverse k
alpha Natural
k k
c =
  k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k
c k -> k -> k
forall r. Multiplicative r => r -> r -> r
* k -> k
forall r. Group r => r -> r
negate (k -> k
forall r. Division r => r -> r
recip k
alpha) k -> Natural -> k
forall r. Unital r => r -> Natural -> r
^ Natural
k)
    GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* ((GeneralTerm k
forall k. GeneralTerm k
N GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall r. Unital r => r
one) GeneralTerm k -> Power -> GeneralTerm k
forall k. GeneralTerm k -> Power -> GeneralTerm k
:^ Natural -> Power
P (Natural -> Natural
forall a. Enum a => a -> a
pred Natural
k))
    GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> k
forall r. Division r => r -> r
recip k
alpha) GeneralTerm k -> Power -> GeneralTerm k
forall k. GeneralTerm k -> Power -> GeneralTerm k
:^ Power
Np

type Rewriter = Writer Any

progress :: a -> Rewriter a
progress :: a -> Rewriter a
progress a
a = a
a a -> WriterT Any Identity () -> Rewriter a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Any -> WriterT Any Identity ()
forall w (m :: * -> *). (Monoid w, Monad m) => w -> WriterT w m ()
tell (Bool -> Any
Any Bool
True)

reduceGeneralTerm :: (Field k, CoeffRing k) => GeneralTerm k -> GeneralTerm k
reduceGeneralTerm :: GeneralTerm k -> GeneralTerm k
reduceGeneralTerm = (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> GeneralTerm k
forall a. (a -> Rewriter a) -> a -> a
fixedPoint GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm

fixedPoint :: (a -> Rewriter a) -> a -> a
fixedPoint :: (a -> Rewriter a) -> a -> a
fixedPoint a -> Rewriter a
f = a -> a
go
  where
    go :: a -> a
go a
x =
      let (a
x', Any Bool
reduced) = Rewriter a -> (a, Any)
forall w a. Monoid w => Writer w a -> (a, w)
runWriter (Rewriter a -> (a, Any)) -> Rewriter a -> (a, Any)
forall a b. (a -> b) -> a -> b
$ a -> Rewriter a
f a
x
       in if Bool
reduced then a -> a
go a
x' else a
x

simplifyGeneralTerm ::
  (Field k, CoeffRing k) => GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm :: GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm k :: GeneralTerm k
k@Const {} = GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GeneralTerm k
k
simplifyGeneralTerm k :: GeneralTerm k
k@GeneralTerm k
N = GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GeneralTerm k
k
simplifyGeneralTerm (GeneralTerm k
l :+ GeneralTerm k
r) =
  ((,) (GeneralTerm k -> GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT
     Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
l WriterT
  Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT Any Identity (GeneralTerm k, GeneralTerm k)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
r) WriterT Any Identity (GeneralTerm k, GeneralTerm k)
-> ((GeneralTerm k, GeneralTerm k) -> Rewriter (GeneralTerm k))
-> Rewriter (GeneralTerm k)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (Const k
z, GeneralTerm k
r') | k -> Bool
forall r. DecidableZero r => r -> Bool
isZero k
z -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
r'
    (GeneralTerm k
l', Const k
z) | k -> Bool
forall r. DecidableZero r => r -> Bool
isZero k
z -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
l'
    (Const k
l', Const k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ k
l' k -> k -> k
forall r. Additive r => r -> r -> r
+ k
r'
    (Const k
l', Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a) ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
l') GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Const k
r') ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
r')
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Lift Proxy s
s' GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
      | Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s Unipol k -> Unipol k -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s' ->
        GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. a -> b
unsafeCoerce GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
    (GeneralTerm k
l', GeneralTerm k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ GeneralTerm k
l' GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ GeneralTerm k
r'
simplifyGeneralTerm (GeneralTerm k
l :- GeneralTerm k
r) =
  ((,) (GeneralTerm k -> GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT
     Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
l WriterT
  Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT Any Identity (GeneralTerm k, GeneralTerm k)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
r) WriterT Any Identity (GeneralTerm k, GeneralTerm k)
-> ((GeneralTerm k, GeneralTerm k) -> Rewriter (GeneralTerm k))
-> Rewriter (GeneralTerm k)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (GeneralTerm k
l', Const k
z) | k -> Bool
forall r. DecidableZero r => r -> Bool
isZero k
z -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
l'
    (Const k
l', Const k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ k
l' k -> k -> k
forall r. Group r => r -> r -> r
- k
r'
    (Const k
l', Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a) ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
l') GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:- GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Const k
r') ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:- WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
r')
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Lift Proxy s
s' GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
      | Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s Unipol k -> Unipol k -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s' ->
        GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:- GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. a -> b
unsafeCoerce GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
    (GeneralTerm k
l', GeneralTerm k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ GeneralTerm k
l' GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:+ GeneralTerm k
r'
simplifyGeneralTerm (GeneralTerm k
l :* GeneralTerm k
r) =
  ((,) (GeneralTerm k -> GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT
     Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
l WriterT
  Any Identity (GeneralTerm k -> (GeneralTerm k, GeneralTerm k))
-> Rewriter (GeneralTerm k)
-> WriterT Any Identity (GeneralTerm k, GeneralTerm k)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
r) WriterT Any Identity (GeneralTerm k, GeneralTerm k)
-> ((GeneralTerm k, GeneralTerm k) -> Rewriter (GeneralTerm k))
-> Rewriter (GeneralTerm k)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (Const k
z, GeneralTerm k
r')
      | k -> Bool
forall r. DecidableZero r => r -> Bool
isZero k
z -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall m. Monoidal m => m
zero
      | k
z k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
forall r. Unital r => r
one -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
r'
    (GeneralTerm k
l', Const k
z)
      | k -> Bool
forall r. DecidableZero r => r -> Bool
isZero k
z -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall m. Monoidal m => m
zero
      | k
z k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
forall r. Unital r => r
one -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
l'
    (Const k
l', Const k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ k
l' k -> k -> k
forall r. Multiplicative r => r -> r -> r
* k
r'
    (Const k
l', Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a) ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
l') GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Const k
r') ->
      GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$
        Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
 -> GeneralTerm k)
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall a b. (a -> b) -> a -> b
$
          GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* WrapDecidableUnits (Quotient s (Unipol k))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. k -> GeneralTerm k
Const (Quotient s (Unipol k) -> WrapDecidableUnits (Quotient s (Unipol k))
forall k. k -> WrapDecidableUnits k
WrapDecidableUnits (Quotient s (Unipol k)
 -> WrapDecidableUnits (Quotient s (Unipol k)))
-> Quotient s (Unipol k)
-> WrapDecidableUnits (Quotient s (Unipol k))
forall a b. (a -> b) -> a -> b
$ Proxy s -> Unipol k -> Quotient s (Unipol k)
forall k (r :: k) a (proxy :: k -> *).
(Reifies r a, Euclidean a) =>
proxy r -> a -> Quotient r a
quotientBy Proxy s
s (Unipol k -> Quotient s (Unipol k))
-> Unipol k -> Quotient s (Unipol k)
forall a b. (a -> b) -> a -> b
$ Coefficient (Unipol k) -> Unipol k
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff k
Coefficient (Unipol k)
r')
    (Lift Proxy s
s GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a, Lift Proxy s
s' GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
      | Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s Unipol k -> Unipol k -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy s -> Unipol k
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect Proxy s
s' ->
        GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
s (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
forall a b. a -> b
unsafeCoerce GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
b)
    (GeneralTerm k
l', GeneralTerm k
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ GeneralTerm k
l' GeneralTerm k -> GeneralTerm k -> GeneralTerm k
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
:* GeneralTerm k
r'
simplifyGeneralTerm (GeneralTerm k
l :^ Power
p) = do
  GeneralTerm k
lred <- GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm k
l
  case (GeneralTerm k
lred, Power
p) of
    (l' :: GeneralTerm k
l'@(Const k
z), Power
_)
      | k
z k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
forall r. Unital r => r
one -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress GeneralTerm k
l'
    (Const k
z, P Natural
n) -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ k
z k -> Natural -> k
forall r. Unital r => r -> Natural -> r
^ Natural
n
    (GeneralTerm k
_, P Natural
0) -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const k
forall r. Unital r => r
one
    (GeneralTerm k
l', Power
r') -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ GeneralTerm k
l' GeneralTerm k -> Power -> GeneralTerm k
forall k. GeneralTerm k -> Power -> GeneralTerm k
:^ Power
r'
simplifyGeneralTerm (Lift Proxy s
p GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a) =
  GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> Rewriter
     (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
a Rewriter (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k))))
-> (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
    -> Rewriter (GeneralTerm k))
-> Rewriter (GeneralTerm k)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Const (WrapDecidableUnits Quotient s (Unipol k)
a')
      | Unipol k -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' (Quotient s (Unipol k) -> Unipol k
forall k (r :: k) a. Quotient r a -> a
representative Quotient s (Unipol k)
a') Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 ->
        GeneralTerm k -> Rewriter (GeneralTerm k)
forall a. a -> Rewriter a
progress (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ k -> GeneralTerm k
forall k. k -> GeneralTerm k
Const (k -> GeneralTerm k) -> k -> GeneralTerm k
forall a b. (a -> b) -> a -> b
$ Unipol k -> Coefficient (Unipol k)
forall poly. IsPolynomial poly => poly -> Coefficient poly
constantTerm (Unipol k -> Coefficient (Unipol k))
-> Unipol k -> Coefficient (Unipol k)
forall a b. (a -> b) -> a -> b
$ Quotient s (Unipol k) -> Unipol k
forall k (r :: k) a. Quotient r a -> a
representative Quotient s (Unipol k)
a'
    GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
r -> GeneralTerm k -> Rewriter (GeneralTerm k)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> Rewriter (GeneralTerm k)
forall a b. (a -> b) -> a -> b
$ Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
p GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
r

{-

Solves fibonnaci sequence; i.e.  recurrent sequence defined by
a_{n + 2} = 1 a_n + 1 a_{n + 1}
a_0 = 0
a_1 = 1

>>> fib <- evalRandIO $ solveTernaryRecurrence (1 :< 1 :< Nil) (0 :< 1 :< Nil) 0
>>> evalGeneralTerm fib 12
144
-}
evalGeneralTerm ::
  (CoeffRing k, Field k) =>
  GeneralTerm k ->
  Natural ->
  GeneralTerm k
evalGeneralTerm :: GeneralTerm k -> Natural -> GeneralTerm k
evalGeneralTerm GeneralTerm k
f Natural
n = (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k -> GeneralTerm k
forall a. (a -> Rewriter a) -> a -> a
fixedPoint (GeneralTerm k -> Rewriter (GeneralTerm k)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN (GeneralTerm k -> Rewriter (GeneralTerm k))
-> (GeneralTerm k -> Rewriter (GeneralTerm k))
-> GeneralTerm k
-> Rewriter (GeneralTerm k)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> GeneralTerm k -> Rewriter (GeneralTerm k)
forall k.
(Field k, CoeffRing k) =>
GeneralTerm k -> Rewriter (GeneralTerm k)
simplifyGeneralTerm) GeneralTerm k
f
  where
    substN :: (CoeffRing f, Field f) => GeneralTerm f -> Rewriter (GeneralTerm f)
    substN :: GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
N = GeneralTerm f -> Rewriter (GeneralTerm f)
forall a. a -> Rewriter a
progress (GeneralTerm f -> Rewriter (GeneralTerm f))
-> GeneralTerm f -> Rewriter (GeneralTerm f)
forall a b. (a -> b) -> a -> b
$ f -> GeneralTerm f
forall k. k -> GeneralTerm k
Const (f -> GeneralTerm f) -> f -> GeneralTerm f
forall a b. (a -> b) -> a -> b
$ Natural -> f
forall r. Rig r => Natural -> r
fromNatural Natural
n
    substN k :: GeneralTerm f
k@Const {} = GeneralTerm f -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GeneralTerm f
k
    substN (GeneralTerm f
l :+ GeneralTerm f
r) = GeneralTerm f -> GeneralTerm f -> GeneralTerm f
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:+) (GeneralTerm f -> GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f)
-> WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
l WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f) -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
r
    substN (GeneralTerm f
l :- GeneralTerm f
r) = GeneralTerm f -> GeneralTerm f -> GeneralTerm f
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:-) (GeneralTerm f -> GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f)
-> WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
l WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f) -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
r
    substN (GeneralTerm f
l :* GeneralTerm f
r) = GeneralTerm f -> GeneralTerm f -> GeneralTerm f
forall k. GeneralTerm k -> GeneralTerm k -> GeneralTerm k
(:*) (GeneralTerm f -> GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f)
-> WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
l WriterT Any Identity (GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f) -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
r
    substN (GeneralTerm f
l :^ Power
Np) = (GeneralTerm f -> Power -> GeneralTerm f
forall k. GeneralTerm k -> Power -> GeneralTerm k
:^ Natural -> Power
P Natural
n) (GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f) -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
l
    substN (GeneralTerm f
l :^ P Natural
k) = (GeneralTerm f -> Power -> GeneralTerm f
forall k. GeneralTerm k -> Power -> GeneralTerm k
:^ Natural -> Power
P Natural
k) (GeneralTerm f -> GeneralTerm f)
-> Rewriter (GeneralTerm f) -> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm f -> Rewriter (GeneralTerm f)
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm f
l
    substN (Lift Proxy s
p GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f)))
s) = Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f)))
-> GeneralTerm f
forall s k.
Reifies s (Unipol k) =>
Proxy s
-> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol k)))
-> GeneralTerm k
Lift Proxy s
p (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f)))
 -> GeneralTerm f)
-> WriterT
     Any
     Identity
     (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f))))
-> Rewriter (GeneralTerm f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f)))
-> WriterT
     Any
     Identity
     (GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f))))
forall f.
(CoeffRing f, Field f) =>
GeneralTerm f -> Rewriter (GeneralTerm f)
substN GeneralTerm (WrapDecidableUnits (Quotient s (Unipol f)))
s