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

Documentation.SBV.Examples.Queries.Enums

Description

Demonstrates the use of enumeration values during queries.

Synopsis

data Day
- = Monday
- | Tuesday
- | Wednesday
- | Thursday
- | Friday
- | Saturday
- | Sunday
type SDay = SBV Day
findDays :: IO [Day]

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 #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods (==) :: Day -> Day -> Bool # (/=) :: Day -> Day -> Bool #
Data Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums 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 #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums 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 #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods readsPrec :: Int -> ReadS Day # readList :: ReadS [Day] # readPrec :: ReadPrec Day # readListPrec :: ReadPrec [Day] #
Show Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods showsPrec :: Int -> Day -> ShowS # show :: Day -> String # showList :: [Day] -> ShowS #
HasKind Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums 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 # isUnbounded :: Day -> Bool Source # isUninterpreted :: Day -> Bool Source # isChar :: Day -> Bool Source # isString :: Day -> Bool Source # isList :: Day -> Bool Source # isSet :: Day -> Bool Source # isTuple :: Day -> Bool Source # isMaybe :: Day -> Bool Source # isEither :: Day -> Bool Source # showType :: Day -> String Source #
SymVal Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV Day) Source # literal :: Day -> SBV Day Source # fromCV :: CV -> Day Source # isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Day) Source # forall_ :: MonadSymbolic m => m (SBV Day) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Day] Source # exists :: MonadSymbolic m => String -> m (SBV Day) Source # exists_ :: MonadSymbolic m => m (SBV Day) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Day] Source # free :: MonadSymbolic m => String -> m (SBV Day) Source # free_ :: MonadSymbolic m => m (SBV Day) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Day] Source # symbolic :: MonadSymbolic m => String -> m (SBV Day) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Day] Source # unliteral :: SBV Day -> Maybe Day Source # isConcrete :: SBV Day -> Bool Source # isSymbolic :: SBV Day -> Bool Source #
SatModel Day Source #	Make `Day` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods parseCVs :: [CV] -> Maybe (Day, [CV]) Source # cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) Source #
SMTValue Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums 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]