Copyright	(c) Curran McConnell Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Misc.Newtypes

Description

Demonstrates how to create symbolic newtypes with the same behaviour as their wrapped type.

Synopsis

newtype Metres = Metres Integer
type SMetres = SBV Metres
newtype HumanHeightInCm = HumanHeightInCm Word16
type SHumanHeightInCm = SBV HumanHeightInCm
tallestHumanEver :: SHumanHeightInCm
ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool
problem :: Predicate

Documentation

newtype Metres Source #

A Metres is a newtype wrapper around Integer.

Constructors

Metres Integer

Instances

Instances details

Enum Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods succ :: Metres -> Metres # pred :: Metres -> Metres # toEnum :: Int -> Metres # fromEnum :: Metres -> Int # enumFrom :: Metres -> [Metres] # enumFromThen :: Metres -> Metres -> [Metres] # enumFromTo :: Metres -> Metres -> [Metres] # enumFromThenTo :: Metres -> Metres -> Metres -> [Metres] #
Eq Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (==) :: Metres -> Metres -> Bool # (/=) :: Metres -> Metres -> Bool #
Integral Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods quot :: Metres -> Metres -> Metres # rem :: Metres -> Metres -> Metres # div :: Metres -> Metres -> Metres # mod :: Metres -> Metres -> Metres # quotRem :: Metres -> Metres -> (Metres, Metres) # divMod :: Metres -> Metres -> (Metres, Metres) # toInteger :: Metres -> Integer #
Num Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (+) :: Metres -> Metres -> Metres # (-) :: Metres -> Metres -> Metres # (*) :: Metres -> Metres -> Metres # negate :: Metres -> Metres # abs :: Metres -> Metres # signum :: Metres -> Metres # fromInteger :: Integer -> Metres #
Ord Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods compare :: Metres -> Metres -> Ordering # (<) :: Metres -> Metres -> Bool # (<=) :: Metres -> Metres -> Bool # (>) :: Metres -> Metres -> Bool # (>=) :: Metres -> Metres -> Bool # max :: Metres -> Metres -> Metres # min :: Metres -> Metres -> Metres #
Real Metres Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods toRational :: Metres -> Rational #
HasKind Metres Source #	To use `Metres` symbolically, we associate it with the underlying symbolic type's kind.
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods kindOf :: Metres -> Kind Source # hasSign :: Metres -> Bool Source # intSizeOf :: Metres -> Int Source # isBoolean :: Metres -> Bool Source # isBounded :: Metres -> Bool Source # isReal :: Metres -> Bool Source # isFloat :: Metres -> Bool Source # isDouble :: Metres -> Bool Source # isFP :: Metres -> Bool Source # isUnbounded :: Metres -> Bool Source # isUserSort :: Metres -> Bool Source # isChar :: Metres -> Bool Source # isString :: Metres -> Bool Source # isList :: Metres -> Bool Source # isSet :: Metres -> Bool Source # isTuple :: Metres -> Bool Source # isMaybe :: Metres -> Bool Source # isEither :: Metres -> Bool Source # showType :: Metres -> String Source #
SymVal Metres Source #	The `SymVal` instance simply uses stock definitions. This is always possible for newtypes that simply wrap over an existing symbolic type.
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Metres) Source # literal :: Metres -> SBV Metres Source # fromCV :: CV -> Metres Source # isConcretely :: SBV Metres -> (Metres -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV Metres) Source # forall_ :: MonadSymbolic m => m (SBV Metres) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV Metres] Source # exists :: MonadSymbolic m => String -> m (SBV Metres) Source # exists_ :: MonadSymbolic m => m (SBV Metres) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV Metres] Source # free :: MonadSymbolic m => String -> m (SBV Metres) Source # free_ :: MonadSymbolic m => m (SBV Metres) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV Metres] Source # symbolic :: MonadSymbolic m => String -> m (SBV Metres) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV Metres] Source # unliteral :: SBV Metres -> Maybe Metres Source # isConcrete :: SBV Metres -> Bool Source # isSymbolic :: SBV Metres -> Bool Source #

type SMetres = SBV Metres Source #

Symbolic version of Metres.

newtype HumanHeightInCm Source #

Similarly, we can create another newtype, this time wrapping over Word16. As an example, consider measuring the human height in centimetres? The tallest person in history, Robert Wadlow, was 272 cm. We don't need negative values, so Word16 is the smallest type that suits our needs.

Constructors

HumanHeightInCm Word16

