{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeOperators              #-}

{-# OPTIONS_GHC -Wall #-}

-- TODO: Complex Numbers

module Language.Fortran.Model.Types.Match where

import           Data.Typeable

import           Data.Singletons
import           Data.Singletons.TypeLits
import           GHC.TypeLits

import           Data.Vinyl                        hiding ((:~:), Field)

import           Language.Fortran.Model.Singletons
import           Language.Fortran.Model.Types

--------------------------------------------------------------------------------
--  Matching on properties of types
--------------------------------------------------------------------------------

data MatchPrim p k a where
  MatchPrim :: Sing p -> Sing k -> MatchPrim p k a

matchPrim :: Prim p k a -> MatchPrim p k a
matchPrim :: Prim p k a -> MatchPrim p k a
matchPrim = \case
  Prim p k a
PInt8   -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PInt16  -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PInt32  -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PInt64  -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PFloat  -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PDouble -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PBool8  -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PBool16 -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PBool32 -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PBool64 -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing
  Prim p k a
PChar   -> Sing p -> Sing k -> MatchPrim p k a
forall k k k (p :: k) (k :: k) (a :: k).
Sing p -> Sing k -> MatchPrim p k a
MatchPrim Sing p
forall k (a :: k). SingI a => Sing a
sing Sing k
forall k (a :: k). SingI a => Sing a
sing


data MatchPrimD a where
  MatchPrimD :: MatchPrim p k a -> Prim p k a -> MatchPrimD (PrimS a)

-- | Checks if the given type is primitive, and if so returns a proof of that
-- fact.
matchPrimD :: D a -> Maybe (MatchPrimD a)
matchPrimD :: D a -> Maybe (MatchPrimD a)
matchPrimD = \case
  DPrim Prim p k a
p -> MatchPrimD (PrimS a) -> Maybe (MatchPrimD (PrimS a))
forall a. a -> Maybe a
Just (MatchPrim p k a -> Prim p k a -> MatchPrimD (PrimS a)
forall (p :: Precision) (k :: BasicType) a.
MatchPrim p k a -> Prim p k a -> MatchPrimD (PrimS a)
MatchPrimD (Prim p k a -> MatchPrim p k a
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MatchPrim p k a
matchPrim Prim p k a
p) Prim p k a
p)
  D a
_ -> Maybe (MatchPrimD a)
forall a. Maybe a
Nothing


data MakePrim p k where
  MakePrim :: Prim p k a -> MakePrim p k

-- | Tries to make a primitive type with the given precision and kind. Fails if
-- there is no primitive with the given combination.
makePrim :: Sing p -> Sing k -> Maybe (MakePrim p k)
makePrim :: Sing p -> Sing k -> Maybe (MakePrim p k)
makePrim = ((SPrecision p, SBasicType k) -> Maybe (MakePrim p k))
-> SPrecision p -> SBasicType k -> Maybe (MakePrim p k)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((SPrecision p, SBasicType k) -> Maybe (MakePrim p k))
 -> SPrecision p -> SBasicType k -> Maybe (MakePrim p k))
-> ((SPrecision p, SBasicType k) -> Maybe (MakePrim p k))
-> SPrecision p
-> SBasicType k
-> Maybe (MakePrim p k)
forall a b. (a -> b) -> a -> b
$ \case
  (SPrecision p
SP8, SBasicType k
SBTInt)      -> MakePrim 'P8 'BTInt -> Maybe (MakePrim 'P8 'BTInt)
forall a. a -> Maybe a
Just (MakePrim 'P8 'BTInt -> Maybe (MakePrim 'P8 'BTInt))
-> MakePrim 'P8 'BTInt -> Maybe (MakePrim 'P8 'BTInt)
forall a b. (a -> b) -> a -> b
$ Prim 'P8 'BTInt Int8 -> MakePrim 'P8 'BTInt
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P8 'BTInt Int8
PInt8
  (SPrecision p
SP16, SBasicType k
SBTInt)     -> MakePrim 'P16 'BTInt -> Maybe (MakePrim 'P16 'BTInt)
forall a. a -> Maybe a
Just (MakePrim 'P16 'BTInt -> Maybe (MakePrim 'P16 'BTInt))
-> MakePrim 'P16 'BTInt -> Maybe (MakePrim 'P16 'BTInt)
forall a b. (a -> b) -> a -> b
$ Prim 'P16 'BTInt Int16 -> MakePrim 'P16 'BTInt
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P16 'BTInt Int16
PInt16
  (SPrecision p
SP32, SBasicType k
SBTInt)     -> MakePrim 'P32 'BTInt -> Maybe (MakePrim 'P32 'BTInt)
forall a. a -> Maybe a
Just (MakePrim 'P32 'BTInt -> Maybe (MakePrim 'P32 'BTInt))
-> MakePrim 'P32 'BTInt -> Maybe (MakePrim 'P32 'BTInt)
forall a b. (a -> b) -> a -> b
$ Prim 'P32 'BTInt Int32 -> MakePrim 'P32 'BTInt
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P32 'BTInt Int32
PInt32
  (SPrecision p
SP64, SBasicType k
SBTInt)     -> MakePrim 'P64 'BTInt -> Maybe (MakePrim 'P64 'BTInt)
forall a. a -> Maybe a
Just (MakePrim 'P64 'BTInt -> Maybe (MakePrim 'P64 'BTInt))
-> MakePrim 'P64 'BTInt -> Maybe (MakePrim 'P64 'BTInt)
forall a b. (a -> b) -> a -> b
$ Prim 'P64 'BTInt Int64 -> MakePrim 'P64 'BTInt
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P64 'BTInt Int64
PInt64
  (SPrecision p
SP32, SBasicType k
SBTReal)    -> MakePrim 'P32 'BTReal -> Maybe (MakePrim 'P32 'BTReal)
forall a. a -> Maybe a
Just (MakePrim 'P32 'BTReal -> Maybe (MakePrim 'P32 'BTReal))
-> MakePrim 'P32 'BTReal -> Maybe (MakePrim 'P32 'BTReal)
forall a b. (a -> b) -> a -> b
$ Prim 'P32 'BTReal Float -> MakePrim 'P32 'BTReal
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P32 'BTReal Float
PFloat
  (SPrecision p
SP64, SBasicType k
SBTReal)    -> MakePrim 'P64 'BTReal -> Maybe (MakePrim 'P64 'BTReal)
forall a. a -> Maybe a
Just (MakePrim 'P64 'BTReal -> Maybe (MakePrim 'P64 'BTReal))
-> MakePrim 'P64 'BTReal -> Maybe (MakePrim 'P64 'BTReal)
forall a b. (a -> b) -> a -> b
$ Prim 'P64 'BTReal Double -> MakePrim 'P64 'BTReal
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P64 'BTReal Double
PDouble
  (SPrecision p
SP8, SBasicType k
SBTLogical)  -> MakePrim 'P8 'BTLogical -> Maybe (MakePrim 'P8 'BTLogical)
forall a. a -> Maybe a
Just (MakePrim 'P8 'BTLogical -> Maybe (MakePrim 'P8 'BTLogical))
-> MakePrim 'P8 'BTLogical -> Maybe (MakePrim 'P8 'BTLogical)
forall a b. (a -> b) -> a -> b
$ Prim 'P8 'BTLogical Bool8 -> MakePrim 'P8 'BTLogical
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P8 'BTLogical Bool8
PBool8
  (SPrecision p
SP16, SBasicType k
SBTLogical) -> MakePrim 'P16 'BTLogical -> Maybe (MakePrim 'P16 'BTLogical)
forall a. a -> Maybe a
Just (MakePrim 'P16 'BTLogical -> Maybe (MakePrim 'P16 'BTLogical))
-> MakePrim 'P16 'BTLogical -> Maybe (MakePrim 'P16 'BTLogical)
forall a b. (a -> b) -> a -> b
$ Prim 'P16 'BTLogical Bool16 -> MakePrim 'P16 'BTLogical
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P16 'BTLogical Bool16
PBool16
  (SPrecision p
SP32, SBasicType k
SBTLogical) -> MakePrim 'P32 'BTLogical -> Maybe (MakePrim 'P32 'BTLogical)
forall a. a -> Maybe a
Just (MakePrim 'P32 'BTLogical -> Maybe (MakePrim 'P32 'BTLogical))
-> MakePrim 'P32 'BTLogical -> Maybe (MakePrim 'P32 'BTLogical)
forall a b. (a -> b) -> a -> b
$ Prim 'P32 'BTLogical Bool32 -> MakePrim 'P32 'BTLogical
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P32 'BTLogical Bool32
PBool32
  (SPrecision p
SP64, SBasicType k
SBTLogical) -> MakePrim 'P64 'BTLogical -> Maybe (MakePrim 'P64 'BTLogical)
forall a. a -> Maybe a
Just (MakePrim 'P64 'BTLogical -> Maybe (MakePrim 'P64 'BTLogical))
-> MakePrim 'P64 'BTLogical -> Maybe (MakePrim 'P64 'BTLogical)
forall a b. (a -> b) -> a -> b
$ Prim 'P64 'BTLogical Bool64 -> MakePrim 'P64 'BTLogical
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P64 'BTLogical Bool64
PBool64
  (SPrecision p
SP8, SBasicType k
SBTChar)     -> MakePrim 'P8 'BTChar -> Maybe (MakePrim 'P8 'BTChar)
forall a. a -> Maybe a
Just (MakePrim 'P8 'BTChar -> Maybe (MakePrim 'P8 'BTChar))
-> MakePrim 'P8 'BTChar -> Maybe (MakePrim 'P8 'BTChar)
forall a b. (a -> b) -> a -> b
$ Prim 'P8 'BTChar Char8 -> MakePrim 'P8 'BTChar
forall (p :: Precision) (k :: BasicType) a.
Prim p k a -> MakePrim p k
MakePrim Prim 'P8 'BTChar Char8
PChar
  (SPrecision p, SBasicType k)
_ -> Maybe (MakePrim p k)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
--  Equality of Fortran types
--------------------------------------------------------------------------------

eqSymbol :: forall n1 n2. SSymbol n1 -> SSymbol n2 -> Maybe (n1 :~: n2)
eqSymbol :: SSymbol n1 -> SSymbol n2 -> Maybe (n1 :~: n2)
eqSymbol SSymbol n1
n1 SSymbol n2
n2 = Sing n1
-> (KnownSymbol n1 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing n1
SSymbol n1
n1 ((KnownSymbol n1 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2))
-> (KnownSymbol n1 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2)
forall a b. (a -> b) -> a -> b
$ Sing n2
-> (KnownSymbol n2 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing n2
SSymbol n2
n2 ((KnownSymbol n2 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2))
-> (KnownSymbol n2 => Maybe (n1 :~: n2)) -> Maybe (n1 :~: n2)
forall a b. (a -> b) -> a -> b
$ Proxy n1 -> Proxy n2 -> Maybe (n1 :~: n2)
forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol (Proxy n1
forall k (t :: k). Proxy t
Proxy :: Proxy n1) (Proxy n2
forall k (t :: k). Proxy t
Proxy :: Proxy n2)


eqPrim :: Prim p1 k1 a -> Prim p2 k2 b -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
eqPrim :: Prim p1 k1 a
-> Prim p2 k2 b -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
eqPrim = ((Prim p1 k1 a, Prim p2 k2 b)
 -> Maybe ('(p1, k1, a) :~: '(p2, k2, b)))
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Prim p1 k1 a, Prim p2 k2 b)
  -> Maybe ('(p1, k1, a) :~: '(p2, k2, b)))
 -> Prim p1 k1 a
 -> Prim p2 k2 b
 -> Maybe ('(p1, k1, a) :~: '(p2, k2, b)))
