--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

{-# LANGUAGE Safe #-}
{-# LANGUAGE ExistentialQuantification, GADTs #-}

module Copilot.Core.Type.Eq
  ( EqWit (..)
  , eqWit
  , UVal (..)
  ) where

import Copilot.Core.Error (impossible)
import Copilot.Core.Type
import Copilot.Core.Type.Dynamic (fromDyn, toDyn)

--------------------------------------------------------------------------------

data EqWit a = Eq a => EqWit

--------------------------------------------------------------------------------

eqWit :: Type a -> EqWit a
eqWit :: Type a -> EqWit a
eqWit Type a
t =
  case Type a
t of
    Type a
Bool   -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Int8   -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Int16  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Int32  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Int64  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Word8  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Word16 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Word32 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Word64 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Float  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Type a
Double -> EqWit a
forall a. Eq a => EqWit a
EqWit

--------------------------------------------------------------------------------

data UVal = forall a. UVal
  { ()
uType :: Type a
  , ()
uVal  :: a
  }

--------------------------------------------------------------------------------

instance Eq UVal where
  == :: UVal -> UVal -> Bool
(==) UVal { uType :: ()
uType = Type a
t1
            , uVal :: ()
uVal = a
a } 
       UVal { uType :: ()
uType = Type a
t2
            , uVal :: ()
uVal = a
b }
    = case Type a -> EqWit a
forall a. Type a -> EqWit a
eqWit Type a
t1 of
        EqWit a
EqWit -> 
          case Type a -> EqWit a
forall a. Type a -> EqWit a
eqWit Type a
t2 of
            EqWit a
EqWit -> 
              let dyn1 :: Dynamic Type
dyn1 = Type a -> a -> Dynamic Type
forall (t :: * -> *) a. t a -> a -> Dynamic t
toDyn Type a
t1 a
a in
              case Type a -> Dynamic Type -> Maybe a
forall (t :: * -> *) a. EqualType t => t a -> Dynamic t -> Maybe a
fromDyn Type a
t2 Dynamic Type
dyn1 of
                Maybe a
Nothing -> Bool
False
                Just a
x  -> 
                  case Type a
t1 of 
                    -- Hacks for QuickChecking between C and Haskell
                    Type a
Float  -> case Type a
t2 of
                                Type a
Float -> Float -> Float -> Float -> Bool
forall a. (Num a, Ord a) => a -> a -> a -> Bool
approx Float
floatErr a
Float
x a
Float
b
                                Type a
_     -> String -> String -> Bool
forall a. String -> String -> a
impossible String
"instance Eq UVal"
                                                    String
"copilot-core"
                    Type a
Double -> case Type a
t2 of
                                Type a
Double -> Double -> Double -> Double -> Bool
forall a. (Num a, Ord a) => a -> a -> a -> Bool
approx Double
doubleErr a
Double
x a
Double
b
                                Type a
_      -> String -> String -> Bool
forall a. String -> String -> a
impossible String
"instance Eq UVal" 
                                                     String
"copilot-core"
                    Type a
_      -> a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
    where 
    approx :: (Num a, Ord a) => a -> a -> a -> Bool
    approx :: a -> a -> a -> Bool
approx a
err a
x a
y = a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
err Bool -> Bool -> Bool
&& a
y a -> a -> a
forall a. Num a => a -> a -> a
- a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
err
    floatErr :: Float
floatErr  = Float
0.0001 :: Float
    doubleErr :: Double
doubleErr = Double
0.0001 :: Double

--------------------------------------------------------------------------------