{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Module      : Data.JoinSemilattice.Class.Mapping
Description : Lift "regular functions" over parameter types.
Copyright   : (c) Tom Harding, 2020
License     : MIT
-}
module Data.JoinSemilattice.Class.Mapping where

import Data.JoinSemilattice.Class.Merge (Merge)
import Data.JoinSemilattice.Defined (Defined (..))
import Data.JoinSemilattice.Intersect (Intersect, Intersectable)
import qualified Data.JoinSemilattice.Intersect as Intersect
import Data.Kind (Constraint, Type)

-- | Lift a relationship between two values over some type constructor.
-- Typically, this type constructor will be the parameter type.
class (forall x. c x => Merge (f x))
    => Mapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
  mapR :: (c x, c y) => (Maybe (x -> y), Maybe (y -> x)) -> ((f x, f y) -> (f x, f y))

instance Mapping Defined Eq where
  mapR :: (Maybe (x -> y), Maybe (y -> x))
-> (Defined x, Defined y) -> (Defined x, Defined y)
mapR ( Maybe (x -> y)
fs, Maybe (y -> x)
gs ) ( Defined x
xs, Defined y
ys )
    = ( case Defined y
ys of
          Defined y
Unknown   -> Defined x
forall x. Defined x
Unknown
          Defined y
Conflict  -> Defined x
forall x. Defined x
Conflict
          Exactly y
y -> case Maybe (y -> x)
gs of Just y -> x
g  -> x -> Defined x
forall x. x -> Defined x
Exactly (y -> x
g y
y)
                                  Maybe (y -> x)
Nothing -> Defined x
forall x. Defined x
Unknown

      , case Defined x
xs of
          Defined x
Unknown   -> Defined y
forall x. Defined x
Unknown
          Defined x
Conflict  -> Defined y
forall x. Defined x
Conflict
          Exactly x
x -> case Maybe (x -> y)
fs of Just x -> y
f  -> y -> Defined y
forall x. x -> Defined x
Exactly (x -> y
f x
x)
                                  Maybe (x -> y)
Nothing -> Defined y
forall x. Defined x
Unknown
      )

instance Mapping Intersect Intersectable where
  mapR :: (Maybe (x -> y), Maybe (y -> x))
-> (Intersect x, Intersect y) -> (Intersect x, Intersect y)
mapR ( Maybe (x -> y)
fs, Maybe (y -> x)
gs ) ( Intersect x
xs, Intersect y
ys )
    = ( case Maybe (y -> x)
gs of Just y -> x
g  -> (y -> x) -> Intersect y -> Intersect x
forall y x.
(Eq y, Hashable y) =>
(x -> y) -> Intersect x -> Intersect y
Intersect.map y -> x
g Intersect y
ys
                   Maybe (y -> x)
Nothing -> Intersect x
forall a. Monoid a => a
mempty

      , case Maybe (x -> y)
fs of Just x -> y
f  -> (x -> y) -> Intersect x -> Intersect y
forall y x.
(Eq y, Hashable y) =>
(x -> y) -> Intersect x -> Intersect y
Intersect.map x -> y
f Intersect x
xs
                   Maybe (x -> y)
Nothing -> Intersect y
forall a. Monoid a => a
mempty
      )