{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE PolyKinds #-}
#endif

{-# OPTIONS_GHC -Wall #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.Glb
-- Copyright   :  (c) Conal Elliott 2010
-- License     :  BSD3
-- 
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
-- 
-- Greatest lower bound
----------------------------------------------------------------------

module Data.Glb (HasGlb(..),glbBottom,flatGlb
  , GHasGlb
  , genericGlb
  ) where

import Control.Applicative (liftA2, Const, ZipList)

import GHC.Generics
import qualified Data.Typeable as Typeable
#if MIN_VERSION_base(4,7,0)
import Data.Type.Equality ((:~:))
import qualified Data.Proxy as Proxy
#endif
#if MIN_VERSION_base(4,8,0)
import qualified Data.Functor.Identity as Identity
import qualified Data.Void as Void
#endif
#if MIN_VERSION_base(4,9,0)
import qualified Data.Functor.Compose as Compose
import qualified Data.Functor.Product as Product
import qualified Data.Functor.Sum as Sum
import qualified Data.Semigroup as Semigroup
#endif
#if MIN_VERSION_base(4,10,0)
import Data.Type.Equality ((:~~:))
import qualified Type.Reflection as TR
#endif


-- | Types that support information intersection ('glb')
class HasGlb a where
  -- | Greatest lower information bound.  Intersects information available
  -- from each argument.
  glb  :: a -> a -> a
  default glb :: (Generic a, GHasGlb (Rep a)) => a -> a -> a
  glb = a -> a -> a
forall a. (Generic a, GHasGlb (Rep a)) => a -> a -> a
genericGlb

  -- | n-ary 'glb' for n > 0.  Defaults to @foldr1 glb@.  Unlike @lub@, we
  -- have no unit for 'glb'.
  glbs1 :: [a] -> a
  glbs1 = (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall a. HasGlb a => a -> a -> a
glb

-- | The 'Semigroup.Semigroup' operation takes the
-- greatest lower bound.
newtype Glb a = Glb { Glb a -> a
getGlb :: a }
  deriving (Int -> Glb a -> ShowS
[Glb a] -> ShowS
Glb a -> String
(Int -> Glb a -> ShowS)
-> (Glb a -> String) -> ([Glb a] -> ShowS) -> Show (Glb a)
forall a. Show a => Int -> Glb a -> ShowS
forall a. Show a => [Glb a] -> ShowS
forall a. Show a => Glb a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Glb a] -> ShowS
$cshowList :: forall a. Show a => [Glb a] -> ShowS
show :: Glb a -> String
$cshow :: forall a. Show a => Glb a -> String
showsPrec :: Int -> Glb a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Glb a -> ShowS
Show, ReadPrec [Glb a]
ReadPrec (Glb a)
Int -> ReadS (Glb a)
ReadS [Glb a]
(Int -> ReadS (Glb a))
-> ReadS [Glb a]
-> ReadPrec (Glb a)
-> ReadPrec [Glb a]
-> Read (Glb a)
forall a. Read a => ReadPrec [Glb a]
forall a. Read a => ReadPrec (Glb a)
forall a. Read a => Int -> ReadS (Glb a)
forall a. Read a => ReadS [Glb a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Glb a]
$creadListPrec :: forall a. Read a => ReadPrec [Glb a]
readPrec :: ReadPrec (Glb a)
$creadPrec :: forall a. Read a => ReadPrec (Glb a)
readList :: ReadS [Glb a]
$creadList :: forall a. Read a => ReadS [Glb a]
readsPrec :: Int -> ReadS (Glb a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Glb a)
Read, Glb a -> Glb a -> Bool
(Glb a -> Glb a -> Bool) -> (Glb a -> Glb a -> Bool) -> Eq (Glb a)
forall a. Eq a => Glb a -> Glb a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Glb a -> Glb a -> Bool
$c/= :: forall a. Eq a => Glb a -> Glb a -> Bool
== :: Glb a -> Glb a -> Bool
$c== :: forall a. Eq a => Glb a -> Glb a -> Bool
Eq, Eq (Glb a)
Eq (Glb a)
-> (Glb a -> Glb a -> Ordering)
-> (Glb a -> Glb a -> Bool)
-> (Glb a -> Glb a -> Bool)
-> (Glb a -> Glb a -> Bool)
-> (Glb a -> Glb a -> Bool)
-> (Glb a -> Glb a -> Glb a)
-> (Glb a -> Glb a -> Glb a)
-> Ord (Glb a)
Glb a -> Glb a -> Bool
Glb a -> Glb a -> Ordering
Glb a -> Glb a -> Glb 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 (Glb a)
forall a. Ord a => Glb a -> Glb a -> Bool
forall a. Ord a => Glb a -> Glb a -> Ordering
forall a. Ord a => Glb a -> Glb a -> Glb a
min :: Glb a -> Glb a -> Glb a
$cmin :: forall a. Ord a => Glb a -> Glb a -> Glb a
max :: Glb a -> Glb a -> Glb a
$cmax :: forall a. Ord a => Glb a -> Glb a -> Glb a
>= :: Glb a -> Glb a -> Bool
$c>= :: forall a. Ord a => Glb a -> Glb a -> Bool
> :: Glb a -> Glb a -> Bool
$c> :: forall a. Ord a => Glb a -> Glb a -> Bool
<= :: Glb a -> Glb a -> Bool
$c<= :: forall a. Ord a => Glb a -> Glb a -> Bool
< :: Glb a -> Glb a -> Bool
$c< :: forall a. Ord a => Glb a -> Glb a -> Bool
compare :: Glb a -> Glb a -> Ordering
$ccompare :: forall a. Ord a => Glb a -> Glb a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Glb a)
Ord, (forall x. Glb a -> Rep (Glb a) x)
-> (forall x. Rep (Glb a) x -> Glb a) -> Generic (Glb a)
forall x. Rep (Glb a) x -> Glb a
forall x. Glb a -> Rep (Glb a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Glb a) x -> Glb a
forall a x. Glb a -> Rep (Glb a) x
$cto :: forall a x. Rep (Glb a) x -> Glb a
$cfrom :: forall a x. Glb a -> Rep (Glb a) x
Generic)

instance HasGlb a => HasGlb (Glb a)

#if MIN_VERSION_base(4,9,0)
instance HasGlb a => Semigroup.Semigroup (Glb a) where
  Glb a
a <> :: Glb a -> Glb a -> Glb a
<> Glb a
b = a -> Glb a
forall a. a -> Glb a
Glb (a
a a -> a -> a
forall a. HasGlb a => a -> a -> a
`glb` a
b)
  stimes :: b -> Glb a -> Glb a
stimes = b -> Glb a -> Glb a
forall b a. Integral b => b -> a -> a
Semigroup.stimesIdempotent
#endif

instance Functor Glb where
  fmap :: (a -> b) -> Glb a -> Glb b
fmap a -> b
f (Glb a
a) = b -> Glb b
forall a. a -> Glb a
Glb (a -> b
f a
a)
instance Applicative Glb where
  pure :: a -> Glb a
pure = a -> Glb a
forall a. a -> Glb a
Glb
  Glb a -> b
f <*> :: Glb (a -> b) -> Glb a -> Glb b
<*> Glb a
a = b -> Glb b
forall a. a -> Glb a
Glb (a -> b
f a
a)
instance Monad Glb where
  Glb a
a >>= :: Glb a -> (a -> Glb b) -> Glb b
>>= a -> Glb b
f = a -> Glb b
f a
a

-- | Bottom for a 'glb'.  In the form of @error \"glb: bottom (\<reason\>)\"@,
-- though not really an error.
glbBottom :: String -> a
glbBottom :: String -> a
glbBottom String
msg = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"glb: bottom (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | 'glb' on flat types with equality.  Gives bottom for unequal
-- arguments.
flatGlb :: Eq a => a -> a -> a
flatGlb :: a -> a -> a
flatGlb a
a a
b | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b    = a
a
            | Bool
otherwise = String -> a
forall a. String -> a
glbBottom String
"flat & unequal"

-- Flat types:
instance HasGlb Char    where glb :: Char -> Char -> Char
glb = Char -> Char -> Char
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb Int     where glb :: Int -> Int -> Int
glb = Int -> Int -> Int
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb Integer where glb :: Integer -> Integer -> Integer
glb = Integer -> Integer -> Integer
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb Float   where glb :: Float -> Float -> Float
glb = Float -> Float -> Float
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb Double  where glb :: Double -> Double -> Double
glb = Double -> Double -> Double
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb Typeable.TypeRep where glb :: TypeRep -> TypeRep -> TypeRep
glb = TypeRep -> TypeRep -> TypeRep
forall a. Eq a => a -> a -> a
flatGlb
#if MIN_VERSION_base(4,7,0)
instance HasGlb (a :~: b) where glb :: (a :~: b) -> (a :~: b) -> a :~: b
glb = (a :~: b) -> (a :~: b) -> a :~: b
forall a. Eq a => a -> a -> a
flatGlb
#endif
#if MIN_VERSION_base(4,10,0)
instance HasGlb (a :~~: b) where glb :: (a :~~: b) -> (a :~~: b) -> a :~~: b
glb = (a :~~: b) -> (a :~~: b) -> a :~~: b
forall a. Eq a => a -> a -> a
flatGlb
instance HasGlb (TR.TypeRep a) where glb :: TypeRep a -> TypeRep a -> TypeRep a
glb = TypeRep a -> TypeRep a -> TypeRep a
forall a. Eq a => a -> a -> a
flatGlb
#endif

-- ...

-- Generic-derived instances
instance HasGlb ()
#if MIN_VERSION_base(4,7,0)
instance HasGlb (Proxy.Proxy a)
#endif
instance HasGlb Bool
instance HasGlb Ordering
instance (HasGlb a, HasGlb b) => HasGlb (Either a b)
instance HasGlb a => HasGlb (Maybe a)
instance HasGlb a => HasGlb [a]
instance HasGlb a => HasGlb (ZipList a)

instance (HasGlb a, HasGlb b) => HasGlb (a, b)
instance (HasGlb a, HasGlb b, HasGlb c) => HasGlb (a, b, c)
instance (HasGlb a, HasGlb b, HasGlb c, HasGlb d) => HasGlb (a, b, c, d)
instance (HasGlb a, HasGlb b, HasGlb c, HasGlb d, HasGlb e) => HasGlb (a, b, c, d, e)

instance HasGlb a => HasGlb (Const a b)

#if MIN_VERSION_base(4,8,0)
instance HasGlb a => HasGlb (Identity.Identity a)
instance HasGlb Void.Void
#endif

-- People often use :+: and :*: rather than Sum and Product
-- even outside of a Generic context.
instance (HasGlb (f a), HasGlb (g a)) => HasGlb ((f :*: g) a)
instance (HasGlb (f a), HasGlb (g a)) => HasGlb ((f :+: g) a)

#if MIN_VERSION_base(4,9,0)
instance HasGlb (f (g a)) => HasGlb (Compose.Compose f g a)
instance (HasGlb (f a), HasGlb (g a)) => HasGlb (Product.Product f g a)
instance (HasGlb (f a), HasGlb (g a)) => HasGlb (Sum.Sum f g a)
#endif


-- Functions
instance HasGlb b => HasGlb (a -> b) where
  glb :: (a -> b) -> (a -> b) -> a -> b
glb = (b -> b -> b) -> (a -> b) -> (a -> b) -> a -> b
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> b -> b
forall a. HasGlb a => a -> a -> a
glb

{- -- Examples

-- It takes care to check that some of these examples are computed
-- correctly, since printing stops at the first error.  For instance, ask
-- for t5!!1 .

t1,t2 :: Int
t1 = 6 `glb` 8  -- _|_
t2 = 7 `glb` 7  -- 7

t3,t4 :: (Int,Int)
t3 = (3,4) `glb` (4,5)  -- (_|_,_|_)
t4 = (3,4) `glb` (3,5)  -- (3,_|_)

t5 :: [Int]
t5 = [2,3,5] `glb` [1,3]  -- _|_:3:_|_

-}

-- | Used for generic deriving of 'HasGlb'
class GHasGlb f where
  gglb :: (Generic a, Rep a ~ f) => a -> a -> a

-- | A suitable definition of 'glb' for instances of 'Generic'.
genericGlb :: (Generic a, GHasGlb (Rep a)) => a -> a -> a
-- What makes genericGlb different from gglb? When using
-- TypeApplications, the first type argument of gglb is
-- the representation type; that's not very friendly.
genericGlb :: a -> a -> a
genericGlb a
a a
b = a -> a -> a
forall (f :: * -> *) a.
(GHasGlb f, Generic a, Rep a ~ f) =>
a -> a -> a
gglb a
a a
b

-- Newtypes don't want their outsides forced/checked, because they don't have any.
instance HasGlb x => GHasGlb (D1 ('MetaData _q _r _s 'True) (C1 _t (S1 _u (K1 _v x)))) where
  gglb :: a -> a -> a
gglb a
a a
b
    | M1 (M1 (M1 (K1 x))) <- a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
a
    , M1 (M1 (M1 (K1 y))) <- a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
b
    = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (M1 C _t (S1 _u (K1 _v x)) Any
-> M1 D ('MetaData _q _r _s 'True) (C1 _t (S1 _u (K1 _v x))) Any
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (M1 S _u (K1 _v x) Any -> M1 C _t (S1 _u (K1 _v x)) Any
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (K1 _v x Any -> M1 S _u (K1 _v x) Any
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (x -> K1 _v x Any
forall k i c (p :: k). c -> K1 i c p
K1 (x -> x -> x
forall a. HasGlb a => a -> a -> a
glb x
x x
y)))))

-- Not a newtype, but possibly a lifted unary tuple.
-- We force the outsides first in case that is so.
instance GHasGlb' f => GHasGlb (D1 ('MetaData _q _r _s 'False) f) where
  gglb :: a -> a -> a
gglb !a
a !a
b
    = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (f Any -> M1 D ('MetaData _q _r _s 'False) f Any
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f Any -> f Any -> f Any
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' f Any
ar f Any
br))
    where
      M1 f Any
