summaryrefslogtreecommitdiff
path: root/Yices/Painless/Language.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Yices/Painless/Language.hs')
-rw-r--r--Yices/Painless/Language.hs143
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