{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP                 #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PatternGuards       #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
{-# OPTIONS_HADDOCK hide #-}
-- |
-- Module      : Data.Array.Accelerate.Analysis.Match
-- Copyright   : [2012..2020] The Accelerate Team
-- License     : BSD3
--
-- Maintainer  : Trevor L. McDonell <trevor.mcdonell@gmail.com>
-- Stability   : experimental
-- Portability : non-portable (GHC extensions)
--

module Data.Array.Accelerate.Analysis.Match (

  -- matching expressions
  MatchAcc,
  (:~:)(..),
  matchPreOpenAcc,
  matchPreOpenAfun,
  matchOpenExp,
  matchOpenFun,
  matchPrimFun,  matchPrimFun',

  -- auxiliary
  matchIdx, matchVar, matchVars, matchArrayR, matchArraysR, matchTypeR, matchShapeR,
  matchShapeType, matchIntegralType, matchFloatingType, matchNumType, matchScalarType,
  matchLeftHandSide, matchALeftHandSide, matchELeftHandSide, matchSingleType, matchTupR

) where

import Data.Array.Accelerate.AST
import Data.Array.Accelerate.AST.Idx
import Data.Array.Accelerate.AST.LeftHandSide
import Data.Array.Accelerate.AST.Var
import Data.Array.Accelerate.Analysis.Hash
import Data.Array.Accelerate.Representation.Array
import Data.Array.Accelerate.Representation.Shape
import Data.Array.Accelerate.Representation.Slice
import Data.Array.Accelerate.Representation.Stencil
import Data.Array.Accelerate.Representation.Type
import Data.Array.Accelerate.Type
import Data.Primitive.Vec
import qualified Data.Array.Accelerate.Sugar.Shape      as Sugar

import Data.Maybe
import Data.Typeable
import Unsafe.Coerce                                    ( unsafeCoerce )
import System.IO.Unsafe                                 ( unsafePerformIO )
import System.Mem.StableName
import Prelude                                          hiding ( exp )


-- The type of matching array computations
--
type MatchAcc acc = forall aenv s t. acc aenv s -> acc aenv t -> Maybe (s :~: t)


-- Compute the congruence of two array computations. The nodes are congruent if
-- they have the same operator and their operands are congruent.
--
{-# INLINEABLE matchPreOpenAcc #-}
matchPreOpenAcc
    :: forall acc aenv s t. HasArraysR acc
    => MatchAcc  acc
    -> PreOpenAcc acc aenv s
    -> PreOpenAcc acc aenv t
    -> Maybe (s :~: t)
matchPreOpenAcc :: MatchAcc acc
-> PreOpenAcc acc aenv s
-> PreOpenAcc acc aenv t
-> Maybe (s :~: t)
matchPreOpenAcc MatchAcc acc
matchAcc = PreOpenAcc acc aenv s -> PreOpenAcc acc aenv t -> Maybe (s :~: t)
match
  where
    matchFun :: OpenFun env' aenv' u -> OpenFun env' aenv' v -> Maybe (u :~: v)
    matchFun :: OpenFun env' aenv' u -> OpenFun env' aenv' v -> Maybe (u :~: v)
matchFun = OpenFun env' aenv' u -> OpenFun env' aenv' v -> Maybe (u :~: v)
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun

    matchExp :: OpenExp env' aenv' u -> OpenExp env' aenv' v -> Maybe (u :~: v)
    matchExp :: OpenExp env' aenv' u -> OpenExp env' aenv' v -> Maybe (u :~: v)
matchExp = OpenExp env' aenv' u -> OpenExp env' aenv' v -> Maybe (u :~: v)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp

    match :: PreOpenAcc acc aenv s -> PreOpenAcc acc aenv t -> Maybe (s :~: t)
    match :: PreOpenAcc acc aenv s -> PreOpenAcc acc aenv t -> Maybe (s :~: t)
match (Alet ALeftHandSide bndArrs aenv aenv'
lhs1 acc aenv bndArrs
x1 acc aenv' s
a1) (Alet ALeftHandSide bndArrs aenv aenv'
lhs2 acc aenv bndArrs
x2 acc aenv' t
a2)
      | Just ALeftHandSide bndArrs aenv aenv'
:~: ALeftHandSide bndArrs aenv aenv'
Refl <- ALeftHandSide bndArrs aenv aenv'
-> ALeftHandSide bndArrs aenv aenv'
-> Maybe
     (ALeftHandSide bndArrs aenv aenv'
      :~: ALeftHandSide bndArrs aenv aenv')
forall aenv aenv1 aenv2 t1 t2.
ALeftHandSide t1 aenv aenv1
-> ALeftHandSide t2 aenv aenv2
-> Maybe
     (ALeftHandSide t1 aenv aenv1 :~: ALeftHandSide t2 aenv aenv2)
matchALeftHandSide ALeftHandSide bndArrs aenv aenv'
lhs1 ALeftHandSide bndArrs aenv aenv'
lhs2
      , Just bndArrs :~: bndArrs
Refl <- acc aenv bndArrs -> acc aenv bndArrs -> Maybe (bndArrs :~: bndArrs)
MatchAcc acc
matchAcc acc aenv bndArrs
x1 acc aenv bndArrs
x2
      , Just s :~: t
Refl <- acc aenv' s -> acc aenv' t -> Maybe (s :~: t)
MatchAcc acc
matchAcc acc aenv' s
a1 acc aenv' t
acc aenv' t
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Avar ArrayVar aenv (Array sh e)
v1) (Avar ArrayVar aenv (Array sh e)
v2)
      = ArrayVar aenv (Array sh e)
-> ArrayVar aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar ArrayVar aenv (Array sh e)
v1 ArrayVar aenv (Array sh e)
v2

    match (Apair acc aenv as
a1 acc aenv bs
a2) (Apair acc aenv as
b1 acc aenv bs
b2)
      | Just as :~: as
Refl <- acc aenv as -> acc aenv as -> Maybe (as :~: as)
MatchAcc acc
matchAcc acc aenv as
a1 acc aenv as
b1
      , Just bs :~: bs
Refl <- acc aenv bs -> acc aenv bs -> Maybe (bs :~: bs)
MatchAcc acc
matchAcc acc aenv bs
a2 acc aenv bs
b2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match PreOpenAcc acc aenv s
Anil PreOpenAcc acc aenv t
Anil
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Apply ArraysR s
_ PreOpenAfun acc aenv (arrs1 -> s)
f1 acc aenv arrs1
a1) (Apply ArraysR t
_ PreOpenAfun acc aenv (arrs1 -> t)
f2 acc aenv arrs1
a2)
      | Just (arrs1 -> s) :~: (arrs1 -> t)
Refl <- MatchAcc acc
-> PreOpenAfun acc aenv (arrs1 -> s)
-> PreOpenAfun acc aenv (arrs1 -> t)
-> Maybe ((arrs1 -> s) :~: (arrs1 -> t))
forall (acc :: * -> * -> *) aenv s t.
MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
matchAcc PreOpenAfun acc aenv (arrs1 -> s)
f1 PreOpenAfun acc aenv (arrs1 -> t)
f2
      , Just arrs1 :~: arrs1
Refl <- acc aenv arrs1 -> acc aenv arrs1 -> Maybe (arrs1 :~: arrs1)
MatchAcc acc
matchAcc                  acc aenv arrs1
a1 acc aenv arrs1
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Aforeign ArraysR s
_ asm (as -> s)
ff1 PreAfun acc (as -> s)
f1 acc aenv as
a1) (Aforeign ArraysR t
_ asm (as -> t)
ff2 PreAfun acc (as -> t)
f2 acc aenv as
a2)
      | Just as :~: as
Refl <- acc aenv as -> acc aenv as -> Maybe (as :~: as)
MatchAcc acc
matchAcc acc aenv as
a1 acc aenv as
a2
      , IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
          StableName (asm (as -> s))
sn1 <- asm (as -> s) -> IO (StableName (asm (as -> s)))
forall a. a -> IO (StableName a)
makeStableName asm (as -> s)
ff1
          StableName (asm (as -> t))
sn2 <- asm (as -> t) -> IO (StableName (asm (as -> t)))
forall a. a -> IO (StableName a)
makeStableName asm (as -> t)
ff2
          Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$! StableName (asm (as -> s)) -> Int
forall a. StableName a -> Int
hashStableName StableName (asm (as -> s))
sn1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== StableName (asm (as -> t)) -> Int
forall a. StableName a -> Int
hashStableName StableName (asm (as -> t))
sn2
      , Just (as -> s) :~: (as -> t)
Refl <- MatchAcc acc
-> PreAfun acc (as -> s)
-> PreAfun acc (as -> t)
-> Maybe ((as -> s) :~: (as -> t))
forall (acc :: * -> * -> *) aenv s t.
MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
matchAcc PreAfun acc (as -> s)
f1 PreAfun acc (as -> t)
f2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Acond Exp aenv PrimBool
p1 acc aenv s
t1 acc aenv s
e1) (Acond Exp aenv PrimBool
p2 acc aenv t
t2 acc aenv t
e2)
      | Just PrimBool :~: PrimBool
Refl <- Exp aenv PrimBool
-> Exp aenv PrimBool -> Maybe (PrimBool :~: PrimBool)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv PrimBool
p1 Exp aenv PrimBool
p2
      , Just s :~: t
Refl <- acc aenv s -> acc aenv t -> Maybe (s :~: t)
MatchAcc acc
matchAcc acc aenv s
t1 acc aenv t
t2
      , Just s :~: t
Refl <- acc aenv s -> acc aenv t -> Maybe (s :~: t)
MatchAcc acc
matchAcc acc aenv s
e1 acc aenv t
e2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Awhile PreOpenAfun acc aenv (s -> Scalar PrimBool)
p1 PreOpenAfun acc aenv (s -> s)
f1 acc aenv s
a1) (Awhile PreOpenAfun acc aenv (t -> Scalar PrimBool)
p2 PreOpenAfun acc aenv (t -> t)
f2 acc aenv t
a2)
      | Just s :~: t
Refl <- acc aenv s -> acc aenv t -> Maybe (s :~: t)
MatchAcc acc
matchAcc acc aenv s
a1 acc aenv t
a2
      , Just (s -> Scalar PrimBool) :~: (t -> Scalar PrimBool)
Refl <- MatchAcc acc
-> PreOpenAfun acc aenv (s -> Scalar PrimBool)
-> PreOpenAfun acc aenv (t -> Scalar PrimBool)
-> Maybe ((s -> Scalar PrimBool) :~: (t -> Scalar PrimBool))
forall (acc :: * -> * -> *) aenv s t.
MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
matchAcc PreOpenAfun acc aenv (s -> Scalar PrimBool)
p1 PreOpenAfun acc aenv (t -> Scalar PrimBool)
p2
      , Just (s -> s) :~: (t -> t)
Refl <- MatchAcc acc
-> PreOpenAfun acc aenv (s -> s)
-> PreOpenAfun acc aenv (t -> t)
-> Maybe ((s -> s) :~: (t -> t))
forall (acc :: * -> * -> *) aenv s t.
MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
matchAcc PreOpenAfun acc aenv (s -> s)
f1 PreOpenAfun acc aenv (t -> t)
f2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Use ArrayR (Array sh e)
repr1 Array sh e
a1) (Use ArrayR (Array sh e)
repr2 Array sh e
a2)
      | Just Array sh e :~: Array sh e
Refl <- ArrayR (Array sh e)
-> ArrayR (Array sh e)
-> Array sh e
-> Array sh e
-> Maybe (Array sh e :~: Array sh e)
forall sh1 e1 sh2 e2.
ArrayR (Array sh1 e1)
-> ArrayR (Array sh2 e2)
-> Array sh1 e1
-> Array sh2 e2
-> Maybe (Array sh1 e1 :~: Array sh2 e2)
matchArray ArrayR (Array sh e)
repr1 ArrayR (Array sh e)
repr2 Array sh e
a1 Array sh e
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Unit TypeR e
t1 Exp aenv e
e1) (Unit TypeR e
t2 Exp aenv e
e2)
      | Just e :~: e
Refl <- TypeR e -> TypeR e -> Maybe (e :~: e)
forall s t. TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR TypeR e
t1 TypeR e
t2
      , Just e :~: e
