module AERN2.Continuity.Principles
  ( maxSeqIndexUsed,
    maxIntParamUsed,
  )
where

import AERN2.Kleenean (Kleenean (..), kleenean)
import AERN2.Real (pi)
import AERN2.Real.CKleenean (CKleenean)
import AERN2.Real.Comparisons ()
import AERN2.Real.Type (CSequence (..), creal)
import GHC.Conc (TVar, atomically, newTVarIO, readTVar, readTVarIO, writeTVar)
import GHC.IO (unsafePerformIO)
import MixedTypesNumPrelude

-- |
--    Apply a predicate to a `CSequence`, assuming it returns True
--    and return the largest index in the sequence that was accessed during the computation.
--    Index 0 means that the sequence was not accessed at all,
--    1 means the first element was accessed, etc.
maxSeqIndexUsed :: (CSequence t -> CKleenean) -> CSequence t -> Integer
maxSeqIndexUsed :: forall t.
(CSequence t -> CSequence Kleenean) -> CSequence t -> Integer
maxSeqIndexUsed = (TVar Integer -> CSequence t -> CSequence t)
-> (CSequence t -> CSequence Kleenean) -> CSequence t -> Integer
forall seq.
(TVar Integer -> seq -> seq)
-> (seq -> CSequence Kleenean) -> seq -> Integer
maxEffortUsed TVar Integer -> CSequence t -> CSequence t
forall t. TVar Integer -> CSequence t -> CSequence t
addCSequenceAccessMonitor

-- |
--    Apply a predicate to a convergent sequence, assuming it returns True
--    and return the largest index in the sequence that was accessed during the computation.
--    Index 0 means that the sequence was not accessed at all,
--    1 means the sequence was called only with index 0, etc.
maxIntParamUsed :: ((Integer -> t) -> CKleenean) -> (Integer -> t) -> Integer
maxIntParamUsed :: forall t.
((Integer -> t) -> CSequence Kleenean) -> (Integer -> t) -> Integer
maxIntParamUsed = (TVar Integer -> (Integer -> t) -> Integer -> t)
-> ((Integer -> t) -> CSequence Kleenean)
-> (Integer -> t)
-> Integer
forall seq.
(TVar Integer -> seq -> seq)
-> (seq -> CSequence Kleenean) -> seq -> Integer
maxEffortUsed TVar Integer -> (Integer -> t) -> Integer -> t
forall a. TVar Integer -> (Integer -> a) -> Integer -> a
addCallMonitor

maxEffortUsed :: (TVar Integer -> seq -> seq) -> (seq -> CKleenean) -> seq -> Integer
maxEffortUsed :: forall seq.
(TVar Integer -> seq -> seq)
-> (seq -> CSequence Kleenean) -> seq -> Integer
maxEffortUsed TVar Integer -> seq -> seq
addMonitor seq -> CSequence Kleenean
f seq
x =
  IO Integer -> Integer
forall a. IO a -> a
unsafePerformIO (IO Integer -> Integer) -> IO Integer -> Integer
forall a b. (a -> b) -> a -> b
$ do
    TVar Integer
maxSoFarTvar <- Integer -> IO (TVar Integer)
forall a. a -> IO (TVar a)
newTVarIO Integer
0
    let res :: CSequence Kleenean
res = seq -> CSequence Kleenean
f (TVar Integer -> seq -> seq
addMonitor TVar Integer
maxSoFarTvar seq
x)
    let true :: CN Kleenean
true = [CN Kleenean] -> CN Kleenean
waitForTrue (CSequence Kleenean -> [CN Kleenean]
forall t. CSequence t -> [CN t]
unCSequence CSequence Kleenean
res)
    if CN Kleenean -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue CN Kleenean
true
      then TVar Integer -> IO Integer
forall a. TVar a -> IO a
readTVarIO TVar Integer
maxSoFarTvar
      else [Char] -> IO Integer
forall a. HasCallStack => [Char] -> a
error [Char]
"internal error in maxEffortUsed" -- this should never happen

addCallMonitor :: TVar Integer -> (Integer -> a) -> Integer -> a
addCallMonitor :: forall a. TVar Integer -> (Integer -> a) -> Integer -> a
addCallMonitor TVar Integer
maxSoFarTvar Integer -> a
x Integer
i =
  IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ do
    STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      Integer
prevMax <- TVar Integer -> STM Integer
forall a. TVar a -> STM a
readTVar TVar Integer
maxSoFarTvar
      TVar Integer -> Integer -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar Integer
