{-# OPTIONS_GHC -Wno-orphans #-}
{-|
    Module      :  AERN2.Real.CKleenean
    Description :  lazy Kleenean
    Copyright   :  (c) Michal Konecny
    License     :  BSD3

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

    Lazy Kleenean, ie a sequence of Kleeneans, usually indexed by increasing precisions.
-}
module AERN2.Real.CKleenean
(
  CKleenean, CanBeCKleenean, ckleenean, CanAndOrCountable(..)
)
where

import MixedTypesNumPrelude

import qualified Numeric.CollectErrors as CN

-- import Data.Complex

import qualified Data.List as List

import AERN2.Select

import AERN2.MP

import AERN2.Real.Type
import Data.List (uncons)

type CKleenean = CSequence Kleenean

type CanBeCKleenean t = ConvertibleExactly t CKleenean

ckleenean :: (CanBeCKleenean t) => t -> CKleenean
ckleenean :: forall t. CanBeCKleenean t => t -> CKleenean
ckleenean = t -> CKleenean
forall t1 t2. ConvertibleExactly t1 t2 => t1 -> t2
convertExactly

-- IsBool CKleenean:

instance (ConvertibleExactly t Kleenean) => ConvertibleExactly t CKleenean where
  safeConvertExactly :: t -> ConvertResult CKleenean
safeConvertExactly t
b = CKleenean -> ConvertResult CKleenean
forall a b. b -> Either a b
Right (CKleenean -> ConvertResult CKleenean)
-> CKleenean -> ConvertResult CKleenean
forall a b. (a -> b) -> a -> b
$ [CN Kleenean] -> CKleenean
forall t. [CN t] -> CSequence t
CSequence ([CN Kleenean] -> CKleenean) -> [CN Kleenean] -> CKleenean
forall a b. (a -> b) -> a -> b
$ CN Kleenean -> [CN Kleenean]
forall a. a -> [a]
List.repeat (CN Kleenean -> [CN Kleenean]) -> CN Kleenean -> [CN Kleenean]
forall a b. (a -> b) -> a -> b
$ Kleenean -> CN Kleenean
forall v. v -> CN v
cn (Kleenean -> CN Kleenean) -> Kleenean -> CN Kleenean
forall a b. (a -> b) -> a -> b
$ t -> Kleenean
forall t. CanBeKleenean t => t -> Kleenean
kleenean t
b

instance (CanNeg t) => CanNeg (CSequence t) where
  type NegType (CSequence t) = CSequence (NegType t)
  negate :: CSequence t -> NegType (CSequence t)
negate = (CN t -> CN (NegType t)) -> CSequence t -> CSequence (NegType t)
forall t1 t2. (CN t1 -> CN t2) -> CSequence t1 -> CSequence t2
lift1 CN t -> CN (NegType t)
CN t -> NegType (CN t)
forall t. CanNeg t => t -> NegType t
negate

instance (CanAndOrAsymmetric t1 t2, CanTestCertainly t1, HasBools t2) => 
  CanAndOrAsymmetric (CSequence t1) (CSequence t2) 
  where
  type AndOrType (CSequence t1)  (CSequence t2) = CSequence (AndOrType t1 t2)
  and2 :: CSequence t1
-> CSequence t2 -> AndOrType (CSequence t1) (CSequence t2)
and2 = (CN t1 -> CN t2 -> CN (AndOrType t1 t2))
-> CSequence t1 -> CSequence t2 -> CSequence (AndOrType t1 t2)
forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst CN t1 -> CN t2 -> CN (AndOrType t1 t2)
CN t1 -> CN t2 -> AndOrType (CN t1) (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1
-> CSequence t2 -> AndOrType (CSequence t1) (CSequence t2)
or2 = (CN t1 -> CN t2 -> CN (AndOrType t1 t2))
-> CSequence t1 -> CSequence t2 -> CSequence (AndOrType t1 t2)
forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst CN t1 -> CN t2 -> CN (AndOrType t1 t2)
CN t1 -> CN t2 -> AndOrType (CN t1) (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance (CanAndOrAsymmetric Bool t2) => CanAndOrAsymmetric Bool (CSequence t2) where
  type AndOrType Bool  (CSequence t2) = CSequence (AndOrType Bool t2)
  and2 :: Bool -> CSequence t2 -> AndOrType Bool (CSequence t2)
and2 = (Bool -> CN t2 -> CN (AndOrType Bool t2))
-> Bool -> CSequence t2 -> CSequence (AndOrType Bool t2)
forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 Bool -> CN t2 -> CN (AndOrType Bool t2)
Bool -> CN t2 -> AndOrType Bool (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: Bool -> CSequence t2 -> AndOrType Bool (CSequence t2)
or2 = (Bool -> CN t2 -> CN (AndOrType Bool t2))
-> Bool -> CSequence t2 -> CSequence (AndOrType Bool t2)
forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 Bool -> CN t2 -> CN (AndOrType Bool t2)
Bool -> CN t2 -> AndOrType Bool (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance (CanAndOrAsymmetric Kleenean t2) => CanAndOrAsymmetric Kleenean (CSequence t2) where
  type AndOrType Kleenean  (CSequence t2) = CSequence (AndOrType Kleenean t2)
  and2 :: Kleenean -> CSequence t2 -> AndOrType Kleenean (CSequence t2)
and2 = (Kleenean -> CN t2 -> CN (AndOrType Kleenean t2))
-> Kleenean -> CSequence t2 -> CSequence (AndOrType Kleenean t2)
forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 Kleenean -> CN t2 -> CN (AndOrType Kleenean t2)
Kleenean -> CN t2 -> AndOrType Kleenean (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: Kleenean -> CSequence t2 -> AndOrType Kleenean (CSequence t2)
or2 = (Kleenean -> CN t2 -> CN (AndOrType Kleenean t2))
-> Kleenean -> CSequence t2 -> CSequence (AndOrType Kleenean t2)
forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 Kleenean -> CN t2 -> CN (AndOrType Kleenean t2)
Kleenean -> CN t2 -> AndOrType Kleenean (CN t2)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance (CanAndOrAsymmetric t1 Bool) => CanAndOrAsymmetric (CSequence t1) Bool where
  type AndOrType (CSequence t1)  Bool = CSequence (AndOrType t1 Bool)
  and2 :: CSequence t1 -> Bool -> AndOrType (CSequence t1) Bool
and2 = (CN t1 -> Bool -> CN (AndOrType t1 Bool))
-> CSequence t1 -> Bool -> CSequence (AndOrType t1 Bool)
forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> Bool -> CN (AndOrType t1 Bool)
CN t1 -> Bool -> AndOrType (CN t1) Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1 -> Bool -> AndOrType (CSequence t1) Bool
or2 = (CN t1 -> Bool -> CN (AndOrType t1 Bool))
-> CSequence t1 -> Bool -> CSequence (AndOrType t1 Bool)
forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> Bool -> CN (AndOrType t1 Bool)
CN t1 -> Bool -> AndOrType (CN t1) Bool
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2

instance (CanAndOrAsymmetric t1 Kleenean) => CanAndOrAsymmetric (CSequence t1) Kleenean where
  type AndOrType (CSequence t1)  Kleenean = CSequence (AndOrType t1 Kleenean)
  and2 :: CSequence t1 -> Kleenean -> AndOrType (CSequence t1) Kleenean
and2 = (CN t1 -> Kleenean -> CN (AndOrType t1 Kleenean))
-> CSequence t1 -> Kleenean -> CSequence (AndOrType t1 Kleenean)
forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> Kleenean -> CN (AndOrType t1 Kleenean)
CN t1 -> Kleenean -> AndOrType (CN t1) Kleenean
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1 -> Kleenean -> AndOrType (CSequence t1) Kleenean
or2 = (CN t1 -> Kleenean -> CN (AndOrType t1 Kleenean))
-> CSequence t1 -> Kleenean -> CSequence (AndOrType t1 Kleenean)
forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T CN t1 -> Kleenean -> CN (AndOrType t1 Kleenean)
CN t1 -> Kleenean -> AndOrType (CN t1) Kleenean
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2
  
class CanAndOrCountable t where
  or_countable :: (Integer -> t) -> t
  and_countable :: (Integer -> t) -> t

instance 
  CanAndOrCountable CKleenean
  where
  or_countable :: (Integer -> CKleenean) -> CKleenean
or_countable = (CN Kleenean -> CN Kleenean -> CN Kleenean)
-> (Integer -> CKleenean) -> CKleenean
lift_countable CN Kleenean -> CN Kleenean -> CN Kleenean
CN Kleenean -> CN Kleenean -> AndOrType (CN Kleenean) (CN Kleenean)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
or2
  and_countable :: (Integer -> CKleenean) -> CKleenean
and_countable = (CN Kleenean -> CN Kleenean -> CN Kleenean)
-> (Integer -> CKleenean) -> CKleenean
lift_countable CN Kleenean -> CN Kleenean -> CN Kleenean
CN Kleenean -> CN Kleenean -> AndOrType (CN Kleenean) (CN Kleenean)
forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2

lift_countable :: (CN Kleenean -> CN Kleenean -> CN Kleenean) -> (Integer -> CKleenean) -> CKleenean
lift_countable :: (CN Kleenean -> CN Kleenean -> CN Kleenean)
-> (Integer -> CKleenean) -> CKleenean
lift_countable CN Kleenean -> CN Kleenean -> CN Kleenean
op Integer -> CKleenean
s = [CN Kleenean] -> CKleenean
forall t. [CN t] -> CSequence t
CSequence ([CN Kleenean] -> CKleenean) -> [CN Kleenean] -> CKleenean
forall a b. (a -> b) -> a -> b
$ (Integer -> CN Kleenean) -> [Integer] -> [CN Kleenean]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> CN Kleenean
withFuel [Integer
0..]
    where
    withFuel :: Integer -> CN Kleenean
withFuel Integer
n = 
      -- try the n'th result of the first n CKleenean's
      -- s00  s01 ... *s0n*
      -- s10  s11 ... *s1n*
      -- ...  ...     ...
      -- sn0  sn1 ... *snn*
      ((CN Kleenean -> CN Kleenean -> CN Kleenean)
-> CN Kleenean -> [CN Kleenean] -> CN Kleenean
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CN Kleenean -> CN Kleenean -> CN Kleenean
op (Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
TrueOrFalse) ((Integer -> CN Kleenean) -> [Integer] -> [CN Kleenean]
forall a b. (a -> b) -> [a] -> [b]
map (([CN Kleenean] -> Integer -> CN Kleenean
forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
n) ([CN Kleenean] -> CN Kleenean)
-> (Integer -> [CN Kleenean]) -> Integer -> CN Kleenean
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CKleenean -> [CN Kleenean]
forall t. CSequence t -> [CN t]
unCSequence (CKleenean -> [CN Kleenean])
-> (Integer -> CKleenean) -> Integer -> [CN Kleenean]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CKleenean
s) [Integer
0..(Integer
nInteger -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
-Integer
1)]))
      CN Kleenean -> CN Kleenean -> CN Kleenean
`op`
      -- try first n results of the n'th CKleenean
      -- .  s00    s01  ...  s0n
      -- .  s10    s11  ...  s1n
      -- .  ...    ...       ...
      -- . *sn0*  *sn1* ... *snn*
      ((CN Kleenean -> CN Kleenean -> CN Kleenean)
-> CN Kleenean -> [CN Kleenean] -> CN Kleenean
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CN Kleenean -> CN Kleenean -> CN Kleenean
op (Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
TrueOrFalse) (Integer -> [CN Kleenean] -> [CN Kleenean]
forall n a. CanBeInteger n => n -> [a] -> [a]
take (Integer
nInteger -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+Integer
1) (CKleenean -> [CN Kleenean]
forall t. CSequence t -> [CN t]
unCSequence (CKleenean -> [CN Kleenean]) -> CKleenean -> [CN Kleenean]
forall a b. (a -> b) -> a -> b
$ Integer -> CKleenean
s Integer
n)))

instance CanSelect CKleenean where
  type SelectType CKleenean = CN Bool
  select :: CKleenean -> CKleenean -> SelectType CKleenean
select (CSequence [CN Kleenean]
s1) (CSequence [CN Kleenean]
s2) = [CN Kleenean] -> [CN Kleenean] -> CN Bool
forall {es} {es}.
(Monoid es, Monoid es, Eq es, Eq es, Show es, Show es,
 CanTestErrorsCertain es, CanTestErrorsCertain es,
 CanTestErrorsPresent es, CanTestErrorsPresent es) =>
[CollectErrors es Kleenean]
-> [CollectErrors es Kleenean] -> CN Bool
aux [CN Kleenean]
s1 [CN Kleenean]
s2
    where
    aux :: [CollectErrors es Kleenean]
-> [CollectErrors es Kleenean] -> CN Bool
aux (CollectErrors es Kleenean
k1 : [CollectErrors es Kleenean]
rest1) (CollectErrors es Kleenean
k2 : [CollectErrors es Kleenean]
rest2) =
      case (CollectErrors es Kleenean -> Either es Kleenean
forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CollectErrors es Kleenean
k1, CollectErrors es Kleenean -> Either es Kleenean
forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CollectErrors es Kleenean
k2) of
        (Right Kleenean
CertainTrue, Either es Kleenean
_) -> Bool -> CN Bool
forall v. v -> CN v
cn Bool
True 
        (Either es Kleenean
_, Right Kleenean
CertainTrue) -> Bool -> CN Bool
forall v. v -> CN v
cn Bool
False
        (Right Kleenean
CertainFalse, Right Kleenean
CertainFalse) -> 
          NumError -> CN Bool
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN Bool) -> NumError -> CN Bool
forall a b. (a -> b) -> a -> b
$ String -> NumError
CN.NumError String
"select: Both branches failed!"
        (Either es Kleenean, Either es Kleenean)
_ -> [CollectErrors es Kleenean]
-> [CollectErrors es Kleenean] -> CN Bool
aux [CollectErrors es Kleenean]
rest1 [CollectErrors es Kleenean]
rest2
    aux [CollectErrors es Kleenean]
_ [CollectErrors es Kleenean]
_ = NumError -> CN Bool
forall v. NumError -> CN v
CN.noValueNumErrorCertain (NumError -> CN Bool) -> NumError -> CN Bool
forall a b. (a -> b) -> a -> b
$ String -> NumError
CN.NumError String
"select: internal error"

instance CanSelectCountable CKleenean where
  type SelectCountableType CKleenean = Integer
  selectCountable :: (Integer -> CKleenean) -> SelectCountableType CKleenean
selectCountable Integer -> CKleenean
ckleeneans = 
    [(CN Kleenean, SelectCountableType CKleenean)]
-> SelectCountableType CKleenean
forall {es} {b}.
(Monoid es, Eq es, Show es, CanTestErrorsCertain es,
 CanTestErrorsPresent es) =>
[(CollectErrors es Kleenean, b)] -> b
findTrue ([(CN Kleenean, SelectCountableType CKleenean)]
 -> SelectCountableType CKleenean)
-> [(CN Kleenean, SelectCountableType CKleenean)]
-> SelectCountableType CKleenean
forall a b. (a -> b) -> a -> b
$ [[CN Kleenean]] -> [(CN Kleenean, Integer)]
forall t. [[t]] -> [(t, Integer)]
concatInfiniteLists ((Integer -> [CN Kleenean]) -> [Integer] -> [[CN Kleenean]]
forall a b. (a -> b) -> [a] -> [b]
map (CKleenean -> [CN Kleenean]
forall t. CSequence t -> [CN t]
unCSequence (CKleenean -> [CN Kleenean])
-> (Integer -> CKleenean) -> Integer -> [CN Kleenean]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CKleenean
ckleeneans) [Integer
0..])
    where
    findTrue :: [(CollectErrors es Kleenean, b)] -> b
findTrue ((CollectErrors es Kleenean
ki, b
i) : [(CollectErrors es Kleenean, b)]
rest) =
      case (CollectErrors es Kleenean -> Either es Kleenean
forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CollectErrors es Kleenean
ki) of
        Right Kleenean
CertainTrue -> b
i
        Either es Kleenean
_ -> [(CollectErrors es Kleenean, b)] -> b
findTrue [(CollectErrors es Kleenean, b)]
rest
    findTrue [] = String -> b
forall a. HasCallStack => String -> a
error String
"selectCountable: internal error"

{-|
  Take an infinite list of infinite lists and concatenate all the elements
  in a single infinite list in such a way that no element is lost.
  Moreoved, each element has the number of the original list added to it
  so that it is possible to work out which of the lists it came from.

  This function orders the elements as follows (where each item corresponds
  to one of the lists and the numbers show the positions in the result list):

  * 1 3 6 10 ... 
  * 2 5 9 ... 
  * 4 8 ...
  * 7 ...
  * ...

-}
concatInfiniteLists :: [[t]] -> [(t, Integer)]
concatInfiniteLists :: forall t. [[t]] -> [(t, Integer)]
concatInfiniteLists [[t]]
lists = 
  [[(t, Integer)]] -> [[(t, Integer)]] -> [(t, Integer)]
forall {a}. [[a]] -> [[a]] -> [a]
aux [] [[(t, Integer)]]
listsWithNumbers 
  where
  aux :: [[a]] -> [[a]] -> [a]
aux [[a]]
openedLists ([a]
nextList:[[a]]
remainingLists) =
    [a]
heads [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ ([[a]] -> [[a]] -> [a]
aux [[a]]
tails [[a]]
remainingLists)
    where
    ([a]
heads, [[a]]
tails) = [(a, [a])] -> ([a], [[a]])
forall a b. [(a, b)] -> ([a], [b])
unzip (([a] -> (a, [a])) -> [[a]] -> [(a, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (a, [a]) -> (a, [a])
forall {a}. Maybe a -> a
removeJust (Maybe (a, [a]) -> (a, [a]))
-> ([a] -> Maybe (a, [a])) -> [a] -> (a, [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe (a, [a])
forall a. [a] -> Maybe (a, [a])
uncons) ([a]
nextList[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
openedLists))
  aux [[a]]
_ [] = [a]
forall {a}. a
e
  removeJust :: Maybe a -> a
removeJust (Just a
x) = a
x
  removeJust Maybe a
Nothing = a
forall {a}. a
e
  e :: a
e = String -> a
forall a. HasCallStack => String -> a
error String
"concatInfiniteLists can be applied only to a list of infinite lists"
  listsWithNumbers :: [[(t, Integer)]]
listsWithNumbers = 
    [[t] -> [Integer] -> [(t, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [t]
list (Integer -> [Integer]
forall a. a -> [a]
repeat Integer
listNumber) 
      | ([t]
list, Integer
listNumber) <- [[t]] -> [Integer] -> [([t], Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[t]]
lists [Integer
0..]]

instance (CanUnionCNSameType t) =>
  HasIfThenElse CKleenean (CSequence t)
  where
  type IfThenElseType CKleenean (CSequence t) = (CSequence t)
  ifThenElse :: CKleenean
-> CSequence t
-> CSequence t
-> IfThenElseType CKleenean (CSequence t)
ifThenElse (CSequence [CN Kleenean]
sc) (CSequence [CN t]
s1) (CSequence [CN t]
s2) = ([CN t] -> CSequence t
forall t. [CN t] -> CSequence t
CSequence [CN t]
r)
    where
    r :: [CN t]
r = (CN Kleenean -> CN t -> CN t -> CN t)
-> [CN Kleenean] -> [CN t] -> [CN t] -> [CN t]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 CN Kleenean -> CN t -> CN t -> CN t
CN Kleenean -> CN t -> CN t -> IfThenElseType (CN Kleenean) (CN t)
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse [CN Kleenean]
sc [CN t]
s1 [CN t]
s2

instance (HasIfThenElse CKleenean t1, HasIfThenElse CKleenean t2) =>
  HasIfThenElse CKleenean (t1, t2)
  where
  type IfThenElseType CKleenean (t1, t2) = (IfThenElseType CKleenean t1, IfThenElseType CKleenean t2)
  ifThenElse :: CKleenean
-> (t1, t2) -> (t1, t2) -> IfThenElseType CKleenean (t1, t2)
ifThenElse CKleenean
s (t1
a1, t2
b1) (t1
a2, t2
b2) =
    (CKleenean -> t1 -> t1 -> IfThenElseType CKleenean t1
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t1
a1 t1
a2, CKleenean -> t2 -> t2 -> IfThenElseType CKleenean t2
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t2
b1 t2
b2)

instance (HasIfThenElse CKleenean t) =>
  HasIfThenElse CKleenean (Maybe t)
  where
  type IfThenElseType CKleenean (Maybe t) = Maybe (IfThenElseType CKleenean t)
  ifThenElse :: CKleenean
-> Maybe t -> Maybe t -> IfThenElseType CKleenean (Maybe t)
ifThenElse CKleenean
_s Maybe t
Nothing Maybe t
Nothing = Maybe (IfThenElseType CKleenean t)
IfThenElseType CKleenean (Maybe t)
forall a. Maybe a
Nothing
  ifThenElse CKleenean
s (Just t
v1) (Just t
v2) = IfThenElseType CKleenean t -> Maybe (IfThenElseType CKleenean t)
forall a. a -> Maybe a
Just (CKleenean -> t -> t -> IfThenElseType CKleenean t
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t
v1 t
v2)
  ifThenElse CKleenean
_ Maybe t
_ Maybe t
_ = 
    String -> Maybe (IfThenElseType CKleenean t)
forall a. HasCallStack => String -> a
error String
"ifThenElse with a sequence of Kleeneans and Maybe: branches clash: Just vs Nothing"

instance (HasIfThenElse CKleenean t) =>
  HasIfThenElse CKleenean [t]
  where
  type IfThenElseType CKleenean [t] = [IfThenElseType CKleenean t]
  ifThenElse :: CKleenean -> [t] -> [t] -> IfThenElseType CKleenean [t]
ifThenElse CKleenean
_s [] [] = []
  ifThenElse CKleenean
s (t
h1:[t]
t1) (t
h2:[t]
t2) = (CKleenean -> t -> t -> IfThenElseType CKleenean t
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t
h1 t
h2) IfThenElseType CKleenean t
-> [IfThenElseType CKleenean t] -> [IfThenElseType CKleenean t]
forall a. a -> [a] -> [a]
: (CKleenean -> [t] -> [t] -> IfThenElseType CKleenean [t]
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s [t]
t1 [t]
t2)
  ifThenElse CKleenean
_ [t]
_ [t]
_ = 
    String -> [IfThenElseType CKleenean t]
forall a. HasCallStack => String -> a
error String
"ifThenElse with a sequence of Kleeneans and lists: branches clash: lists of different lengths"

instance (HasIfThenElse CKleenean v) =>
  HasIfThenElse CKleenean (k -> v)
  where
  type IfThenElseType CKleenean (k -> v) = k -> (IfThenElseType CKleenean v)
  ifThenElse :: CKleenean
-> (k -> v) -> (k -> v) -> IfThenElseType CKleenean (k -> v)
ifThenElse CKleenean
s k -> v
f1 k -> v
f2 = \k
k -> CKleenean -> v -> v -> IfThenElseType CKleenean v
forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s (k -> v
f1 k
k) (k -> v
f2 k
k)