-> ((Prim p1 k1 a, Prim p2 k2 b)
    -> Maybe ('(p1, k1, a) :~: '(p2, k2, b)))
-> Prim p1 k1 a
-> Prim p2 k2 b
-> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
forall a b. (a -> b) -> a -> b
$ \case
  (Prim p1 k1 a
PInt8, Prim p2 k2 b
PInt8) -> ('( 'P8, 'BTInt, Int8) :~: '( 'P8, 'BTInt, Int8))
-> Maybe ('( 'P8, 'BTInt, Int8) :~: '( 'P8, 'BTInt, Int8))
forall a. a -> Maybe a
Just '( 'P8, 'BTInt, Int8) :~: '( 'P8, 'BTInt, Int8)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PInt16, Prim p2 k2 b
PInt16) -> ('( 'P16, 'BTInt, Int16) :~: '( 'P16, 'BTInt, Int16))
-> Maybe ('( 'P16, 'BTInt, Int16) :~: '( 'P16, 'BTInt, Int16))
forall a. a -> Maybe a
Just '( 'P16, 'BTInt, Int16) :~: '( 'P16, 'BTInt, Int16)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PInt32, Prim p2 k2 b
PInt32) -> ('( 'P32, 'BTInt, Int32) :~: '( 'P32, 'BTInt, Int32))
-> Maybe ('( 'P32, 'BTInt, Int32) :~: '( 'P32, 'BTInt, Int32))
forall a. a -> Maybe a
Just '( 'P32, 'BTInt, Int32) :~: '( 'P32, 'BTInt, Int32)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PInt64, Prim p2 k2 b
PInt64) -> ('( 'P64, 'BTInt, Int64) :~: '( 'P64, 'BTInt, Int64))
-> Maybe ('( 'P64, 'BTInt, Int64) :~: '( 'P64, 'BTInt, Int64))
forall a. a -> Maybe a
Just '( 'P64, 'BTInt, Int64) :~: '( 'P64, 'BTInt, Int64)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PBool8, Prim p2 k2 b
PBool8) -> ('( 'P8, 'BTLogical, Bool8) :~: '( 'P8, 'BTLogical, Bool8))
-> Maybe
     ('( 'P8, 'BTLogical, Bool8) :~: '( 'P8, 'BTLogical, Bool8))
