summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Yices/Painless/Language.hs143
-rw-r--r--Yices/Painless/Type.hs51
-rw-r--r--tests/examples/ex1.hs5
-rw-r--r--tests/examples/ex2.hs5
-rw-r--r--tests/examples/ex24.hs16
-rw-r--r--tests/examples/ex3.hs38
-rw-r--r--tests/examples/ex5.ys18
-rw-r--r--tests/examples/ex6.ys18
-rw-r--r--tests/examples/ex66.hs7
-rw-r--r--tests/examples/ex67.hs10
-rw-r--r--yices-painless.cabal15
11 files changed, 235 insertions, 91 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
diff --git a/Yices/Painless/Type.hs b/Yices/Painless/Type.hs
index a4e56a8..ad9bfb4 100644
--- a/Yices/Painless/Type.hs
+++ b/Yices/Painless/Type.hs
@@ -136,6 +136,8 @@ data IntegralType a where
TypeCLLong :: IntegralDict CLLong -> IntegralType CLLong
TypeCULLong :: IntegralDict CULLong -> IntegralType CULLong
+ TypeVectorBool :: IntegralDict BitVector -> IntegralType BitVector
+
-- |Floating-point types supported in yices computations.
--
data FloatingType a where
@@ -153,16 +155,35 @@ data NonNumType a where
TypeCSChar :: NonNumDict CSChar -> NonNumType CSChar
TypeCUChar :: NonNumDict CUChar -> NonNumType CUChar
- -- Could define a Num instance
- TypeVectorBool :: NonNumDict BitVector -> NonNumType BitVector
-
-
------------------------------------------------------------------------
-- Todo: support 'Word' packed representation (for fast constants).
newtype BitVector = BitVector { unBV :: V.Vector Bool }
deriving (Eq, Ord, Typeable)
+instance Num BitVector where
+ (+) = error "Prelude.Num.+ applied to BitVectors"
+ (-) = error "Prelude.Num.- applied to BitVectors"
+ (*) = error "Prelude.Num.* applied to BitVectors"
+ negate = error "Prelude.Num.negate applied to BitVectors"
+ abs _ = error "Prelude.Num.abs applied to EDSL types"
+ signum _ = error "Prelude.Num.signum applied to EDSL types"
+
+ -- TODO: size is fixed
+ fromInteger n = BitVector $ V.generate (8 * sizeOf (undefined :: Word)) (testBit w)
+ where
+ w :: Word
+ w = fromIntegral n
+
+-- Fake instances so we can get Num BitVector. We could do it for real via Integer...
+-- Or just use Integers
+
+instance Integral BitVector
+instance Bits BitVector
+instance Enum BitVector
+instance Bounded BitVector
+instance Real BitVector
+
-- Smart show instance.
instance Show BitVector where
show (BitVector v)
@@ -215,6 +236,7 @@ instance Show (IntegralType a) where
show (TypeCULong _) = "CULong"
show (TypeCLLong _) = "CLLong"
show (TypeCULLong _) = "CULLong"
+ show (TypeVectorBool _) = "(Vector Bool)"
instance Show (FloatingType a) where
show (TypeFloat _) = "Float"
@@ -228,7 +250,6 @@ instance Show (NonNumType a) where
show (TypeCChar _) = "CChar"
show (TypeCSChar _) = "CSChar"
show (TypeCUChar _) = "CUChar"
- show (TypeVectorBool _) = "(Vector Bool)"
instance Show (NumType a) where
show (IntegralNumType ty) = show ty
@@ -253,6 +274,9 @@ class (IsScalar a, IsNum a, IsBounded a) => IsIntegral a where
instance IsIntegral Int where
integralType = TypeInt IntegralDict
+instance IsIntegral BitVector where
+ integralType = TypeVectorBool IntegralDict
+
instance IsIntegral Int8 where
integralType = TypeInt8 IntegralDict
@@ -341,9 +365,6 @@ instance IsNonNum CSChar where
instance IsNonNum CUChar where
nonNumType = TypeCUChar NonNumDict
-instance IsNonNum BitVector where
- nonNumType = TypeVectorBool NonNumDict
-
-- |Numeric types
--
class (Num a, IsScalar a) => IsNum a where
@@ -403,6 +424,9 @@ instance IsNum CLLong where
instance IsNum CULLong where
numType = IntegralNumType integralType
+instance IsNum BitVector where
+ numType = IntegralNumType integralType
+
instance IsNum Float where
numType = FloatingNumType floatingType
@@ -423,6 +447,9 @@ class IsBounded a where
instance IsBounded Int where
boundedType = IntegralBoundedType integralType
+instance IsBounded BitVector where
+ boundedType = IntegralBoundedType integralType
+
instance IsBounded Int8 where
boundedType = IntegralBoundedType integralType
@@ -560,6 +587,9 @@ instance IsScalar CFloat where
instance IsScalar CDouble where
scalarType = NumScalarType numType
+instance IsScalar BitVector where
+ scalarType = NumScalarType numType
+
-- Non-numerical scalar types
instance IsScalar Bool where
@@ -577,9 +607,6 @@ instance IsScalar CSChar where
instance IsScalar CUChar where
scalarType = NonNumScalarType nonNumType
-instance IsScalar BitVector where
- scalarType = NonNumScalarType nonNumType -- false for bitvectors...
-
-- Extract reified dictionaries
--
@@ -602,6 +629,7 @@ integralDict (TypeCLong dict) = dict
integralDict (TypeCULong dict) = dict
integralDict (TypeCLLong dict) = dict
integralDict (TypeCULLong dict) = dict
+integralDict (TypeVectorBool dict) = dict
floatingDict :: FloatingType a -> FloatingDict a
floatingDict (TypeFloat dict) = dict
@@ -615,7 +643,6 @@ nonNumDict (TypeChar dict) = dict
nonNumDict (TypeCChar dict) = dict
nonNumDict (TypeCSChar dict) = dict
nonNumDict (TypeCUChar dict) = dict
-nonNumDict (TypeVectorBool dict) = dict
-- Tuple type
-- ----------
diff --git a/tests/examples/ex1.hs b/tests/examples/ex1.hs
new file mode 100644
index 0000000..7e924e0
--- /dev/null
+++ b/tests/examples/ex1.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = 0 ==* (1 :: Exp Int)
diff --git a/tests/examples/ex2.hs b/tests/examples/ex2.hs
new file mode 100644
index 0000000..fbf6a73
--- /dev/null
+++ b/tests/examples/ex2.hs
@@ -0,0 +1,5 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+p = false
diff --git a/tests/examples/ex24.hs b/tests/examples/ex24.hs
new file mode 100644
index 0000000..6327503
--- /dev/null
+++ b/tests/examples/ex24.hs
@@ -0,0 +1,16 @@
+import Yices.Painless.Language
+
+main = print =<< solve p
+
+data S = S1 | S2 | S3
+ deriving (Show, Enum)
+
+p x1 x2 x3 x4 =
+ and
+ [ (/=*) x1 x2
+ , (/=*) x1 x3
+ , (/=*) x1 x4
+ , (/=*) x2 x3
+ , (/=*) x2 x4
+ , (/=*) x3 x4
+ ]
diff --git a/tests/examples/ex3.hs b/tests/examples/ex3.hs
new file mode 100644
index 0000000..886f8f9
--- /dev/null
+++ b/tests/examples/ex3.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Yices.Painless.Language
+import Prelude hiding (and)
+
+main = print =<< solve p
+
+-- Currently, need to derive Int, then translate in and out.
+
+data PC = Sleeping | Trying | Critical
+ deriving (Show, Enum)
+
+p x1 x2 z1 z2 (w1 :: Exp Int) (w2 :: Exp Int) =
+ and
+ [ x1 ==* x2
+ , x1 ==* z1
+ , x2 ==* fromIntegral (fromEnum Critical)
+ , x2 ==* z2
+ , x2 ==* w1
+ , x1 ==* fromIntegral (fromEnum Trying)
+ ]
+
+{-
+-- (define-type pc (scalar sleeping trying critical))
+(define x1::pc)
+(define x2::pc)
+(define z1::pc)
+(define z2::pc)
+(define w1::pc)
+(define w2::pc)
+
+(assert (= x1 x2))
+(assert (= x1 z1))
+(assert (= x2 critical))
+(assert (= x2 z2))
+(assert (= z2 w1))
+(assert (= x1 trying))
+-}
diff --git a/tests/examples/ex5.ys b/tests/examples/ex5.ys
new file mode 100644
index 0000000..e813861
--- /dev/null
+++ b/tests/examples/ex5.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (/= (g (f x1)) (g (f x2))))
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+
diff --git a/tests/examples/ex6.ys b/tests/examples/ex6.ys
new file mode 100644
index 0000000..0bd00f3
--- /dev/null
+++ b/tests/examples/ex6.ys
@@ -0,0 +1,18 @@
+
+(define-type pc (scalar sleeping trying critical))
+(define f::(-> pc pc))
+(define g::(-> pc pc))
+(define x1::pc)
+(define x2::pc)
+(define x3::pc)
+(define x4::pc)
+(define x5::pc)
+(define x6::pc)
+
+
+
+(assert (= x1 x3))
+(assert (= x1 x4))
+(assert (= x3 x2))
+(assert (/= (g (f x1)) (g (f x2))))
+
diff --git a/tests/examples/ex66.hs b/tests/examples/ex66.hs
new file mode 100644
index 0000000..d787cdb
--- /dev/null
+++ b/tests/examples/ex66.hs
@@ -0,0 +1,7 @@
+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
+
diff --git a/tests/examples/ex67.hs b/tests/examples/ex67.hs
new file mode 100644
index 0000000..ecf451c
--- /dev/null
+++ b/tests/examples/ex67.hs
@@ -0,0 +1,10 @@
+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) + z ==* 1
+ &&*
+ z ==* 2
+
diff --git a/yices-painless.cabal b/yices-painless.cabal
index 125fdad..b215e4d 100644
--- a/yices-painless.cabal
+++ b/yices-painless.cabal
@@ -1,5 +1,5 @@
Name: yices-painless
-Version: 0.1
+Version: 0.1.1
Synopsis: An embedded language for programming the Yices SMT solver
Description:
This library defines an embedded language in Haskell for programming
@@ -26,9 +26,16 @@ Description:
.
* <http://yices.csl.sri.com/>
.
- Low and medium-level bindings to the Yices C API are also provided.
- The medium-level bindings add significant type and resource safety
- to that which the C API provides.
+ The primary interface is via the EDSL, "Yices.Painless.Language",
+ however, low and medium-level bindings to the Yices C API are also provided
+ ("Yices.Painless.Base.C" and "Yices.Painless.Base"). The
+ medium-level bindings add significant type and resource safety to
+ that which the C API provides.
+ .
+ Documentation for this package is available:
+ .
+ * <http://www.galois.com/~dons/yices-painless/>
+ .
Homepage: http://code.haskell.org/~dons/code/yices-painless
License: BSD3