{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}

{-|
Module      : Data.JoinSemilattice.Class.FlatMapping
Description : Refine parameters using their raw values.
Copyright   : (c) Tom Harding, 2020
License     : MIT
-}
module Data.JoinSemilattice.Class.FlatMapping where

import Data.JoinSemilattice.Class.Zipping (Zipping)
import Data.JoinSemilattice.Defined (Defined (..))
import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
import qualified Data.JoinSemilattice.Intersect as Intersect
import Data.Kind (Constraint, Type)
import Prelude hiding (unzip)

-- | Some types, such as `Intersect`, contain multiple "candidate values". This
-- function allows us to take /each/ candidate, apply a function, and then
-- union all the results. Perhaps @fanOut@ would have been a better name for
-- this function, but we use `(>>=)` to lend an intuition when we lift this
-- into `Prop` via `(Data.Propagator..>>=)`.
--
-- There's not normally much reverse-flow information here, sadly, as it
-- typically requires us to have a way to generate an "empty candidate" a la
-- 'mempty'. It's quite hard to articulate this in a succinct way, but try
-- implementing the reverse flow for 'Defined' or 'Intersect', and see what
-- happens.
class Zipping f c => FlatMapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
  flatMapR :: (c x, c y) => (Maybe (x -> f y), Maybe (f y -> x)) -> ((f x, f y) -> (f x, f y))

instance FlatMapping Defined Eq where
  flatMapR :: (Maybe (x -> Defined y), Maybe (Defined y -> x))
-> (Defined x, Defined y) -> (Defined x, Defined y)
flatMapR ( Maybe (x -> Defined y)
fs, Maybe (Defined y -> x)
gs ) ( Defined x
xs, Defined y
ys )
    = ( case Maybe (Defined y -> x)
gs of Just Defined y -> x
g  -> x -> Defined x
forall x. x -> Defined x
Exactly (Defined y -> x
g Defined y
ys)
                   Maybe (Defined y -> x)
Nothing -> Defined x
forall a. Monoid a => a
mempty

      , 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 -> Defined y)
fs of Just x -> Defined y
f  -> x -> Defined y
f x
x
                                  Maybe (x -> Defined y)
Nothing -> Defined y
forall a. Monoid a => a
mempty
      )

instance FlatMapping Intersect Intersectable where
  flatMapR :: (Maybe (x -> Intersect y), Maybe (Intersect y -> x))
-> (Intersect x, Intersect y) -> (Intersect x, Intersect y)
flatMapR ( Maybe (x -> Intersect y)
fs, Maybe (Intersect y -> x)
gs ) ( Intersect x
xs, Intersect y
ys )
    = ( case Maybe (Intersect y -> x)
gs of Just Intersect y -> x
g  -> (Intersect y -> x) -> Intersect (Intersect y) -> Intersect x
forall y x.
(Eq y, Hashable y) =>
(x -> y) -> Intersect x -> Intersect y
Intersect.map Intersect y -> x
g (Intersect y -> Intersect (Intersect y)
forall x.
(Bounded x, Enum x, Hashable x, Ord x) =>
Intersect x -> Intersect (Intersect x)
Intersect.powerSet Intersect y
ys)
                   Maybe (Intersect y -> x)
Nothing -> Intersect x
forall a. Monoid a => a
mempty

      , case Maybe (x -> Intersect y)
fs of Just x -> Intersect y
f  -> (x -> Intersect y -> Intersect y)
-> Intersect y -> Intersect x -> Intersect y
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Intersect y -> Intersect y -> Intersect y
forall x.
Intersectable x =>
Intersect x -> Intersect x -> Intersect x
Intersect.union (Intersect y -> Intersect y -> Intersect y)
-> (x -> Intersect y) -> x -> Intersect y -> Intersect y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Intersect y
f) (HashSet y -> Intersect y
forall x. HashSet x -> Intersect x
Intersect HashSet y
forall a. Monoid a => a
mempty) Intersect x
xs
                   Maybe (x -> Intersect y)
Nothing -> Intersect y
forall a. Monoid a => a
mempty
      )