-----------------------------------------------------------------------------
-- |
-- 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
Num Metres -> Ord Metres -> (Metres -> Rational) -> Real Metres
Metres -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Metres -> Rational
$ctoRational :: Metres -> Rational
$cp2Real :: Ord Metres
$cp1Real :: Num Metres
Real, Enum Metres
Real Metres
Real Metres
-> Enum Metres
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> (Metres, Metres))
-> (Metres -> Metres -> (Metres, Metres))
-> (Metres -> Integer)
-> Integral 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
$cp2Integral :: Enum Metres
$cp1Integral :: Real Metres
Integral, Integer -> Metres
Metres -> Metres
Metres -> Metres -> Metres
(Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres)
-> (Metres -> Metres)
-> (Metres -> Metres)
-> (Integer -> Metres)
-> Num 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]
(Metres -> Metres)
-> (Metres -> Metres)
-> (Int -> Metres)
-> (Metres -> Int)
-> (Metres -> [Metres])
-> (Metres -> Metres -> [Metres])
-> (Metres -> Metres -> [Metres])
-> (Metres -> Metres -> Metres -> [Metres])
-> Enum 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
(Metres -> Metres -> Bool)
-> (Metres -> Metres -> Bool) -> Eq Metres
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
Eq Metres
-> (Metres -> Metres -> Ordering)
-> (Metres -> Metres -> Bool)
-> (Metres -> Metres -> Bool)
-> (Metres -> Metres -> Bool)
-> (Metres -> Metres -> Bool)
-> (Metres -> Metres -> Metres)
-> (Metres -> Metres -> Metres)
-> Ord 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
$cp1Ord :: Eq Metres
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 :: VarContext -> Maybe String -> m (SBV Metres)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Metres)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
SI.genMkSymVar Kind
KUnbounded
   literal :: Metres -> SBV Metres
literal  = Kind -> Metres -> SBV Metres
forall a b. Integral a => Kind -> a -> SBV b
SI.genLiteral  Kind
KUnbounded
   fromCV :: CV -> Metres
fromCV   = CV -> Metres
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
Num HumanHeightInCm
-> Ord HumanHeightInCm
-> (HumanHeightInCm -> Rational)
-> Real HumanHeightInCm
HumanHeightInCm -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: HumanHeightInCm -> Rational
$ctoRational :: HumanHeightInCm -> Rational
$cp2Real :: Ord HumanHeightInCm
$cp1Real :: Num HumanHeightInCm
Real, Enum HumanHeightInCm
Real HumanHeightInCm
Real HumanHeightInCm
-> Enum HumanHeightInCm
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm))
-> (HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm))
-> (HumanHeightInCm -> Integer)
-> Integral 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
$cp2Integral :: Enum HumanHeightInCm
$cp1Integral :: Real HumanHeightInCm
Integral, Integer -> HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm
HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
(HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm)
-> (Integer -> HumanHeightInCm)
-> Num 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]
(HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm)
-> (Int -> HumanHeightInCm)
-> (HumanHeightInCm -> Int)
-> (HumanHeightInCm -> [HumanHeightInCm])
-> (HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
-> (HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
-> (HumanHeightInCm
    -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
-> Enum 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
(HumanHeightInCm -> HumanHeightInCm -> Bool)
-> (HumanHeightInCm -> HumanHeightInCm -> Bool)
-> Eq HumanHeightInCm
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
Eq HumanHeightInCm
-> (HumanHeightInCm -> HumanHeightInCm -> Ordering)
-> (HumanHeightInCm -> HumanHeightInCm -> Bool)
-> (HumanHeightInCm -> HumanHeightInCm -> Bool)
-> (HumanHeightInCm -> HumanHeightInCm -> Bool)
-> (HumanHeightInCm -> HumanHeightInCm -> Bool)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
-> Ord 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
$cp1Ord :: Eq HumanHeightInCm
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 :: VarContext -> Maybe String -> m (SBV HumanHeightInCm)
mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV HumanHeightInCm)
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
SI.genMkSymVar (Kind -> VarContext -> Maybe String -> m (SBV HumanHeightInCm))
-> Kind -> VarContext -> Maybe String -> m (SBV HumanHeightInCm)
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
    literal :: HumanHeightInCm -> SBV HumanHeightInCm
literal  = Kind -> HumanHeightInCm -> SBV HumanHeightInCm
forall a b. Integral a => Kind -> a -> SBV b
SI.genLiteral  (Kind -> HumanHeightInCm -> SBV HumanHeightInCm)
-> Kind -> HumanHeightInCm -> SBV HumanHeightInCm
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
    fromCV :: CV -> HumanHeightInCm
fromCV   = CV -> HumanHeightInCm
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 :: SBV HumanHeightInCm
tallestHumanEver = HumanHeightInCm -> SBV HumanHeightInCm
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 -> SBV HumanHeightInCm -> SBool
ceilingHighEnoughForHuman SBV Metres
ceiling SBV HumanHeightInCm
humanHeight = SInteger
humanHeight' SInteger -> SInteger -> SBool
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'     = Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
100 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SBV Metres -> SInteger
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' = SBV HumanHeightInCm -> SInteger
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV HumanHeightInCm
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    = 253 :: Word16
problem :: Predicate
problem :: Predicate
problem = do
    SBV Metres
ceiling     :: SMetres          <- String -> Symbolic (SBV Metres)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"floorToCeiling"
    SBV HumanHeightInCm
humanHeight :: SHumanHeightInCm <- String -> Symbolic (SBV HumanHeightInCm)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"humanheight"
    SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV HumanHeightInCm
humanHeight SBV HumanHeightInCm -> SBV HumanHeightInCm -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SBV HumanHeightInCm
tallestHumanEver

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