aern2-real 0.2.15 → 0.2.15.1

raw patch · 3 files changed

+78/−2 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• aern2-real.cabal +3/−2
• changelog.md +2/−0
• src/AERN2/Continuity/Principles.hs +73/−0

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0.+-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack  name:           aern2-real-version:        0.2.15+version:        0.2.15.1 synopsis:       Real numbers as convergent sequences of intervals description:    Please see the README on GitHub at <https://github.com/michalkonecny/aern2/#readme> category:       Math@@ -28,6 +28,7 @@ library   exposed-modules:       AERN2.Complex+      AERN2.Continuity.Principles       AERN2.Real       AERN2.Real.CKleenean       AERN2.Real.Comparisons

@@ -1,6 +1,8 @@ # Change log for aern2-real  * current+* v 0.2.15.1 2024-??+  * an implementation of continuity principles for coq-aern * v 0.2.15 2023-04-11   * CanSelectCountable instance for CKleenean * v 0.2.14.1 2023-04-10

@@ -0,0 +1,73 @@+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 = maxEffortUsed 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 = maxEffortUsed addCallMonitor++maxEffortUsed :: (TVar Integer -> seq -> seq) -> (seq -> CKleenean) -> seq -> Integer+maxEffortUsed addMonitor f x =+  unsafePerformIO $ do+    maxSoFarTvar <- newTVarIO 0+    let res = f (addMonitor maxSoFarTvar x)+    let true = waitForTrue (unCSequence res)+    if isCertainlyTrue true+      then readTVarIO maxSoFarTvar+      else error "internal error in maxEffortUsed" -- this should never happen++addCallMonitor :: TVar Integer -> (Integer -> a) -> Integer -> a+addCallMonitor maxSoFarTvar x i =+  unsafePerformIO $ do+    atomically $ do+      prevMax <- readTVar maxSoFarTvar+      writeTVar maxSoFarTvar (prevMax `max` (i + 1)) -- calling x with 0 sets max to 1, etc.+    pure (x i)++addCSequenceAccessMonitor :: TVar Integer -> CSequence t -> CSequence t+addCSequenceAccessMonitor maxSoFarTvar x = CSequence (monitorSeq 1 (unCSequence x))+  where+    monitorSeq _ [] = []+    monitorSeq i (h : t) = monitorH : monitorSeq (i + 1) t+      where+        monitorH = unsafePerformIO $ do+          atomically $ writeTVar maxSoFarTvar i+          pure h++waitForTrue :: [CN Kleenean] -> CN Kleenean+waitForTrue [] = cn TrueOrFalse+waitForTrue (h : t)+  | isCertainlyTrue h = h+  | otherwise = waitForTrue t++_testNever :: Integer+_testNever = maxSeqIndexUsed (> 0) (pi - pi) -- loop forever++_test0 :: Integer+_test0 = maxSeqIndexUsed (> 0) (pi - pi + creal (1 / 1000000000)) -- 8++_test1 :: Integer+_test1 = maxIntParamUsed (\x -> CSequence (map (\n -> cn (kleenean (n > 3 * x n))) [0 ..])) (const 3) -- 11