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 #

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

Constructors

Monday
Tuesday
Wednesday
Thursday
Friday
Saturday
Sunday

Instances

Eq Day #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods (==) :: Day -> Day -> Bool # (/=) :: Day -> Day -> Bool #
Data Day #
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 #
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 #
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 #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods showsPrec :: Int -> Day -> ShowS # show :: Day -> String # showList :: [Day] -> ShowS #
HasKind Day #
Instance details 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 # isInteger :: Day -> Bool # isUninterpreted :: Day -> Bool # isChar :: Day -> Bool # isString :: Day -> Bool # isList :: Day -> Bool # showType :: Day -> String #
SymWord Day #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods forall :: String -> Symbolic (SBV Day) # forall_ :: Symbolic (SBV Day) # mkForallVars :: Int -> Symbolic [SBV Day] # exists :: String -> Symbolic (SBV Day) # exists_ :: Symbolic (SBV Day) # mkExistVars :: Int -> Symbolic [SBV Day] # free :: String -> Symbolic (SBV Day) # free_ :: Symbolic (SBV Day) # mkFreeVars :: Int -> Symbolic [SBV Day] # symbolic :: String -> Symbolic (SBV Day) # symbolics :: [String] -> Symbolic [SBV Day] # literal :: Day -> SBV Day # unliteral :: SBV Day -> Maybe Day # fromCW :: CW -> Day # isConcrete :: SBV Day -> Bool # isSymbolic :: SBV Day -> Bool # isConcretely :: SBV Day -> (Day -> Bool) -> Bool # mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Day) #
SatModel Day #	Make `Day` a symbolic value.
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods parseCWs :: [CW] -> Maybe (Day, [CW]) # cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CW]) -> Maybe (b, [CW]) #
SMTValue Day #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods sexprToVal :: SExpr -> Maybe Day #

type SDay = SBV Day #

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

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]