{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Structure.Number.Definition
-- Description : definition of numbers as ordered semi rings with infinitely many elements
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of numbers as ordered 'Semiring' with infinitely many elements.
module OAlg.Structure.Number.Definition
  (
    -- * Number
    Number(..), zFloor

    -- | digital represenation of numbers
  , toDigits, Digits(..)
  , toDigitsFinite, fromDigits
  , dgsBase, dgsProxy, dgsFrcTake

    -- * Integral
  , Integral(..), primes

    -- * Acyclic
  , Acyclic(..)

    -- * Fractional
  , Fractional

    -- * Measurable
  , Measurable(..)
  )
  where

import qualified Prelude as A

import Data.Proxy

import OAlg.Prelude

import OAlg.Data.TypeLits
import OAlg.Data.Canonical

import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Multiplicative.Definition
import OAlg.Structure.Additive.Definition
import OAlg.Structure.Distributive.Definition
import OAlg.Structure.Ring.Definition

--------------------------------------------------------------------------------
-- Number -

-- | ordered commutative semi ring where v'+' and v'*' respect the given ordering.
--
-- __Definitions__
--
-- (1) A number @x@ is called __/positive/__ if @0 < x@ and __/negative/__ if @x < 0@.
--
-- (2) A number structure is called __/positive/__ if it contains no negative elements.
--
-- __Properties__
--
-- (1) @1@ is positive.
--
-- (2) For all @x < y@ and @z@ holds: @x v'+' z < y v'+' z@
--
-- (3) For all @0 < x@, @0 < y@ holds: @0 < x v'*' y@.
--
-- (4) For all @x@ holds: @x == 'signum' x v'*' 'abs' x@.
--
-- (5) For all @x@ holds: @'floor' x  v'+' 'fraction' x == x@.
--
-- __Note__
--
-- (1) A not positive structure of numbers contain always also the additive inverse of @1@
-- which is negative.
--
-- (2) Structures of numbers have infinitely many values, because from the
-- properties above follows that
-- @0 < 1 < 2 < .. < 'ntimes' n 1 < 'ntimes' (n v'+' 1) 1 < .. @ for all @0 <= n@.
class (Semiring r, Commutative r, Ord r) => Number r where
  {-# MINIMAL minusOne, zFloorFraction #-}

  -- | the additive inverse of @1@ - if it exists - and will be
  --   denoted by @-1@ (see the note above).
  minusOne :: Maybe r

  -- | sign of a number.
  --
  -- __Property__ For all @x@ holds: if @0 < x@ then @signum x == 1@ and if @x == 0@
  -- then @signum x == 0@ and if @x < 0@ then @signum x == -1@ (for @-1@ see @'minusOne'@).
  --
  -- __Note__ The default implementation is:
  --
  -- @
  -- signum x = case rZero `compare` x of
  --              GT -> rOne
  --              EQ -> rZero
  --              LT -> e where Just e = minusOne
  -- @
  signum :: r -> r
  signum r
x = case r
forall r. Semiring r => r
rZero r -> r -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` r
x of
             Ordering
GT -> r
forall r. Semiring r => r
rOne
             Ordering
EQ -> r
forall r. Semiring r => r
rZero
             Ordering
LT -> r
e where Just r
e = Maybe r
forall r. Number r => Maybe r
minusOne
             
  -- | absolute value of a number.
  --
  -- __Definition__ The __/absolute value/__ of a @x@ is defined by
  -- @abs x = 'signum' x v'*' x@ (which serves as the default implementation).
  --
  -- __Properties__ For all @x@ holds:
  --
  -- (1) @0 <= abs x@.
  --
  -- (2) if @0 <= x@ then @abs x == x@.
  abs :: r -> r
  abs r
x = r -> r
forall r. Number r => r -> r
signum r
x r -> r -> r
forall c. Multiplicative c => c -> c -> c
* r
x

  -- | floor of a value of a number.
  --
  -- __Properties__
  --
  -- (1) @floor 0 == 0@.
  --
  -- (2) For all @x@ holds: @floor (x v'+' 1) = floor x v'+' 1@.
  floor :: r -> r
  floor r
x = N -> r -> r
forall a. Additive a => N -> a -> a
ntimes (Z -> N
forall a b. Projectible a b => b -> a
prj (Z -> N) -> Z -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Z, r) -> Z
forall a b. (a, b) -> a
fst ((Z, r) -> Z) -> (Z, r) -> Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction (r -> (Z, r)) -> r -> (Z, r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ r
x) (r -> r
forall r. Number r => r -> r
signum r
x)

  -- | fractional part of a number.
  --
  -- __Property__ For all @x@ holds: 0 <= fraction x < 1.
  fraction :: r -> r
  fraction = (Z, r) -> r
forall a b. (a, b) -> b
snd ((Z, r) -> r) -> (r -> (Z, r)) -> r -> r
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction

  -- | simultaneous evaluation of @'floor'@ - represented as an integer - and its
  -- @'fraction'@.
  --
  -- __Properties__ For all @x@ holds:
  --
  -- (1) @'floor' x == 'ntimes' ('prj' '$' fst '$' 'zFloorFraction' '$' x) ('signum' x)@.
  --
  -- (2) @'fraction' x == 'snd' '.' 'zFloorFraction'@.
  --
  -- __Note__ This properties are used for the default implementation of @'floor'@
  -- and @'fraction'@.
  zFloorFraction :: r -> (Z,r)

--------------------------------------------------------------------------------
-- zFloor -

-- | floor to 'Z'.
zFloor :: Number r => r -> Z
zFloor :: forall r. Number r => r -> Z
zFloor = (Z, r) -> Z
forall a b. (a, b) -> a
fst((Z, r) -> Z) -> (r -> (Z, r)) -> r -> Z
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction

--------------------------------------------------------------------------------
-- Number - Instances -

instance Number N where
  minusOne :: Maybe N
minusOne          = Maybe N
forall a. Maybe a
Nothing
  abs :: N -> N
abs             N
n = N
n
  signum :: N -> N
signum          N
n = if N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 then N
0 else N
1
  floor :: N -> N
floor           N
n = N
n
  fraction :: N -> N
fraction        N
_ = N
0
  zFloorFraction :: N -> (Z, N)
zFloorFraction  N
n = (N -> Z
forall a b. Embeddable a b => a -> b
inj N
n, N
0)  
  
instance Number Integer where
  minusOne :: Maybe Integer
minusOne         = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (-Integer
1)
  abs :: Integer -> Integer
abs              = Integer -> Integer
forall a. Num a => a -> a
A.abs
  signum :: Integer -> Integer
signum           = Integer -> Integer
forall a. Num a => a -> a
A.signum
  floor :: Integer -> Integer
floor          Integer
z = Integer
z
  fraction :: Integer -> Integer
fraction       Integer
_ = Integer
0
  zFloorFraction :: Integer -> (Z, Integer)
zFloorFraction Integer
z = (Integer -> Z
forall a b. Embeddable a b => a -> b
inj Integer
z,Integer
0)

instance Number Z where
  minusOne :: Maybe Z
minusOne         = Z -> Maybe Z
forall a. a -> Maybe a
Just (-Z
1)
  abs :: Z -> Z
abs              = Z -> Z
forall a. Num a => a -> a
A.abs
  signum :: Z -> Z
signum           = Z -> Z
forall a. Num a => a -> a
A.signum
  floor :: Z -> Z
floor          Z
z = Z
z
  fraction :: Z -> Z
fraction       Z
_ = Z
0
  zFloorFraction :: Z -> (Z, Z)
zFloorFraction Z
z = (Z
z,Z
0)

instance Number Q where
  minusOne :: Maybe Q
minusOne       = Q -> Maybe Q
forall a. a -> Maybe a
Just (-Q
1)
  abs :: Q -> Q
abs            = Q -> Q
forall a. Num a => a -> a
A.abs
  signum :: Q -> Q
signum         = Q -> Q
forall a. Num a => a -> a
A.signum
  floor :: Q -> Q
floor  Q
q       = Q -> Z
forall b. Integral b => Q -> b
forall a b. (RealFrac a, Integral b) => a -> b
A.floor Q
q Z -> N -> Q
% N
1
  zFloorFraction :: Q -> (Z, Q)
zFloorFraction = Q -> (Z, Q)
forall b. Integral b => Q -> (b, Q)
forall a b. (RealFrac a, Integral b) => a -> (b, a)
A.properFraction

--------------------------------------------------------------------------------
-- Integral -

-- | discrete numbers.
--
-- __Property__ For all @x@ holds: @'fraction' x '==' 0@.
class Number a => Integral a where
  {-# MINIMAL divMod #-}

  divMod :: a -> a -> (a,a)

  div :: a -> a -> a
  div a
a a
b = (a, a) -> a
forall a b. (a, b) -> a
fst (a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
a a
b)

  mod :: a -> a -> a
  mod a
a a
b = (a, a) -> a
forall a b. (a, b) -> b
snd (a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
a a
b)

instance Integral N where
  divMod :: N -> N -> (N, N)
divMod = N -> N -> (N, N)
forall a. Integral a => a -> a -> (a, a)
A.divMod
  div :: N -> N -> N
div    = N -> N -> N
forall a. Integral a => a -> a -> a
A.div
  mod :: N -> N -> N
mod    = N -> N -> N
forall a. Integral a => a -> a -> a
A.mod
  
instance Integral Z where
  divMod :: Z -> Z -> (Z, Z)
divMod = Z -> Z -> (Z, Z)
forall a. Integral a => a -> a -> (a, a)
A.divMod
  div :: Z -> Z -> Z
div    = Z -> Z -> Z
forall a. Integral a => a -> a -> a
A.div
  mod :: Z -> Z -> Z
mod    = Z -> Z -> Z
forall a. Integral a => a -> a -> a
A.mod
  
--------------------------------------------------------------------------------
-- primes 

-- | the list of prime numbers.
primes :: [N]
primes :: [N]
primes = [N] -> [N]
forall {a}. (Integral a, Num a) => [a] -> [a]
filterPrime [N
2..]
  where filterPrime :: [a] -> [a]
filterPrime (a
p:[a]
xs) = a
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
filterPrime [a
x | a
x <- [a]
xs, a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
0]

--------------------------------------------------------------------------------
-- Acyclic -

-- | distributive structure with entities scaleable by 'Q'.
--
-- __Property__ For every @0 '<' n@ and point @p@ holds: @'ntimes' n ('one' p)@ is
-- invertible.
--
-- __Note__
--
-- (1) The cyclic rings @'OAlg.Entity.Commutative.Mod' n@ for @2 <= n@ are not scaleable by
-- @'Q'@, because @1 '/=' 0@ and @'ntimes' n 1 '==' 0@!
--
-- (2) If for every point @p@ holds that @'zero' (p':>'p) '==' 'one' p@ then the structure
-- is scaleable by 'Q' (e.g. @'Orientation' p@).
class (Distributive a, Abelian a, Invertible a) => Acyclic a where
  
  -- | @'qtimes' q a '==' 'ztimes' z a v'*' 'invert' ('ntimes' n ('one' ('start' a)))@.
  --   where @z = 'numerator' q@ and @n = 'denominator' q@.
  qtimes :: Q -> a -> a
  qtimes Q
q a
a = Z -> a -> a
forall a. Abelian a => Z -> a -> a
ztimes Z
z a
a a -> a -> a
forall c. Multiplicative c => c -> c -> c
* a -> a
forall c. Invertible c => c -> c
invert (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes N
n (Point a -> a
forall c. Multiplicative c => Point c -> c
one (a -> Point a
forall q. Oriented q => q -> Point q
start a
a)))
    where z :: Z
z = Q -> Z
numerator Q
q
          n :: N
n = Q -> N
denominator Q
q

instance Acyclic () where
  qtimes :: Q -> () -> ()
qtimes Q
_ ()
_ = ()
  
instance Acyclic Q where
  qtimes :: Q -> Q -> Q
qtimes = Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
(*)
  
--------------------------------------------------------------------------------
-- Fractional -

-- | continuous numbers, i.e acyclic and negateable numbers. They induce a sub
--   @'Q'@-vectorial structures of the real numbers.
--
--   __Note__ We will distinguish here instances of @'Fractional'@ and the mathematical
--   entities of real numbers! 
type Fractional r = (Number r, Abelian r, Acyclic r)

--------------------------------------------------------------------------------
-- Measurable -

-- | measurable entities.
class (Entity a, Number r) => Measurable a r where

  -- | distance of two points.
  --
  --   __Properties__ Let @__a__@ @__r__@ be 'Measurable', then holds:
  --
  --   (1) For all @x@ and @y@ in @__a__@ holds: @0 <= dist x y@
  --
  --   (2) For all @x@ and @y@ in @__a__@ holds: @dist x y == 0@ if and only if @x == y@.
  --
  --   (3) For all @x@ and @y@ in @__a__@ holds: @dist x y == dist y x@.
  --
  --   (4) For all @x@, @y@ and @z@ in @__a__@ holds: @dist x z@ <= @dist x y@ v'+' @dist y z@
  dist :: a -> a -> r

instance (Number r, Abelian r) => Measurable r r where
  dist :: r -> r -> r
dist r
a r
b = r -> r
forall r. Number r => r -> r
abs (r
b r -> r -> r
forall a. Abelian a => a -> a -> a
- r
a)

instance Measurable N Z where
  dist :: N -> N -> Z
dist N
a N
b = N -> Z
forall a b. Embeddable a b => a -> b
inj (N -> Z) -> N -> Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N
forall a. Num a => a -> a
A.abs (N -> N) -> N -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (N
b N -> N -> N
forall a. Num a => a -> a -> a
A.- N
a)

----------------------------------------
-- Digits -

-- | digital representation of numbers for the given base @b@.
--
-- __Note__
--
-- (1) 'dgsFlr' is a finite list
--
-- (2) 'dgsFrc' maybe a infinite list and as such 'valid' could end up in an
-- infinite proposition!
data Digits (b :: Nat) r where
  Digits :: 2 <= b
    => { forall (b :: Natural) r. Digits b r -> r
dgsSig :: r    -- ^ the signum.
       , forall (b :: Natural) r. Digits b r -> [N]
dgsFlr :: [N]  -- ^ the digital representation of the floor part
       , forall (b :: Natural) r. Digits b r -> [N]
dgsFrc :: [N]  -- ^ the digital representation of the fractional part
       }
    -> Digits b r

deriving instance Show r => Show (Digits b r)
deriving instance Eq r => Eq (Digits b r)
deriving instance Ord r => Ord (Digits b r)

instance Validable r => Validable (Digits b r) where
  valid :: Digits b r -> Statement
valid (Digits r
r [N]
n [N]
m) = [Statement] -> Statement
And [r -> Statement
forall a. Validable a => a -> Statement
valid r
r,[N] -> Statement
forall a. Validable a => a -> Statement
valid [N]
n,[N] -> Statement
forall a. Validable a => a -> Statement
valid [N]
m]
  
--------------------------------------------------------------------------------
-- dgsProxy -

-- | the proxy with the same type @b@.
dgsProxy :: Digits b r -> Proxy b
dgsProxy :: forall (b :: Natural) r. Digits b r -> Proxy b
dgsProxy Digits b r
_ = Proxy b
forall {k} (t :: k). Proxy t
Proxy 

--------------------------------------------------------------------------------
-- dgsBase -

-- | the base of a digit, i.e. the corresponding natural number of the type literal @b@.
dgsBase :: KnownNat b => Digits b r -> N
dgsBase :: forall (b :: Natural) r. KnownNat b => Digits b r -> N
dgsBase = Integer -> N
forall a b. Projectible a b => b -> a
prj (Integer -> N) -> (Digits b r -> Integer) -> Digits b r -> N
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Proxy b -> Integer
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy b -> Integer)
-> (Digits b r -> Proxy b) -> Digits b r -> Integer
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Digits b r -> Proxy b
forall (b :: Natural) r. Digits b r -> Proxy b
dgsProxy

--------------------------------------------------------------------------------
-- dgsFrcTake -

-- | limits the fractional part 'dgsFrc' to the length of @n@.
dgsFrcTake :: N -> Digits b r -> Digits b r
dgsFrcTake :: forall (b :: Natural) r. N -> Digits b r -> Digits b r
dgsFrcTake N
n (Digits r
r [N]
flr [N]
frc) = r -> [N] -> [N] -> Digits b r
forall (b :: Natural) r. (2 <= b) => r -> [N] -> [N] -> Digits b r
Digits r
r [N]
flr (N -> [N] -> [N]
forall a. N -> [a] -> [a]
takeN N
n ([N] -> [N]) -> [N] -> [N]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [N]
frc)

--------------------------------------------------------------------------------
-- toDigits -
-- | the digital representation of @x@ in the base @b@.
--
--   Let @'Digits' s xs ys = 'toDigits' r@ then
--
--   * @s@ is the @'signum' x@.
--
--   * @xs@ is the digital representation of @'abs' ('floor' x)@ .
--
--   * @ys@ is the - possibly infinite - digital representation of @'abs' ('fraction' x)@
--     in the base @b@.
--
--   __Examples__
--
-- >>> toDigits (1/3) :: Digits 10 Q
-- Digits 1 [] [3,3,3..]
--
-- >>> toDigits (-4/3) :: Digits 3 Q
-- Digits (-1) [1] [1]
--
-- __Note__ To get the first @n@ digits of the fractional part @ys@ for the digital
-- representation of @x@ use @'toDigitsFinite' n x@.
toDigits :: (Number r, KnownNat b, 2 <= b) => r -> Digits b r
toDigits :: forall r (b :: Natural).
(Number r, KnownNat b, 2 <= b) =>
r -> Digits b r
toDigits r
x = Digits b r
res
  where res :: Digits b r
res   = r -> [N] -> [N] -> Digits b r
forall (b :: Natural) r. (2 <= b) => r -> [N] -> [N] -> Digits b r
Digits r
sig (Z -> [N] -> [N]
dgtsFlr Z
z []) (r -> [N]
dgtsFrc r
f)
        base :: N
base  = Digits b r -> N
forall (b :: Natural) r. KnownNat b => Digits b r -> N
dgsBase Digits b r
res
        sig :: r
sig   = r -> r
forall r. Number r => r -> r
signum r
x
        (Z
z,r
f) = r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction (r -> (Z, r)) -> r -> (Z, r)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ r -> r
forall r. Number r => r -> r
abs r
x
          
        zbs :: Z
zbs          = N -> Z
forall a b. Embeddable a b => a -> b
inj N
base
        dgtsFlr :: Z -> [N] -> [N]
dgtsFlr Z
t [N]
ds = if Z
t Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
== Z
forall r. Semiring r => r
rZero then [N]
ds else Z -> [N] -> [N]
dgtsFlr Z
z' [N]
ds'
          where (Z
z',Z
zn) = Z -> Z -> (Z, Z)
forall a. Integral a => a -> a -> (a, a)
divMod Z
t Z
zbs
                ds' :: [N]
ds'     = Z -> N
forall a b. Projectible a b => b -> a
prj Z
zn N -> [N] -> [N]
forall a. a -> [a] -> [a]
: [N]
ds
          
        dgtsFrc :: r -> [N]
dgtsFrc r
frc = if r
frc r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
forall r. Semiring r => r
rZero then [] else Z -> N
forall a b. Projectible a b => b -> a
prj Z
flr N -> [N] -> [N]
forall a. a -> [a] -> [a]
: r -> [N]
dgtsFrc r
frc'
          where (Z
flr,r
frc') = r -> (Z, r)
forall r. Number r => r -> (Z, r)
zFloorFraction (N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
base r
frc)

--------------------------------------------------------------------------------
-- toDigitsFinite -

-- | @toDigitsFinite n@ is like 'toDigits' but the fractional part is limited to the
-- length of @n@ and is given by @'dgsFrcTake' n '.' 'toDigits'@.
toDigitsFinite :: (Number r, KnownNat b, 2 <= b) => N -> r -> Digits b r
toDigitsFinite :: forall r (b :: Natural).
(Number r, KnownNat b, 2 <= b) =>
N -> r -> Digits b r
toDigitsFinite N
n = N -> Digits b r -> Digits b r
forall (b :: Natural) r. N -> Digits b r -> Digits b r
dgsFrcTake N
n (Digits b r -> Digits b r) -> (r -> Digits b r) -> r -> Digits b r
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. r -> Digits b r
forall r (b :: Natural).
(Number r, KnownNat b, 2 <= b) =>
r -> Digits b r
toDigits

--------------------------------------------------------------------------------
-- fromDigits -

-- | @fromDigits n dgs\@('Digits' s xs ys)@ is given by
--   @s v'*' (xm v'*' b'^'m v'+' .. v'+' xi v'*' b'^'i v'+' .. v'+' x0 v'*' b'^'0  v'+' y1 v'*' r'^'1 v'+' .. v'+' yj v'*' r'^'j v'+' .. v'+' yn v'*' r'^'n@
-- where @b = 'dgsBase' dgs@, @xs = [xm..xi..x0]@, @ys = [y1,y2..yj..yn..]@
-- and @r = 'invert' b@.
--
-- __Property__ Let @1 '<' b@ and @dgs = 'Digits' s xs ys@ where @s@ is either 1 or -1
-- and @0 v'<=' xi '<' b@ for all @i@ and @0 v'<=' yj '<' b@ for all @j@
-- then for all @n@ holds: @'toDigits' b n ('fromDigits' b n dgs) '==' dgs@.
--
-- __Note__
--
-- (1) All the elements of the above formula are lifted to the type @r@ via
-- @\\x -> 'ntimes' x 'rOne'@.
--
-- (2) Because the type @r@ is acyclic, the expression @'invert' b@ - which is actually
-- @'invert' ('ntimes' b 'rOne')@ - is regular.
--
-- (3) If @b@ is not bigger then 1 then an exception 'Undefined' will be thrown.
fromDigits :: (Number r, Acyclic r, KnownNat b) => N -> Digits b r -> r
fromDigits :: forall r (b :: Natural).
(Number r, Acyclic r, KnownNat b) =>
N -> Digits b r -> r
fromDigits N
n dgs :: Digits b r
dgs@(Digits r
s [N]
flr [N]
frc)
  = r
s r -> r -> r
forall c. Multiplicative c => c -> c -> c
* (r -> [N] -> r -> r
forall r. Number r => r -> [N] -> r -> r
rFlr r
b' [N]
flr r
forall r. Semiring r => r
rZero r -> r -> r
forall a. Additive a => a -> a -> a
+ r -> r -> [N] -> r -> r
forall r. Number r => r -> r -> [N] -> r -> r
rFrc r
br r
br (N -> [N] -> [N]
forall a. N -> [a] -> [a]
takeN N
n [N]
frc) r
forall r. Semiring r => r
rZero) where
    b :: N
b  = Digits b r -> N
forall (b :: Natural) r. KnownNat b => Digits b r -> N
dgsBase Digits b r
dgs
    b' :: r
b' = N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
b r
forall r. Semiring r => r
rOne
    br :: r
br = r -> r
forall c. Invertible c => c -> c
invert r
b'
        -- invert b' is regular, because r is acyclic!!
        
    rFlr :: Number r => r -> [N] -> r -> r
    rFlr :: forall r. Number r => r -> [N] -> r -> r
rFlr r
_ []     r
r = r
r
    rFlr r
x (N
d:[N]
ds) r
r = r -> [N] -> r -> r
forall r. Number r => r -> [N] -> r -> r
rFlr r
x [N]
ds (r
x r -> r -> r
forall c. Multiplicative c => c -> c -> c
* r
r r -> r -> r
forall a. Additive a => a -> a -> a
+ N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
d r
forall r. Semiring r => r
rOne)

    rFrc :: Number r => r -> r -> [N] -> r -> r
    rFrc :: forall r. Number r => r -> r -> [N] -> r -> r
rFrc r
_  r
_ [] r
r    = r
r
    rFrc r
x r
y (N
d:[N]
ds) r
r = r -> r -> [N] -> r -> r
forall r. Number r => r -> r -> [N] -> r -> r
rFrc r
x r
z [N]
ds (r
r r -> r -> r
forall a. Additive a => a -> a -> a
+ r
y r -> r -> r
forall c. Multiplicative c => c -> c -> c
* N -> r -> r
forall a. Additive a => N -> a -> a
ntimes N
d r
forall r. Semiring r => r
rOne) where z :: r
z = r
xr -> r -> r
forall c. Multiplicative c => c -> c -> c
*r
y