{-# 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_
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
solveTernaryRecurrence ::
(MonadRandom m) =>
Sized 2 Rational ->
Sized 2 Rational ->
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)
solveRationalRecurrence ::
(MonadRandom m) =>
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')
solveFiniteFieldRecurrence ::
(MonadRandom m, CoeffRing k, FiniteField k, Random k) =>
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) =>
(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)
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
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) =>
Natural ->
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 ->
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) =>
k ->
Natural ->
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
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