{-# 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

type CKleenean = CSequence Kleenean

type CanBeCKleenean t = ConvertibleExactly t CKleenean

ckleenean :: (CanBeCKleenean t) => t -> CKleenean
ckleenean :: forall t. CanBeCKleenean t => t -> CKleenean
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 = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
List.repeat forall a b. (a -> b) -> a -> b
$ forall v. v -> CN v
cn forall a b. (a -> b) -> a -> b
$ 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 = forall t1 t2. (CN t1 -> CN t2) -> CSequence t1 -> CSequence t2
lift1 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 = forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1
-> CSequence t2 -> AndOrType (CSequence t1) (CSequence t2)
or2 = forall t1 t2 t3.
(CN t1 -> CN t2 -> CN t3)
-> CSequence t1 -> CSequence t2 -> CSequence t3
lift2LeftFirst 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 = forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: Bool -> CSequence t2 -> AndOrType Bool (CSequence t2)
or2 = forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 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 = forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: Kleenean -> CSequence t2 -> AndOrType Kleenean (CSequence t2)
or2 = forall t1 t2 t3.
(t1 -> CN t2 -> CN t3) -> t1 -> CSequence t2 -> CSequence t3
liftT1 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 = forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1 -> Bool -> AndOrType (CSequence t1) Bool
or2 = forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T 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 = forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T forall t1 t2.
CanAndOrAsymmetric t1 t2 =>
t1 -> t2 -> AndOrType t1 t2
and2
  or2 :: CSequence t1 -> Kleenean -> AndOrType (CSequence t1) Kleenean
or2 = forall t1 t2 t3.
(CN t1 -> t2 -> CN t3) -> CSequence t1 -> t2 -> CSequence t3
lift1T 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 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 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 = forall t. [CN t] -> CSequence t
CSequence forall a b. (a -> b) -> a -> b
$ 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*
      (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CN Kleenean -> CN Kleenean -> CN Kleenean
op (forall v. v -> CN v
cn Kleenean
TrueOrFalse) (forall a b. (a -> b) -> [a] -> [b]
map ((forall n a. CanBeInteger n => [a] -> n -> a
!! Integer
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. CSequence t -> [CN t]
unCSequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CKleenean
s) [Integer
0..(Integer
nforall 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*
      (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CN Kleenean -> CN Kleenean -> CN Kleenean
op (forall v. v -> CN v
cn Kleenean
TrueOrFalse) (forall n a. CanBeInteger n => n -> [a] -> [a]
take (Integer
nforall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+Integer
1) (forall t. CSequence t -> [CN t]
unCSequence 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) = 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 (forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CollectErrors es Kleenean
k1, forall es v. CanBeErrors es => CollectErrors es v -> Either es v
CN.toEither CollectErrors es Kleenean
k2) of
        (Right Kleenean
CertainTrue, Either es Kleenean
_) -> forall v. v -> CN v
cn Bool
True 
        (Either es Kleenean
_, Right Kleenean
CertainTrue) -> forall v. v -> CN v
cn Bool
False
        (Right Kleenean
CertainFalse, Right Kleenean
CertainFalse) -> 
          forall v. NumError -> CN v
CN.noValueNumErrorCertain 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]
_ = forall v. NumError -> CN v
CN.noValueNumErrorCertain forall a b. (a -> b) -> a -> b
$ String -> NumError
CN.NumError String
"select: internal error"

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) = (forall t. [CN t] -> CSequence t
CSequence [CN t]
r)
    where
    r :: [CN t]
r = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 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) =
    (forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t1
a1 t1
a2, 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 = forall a. Maybe a
Nothing
  ifThenElse CKleenean
s (Just t
v1) (Just t
v2) = forall a. a -> Maybe a
Just (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
_ = 
    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) = (forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s t
h1 t
h2) forall a. a -> [a] -> [a]
: (forall b t. HasIfThenElse b t => b -> t -> t -> IfThenElseType b t
ifThenElse CKleenean
s [t]
t1 [t]
t2)
  ifThenElse CKleenean
_ [t]
_ [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 -> 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)