ar = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
a
      M1 f Any
br = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
b

-- | Used for non-newtype 'Generic' deriving.
class GHasGlb' f where
  gglb' :: f p -> f p -> f p

instance GHasGlb' f => GHasGlb' (M1 i c f) where
  gglb' :: M1 i c f p -> M1 i c f p -> M1 i c f p
gglb' (M1 f p
l) (M1 f p
r) = f p -> M1 i c f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> f p -> f p
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' f p
l f p
r)

instance (GHasGlb' f, GHasGlb' g, HasCon f, HasCon g) => GHasGlb' (f :+: g) where
  gglb' :: (:+:) f g p -> (:+:) f g p -> (:+:) f g p
gglb' (L1 f p
l1) (L1 f p
l2) = f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f p -> f p -> f p
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' f p
l1 f p
l2)
  gglb' (R1 g p
r1) (R1 g p
r2) = g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g p -> g p -> g p
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' g p
r1 g p
r2)

  gglb' (L1 f p
l1) (R1 g p
r2) = String -> String -> (:+:) f g p
forall a. String -> String -> a
mismatchedCons (f p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName f p
l1) (g p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName g p
r2)
  gglb' (R1 g p
r1) (L1 f p
l2) = String -> String -> (:+:) f g p
forall a. String -> String -> a
mismatchedCons (g p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName g p
r1) (f p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName f p
l2)

