Documentation.SBV.Examples.Queries.Enums

Demonstrates the use of enumeration values during queries.

Documentation

data Day

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

Constructors

Monday

Tuesday

Wednesday

Thursday

Friday

Saturday

Sunday

Instances

Data Day

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

Read Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

readsPrec :: Int -> ReadS Day

readList :: ReadS [Day]

readPrec :: ReadPrec Day

readListPrec :: ReadPrec [Day]

Show Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

showsPrec :: Int -> Day -> ShowS

show :: Day -> String

showList :: [Day] -> ShowS

Eq Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

(==) :: Day -> Day -> Bool

(/=) :: Day -> Day -> Bool

Ord Day

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

SymVal Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Day)

literal :: Day -> SBV Day

fromCV :: CV -> Day

isConcretely :: SBV Day -> (Day -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Day)

sbvForall_ :: MonadSymbolic m => m (SBV Day)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Day]

sbvExists :: MonadSymbolic m => String -> m (SBV Day)

sbvExists_ :: MonadSymbolic m => m (SBV Day)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Day]

free :: MonadSymbolic m => String -> m (SBV Day)

free_ :: MonadSymbolic m => m (SBV Day)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Day]

symbolic :: MonadSymbolic m => String -> m (SBV Day)

symbolics :: MonadSymbolic m => [String] -> m [SBV Day]

unliteral :: SBV Day -> Maybe Day

isConcrete :: SBV Day -> Bool

isSymbolic :: SBV Day -> Bool

HasKind Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

kindOf :: Day -> Kind

hasSign :: Day -> Bool

intSizeOf :: Day -> Int

isBoolean :: Day -> Bool

isBounded :: Day -> Bool

isReal :: Day -> Bool

isFloat :: Day -> Bool

isDouble :: Day -> Bool

isRational :: Day -> Bool

isFP :: Day -> Bool

isUnbounded :: Day -> Bool

isUserSort :: Day -> Bool

isChar :: Day -> Bool

isString :: Day -> Bool

isList :: Day -> Bool

isSet :: Day -> Bool

isTuple :: Day -> Bool

isMaybe :: Day -> Bool

isEither :: Day -> Bool

showType :: Day -> String

SatModel Day

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

parseCVs :: [CV] -> Maybe (Day, [CV])

cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV])

type SDay = SBV Day

Symbolic version of the type Day.

sSunday :: SBV Day

Symbolic version of the constructor Sunday.

sSaturday :: SBV Day

Symbolic version of the constructor Saturday.

sFriday :: SBV Day

Symbolic version of the constructor Friday.

sThursday :: SBV Day

Symbolic version of the constructor Thursday.

sWednesday :: SBV Day

Symbolic version of the constructor Wednesday.

sTuesday :: SBV Day

Symbolic version of the constructor Tuesday.

sMonday :: SBV Day

Symbolic version of the constructor Monday.

findDays :: IO [Day]

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]