content: {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedLists #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE UndecidableInstances #-}
  module Data.GaloisConnection where
  
  import           Data.Hashable
  import           Data.Order
  import qualified Data.Abstract.Powerset as Abs
  import qualified Data.Concrete.Powerset as Con
  import qualified Data.Concrete.Error as Con
  import qualified Data.Abstract.Except as Abs
  import qualified Data.Abstract.Failure as AbsF
  import qualified Data.Concrete.Boolean as Con
  import qualified Data.Abstract.Boolean as Abs
  import qualified Data.Abstract.Interval as Abs
  import           Data.Identifiable
  
  -- | A galois connection consisting of an abstraction function alpha
  -- and a concretization function gamma between two pre-ordered sets
  -- has to satisfy forall x,y. alpha x ⊑ y iff x ⊑ gamma y
  class (PreOrd x, PreOrd y) => Galois x y where
    alpha :: x -> y
    gamma :: y -> x
  
  instance (Galois x x', Galois y y') => Galois (x,y) (x',y') where
    alpha (x,y) = (alpha x, alpha y)
    gamma (x',y') = (gamma x', gamma y')
  
  instance (Identifiable (x,y), Galois (Con.Pow x) x', Galois (Con.Pow y) y')
    => Galois (Con.Pow (x,y)) (x',y') where
    alpha m = (alpha (fst <$> m),alpha (snd <$> m))
    gamma m = Con.cartesian (gamma (fst m),gamma (snd m))
  
  instance Galois (Con.Pow Con.Bool) Abs.Bool where
    alpha = lifted $ \b -> case b of
      Con.True -> Abs.True
      Con.False -> Abs.False
    gamma x = case x of
      Abs.Top   -> [Con.True, Con.False]
      Abs.True  -> [Con.True]
      Abs.False -> [Con.False]
  
  instance (Hashable a, Ord a, Enum a) => Galois (Con.Pow a) (Abs.Interval a) where
    alpha x = Abs.Interval (minimum x) (maximum x)
    gamma (Abs.Interval x y) = [x..y]
  
  instance (Complete a', Hashable a, Galois (Con.Pow a) a', Hashable b, Complete b', Galois (Con.Pow b) b')
      => Galois (Con.Pow (Con.Error a b)) (Abs.Except a' b') where
    alpha = lifted $ \e -> case e of
      Con.Fail x -> Abs.Fail (alphaSing x)
      Con.Success y -> Abs.Success (alphaSing y)
    gamma = error "noncomputable"
  
  instance (Hashable e, Hashable b, Complete b', Galois (Con.Pow b) b')
      => Galois (Con.Pow (Con.Error e b)) (AbsF.Failure e b') where
    alpha = lifted $ \e -> case e of
      Con.Fail x -> AbsF.Fail x
      Con.Success y -> AbsF.Success (alphaSing y)
    gamma = error "noncomputable"
  
  instance (Hashable a, Complete a', Galois (Con.Pow a) a')
      => Galois (Con.Pow (Maybe a)) (Maybe a') where
    alpha = lifted $ \e -> case e of
      Just x -> Just (alphaSing x)
      Nothing -> Nothing
    gamma = error "noncomputable"
  
  instance Galois (Con.Pow a) a' => Galois (Con.Pow a) (Abs.Pow a') where
    alpha x = Abs.fromFoldable (fmap alphaSing x)
    gamma y' = Con.unions (Con.fromFoldable (fmap gamma y'))
  
  instance Galois (Con.Pow ()) () where
    alpha = const ()
    gamma = const $ Con.singleton ()
  
  alphaSing :: Galois (Con.Pow x) x' => x -> x'
  alphaSing = alpha . (return :: x -> Con.Pow x)
  
  lifted :: Complete y => (x -> y) -> Con.Pow x -> y
  lifted lift = foldr1 (⊔) . fmap lift
  