-----------------------------------------------------------------------------
-- |
-- 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.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                        #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}

{-# OPTIONS_GHC -Wall -Werror           #-}

module Documentation.SBV.Examples.Misc.Newtypes where

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

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
#endif

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

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

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

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

-- | Symbolic instance simply follows the underlying type, just like t'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 = Kind -> VarContext -> Maybe String -> m SHumanHeightInCm
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
SI.genMkSymVar (Kind -> VarContext -> Maybe String -> m SHumanHeightInCm)
-> Kind -> VarContext -> Maybe String -> m SHumanHeightInCm
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
    literal :: HumanHeightInCm -> SHumanHeightInCm
literal  = Kind -> HumanHeightInCm -> SHumanHeightInCm
forall a b. Integral a => Kind -> a -> SBV b
SI.genLiteral  (Kind -> HumanHeightInCm -> SHumanHeightInCm)
-> Kind -> HumanHeightInCm -> SHumanHeightInCm
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 :: SHumanHeightInCm
tallestHumanEver = HumanHeightInCm -> SHumanHeightInCm
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' 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' = SHumanHeightInCm -> SInteger
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    = 272 :: Word16
problem :: Predicate
problem :: Predicate
problem = do
    ceiling     :: SMetres          <- String -> Symbolic (SBV Metres)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"floorToCeiling"
    humanHeight :: SHumanHeightInCm <- free "humanheight"
    constrain $ humanHeight .== tallestHumanEver

    return $ ceilingHighEnoughForHuman ceiling humanHeight