Instances

Instances details

Enum HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods succ :: HumanHeightInCm -> HumanHeightInCm # pred :: HumanHeightInCm -> HumanHeightInCm # toEnum :: Int -> HumanHeightInCm # fromEnum :: HumanHeightInCm -> Int # enumFrom :: HumanHeightInCm -> [HumanHeightInCm] # enumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm] # enumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm] # enumFromThenTo :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm] #
Eq HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (==) :: HumanHeightInCm -> HumanHeightInCm -> Bool # (/=) :: HumanHeightInCm -> HumanHeightInCm -> Bool #
Integral HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods quot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # rem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # div :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # mod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # quotRem :: HumanHeightInCm -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm) # divMod :: HumanHeightInCm -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm) # toInteger :: HumanHeightInCm -> Integer #
Num HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods (+) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # (-) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # (*) :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # negate :: HumanHeightInCm -> HumanHeightInCm # abs :: HumanHeightInCm -> HumanHeightInCm # signum :: HumanHeightInCm -> HumanHeightInCm # fromInteger :: Integer -> HumanHeightInCm #
Ord HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods compare :: HumanHeightInCm -> HumanHeightInCm -> Ordering # (<) :: HumanHeightInCm -> HumanHeightInCm -> Bool # (<=) :: HumanHeightInCm -> HumanHeightInCm -> Bool # (>) :: HumanHeightInCm -> HumanHeightInCm -> Bool # (>=) :: HumanHeightInCm -> HumanHeightInCm -> Bool # max :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm # min :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm #
Real HumanHeightInCm Source #
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods toRational :: HumanHeightInCm -> Rational #
HasKind HumanHeightInCm Source #	Symbolic instance simply follows the underlying type, just like `Metres`.
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods kindOf :: HumanHeightInCm -> Kind Source # hasSign :: HumanHeightInCm -> Bool Source # intSizeOf :: HumanHeightInCm -> Int Source # isBoolean :: HumanHeightInCm -> Bool Source # isBounded :: HumanHeightInCm -> Bool Source # isReal :: HumanHeightInCm -> Bool Source # isFloat :: HumanHeightInCm -> Bool Source # isDouble :: HumanHeightInCm -> Bool Source # isFP :: HumanHeightInCm -> Bool Source # isUnbounded :: HumanHeightInCm -> Bool Source # isUserSort :: HumanHeightInCm -> Bool Source # isChar :: HumanHeightInCm -> Bool Source # isString :: HumanHeightInCm -> Bool Source # isList :: HumanHeightInCm -> Bool Source # isSet :: HumanHeightInCm -> Bool Source # isTuple :: HumanHeightInCm -> Bool Source # isMaybe :: HumanHeightInCm -> Bool Source # isEither :: HumanHeightInCm -> Bool Source # showType :: HumanHeightInCm -> String Source #
SymVal HumanHeightInCm Source #	Similarly here, for the `SymVal` instance.
Instance details Defined in Documentation.SBV.Examples.Misc.Newtypes Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV HumanHeightInCm) Source # literal :: HumanHeightInCm -> SBV HumanHeightInCm Source # fromCV :: CV -> HumanHeightInCm Source # isConcretely :: SBV HumanHeightInCm -> (HumanHeightInCm -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source # forall_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source # exists :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source # exists_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source # free :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source # free_ :: MonadSymbolic m => m (SBV HumanHeightInCm) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm] Source # symbolic :: MonadSymbolic m => String -> m (SBV HumanHeightInCm) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV HumanHeightInCm] Source # unliteral :: SBV HumanHeightInCm -> Maybe HumanHeightInCm Source # isConcrete :: SBV HumanHeightInCm -> Bool Source # isSymbolic :: SBV HumanHeightInCm -> Bool Source #

type SHumanHeightInCm = SBV HumanHeightInCm Source #

Symbolic version of HumanHeightInCm.

tallestHumanEver :: SHumanHeightInCm Source #

The tallest human ever was 272 cm. We can simply use literal to lift it to the symbolic space.

ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool Source #

Given a distance between a floor and a ceiling, we can see whether the human can stand in that room. Comparison is expressed using sFromIntegral.

problem :: Predicate Source #

Now, suppose we want to see whether we could design a room with a ceiling high enough that any human could stand in it. We have:

>>> sat problem
Satisfiable. Model:
  floorToCeiling =   3 :: Integer
  humanheight    = 255 :: Word16