UnsafeFunctionEquality.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Examples.Basics.UnsafeFunctionEquality
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-- Lifting of equality directly to functions, i.e., making functions
-- instance of the Haskell Eq class. This is unsafe (due to the use of
-- unsafePerformIO), but it's actually more akin to trusted FFI calls,
-- and can be marked "pure"
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

module Data.SBV.Examples.Basics.UnsafeFunctionEquality where

import System.IO.Unsafe (unsafePerformIO)

import Data.SBV

instance Equality (a -> b) => Eq (a -> b) where
  f == g = unsafePerformIO $ do
              r <- f === g
              case r of
                ThmResult (Unsatisfiable _) -> return True
                ThmResult (Satisfiable _ _) -> return False
                _                           ->  error $ "Cannot decide function equality!"


-- tests

type B = SWord8

f11 :: B -> B
f11 x = x

f12 :: B -> (B, B)
f12 x = (x, x)

f21 :: (B, B) -> B
f21 (x, y) = x + y

f22 :: (B, B) -> (B, B)
f22 (x, y) = (x, y)

f31 :: B -> B -> B
f31 x y = x + y

f32 :: B -> B -> (B, B)
f32 x y = (x, y)

f33 :: B -> B -> B -> (B, B, B)
f33 x y z = (x, y, z)


t :: [Bool]
t =  [ f11 == f11
     , f12 == f12
     , f21 == f21
     , f22 == f22
     , f31 == f31
     , f32 == f32
     , f33 == f33
     , f33 /= f33
     ]