maxSoFarTvar (Integer
prevMax Integer -> Integer -> MinMaxType Integer Integer
forall t1 t2.
CanMinMaxAsymmetric t1 t2 =>
t1 -> t2 -> MinMaxType t1 t2
`max` (Integer
i Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1)) -- calling x with 0 sets max to 1, etc.
    a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> a
x Integer
i)

addCSequenceAccessMonitor :: TVar Integer -> CSequence t -> CSequence t
addCSequenceAccessMonitor :: forall t. TVar Integer -> CSequence t -> CSequence t
addCSequenceAccessMonitor TVar Integer
maxSoFarTvar CSequence t
x = [CN t] -> CSequence t
forall t. [CN t] -> CSequence t
CSequence (Integer -> [CN t] -> [CN t]
monitorSeq Integer
1 (CSequence t -> [CN t]
forall t. CSequence t -> [CN t]
unCSequence CSequence t
x))
  where
    monitorSeq :: Integer -> [CN t] -> [CN t]
monitorSeq Integer
_ [] = []
    monitorSeq Integer
i (CN t
h : [CN t]
t) = CN t
monitorH CN t -> [CN t] -> [CN t]
forall a. a -> [a] -> [a]
: Integer -> [CN t] -> [CN t]
monitorSeq (Integer
i Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) [CN t]
t
      where
        monitorH :: CN t
monitorH = IO (CN t) -> CN t
forall a. IO a -> a
unsafePerformIO (IO (CN t) -> CN t) -> IO (CN t) -> CN t
forall a b. (a -> b) -> a -> b
$ do
          STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar Integer -> Integer -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar Integer
maxSoFarTvar Integer
i
          CN t -> IO (CN t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CN t
h

waitForTrue :: [CN Kleenean] -> CN Kleenean
waitForTrue :: [CN Kleenean] -> CN Kleenean
waitForTrue [] = Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
TrueOrFalse
waitForTrue (CN Kleenean
h : [CN Kleenean]
t)
  | CN Kleenean -> Bool
forall t. CanTestCertainly t => t -> Bool
isCertainlyTrue CN Kleenean
h = CN Kleenean
h
  | Bool
otherwise = [CN Kleenean] -> CN Kleenean
waitForTrue [CN Kleenean]
t

_testNever :: Integer
_testNever :: Integer
_testNever = (CSequence MPBall -> CSequence Kleenean)
-> CSequence MPBall -> Integer
forall t.
(CSequence t -> CSequence Kleenean) -> CSequence t -> Integer
maxSeqIndexUsed (CSequence MPBall
-> Integer -> OrderCompareType (CSequence MPBall) Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Integer
0) (CSequence MPBall
pi CSequence MPBall
-> CSequence MPBall
-> SubType (CSequence MPBall) (CSequence MPBall)
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- CSequence MPBall
pi) -- loop forever

_test0 :: Integer
_test0 :: Integer
_test0 = (CSequence MPBall -> CSequence Kleenean)
-> CSequence MPBall -> Integer
forall t.
(CSequence t -> CSequence Kleenean) -> CSequence t -> Integer
maxSeqIndexUsed (CSequence MPBall
-> Integer -> OrderCompareType (CSequence MPBall) Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Integer
0) (CSequence MPBall
pi CSequence MPBall
-> CSequence MPBall
-> SubType (CSequence MPBall) (CSequence MPBall)
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- CSequence MPBall
pi CSequence MPBall
-> CSequence MPBall
-> AddType (CSequence MPBall) (CSequence MPBall)
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Rational -> CSequence MPBall
forall t. CanBeCReal t => t -> CSequence MPBall
creal (Integer
1 Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Integer
1000000000)) -- 8

_test1 :: Integer
_test1 :: Integer
_test1 = ((Integer -> Integer) -> CSequence Kleenean)
-> (Integer -> Integer) -> Integer
forall t.
((Integer -> t) -> CSequence Kleenean) -> (Integer -> t) -> Integer
maxIntParamUsed (\Integer -> Integer
x -> [CN Kleenean] -> CSequence Kleenean
forall t. [CN t] -> CSequence t
CSequence ((Integer -> CN Kleenean) -> [Integer] -> [CN Kleenean]
forall a b. (a -> b) -> [a] -> [b]
map (\Integer
n -> Kleenean -> CN Kleenean
forall v. v -> CN v
cn (OrderCompareType Integer Integer -> Kleenean
forall t. CanBeKleenean t => t -> Kleenean
kleenean (Integer
n Integer -> Integer -> OrderCompareType Integer Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Integer
3 Integer -> Integer -> MulType Integer Integer
forall t1 t2. CanMulAsymmetric t1 t2 => t1 -> t2 -> MulType t1 t2
* Integer -> Integer
x Integer
n))) [Integer
0 ..])) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const Integer
3) -- 11