class HasCon f where
  getConName :: f p -> String
instance Constructor i => HasCon (C1 i f) where
  getConName :: C1 i f p -> String
getConName = C1 i f p -> String
forall k (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> String
conName
instance (HasCon f, HasCon g) => HasCon (f :+: g) where
  getConName :: (:+:) f g p -> String
getConName (L1 f p
x) = f p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName f p
x
  getConName (R1 g p
x) = g p -> String
forall k (f :: k -> *) (p :: k). HasCon f => f p -> String
getConName g p
x

mismatchedCons :: String -> String -> a
mismatchedCons :: String -> String -> a
mismatchedCons String
l String
r = String -> a
forall a. String -> a
glbBottom (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
    String
"Mismatched constructors.\nThe left argument was built with "
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
",\nbut the right one was built with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."

instance (GHasGlb' f, GHasGlb' g) => GHasGlb' (f :*: g) where
  gglb' :: (:*:) f g p -> (:*:) f g p -> (:*:) f g p
gglb' (f p
l1 :*: g p
l2) (f p
r1 :*: g p
r2) =
    f p -> f p -> f p
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' f p
l1 f p
r1 f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p -> g p -> g p
forall k (f :: k -> *) (p :: k). GHasGlb' f => f p -> f p -> f p
gglb' g p
l2 g p
r2

instance GHasGlb' U1 where
  -- We pattern match strictly so we don't get
  --
  -- glb @() () undefined = ()
  gglb' :: U1 p -> U1 p -> U1 p
gglb' U1 p
U1 U1 p
U1 = U1 p
forall k (p :: k). U1 p
U1

instance GHasGlb' V1 where
#if __GLASGOW_HASKELL__ >= 708
  gglb' :: V1 p -> V1 p -> V1 p
gglb' V1 p
v V1 p
_ = case V1 p
v of
#else
  gglb' !_ _ = error "Can't happen"
#endif

instance HasGlb c => GHasGlb' (K1 i c) where
  gglb' :: K1 i c p -> K1 i c p -> K1 i c p
gglb' (K1 c
l) (K1 c
r) = c -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c p) -> c -> K1 i c p
forall a b. (a -> b) -> a -> b
$ c -> c -> c
forall a. HasGlb a => a -> a -> a
glb c
l c
r