{-# OPTIONS_GHC -Wno-orphans #-}
{-|
    Module      :  AERN2.MP.Enclosure
    Description :  Enclosure operations
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

    Maintainer  :  mikkonecny@gmail.com
    Stability   :  experimental
    Portability :  portable

    Enclosure classes and operations.
-}
module AERN2.MP.Enclosure
(
  IsBall(..), ballFunctionUsingLipschitz
  , IsInterval(..), endpointL, endpointR
  , fromEndpointsAsIntervals, endpointsAsIntervals, endpointLAsInterval, endpointRAsInterval
  , intervalFunctionByEndpoints, intervalFunctionByEndpointsUpDown
  , CanPlusMinus(..), (+-)
  , CanTestContains(..), CanMapInside(..), specCanMapInside
  , CanIntersectAsymmetric(..), CanIntersect
  , CanIntersectBy, CanIntersectSameType
  , CanIntersectCNBy, CanIntersectCNSameType
  , CanUnionAsymmetric(..), CanUnion
  , CanUnionBy, CanUnionSameType
  , CanUnionCNBy, CanUnionCNSameType
  )
where

import MixedTypesNumPrelude
-- import qualified Prelude as P

-- import Control.Arrow

import Test.Hspec
import Test.QuickCheck

import qualified Numeric.CollectErrors as CN

import AERN2.Kleenean
import AERN2.MP.ErrorBound
-- import AERN2.MP.Accuracy

{- ball-specific operations -}

class IsBall t where
  type CentreType t
  centre :: t -> CentreType t
  centreAsBallAndRadius :: t-> (t,ErrorBound)
  centreAsBall :: t -> t
  centreAsBall = (t, ErrorBound) -> t
forall a b. (a, b) -> a
fst ((t, ErrorBound) -> t) -> (t -> (t, ErrorBound)) -> t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> (t, ErrorBound)
forall t. IsBall t => t -> (t, ErrorBound)
centreAsBallAndRadius
  radius :: t -> ErrorBound
  radius = (t, ErrorBound) -> ErrorBound
forall a b. (a, b) -> b
snd ((t, ErrorBound) -> ErrorBound)
-> (t -> (t, ErrorBound)) -> t -> ErrorBound
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> (t, ErrorBound)
forall t. IsBall t => t -> (t, ErrorBound)
centreAsBallAndRadius
  updateRadius :: (ErrorBound -> ErrorBound) -> (t -> t)
  {-|  When the radius of the ball is implicitly contributed to by imprecision in the centre
     (eg if the centre is a polynomial with inexact coefficients), move all that imprecision
     to the explicit radius, making the centre exact.  This may lose some information,
     but as a ball is equivalent to the original.
     For MPBall this function is pointless because it is equivalent to the identity.  -}
  makeExactCentre :: t -> t
  makeExactCentre t
v =
    (ErrorBound -> ErrorBound) -> t -> t
forall t. IsBall t => (ErrorBound -> ErrorBound) -> t -> t
updateRadius (ErrorBound -> ErrorBound -> AddType ErrorBound ErrorBound
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ErrorBound
r) t
c
    where
    (t
c, ErrorBound
r) = t -> (t, ErrorBound)
forall t. IsBall t => t -> (t, ErrorBound)
centreAsBallAndRadius t
v

instance IsBall t => IsBall (CN t) where
    type CentreType (CN t) = CN (CentreType t)
    centre :: CN t -> CentreType (CN t)
centre = (t -> CentreType t)
-> CN t -> CollectErrors NumErrors (CentreType t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> CentreType t
forall t. IsBall t => t -> CentreType t
centre
    updateRadius :: (ErrorBound -> ErrorBound) -> CN t -> CN t
updateRadius ErrorBound -> ErrorBound
f = (t -> t) -> CN t -> CN t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ErrorBound -> ErrorBound) -> t -> t
forall t. IsBall t => (ErrorBound -> ErrorBound) -> t -> t
updateRadius ErrorBound -> ErrorBound
f)
    centreAsBallAndRadius :: CN t -> (CN t, ErrorBound)
