{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.Utils
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.Utils
  ( pattern Dyn,
    cmpHetero,
    eqHetero,
    cmpHeteroRep,
    eqHeteroRep,
    eqTypeRepBool,
  )
where

import Data.Typeable (cast)
import Type.Reflection

pattern Dyn :: (Typeable a, Typeable b) => a -> b
pattern $mDyn :: forall {r} {a} {b}.
(Typeable a, Typeable b) =>
b -> (a -> r) -> (Void# -> r) -> r
Dyn x <- (cast -> Just x)

cmpHeteroRep :: forall a b. TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep :: forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep TypeRep a
ta TypeRep b
tb a -> a -> Bool
f a
a b
b = case TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
ta TypeRep b
tb of
  Just a :~~: b
HRefl -> a -> a -> Bool
f a
a a
b
b
  Maybe (a :~~: b)
_ -> Bool
False
{-# INLINE cmpHeteroRep #-}

cmpHetero :: forall a b. (Typeable a, Typeable b) => (a -> a -> Bool) -> a -> b -> Bool
cmpHetero :: forall a b.
(Typeable a, Typeable b) =>
(a -> a -> Bool) -> a -> b -> Bool
cmpHetero = TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b)
{-# INLINE cmpHetero #-}

eqHetero :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Bool
eqHetero :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Bool
eqHetero = (a -> a -> Bool) -> a -> b -> Bool
forall a b.
(Typeable a, Typeable b) =>
(a -> a -> Bool) -> a -> b -> Bool
cmpHetero a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE eqHetero #-}

eqHeteroRep :: forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep :: forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep TypeRep a
ta TypeRep b
tb = TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep TypeRep a
ta TypeRep b
tb a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE eqHeteroRep #-}

eqTypeRepBool :: forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool :: forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b = case TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
a TypeRep b
b of
  Just a :~~: b
HRefl -> Bool
True
  Maybe (a :~~: b)
_ -> Bool
False
{-# INLINE eqTypeRepBool #-}