--------------------------------------------------------------------------------
-- 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 t :: Type a
t =
  case Type a
t of
    Bool   -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Int8   -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Int16  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Int32  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Int64  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Word8  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Word16 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Word32 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Word64 -> EqWit a
forall a. Eq a => EqWit a
EqWit
    Float  -> EqWit a
forall a. Eq a => EqWit a
EqWit
    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 -> 
          case Type a -> EqWit a
forall a. Type a -> EqWit a
eqWit Type a
t2 of
            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
                Nothing -> Bool
False
                Just x :: a
x  -> 
                  case Type a
t1 of 
                    -- Hacks for QuickChecking between C and Haskell
                    Float  -> case Type a
t2 of
                                Float -> Float -> Float -> Float -> Bool
forall a. (Num a, Ord a) => a -> a -> a -> Bool
approx Float
floatErr a
Float
x a
Float
b
                                _     -> String -> String -> Bool
forall a. String -> String -> a
impossible "instance Eq UVal"
                                                    "copilot-core"
                    Double -> case Type a
t2 of
                                Double -> Double -> Double -> Double -> Bool
forall a. (Num a, Ord a) => a -> a -> a -> Bool
approx Double
doubleErr a
Double
x a
Double
b
                                _      -> String -> String -> Bool
forall a. String -> String -> a
impossible "instance Eq UVal" 
                                                     "copilot-core"
                    _      -> 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 err :: a
err x :: a
x y :: 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  = 0.0001 :: Float
    doubleErr :: Double
doubleErr = 0.0001 :: Double

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