diff options
Diffstat (limited to 'Yices/Painless/Language.hs')
| -rw-r--r-- | Yices/Painless/Language.hs | 143 |
1 files changed, 68 insertions, 75 deletions
diff --git a/Yices/Painless/Language.hs b/Yices/Painless/Language.hs index eaf56cd..a607f60 100644 --- a/Yices/Painless/Language.hs +++ b/Yices/Painless/Language.hs @@ -1,11 +1,10 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE OverlappingInstances #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -28,6 +27,15 @@ -- Terms and types are embedded in Haskell, so all the usual type -- inference and checking works for Yices propositions. -- +-- /A simple example: integers/ +-- +-- > import Yices.Painless.Language +-- > +-- > main = print =<< solve p +-- > +-- > p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool +-- > p x y z = (3 * x) + (6 * y) ==* 1 +-- -- /A simple example: bitvectors/ -- -- > solve $ \b1 (b2 :: Exp BitVector) @@ -86,7 +94,6 @@ import Data.Typeable import qualified Data.Map as M import Data.Bits -import qualified Data.Vector.Storable as V import Control.Monad import Control.Applicative ((<$>)) @@ -105,9 +112,6 @@ import qualified Yices.Painless.Tuple as Tuple -- -- /Future work/: -- --- * Separate 'BitVector's into their own type, so that we can reuse --- their 'Num' instance, avoiding OverlappingInstances. --- -- * BitVectors are sized, yet we do not represent their size at all -- currently. Size types would let us statically check e.g. bit vector -- concatenation. @@ -118,13 +122,17 @@ import qualified Yices.Painless.Tuple as Tuple -- -- * A 'Monoid' instance for bit vectors? -- +-- * A monoid for conjunction? +-- -- * Support other numeric types. -- -- * Support function types in the core language. -- --- * Support more Yices types: tuples, records, recursive types. +-- * Support more SMT types: functions, tuples, records, recursive types. +-- +-- * Deriving Exp. A (derivable) class for lifting Haskell data types +-- into their symbolic form. -- - ------------------------------------------------------------------------ -- Language @@ -225,38 +233,16 @@ instance (IsScalar t) => Enum (Exp t) -} instance (IsScalar t) => Prelude.Eq (Exp t) where - -- FIXME: instance makes no sense with standard signatures + -- instance makes no sense with standard signatures (==) = error "Prelude.Eq.== applied to EDSL types" instance (IsScalar t) => Prelude.Ord (Exp t) where - -- FIXME: instance makes no sense with standard signatures + -- instance makes no sense with standard signatures compare = error "Prelude.Ord.compare applied to EDSL types" ------------------------------------------------------------------------ -- Bit vector operations --- /TODO/ Vector Bool isn't an instance of num, but abstract Exp BitVectors are! --- --- We could have an instance of Num BitVector and overload the operators. --- via the Num (Exp a) instance. --- - -instance Num (Exp BitVector) where - (+) = mkBVAdd - (-) = mkBVSub - (*) = mkBVMul - negate = mkBVNeg - - fromInteger n = constant . BitVector $ - V.generate (8 * sizeOf (undefined :: Word)) (testBit w) - where - w :: Word - w = fromIntegral n - - abs _ = error "Prelude.Num.abs applied to EDSL types" - -- if n >= 0 then n else negate n - signum _ = error "Prelude.Num.signum applied to EDSL types" - -- TODO: fromInteger should probably build from mkBVConstant -- TOD0: need size information. -- TOD0: support construction of a specific size @@ -267,17 +253,24 @@ instance Num (Exp BitVector) where -- needs size types! -- $BitInstances --- The 'Exp BitVector' type is an instance of 'Bits', allowing the usual +-- The 'Exp BitVector' type is an instance of 'Bits' and 'Num', allowing the usual -- Haskell bitwise operators to be used to construct propositions involving -- bitwise operations on bit vectors. -- --- > (.&,), (.|.), xor, complement, shiftL, shiftR +-- > (.&.) :: Exp BitVector -> Exp BitVector -> Exp BitVector +-- > (.|.) +-- > xor +-- > complement +-- > shiftL +-- > shiftR -- -- Currently bit vectors are fixed at 'sizeOf (undefined :: Word)' bits. -- -- Bit vector constants can be constructed using overloaded numeric -- literals. -- +-- TODO: instance Bits a => Bits (Exp a) +-- instance Bits (Exp BitVector) where (.&.) = mkBVAnd @@ -288,7 +281,6 @@ instance Bits (Exp BitVector) where shiftR = mkBVShiftR0 isSigned _ = False bitSize _ = 8 * sizeOf (undefined :: Word) -- TODO! size type - ------------------------------------------------------------------------ @@ -357,17 +349,10 @@ min x y = x <* y ? (x , y) -- Bit vector operators -mkBVAdd :: Exp BitVector -> Exp BitVector -> Exp BitVector -mkBVAdd x y = PrimBVAdd `PrimApp` tup2 (x, y) - -mkBVMul :: Exp BitVector -> Exp BitVector -> Exp BitVector -mkBVMul x y = PrimBVMul `PrimApp` tup2 (x, y) +-- mkBVNeg :: Exp BitVector -> Exp BitVector +-- mkBVNeg x = PrimBVNeg `PrimApp` x -mkBVSub :: Exp BitVector -> Exp BitVector -> Exp BitVector -mkBVSub x y = PrimBVSub `PrimApp` tup2 (x, y) - -mkBVNeg :: Exp BitVector -> Exp BitVector -mkBVNeg x = PrimBVNeg `PrimApp` x +-- Bits instance mkBVAnd :: Exp BitVector -> Exp BitVector -> Exp BitVector mkBVAnd x y = PrimBVAnd `PrimApp` tup2 (x, y) @@ -387,7 +372,10 @@ mkBVShiftL0 x n = PrimBVSL0 `PrimApp` tup2 (x, constant n) -- lift the int shift mkBVShiftR0 :: Exp BitVector -> Int -> Exp BitVector mkBVShiftR0 x n = PrimBVSR0 `PrimApp` tup2 (x, constant n) -- shiftR fills with 0 --- Operators from Num +------------------------------------------------------------------------ +-- Scalar operations + +-- Operators from Num, also includes BitVector operations mkAdd :: (IsNum t) => Exp t -> Exp t -> Exp t mkAdd x y = PrimAdd numType `PrimApp` tup2 (x, y) @@ -429,6 +417,7 @@ mkLOr x y = PrimLOr `PrimApp` tup2 (x, y) mkLNot :: Exp Bool -> Exp Bool mkLNot x = PrimLNot `PrimApp` x +------------------------------------------------------------------------ -- Smart constructor for literals -- | Literal 'True' @@ -990,7 +979,7 @@ get m v (YType (ty :: ScalarType t)) d = do mn <- Yices.getValueBool m d return (v, YValue mn) - | NonNumScalarType (TypeVectorBool _) <- ty + | NumScalarType (IntegralNumType (TypeVectorBool _)) <- ty = do mn <- Yices.getValueBitVector m d (fromIntegral $ 8 * sizeOf (undefined :: Word)) return (v, YValue $ fmap BitVector mn) @@ -1048,7 +1037,7 @@ execF c fn = go fn 0 M.empty -- Bit vectors go (OLam (f :: OpenFun (env, a) t)) n g - | ty@(NonNumScalarType (TypeVectorBool _)) <- scalarType :: ScalarType a + | ty@(NumScalarType (IntegralNumType (TypeVectorBool _))) <- scalarType :: ScalarType a = do let nm = "x" ++ show n -- TODO: hack, no size information for bit vectors yet. @@ -1083,7 +1072,7 @@ exec c (OConst n) = if n then Yices.mkTrue c else Yices.mkFalse c - | NonNumScalarType (TypeVectorBool _) <- scalarType :: ScalarType t + | NumScalarType (IntegralNumType (TypeVectorBool _)) <- scalarType :: ScalarType t = Yices.mkBVConstantFromVector c (unBV n) @@ -1118,7 +1107,7 @@ exec c (OPrimApp (PrimNEq _) Yices.mkNeq c e1 e2 -- Specialize for BitVector first -exec c (OPrimApp (PrimLt (NonNumScalarType (TypeVectorBool _))) +exec c (OPrimApp (PrimLt (NumScalarType (IntegralNumType (TypeVectorBool _)))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 @@ -1132,7 +1121,7 @@ exec c (OPrimApp (PrimLt _) Yices.mkLt c e1 e2 -- Specialize for BitVector first -exec c (OPrimApp (PrimLtEq (NonNumScalarType (TypeVectorBool _))) +exec c (OPrimApp (PrimLtEq (NumScalarType (IntegralNumType (TypeVectorBool _)))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 @@ -1145,7 +1134,7 @@ exec c (OPrimApp (PrimLtEq _) Yices.mkLe c e1 e2 -- Specialize for BitVector first -exec c (OPrimApp (PrimGt (NonNumScalarType (TypeVectorBool _))) +exec c (OPrimApp (PrimGt (NumScalarType (IntegralNumType (TypeVectorBool _)))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 @@ -1159,7 +1148,7 @@ exec c (OPrimApp (PrimGt _) -- TODO think about what gets through the overloading incorrectly. -- Specialize for BitVector first -exec c (OPrimApp (PrimGtEq (NonNumScalarType (TypeVectorBool _))) +exec c (OPrimApp (PrimGtEq (NumScalarType (IntegralNumType (TypeVectorBool _)))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 @@ -1189,45 +1178,49 @@ exec c (OPrimApp PrimLNot x) = do -- Numerical operations -exec c (OPrimApp (PrimAdd _) - (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do +-- overloaded on bit vectors +exec c (OPrimApp (PrimAdd (IntegralNumType (TypeVectorBool _))) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 - Yices.mkSum c [e1,e2] + Yices.mkBVAdd c e1 e2 -exec c (OPrimApp (PrimSub _) +exec c (OPrimApp (PrimAdd _) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 - Yices.mkSub c [e1,e2] + Yices.mkSum c [e1,e2] -exec c (OPrimApp (PrimMul _) +-- overloaded on bit vectors +exec c (OPrimApp (PrimSub (IntegralNumType (TypeVectorBool _))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 - Yices.mkMul c [e1,e2] - ------------------------------------------------------------------------- --- Bit Vector operations + Yices.mkBVSub c e1 e2 -exec c (OPrimApp PrimBVAdd - (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do +exec c (OPrimApp (PrimSub _) + (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 - Yices.mkBVAdd c e1 e2 + Yices.mkSub c [e1,e2] -exec c (OPrimApp PrimBVMul +-- overloaded on bit vectors +exec c (OPrimApp (PrimMul (IntegralNumType (TypeVectorBool _))) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 Yices.mkBVMul c e1 e2 -exec c (OPrimApp PrimBVSub +exec c (OPrimApp (PrimMul _) (OTuple (NilTup `SnocTup` x1 `SnocTup` x2))) = do e1 <- exec c x1 e2 <- exec c x2 - Yices.mkBVSub c e1 e2 + Yices.mkMul c [e1,e2] + +------------------------------------------------------------------------ +-- Bit Vector operations +-- TODO exec c (OPrimApp PrimBVNeg (OTuple (NilTup `SnocTup` x1))) = do e1 <- exec c x1 |