summaryrefslogtreecommitdiff
path: root/Yices/Painless/Type.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Yices/Painless/Type.hs')
-rw-r--r--Yices/Painless/Type.hs51
1 files changed, 39 insertions, 12 deletions
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
-- ----------