copilot-theorem 4.7 → 4.7.1

raw patch · 3 files changed

+26/−5 lines, 3 filesdep +fp-ieeedep ~copilot-coredep ~copilot-prettyprinterPVP ok

version bump matches the API change (PVP)

Dependencies added: fp-ieee

Dependency ranges changed: copilot-core, copilot-prettyprinter

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot-theorem.cabal +4/−3
• src/Copilot/Theorem/What4.hs +17/−2

@@ -1,3 +1,8 @@+2026-05-07+        * Version bump (4.7.1). (#730)+        * Handle special Float values correctly for counterexamples. (#697)+        * Update examples to compile with copilot-theorem >= 3.0. (#692)+ 2026-03-07         * Version bump (4.7). (#714) 

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 4.7+version                   : 4.7.1 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -51,6 +51,7 @@                           , containers            >= 0.4 && < 0.9                           , data-default          >= 0.7 && < 0.9                           , directory             >= 1.3 && < 1.4+                          , fp-ieee               >= 0.1 && < 0.2                           , libBF                 >= 0.6.2 && < 0.7                           , mtl                   >= 2.0 && < 2.4                           , panic                 >= 0.4.0 && < 0.5@@ -62,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.8 -                          , copilot-core          >= 4.7 && < 4.8-                          , copilot-prettyprinter >= 4.7 && < 4.8+                          , copilot-core          >= 4.7.1 && < 4.8+                          , copilot-prettyprinter >= 4.7.1 && < 4.8    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

@@ -77,8 +77,9 @@ import Data.Parameterized.Nonce import Data.Parameterized.Some import qualified Data.Parameterized.Vector as V-import GHC.Float (castWord32ToFloat, castWord64ToDouble)+import GHC.Float (castWord32ToFloat, castWord64ToDouble, double2Float) import LibBF (BigFloat, bfToDouble, pattern NearEven)+import Numeric.Floating.IEEE.NaN (getPayload, isSignaling, setPayload, setPayloadSignaling) import qualified Panic as Panic  import Copilot.Theorem.What4.Translate@@ -707,7 +708,7 @@   XFloat e ->     Some . CopilotValue CT.Float <$>       iFloatGroundEval WFP.SingleFloatRepr e-                       (realToFrac . fst . bfToDouble NearEven)+                       (nanSafeDoubleToFloat . fst . bfToDouble NearEven)                        fromRational                        (castWord32ToFloat . fromInteger . BV.asUnsigned)   XDouble e ->@@ -757,3 +758,17 @@         WB.FloatIEEERepr          -> ieeeK <$> WG.groundEval ge e         WB.FloatRealRepr          -> realK <$> WG.groundEval ge e         WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e++    -- Convert a Double to a Float. This function takes care to preserve+    -- special floating-point values, such as negative zero, infinity, and NaN+    -- values.+    nanSafeDoubleToFloat :: Double -> Float+    nanSafeDoubleToFloat x+        -- double2Float does not preserve the payloads of NaN values, so we+        -- include a special case for translating NaNs.+        | isNaN x && isSignaling x = setPayloadSignaling payload+        | isNaN x                  = setPayload payload+        | otherwise                = double2Float x+      where+        payload :: Float+        payload = double2Float $ getPayload x