copilot-theorem 3.7 → 3.8
raw patch · 4 files changed
+29/−24 lines, 4 filesdep ~copilot-corePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-core
API changes (from Hackage documentation)
Files
- CHANGELOG +4/−0
- copilot-theorem.cabal +4/−2
- src/Copilot/Theorem/TransSys/Cast.hs +19/−20
- src/Copilot/Theorem/TransSys/Translate.hs +2/−2
CHANGELOG view
@@ -1,3 +1,7 @@+2022-03-07+ * Version bump (3.8). (#298)+ * Mark package as uncurated to avoid modification. (#288)+ 2022-01-07 * Version bump (3.7). (#287) * Relax version contraints on what4. (#277)
copilot-theorem.cabal view
@@ -14,7 +14,7 @@ <https://copilot-language.github.io>. -version : 3.7+version : 3.8 license : BSD3 license-file : LICENSE maintainer : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -28,6 +28,8 @@ author : Jonathan Laurent +x-curation: uncurated+ library default-language : Haskell2010 hs-source-dirs : src@@ -72,7 +74,7 @@ , xml >= 1.3 && < 1.4 , what4 >= 1.1 && < 1.3 - , copilot-core >= 3.7 && < 3.8+ , copilot-core >= 3.8 && < 3.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove
src/Copilot/Theorem/TransSys/Cast.hs view
@@ -17,9 +17,8 @@ -------------------------------------------------------------------------------- import Copilot.Core as C-import Copilot.Core.Type.Equality-import Copilot.Core.Type.Dynamic +import Data.Dynamic (Dynamic(..), fromDynamic, toDyn) import GHC.Float import qualified Copilot.Theorem.TransSys.Type as K@@ -27,7 +26,7 @@ -------------------------------------------------------------------------------- -- | Synonym for a dynamic type in Copilot core.-type Dyn = Dynamic Type+type Dyn = Dynamic -- | Translation of a Copilot type into Copilot theorem's internal -- representation.@@ -67,26 +66,26 @@ _cast :: Dyn -> Maybe b instance Casted Integer where- _cast (Dynamic v tv)- | Just Refl <- tv =~= Int8 = Just $ toInteger v- | Just Refl <- tv =~= Int16 = Just $ toInteger v- | Just Refl <- tv =~= Int32 = Just $ toInteger v- | Just Refl <- tv =~= Int64 = Just $ toInteger v- | Just Refl <- tv =~= Word16 = Just $ toInteger v- | Just Refl <- tv =~= Word8 = Just $ toInteger v- | Just Refl <- tv =~= Word32 = Just $ toInteger v- | Just Refl <- tv =~= Word64 = Just $ toInteger v- | otherwise = Nothing+ _cast d+ | Just (v :: Int8) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Int16) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Int32) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Int64) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Word8) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Word16) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Word32) <- fromDynamic d = Just $ toInteger v+ | Just (v :: Word64) <- fromDynamic d = Just $ toInteger v+ | otherwise = Nothing instance Casted Bool where- _cast (Dynamic v tv)- | Just Refl <- tv =~= Bool = Just v- | otherwise = Nothing+ _cast d+ | Just (v :: Bool) <- fromDynamic d = Just v+ | otherwise = Nothing instance Casted Double where- _cast (Dynamic v tv)- | Just Refl <- tv =~= Float = Just $ float2Double v- | Just Refl <- tv =~= Double = Just v- | otherwise = Nothing+ _cast d+ | Just (v :: Float) <- fromDynamic d = Just $ float2Double v+ | Just (v :: Double) <- fromDynamic d = Just v+ | otherwise = Nothing --------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Translate.hs view
@@ -161,7 +161,7 @@ let nodeId = ncNode streamId outvar i = Var (ncMain `ncTimeAnnot` i)- buf = map (cast t . toDyn streamExprType) streamBuffer+ buf = map (cast t . toDyn) streamBuffer (e, nodeAuxVars, nodeImportedVars, nodeDependencies) <- runExprTrans t nodeId streamExpr@@ -184,7 +184,7 @@ expr :: Type t -> C.Expr t' -> Trans (Expr t) -expr t (C.Const t' v) = return $ Const t (cast t $ toDyn t' v)+expr t (C.Const _ v) = return $ Const t (cast t $ toDyn v) expr t (C.Drop _ (fromIntegral -> k :: Int) id) = do let node = ncNode id