{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.Helpers
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.Helpers
  ( pattern UnaryTermPatt,
    pattern BinaryTermPatt,
    pattern TernaryTermPatt,
    pattern UnsafeUnaryTermPatt,
    pattern UnsafeBinaryTermPatt,
    pattern Unsafe1t21BinaryTermPatt,
    pattern Unsafe1u2t32TernaryTermPatt,
  )
where

import Data.Typeable
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Unsafe.Coerce

unsafeUnaryTermView :: forall a b tag. (Typeable tag) => Term a -> Maybe (tag, Term b)
unsafeUnaryTermView :: forall a b tag. Typeable tag => Term a -> Maybe (tag, Term b)
unsafeUnaryTermView (UnaryTerm Id
_ (tag
tag :: tagt) Term arg
t1) =
  case tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag of
    Just tag
t -> (tag, Term b) -> Maybe (tag, Term b)
forall a. a -> Maybe a
Just (tag
t, Term arg -> Term b
forall a b. a -> b
unsafeCoerce Term arg
t1)
    Maybe tag
Nothing -> Maybe (tag, Term b)
forall a. Maybe a
Nothing
-- (,) <$> cast tag <*> castTerm t1
unsafeUnaryTermView Term a
_ = Maybe (tag, Term b)
forall a. Maybe a
Nothing

pattern UnsafeUnaryTermPatt :: forall a b tag. (Typeable tag) => tag -> Term b -> Term a
pattern $mUnsafeUnaryTermPatt :: forall {r} {a} {b} {tag}.
Typeable tag =>
Term a -> (tag -> Term b -> r) -> (Void# -> r) -> r
UnsafeUnaryTermPatt tag t <- (unsafeUnaryTermView @a @b @tag -> Just (tag, t))

unaryTermView :: forall a b tag. (Typeable tag, Typeable b) => Term a -> Maybe (tag, Term b)
unaryTermView :: forall a b tag.
(Typeable tag, Typeable b) =>
Term a -> Maybe (tag, Term b)
unaryTermView (UnaryTerm Id
_ (tag
tag :: tagt) Term arg
t1) =
  (,) (tag -> Term b -> (tag, Term b))
-> Maybe tag -> Maybe (Term b -> (tag, Term b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag Maybe (Term b -> (tag, Term b))
-> Maybe (Term b) -> Maybe (tag, Term b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg -> Maybe (Term b)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg
t1
unaryTermView Term a
_ = Maybe (tag, Term b)
forall a. Maybe a
Nothing

pattern UnaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term a
pattern $mUnaryTermPatt :: forall {r} {a} {b} {tag}.
(Typeable tag, Typeable b) =>
Term a -> (tag -> Term b -> r) -> (Void# -> r) -> r
UnaryTermPatt tag t <- (unaryTermView @a @b @tag -> Just (tag, t))

unsafeBinaryTermView :: forall a b c tag. (Typeable tag) => Term a -> Maybe (tag, Term b, Term c)
unsafeBinaryTermView :: forall a b c tag.
Typeable tag =>
Term a -> Maybe (tag, Term b, Term c)
unsafeBinaryTermView (BinaryTerm Id
_ (tag
tag :: tagt) Term arg1
t1 Term arg2
t2) =
  case tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag of
    Just tag
t -> (tag, Term b, Term c) -> Maybe (tag, Term b, Term c)
forall a. a -> Maybe a
Just (tag
t, Term arg1 -> Term b
forall a b. a -> b
unsafeCoerce Term arg1
t1, Term arg2 -> Term c
forall a b. a -> b
unsafeCoerce Term arg2
t2)
    Maybe tag
Nothing -> Maybe (tag, Term b, Term c)
forall a. Maybe a
Nothing
-- (,) <$> cast tag <*> castTerm t1
unsafeBinaryTermView Term a
_ = Maybe (tag, Term b, Term c)
forall a. Maybe a
Nothing

pattern UnsafeBinaryTermPatt :: forall a b c tag. (Typeable tag) => tag -> Term b -> Term c -> Term a
pattern $mUnsafeBinaryTermPatt :: forall {r} {a} {b} {c} {tag}.
Typeable tag =>
Term a -> (tag -> Term b -> Term c -> r) -> (Void# -> r) -> r
UnsafeBinaryTermPatt tag t1 t2 <- (unsafeBinaryTermView @a @b @c @tag -> Just (tag, t1, t2))

unsafe1t21BinaryTermView :: forall a b tag. (Typeable tag, Typeable b) => Term a -> Maybe (tag, Term b, Term b)
unsafe1t21BinaryTermView :: forall a b tag.
(Typeable tag, Typeable b) =>
Term a -> Maybe (tag, Term b, Term b)
unsafe1t21BinaryTermView (BinaryTerm Id
_ (tag
tag :: tagt) Term arg1
t1 Term arg2
t2) =
  case (tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag, Term arg1 -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term arg1
t1) of
    (Just tag
tg, Just Term b
t1') -> (tag, Term b, Term b) -> Maybe (tag, Term b, Term b)
forall a. a -> Maybe a
Just (tag
tg, Term b
t1', Term arg2 -> Term b
forall a b. a -> b
unsafeCoerce Term arg2
t2)
    (Maybe tag, Maybe (Term b))
_ -> Maybe (tag, Term b, Term b)
forall a. Maybe a
Nothing
-- (,) <$> cast tag <*> castTerm t1
unsafe1t21BinaryTermView Term a
_ = Maybe (tag, Term b, Term b)
forall a. Maybe a
Nothing

pattern Unsafe1t21BinaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term b -> Term a
pattern $mUnsafe1t21BinaryTermPatt :: forall {r} {a} {b} {tag}.
(Typeable tag, Typeable b) =>
Term a -> (tag -> Term b -> Term b -> r) -> (Void# -> r) -> r
Unsafe1t21BinaryTermPatt tag t1 t2 <- (unsafe1t21BinaryTermView @a @b @tag -> Just (tag, t1, t2))

binaryTermView :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => Term a -> Maybe (tag, Term b, Term c)
binaryTermView :: forall a b c tag.
(Typeable tag, Typeable b, Typeable c) =>
Term a -> Maybe (tag, Term b, Term c)
binaryTermView (BinaryTerm Id
_ (tag
tag :: tagt) Term arg1
t1 Term arg2
t2) =
  (,,) (tag -> Term b -> Term c -> (tag, Term b, Term c))
-> Maybe tag -> Maybe (Term b -> Term c -> (tag, Term b, Term c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag Maybe (Term b -> Term c -> (tag, Term b, Term c))
-> Maybe (Term b) -> Maybe (Term c -> (tag, Term b, Term c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg1 -> Maybe (Term b)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg1
t1 Maybe (Term c -> (tag, Term b, Term c))
-> Maybe (Term c) -> Maybe (tag, Term b, Term c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg2 -> Maybe (Term c)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg2
t2
binaryTermView Term a
_ = Maybe (tag, Term b, Term c)
forall a. Maybe a
Nothing

pattern BinaryTermPatt :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => tag -> Term b -> Term c -> Term a
pattern $mBinaryTermPatt :: forall {r} {a} {b} {c} {tag}.
(Typeable tag, Typeable b, Typeable c) =>
Term a -> (tag -> Term b -> Term c -> r) -> (Void# -> r) -> r
BinaryTermPatt tag l r <- (binaryTermView @a @b @c @tag -> Just (tag, l, r))

unsafe1u2t32TernaryTermView ::
  forall a b c tag.
  (Typeable tag, Typeable c) =>
  Term a ->
  Maybe (tag, Term b, Term c, Term c)
unsafe1u2t32TernaryTermView :: forall a b c tag.
(Typeable tag, Typeable c) =>
Term a -> Maybe (tag, Term b, Term c, Term c)
unsafe1u2t32TernaryTermView (TernaryTerm Id
_ (tag
tag :: tagt) Term arg1
t1 Term arg2
t2 Term arg3
t3) =
  case (tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag, Term arg2 -> Maybe (Term c)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg2
t2) of
    (Just tag
tg, Just Term c
t2') -> (tag, Term b, Term c, Term c)
-> Maybe (tag, Term b, Term c, Term c)
forall a. a -> Maybe a
Just (tag
tg, Term arg1 -> Term b
forall a b. a -> b
unsafeCoerce Term arg1
t1, Term c
t2', Term arg3 -> Term c
forall a b. a -> b
unsafeCoerce Term arg3
t3)
    (Maybe tag, Maybe (Term c))
_ -> Maybe (tag, Term b, Term c, Term c)
forall a. Maybe a
Nothing
unsafe1u2t32TernaryTermView Term a
_ = Maybe (tag, Term b, Term c, Term c)
forall a. Maybe a
Nothing

pattern Unsafe1u2t32TernaryTermPatt ::
  forall a b c tag.
  (Typeable tag, Typeable c) =>
  tag ->
  Term b ->
  Term c ->
  Term c ->
  Term a
pattern $mUnsafe1u2t32TernaryTermPatt :: forall {r} {a} {b} {c} {tag}.
(Typeable tag, Typeable c) =>
Term a
-> (tag -> Term b -> Term c -> Term c -> r) -> (Void# -> r) -> r
Unsafe1u2t32TernaryTermPatt tag a b c <-
  (unsafe1u2t32TernaryTermView @a @b @c @tag -> Just (tag, a, b, c))

ternaryTermView ::
  forall a b c d tag.
  (Typeable tag, Typeable b, Typeable c, Typeable d) =>
  Term a ->
  Maybe (tag, Term b, Term c, Term d)
ternaryTermView :: forall a b c d tag.
(Typeable tag, Typeable b, Typeable c, Typeable d) =>
Term a -> Maybe (tag, Term b, Term c, Term d)
ternaryTermView (TernaryTerm Id
_ (tag
tag :: tagt) Term arg1
t1 Term arg2
t2 Term arg3
t3) =
  (,,,) (tag
 -> Term b -> Term c -> Term d -> (tag, Term b, Term c, Term d))
-> Maybe tag
-> Maybe
     (Term b -> Term c -> Term d -> (tag, Term b, Term c, Term d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tag -> Maybe tag
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast tag
tag Maybe (Term b -> Term c -> Term d -> (tag, Term b, Term c, Term d))
-> Maybe (Term b)
-> Maybe (Term c -> Term d -> (tag, Term b, Term c, Term d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg1 -> Maybe (Term b)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg1
t1 Maybe (Term c -> Term d -> (tag, Term b, Term c, Term d))
-> Maybe (Term c)
-> Maybe (Term d -> (tag, Term b, Term c, Term d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg2 -> Maybe (Term c)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg2
t2 Maybe (Term d -> (tag, Term b, Term c, Term d))
-> Maybe (Term d) -> Maybe (tag, Term b, Term c, Term d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term arg3 -> Maybe (Term d)
forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term arg3
t3
ternaryTermView Term a
_ = Maybe (tag, Term b, Term c, Term d)
forall a. Maybe a
Nothing

pattern TernaryTermPatt ::
  forall a b c d tag.
  (Typeable tag, Typeable b, Typeable c, Typeable d) =>
  tag ->
  Term b ->
  Term c ->
  Term d ->
  Term a
pattern $mTernaryTermPatt :: forall {r} {a} {b} {c} {d} {tag}.
(Typeable tag, Typeable b, Typeable c, Typeable d) =>
Term a
-> (tag -> Term b -> Term c -> Term d -> r) -> (Void# -> r) -> r
TernaryTermPatt tag a b c <- (ternaryTermView @a @b @c @d @tag -> Just (tag, a, b, c))