{-# LANGUAGE NoImplicitPrelude #-}

-- |
-- Module      : OAlg.AbelianGroup.Euclid
-- Description : basic algorithms for integers
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- basic algorithms for the integers 'Z'.
module OAlg.AbelianGroup.Euclid
  ( gcd, gcds, lcm, lcms, euclid, mod0, (//)
  )
  where

import OAlg.Prelude

import Data.List (foldl)

import OAlg.Data.Canonical

import OAlg.Structure.Additive
import OAlg.Structure.Multiplicative
import OAlg.Structure.Number


--------------------------------------------------------------------------------
-- mod0 -

-- | extended modulo in 'Z' according to 'N'.
--
-- __Property__ For all @z@ and @n@ holds
--
-- (1) @'mod0' z 0 '==' z@.
--
-- (2) if @0 < n@ than @'mod0' z n '==' 'mod' z ('inj' n)@.
mod0 :: Z -> N -> Z
mod0 :: Z -> N -> Z
mod0 Z
z N
0 = Z
z
mod0 Z
z N
n = Z -> Z -> Z
forall a. Integral a => a -> a -> a
mod Z
z (N -> Z
forall a b. Embeddable a b => a -> b
inj N
n)

--------------------------------------------------------------------------------
-- (//) -

infix 7 //

-- | extended division in 'Z' by a dividend in 'N'.
--
--  __Properties__ For all @z@ and @n@ holds:
--
--  (1) @0 // 0 '==' 1@.
--
--  (2) if @z '/=' 0@ then @z // 0 '==' 0@.
--
--  (3) if @0 '<' n@ then @z // n '==' 'div' z n@.
--
--  (4) @z '==' (z // n) '*' 'inj' n '+' 'mod0' z n@.
(//) :: Z -> N -> Z
Z
0 // :: Z -> N -> Z
// N
0 = Z
1
Z
_ // N
0 = Z
0
Z
z // N
n = Z -> Z -> Z
forall a. Integral a => a -> a -> a
div Z
z (N -> Z
forall a b. Embeddable a b => a -> b
inj N
n)

--------------------------------------------------------------------------------
-- euclid -

-- | extended euclidean algorithm to determine the greatest cowmon divisor.
--
-- __Properties__ @(g,s,t) = 'euclid' a b@ then
--
-- (1) @g@ is the greatest common divisor of @a@ and @b@.
--
-- (2) @g '==' s '*' a '+' t '*' b@.
euclid :: Z -> Z -> (N,Z,Z)
  -- we use the property: signum x * x == abs x for all x :: Z
euclid :: Z -> Z -> (N, Z, Z)
euclid Z
a Z
b = (Z -> N
forall a b. Projectible a b => b -> a
prj Z
r,Z -> Z
forall r. Number r => r -> r
signum Z
a Z -> Z -> Z
forall c. Multiplicative c => c -> c -> c
* Z
s,Z -> Z
forall r. Number r => r -> r
signum Z
b Z -> Z -> Z
forall c. Multiplicative c => c -> c -> c
* Z
t) where
  (Z
r,Z
s,Z
t) = (Z, Z, Z) -> (Z, Z, Z) -> (Z, Z, Z)
forall {c}.
(Num c, Abelian c, Integral c) =>
(c, c, c) -> (c, c, c) -> (c, c, c)
eval (Z -> Z
forall r. Number r => r -> r
abs Z
a,Z
1,Z
0) (Z -> Z
forall r. Number r => r -> r
abs Z
b,Z
0,Z
1)

 -- invariants for eval (r'',s'',t'') (r',s',t'):  r'' = s''*a + t''*b and r' = s'*a + t'*b 
  eval :: (c, c, c) -> (c, c, c) -> (c, c, c)
eval (c, c, c)
u             (c
0 ,c
_ ,c
_ ) = (c, c, c)
u
  eval (c
r'',c
s'',c
t'') (c
r',c
s',c
t') 
    = c
s' c -> (c, c, c) -> (c, c, c)
forall a b. a -> b -> b
`seq` c
t' c -> (c, c, c) -> (c, c, c)
forall a b. a -> b -> b
`seq` (c, c, c) -> (c, c, c) -> (c, c, c)
eval (c
r',c
s',c
t') (c
r,c
s'' c -> c -> c
forall a. Abelian a => a -> a -> a
- c
qc -> c -> c
forall c. Multiplicative c => c -> c -> c
*c
s',c
t'' c -> c -> c
forall a. Abelian a => a -> a -> a
- c
qc -> c -> c
forall c. Multiplicative c => c -> c -> c
*c
t') where (c
q,c
r) = c -> c -> (c, c)
forall a. Integral a => a -> a -> (a, a)
divMod c
r'' c
r'

--------------------------------------------------------------------------------
-- gcd -

-- | greatest common divisor.
--
-- __Properties__ For all @a@ and @b@ in 'N' holds:
--
-- (1) @gcd a b '==' gcd b a@.
--
-- (2) @gcd a b '==' 0@ if and only if @a '==' 0@ and @b '==' 0@.
--
-- (4) @gcd a 0 '==' a@.
--
-- (4) @gcd a 1 '==' 1@.
--
-- (5) @gcd a b '*' 'lcm' a b '==' a '*' b@.
gcd :: N -> N -> N
gcd :: N -> N -> N
gcd N
a N
b = N
g where (N
g,Z
_,Z
_) = Z -> Z -> (N, Z, Z)
euclid (N -> Z
forall a b. Embeddable a b => a -> b
inj N
a) (N -> Z
forall a b. Embeddable a b => a -> b
inj N
b)

--------------------------------------------------------------------------------
-- gcds -

-- | greatest common divisor of the given list.
--
-- __Note__ @gcds [] '==' 0@.
gcds :: [N] -> N
gcds :: [N] -> N
gcds = (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
gcd N
0

--------------------------------------------------------------------------------
-- lcm -

-- | least common multiple.
--
-- __Properties__ For all @a@ and @b@ in 'N' holds:
--
-- (1) @lcm a b '==' lcm b a@.
--
-- (2) @lcm a b '==' 1@ if and only if @a '==' 1@ and @b '==' 1@.
--
-- (3) @lcm a 0 '==' 0@.
--
-- (4) @lcm a 1 '==' a@.
--
-- (5) @'gcd' a b '*' lcm a b '==' a '*' b@.
lcm :: N -> N -> N
lcm :: N -> N -> N
lcm N
0 N
0 = N
0
lcm N
a N
b = (N
a N -> N -> N
forall c. Multiplicative c => c -> c -> c
* N
b) N -> N -> N
forall a. Integral a => a -> a -> a
`div` N -> N -> N
gcd N
a N
b

--------------------------------------------------------------------------------
-- lcms -

-- | least common multiple of the given list.
--
-- __Property__ @'lcms' [] '==' 1@.
lcms :: [N] -> N
lcms :: [N] -> N
lcms = (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
lcm N
1