Documentation.SBV.Examples.Misc.Newtypes

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

Documentation

newtype Metres

A Metres is a newtype wrapper around Integer.

Constructors

Metres Integer

Instances

Enum Metres

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

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

(==) :: Metres -> Metres -> Bool

(/=) :: Metres -> Metres -> Bool

Integral Metres

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

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

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

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

toRational :: Metres -> Rational

HasKind Metres

To use Metres symbolically, we associate it with the underlying symbolic type's kind.

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: Metres -> Kind

hasSign :: Metres -> Bool

intSizeOf :: Metres -> Int

isBoolean :: Metres -> Bool

isBounded :: Metres -> Bool

isReal :: Metres -> Bool

isFloat :: Metres -> Bool

isDouble :: Metres -> Bool

isUnbounded :: Metres -> Bool

isUserSort :: Metres -> Bool

isChar :: Metres -> Bool

isString :: Metres -> Bool

isList :: Metres -> Bool

isSet :: Metres -> Bool

isTuple :: Metres -> Bool

isMaybe :: Metres -> Bool

isEither :: Metres -> Bool

showType :: Metres -> String

SymVal Metres

The SymVal instance simply uses stock definitions. This is always possible for newtypes that simply wrap over an existing symbolic type.

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Metres)

literal :: Metres -> SBV Metres

fromCV :: CV -> Metres

isConcretely :: SBV Metres -> (Metres -> Bool) -> Bool

forall :: MonadSymbolic m => String -> m (SBV Metres)

forall_ :: MonadSymbolic m => m (SBV Metres)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Metres]

exists :: MonadSymbolic m => String -> m (SBV Metres)

exists_ :: MonadSymbolic m => m (SBV Metres)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Metres]

free :: MonadSymbolic m => String -> m (SBV Metres)

free_ :: MonadSymbolic m => m (SBV Metres)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Metres]

symbolic :: MonadSymbolic m => String -> m (SBV Metres)

symbolics :: MonadSymbolic m => [String] -> m [SBV Metres]

unliteral :: SBV Metres -> Maybe Metres

isConcrete :: SBV Metres -> Bool

isSymbolic :: SBV Metres -> Bool

type SMetres = SBV Metres

Symbolic version of Metres.

newtype HumanHeightInCm

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

Enum HumanHeightInCm

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

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

(==) :: HumanHeightInCm -> HumanHeightInCm -> Bool

(/=) :: HumanHeightInCm -> HumanHeightInCm -> Bool

Integral HumanHeightInCm

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

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

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

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

toRational :: HumanHeightInCm -> Rational

HasKind HumanHeightInCm

Symbolic instance simply follows the underlying type, just like Metres.

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

kindOf :: HumanHeightInCm -> Kind

hasSign :: HumanHeightInCm -> Bool

intSizeOf :: HumanHeightInCm -> Int

isBoolean :: HumanHeightInCm -> Bool

isBounded :: HumanHeightInCm -> Bool

isReal :: HumanHeightInCm -> Bool

isFloat :: HumanHeightInCm -> Bool

isDouble :: HumanHeightInCm -> Bool

isUnbounded :: HumanHeightInCm -> Bool

isUserSort :: HumanHeightInCm -> Bool

isChar :: HumanHeightInCm -> Bool

isString :: HumanHeightInCm -> Bool

isList :: HumanHeightInCm -> Bool

isSet :: HumanHeightInCm -> Bool

isTuple :: HumanHeightInCm -> Bool

isMaybe :: HumanHeightInCm -> Bool

isEither :: HumanHeightInCm -> Bool

showType :: HumanHeightInCm -> String

SymVal HumanHeightInCm

Similarly here, for the SymVal instance.

Defined in Documentation.SBV.Examples.Misc.Newtypes

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV HumanHeightInCm)

literal :: HumanHeightInCm -> SBV HumanHeightInCm

fromCV :: CV -> HumanHeightInCm

isConcretely :: SBV HumanHeightInCm -> (HumanHeightInCm -> Bool) -> Bool

forall :: MonadSymbolic m => String -> m (SBV HumanHeightInCm)

forall_ :: MonadSymbolic m => m (SBV HumanHeightInCm)

mkForallVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm]

exists :: MonadSymbolic m => String -> m (SBV HumanHeightInCm)

exists_ :: MonadSymbolic m => m (SBV HumanHeightInCm)

mkExistVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm]

free :: MonadSymbolic m => String -> m (SBV HumanHeightInCm)

free_ :: MonadSymbolic m => m (SBV HumanHeightInCm)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV HumanHeightInCm]

symbolic :: MonadSymbolic m => String -> m (SBV HumanHeightInCm)

symbolics :: MonadSymbolic m => [String] -> m [SBV HumanHeightInCm]

unliteral :: SBV HumanHeightInCm -> Maybe HumanHeightInCm

isConcrete :: SBV HumanHeightInCm -> Bool

isSymbolic :: SBV HumanHeightInCm -> Bool

type SHumanHeightInCm = SBV HumanHeightInCm

Symbolic version of HumanHeightInCm.

tallestHumanEver :: SHumanHeightInCm

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

ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool

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

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