forall a. a -> Maybe a
Just '( 'P8, 'BTLogical, Bool8) :~: '( 'P8, 'BTLogical, Bool8)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PBool16, Prim p2 k2 b
PBool16) -> ('( 'P16, 'BTLogical, Bool16) :~: '( 'P16, 'BTLogical, Bool16))
-> Maybe
     ('( 'P16, 'BTLogical, Bool16) :~: '( 'P16, 'BTLogical, Bool16))
forall a. a -> Maybe a
Just '( 'P16, 'BTLogical, Bool16) :~: '( 'P16, 'BTLogical, Bool16)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PBool32, Prim p2 k2 b
PBool32) -> ('( 'P32, 'BTLogical, Bool32) :~: '( 'P32, 'BTLogical, Bool32))
-> Maybe
     ('( 'P32, 'BTLogical, Bool32) :~: '( 'P32, 'BTLogical, Bool32))
forall a. a -> Maybe a
Just '( 'P32, 'BTLogical, Bool32) :~: '( 'P32, 'BTLogical, Bool32)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PBool64, Prim p2 k2 b
PBool64) -> ('( 'P64, 'BTLogical, Bool64) :~: '( 'P64, 'BTLogical, Bool64))
-> Maybe
     ('( 'P64, 'BTLogical, Bool64) :~: '( 'P64, 'BTLogical, Bool64))
