copilot-sbv 0.6 → 2.1.1
raw patch · 4 files changed
+20/−23 lines, 4 filesdep ~basedep ~copilot-coredep ~sbvPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, copilot-core, sbv
API changes (from Hackage documentation)
- Copilot.Compile.SBV.Queue: lookahead :: (HasSignAndSize a, SymWord a) => DropIdx -> [SBV a] -> SBV QueueSize -> SBV a
+ Copilot.Compile.SBV.Queue: lookahead :: SymWord a => DropIdx -> [SBV a] -> SBV QueueSize -> SBV a
Files
- copilot-sbv.cabal +9/−9
- src/Copilot/Compile/SBV/Copilot2SBV.hs +2/−2
- src/Copilot/Compile/SBV/Queue.hs +2/−4
- src/Copilot/Compile/SBV/Witness.hs +7/−8
copilot-sbv.cabal view
@@ -1,16 +1,16 @@ cabal-version : >= 1.10 name : copilot-sbv-version : 0.6+version : 2.1.1 synopsis : A compiler for CoPilot targeting SBV.-description : +description : The Copilot back-end targeting SBV <http://hackage.haskell.org/package/sbv>.- . + . Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at- <https://github.com/niswegmann/copilot-discussion>. - . + <https://github.com/niswegmann/copilot-discussion>.+ . Examples are available at <https://github.com/leepike/Copilot/tree/master/Examples>. @@ -38,11 +38,11 @@ ghc-options : -Wall -fwarn-tabs ghc-prof-options : -auto-all -caf-all - build-depends : sbv >= 1.0 && <= 1.3- , base >= 4.3 && < 5+ build-depends : sbv >= 2.4+ , base >= 4.0 && <= 5.0 , containers >= 0.4- , copilot-core- , pretty >= 1 + , copilot-core >= 0.2.4+ , pretty >= 1 , filepath >= 1.1 exposed-modules : Copilot.Compile.SBV
src/Copilot/Compile/SBV/Copilot2SBV.hs view
@@ -252,9 +252,9 @@ Gt t -> case W.ordInst t of W.OrdInst -> (S..>) Div t -> case W.divInst t of W.BVDivisibleInst -> - \x y -> fst (S.bvQuotRem x y)+ \x y -> fst (S.sQuotRem x y) Mod t -> case W.divInst t of W.BVDivisibleInst -> - \x y -> snd (S.bvQuotRem x y)+ \x y -> snd (S.sQuotRem x y) BwAnd t -> case W.bitsInst t of W.BitsInst -> (S..&.) BwOr t -> case W.bitsInst t of W.BitsInst -> (S..|.)
src/Copilot/Compile/SBV/Queue.hs view
@@ -12,7 +12,6 @@ import Prelude hiding (id, rem) import qualified Data.SBV as S-import qualified Data.SBV.Internals as S import Copilot.Core.Expr (DropIdx) import Copilot.Core.Error (impossible)@@ -26,11 +25,10 @@ -------------------------------------------------------------------------------- -lookahead :: (S.HasSignAndSize a, S.SymWord a) - => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a+lookahead :: (S.SymWord a) => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a lookahead i buf ptr = let sz = fromIntegral $ length buf in- let (_, rem) = (ptr + fromIntegral i) `S.bvQuotRem` sz in+ let (_, rem) = (ptr + fromIntegral i) `S.sQuotRem` sz in let defaultVal = if null buf then impossible "lookahead" "copilot-sbv" else head buf in
src/Copilot/Compile/SBV/Witness.hs view
@@ -17,7 +17,6 @@ ) where import qualified Data.SBV as S-import qualified Data.SBV.Internals as S import qualified Copilot.Core as C import Data.Word (Word8, Word16, Word32, Word64)@@ -27,7 +26,7 @@ -------------------------------------------------------------------------------- badInst :: a-badInst = C.impossible "witnesses" "copilot-sbv"+badInst = error "Fatal cast in the witnesses of SBV in copilot-sbv. Are you sure that SBV supports the type you are using? (It doesn't support floats or doubles.) If you you are, or you don't understand the error, email leepike @ gmail . com (remove spaces) or file a bug report on github.com" -------------------------------------------------------------------------------- @@ -61,7 +60,7 @@ -------------------------------------------------------------------------------- -data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst+data HasSignAndSizeInst a = S.SymWord a => HasSignAndSizeInst hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a hasSignAndSizeInst t =@@ -95,16 +94,16 @@ -------------------------------------------------------------------------------- -data BVDivisibleInst a = S.BVDivisible (S.SBV a) => BVDivisibleInst+data BVDivisibleInst a = S.SDivisible (S.SBV a) => BVDivisibleInst divInst :: C.Type a -> BVDivisibleInst a divInst t = case t of C.Bool -> badInst- C.Int8 -> badInst- C.Int16 -> badInst- C.Int32 -> badInst- C.Int64 -> badInst+ C.Int8 -> BVDivisibleInst+ C.Int16 -> BVDivisibleInst+ C.Int32 -> BVDivisibleInst+ C.Int64 -> BVDivisibleInst C.Word8 -> BVDivisibleInst C.Word16 -> BVDivisibleInst C.Word32 -> BVDivisibleInst