{-# 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
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)
type SMetres = SBV Metres
instance HasKind Metres where
kindOf :: Metres -> Kind
kindOf Metres
_ = Kind
KUnbounded
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
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)
type SHumanHeightInCm = SBV HumanHeightInCm
instance HasKind HumanHeightInCm where
kindOf :: HumanHeightInCm -> Kind
kindOf HumanHeightInCm
_ = Bool -> Int -> Kind
KBounded Bool
False Int
16
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
tallestHumanEver :: SHumanHeightInCm
tallestHumanEver :: SBV HumanHeightInCm
tallestHumanEver = HumanHeightInCm -> SBV HumanHeightInCm
forall a. SymVal a => a -> SBV a
literal HumanHeightInCm
272
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
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
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