sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Documentation.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.

Instances

Instances details
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 #

Read Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Show Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

showsPrec :: Int -> Day -> ShowS #

show :: Day -> String #

showList :: [Day] -> ShowS #

Eq Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

Methods

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

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

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 #

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

HasKind Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

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 #

Symbolic version of the type Day.

sSunday :: SBV Day Source #

Symbolic version of the constructor Sunday.

sSaturday :: SBV Day Source #

Symbolic version of the constructor Saturday.

sFriday :: SBV Day Source #

Symbolic version of the constructor Friday.

sThursday :: SBV Day Source #

Symbolic version of the constructor Thursday.

sWednesday :: SBV Day Source #

Symbolic version of the constructor Wednesday.

sTuesday :: SBV Day Source #

Symbolic version of the constructor Tuesday.

sMonday :: SBV Day Source #

Symbolic version of the constructor Monday.

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]