centreAsBallAndRadius = [Char] -> CN t -> (CN t, ErrorBound)
forall a. HasCallStack => [Char] -> a
error ([Char] -> CN t -> (CN t, ErrorBound))
-> [Char] -> CN t -> (CN t, ErrorBound)
forall a b. (a -> b) -> a -> b
$ [Char]
"centreAsBallAndRadius not defined for CN types"

{-|
    Computes a ball function @f@ on the centre and updating the error bound using a Lipschitz constant.
-}
ballFunctionUsingLipschitz ::
  (IsBall t, HasEqCertainly t t)
  =>
  (t -> t) {-^ @fThin@: a version of @f@ that works well on thin balls -} ->
  (t -> ErrorBound) {-^ @fLip@: a Lipschitz function of @f@ over large balls -} ->
  (t -> t) {-^ @f@ on *large* balls -}
ballFunctionUsingLipschitz :: (t -> t) -> (t -> ErrorBound) -> t -> t
ballFunctionUsingLipschitz t -> t
fThin t -> ErrorBound
fLip t
x
  | ErrorBound
r ErrorBound -> Integer -> EqCompareType ErrorBound Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
0 = t -> t
fThin t
c
  | Bool
otherwise = (ErrorBound -> ErrorBound) -> t -> t
forall t. IsBall t => (ErrorBound -> ErrorBound) -> t -> t
updateRadius (ErrorBound -> ErrorBound -> AddType ErrorBound ErrorBound
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ (t -> ErrorBound
fLip t
x)ErrorBound -> ErrorBound -> MulType ErrorBound ErrorBound
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
*ErrorBound
r) (t -> t
fThin t
c)
  where
  (t
c, ErrorBound
r) = t -> (t, ErrorBound)
forall t. IsBall t => t -> (t, ErrorBound)
centreAsBallAndRadius t
x


{- interval-specific operations -}
class IsInterval i where
  type IntervalEndpoint i
  endpoints :: i -> (IntervalEndpoint i, IntervalEndpoint i)
  fromEndpoints :: IntervalEndpoint i -> IntervalEndpoint i -> i

instance (IsInterval t) => (IsInterval (CN t)) where
    type (IntervalEndpoint (CN t)) = CN (IntervalEndpoint t)
    fromEndpoints :: IntervalEndpoint (CN t) -> IntervalEndpoint (CN t) -> CN t
fromEndpoints IntervalEndpoint (CN t)
l IntervalEndpoint (CN t)
u = (IntervalEndpoint t -> IntervalEndpoint t -> t)
-> CollectErrors NumErrors (IntervalEndpoint t)
-> CollectErrors NumErrors (IntervalEndpoint t)
-> CN t
forall es a b c.
Monoid es =>
(a -> b -> c)
-> CollectErrors es a -> CollectErrors es b -> CollectErrors es c
CN.lift2 IntervalEndpoint t -> IntervalEndpoint t -> t
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints CollectErrors NumErrors (IntervalEndpoint t)
IntervalEndpoint (CN t)
l CollectErrors NumErrors (IntervalEndpoint t)
IntervalEndpoint (CN t)
u
    endpoints :: CN t -> (IntervalEndpoint (CN t), IntervalEndpoint (CN t))
endpoints = (t -> (IntervalEndpoint t, IntervalEndpoint t))
-> CN t
-> (CollectErrors NumErrors (IntervalEndpoint t),
    CollectErrors NumErrors (IntervalEndpoint t))
forall es a c d.
Monoid es =>
(a -> (c, d))
-> CollectErrors es a -> (CollectErrors es c, CollectErrors es d)
CN.liftPair t -> (IntervalEndpoint t, IntervalEndpoint t)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints

endpointL :: (IsInterval i) => i -> IntervalEndpoint i
endpointL :: i -> IntervalEndpoint i
endpointL = (IntervalEndpoint i, IntervalEndpoint i) -> IntervalEndpoint i
forall a b. (a, b) -> a
fst ((IntervalEndpoint i, IntervalEndpoint i) -> IntervalEndpoint i)
-> (i -> (IntervalEndpoint i, IntervalEndpoint i))
-> i
-> IntervalEndpoint i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints

