module Data.SBV.BitVectors.Kind
( Kind(..)
, kindHasSign
, constructUKind
) where
import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields)
import Data.SBV.BitVectors.AlgReals ()
data Kind = KBool
| KBounded Bool Int
| KUnbounded
| KReal
| KUserSort String (Either String [String], G.DataType)
| KFloat
| KDouble
deriving (Eq, Ord)
instance Show Kind where
show KBool = "SBool"
show (KBounded False n) = "SWord" ++ show n
show (KBounded True n) = "SInt" ++ show n
show KUnbounded = "SInteger"
show KReal = "SReal"
show (KUserSort s _) = s
show KFloat = "SFloat"
show KDouble = "SDouble"
instance Eq G.DataType where
a == b = G.tyconUQname (G.dataTypeName a) == G.tyconUQname (G.dataTypeName b)
instance Ord G.DataType where
a `compare` b = G.tyconUQname (G.dataTypeName a) `compare` G.tyconUQname (G.dataTypeName b)
kindHasSign :: Kind -> Bool
kindHasSign k =
case k of
KBool -> False
KBounded b _ -> b
KUnbounded -> True
KReal -> True
KFloat -> True
KDouble -> True
KUserSort{} -> False
constructUKind :: forall a. (Read a, G.Data a) => a -> Kind
constructUKind a = KUserSort sortName (mbEnumFields, dataType)
where dataType = G.dataTypeOf a
sortName = G.tyconUQname . G.dataTypeName $ dataType
constrs = G.dataTypeConstrs dataType
isEnumeration = not (null constrs) && all (null . G.constrFields) constrs
mbEnumFields
| isEnumeration = check constrs []
| True = Left $ sortName ++ "is not a finite non-empty enumeration"
check [] sofar = Right $ reverse sofar
check (c:cs) sofar = case checkConstr c of
Nothing -> check cs (show c : sofar)
Just s -> Left $ sortName ++ "." ++ show c ++ ": " ++ s
checkConstr c = case (reads (show c) :: [(a, String)]) of
((_, "") : _) -> Nothing
_ -> Just "not a nullary constructor"