sbv-9.0: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Curran McConnell
Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Misc.Newtypes

Description

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

Synopsis

Documentation

>>> -- For doctest purposes only:
>>> import Data.SBV

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

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

Num Metres Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Ord Metres Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Real Metres Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

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

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

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

Eq HumanHeightInCm Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Integral HumanHeightInCm Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Num HumanHeightInCm Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Ord HumanHeightInCm Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

Real HumanHeightInCm Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

HasKind HumanHeightInCm Source #

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

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

SymVal HumanHeightInCm Source #

Similarly here, for the SymVal instance.

Instance details

Defined in Documentation.SBV.Examples.Misc.Newtypes

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    = 253 :: Word16