endpointR :: (IsInterval i) => i -> IntervalEndpoint i
endpointR :: i -> IntervalEndpoint i
endpointR = (IntervalEndpoint i, IntervalEndpoint i) -> IntervalEndpoint i
forall a b. (a, b) -> b
snd ((IntervalEndpoint i, IntervalEndpoint i) -> IntervalEndpoint i)
-> (i -> (IntervalEndpoint i, IntervalEndpoint i))
-> i
-> IntervalEndpoint i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints

endpointsAsIntervals :: 
  (IsInterval i) => i -> (i,i)
endpointsAsIntervals :: i -> (i, i)
endpointsAsIntervals i
x = (i
lI,i
rI)
  where
  lI :: i
lI = IntervalEndpoint i -> IntervalEndpoint i -> i
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints IntervalEndpoint i
l IntervalEndpoint i
l
  rI :: i
rI = IntervalEndpoint i -> IntervalEndpoint i -> i
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints IntervalEndpoint i
r IntervalEndpoint i
r
  (IntervalEndpoint i
l,IntervalEndpoint i
r) = i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints i
x

endpointLAsInterval :: (IsInterval i) => i -> i
endpointLAsInterval :: i -> i
endpointLAsInterval = (i, i) -> i
forall a b. (a, b) -> a
fst ((i, i) -> i) -> (i -> (i, i)) -> i -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> (i, i)
forall i. IsInterval i => i -> (i, i)
endpointsAsIntervals

endpointRAsInterval :: (IsInterval i) => i -> i
endpointRAsInterval :: i -> i
endpointRAsInterval = (i, i) -> i
forall a b. (a, b) -> b
snd ((i, i) -> i) -> (i -> (i, i)) -> i -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> (i, i)
forall i. IsInterval i => i -> (i, i)
endpointsAsIntervals

