{-# OPTIONS_GHC -Wno-orphans #-}
module AERN2.Real.CKleenean
(
CKleenean, CanBeCKleenean, ckleenean, CanAndOrCountable(..)
)
where
import MixedTypesNumPrelude
import qualified Numeric.CollectErrors as CN
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
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 =
(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`
(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"
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)