forall a. a -> Maybe a
Just '( 'P64, 'BTLogical, Bool64) :~: '( 'P64, 'BTLogical, Bool64)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PFloat, Prim p2 k2 b
PFloat) -> ('( 'P32, 'BTReal, Float) :~: '( 'P32, 'BTReal, Float))
-> Maybe ('( 'P32, 'BTReal, Float) :~: '( 'P32, 'BTReal, Float))
forall a. a -> Maybe a
Just '( 'P32, 'BTReal, Float) :~: '( 'P32, 'BTReal, Float)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PDouble, Prim p2 k2 b
PDouble) -> ('( 'P64, 'BTReal, Double) :~: '( 'P64, 'BTReal, Double))
-> Maybe ('( 'P64, 'BTReal, Double) :~: '( 'P64, 'BTReal, Double))
forall a. a -> Maybe a
Just '( 'P64, 'BTReal, Double) :~: '( 'P64, 'BTReal, Double)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a
PChar, Prim p2 k2 b
PChar) -> ('( 'P8, 'BTChar, Char8) :~: '( 'P8, 'BTChar, Char8))
-> Maybe ('( 'P8, 'BTChar, Char8) :~: '( 'P8, 'BTChar, Char8))
forall a. a -> Maybe a
Just '( 'P8, 'BTChar, Char8) :~: '( 'P8, 'BTChar, Char8)
forall k (a :: k). a :~: a
Refl
  (Prim p1 k1 a, Prim p2 k2 b)
_ -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
forall a. Maybe a
Nothing


eqField :: (forall x y. f x -> g y -> Maybe (x :~: y)) -> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2)
eqField :: (forall (x :: k) (y :: k). f x -> g y -> Maybe (x :~: y))
-> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2)
eqField forall (x :: k) (y :: k). f x -> g y -> Maybe (x :~: y)
eqVals = ((Field f p1, Field g p2) -> Maybe (p1 :~: p2))
-> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Field f p1, Field g p2) -> Maybe (p1 :~: p2))
 -> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2))
