diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -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 * Version bump (3.1). - * Remove ExternFun (#6). + * Remove ExternFun (#99). diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -[![Build Status](https://travis-ci.org/Copilot-Language/copilot-theorem.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-theorem) +[![Build Status](https://travis-ci.org/Copilot-Language/copilot.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot) # Copilot Theorem diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal --- a/copilot-theorem.cabal +++ b/copilot-theorem.cabal @@ -14,12 +14,12 @@ . -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 diff --git a/src/Copilot/Theorem/Misc/Error.hs b/src/Copilot/Theorem/Misc/Error.hs --- a/src/Copilot/Theorem/Misc/Error.hs +++ b/src/Copilot/Theorem/Misc/Error.hs @@ -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 diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs --- a/src/Copilot/Theorem/What4.hs +++ b/src/Copilot/Theorem/What4.hs @@ -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