-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Newtypes
-- Copyright : (c) Curran McConnell
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how to create symbolic newtypes with the same behaviour as
-- their wrapped type.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror           #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}

module Documentation.SBV.Examples.Misc.Newtypes where

import Prelude hiding (ceiling)
import Data.SBV
import qualified Data.SBV.Internals as SI

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

-- | A 'Metres' is a newtype wrapper around 'Integer'.
newtype Metres = Metres Integer deriving (Num Metres
Ord Metres
Metres -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Metres -> Rational
$ctoRational :: Metres -> Rational
Real, Enum Metres
Real Metres
Metres -> Integer
Metres -> Metres -> (Metres, Metres)
Metres -> Metres -> Metres
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Metres -> Integer
$ctoInteger :: Metres -> Integer
divMod :: Metres -> Metres -> (Metres, Metres)
$cdivMod :: Metres -> Metres -> (Metres, Metres)
quotRem :: Metres -> Metres -> (Metres, Metres)
$cquotRem :: Metres -> Metres -> (Metres, Metres)
mod :: Metres -> Metres -> Metres
$cmod :: Metres -> Metres -> Metres
div :: Metres -> Metres -> Metres
$cdiv :: Metres -> Metres -> Metres
rem :: Metres -> Metres -> Metres
$crem :: Metres -> Metres -> Metres
quot :: Metres -> Metres -> Metres
$cquot :: Metres -> Metres -> Metres
Integral, Integer -> Metres
Metres -> Metres
Metres -> Metres -> Metres
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Metres
$cfromInteger :: Integer -> Metres
signum :: Metres -> Metres
$csignum :: Metres -> Metres
abs :: Metres -> Metres
$cabs :: Metres -> Metres
negate :: Metres -> Metres
$cnegate :: Metres -> Metres
* :: Metres -> Metres -> Metres
$c* :: Metres -> Metres -> Metres
- :: Metres -> Metres -> Metres
$c- :: Metres -> Metres -> Metres
+ :: Metres -> Metres -> Metres
$c+ :: Metres -> Metres -> Metres
Num, Int -> Metres
Metres -> Int
Metres -> [Metres]
Metres -> Metres
Metres -> Metres -> [Metres]
Metres -> Metres -> Metres -> [Metres]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Metres -> Metres -> Metres -> [Metres]
$cenumFromThenTo :: Metres -> Metres -> Metres -> [Metres]
enumFromTo :: Metres -> Metres -> [Metres]
$cenumFromTo :: Metres -> Metres -> [Metres]
enumFromThen :: Metres -> Metres -> [Metres]
$cenumFromThen :: Metres -> Metres -> [Metres]
enumFrom :: Metres -> [Metres]
$cenumFrom :: Metres -> [Metres]
fromEnum :: Metres -> Int
$cfromEnum :: Metres -> Int
toEnum :: Int -> Metres
$ctoEnum :: Int -> Metres
pred :: Metres -> Metres
$cpred :: Metres -> Metres
succ :: Metres -> Metres
$csucc :: Metres -> Metres
Enum, Metres -> Metres -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Metres -> Metres -> Bool
$c/= :: Metres -> Metres -> Bool
== :: Metres -> Metres -> Bool
$c== :: Metres -> Metres -> Bool
Eq, Eq Metres
Metres -> Metres -> Bool
Metres -> Metres -> Ordering
Metres -> Metres -> Metres
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Metres -> Metres -> Metres
$cmin :: Metres -> Metres -> Metres
max :: Metres -> Metres -> Metres
$cmax :: Metres -> Metres -> Metres
>= :: Metres -> Metres -> Bool
$c>= :: Metres -> Metres -> Bool
> :: Metres -> Metres -> Bool
$c> :: Metres -> Metres -> Bool
<= :: Metres -> Metres -> Bool
$c<= :: Metres -> Metres -> Bool
< :: Metres -> Metres -> Bool
$c< :: Metres -> Metres -> Bool
compare :: Metres -> Metres -> Ordering
$ccompare :: Metres -> Metres -> Ordering
Ord)

-- | Symbolic version of 'Metres'.
type SMetres   = SBV Metres

-- | To use 'Metres' symbolically, we associate it with the underlying symbolic
-- type's kind.
instance HasKind Metres where
   kindOf :: Metres -> Kind
kindOf Metres
_ = Kind
KUnbounded

-- | The 'SymVal' instance simply uses stock definitions. This is always
-- possible for newtypes that simply wrap over an existing symbolic type.
instance SymVal Metres where
   mkSymVal :: forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m (SBV Metres)
mkSymVal = forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
SI.genMkSymVar Kind
KUnbounded
   literal :: Metres -> SBV Metres
literal  = forall a b. Integral a => Kind -> a -> SBV b
SI.genLiteral  Kind
KUnbounded
   fromCV :: CV -> Metres
fromCV   = forall a. Integral a => CV -> a
SI.genFromCV

