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
cv2Day :: String -> [CV] -> Day
_undefiner_Day :: a
type SDay = SBV Day
sMonday :: SBV Day
sTuesday :: SBV Day
sWednesday :: SBV Day
sThursday :: SBV Day
sFriday :: SBV Day
sSaturday :: SBV Day
sSunday :: SBV Day
isMonday :: SBV Day -> SBool
isTuesday :: SBV Day -> SBool
isWednesday :: SBV Day -> SBool
isThursday :: SBV Day -> SBool
isFriday :: SBV Day -> SBool
isSaturday :: SBV Day -> SBool
isSunday :: SBV Day -> SBool
sCaseDay :: Mergeable result => SBV Day -> result -> result -> result -> result -> result -> result -> result -> result
findDays :: IO [Day]

Documentation

data Day Source #

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

Constructors

Monday
Tuesday
Wednesday
Thursday
Friday
Saturday
Sunday

Instances

Instances details

Arbitrary Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods arbitrary :: Gen Day # shrink :: Day -> [Day] #
Show Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods showsPrec :: Int -> Day -> ShowS # show :: Day -> String # showList :: [Day] -> ShowS #
SymVal Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Day) Source # mkSymValInit :: State -> SBV Day -> IO () Source # literal :: Day -> SBV Day Source # fromCV :: CV -> Day Source # isConcretely :: SBV Day -> (Day -> Bool) -> Bool Source # minMaxBound :: Maybe (Day, 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 # unlitCV :: SBV Day -> Maybe (Kind, CVal) Source # isConcrete :: SBV Day -> Bool Source # isSymbolic :: SBV Day -> Bool Source #
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 # isADT :: Day -> Bool Source # isChar :: Day -> Bool Source # isString :: Day -> Bool Source # isList :: Day -> Bool Source # isSet :: Day -> Bool Source # isTuple :: Day -> Bool Source # isArray :: Day -> Bool Source # isRoundingMode :: Day -> Bool Source # isUninterpreted :: Day -> Bool Source # showType :: Day -> String Source #
EnumSymbolic Day Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods succ :: SBV Day -> SBV Day Source # pred :: SBV Day -> SBV Day Source # toEnum :: SInteger -> SBV Day Source # fromEnum :: SBV Day -> SInteger Source # enumFrom :: SBV Day -> SList Day Source # enumFromThen :: SBV Day -> SBV Day -> SList Day Source # enumFromTo :: SBV Day -> SBV Day -> SList Day Source # enumFromThenTo :: SBV Day -> SBV Day -> SBV Day -> SList Day 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 #
OrdSymbolic (SBV Day) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods (.<) :: SBV Day -> SBV Day -> SBool Source # (.<=) :: SBV Day -> SBV Day -> SBool Source # (.>) :: SBV Day -> SBV Day -> SBool Source # (.>=) :: SBV Day -> SBV Day -> SBool Source # smin :: SBV Day -> SBV Day -> SBV Day Source # smax :: SBV Day -> SBV Day -> SBV Day Source # inRange :: SBV Day -> (SBV Day, SBV Day) -> SBool Source #
HasInductionSchema (Forall ta Day -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta Day -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.Queries.Enums Methods inductionSchema :: (Forall ta Day -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Day :: String -> [CV] -> Day Source #

Conversion from SMT values to Day values.

_undefiner_Day :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SDay = SBV Day Source #

Symbolic version of the type Day.

sMonday :: SBV Day Source #

Symbolic version of the constructor Monday.

sTuesday :: SBV Day Source #

Symbolic version of the constructor Tuesday.

sWednesday :: SBV Day Source #

Symbolic version of the constructor Wednesday.

sThursday :: SBV Day Source #

Symbolic version of the constructor Thursday.

sFriday :: SBV Day Source #

Symbolic version of the constructor Friday.

sSaturday :: SBV Day Source #

Symbolic version of the constructor Saturday.

sSunday :: SBV Day Source #

Symbolic version of the constructor Sunday.

isMonday :: SBV Day -> SBool Source #

Field recognizer predicate.

isTuesday :: SBV Day -> SBool Source #

Field recognizer predicate.

isWednesday :: SBV Day -> SBool Source #

Field recognizer predicate.

isThursday :: SBV Day -> SBool Source #

Field recognizer predicate.

isFriday :: SBV Day -> SBool Source #

Field recognizer predicate.

isSaturday :: SBV Day -> SBool Source #

Field recognizer predicate.

isSunday :: SBV Day -> SBool Source #

Field recognizer predicate.

sCaseDay :: Mergeable result => SBV Day -> result -> result -> result -> result -> result -> result -> result -> result Source #

Case analyzer for the type Day.

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]