fromEndpointsAsIntervals :: 
  (IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
  i -> i -> i
fromEndpointsAsIntervals :: i -> i -> i
fromEndpointsAsIntervals i
l i
r = 
  IntervalEndpoint i -> IntervalEndpoint i -> i
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
IntervalEndpoint i
lMP MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
IntervalEndpoint i
uMP
  where
  lMP :: MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
lMP = IntervalEndpoint i
-> IntervalEndpoint i
-> MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
min IntervalEndpoint i
llMP IntervalEndpoint i
rlMP
  uMP :: MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
uMP = IntervalEndpoint i
-> IntervalEndpoint i
-> MinMaxType (IntervalEndpoint i) (IntervalEndpoint i)
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
max IntervalEndpoint i
luMP IntervalEndpoint i
ruMP
  (IntervalEndpoint i
llMP, IntervalEndpoint i
luMP) = i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints i
l
  (IntervalEndpoint i
rlMP, IntervalEndpoint i
ruMP) = i -> (IntervalEndpoint i, IntervalEndpoint i)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints i
r

{- plusMinus (+-) operator -}

class CanPlusMinus t1 t2 where
  type PlusMinusType t1 t2
  type PlusMinusType t1 t2 = t1
  {-| Operator for constructing or enlarging enclosures such as balls or intervals -}
  plusMinus :: t1 -> t2 -> PlusMinusType t1 t2

infixl 6  +-

{-| Operator for constructing or enlarging enclosures such as balls or intervals -}
(+-) :: (CanPlusMinus t1 t2) => t1 -> t2 -> PlusMinusType t1 t2
+- :: t1 -> t2 -> PlusMinusType t1 t2
(+-) = t1 -> t2 -> PlusMinusType t1 t2
forall t1 t2. CanPlusMinus t1 t2 => t1 -> t2 -> PlusMinusType t1 t2
plusMinus


{-|
    Computes a *monotone* ball function @f@ on intervals using the interval endpoints.
-}
intervalFunctionByEndpoints ::
  (IsInterval t, CanMinMaxSameType (IntervalEndpoint t), HasEqCertainly t t)
  =>
  (t -> t) {-^ @fThin@: a version of @f@ that works well on thin intervals -} ->
  (t -> t) {-^ @f@ on *large* intervals -}
intervalFunctionByEndpoints :: (t -> t) -> t -> t
intervalFunctionByEndpoints t -> t
fThin t
x
  | t
l t -> t -> Bool
forall a b. HasEqCertainlyAsymmetric a b => a -> b -> Bool
!==! t
u = t -> t
fThin t
l
  | Bool
otherwise = t -> t -> t
forall i.
(IsInterval i, CanMinMaxSameType (IntervalEndpoint i)) =>
i -> i -> i
fromEndpointsAsIntervals (t -> t
fThin t
l) (t -> t
fThin t
u)
  where
  (t
l,t
u) = t -> (t, t)
forall i. IsInterval i => i -> (i, i)
endpointsAsIntervals t
x

{-|
    Computes a *monotone* ball function @f@ on intervals using the interval endpoints.
-}
intervalFunctionByEndpointsUpDown ::
  (IsInterval t)
  =>
  (IntervalEndpoint t -> IntervalEndpoint t) {-^ @fDown@: a version of @f@ working on endpoints, rounded down -} ->
  (IntervalEndpoint t -> IntervalEndpoint t) {-^ @fUp@: a version of @f@ working on endpoints, rounded up -} ->
  (t -> t) {-^ @f@ on intervals rounding *outwards* -}
intervalFunctionByEndpointsUpDown :: (IntervalEndpoint t -> IntervalEndpoint t)
-> (IntervalEndpoint t -> IntervalEndpoint t) -> t -> t
intervalFunctionByEndpointsUpDown IntervalEndpoint t -> IntervalEndpoint t
fDown IntervalEndpoint t -> IntervalEndpoint t
fUp t
x =
  IntervalEndpoint t -> IntervalEndpoint t -> t
forall i.
IsInterval i =>
IntervalEndpoint i -> IntervalEndpoint i -> i
fromEndpoints (IntervalEndpoint t -> IntervalEndpoint t
fDown IntervalEndpoint t
l) (IntervalEndpoint t -> IntervalEndpoint t
fUp IntervalEndpoint t
u)
  where
  (IntervalEndpoint t
l,IntervalEndpoint t
u) = t -> (IntervalEndpoint t, IntervalEndpoint t)
forall i.
IsInterval i =>
i -> (IntervalEndpoint i, IntervalEndpoint i)
endpoints t
x


{- containment -}

class CanTestContains dom e where
  {-| Test if @e@ is inside @dom@. -}
  contains :: dom {-^ @dom@ -} -> e  {-^ @e@ -} -> Bool

class CanMapInside dom e where
  {-| Return some value contained in @dom@.
      The returned value does not have to equal the given @e@
      even if @e@ is already inside @dom@.
      All elements of @dom@ should be covered with roughly the same probability
      when calling this function for evenly distributed @e@'s.

      This function is intended mainly for generating values inside @dom@
      for randomised tests.
  -}
  mapInside :: dom {-^ @dom@ -} -> e  {-^ @e@ -} -> e

specCanMapInside ::
  (CanMapInside d e, CanTestContains d e
  , Arbitrary d, Arbitrary e, Show d, Show e)
  =>
  T d -> T e -> Spec
specCanMapInside :: T d -> T e -> Spec
specCanMapInside (T [Char]
dName :: T d) (T [Char]
eName :: T e) =
  [Char] -> Property -> SpecWith (Arg Property)
forall a.
(HasCallStack, Example a) =>
[Char] -> a -> SpecWith (Arg a)
it ([Char]
"CanMapInside " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
dName [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
eName) (Property -> SpecWith (Arg Property))
-> Property -> SpecWith (Arg Property)
forall a b. (a -> b) -> a -> b
$ do
    (d -> e -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((d -> e -> Bool) -> Property) -> (d -> e -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$
      \ (d
d :: d) (e
e :: e) ->
        d -> e -> Bool
forall dom e. CanTestContains dom e => dom -> e -> Bool
contains d
d (e -> Bool) -> e -> Bool
forall a b. (a -> b) -> a -> b
$ d -> e -> e
forall dom e. CanMapInside dom e => dom -> e -> e
mapInside d
d e
e

{- intersection -}

type CanIntersect e1 e2 =
  (CanIntersectAsymmetric e1 e2, CanIntersectAsymmetric e1 e2
  , IntersectionType e1 e2 ~ IntersectionType e2 e1)

{-| A set intersection (usually partial) -}
class CanIntersectAsymmetric e1 e2 where
  type IntersectionType e1 e2
  type IntersectionType e1 e2 = CN e1
  intersect :: e1 -> e2 -> IntersectionType e1 e2

type CanIntersectBy e1 e2 =
  (CanIntersect e1 e2, IntersectionType e1 e2 ~ e1)

type CanIntersectSameType e1 =
  (CanIntersectBy e1 e1)

type CanIntersectCNBy e1 e2 =
  (CanIntersect e1 e2, IntersectionType e1 e2 ~ CN e1)

type CanIntersectCNSameType e1 =
  (CanIntersectCNBy e1 e1)

instance
  CanIntersectAsymmetric Bool Bool
  where
  intersect :: Bool -> Bool -> IntersectionType Bool Bool
intersect Bool
b1 Bool
b2
    | Bool
b1 Bool -> Bool -> EqCompareType Bool Bool
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Bool
b2 = Bool -> CN Bool
forall v. v -> CN v
cn Bool
b1
    | Bool
otherwise =
      NumError -> CN Bool
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN Bool) -> NumError -> CN Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> NumError
CN.NumError [Char]
"empty Boolean intersection"

instance
  CanIntersectAsymmetric Kleenean Kleenean
  where
  intersect :: Kleenean -> Kleenean -> IntersectionType Kleenean Kleenean
intersect Kleenean
CertainTrue Kleenean
CertainFalse =
    NumError -> CN Kleenean
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN Kleenean) -> NumError -> CN Kleenean
forall a b. (a -> b) -> a -> b
$ [Char] -> NumError
CN.NumError [Char]
"empty Kleenean intersection"
  intersect Kleenean
CertainFalse Kleenean
CertainTrue =
    NumError -> CN Kleenean
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN Kleenean) -> NumError -> CN Kleenean
forall a b. (a -> b) -> a -> b
$ [Char] -> NumError
CN.NumError [Char]
"empty Kleenean intersection"
  intersect Kleenean
TrueOrFalse Kleenean
k2 = Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
k2
  intersect Kleenean
k1 Kleenean
_ = Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
k1

instance 
  (CanIntersectAsymmetric a b, IntersectionType a b ~ CN c)
  =>
  CanIntersectAsymmetric (CN a) (CN b) 
  where
  type IntersectionType (CN a) (CN b) = IntersectionType a b
  intersect :: CN a -> CN b -> IntersectionType (CN a) (CN b)
intersect = (a -> b -> CN c) -> CN a -> CN b -> CN c
forall a b c. (a -> b -> CN c) -> CN a -> CN b -> CN c
CN.lift2CN a -> b -> CN c
forall e1 e2.
CanIntersectAsymmetric e1 e2 =>
e1 -> e2 -> IntersectionType e1 e2
intersect

instance
  (CanIntersectAsymmetric (CN Bool) (CN b))
  =>
  CanIntersectAsymmetric Bool (CN b)
  where
  type IntersectionType Bool (CN b) = IntersectionType (CN Bool) (CN b)
  intersect :: Bool -> CN b -> IntersectionType Bool (CN b)
intersect Bool
b1 = CN Bool -> CN b -> IntersectionType (CN Bool) (CN b)
forall e1 e2.
CanIntersectAsymmetric e1 e2 =>
e1 -> e2 -> IntersectionType e1 e2
intersect (Bool -> CN Bool
forall v. v -> CN v
cn Bool
b1)

instance
  (CanIntersectAsymmetric (CN a) (CN Bool))
  =>
  CanIntersectAsymmetric (CN a) Bool
  where
  type IntersectionType (CN a) Bool = IntersectionType (CN a) (CN Bool)
  intersect :: CN a -> Bool -> IntersectionType (CN a) Bool
intersect CN a
b1 Bool
b2 = CN a -> CN Bool -> IntersectionType (CN a) (CN Bool)
forall e1 e2.
CanIntersectAsymmetric e1 e2 =>
e1 -> e2 -> IntersectionType e1 e2
intersect CN a
b1 (Bool -> CN Bool
forall v. v -> CN v
cn Bool
b2)

instance
  (CanIntersectAsymmetric (CN Kleenean) (CN b))
  =>
  CanIntersectAsymmetric Kleenean (CN b)
  where
  type IntersectionType Kleenean (CN b) = IntersectionType (CN Kleenean) (CN b)
  intersect :: Kleenean -> CN b -> IntersectionType Kleenean (CN b)
intersect Kleenean
k1 = CN Kleenean -> CN b -> IntersectionType (CN Kleenean) (CN b)
forall e1 e2.
CanIntersectAsymmetric e1 e2 =>
e1 -> e2 -> IntersectionType e1 e2
intersect (Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
k1)

instance
  (CanIntersectAsymmetric (CN a) (CN Kleenean))
  =>
  CanIntersectAsymmetric (CN a) Kleenean
  where
  type IntersectionType (CN a) Kleenean = IntersectionType (CN a) (CN Kleenean)
  intersect :: CN a -> Kleenean -> IntersectionType (CN a) Kleenean
intersect CN a
k1 Kleenean
k2 = CN a -> CN Kleenean -> IntersectionType (CN a) (CN Kleenean)
forall e1 e2.
CanIntersectAsymmetric e1 e2 =>
e1 -> e2 -> IntersectionType e1 e2
intersect CN a
k1 (Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
k2)

{- set union -}

type CanUnion e1 e2 =
  (CanUnionAsymmetric e1 e2, CanUnionAsymmetric e1 e2
  , UnionType e1 e2 ~ UnionType e2 e1)

{-| A set union (usually partial) -}
class CanUnionAsymmetric e1 e2 where
  type UnionType e1 e2
  type UnionType e1 e2 = CN e1
  union :: e1 -> e2 -> UnionType e1 e2

type CanUnionBy e1 e2 =
  (CanUnion e1 e2, UnionType e1 e2 ~ e1)

type CanUnionSameType e1 =
  (CanUnionBy e1 e1)

type CanUnionCNBy e1 e2 =
  (CanUnion e1 e2, UnionType e1 e2 ~ CN e1)

type CanUnionCNSameType e1 =
  (CanUnionCNBy e1 e1)

instance 
  (CanUnionAsymmetric a b, UnionType a b ~ CN c)
  =>
  CanUnionAsymmetric (CN a) (CN b) 
  where
  type UnionType (CN a) (CN b) = UnionType a b
  union :: CN a -> CN b -> UnionType (CN a) (CN b)
union = (a -> b -> CN c) -> CN a -> CN b -> CN c
forall a b c. (a -> b -> CN c) -> CN a -> CN b -> CN c
CN.lift2CN a -> b -> CN c
forall e1 e2.
CanUnionAsymmetric e1 e2 =>
e1 -> e2 -> UnionType e1 e2
union

instance (CanUnionSameType t, CN.CanTakeCNErrors t) =>
  HasIfThenElse Kleenean t
  where
  type IfThenElseType Kleenean t = t
  ifThenElse :: Kleenean -> t -> t -> IfThenElseType Kleenean t
ifThenElse Kleenean
CertainTrue t
e1 t
_  = t
IfThenElseType Kleenean t
e1
  ifThenElse Kleenean
CertainFalse t
_ t
e2 = t
IfThenElseType Kleenean t
e2
  ifThenElse Kleenean
TrueOrFalse t
e1 t
e2 = t
e1 t -> t -> UnionType t t
forall e1 e2.
CanUnionAsymmetric e1 e2 =>
e1 -> e2 -> UnionType e1 e2
`union` t
e2