sbv-8.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

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.

Constructors

 Monday Tuesday Wednesday Thursday Friday Saturday Sunday
Instances
 Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums Methods(==) :: Day -> Day -> Bool #(/=) :: Day -> Day -> Bool # Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums Methodsgfoldl :: (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 #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 # Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums Methodscompare :: Day -> Day -> Ordering #(<) :: Day -> Day -> Bool #(<=) :: Day -> Day -> Bool #(>) :: Day -> Day -> Bool #(>=) :: Day -> Day -> Bool #max :: Day -> Day -> Day #min :: Day -> Day -> Day # Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums MethodsshowsPrec :: Int -> Day -> ShowS #show :: Day -> String #showList :: [Day] -> ShowS # Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums Methods Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums MethodsmkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV 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 # Source # Make Day a symbolic value. Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums MethodsparseCVs :: [CV] -> Maybe (Day, [CV]) Source #cvtModel :: (Day -> Maybe b) -> Maybe (Day, [CV]) -> Maybe (b, [CV]) Source # Source # Instance detailsDefined in Documentation.SBV.Examples.Queries.Enums MethodssexprToVal :: 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.)

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]