copilot-theorem 3.2.1 → 3.3
raw patch · 5 files changed
+33/−28 lines, 5 filesdep +libBFdep ~copilot-coredep ~what4PVP ok
version bump matches the API change (PVP)
Dependencies added: libBF
Dependency ranges changed: copilot-core, what4
API changes (from Hackage documentation)
Files
- CHANGELOG +8/−4
- README.md +1/−1
- copilot-theorem.cabal +5/−4
- src/Copilot/Theorem/Misc/Error.hs +0/−4
- src/Copilot/Theorem/What4.hs +19/−15
CHANGELOG view
@@ -1,12 +1,16 @@+2021-05-07+ * Version bump (3.3). (#217).+ * Adjust contraints on version of what4. (#90).+ 2021-03-07- * Version bump (3.2.1). (#15).- * Completed the documentation. (#11, #14).+ * Version bump (3.2.1). (#92).+ * Completed the documentation. (#95, #93). 2020-12-06 * Version bump (3.2). * Update description, bug-reports and homepage field in cabal file- (#8).+ (#97). 2019-11-22 Ivan Perez <ivan.perez@nianet.org> * Version bump (3.1).- * Remove ExternFun (#6).+ * Remove ExternFun (#99).
README.md view
@@ -1,4 +1,4 @@-[](https://travis-ci.org/Copilot-Language/copilot-theorem)+[](https://travis-ci.org/Copilot-Language/copilot) # Copilot Theorem
copilot-theorem.cabal view
@@ -14,12 +14,12 @@ <https://copilot-language.github.io>. -version : 3.2.1+version : 3.3 license : BSD3 license-file : LICENSE maintainer : jonathan.laurent@ens.fr homepage : https://copilot-language.github.io-bug-reports : https://github.com/Copilot-Language/copilot-theorem/issues+bug-reports : https://github.com/Copilot-Language/copilot/issues stability : Experimental category : Language, Embedded build-type : Simple@@ -60,6 +60,7 @@ , data-default >= 0.7 && < 0.8 , directory >= 1.3 && < 1.4 , filepath >= 1.4.2 && < 1.5+ , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.3 , panic >= 0.4.0 && < 0.5 , parsec >= 2.0 && < 3.2@@ -69,9 +70,9 @@ , random >= 1.1 && < 1.2 , transformers >= 0.5 && < 0.6 , xml >= 1.3 && < 1.4- , what4 >= 1.0 && < 1.1+ , what4 >= 1.1 && < 1.2 - , copilot-core >= 3.2.1 && < 3.3+ , copilot-core >= 3.3 && < 3.4 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove
src/Copilot/Theorem/Misc/Error.hs view
@@ -7,7 +7,6 @@ ( badUse , impossible , impossible_- , notHandled , fatal ) where @@ -31,9 +30,6 @@ -- | Report an error due to a bug in Copilot. impossible_ :: a impossible_ = error $ errorHeader ++ "Unexpected internal error"--notHandled :: String -> a-notHandled s = error $ errorHeader ++ "Not handled : " ++ s -- | Report an unrecoverable error (e.g., incorrect format). fatal :: String -> a
src/Copilot/Theorem/What4.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -90,7 +91,10 @@ import Data.Parameterized.SymbolRepr import qualified Data.Parameterized.Vector as V import Data.Word-import GHC.Float (castWord32ToFloat, castWord64ToDouble)+import LibBF ( bfToDouble+ , bfFromDouble+ , bfPosZero+ , pattern NearEven ) import GHC.TypeNats (KnownNat) import qualified Panic as Panic @@ -215,11 +219,11 @@ -- stateful value. streams :: Map.Map CE.Id CS.Stream, -- | Binary power operator, represented as an uninterpreted function.- pow :: WB.ExprSymFn t (WB.Expr t)+ pow :: WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType, -- | Binary logarithm operator, represented as an uninterpreted function.- logb :: WB.ExprSymFn t (WB.Expr t)+ logb :: WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType }@@ -239,7 +243,7 @@ instance Panic.PanicComponent CopilotWhat4 where panicComponentName _ = "Copilot/What4 translation"- panicComponentIssues _ = "https://github.com/Copilot-Language/copilot-theorem/issues"+ panicComponentIssues _ = "https://github.com/Copilot-Language/copilot/issues" {-# NOINLINE Panic.panicComponentRevision #-} panicComponentRevision = $(Panic.useGitRevision)@@ -295,9 +299,9 @@ XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e XFloat e ->- Some . CopilotValue CT.Float . castWord32ToFloat . fromBV <$> WG.groundEval ge e+ Some . CopilotValue CT.Float . realToFrac . fst . bfToDouble NearEven <$> WG.groundEval ge e XDouble e ->- Some . CopilotValue CT.Double . castWord64ToDouble . fromBV <$> WG.groundEval ge e+ Some . CopilotValue CT.Double . fst . bfToDouble NearEven <$> WG.groundEval ge e _ -> error "valFromExpr unhandled case" where fromBV :: forall a w . Num a => BV.BV w -> a fromBV = fromInteger . BV.asUnsigned@@ -351,8 +355,8 @@ CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a) CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a) CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a)- CT.Float -> XFloat <$> WI.floatLit sym knownRepr (toRational a)- CT.Double -> XDouble <$> WI.floatLit sym knownRepr (toRational a)+ CT.Float -> XFloat <$> WI.floatLit sym knownRepr (bfFromDouble (realToFrac a))+ CT.Double -> XDouble <$> WI.floatLit sym knownRepr (bfFromDouble a) CT.Array tp -> do elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a) Just (Some n) <- return $ someNat (length elts)@@ -560,7 +564,7 @@ neg_e <- WI.bvSub sym zero e WI.bvIte sym e_neg neg_e e fpAbs :: FPOp1 fpp t- fpAbs e = do zero <- WI.floatLit sym knownRepr 0+ fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero e_neg <- WI.floatLt sym e zero neg_e <- WI.floatSub sym fpRM zero e WI.floatIte sym e_neg neg_e e@@ -574,16 +578,16 @@ t <- WI.bvIte sym e_neg neg_one pos_one WI.bvIte sym e_zero zero t fpSign :: FPOp1 fpp t- fpSign e = do zero <- WI.floatLit sym knownRepr 0- neg_one <- WI.floatLit sym knownRepr (-1)- pos_one <- WI.floatLit sym knownRepr 1+ fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero+ neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0))+ pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0) e_zero <- WI.floatEq sym e zero e_neg <- WI.floatLt sym e zero t <- WI.floatIte sym e_neg neg_one pos_one WI.floatIte sym e_zero zero t (CE.Recip _, xe) -> fpOp recip xe where recip :: FPOp1 fpp t- recip e = do one <- WI.floatLit sym knownRepr 1+ recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0) WI.floatDiv sym fpRM one e (CE.Exp _, xe) -> realOp (WI.realExp sym) xe (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe@@ -708,11 +712,11 @@ translateOp2 :: forall t st fs a b c . WB.ExprBuilder t st fs- -> (WB.ExprSymFn t (WB.Expr t)+ -> (WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType) -- ^ Pow function- -> (WB.ExprSymFn t (WB.Expr t)+ -> (WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType) -- ^ Logb function