{-# 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 = 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 CanSelectCountable CKleenean where
  type SelectCountableType CKleenean = Integer
  selectCountable :: (Integer -> CKleenean) -> SelectCountableType CKleenean
selectCountable Integer -> CKleenean
ckleeneans = 
    forall {es} {b}.
(Monoid es, Eq es, Show es, CanTestErrorsCertain es,
 CanTestErrorsPresent es) =>
[(CollectErrors es Kleenean, b)] -> b
findTrue forall a b. (a -> b) -> a -> b
$ forall t. [[t]] -> [(t, Integer)]
concatInfiniteLists (forall a b. (a -> b) -> [a] -> [b]
map (forall t. CSequence t -> [CN t]
unCSequence 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 (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 [] = 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 = 
  forall {a}. [[a]] -> [[a]] -> [a]
aux [] [[(t, Integer)]]
listsWithNumbers 
  where
  aux :: [[a]] -> [[a]] -> [a]
aux [[a]]
openedLists ([a]
nextList:[[a]]
remainingLists) =
    [a]
heads forall a. [a] -> [a] -> [a]
++ ([[a]] -> [[a]] -> [a]
aux [[a]]
tails [[a]]
remainingLists)
    where
    ([a]
heads, [[a]]
tails) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. Maybe a -> a
removeJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (a, [a])
uncons) ([a]
nextListforall a. a -> [a] -> [a]
:[[a]]
openedLists))
  aux [[a]]
_ [] = forall {a}. a
e
  removeJust :: Maybe a -> a
removeJust (Just a
x) = a
x
  removeJust Maybe a
Nothing = forall {a}. a
e
  e :: a
e = forall a. HasCallStack => String -> a
error String
"concatInfiniteLists can be applied only to a list of infinite lists"
  listsWithNumbers :: [[(t, Integer)]]
listsWithNumbers = 
    [forall a b. [a] -> [b] -> [(a, b)]
zip [t]
list (forall a. a -> [a]
repeat Integer
listNumber) 
      | ([t]
list, Integer
listNumber) <- 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) = (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)