Newtypes.hs

-----------------------------------------------------------------------------
-- |
-- 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
import Test.QuickCheck(Arbitrary)

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV
#endif

-- | A t'Metres' is a newtype wrapper around 'Integer'.
newtype Metres = Metres Integer deriving (Real, Integral, Num, Enum, Eq, Ord, Arbitrary)

-- | 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 _ = 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    = SI.genMkSymVar KUnbounded
   literal     = SI.genLiteral  KUnbounded
   fromCV      = SI.genFromCV
   minMaxBound = Nothing

-- | 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 (Real, Integral, Num, Enum, Eq, Ord, Bounded, Arbitrary)

-- | 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 _ = KBounded False 16

-- | Similarly here, for the 'SymVal' instance.
instance SymVal HumanHeightInCm where
    mkSymVal = SI.genMkSymVar $ KBounded False 16
    literal  = SI.genLiteral  $ KBounded False 16
    fromCV   = SI.genFromCV

-- | The tallest human ever was 272 cm. We can simply use 'literal' to lift it
-- to the symbolic space.
tallestHumanEver :: SHumanHeightInCm
tallestHumanEver = literal 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 ceiling humanHeight = humanHeight' .< ceiling'
    where -- In a real codebase, the code for comparing these newtypes
          -- should be reusable, perhaps through a typeclass.
        ceiling'     = literal 100 * sFromIntegral ceiling :: SInteger
        humanHeight' = sFromIntegral 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 = do
    ceiling     :: SMetres          <- free "floorToCeiling"
    humanHeight :: SHumanHeightInCm <- free "humanheight"
    constrain $ humanHeight .== tallestHumanEver

    pure $ ceilingHighEnoughForHuman ceiling humanHeight