Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.SBV.Examples.Queries.Enums

Description

Demonstrates the use of enumeration values during queries.

Synopsis

Documentation

data Day Source #

Days of the week. We make it symbolic using the mkSymbolicEnumeration splice.

Constructors

Monday
Tuesday
Wednesday
Thursday
Friday
Saturday
Sunday

Instances

Eq Day Source #
Methods (==) :: Day -> Day -> Bool # (/=) :: Day -> Day -> Bool #
Data Day Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Day -> c Day # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Day # toConstr :: Day -> Constr # dataTypeOf :: Day -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Day) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Day) # gmapT :: (forall b. Data b => b -> b) -> Day -> Day # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Day -> r # gmapQ :: (forall d. Data d => d -> u) -> Day -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Day -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Day -> m Day # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Day -> m Day #
Ord Day Source #
Methods compare :: Day -> Day -> Ordering # (<) :: Day -> Day -> Bool # (<=) :: Day -> Day -> Bool # (>) :: Day -> Day -> Bool # (>=) :: Day -> Day -> Bool # max :: Day -> Day -> Day # min :: Day -> Day -> Day #
Read Day Source #
Methods readsPrec :: Int -> ReadS Day # readList :: ReadS [Day] # readPrec :: ReadPrec Day # readListPrec :: ReadPrec [Day] #
Show Day Source #
Methods showsPrec :: Int -> Day -> ShowS # show :: Day -> String # showList :: [Day] -> ShowS #
HasKind Day Source #
Methods kindOf :: Day -> Kind Source # hasSign :: Day -> Bool Source # intSizeOf :: Day -> Int Source # isBoolean :: Day -> Bool Source # isBounded :: Day -> Bool Source # isReal :: Day -> Bool Source # isFloat :: Day -> Bool Source # isDouble :: Day -> Bool Source # isInteger :: Day -> Bool Source # isUninterpreted :: Day -> Bool Source # showType :: Day -> String Source #
SymWord Day Source #
Methods forall :: String -> Symbolic (SBV Day) Source # forall_ :: Symbolic (SBV Day) Source # mkForallVars :: Int -> Symbolic [SBV Day] Source # exists :: String -> Symbolic (SBV Day) Source # exists_ :: Symbolic (SBV Day) Source # mkExistVars :: Int -> Symbolic [SBV Day] Source # free :: String -> Symbolic (SBV Day) Source # free_ :: Symbolic (SBV Day) Source # mkFreeVars :: Int -> Symbolic [SBV Day] Source # symbolic :: String -> Symbolic (SBV Day) Source # symbolics :: [String] -> Symbolic [SBV Day] Source # literal :: Day -> SBV Day Source # unliteral :: SBV Day -> Maybe Day Source # fromCW :: CW -> Day Source # isConcrete :: SBV Day -> Bool Source # isSymbolic :: SBV Day -> Bool Source # isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Day) Source #
SatModel Day Source #	Make `Day` a symbolic value.
Methods parseCWs :: [CW] -> Maybe (Day, [CW]) Source # cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CW]) -> Maybe (b, [CW]) Source #
SMTValue Day Source #
Methods sexprToVal :: SExpr -> Maybe Day Source #

type SDay = SBV Day Source #

The type synonym SDay is the symbolic variant of Day. (Similar to 'SInteger'/'Integer' and others.)

findDays :: IO [Day] Source #

A trivial query to find three consecutive days that's all before Thursday. The point here is that we can perform queries on such enumerated values and use getValue on them and return their values from queries just like any other value. We have:

>>> findDays
[Monday,Tuesday,Wednesday]