-- | Representation of Bezout domains. That is non-Noetherian analogues of 
-- principal ideal domains. This means that all finitely generated ideals are
-- principal.
--
{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
module Algebra.Structures.BezoutDomain
  ( BezoutDomain(..)
  , propBezoutDomain
  , dividesB
  , intersectionB, intersectionBWitness
  , solveB
  ) where

import Test.QuickCheck 

import Algebra.Structures.IntegralDomain
import Algebra.Structures.Coherent
import Algebra.Structures.EuclideanDomain
import Algebra.Structures.PruferDomain
import Algebra.Structures.StronglyDiscrete
import Algebra.Matrix
import Algebra.Ideal


-------------------------------------------------------------------------------
-- | Bezout domains
-- 
-- Compute a principal ideal from another ideal. Also give witness that the
-- principal ideal is equal to the first ideal.
--
-- toPrincipal \<a_1,...,a_n> = (\<a>,u_i,v_i)
--   where
--
--   sum (u_i * a_i) = a
--
--   a_i = v_i * a
--
class IntegralDomain a => BezoutDomain a where
  toPrincipal :: Ideal a -> (Ideal a,[a],[a])

propToPrincipal :: (BezoutDomain a, Eq a) => Ideal a -> Bool
propToPrincipal = isPrincipal . (\(a,_,_) -> a) . toPrincipal

propIsSameIdeal :: (BezoutDomain a, Eq a) => Ideal a -> Bool
propIsSameIdeal (Id as) =
  let (Id [a], us, vs) = toPrincipal (Id as) 
  in a == foldr1 (<+>) (zipWith (<*>) as us) 
  && and [ ai == a <*> vi | (ai,vi) <- zip as vs ]
  && length us == l_as && length vs == l_as
  where l_as = length as

propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property
propBezoutDomain id@(Id xs) a b c = zero `notElem` xs ==> 
  if propToPrincipal id
     then if propIsSameIdeal id
             then propIntegralDomain a b c 
             else whenFail (print "propIsSameIdeal") False
     else whenFail (print "propToPrincipal") False

dividesB :: (BezoutDomain a, Eq a) => a -> a -> Bool
dividesB a b = a == x || a == neg x
    where (Id [x],_,_) = toPrincipal (Id [a,b])

-------------------------------------------------------------------------------
-- Euclidean domain -> Bezout domain

instance (EuclideanDomain a, Eq a) => BezoutDomain a where
  toPrincipal (Id [x]) = (Id [x], [one], [one])
  toPrincipal (Id xs)  = (Id [a], as, [ quotient ai a | ai <- xs ])
    where
    a  = genEuclidAlg xs
    as = genExtendedEuclidAlg xs


-------------------------------------------------------------------------------
-- | Intersection of ideals with witness.
-- 
-- If one of the ideals is the zero ideal then the intersection is the zero 
-- ideal.
-- 
intersectionBWitness :: (BezoutDomain a, Eq a) 
              => Ideal a 
              -> Ideal a 
              -> (Ideal a, [[a]], [[a]])
intersectionBWitness (Id xs) (Id ys) 
  | xs' == [] = zeroIdealWitnesses xs ys
  | ys' == [] = zeroIdealWitnesses xs ys
  | otherwise = (Id [l], [handleZero xs as], [handleZero ys bs])
  where
  xs'            = filter (/= zero) xs
  ys'            = filter (/= zero) ys

  (Id [a],us1,vs1) = toPrincipal (Id xs') 
  (Id [b],us2,vs2) = toPrincipal (Id ys')

  (Id [g],[u1,u2],[v1,v2]) = toPrincipal (Id [a,b])

  l  = g <*> v1 <*> v2
  as = map (v2 <*>) us1
  bs = map (v1 <*>) us2
  
-- Handle the zeroes specially. If the first element in xs is a zero
-- then the witness should be zero otherwise use the computed witness. 
handleZero :: (Ring a, Eq a) => [a] -> [a] -> [a]
handleZero xs [] 
  | all (==zero) xs = xs
  | otherwise       = error "intersectionB: This should be impossible"
handleZero (x:xs) (a:as) 
  | x == zero = zero : handleZero xs (a:as)
  | otherwise = a    : handleZero xs as
handleZero [] _  = error "intersectionB: This should be impossible"


-- | Intersection without witness.
intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a
intersectionB a b = (\(x,_,_) -> x) $ intersectionBWitness a b


-------------------------------------------------------------------------------
-- | Coherence of Bezout domains.
solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a
solveB x = solveWithIntersection x intersectionBWitness

-- instance (BezoutDomain r, Eq r) => Coherent r where
--   solve x = solveWithIntersection x intersectionB


-------------------------------------------------------------------------------
-- | Strongly discreteness for Bezout domains
-- 
-- Given x, compute as such that x = sum (a_i * x_i)
--
instance (BezoutDomain a, Eq a) => StronglyDiscrete a where
  member x (Id xs) | x == zero = Just (replicate (length xs) zero)
                   | otherwise = if a == g 
                                    then Just witness 
                                    else Nothing
    where
    -- (<g>, as, bs)   = <x1,...,xn>
    -- sum (a_i * x_i) = g
    -- x_i             = b_i * g
    (Id [g], as, bs) = toPrincipal (Id (filter (/= zero) xs))
    (Id [a], _,[q1,q2]) = toPrincipal (Id [x,g])
    
    -- x = qg = q (sum (ai * xi)) = sum (q * ai * xi)
    witness = handleZero xs (map (q1 <*>) as)

--------------------------------------------------------------------------------
-- | Bezout domain -> Prüfer domain
--
{-
Prufer: forall a b exists u v w t.  u+t = 1 &  ua = vb & wa = tb

We consider only domain.
We assume we have the Bezout condition: given a, b we can find g,a1,b1,c,d s.t.

a = g a1
b = g b1
1 = c a1 + d b1

We try then 

u = d b1
t = c a1

We should find v such that
a d b1 = b v
this simplifies to 
g a1 d b1 = g b1 v
and we can take 
v = a1 d
Similarly we can take 
w = b1 c

We have shown that Bezout domain -> Prufer domain.
-}
instance (BezoutDomain a, Eq a) => PruferDomain a where
  calcUVW a b | a == zero = (one,zero,zero)
              | b == zero = (zero,zero,zero)
              | otherwise = fromUVWTtoUVW (u,v,w,t)
    where
    -- Compute g, a1 and b1 such that:
    -- a = g*a1
    -- b = g*b1
    (g,[_,_],[a1,b1])  = toPrincipal (Id [a,b])
    
    -- Compute c and d such that:
    -- 1 = a1*c + a2*d
    (_,[c,d],_) = toPrincipal (Id [a1,b1])

    u = d <*> b1
    t = c <*> a1
    v = d <*> a1
    w = c <*> b1