-> ((Field f p1, Field g p2) -> Maybe (p1 :~: p2))
-> Field f p1
-> Field g p2
-> Maybe (p1 :~: p2)
forall a b. (a -> b) -> a -> b
$ \case
  (Field SSymbol name
n1 f a
x1, Field n2 x2) ->
    case (SSymbol name -> SSymbol name -> Maybe (name :~: name)
forall (n1 :: Symbol) (n2 :: Symbol).
SSymbol n1 -> SSymbol n2 -> Maybe (n1 :~: n2)
eqSymbol SSymbol name
n1 SSymbol name
n2, f a -> g a -> Maybe (a :~: a)
forall (x :: k) (y :: k). f x -> g y -> Maybe (x :~: y)
eqVals f a
x1 g a
x2) of
      (Just name :~: name
Refl, Just a :~: a
Refl) -> ('(name, a) :~: '(name, a)) -> Maybe ('(name, a) :~: '(name, a))
forall a. a -> Maybe a
Just '(name, a) :~: '(name, a)
forall k (a :: k). a :~: a
Refl
      (Maybe (name :~: name), Maybe (a :~: a))
_                      -> Maybe (p1 :~: p2)
forall a. Maybe a
Nothing


eqRec :: (forall a b. t a -> t b -> Maybe (a :~: b)) -> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
eqRec :: (forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b))
-> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
eqRec forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b)
eqInside = ((Rec (Field t) fs, Rec (Field t) gs) -> Maybe (fs :~: gs))
-> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Rec (Field t) fs, Rec (Field t) gs) -> Maybe (fs :~: gs))
 -> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs))
-> ((Rec (Field t) fs, Rec (Field t) gs) -> Maybe (fs :~: gs))
-> Rec (Field t) fs
-> Rec (Field t) gs
-> Maybe (fs :~: gs)
forall a b. (a -> b) -> a -> b
$ \case
  (Rec (Field t) fs
RNil, Rec (Field t) gs
RNil) -> ('[] :~: '[]) -> Maybe ('[] :~: '[])
forall a. a -> Maybe a
Just '[] :~: '[]
forall k (a :: k). a :~: a
Refl
  (Field t r
h1 :& Rec (Field t) rs
t1, h2 :& t2) ->
    case ((forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b))
-> Field t r -> Field t r -> Maybe (r :~: r)
forall k (f :: k -> *) (g :: k -> *) (p1 :: (Symbol, k))
       (p2 :: (Symbol, k)).
(forall (x :: k) (y :: k). f x -> g y -> Maybe (x :~: y))
-> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2)
eqField forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b)
eqInside Field t r
h1 Field t r
h2, (forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b))
-> Rec (Field t) rs -> Rec (Field t) rs -> Maybe (rs :~: rs)
forall k (t :: k -> *) (fs :: [(Symbol, k)]) (gs :: [(Symbol, k)]).
(forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b))
-> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
eqRec forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b)
eqInside Rec (Field t) rs
t1 Rec (Field t) rs
t2) of
      (Just r :~: r
Refl, Just rs :~: rs
Refl) -> ((r : rs) :~: (r : rs)) -> Maybe ((r : rs) :~: (r : rs))
forall a. a -> Maybe a
Just (r : rs) :~: (r : rs)
forall k (a :: k). a :~: a
Refl
      (Maybe (r :~: r), Maybe (rs :~: rs))
_                      -> Maybe (fs :~: gs)
forall a. Maybe a
Nothing
  (Rec (Field t) fs, Rec (Field t) gs)
_ -> Maybe (fs :~: gs)
forall a. Maybe a
Nothing


eqArrValue :: ArrValue a -> ArrValue b -> Maybe (a :~: b)
eqArrValue :: ArrValue a -> ArrValue b -> Maybe (a :~: b)
eqArrValue ArrValue a
a1 ArrValue b
a2 = D a -> D b -> Maybe (a :~: b)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD (ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue ArrValue a
a1) (ArrValue b -> D b
forall a. ArrValue a -> D a
dArrValue ArrValue b
a2)


