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
sSunday :: SBV Day
sSaturday :: SBV Day
sFriday :: SBV Day
sThursday :: SBV Day
sWednesday :: SBV Day
sTuesday :: SBV Day
sMonday :: 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

Instances details

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 :: forall r r'. (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 # isRational :: Day -> Bool Source # isFP :: Day -> Bool Source # isUnbounded :: Day -> Bool Source # isUserSort :: 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 => VarContext -> Maybe String -> m (SBV Day) Source # literal :: Day -> SBV Day Source # fromCV :: CV -> Day Source # isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source # sbvForall :: MonadSymbolic m => String -> m (SBV Day) Source # sbvForall_ :: MonadSymbolic m => m (SBV Day) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Day] Source # sbvExists :: MonadSymbolic m => String -> m (SBV Day) Source # sbvExists_ :: 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 #
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 #

type SDay = SBV Day Source #

Make Day a symbolic value.

sSunday :: SBV Day Source #

sSaturday :: SBV Day Source #

sFriday :: SBV Day Source #

sThursday :: SBV Day Source #

sWednesday :: SBV Day Source #

sTuesday :: SBV Day Source #

sMonday :: SBV Day Source #

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]