-- | 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.
newtype HumanHeightInCm = HumanHeightInCm Word16 deriving (Num HumanHeightInCm
Ord HumanHeightInCm
HumanHeightInCm -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: HumanHeightInCm -> Rational
$ctoRational :: HumanHeightInCm -> Rational
Real, Enum HumanHeightInCm
Real HumanHeightInCm
HumanHeightInCm -> Integer
HumanHeightInCm
-> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: HumanHeightInCm -> Integer
$ctoInteger :: HumanHeightInCm -> Integer
divMod :: HumanHeightInCm
-> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
$cdivMod :: HumanHeightInCm
-> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
quotRem :: HumanHeightInCm
-> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
$cquotRem :: HumanHeightInCm
-> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
mod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$cmod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
div :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$cdiv :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
rem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$crem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
quot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$cquot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
Integral, Integer -> HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> HumanHeightInCm
$cfromInteger :: Integer -> HumanHeightInCm
signum :: HumanHeightInCm -> HumanHeightInCm
$csignum :: HumanHeightInCm -> HumanHeightInCm
abs :: HumanHeightInCm -> HumanHeightInCm
$cabs :: HumanHeightInCm -> HumanHeightInCm
negate :: HumanHeightInCm -> HumanHeightInCm
$cnegate :: HumanHeightInCm -> HumanHeightInCm
* :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$c* :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
- :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$c- :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
+ :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$c+ :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
Num, Int -> HumanHeightInCm
HumanHeightInCm -> Int
HumanHeightInCm -> [HumanHeightInCm]
HumanHeightInCm -> HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
HumanHeightInCm
-> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: HumanHeightInCm
-> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
$cenumFromThenTo :: HumanHeightInCm
-> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
enumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
$cenumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
enumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
$cenumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
enumFrom :: HumanHeightInCm -> [HumanHeightInCm]
$cenumFrom :: HumanHeightInCm -> [HumanHeightInCm]
fromEnum :: HumanHeightInCm -> Int
$cfromEnum :: HumanHeightInCm -> Int
toEnum :: Int -> HumanHeightInCm
$ctoEnum :: Int -> HumanHeightInCm
pred :: HumanHeightInCm -> HumanHeightInCm
$cpred :: HumanHeightInCm -> HumanHeightInCm
succ :: HumanHeightInCm -> HumanHeightInCm
$csucc :: HumanHeightInCm -> HumanHeightInCm
Enum, HumanHeightInCm -> HumanHeightInCm -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c/= :: HumanHeightInCm -> HumanHeightInCm -> Bool
== :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c== :: HumanHeightInCm -> HumanHeightInCm -> Bool
Eq, Eq HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm -> Bool
HumanHeightInCm -> HumanHeightInCm -> Ordering
HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$cmin :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
max :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
$cmax :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
>= :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c>= :: HumanHeightInCm -> HumanHeightInCm -> Bool
> :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c> :: HumanHeightInCm -> HumanHeightInCm -> Bool
<= :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c<= :: HumanHeightInCm -> HumanHeightInCm -> Bool
< :: HumanHeightInCm -> HumanHeightInCm -> Bool
$c< :: HumanHeightInCm -> HumanHeightInCm -> Bool
compare :: HumanHeightInCm -> HumanHeightInCm -> Ordering
$ccompare :: HumanHeightInCm -> HumanHeightInCm -> Ordering
Ord)

-- | Symbolic version of 'HumanHeightInCm'.
type SHumanHeightInCm = SBV HumanHeightInCm

-- | Symbolic instance simply follows the underlying type, just like 'Metres'.
instance HasKind HumanHeightInCm where
    kindOf :: HumanHeightInCm -> Kind
kindOf HumanHeightInCm
_ = Bool -> Int -> Kind
KBounded Bool
False Int
16

-- | Similarly here, for the 'SymVal' instance.
instance SymVal HumanHeightInCm where
    mkSymVal :: forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m SHumanHeightInCm
mkSymVal = forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
SI.genMkSymVar forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
    literal :: HumanHeightInCm -> SHumanHeightInCm
literal  = forall a b. Integral a => Kind -> a -> SBV b
SI.genLiteral  forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
    fromCV :: CV -> HumanHeightInCm
fromCV   = forall a. Integral a => CV -> a
SI.genFromCV

-- | The tallest human ever was 272 cm. We can simply use 'literal' to lift it
-- to the symbolic space.
tallestHumanEver :: SHumanHeightInCm
tallestHumanEver :: SHumanHeightInCm
tallestHumanEver = forall a. SymVal a => a -> SBV a
literal HumanHeightInCm
272

-- | 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'.
ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool
ceilingHighEnoughForHuman :: SBV Metres -> SHumanHeightInCm -> SBool
ceilingHighEnoughForHuman SBV Metres
ceiling SHumanHeightInCm
humanHeight = SInteger
humanHeight' forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
ceiling'
    where -- In a real codebase, the code for comparing these newtypes
          -- should be reusable, perhaps through a typeclass.
        ceiling' :: SInteger
ceiling'     = forall a. SymVal a => a -> SBV a
literal Integer
100 forall a. Num a => a -> a -> a
* forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV Metres
ceiling :: SInteger
        humanHeight' :: SInteger
humanHeight' = forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SHumanHeightInCm
humanHeight :: SInteger

-- | 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
problem :: Predicate
problem :: Predicate
problem = do
    SBV Metres
ceiling     :: SMetres          <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"floorToCeiling"
    SHumanHeightInCm
humanHeight :: SHumanHeightInCm <- forall a. SymVal a => String -> Symbolic (SBV a)
free String
"humanheight"
    forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SHumanHeightInCm
humanHeight forall a. OrdSymbolic a => a -> a -> SBool
.<= SHumanHeightInCm
tallestHumanEver

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SBV Metres -> SHumanHeightInCm -> SBool
ceilingHighEnoughForHuman SBV Metres
ceiling SHumanHeightInCm
humanHeight