eqD :: D a -> D b -> Maybe (a :~: b)
eqD :: D a -> D b -> Maybe (a :~: b)
eqD = ((D a, D b) -> Maybe (a :~: b)) -> D a -> D b -> Maybe (a :~: b)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((D a, D b) -> Maybe (a :~: b)) -> D a -> D b -> Maybe (a :~: b))
-> ((D a, D b) -> Maybe (a :~: b)) -> D a -> D b -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case
  (DPrim Prim p k a
p1, DPrim p2) ->
    case Prim p k a -> Prim p k a -> Maybe ('(p, k, a) :~: '(p, k, a))
forall (p1 :: Precision) (k1 :: BasicType) a (p2 :: Precision)
       (k2 :: BasicType) b.
Prim p1 k1 a
-> Prim p2 k2 b -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
eqPrim Prim p k a
p1 Prim p k a
p2 of
      Just '(p, k, a) :~: '(p, k, a)
Refl -> (PrimS a :~: PrimS a) -> Maybe (PrimS a :~: PrimS a)
forall a. a -> Maybe a
Just PrimS a :~: PrimS a
forall k (a :: k). a :~: a
Refl
      Maybe ('(p, k, a) :~: '(p, k, a))
_         -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  (DArray (Index Prim p 'BTInt a
i1) ArrValue a
av1, DArray (Index i2) av2) ->
    case (Prim p 'BTInt a
-> Prim p 'BTInt a -> Maybe ('(p, 'BTInt, a) :~: '(p, 'BTInt, a))
forall (p1 :: Precision) (k1 :: BasicType) a (p2 :: Precision)
       (k2 :: BasicType) b.
Prim p1 k1 a
-> Prim p2 k2 b -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
eqPrim Prim p 'BTInt a
i1 Prim p 'BTInt a
i2, ArrValue a -> ArrValue a -> Maybe (a :~: a)
forall a b. ArrValue a -> ArrValue b -> Maybe (a :~: b)
eqArrValue ArrValue a
av1 ArrValue a
av2) of
      (Just '(p, 'BTInt, a) :~: '(p, 'BTInt, a)
Refl, Just a :~: a
Refl) -> (Array (PrimS a) a :~: Array (PrimS a) a)
-> Maybe (Array (PrimS a) a :~: Array (PrimS a) a)
forall a. a -> Maybe a
Just Array (PrimS a) a :~: Array (PrimS a) a
forall k (a :: k). a :~: a
Refl
      (Maybe ('(p, 'BTInt, a) :~: '(p, 'BTInt, a)), Maybe (a :~: a))
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  (DData SSymbol name
n1 Rec (Field D) fs
r1, DData n2 r2) ->
    case (SSymbol name -> SSymbol name -> Maybe (name :~: name)
forall (n1 :: Symbol) (n2 :: Symbol).
SSymbol n1 -> SSymbol n2 -> Maybe (n1 :~: n2)
eqSymbol SSymbol name
n1 SSymbol name
n2, (forall a b. D a -> D b -> Maybe (a :~: b))
-> Rec (Field D) fs -> Rec (Field D) fs -> Maybe (fs :~: fs)
forall k (t :: k -> *) (fs :: [(Symbol, k)]) (gs :: [(Symbol, k)]).
(forall (a :: k) (b :: k). t a -> t b -> Maybe (a :~: b))
-> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
eqRec forall a b. D a -> D b -> Maybe (a :~: b)
eqD Rec (Field D) fs
r1 Rec (Field D) fs
r2) of
      (Just name :~: name
Refl, Just fs :~: fs
Refl) -> (Record name fs :~: Record name fs)
-> Maybe (Record name fs :~: Record name fs)
forall a. a -> Maybe a
Just Record name fs :~: Record name fs
forall k (a :: k). a :~: a
Refl
      (Maybe (name :~: name), Maybe (fs :~: fs))
_                      -> Maybe (a :~: b)
forall a. Maybe a
Nothing
  (D a, D b)
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing


dcast :: D a -> D b -> f a -> Maybe (f b)
dcast :: D a -> D b -> f a -> Maybe (f b)
dcast D a
d1 D b
d2 = case D a -> D b -> Maybe (a :~: b)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D b
d2 of
  Just a :~: b
Refl -> f a -> Maybe (f b)
forall a. a -> Maybe a
Just
  Maybe (a :~: b)
_         -> Maybe (f b) -> f a -> Maybe (f b)
forall a b. a -> b -> a
const Maybe (f b)
forall a. Maybe a
Nothing