Refl <- Exp aenv e -> Exp aenv e -> Maybe (e :~: e)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv e
e1 Exp aenv e
e2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Reshape ShapeR sh
_ Exp aenv sh
sh1 acc aenv (Array sh' e)
a1) (Reshape ShapeR sh
_ Exp aenv sh
sh2 acc aenv (Array sh' e)
a2)
      | Just sh :~: sh
Refl <- Exp aenv sh -> Exp aenv sh -> Maybe (sh :~: sh)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv sh
sh1 Exp aenv sh
sh2
      , Just Array sh' e :~: Array sh' e
Refl <- acc aenv (Array sh' e)
-> acc aenv (Array sh' e) -> Maybe (Array sh' e :~: Array sh' e)
MatchAcc acc
matchAcc acc aenv (Array sh' e)
a1  acc aenv (Array sh' e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Generate ArrayR (Array sh e)
_ Exp aenv sh
sh1 Fun aenv (sh -> e)
f1) (Generate ArrayR (Array sh e)
_ Exp aenv sh
sh2 Fun aenv (sh -> e)
f2)
      | Just sh :~: sh
Refl <- Exp aenv sh -> Exp aenv sh -> Maybe (sh :~: sh)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv sh
sh1 Exp aenv sh
sh2
      , Just (sh -> e) :~: (sh -> e)
Refl <- Fun aenv (sh -> e)
-> Fun aenv (sh -> e) -> Maybe ((sh -> e) :~: (sh -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (sh -> e)
f1  Fun aenv (sh -> e)
f2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Transform ArrayR (Array sh' b)
_ Exp aenv sh'
sh1 Fun aenv (sh' -> sh)
ix1 Fun aenv (a -> b)
f1 acc aenv (Array sh a)
a1) (Transform ArrayR (Array sh' b)
_ Exp aenv sh'
sh2 Fun aenv (sh' -> sh)
ix2 Fun aenv (a -> b)
f2 acc aenv (Array sh a)
a2)
      | Just sh' :~: sh'
Refl <- Exp aenv sh' -> Exp aenv sh' -> Maybe (sh' :~: sh')
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv sh'
sh1 Exp aenv sh'
sh2
      , Just (sh' -> sh) :~: (sh' -> sh)
Refl <- Fun aenv (sh' -> sh)
-> Fun aenv (sh' -> sh) -> Maybe ((sh' -> sh) :~: (sh' -> sh))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (sh' -> sh)
ix1 Fun aenv (sh' -> sh)
ix2
      , Just (a -> b) :~: (a -> b)
Refl <- Fun aenv (a -> b)
-> Fun aenv (a -> b) -> Maybe ((a -> b) :~: (a -> b))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (a -> b)
f1  Fun aenv (a -> b)
f2
      , Just Array sh a :~: Array sh a
Refl <- acc aenv (Array sh a)
-> acc aenv (Array sh a) -> Maybe (Array sh a :~: Array sh a)
MatchAcc acc
matchAcc acc aenv (Array sh a)
a1  acc aenv (Array sh a)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Replicate SliceIndex slix sl co sh
si1 Exp aenv slix
ix1 acc aenv (Array sl e)
a1) (Replicate SliceIndex slix sl co sh
si2 Exp aenv slix
ix2 acc aenv (Array sl e)
a2)
      | Just SliceIndex slix sl co sh :~: SliceIndex slix sl co sh
Refl <- SliceIndex slix sl co sh
-> SliceIndex slix sl co sh
-> Maybe (SliceIndex slix sl co sh :~: SliceIndex slix sl co sh)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex slix sl co sh
si1 SliceIndex slix sl co sh
si2
      , Just slix :~: slix
Refl <- Exp aenv slix -> Exp aenv slix -> Maybe (slix :~: slix)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv slix
ix1 Exp aenv slix
ix2
      , Just Array sl e :~: Array sl e
Refl <- acc aenv (Array sl e)
-> acc aenv (Array sl e) -> Maybe (Array sl e :~: Array sl e)
MatchAcc acc
matchAcc acc aenv (Array sl e)
a1  acc aenv (Array sl e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Slice SliceIndex slix sl co sh
si1 acc aenv (Array sh e)
a1 Exp aenv slix
ix1) (Slice SliceIndex slix sl co sh
si2 acc aenv (Array sh e)
a2 Exp aenv slix
ix2)
      | Just SliceIndex slix sl co sh :~: SliceIndex slix sl co sh
Refl <- SliceIndex slix sl co sh
-> SliceIndex slix sl co sh
-> Maybe (SliceIndex slix sl co sh :~: SliceIndex slix sl co sh)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex slix sl co sh
si1 SliceIndex slix sl co sh
si2
      , Just Array sh e :~: Array sh e
Refl <- acc aenv (Array sh e)
-> acc aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
MatchAcc acc
matchAcc acc aenv (Array sh e)
a1  acc aenv (Array sh e)
a2
      , Just slix :~: slix
Refl <- Exp aenv slix -> Exp aenv slix -> Maybe (slix :~: slix)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv slix
ix1 Exp aenv slix
ix2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Map TypeR e'
_ Fun aenv (e -> e')
f1 acc aenv (Array sh e)
a1) (Map TypeR e'
_ Fun aenv (e -> e')
f2 acc aenv (Array sh e)
a2)
      | Just (e -> e') :~: (e -> e')
Refl <- Fun aenv (e -> e')
-> Fun aenv (e -> e') -> Maybe ((e -> e') :~: (e -> e'))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e')
f1 Fun aenv (e -> e')
f2
      , Just Array sh e :~: Array sh e
Refl <- acc aenv (Array sh e)
-> acc aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
MatchAcc acc
matchAcc acc aenv (Array sh e)
a1 acc aenv (Array sh e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (ZipWith TypeR e3
_ Fun aenv (e1 -> e2 -> e3)
f1 acc aenv (Array sh e1)
a1 acc aenv (Array sh e2)
b1) (ZipWith TypeR e3
_ Fun aenv (e1 -> e2 -> e3)
f2 acc aenv (Array sh e1)
a2 acc aenv (Array sh e2)
b2)
      | Just (e1 -> e2 -> e3) :~: (e1 -> e2 -> e3)
Refl <- Fun aenv (e1 -> e2 -> e3)
-> Fun aenv (e1 -> e2 -> e3)
-> Maybe ((e1 -> e2 -> e3) :~: (e1 -> e2 -> e3))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e1 -> e2 -> e3)
f1 Fun aenv (e1 -> e2 -> e3)
f2
      , Just Array sh e1 :~: Array sh e1
Refl <- acc aenv (Array sh e1)
-> acc aenv (Array sh e1) -> Maybe (Array sh e1 :~: Array sh e1)
MatchAcc acc
matchAcc acc aenv (Array sh e1)
a1 acc aenv (Array sh e1)
a2
      , Just Array sh e2 :~: Array sh e2
Refl <- acc aenv (Array sh e2)
-> acc aenv (Array sh e2) -> Maybe (Array sh e2 :~: Array sh e2)
MatchAcc acc
matchAcc acc aenv (Array sh e2)
b1 acc aenv (Array sh e2)
b2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Fold Fun aenv (e -> e -> e)
f1 Maybe (Exp aenv e)
z1 acc aenv (Array (sh, Int) e)
a1) (Fold Fun aenv (e -> e -> e)
f2 Maybe (Exp aenv e)
z2 acc aenv (Array (sh, Int) e)
a2)
      | Just (e -> e -> e) :~: (e -> e -> e)
Refl <- Fun aenv (e -> e -> e)
-> Fun aenv (e -> e -> e)
-> Maybe ((e -> e -> e) :~: (e -> e -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e -> e)
f1 Fun aenv (e -> e -> e)
f2
      , (Exp aenv e -> Exp aenv e -> Maybe (e :~: e))
-> Maybe (Exp aenv e) -> Maybe (Exp aenv e) -> Bool
forall s1 s2 t1 t2.
(s1 -> s2 -> Maybe (t1 :~: t2)) -> Maybe s1 -> Maybe s2 -> Bool
matchMaybe Exp aenv e -> Exp aenv e -> Maybe (e :~: e)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Maybe (Exp aenv e)
z1 Maybe (Exp aenv e)
z2
      , Just Array (sh, Int) e :~: Array (sh, Int) e
Refl <- acc aenv (Array (sh, Int) e)
-> acc aenv (Array (sh, Int) e)
-> Maybe (Array (sh, Int) e :~: Array (sh, Int) e)
MatchAcc acc
matchAcc acc aenv (Array (sh, Int) e)
a1 acc aenv (Array (sh, Int) e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (FoldSeg IntegralType i
_ Fun aenv (e -> e -> e)
f1 Maybe (Exp aenv e)
z1 acc aenv (Array (sh, Int) e)
a1 acc aenv (Segments i)
s1) (FoldSeg IntegralType i
_ Fun aenv (e -> e -> e)
f2 Maybe (Exp aenv e)
z2 acc aenv (Array (sh, Int) e)
a2 acc aenv (Segments i)
s2)
      | Just (e -> e -> e) :~: (e -> e -> e)
Refl <- Fun aenv (e -> e -> e)
-> Fun aenv (e -> e -> e)
-> Maybe ((e -> e -> e) :~: (e -> e -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e -> e)
f1 Fun aenv (e -> e -> e)
f2
      , (Exp aenv e -> Exp aenv e -> Maybe (e :~: e))
-> Maybe (Exp aenv e) -> Maybe (Exp aenv e) -> Bool
forall s1 s2 t1 t2.
(s1 -> s2 -> Maybe (t1 :~: t2)) -> Maybe s1 -> Maybe s2 -> Bool
matchMaybe Exp aenv e -> Exp aenv e -> Maybe (e :~: e)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Maybe (Exp aenv e)
z1 Maybe (Exp aenv e)
z2
      , Just Array (sh, Int) e :~: Array (sh, Int) e
Refl <- acc aenv (Array (sh, Int) e)
-> acc aenv (Array (sh, Int) e)
-> Maybe (Array (sh, Int) e :~: Array (sh, Int) e)
MatchAcc acc
matchAcc acc aenv (Array (sh, Int) e)
a1 acc aenv (Array (sh, Int) e)
a2
      , Just Segments i :~: Segments i
Refl <- acc aenv (Segments i)
-> acc aenv (Segments i) -> Maybe (Segments i :~: Segments i)
MatchAcc acc
matchAcc acc aenv (Segments i)
s1 acc aenv (Segments i)
s2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Scan Direction
d1 Fun aenv (e -> e -> e)
f1 Maybe (Exp aenv e)
z1 acc aenv (Array (sh, Int) e)
a1) (Scan Direction
d2 Fun aenv (e -> e -> e)
f2 Maybe (Exp aenv e)
z2 acc aenv (Array (sh, Int) e)
a2)
      | Direction
d1 Direction -> Direction -> Bool
forall a. Eq a => a -> a -> Bool
== Direction
d2
      , Just (e -> e -> e) :~: (e -> e -> e)
Refl <- Fun aenv (e -> e -> e)
-> Fun aenv (e -> e -> e)
-> Maybe ((e -> e -> e) :~: (e -> e -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e -> e)
f1 Fun aenv (e -> e -> e)
f2
      , (Exp aenv e -> Exp aenv e -> Maybe (e :~: e))
-> Maybe (Exp aenv e) -> Maybe (Exp aenv e) -> Bool
forall s1 s2 t1 t2.
(s1 -> s2 -> Maybe (t1 :~: t2)) -> Maybe s1 -> Maybe s2 -> Bool
matchMaybe Exp aenv e -> Exp aenv e -> Maybe (e :~: e)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Maybe (Exp aenv e)
z1 Maybe (Exp aenv e)
z2
      , Just Array (sh, Int) e :~: Array (sh, Int) e
Refl <- acc aenv (Array (sh, Int) e)
-> acc aenv (Array (sh, Int) e)
-> Maybe (Array (sh, Int) e :~: Array (sh, Int) e)
MatchAcc acc
matchAcc acc aenv (Array (sh, Int) e)
a1 acc aenv (Array (sh, Int) e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Scan' Direction
d1 Fun aenv (e -> e -> e)
f1 Exp aenv e
z1 acc aenv (Array (sh, Int) e)
a1) (Scan' Direction
d2 Fun aenv (e -> e -> e)
f2 Exp aenv e
z2 acc aenv (Array (sh, Int) e)
a2)
      | Direction
d1 Direction -> Direction -> Bool
forall a. Eq a => a -> a -> Bool
== Direction
d2
      , Just (e -> e -> e) :~: (e -> e -> e)
Refl <- Fun aenv (e -> e -> e)
-> Fun aenv (e -> e -> e)
-> Maybe ((e -> e -> e) :~: (e -> e -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e -> e)
f1 Fun aenv (e -> e -> e)
f2
      , Just e :~: e
Refl <- Exp aenv e -> Exp aenv e -> Maybe (e :~: e)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv e
z1 Exp aenv e
z2
      , Just Array (sh, Int) e :~: Array (sh, Int) e
Refl <- acc aenv (Array (sh, Int) e)
-> acc aenv (Array (sh, Int) e)
-> Maybe (Array (sh, Int) e :~: Array (sh, Int) e)
MatchAcc acc
matchAcc acc aenv (Array (sh, Int) e)
a1 acc aenv (Array (sh, Int) e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Permute Fun aenv (e -> e -> e)
f1 acc aenv (Array sh' e)
d1 Fun aenv (sh -> PrimMaybe sh')
p1 acc aenv (Array sh e)
a1) (Permute Fun aenv (e -> e -> e)
f2 acc aenv (Array sh' e)
d2 Fun aenv (sh -> PrimMaybe sh')
p2 acc aenv (Array sh e)
a2)
      | Just (e -> e -> e) :~: (e -> e -> e)
Refl <- Fun aenv (e -> e -> e)
-> Fun aenv (e -> e -> e)
-> Maybe ((e -> e -> e) :~: (e -> e -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (e -> e -> e)
f1 Fun aenv (e -> e -> e)
f2
      , Just Array sh' e :~: Array sh' e
Refl <- acc aenv (Array sh' e)
-> acc aenv (Array sh' e) -> Maybe (Array sh' e :~: Array sh' e)
MatchAcc acc
matchAcc acc aenv (Array sh' e)
d1 acc aenv (Array sh' e)
d2
      , Just (sh -> PrimMaybe sh') :~: (sh -> PrimMaybe sh')
Refl <- Fun aenv (sh -> PrimMaybe sh')
-> Fun aenv (sh -> PrimMaybe sh')
-> Maybe ((sh -> PrimMaybe sh') :~: (sh -> PrimMaybe sh'))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (sh -> PrimMaybe sh')
p1 Fun aenv (sh -> PrimMaybe sh')
p2
      , Just Array sh e :~: Array sh e
Refl <- acc aenv (Array sh e)
-> acc aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
MatchAcc acc
matchAcc acc aenv (Array sh e)
a1 acc aenv (Array sh e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Backpermute ShapeR sh'
_ Exp aenv sh'
sh1 Fun aenv (sh' -> sh)
ix1 acc aenv (Array sh e)
a1) (Backpermute ShapeR sh'
_ Exp aenv sh'
sh2 Fun aenv (sh' -> sh)
ix2 acc aenv (Array sh e)
a2)
      | Just sh' :~: sh'
Refl <- Exp aenv sh' -> Exp aenv sh' -> Maybe (sh' :~: sh')
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchExp Exp aenv sh'
sh1 Exp aenv sh'
sh2
      , Just (sh' -> sh) :~: (sh' -> sh)
Refl <- Fun aenv (sh' -> sh)
-> Fun aenv (sh' -> sh) -> Maybe ((sh' -> sh) :~: (sh' -> sh))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (sh' -> sh)
ix1 Fun aenv (sh' -> sh)
ix2
      , Just Array sh e :~: Array sh e
Refl <- acc aenv (Array sh e)
-> acc aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
MatchAcc acc
matchAcc acc aenv (Array sh e)
a1  acc aenv (Array sh e)
a2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Stencil StencilR sh e stencil
s1 TypeR e'
_ Fun aenv (stencil -> e')
f1 Boundary aenv (Array sh e)
b1 acc aenv (Array sh e)
a1) (Stencil StencilR sh e stencil
_ TypeR e'
_ Fun aenv (stencil -> e')
f2 Boundary aenv (Array sh e)
b2 acc aenv (Array sh e)
a2)
      | Just (stencil -> e') :~: (stencil -> e')
Refl <- Fun aenv (stencil -> e')
-> Fun aenv (stencil -> e')
-> Maybe ((stencil -> e') :~: (stencil -> e'))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (stencil -> e')
f1 Fun aenv (stencil -> e')
f2
      , Just Array sh e :~: Array sh e
Refl <- acc aenv (Array sh e)
-> acc aenv (Array sh e) -> Maybe (Array sh e :~: Array sh e)
MatchAcc acc
matchAcc acc aenv (Array sh e)
a1 acc aenv (Array sh e)
a2
      , TypeR e
-> Boundary aenv (Array sh e) -> Boundary aenv (Array sh e) -> Bool
forall t aenv sh.
TypeR t
-> Boundary aenv (Array sh t) -> Boundary aenv (Array sh t) -> Bool
matchBoundary (StencilR sh e stencil -> TypeR e
forall sh e pat. StencilR sh e pat -> TypeR e
stencilEltR StencilR sh e stencil
s1) Boundary aenv (Array sh e)
b1 Boundary aenv (Array sh e)
Boundary aenv (Array sh e)
b2
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    match (Stencil2 StencilR sh a stencil1
s1 StencilR sh b stencil2
s2 TypeR c
_ Fun aenv (stencil1 -> stencil2 -> c)
f1 Boundary aenv (Array sh a)
b1  acc aenv (Array sh a)
a1  Boundary aenv (Array sh b)
b2  acc aenv (Array sh b)
a2) (Stencil2 StencilR sh a stencil1
_ StencilR sh b stencil2
_ TypeR c
_ Fun aenv (stencil1 -> stencil2 -> c)
f2 Boundary aenv (Array sh a)
b1' acc aenv (Array sh a)
a1' Boundary aenv (Array sh b)
b2' acc aenv (Array sh b)
a2')
      | Just (stencil1 -> stencil2 -> c) :~: (stencil1 -> stencil2 -> c)
Refl <- Fun aenv (stencil1 -> stencil2 -> c)
-> Fun aenv (stencil1 -> stencil2 -> c)
-> Maybe
     ((stencil1 -> stencil2 -> c) :~: (stencil1 -> stencil2 -> c))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchFun Fun aenv (stencil1 -> stencil2 -> c)
f1 Fun aenv (stencil1 -> stencil2 -> c)
f2
      , Just Array sh a :~: Array sh a
Refl <- acc aenv (Array sh a)
-> acc aenv (Array sh a) -> Maybe (Array sh a :~: Array sh a)
MatchAcc acc
matchAcc acc aenv (Array sh a)
a1 acc aenv (Array sh a)
a1'
      , Just Array sh b :~: Array sh b
Refl <- acc aenv (Array sh b)
-> acc aenv (Array sh b) -> Maybe (Array sh b :~: Array sh b)
MatchAcc acc
matchAcc acc aenv (Array sh b)
a2 acc aenv (Array sh b)
a2'
      , TypeR a
-> Boundary aenv (Array sh a) -> Boundary aenv (Array sh a) -> Bool
forall t aenv sh.
TypeR t
-> Boundary aenv (Array sh t) -> Boundary aenv (Array sh t) -> Bool
matchBoundary (StencilR sh a stencil1 -> TypeR a
forall sh e pat. StencilR sh e pat -> TypeR e
stencilEltR StencilR sh a stencil1
s1) Boundary aenv (Array sh a)
b1 Boundary aenv (Array sh a)
Boundary aenv (Array sh a)
b1'
      , TypeR b
-> Boundary aenv (Array sh b) -> Boundary aenv (Array sh b) -> Bool
forall t aenv sh.
TypeR t
-> Boundary aenv (Array sh t) -> Boundary aenv (Array sh t) -> Bool
matchBoundary (StencilR sh b stencil2 -> TypeR b
forall sh e pat. StencilR sh e pat -> TypeR e
stencilEltR StencilR sh b stencil2
s2) Boundary aenv (Array sh b)
b2 Boundary aenv (Array sh b)
Boundary aenv (Array sh b)
b2'
      = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

    -- match (Collect s1) (Collect s2)
    --   = matchSeq matchAcc encodeAcc s1 s2

    match PreOpenAcc acc aenv s
_ PreOpenAcc acc aenv t
_
      = Maybe (s :~: t)
forall a. Maybe a
Nothing

-- Array functions
--
{-# INLINEABLE matchPreOpenAfun #-}
matchPreOpenAfun
    :: MatchAcc acc
    -> PreOpenAfun acc aenv s
    -> PreOpenAfun acc aenv t
    -> Maybe (s :~: t)
matchPreOpenAfun :: MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
m (Alam ALeftHandSide a aenv aenv'
lhs1 PreOpenAfun acc aenv' t
s) (Alam ALeftHandSide a aenv aenv'
lhs2 PreOpenAfun acc aenv' t
t)
  | Just ALeftHandSide a aenv aenv' :~: ALeftHandSide a aenv aenv'
Refl <- ALeftHandSide a aenv aenv'
-> ALeftHandSide a aenv aenv'
-> Maybe
     (ALeftHandSide a aenv aenv' :~: ALeftHandSide a aenv aenv')
forall aenv aenv1 aenv2 t1 t2.
ALeftHandSide t1 aenv aenv1
-> ALeftHandSide t2 aenv aenv2
-> Maybe
     (ALeftHandSide t1 aenv aenv1 :~: ALeftHandSide t2 aenv aenv2)
matchALeftHandSide ALeftHandSide a aenv aenv'
lhs1 ALeftHandSide a aenv aenv'
lhs2
  , Just t :~: t
Refl <- MatchAcc acc
-> PreOpenAfun acc aenv' t
-> PreOpenAfun acc aenv' t
-> Maybe (t :~: t)
forall (acc :: * -> * -> *) aenv s t.
MatchAcc acc
-> PreOpenAfun acc aenv s
-> PreOpenAfun acc aenv t
-> Maybe (s :~: t)
matchPreOpenAfun MatchAcc acc
m PreOpenAfun acc aenv' t
s PreOpenAfun acc aenv' t
PreOpenAfun acc aenv' t
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPreOpenAfun MatchAcc acc
m (Abody acc aenv s
s) (Abody acc aenv t
t) = acc aenv s -> acc aenv t -> Maybe (s :~: t)
MatchAcc acc
m acc aenv s
s acc aenv t
t
matchPreOpenAfun MatchAcc acc
_ PreOpenAfun acc aenv s
_           PreOpenAfun acc aenv t
_           = Maybe (s :~: t)
forall a. Maybe a
Nothing

matchALeftHandSide
    :: forall aenv aenv1 aenv2 t1 t2.
       ALeftHandSide t1 aenv aenv1
    -> ALeftHandSide t2 aenv aenv2
    -> Maybe (ALeftHandSide t1 aenv aenv1 :~: ALeftHandSide t2 aenv aenv2)
matchALeftHandSide :: ALeftHandSide t1 aenv aenv1
-> ALeftHandSide t2 aenv aenv2
-> Maybe
     (ALeftHandSide t1 aenv aenv1 :~: ALeftHandSide t2 aenv aenv2)
matchALeftHandSide = (forall x y. ArrayR x -> ArrayR y -> Maybe (x :~: y))
-> ALeftHandSide t1 aenv aenv1
-> ALeftHandSide t2 aenv aenv2
-> Maybe
     (ALeftHandSide t1 aenv aenv1 :~: ALeftHandSide t2 aenv aenv2)
forall (s :: * -> *) env env1 env2 t1 t2.
(forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s t1 env env1
-> LeftHandSide s t2 env env2
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide forall x y. ArrayR x -> ArrayR y -> Maybe (x :~: y)
matchArrayR

matchELeftHandSide
    :: forall env env1 env2 t1 t2.
       ELeftHandSide t1 env env1
    -> ELeftHandSide t2 env env2
    -> Maybe (ELeftHandSide t1 env env1 :~: ELeftHandSide t2 env env2)
matchELeftHandSide :: ELeftHandSide t1 env env1
-> ELeftHandSide t2 env env2
-> Maybe (ELeftHandSide t1 env env1 :~: ELeftHandSide t2 env env2)
matchELeftHandSide = (forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y))
-> ELeftHandSide t1 env env1
-> ELeftHandSide t2 env env2
-> Maybe (ELeftHandSide t1 env env1 :~: ELeftHandSide t2 env env2)
forall (s :: * -> *) env env1 env2 t1 t2.
(forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s t1 env env1
-> LeftHandSide s t2 env env2
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y)
matchScalarType

matchLeftHandSide
    :: forall s env env1 env2 t1 t2.
      (forall x y. s x -> s y -> Maybe (x :~: y))
    -> LeftHandSide s t1 env env1
    -> LeftHandSide s t2 env env2
    -> Maybe (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide :: (forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s t1 env env1
-> LeftHandSide s t2 env env2
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
f (LeftHandSideWildcard TupR s t1
repr1) (LeftHandSideWildcard TupR s t2
repr2)
  | Just t1 :~: t2
Refl <- (forall x y. s x -> s y -> Maybe (x :~: y))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
forall (s :: * -> *) t1 t2.
(forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall x y. s x -> s y -> Maybe (x :~: y)
f TupR s t1
repr1 TupR s t2
repr2
  = (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
forall a. a -> Maybe a
Just LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1
forall k (a :: k). a :~: a
Refl
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
f (LeftHandSideSingle s t1
x) (LeftHandSideSingle s t2
y)
  | Just t1 :~: t2
Refl <- s t1 -> s t2 -> Maybe (t1 :~: t2)
forall x y. s x -> s y -> Maybe (x :~: y)
f s t1
x s t2
y
  = (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
forall a. a -> Maybe a
Just LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1
forall k (a :: k). a :~: a
Refl
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
f (LeftHandSidePair LeftHandSide s v1 env env'
a1 LeftHandSide s v2 env' env1
a2) (LeftHandSidePair LeftHandSide s v1 env env'
b1 LeftHandSide s v2 env' env2
b2)
  | Just LeftHandSide s v1 env env' :~: LeftHandSide s v1 env env'
Refl <- (forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s v1 env env'
-> LeftHandSide s v1 env env'
-> Maybe
     (LeftHandSide s v1 env env' :~: LeftHandSide s v1 env env')
forall (s :: * -> *) env env1 env2 t1 t2.
(forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s t1 env env1
-> LeftHandSide s t2 env env2
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
f LeftHandSide s v1 env env'
a1 LeftHandSide s v1 env env'
b1
  , Just LeftHandSide s v2 env' env1 :~: LeftHandSide s v2 env' env2
Refl <- (forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s v2 env' env1
-> LeftHandSide s v2 env' env2
-> Maybe
     (LeftHandSide s v2 env' env1 :~: LeftHandSide s v2 env' env2)
forall (s :: * -> *) env env1 env2 t1 t2.
(forall x y. s x -> s y -> Maybe (x :~: y))
-> LeftHandSide s t1 env env1
-> LeftHandSide s t2 env env2
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
f LeftHandSide s v2 env' env1
a2 LeftHandSide s v2 env' env2
LeftHandSide s v2 env' env2
b2
  = (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
-> Maybe
     (LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1)
forall a. a -> Maybe a
Just LeftHandSide s t1 env env1 :~: LeftHandSide s t1 env env1
forall k (a :: k). a :~: a
Refl
matchLeftHandSide forall x y. s x -> s y -> Maybe (x :~: y)
_ LeftHandSide s t1 env env1
_ LeftHandSide s t2 env env2
_ = Maybe (LeftHandSide s t1 env env1 :~: LeftHandSide s t2 env env2)
forall a. Maybe a
Nothing

-- Match stencil boundaries
--
matchBoundary
    :: TypeR t
    -> Boundary aenv (Array sh t)
    -> Boundary aenv (Array sh t)
    -> Bool
matchBoundary :: TypeR t
-> Boundary aenv (Array sh t) -> Boundary aenv (Array sh t) -> Bool
matchBoundary TypeR t
_  Boundary aenv (Array sh t)
Clamp        Boundary aenv (Array sh t)
Clamp        = Bool
True
matchBoundary TypeR t
_  Boundary aenv (Array sh t)
Mirror       Boundary aenv (Array sh t)
Mirror       = Bool
True
matchBoundary TypeR t
_  Boundary aenv (Array sh t)
Wrap         Boundary aenv (Array sh t)
Wrap         = Bool
True
matchBoundary TypeR t
tp (Constant e
s) (Constant e
t) = TypeR t -> t -> t -> Bool
forall a. TypeR a -> a -> a -> Bool
matchConst TypeR t
tp t
e
s t
e
t
matchBoundary TypeR t
_  (Function Fun aenv (sh -> e)
f) (Function Fun aenv (sh -> e)
g)
  | Just (sh -> e) :~: (sh -> e)
Refl <- Fun aenv (sh -> e)
-> Fun aenv (sh -> e) -> Maybe ((sh -> e) :~: (sh -> e))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun Fun aenv (sh -> e)
f Fun aenv (sh -> e)
g
  = Bool
True
matchBoundary TypeR t
_ Boundary aenv (Array sh t)
_ Boundary aenv (Array sh t)
_
  = Bool
False

matchMaybe :: (s1 -> s2 -> Maybe (t1 :~: t2)) -> Maybe s1 -> Maybe s2 -> Bool
matchMaybe :: (s1 -> s2 -> Maybe (t1 :~: t2)) -> Maybe s1 -> Maybe s2 -> Bool
matchMaybe s1 -> s2 -> Maybe (t1 :~: t2)
_ Maybe s1
Nothing  Maybe s2
Nothing  = Bool
True
matchMaybe s1 -> s2 -> Maybe (t1 :~: t2)
f (Just s1
x) (Just s2
y)
  | Just t1 :~: t2
Refl <- s1 -> s2 -> Maybe (t1 :~: t2)
f s1
x s2
y         = Bool
True
matchMaybe s1 -> s2 -> Maybe (t1 :~: t2)
_ Maybe s1
_        Maybe s2
_        = Bool
False

{--
-- Match sequences
--
matchSeq
    :: forall acc aenv senv s t.
       MatchAcc  acc
    -> EncodeAcc acc
    -> PreOpenSeq acc aenv senv s
    -> PreOpenSeq acc aenv senv t
    -> Maybe (s :~: t)
matchSeq m h = match
  where
    matchFun :: OpenFun env' aenv' u -> OpenFun env' aenv' v -> Maybe (u :~: v)
    matchFun = matchOpenFun m h

    matchExp :: OpenExp env' aenv' u -> OpenExp env' aenv' v -> Maybe (u :~: v)
    matchExp = matchOpenExp m h

    match :: PreOpenSeq acc aenv senv' u -> PreOpenSeq acc aenv senv' v -> Maybe (u :~: v)
    match (Producer p1 s1)   (Producer p2 s2)
      | Just Refl <- matchP p1 p2
      , Just Refl <- match s1 s2
      = Just Refl
    match (Consumer c1)   (Consumer c2)
      | Just Refl <- matchC c1 c2
      = Just Refl
    match (Reify ix1) (Reify ix2)
      | Just Refl <- matchIdx ix1 ix2
      = Just Refl
    match _ _
      = Nothing

    matchP :: Producer acc aenv senv' u -> Producer acc aenv senv' v -> Maybe (u :~: v)
    matchP (StreamIn arrs1) (StreamIn arrs2)
      | unsafePerformIO $ do
          sn1 <- makeStableName arrs1
          sn2 <- makeStableName arrs2
          return $! hashStableName sn1 == hashStableName sn2
      = gcast Refl
    matchP (ToSeq _ (_::proxy1 slix1) a1) (ToSeq _ (_::proxy2 slix2) a2)
      | Just Refl <- gcast Refl :: Maybe (slix1 :~: slix2) -- Divisions are singleton.
      , Just Refl <- m a1 a2
      = gcast Refl
    matchP (MapSeq f1 x1) (MapSeq f2 x2)
      | Just Refl <- matchPreOpenAfun m f1 f2
      , Just Refl <- matchIdx x1 x2
      = Just Refl
    matchP (ZipWithSeq f1 x1 y1) (ZipWithSeq f2 x2 y2)
      | Just Refl <- matchPreOpenAfun m f1 f2
      , Just Refl <- matchIdx x1 x2
      , Just Refl <- matchIdx y1 y2
      = Just Refl
    matchP (ScanSeq f1 e1 x1) (ScanSeq f2 e2 x2)
      | Just Refl <- matchFun f1 f2
      , Just Refl <- matchIdx x1 x2
      , Just Refl <- matchExp e1 e2
      = Just Refl
    matchP _ _
      = Nothing

    matchC :: Consumer acc aenv senv' u -> Consumer acc aenv senv' v -> Maybe (u :~: v)
    matchC (FoldSeq f1 e1 x1) (FoldSeq f2 e2 x2)
      | Just Refl <- matchIdx x1 x2
      , Just Refl <- matchFun f1 f2
      , Just Refl <- matchExp e1 e2
      = Just Refl
    matchC (FoldSeqFlatten f1 acc1 x1) (FoldSeqFlatten f2 acc2 x2)
      | Just Refl <- matchIdx x1 x2
      , Just Refl <- matchPreOpenAfun m f1 f2
      , Just Refl <- m acc1 acc2
      = Just Refl
    matchC (Stuple s1) (Stuple s2)
      | Just Refl <- matchAtuple matchC s1 s2
      = gcast Refl
    matchC _ _
      = Nothing
--}

-- Match arrays
--
-- As a convenience, we are just comparing the stable names, but we could also
-- walk the structure comparing the underlying ptrsOfArrayData.
--
matchArray :: ArrayR (Array sh1 e1)
           -> ArrayR (Array sh2 e2)
           -> Array sh1 e1
           -> Array sh2 e2
           -> Maybe (Array sh1 e1 :~: Array sh2 e2)
matchArray :: ArrayR (Array sh1 e1)
-> ArrayR (Array sh2 e2)
-> Array sh1 e1
-> Array sh2 e2
-> Maybe (Array sh1 e1 :~: Array sh2 e2)
matchArray ArrayR (Array sh1 e1)
repr1 ArrayR (Array sh2 e2)
repr2 (Array sh1
_ ArrayData e1
ad1) (Array sh2
_ ArrayData e2
ad2)
  | Just Array sh1 e1 :~: Array sh2 e2
Refl <- ArrayR (Array sh1 e1)
-> ArrayR (Array sh2 e2) -> Maybe (Array sh1 e1 :~: Array sh2 e2)
forall x y. ArrayR x -> ArrayR y -> Maybe (x :~: y)
matchArrayR ArrayR (Array sh1 e1)
repr1 ArrayR (Array sh2 e2)
repr2
  , IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
      StableName (ArrayData e1)
sn1 <- ArrayData e1 -> IO (StableName (ArrayData e1))
forall a. a -> IO (StableName a)
makeStableName ArrayData e1
ad1
      StableName (ArrayData e1)
sn2 <- ArrayData e1 -> IO (StableName (ArrayData e1))
forall a. a -> IO (StableName a)
makeStableName ArrayData e1
ArrayData e2
ad2
      Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$! StableName (ArrayData e1) -> Int
forall a. StableName a -> Int
hashStableName StableName (ArrayData e1)
sn1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== StableName (ArrayData e1) -> Int
forall a. StableName a -> Int
hashStableName StableName (ArrayData e1)
sn2
  = (Array sh1 e1 :~: Array sh1 e1)
-> Maybe (Array sh1 e1 :~: Array sh1 e1)
forall a. a -> Maybe a
Just Array sh1 e1 :~: Array sh1 e1
forall k (a :: k). a :~: a
Refl

matchArray ArrayR (Array sh1 e1)
_ ArrayR (Array sh2 e2)
_ Array sh1 e1
_ Array sh2 e2
_
  = Maybe (Array sh1 e1 :~: Array sh2 e2)
forall a. Maybe a
Nothing

matchTupR :: (forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)) -> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR :: (forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
_ TupR s t1
TupRunit         TupR s t2
TupRunit         = (t1 :~: t1) -> Maybe (t1 :~: t1)
forall a. a -> Maybe a
Just t1 :~: t1
forall k (a :: k). a :~: a
Refl
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
f (TupRsingle s t1
x)   (TupRsingle s t2
y)   = s t1 -> s t2 -> Maybe (t1 :~: t2)
forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
f s t1
x s t2
y
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
f (TupRpair TupR s a
x1 TupR s b
x2) (TupRpair TupR s a
y1 TupR s b
y2)
  | Just a :~: a
Refl <- (forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s a -> TupR s a -> Maybe (a :~: a)
forall (s :: * -> *) t1 t2.
(forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
f TupR s a
x1 TupR s a
y1
  , Just b :~: b
Refl <- (forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s b -> TupR s b -> Maybe (b :~: b)
forall (s :: * -> *) t1 t2.
(forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
f TupR s b
x2 TupR s b
y2            = (t1 :~: t1) -> Maybe (t1 :~: t1)
forall a. a -> Maybe a
Just t1 :~: t1
forall k (a :: k). a :~: a
Refl
matchTupR forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2)
_ TupR s t1
_                TupR s t2
_                = Maybe (t1 :~: t2)
forall a. Maybe a
Nothing

matchArraysR :: ArraysR s -> ArraysR t -> Maybe (s :~: t)
matchArraysR :: ArraysR s -> ArraysR t -> Maybe (s :~: t)
matchArraysR = (forall x y. ArrayR x -> ArrayR y -> Maybe (x :~: y))
-> ArraysR s -> ArraysR t -> Maybe (s :~: t)
forall (s :: * -> *) t1 t2.
(forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall x y. ArrayR x -> ArrayR y -> Maybe (x :~: y)
matchArrayR

matchArrayR :: ArrayR s -> ArrayR t -> Maybe (s :~: t)
matchArrayR :: ArrayR s -> ArrayR t -> Maybe (s :~: t)
matchArrayR (ArrayR ShapeR sh
shr1 TypeR e
tp1) (ArrayR ShapeR sh
shr2 TypeR e
tp2)
  | Just sh :~: sh
Refl <- ShapeR sh -> ShapeR sh -> Maybe (sh :~: sh)
forall s t. ShapeR s -> ShapeR t -> Maybe (s :~: t)
matchShapeR ShapeR sh
shr1 ShapeR sh
shr2
  , Just e :~: e
Refl <- TypeR e -> TypeR e -> Maybe (e :~: e)
forall s t. TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR TypeR e
tp1 TypeR e
tp2 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchArrayR ArrayR s
_ ArrayR t
_ = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Compute the congruence of two scalar expressions. Two nodes are congruent if
-- either:
--
--  1. The nodes label constants and the contents are equal
--  2. They have the same operator and their operands are congruent
--
-- The below attempts to use real typed equality, but occasionally still needs
-- to use a cast, particularly when we can only match the representation types.
--
{-# INLINEABLE matchOpenExp #-}
matchOpenExp
    :: forall env aenv s t.
       OpenExp env aenv s
    -> OpenExp env aenv t
    -> Maybe (s :~: t)

matchOpenExp :: OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp (Let ELeftHandSide bnd_t env env'
lhs1 OpenExp env aenv bnd_t
x1 OpenExp env' aenv s
e1) (Let ELeftHandSide bnd_t env env'
lhs2 OpenExp env aenv bnd_t
x2 OpenExp env' aenv t
e2)
  | Just ELeftHandSide bnd_t env env' :~: ELeftHandSide bnd_t env env'
Refl <- ELeftHandSide bnd_t env env'
-> ELeftHandSide bnd_t env env'
-> Maybe
     (ELeftHandSide bnd_t env env' :~: ELeftHandSide bnd_t env env')
forall env env1 env2 t1 t2.
ELeftHandSide t1 env env1
-> ELeftHandSide t2 env env2
-> Maybe (ELeftHandSide t1 env env1 :~: ELeftHandSide t2 env env2)
matchELeftHandSide ELeftHandSide bnd_t env env'
lhs1 ELeftHandSide bnd_t env env'
lhs2
  , Just bnd_t :~: bnd_t
Refl <- OpenExp env aenv bnd_t
-> OpenExp env aenv bnd_t -> Maybe (bnd_t :~: bnd_t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv bnd_t
x1 OpenExp env aenv bnd_t
x2
  , Just s :~: t
Refl <- OpenExp env' aenv s -> OpenExp env' aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env' aenv s
e1 OpenExp env' aenv t
OpenExp env' aenv t
e2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Evar ExpVar env s
v1) (Evar ExpVar env t
v2)
  = ExpVar env s -> ExpVar env t -> Maybe (s :~: t)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar ExpVar env s
v1 ExpVar env t
v2

matchOpenExp (Foreign TypeR s
_ asm (x -> s)
ff1 Fun () (x -> s)
f1 OpenExp env aenv x
e1) (Foreign TypeR t
_ asm (x -> t)
ff2 Fun () (x -> t)
f2 OpenExp env aenv x
e2)
  | Just x :~: x
Refl <- OpenExp env aenv x -> OpenExp env aenv x -> Maybe (x :~: x)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv x
e1 OpenExp env aenv x
e2
  , IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
      StableName (asm (x -> s))
sn1 <- asm (x -> s) -> IO (StableName (asm (x -> s)))
forall a. a -> IO (StableName a)
makeStableName asm (x -> s)
ff1
      StableName (asm (x -> t))
sn2 <- asm (x -> t) -> IO (StableName (asm (x -> t)))
forall a. a -> IO (StableName a)
makeStableName asm (x -> t)
ff2
      Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$! StableName (asm (x -> s)) -> Int
forall a. StableName a -> Int
hashStableName StableName (asm (x -> s))
sn1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== StableName (asm (x -> t)) -> Int
forall a. StableName a -> Int
hashStableName StableName (asm (x -> t))
sn2
  , Just (x -> s) :~: (x -> t)
Refl <- Fun () (x -> s) -> Fun () (x -> t) -> Maybe ((x -> s) :~: (x -> t))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun Fun () (x -> s)
f1 Fun () (x -> t)
f2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Const ScalarType s
t1 s
c1) (Const ScalarType t
t2 t
c2)
  | Just s :~: t
Refl <- ScalarType s -> ScalarType t -> Maybe (s :~: t)
forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y)
matchScalarType ScalarType s
t1 ScalarType t
t2
  , TypeR s -> s -> s -> Bool
forall a. TypeR a -> a -> a -> Bool
matchConst (ScalarType s -> TypeR s
forall (s :: * -> *) a. s a -> TupR s a
TupRsingle ScalarType s
t1) s
c1 s
t
c2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Undef ScalarType s
t1) (Undef ScalarType t
t2) = ScalarType s -> ScalarType t -> Maybe (s :~: t)
forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y)
matchScalarType ScalarType s
t1 ScalarType t
t2

matchOpenExp (Coerce ScalarType a
_ ScalarType s
t1 OpenExp env aenv a
e1) (Coerce ScalarType a
_ ScalarType t
t2 OpenExp env aenv a
e2)
  | Just s :~: t
Refl <- ScalarType s -> ScalarType t -> Maybe (s :~: t)
forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y)
matchScalarType ScalarType s
t1 ScalarType t
t2
  , Just a :~: a
Refl <- OpenExp env aenv a -> OpenExp env aenv a -> Maybe (a :~: a)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv a
e1 OpenExp env aenv a
e2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Pair OpenExp env aenv t1
a1 OpenExp env aenv t2
b1) (Pair OpenExp env aenv t1
a2 OpenExp env aenv t2
b2)
  | Just t1 :~: t1
Refl <- OpenExp env aenv t1 -> OpenExp env aenv t1 -> Maybe (t1 :~: t1)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv t1
a1 OpenExp env aenv t1
a2
  , Just t2 :~: t2
Refl <- OpenExp env aenv t2 -> OpenExp env aenv t2 -> Maybe (t2 :~: t2)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv t2
b1 OpenExp env aenv t2
b2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp OpenExp env aenv s
Nil OpenExp env aenv t
Nil
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (IndexSlice SliceIndex slix s co sh
sliceIndex1 OpenExp env aenv slix
ix1 OpenExp env aenv sh
sh1) (IndexSlice SliceIndex slix t co sh
sliceIndex2 OpenExp env aenv slix
ix2 OpenExp env aenv sh
sh2)
  | Just slix :~: slix
Refl <- OpenExp env aenv slix
-> OpenExp env aenv slix -> Maybe (slix :~: slix)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv slix
ix1 OpenExp env aenv slix
ix2
  , Just sh :~: sh
Refl <- OpenExp env aenv sh -> OpenExp env aenv sh -> Maybe (sh :~: sh)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv sh
sh1 OpenExp env aenv sh
sh2
  , Just SliceIndex slix s co sh :~: SliceIndex slix t co sh
Refl <- SliceIndex slix s co sh
-> SliceIndex slix t co sh
-> Maybe (SliceIndex slix s co sh :~: SliceIndex slix t co sh)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex slix s co sh
sliceIndex1 SliceIndex slix t co sh
sliceIndex2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (IndexFull SliceIndex slix sl co s
sliceIndex1 OpenExp env aenv slix
ix1 OpenExp env aenv sl
sl1) (IndexFull SliceIndex slix sl co t
sliceIndex2 OpenExp env aenv slix
ix2 OpenExp env aenv sl
sl2)
  | Just slix :~: slix
Refl <- OpenExp env aenv slix
-> OpenExp env aenv slix -> Maybe (slix :~: slix)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv slix
ix1 OpenExp env aenv slix
ix2
  , Just sl :~: sl
Refl <- OpenExp env aenv sl -> OpenExp env aenv sl -> Maybe (sl :~: sl)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv sl
sl1 OpenExp env aenv sl
sl2
  , Just SliceIndex slix sl co s :~: SliceIndex slix sl co t
Refl <- SliceIndex slix sl co s
-> SliceIndex slix sl co t
-> Maybe (SliceIndex slix sl co s :~: SliceIndex slix sl co t)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex slix sl co s
sliceIndex1 SliceIndex slix sl co t
sliceIndex2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (ToIndex ShapeR sh
_ OpenExp env aenv sh
sh1 OpenExp env aenv sh
i1) (ToIndex ShapeR sh
_ OpenExp env aenv sh
sh2 OpenExp env aenv sh
i2)
  | Just sh :~: sh
Refl <- OpenExp env aenv sh -> OpenExp env aenv sh -> Maybe (sh :~: sh)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv sh
sh1 OpenExp env aenv sh
sh2
  , Just sh :~: sh
Refl <- OpenExp env aenv sh -> OpenExp env aenv sh -> Maybe (sh :~: sh)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv sh
i1  OpenExp env aenv sh
i2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (FromIndex ShapeR s
_ OpenExp env aenv s
sh1 OpenExp env aenv Int
i1) (FromIndex ShapeR t
_ OpenExp env aenv t
sh2 OpenExp env aenv Int
i2)
  | Just Int :~: Int
Refl <- OpenExp env aenv Int -> OpenExp env aenv Int -> Maybe (Int :~: Int)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv Int
i1  OpenExp env aenv Int
i2
  , Just s :~: t
Refl <- OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv s
sh1 OpenExp env aenv t
sh2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Cond OpenExp env aenv PrimBool
p1 OpenExp env aenv s
t1 OpenExp env aenv s
e1) (Cond OpenExp env aenv PrimBool
p2 OpenExp env aenv t
t2 OpenExp env aenv t
e2)
  | Just PrimBool :~: PrimBool
Refl <- OpenExp env aenv PrimBool
-> OpenExp env aenv PrimBool -> Maybe (PrimBool :~: PrimBool)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv PrimBool
p1 OpenExp env aenv PrimBool
p2
  , Just s :~: t
Refl <- OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv s
t1 OpenExp env aenv t
t2
  , Just s :~: t
Refl <- OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv s
e1 OpenExp env aenv t
e2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (While OpenFun env aenv (s -> PrimBool)
p1 OpenFun env aenv (s -> s)
f1 OpenExp env aenv s
x1) (While OpenFun env aenv (t -> PrimBool)
p2 OpenFun env aenv (t -> t)
f2 OpenExp env aenv t
x2)
  | Just s :~: t
Refl <- OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv s
x1 OpenExp env aenv t
x2
  , Just (s -> PrimBool) :~: (t -> PrimBool)
Refl <- OpenFun env aenv (s -> PrimBool)
-> OpenFun env aenv (t -> PrimBool)
-> Maybe ((s -> PrimBool) :~: (t -> PrimBool))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun OpenFun env aenv (s -> PrimBool)
p1 OpenFun env aenv (t -> PrimBool)
p2
  , Just (s -> s) :~: (t -> t)
Refl <- OpenFun env aenv (s -> s)
-> OpenFun env aenv (t -> t) -> Maybe ((s -> s) :~: (t -> t))
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun OpenFun env aenv (s -> s)
f1 OpenFun env aenv (t -> t)
f2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (PrimConst PrimConst s
c1) (PrimConst PrimConst t
c2)
  = PrimConst s -> PrimConst t -> Maybe (s :~: t)
forall s t. PrimConst s -> PrimConst t -> Maybe (s :~: t)
matchPrimConst PrimConst s
c1 PrimConst t
c2

matchOpenExp (PrimApp PrimFun (a -> s)
f1 OpenExp env aenv a
x1) (PrimApp PrimFun (a -> t)
f2 OpenExp env aenv a
x2)
  | Just OpenExp env aenv a
x1'  <- PrimFun (a -> s)
-> OpenExp env aenv a -> Maybe (OpenExp env aenv a)
forall env aenv a r.
PrimFun (a -> r)
-> OpenExp env aenv a -> Maybe (OpenExp env aenv a)
commutes PrimFun (a -> s)
f1 OpenExp env aenv a
x1
  , Just OpenExp env aenv a
x2'  <- PrimFun (a -> t)
-> OpenExp env aenv a -> Maybe (OpenExp env aenv a)
forall env aenv a r.
PrimFun (a -> r)
-> OpenExp env aenv a -> Maybe (OpenExp env aenv a)
commutes PrimFun (a -> t)
f2 OpenExp env aenv a
x2
  , Just a :~: a
Refl <- OpenExp env aenv a -> OpenExp env aenv a -> Maybe (a :~: a)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv a
x1' OpenExp env aenv a
x2'
  , Just s :~: t
Refl <- PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
forall a s t.
PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
matchPrimFun PrimFun (a -> s)
f1  PrimFun (a -> t)
PrimFun (a -> t)
f2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

  | Just a :~: a
Refl <- OpenExp env aenv a -> OpenExp env aenv a -> Maybe (a :~: a)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv a
x1 OpenExp env aenv a
x2
  , Just s :~: t
Refl <- PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
forall a s t.
PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
matchPrimFun PrimFun (a -> s)
f1 PrimFun (a -> t)
PrimFun (a -> t)
f2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Index ArrayVar aenv (Array dim s)
a1 OpenExp env aenv dim
x1) (Index ArrayVar aenv (Array dim t)
a2 OpenExp env aenv dim
x2)
  | Just Array dim s :~: Array dim t
Refl <- ArrayVar aenv (Array dim s)
-> ArrayVar aenv (Array dim t)
-> Maybe (Array dim s :~: Array dim t)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar ArrayVar aenv (Array dim s)
a1 ArrayVar aenv (Array dim t)
a2
  , Just dim :~: dim
Refl <- OpenExp env aenv dim -> OpenExp env aenv dim -> Maybe (dim :~: dim)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv dim
x1 OpenExp env aenv dim
x2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (LinearIndex ArrayVar aenv (Array dim s)
a1 OpenExp env aenv Int
x1) (LinearIndex ArrayVar aenv (Array dim t)
a2 OpenExp env aenv Int
x2)
  | Just Array dim s :~: Array dim t
Refl <- ArrayVar aenv (Array dim s)
-> ArrayVar aenv (Array dim t)
-> Maybe (Array dim s :~: Array dim t)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar ArrayVar aenv (Array dim s)
a1 ArrayVar aenv (Array dim t)
a2
  , Just Int :~: Int
Refl <- OpenExp env aenv Int -> OpenExp env aenv Int -> Maybe (Int :~: Int)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv Int
x1 OpenExp env aenv Int
x2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (Shape ArrayVar aenv (Array s e)
a1) (Shape ArrayVar aenv (Array t e)
a2)
  | Just Array s e :~: Array t e
Refl <- ArrayVar aenv (Array s e)
-> ArrayVar aenv (Array t e) -> Maybe (Array s e :~: Array t e)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar ArrayVar aenv (Array s e)
a1 ArrayVar aenv (Array t e)
a2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp (ShapeSize ShapeR dim
_ OpenExp env aenv dim
sh1) (ShapeSize ShapeR dim
_ OpenExp env aenv dim
sh2)
  | Just dim :~: dim
Refl <- OpenExp env aenv dim -> OpenExp env aenv dim -> Maybe (dim :~: dim)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv dim
sh1 OpenExp env aenv dim
sh2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenExp OpenExp env aenv s
_ OpenExp env aenv t
_
  = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Match scalar functions
--
{-# INLINEABLE matchOpenFun #-}
matchOpenFun
    :: OpenFun env aenv s
    -> OpenFun env aenv t
    -> Maybe (s :~: t)
matchOpenFun :: OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun (Lam ELeftHandSide a env env'
lhs1 OpenFun env' aenv t
s) (Lam ELeftHandSide a env env'
lhs2 OpenFun env' aenv t
t)
  | Just ELeftHandSide a env env' :~: ELeftHandSide a env env'
Refl <- ELeftHandSide a env env'
-> ELeftHandSide a env env'
-> Maybe (ELeftHandSide a env env' :~: ELeftHandSide a env env')
forall env env1 env2 t1 t2.
ELeftHandSide t1 env env1
-> ELeftHandSide t2 env env2
-> Maybe (ELeftHandSide t1 env env1 :~: ELeftHandSide t2 env env2)
matchELeftHandSide ELeftHandSide a env env'
lhs1 ELeftHandSide a env env'
lhs2
  , Just t :~: t
Refl <- OpenFun env' aenv t -> OpenFun env' aenv t -> Maybe (t :~: t)
forall env aenv s t.
OpenFun env aenv s -> OpenFun env aenv t -> Maybe (s :~: t)
matchOpenFun OpenFun env' aenv t
s OpenFun env' aenv t
OpenFun env' aenv t
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchOpenFun (Body OpenExp env aenv s
s) (Body OpenExp env aenv t
t) = OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
forall env aenv s t.
OpenExp env aenv s -> OpenExp env aenv t -> Maybe (s :~: t)
matchOpenExp OpenExp env aenv s
s OpenExp env aenv t
t
matchOpenFun OpenFun env aenv s
_        OpenFun env aenv t
_        = Maybe (s :~: t)
forall a. Maybe a
Nothing

-- Matching constants
--
matchConst :: TypeR a -> a -> a -> Bool
matchConst :: TypeR a -> a -> a -> Bool
matchConst TypeR a
TupRunit         ()      ()      = Bool
True
matchConst (TupRsingle ScalarType a
ty)  a
a       a
b       = ScalarType a -> (a, a) -> Bool
forall a. ScalarType a -> (a, a) -> Bool
evalEq ScalarType a
ty (a
a,a
b)
matchConst (TupRpair TupR ScalarType a
ta TupR ScalarType b
tb) (a1,b1) (a2,b2) = TupR ScalarType a -> a -> a -> Bool
forall a. TypeR a -> a -> a -> Bool
matchConst TupR ScalarType a
ta a
a1 a
a2 Bool -> Bool -> Bool
&& TupR ScalarType b -> b -> b -> Bool
forall a. TypeR a -> a -> a -> Bool
matchConst TupR ScalarType b
tb b
b1 b
b2

evalEq :: ScalarType a -> (a, a) -> Bool
evalEq :: ScalarType a -> (a, a) -> Bool
evalEq (SingleScalarType SingleType a
t) = SingleType a -> (a, a) -> Bool
forall a. SingleType a -> (a, a) -> Bool
evalEqSingle SingleType a
t
evalEq (VectorScalarType VectorType (Vec n a)
t) = VectorType (Vec n a) -> (Vec n a, Vec n a) -> Bool
forall a. VectorType a -> (a, a) -> Bool
evalEqVector VectorType (Vec n a)
t

evalEqSingle :: SingleType a -> (a, a) -> Bool
evalEqSingle :: SingleType a -> (a, a) -> Bool
evalEqSingle (NumSingleType NumType a
t) = NumType a -> (a, a) -> Bool
forall a. NumType a -> (a, a) -> Bool
evalEqNum NumType a
t

evalEqVector :: VectorType a -> (a, a) -> Bool
evalEqVector :: VectorType a -> (a, a) -> Bool
evalEqVector VectorType{} = (a -> a -> Bool) -> (a, a) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

evalEqNum :: NumType a -> (a, a) -> Bool
evalEqNum :: NumType a -> (a, a) -> Bool
evalEqNum (IntegralNumType IntegralType a
t) | IntegralDict a
IntegralDict <- IntegralType a -> IntegralDict a
forall a. IntegralType a -> IntegralDict a
integralDict IntegralType a
t  = (a -> a -> Bool) -> (a, a) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
evalEqNum (FloatingNumType FloatingType a
t) | FloatingDict a
FloatingDict <- FloatingType a -> FloatingDict a
forall a. FloatingType a -> FloatingDict a
floatingDict FloatingType a
t  = (a -> a -> Bool) -> (a, a) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)


-- Environment projection indices
--
{-# INLINEABLE matchIdx #-}
matchIdx :: Idx env s -> Idx env t -> Maybe (s :~: t)
matchIdx :: Idx env s -> Idx env t -> Maybe (s :~: t)
matchIdx Idx env s
ZeroIdx     Idx env t
ZeroIdx     = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIdx (SuccIdx Idx env s
u) (SuccIdx Idx env t
v) = Idx env s -> Idx env t -> Maybe (s :~: t)
forall env s t. Idx env s -> Idx env t -> Maybe (s :~: t)
matchIdx Idx env s
u Idx env t
Idx env t
v
matchIdx Idx env s
_           Idx env t
_           = Maybe (s :~: t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchVar #-}
matchVar :: Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar :: Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar (Var s t1
_ Idx env t1
v1) (Var s t2
_ Idx env t2
v2) = Idx env t1 -> Idx env t2 -> Maybe (t1 :~: t2)
forall env s t. Idx env s -> Idx env t -> Maybe (s :~: t)
matchIdx Idx env t1
v1 Idx env t2
v2

{-# INLINEABLE matchVars #-}
matchVars :: Vars s env t1 -> Vars s env t2 -> Maybe (t1 :~: t2)
matchVars :: Vars s env t1 -> Vars s env t2 -> Maybe (t1 :~: t2)
matchVars Vars s env t1
TupRunit         Vars s env t2
TupRunit = (t1 :~: t1) -> Maybe (t1 :~: t1)
forall a. a -> Maybe a
Just t1 :~: t1
forall k (a :: k). a :~: a
Refl
matchVars (TupRsingle Var s env t1
v1) (TupRsingle Var s env t2
v2)
  | Just t1 :~: t2
Refl <- Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
forall (s :: * -> *) env t1 t2.
Var s env t1 -> Var s env t2 -> Maybe (t1 :~: t2)
matchVar Var s env t1
v1 Var s env t2
v2 = (t1 :~: t1) -> Maybe (t1 :~: t1)
forall a. a -> Maybe a
Just t1 :~: t1
forall k (a :: k). a :~: a
Refl
matchVars (TupRpair TupR (Var s env) a
v TupR (Var s env) b
w) (TupRpair TupR (Var s env) a
x TupR (Var s env) b
y)
  | Just a :~: a
Refl <- TupR (Var s env) a -> TupR (Var s env) a -> Maybe (a :~: a)
forall (s :: * -> *) env t1 t2.
Vars s env t1 -> Vars s env t2 -> Maybe (t1 :~: t2)
matchVars TupR (Var s env) a
v TupR (Var s env) a
x
  , Just b :~: b
Refl <- TupR (Var s env) b -> TupR (Var s env) b -> Maybe (b :~: b)
forall (s :: * -> *) env t1 t2.
Vars s env t1 -> Vars s env t2 -> Maybe (t1 :~: t2)
matchVars TupR (Var s env) b
w TupR (Var s env) b
y  = (t1 :~: t1) -> Maybe (t1 :~: t1)
forall a. a -> Maybe a
Just t1 :~: t1
forall k (a :: k). a :~: a
Refl
matchVars Vars s env t1
_ Vars s env t2
_ = Maybe (t1 :~: t2)
forall a. Maybe a
Nothing


-- Slice specifications
--
matchSliceIndex :: SliceIndex slix1 sl1 co1 sh1 -> SliceIndex slix2 sl2 co2 sh2 -> Maybe (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex :: SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex slix1 sl1 co1 sh1
SliceNil SliceIndex slix2 sl2 co2 sh2
SliceNil
  = (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
forall a. a -> Maybe a
Just SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1
forall k (a :: k). a :~: a
Refl

matchSliceIndex (SliceAll   SliceIndex ix slice co1 dim
sl1) (SliceAll   SliceIndex ix slice co2 dim
sl2)
  | Just SliceIndex ix slice co1 dim :~: SliceIndex ix slice co2 dim
Refl <- SliceIndex ix slice co1 dim
-> SliceIndex ix slice co2 dim
-> Maybe
     (SliceIndex ix slice co1 dim :~: SliceIndex ix slice co2 dim)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex ix slice co1 dim
sl1 SliceIndex ix slice co2 dim
sl2
  = (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
forall a. a -> Maybe a
Just SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1
forall k (a :: k). a :~: a
Refl

matchSliceIndex (SliceFixed SliceIndex ix sl1 co dim
sl1) (SliceFixed SliceIndex ix sl2 co dim
sl2)
  | Just SliceIndex ix sl1 co dim :~: SliceIndex ix sl2 co dim
Refl <- SliceIndex ix sl1 co dim
-> SliceIndex ix sl2 co dim
-> Maybe (SliceIndex ix sl1 co dim :~: SliceIndex ix sl2 co dim)
forall slix1 sl1 co1 sh1 slix2 sl2 co2 sh2.
SliceIndex slix1 sl1 co1 sh1
-> SliceIndex slix2 sl2 co2 sh2
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
matchSliceIndex SliceIndex ix sl1 co dim
sl1 SliceIndex ix sl2 co dim
sl2
  = (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
-> Maybe
     (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1)
forall a. a -> Maybe a
Just SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix1 sl1 co1 sh1
forall k (a :: k). a :~: a
Refl

matchSliceIndex SliceIndex slix1 sl1 co1 sh1
_ SliceIndex slix2 sl2 co2 sh2
_
  = Maybe
  (SliceIndex slix1 sl1 co1 sh1 :~: SliceIndex slix2 sl2 co2 sh2)
forall a. Maybe a
Nothing

-- Primitive constants and functions
--
matchPrimConst :: PrimConst s -> PrimConst t -> Maybe (s :~: t)
matchPrimConst :: PrimConst s -> PrimConst t -> Maybe (s :~: t)
matchPrimConst (PrimMinBound BoundedType s
s) (PrimMinBound BoundedType t
t) = BoundedType s -> BoundedType t -> Maybe (s :~: t)
forall s t. BoundedType s -> BoundedType t -> Maybe (s :~: t)
matchBoundedType BoundedType s
s BoundedType t
t
matchPrimConst (PrimMaxBound BoundedType s
s) (PrimMaxBound BoundedType t
t) = BoundedType s -> BoundedType t -> Maybe (s :~: t)
forall s t. BoundedType s -> BoundedType t -> Maybe (s :~: t)
matchBoundedType BoundedType s
s BoundedType t
t
matchPrimConst (PrimPi FloatingType s
s)       (PrimPi FloatingType t
t)       = FloatingType s -> FloatingType t -> Maybe (s :~: t)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType s
s FloatingType t
t
matchPrimConst PrimConst s
_                PrimConst t
_                = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Covariant function matching
--
{-# INLINEABLE matchPrimFun #-}
matchPrimFun :: PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
matchPrimFun :: PrimFun (a -> s) -> PrimFun (a -> t) -> Maybe (s :~: t)
matchPrimFun (PrimAdd NumType a
_)                (PrimAdd NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimSub NumType a
_)                (PrimSub NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimMul NumType a
_)                (PrimMul NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimNeg NumType a
_)                (PrimNeg NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAbs NumType a
_)                (PrimAbs NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimSig NumType a
_)                (PrimSig NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimQuot IntegralType a
_)               (PrimQuot IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimRem IntegralType a
_)                (PrimRem IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimQuotRem IntegralType a
_)            (PrimQuotRem IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimIDiv IntegralType a
_)               (PrimIDiv IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimMod IntegralType a
_)                (PrimMod IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimDivMod IntegralType a
_)             (PrimDivMod IntegralType a
_)             = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBAnd IntegralType a
_)               (PrimBAnd IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBOr IntegralType a
_)                (PrimBOr IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBXor IntegralType a
_)               (PrimBXor IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBNot IntegralType a
_)               (PrimBNot IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBShiftL IntegralType a
_)            (PrimBShiftL IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBShiftR IntegralType a
_)            (PrimBShiftR IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBRotateL IntegralType a
_)           (PrimBRotateL IntegralType a
_)           = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimBRotateR IntegralType a
_)           (PrimBRotateR IntegralType a
_)           = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimPopCount IntegralType a
_)           (PrimPopCount IntegralType a
_)           = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimCountLeadingZeros IntegralType a
_)  (PrimCountLeadingZeros IntegralType a
_)  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimCountTrailingZeros IntegralType a
_) (PrimCountTrailingZeros IntegralType a
_) = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimFDiv FloatingType a
_)               (PrimFDiv FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimRecip FloatingType a
_)              (PrimRecip FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimSin FloatingType a
_)                (PrimSin FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimCos FloatingType a
_)                (PrimCos FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimTan FloatingType a
_)                (PrimTan FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAsin FloatingType a
_)               (PrimAsin FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAcos FloatingType a
_)               (PrimAcos FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAtan FloatingType a
_)               (PrimAtan FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimSinh FloatingType a
_)               (PrimSinh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimCosh FloatingType a
_)               (PrimCosh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimTanh FloatingType a
_)               (PrimTanh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAsinh FloatingType a
_)              (PrimAsinh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAcosh FloatingType a
_)              (PrimAcosh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAtanh FloatingType a
_)              (PrimAtanh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimExpFloating FloatingType a
_)        (PrimExpFloating FloatingType a
_)        = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimSqrt FloatingType a
_)               (PrimSqrt FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimLog FloatingType a
_)                (PrimLog FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimFPow FloatingType a
_)               (PrimFPow FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimLogBase FloatingType a
_)            (PrimLogBase FloatingType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimAtan2 FloatingType a
_)              (PrimAtan2 FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimTruncate FloatingType a
_ IntegralType b
s)         (PrimTruncate FloatingType a
_ IntegralType b
t)         = IntegralType b -> IntegralType b -> Maybe (b :~: b)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType b
s IntegralType b
t
matchPrimFun (PrimRound FloatingType a
_ IntegralType b
s)            (PrimRound FloatingType a
_ IntegralType b
t)            = IntegralType b -> IntegralType b -> Maybe (b :~: b)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType b
s IntegralType b
t
matchPrimFun (PrimFloor FloatingType a
_ IntegralType b
s)            (PrimFloor FloatingType a
_ IntegralType b
t)            = IntegralType b -> IntegralType b -> Maybe (b :~: b)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType b
s IntegralType b
t
matchPrimFun (PrimCeiling FloatingType a
_ IntegralType b
s)          (PrimCeiling FloatingType a
_ IntegralType b
t)          = IntegralType b -> IntegralType b -> Maybe (b :~: b)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType b
s IntegralType b
t
matchPrimFun (PrimIsNaN FloatingType a
_)              (PrimIsNaN FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimIsInfinite FloatingType a
_)         (PrimIsInfinite FloatingType a
_)         = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimLt SingleType a
_)                 (PrimLt SingleType a
_)                 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimGt SingleType a
_)                 (PrimGt SingleType a
_)                 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimLtEq SingleType a
_)               (PrimLtEq SingleType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimGtEq SingleType a
_)               (PrimGtEq SingleType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimEq SingleType a
_)                 (PrimEq SingleType a
_)                 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimNEq SingleType a
_)                (PrimNEq SingleType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimMax SingleType a
_)                (PrimMax SingleType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimMin SingleType a
_)                (PrimMin SingleType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun (PrimFromIntegral IntegralType a
_ NumType b
s)     (PrimFromIntegral IntegralType a
_ NumType b
t)     = NumType b -> NumType b -> Maybe (b :~: b)
forall s t. NumType s -> NumType t -> Maybe (s :~: t)
matchNumType NumType b
s NumType b
t
matchPrimFun (PrimToFloating NumType a
_ FloatingType b
s)       (PrimToFloating NumType a
_ FloatingType b
t)       = FloatingType b -> FloatingType b -> Maybe (b :~: b)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType b
s FloatingType b
t
matchPrimFun PrimFun (a -> s)
PrimLAnd                   PrimFun (a -> t)
PrimLAnd                   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun PrimFun (a -> s)
PrimLOr                    PrimFun (a -> t)
PrimLOr                    = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun PrimFun (a -> s)
PrimLNot                   PrimFun (a -> t)
PrimLNot                   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun PrimFun (a -> s)
_ PrimFun (a -> t)
_
  = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Contravariant function matching
--
{-# INLINEABLE matchPrimFun' #-}
matchPrimFun' :: PrimFun (s -> a) -> PrimFun (t -> a) -> Maybe (s :~: t)
matchPrimFun' :: PrimFun (s -> a) -> PrimFun (t -> a) -> Maybe (s :~: t)
matchPrimFun' (PrimAdd NumType a
_)                (PrimAdd NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimSub NumType a
_)                (PrimSub NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimMul NumType a
_)                (PrimMul NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimNeg NumType a
_)                (PrimNeg NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAbs NumType a
_)                (PrimAbs NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimSig NumType a
_)                (PrimSig NumType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimQuot IntegralType a
_)               (PrimQuot IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimRem IntegralType a
_)                (PrimRem IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimQuotRem IntegralType a
_)            (PrimQuotRem IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimIDiv IntegralType a
_)               (PrimIDiv IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimMod IntegralType a
_)                (PrimMod IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimDivMod IntegralType a
_)             (PrimDivMod IntegralType a
_)             = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBAnd IntegralType a
_)               (PrimBAnd IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBOr IntegralType a
_)                (PrimBOr IntegralType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBXor IntegralType a
_)               (PrimBXor IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBNot IntegralType a
_)               (PrimBNot IntegralType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBShiftL IntegralType a
_)            (PrimBShiftL IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBShiftR IntegralType a
_)            (PrimBShiftR IntegralType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBRotateL IntegralType a
_)           (PrimBRotateL IntegralType a
_)           = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimBRotateR IntegralType a
_)           (PrimBRotateR IntegralType a
_)           = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimPopCount IntegralType a
s)           (PrimPopCount IntegralType a
t)           = IntegralType a -> IntegralType a -> Maybe (a :~: a)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType a
s IntegralType a
t
matchPrimFun' (PrimCountLeadingZeros IntegralType a
s)  (PrimCountLeadingZeros IntegralType a
t)  = IntegralType a -> IntegralType a -> Maybe (a :~: a)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType a
s IntegralType a
t
matchPrimFun' (PrimCountTrailingZeros IntegralType a
s) (PrimCountTrailingZeros IntegralType a
t) = IntegralType a -> IntegralType a -> Maybe (a :~: a)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType a
s IntegralType a
t
matchPrimFun' (PrimFDiv FloatingType a
_)               (PrimFDiv FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimRecip FloatingType a
_)              (PrimRecip FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimSin FloatingType a
_)                (PrimSin FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimCos FloatingType a
_)                (PrimCos FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimTan FloatingType a
_)                (PrimTan FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAsin FloatingType a
_)               (PrimAsin FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAcos FloatingType a
_)               (PrimAcos FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAtan FloatingType a
_)               (PrimAtan FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimSinh FloatingType a
_)               (PrimSinh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimCosh FloatingType a
_)               (PrimCosh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimTanh FloatingType a
_)               (PrimTanh FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAsinh FloatingType a
_)              (PrimAsinh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAcosh FloatingType a
_)              (PrimAcosh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAtanh FloatingType a
_)              (PrimAtanh FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimExpFloating FloatingType a
_)        (PrimExpFloating FloatingType a
_)        = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimSqrt FloatingType a
_)               (PrimSqrt FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimLog FloatingType a
_)                (PrimLog FloatingType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimFPow FloatingType a
_)               (PrimFPow FloatingType a
_)               = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimLogBase FloatingType a
_)            (PrimLogBase FloatingType a
_)            = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimAtan2 FloatingType a
_)              (PrimAtan2 FloatingType a
_)              = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimTruncate FloatingType a
s IntegralType b
_)         (PrimTruncate FloatingType a
t IntegralType b
_)         = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimRound FloatingType a
s IntegralType b
_)            (PrimRound FloatingType a
t IntegralType b
_)            = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimFloor FloatingType a
s IntegralType b
_)            (PrimFloor FloatingType a
t IntegralType b
_)            = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimCeiling FloatingType a
s IntegralType b
_)          (PrimCeiling FloatingType a
t IntegralType b
_)          = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimIsNaN FloatingType a
s)              (PrimIsNaN FloatingType a
t)              = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimIsInfinite FloatingType a
s)         (PrimIsInfinite FloatingType a
t)         = FloatingType a -> FloatingType a -> Maybe (a :~: a)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType a
s FloatingType a
t
matchPrimFun' (PrimMax SingleType a
_)                (PrimMax SingleType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimMin SingleType a
_)                (PrimMin SingleType a
_)                = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' (PrimFromIntegral IntegralType a
s NumType b
_)     (PrimFromIntegral IntegralType a
t NumType b
_)     = IntegralType a -> IntegralType a -> Maybe (a :~: a)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType a
s IntegralType a
t
matchPrimFun' (PrimToFloating NumType a
s FloatingType b
_)       (PrimToFloating NumType a
t FloatingType b
_)       = NumType a -> NumType a -> Maybe (a :~: a)
forall s t. NumType s -> NumType t -> Maybe (s :~: t)
matchNumType NumType a
s NumType a
t
matchPrimFun' PrimFun (s -> a)
PrimLAnd                   PrimFun (t -> a)
PrimLAnd                   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' PrimFun (s -> a)
PrimLOr                    PrimFun (t -> a)
PrimLOr                    = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchPrimFun' PrimFun (s -> a)
PrimLNot                   PrimFun (t -> a)
PrimLNot                   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimLt SingleType a
s) (PrimLt SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimGt SingleType a
s) (PrimGt SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimLtEq SingleType a
s) (PrimLtEq SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimGtEq SingleType a
s) (PrimGtEq SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimEq SingleType a
s) (PrimEq SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' (PrimNEq SingleType a
s) (PrimNEq SingleType a
t)
  | Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl

matchPrimFun' PrimFun (s -> a)
_ PrimFun (t -> a)
_
  = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Match reified types
--
{-# INLINEABLE matchTypeR #-}
matchTypeR :: TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR :: TypeR s -> TypeR t -> Maybe (s :~: t)
matchTypeR = (forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y))
-> TypeR s -> TypeR t -> Maybe (s :~: t)
forall (s :: * -> *) t1 t2.
(forall u1 u2. s u1 -> s u2 -> Maybe (u1 :~: u2))
-> TupR s t1 -> TupR s t2 -> Maybe (t1 :~: t2)
matchTupR forall x y. ScalarType x -> ScalarType y -> Maybe (x :~: y)
matchScalarType


-- Match shapes (dimensionality)
--
-- XXX: Matching shapes is sort of a special case because the representation
-- types really are isomorphic to the surface type. However, 'gcast' does not
-- inline here, meaning that it will always do the fingerprint check, even if
-- the dimensions are known statically and thus the check could be elided as
-- a known branch.
--
{-# INLINEABLE matchShapeType #-}
matchShapeType :: forall s t. (Sugar.Shape s, Sugar.Shape t) => Maybe (s :~: t)
matchShapeType :: Maybe (s :~: t)
matchShapeType
  | Just EltR s :~: EltR t
Refl <- ShapeR (EltR s) -> ShapeR (EltR t) -> Maybe (EltR s :~: EltR t)
forall s t. ShapeR s -> ShapeR t -> Maybe (s :~: t)
matchShapeR (Shape s => ShapeR (EltR s)
forall sh. Shape sh => ShapeR (EltR sh)
Sugar.shapeR @s) (Shape t => ShapeR (EltR t)
forall sh. Shape sh => ShapeR (EltR sh)
Sugar.shapeR @t)
#ifdef ACCELERATE_INTERNAL_CHECKS
  = gcast Refl
#else
  = (s :~: t) -> Maybe (s :~: t)
forall a. a -> Maybe a
Just ((Any :~: Any) -> s :~: t
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
#endif
  | Bool
otherwise
  = Maybe (s :~: t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchShapeR #-}
matchShapeR :: forall s t. ShapeR s -> ShapeR t -> Maybe (s :~: t)
matchShapeR :: ShapeR s -> ShapeR t -> Maybe (s :~: t)
matchShapeR ShapeR s
ShapeRz ShapeR t
ShapeRz = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchShapeR (ShapeRsnoc ShapeR sh
shr1) (ShapeRsnoc ShapeR sh
shr2)
  | Just sh :~: sh
Refl <- ShapeR sh -> ShapeR sh -> Maybe (sh :~: sh)
forall s t. ShapeR s -> ShapeR t -> Maybe (s :~: t)
matchShapeR ShapeR sh
shr1 ShapeR sh
shr2
  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchShapeR ShapeR s
_ ShapeR t
_ = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Match reified type dictionaries
--
{-# INLINEABLE matchScalarType #-}
matchScalarType :: ScalarType s -> ScalarType t -> Maybe (s :~: t)
matchScalarType :: ScalarType s -> ScalarType t -> Maybe (s :~: t)
matchScalarType (SingleScalarType SingleType s
s) (SingleScalarType SingleType t
t) = SingleType s -> SingleType t -> Maybe (s :~: t)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType s
s SingleType t
t
matchScalarType (VectorScalarType VectorType (Vec n a)
s) (VectorScalarType VectorType (Vec n a)
t) = VectorType (Vec n a)
-> VectorType (Vec n a) -> Maybe (Vec n a :~: Vec n a)
forall (m :: Nat) (n :: Nat) s t.
VectorType (Vec n s)
-> VectorType (Vec m t) -> Maybe (Vec n s :~: Vec m t)
matchVectorType VectorType (Vec n a)
s VectorType (Vec n a)
t
matchScalarType ScalarType s
_                    ScalarType t
_                    = Maybe (s :~: t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchSingleType #-}
matchSingleType :: SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType :: SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType (NumSingleType NumType s
s) (NumSingleType NumType t
t) = NumType s -> NumType t -> Maybe (s :~: t)
forall s t. NumType s -> NumType t -> Maybe (s :~: t)
matchNumType NumType s
s NumType t
t

{-# INLINEABLE matchVectorType #-}
matchVectorType :: forall m n s t. VectorType (Vec n s) -> VectorType (Vec m t) -> Maybe (Vec n s :~: Vec m t)
matchVectorType :: VectorType (Vec n s)
-> VectorType (Vec m t) -> Maybe (Vec n s :~: Vec m t)
matchVectorType (VectorType Int
n SingleType a
s) (VectorType Int
m SingleType a
t)
  | Just n :~: m
Refl <- if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m
                   then (n :~: m) -> Maybe (n :~: m)
forall a. a -> Maybe a
Just ((Any :~: Any) -> n :~: m
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl :: n :~: m) -- XXX: we don't have an embedded KnownNat constraint, but
                   else Maybe (n :~: m)
forall a. Maybe a
Nothing                             -- this implementation is the same as 'GHC.TypeLits.sameNat'
  , Just a :~: a
Refl <- SingleType a -> SingleType a -> Maybe (a :~: a)
forall s t. SingleType s -> SingleType t -> Maybe (s :~: t)
matchSingleType SingleType a
s SingleType a
t
  = (Vec n s :~: Vec n s) -> Maybe (Vec n s :~: Vec n s)
forall a. a -> Maybe a
Just Vec n s :~: Vec n s
forall k (a :: k). a :~: a
Refl
matchVectorType VectorType (Vec n s)
_ VectorType (Vec m t)
_
  = Maybe (Vec n s :~: Vec m t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchNumType #-}
matchNumType :: NumType s -> NumType t -> Maybe (s :~: t)
matchNumType :: NumType s -> NumType t -> Maybe (s :~: t)
matchNumType (IntegralNumType IntegralType s
s) (IntegralNumType IntegralType t
t) = IntegralType s -> IntegralType t -> Maybe (s :~: t)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType s
s IntegralType t
t
matchNumType (FloatingNumType FloatingType s
s) (FloatingNumType FloatingType t
t) = FloatingType s -> FloatingType t -> Maybe (s :~: t)
forall s t. FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType s
s FloatingType t
t
matchNumType NumType s
_                   NumType t
_                   = Maybe (s :~: t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchBoundedType #-}
matchBoundedType :: BoundedType s -> BoundedType t -> Maybe (s :~: t)
matchBoundedType :: BoundedType s -> BoundedType t -> Maybe (s :~: t)
matchBoundedType (IntegralBoundedType IntegralType s
s) (IntegralBoundedType IntegralType t
t) = IntegralType s -> IntegralType t -> Maybe (s :~: t)
forall s t. IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType s
s IntegralType t
t

{-# INLINEABLE matchIntegralType #-}
matchIntegralType :: IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType :: IntegralType s -> IntegralType t -> Maybe (s :~: t)
matchIntegralType IntegralType s
TypeInt    IntegralType t
TypeInt    = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeInt8   IntegralType t
TypeInt8   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeInt16  IntegralType t
TypeInt16  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeInt32  IntegralType t
TypeInt32  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeInt64  IntegralType t
TypeInt64  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeWord   IntegralType t
TypeWord   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeWord8  IntegralType t
TypeWord8  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeWord16 IntegralType t
TypeWord16 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeWord32 IntegralType t
TypeWord32 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
TypeWord64 IntegralType t
TypeWord64 = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchIntegralType IntegralType s
_            IntegralType t
_            = Maybe (s :~: t)
forall a. Maybe a
Nothing

{-# INLINEABLE matchFloatingType #-}
matchFloatingType :: FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType :: FloatingType s -> FloatingType t -> Maybe (s :~: t)
matchFloatingType FloatingType s
TypeHalf   FloatingType t
TypeHalf   = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchFloatingType FloatingType s
TypeFloat  FloatingType t
TypeFloat  = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchFloatingType FloatingType s
TypeDouble FloatingType t
TypeDouble = (s :~: s) -> Maybe (s :~: s)
forall a. a -> Maybe a
Just s :~: s
forall k (a :: k). a :~: a
Refl
matchFloatingType FloatingType s
_            FloatingType t
_            = Maybe (s :~: t)
forall a. Maybe a
Nothing


-- Auxiliary
-- ---------

-- Discriminate binary functions that commute, and if so return the operands in
-- a stable ordering such that matching recognises expressions modulo
-- commutativity.
--
commutes
    :: forall env aenv a r.
       PrimFun (a -> r)
    -> OpenExp env aenv a
    -> Maybe (OpenExp env aenv a)
commutes :: PrimFun (a -> r)
-> OpenExp env aenv a -> Maybe (OpenExp env aenv a)
commutes PrimFun (a -> r)
f OpenExp env aenv a
x = case PrimFun (a -> r)
f of
  PrimAdd{}     -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimMul{}     -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimBAnd{}    -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimBOr{}     -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimBXor{}    -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimEq{}      -> OpenExp env aenv (a, a) -> Maybe (OpenExp env aenv (a, a))
forall a. a -> Maybe a
Just (OpenExp env aenv (a, a) -> OpenExp env aenv (a, a)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (a, a)
x)
  PrimNEq{}     -> OpenExp env aenv (a, a) -> Maybe (OpenExp env aenv (a, a))
forall a. a -> Maybe a
Just (OpenExp env aenv (a, a) -> OpenExp env aenv (a, a)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (a, a)
x)
  PrimMax{}     -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimMin{}     -> OpenExp env aenv (r, r) -> Maybe (OpenExp env aenv (r, r))
forall a. a -> Maybe a
Just (OpenExp env aenv (r, r) -> OpenExp env aenv (r, r)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (r, r)
x)
  PrimFun (a -> r)
PrimLAnd      -> OpenExp env aenv (PrimBool, PrimBool)
-> Maybe (OpenExp env aenv (PrimBool, PrimBool))
forall a. a -> Maybe a
Just (OpenExp env aenv (PrimBool, PrimBool)
-> OpenExp env aenv (PrimBool, PrimBool)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (PrimBool, PrimBool)
x)
  PrimFun (a -> r)
PrimLOr       -> OpenExp env aenv (PrimBool, PrimBool)
-> Maybe (OpenExp env aenv (PrimBool, PrimBool))
forall a. a -> Maybe a
Just (OpenExp env aenv (PrimBool, PrimBool)
-> OpenExp env aenv (PrimBool, PrimBool)
forall a'. OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv a
OpenExp env aenv (PrimBool, PrimBool)
x)
  PrimFun (a -> r)
_             -> Maybe (OpenExp env aenv a)
forall a. Maybe a
Nothing
  where
    swizzle :: OpenExp env aenv (a',a') -> OpenExp env aenv (a',a')
    swizzle :: OpenExp env aenv (a', a') -> OpenExp env aenv (a', a')
swizzle OpenExp env aenv (a', a')
exp
      | (OpenExp env aenv t1
a `Pair` OpenExp env aenv t2
b)  <- OpenExp env aenv (a', a')
exp
      , OpenExp env aenv t1 -> Hash
forall env aenv t. OpenExp env aenv t -> Hash
hashOpenExp OpenExp env aenv t1
a Hash -> Hash -> Bool
forall a. Ord a => a -> a -> Bool
> OpenExp env aenv t2 -> Hash
forall env aenv t. OpenExp env aenv t -> Hash
hashOpenExp OpenExp env aenv t2
b = OpenExp env aenv t2
b OpenExp env aenv t2
-> OpenExp env aenv t1 -> OpenExp env aenv (t2, t1)
forall env aenv t1 t2.
OpenExp env aenv t1
-> OpenExp env aenv t2 -> OpenExp env aenv (t1, t2)
`Pair` OpenExp env aenv t1
a
      --
      | Bool
otherwise                               = OpenExp env aenv (a', a')
exp