{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
-- Force PlutusType constraint when using fake strategy for wrappers
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Plutarch.Repr.Tag (
  PTag (..),
  TagLiftHelper (..),
  DeriveTagPlutusType (..),
  DeriveTagPLiftable (..),
) where

import Data.Proxy (Proxy (Proxy))

import Data.Coerce (coerce)
import Data.Kind (Type)
import GHC.Exts (Any)
import GHC.Generics qualified as GHC
import GHC.TypeError (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), TypeError)
import GHC.TypeLits (type (+))
import Generics.SOP (
  All,
  Code,
  I,
  K (K),
  NP (Nil, (:*)),
  NS (S, Z),
  SOP (SOP),
 )
import Generics.SOP qualified as SOP
import Plutarch.Builtin.Integer (PInteger)

import Plutarch.Builtin.Opaque (popaque)
import Plutarch.Internal.Lift (
  LiftError (OtherLiftError),
  PLiftable (AsHaskell, PlutusRepr, haskToRepr, plutToRepr, reprToHask, reprToPlut),
  PLifted (PLifted),
  pconstant,
 )
import Plutarch.Internal.PlutusType (
  DeriveFakePlutusType (DeriveFakePlutusType),
  PContravariant',
  PCovariant',
  PInner,
  PVariant',
  PlutusType,
  pcon',
  pmatch',
 )
import Plutarch.Internal.Term (S, Term)
import Plutarch.Repr.Internal (groupHandlers)
import Plutarch.Repr.Newtype (DeriveNewtypePlutusType (DeriveNewtypePlutusType))
import Plutarch.TermCont (pletC, unTermCont)

-- | @since 1.10.0
newtype PTag (struct :: [S -> Type]) (s :: S) = PTag
  { forall (struct :: [S -> Type]) (s :: S).
PTag struct s -> Term s PInteger
unPTag :: Term s PInteger
  -- ^ @since 1.10.0
  }
  deriving stock ((forall x. PTag struct s -> Rep (PTag struct s) x)
-> (forall x. Rep (PTag struct s) x -> PTag struct s)
-> Generic (PTag struct s)
forall (struct :: [S -> Type]) (s :: S) x.
Rep (PTag struct s) x -> PTag struct s
forall (struct :: [S -> Type]) (s :: S) x.
PTag struct s -> Rep (PTag struct s) x
forall x. Rep (PTag struct s) x -> PTag struct s
forall x. PTag struct s -> Rep (PTag struct s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (struct :: [S -> Type]) (s :: S) x.
PTag struct s -> Rep (PTag struct s) x
from :: forall x. PTag struct s -> Rep (PTag struct s) x
$cto :: forall (struct :: [S -> Type]) (s :: S) x.
Rep (PTag struct s) x -> PTag struct s
to :: forall x. Rep (PTag struct s) x -> PTag struct s
GHC.Generic)

-- | @since 1.10.0
instance SOP.Generic (PTag struct s)

-- | @since 1.10.0
deriving via DeriveNewtypePlutusType (PTag struct) instance PlutusType (PTag struct)

-- | @since IWP
newtype DeriveTagPlutusType (a :: S -> Type) s = DeriveTagPlutusType
  { forall (a :: S -> Type) (s :: S). DeriveTagPlutusType a s -> a s
unDeriveTagPlutusType :: a s
  -- ^ @since WIP
  }

{- | This derives tag-only PlutusType automatically. Resulted instances will use `PInteger` as underlying type, making this much more efficient than using regular Data/Scott/SOP based encoding. As name suggests, types with no-argument constructors can use this.

Example:
@@
data PFoo s = A | B | C | D | E
  deriving stock (GHC.Generic, Show)
  deriving anyclass (PEq, PIsData)
  deriving (PlutusType) via DeriveTagPlutusType PFoo

instance SOP.Generic (PFoo s)
@@

@since 1.10.0
-}
instance (forall s. TagTypeConstraints s a struct) => PlutusType (DeriveTagPlutusType a) where
  type PInner (DeriveTagPlutusType a) = PInteger
  type PCovariant' (DeriveTagPlutusType a) = (PCovariant' a)
  type PContravariant' (DeriveTagPlutusType a) = (PContravariant' a)
  type PVariant' (DeriveTagPlutusType a) = (PVariant' a)
  pcon' :: forall s. DeriveTagPlutusType a s -> Term s (PInner (DeriveTagPlutusType a))
  pcon' :: forall (s :: S).
DeriveTagPlutusType a s -> Term s (PInner (DeriveTagPlutusType a))
pcon' (DeriveTagPlutusType a s
x) =
    forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PInteger (AsHaskell PInteger -> Term s PInteger)
-> AsHaskell PInteger -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ SOP @Type I (Code (a s)) -> Int
forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
forall (f :: Type -> Type) (xs :: [[Type]]). SOP @Type f xs -> Int
SOP.hindex (SOP @Type I (Code (a s)) -> Int)
-> SOP @Type I (Code (a s)) -> Int
forall a b. (a -> b) -> a -> b
$ a s -> SOP @Type I (Code (a s))
forall a. Generic a => a -> Rep a
SOP.from a s
x

  pmatch' :: forall s b. Term s (PInner (DeriveTagPlutusType a)) -> (DeriveTagPlutusType a s -> Term s b) -> Term s b
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveTagPlutusType a))
-> (DeriveTagPlutusType a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveTagPlutusType a))
tag DeriveTagPlutusType a s -> Term s b
f = TermCont @b s (Term s b) -> Term s b
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ do
    -- plet here because tag might be a big computation
    Term s PInteger
tag' <- Term s (PInner (DeriveTagPlutusType a))
-> TermCont @b s (Term s (PInner (DeriveTagPlutusType a)))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s (Term s a)
pletC Term s (PInner (DeriveTagPlutusType a))
tag
    let
      g :: SOP I (Code (a s)) -> Term s b
      g :: SOP @Type I (Code (a s)) -> Term s b
g = DeriveTagPlutusType a s -> Term s b
f (DeriveTagPlutusType a s -> Term s b)
-> (SOP @Type I (Code (a s)) -> DeriveTagPlutusType a s)
-> SOP @Type I (Code (a s))
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveTagPlutusType a s
forall (a :: S -> Type) (s :: S). a s -> DeriveTagPlutusType a s
DeriveTagPlutusType (a s -> DeriveTagPlutusType a s)
-> (SOP @Type I (Code (a s)) -> a s)
-> SOP @Type I (Code (a s))
-> DeriveTagPlutusType a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP @Type I (Code (a s)) -> a s
forall a. Generic a => Rep a -> a
SOP.to

      go :: forall x xs. IsEmpty x => TagMatchHandler s b xs -> TagMatchHandler s b (x ': xs)
      go :: forall (x :: [Type]) (xs :: [[Type]]).
IsEmpty @Type x =>
TagMatchHandler s b xs -> TagMatchHandler s b ((':) @[Type] x xs)
go (TagMatchHandler Integer
-> (SOP @Type I xs -> Term s b)
-> NP @[Type] (K @[Type] (Integer, Term s b)) xs
rest) =
        (Integer
 -> (SOP @Type I ((':) @[Type] x xs) -> Term s b)
 -> NP @[Type] (K @[Type] (Integer, Term s b)) ((':) @[Type] x xs))
-> TagMatchHandler s b ((':) @[Type] x xs)
forall (s :: S) (b :: S -> Type) (struct :: [[Type]]).
(Integer
 -> (SOP @Type I struct -> Term s b)
 -> NP @[Type] (K @[Type] (Integer, Term s b)) struct)
-> TagMatchHandler s b struct
TagMatchHandler ((Integer
  -> (SOP @Type I ((':) @[Type] x xs) -> Term s b)
  -> NP @[Type] (K @[Type] (Integer, Term s b)) ((':) @[Type] x xs))
 -> TagMatchHandler s b ((':) @[Type] x xs))
-> (Integer
    -> (SOP @Type I ((':) @[Type] x xs) -> Term s b)
    -> NP @[Type] (K @[Type] (Integer, Term s b)) ((':) @[Type] x xs))
-> TagMatchHandler s b ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ \Integer
idx SOP @Type I ((':) @[Type] x xs) -> Term s b
handle ->
          (Integer, Term s b) -> K @[Type] (Integer, Term s b) x
forall k a (b :: k). a -> K @k a b
K (Integer
idx, SOP @Type I ((':) @[Type] x xs) -> Term s b
handle (SOP @Type I ((':) @[Type] x xs) -> Term s b)
-> SOP @Type I ((':) @[Type] x xs) -> Term s b
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) ((':) @[Type] x xs)
 -> SOP @Type I ((':) @[Type] x xs))
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ NP @Type I ('[] @Type)
-> NS @[Type] (NP @Type I) ((':) @[Type] ('[] @Type) xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) K @[Type] (Integer, Term s b) x
-> NP @[Type] (K @[Type] (Integer, Term s b)) xs
-> NP @[Type] (K @[Type] (Integer, Term s b)) ((':) @[Type] x xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* Integer
-> (SOP @Type I xs -> Term s b)
-> NP @[Type] (K @[Type] (Integer, Term s b)) xs
rest (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (\(SOP NS @[Type] (NP @Type I) xs
x) -> SOP @Type I ((':) @[Type] x xs) -> Term s b
handle (SOP @Type I ((':) @[Type] x xs) -> Term s b)
-> SOP @Type I ((':) @[Type] x xs) -> Term s b
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) ((':) @[Type] x xs)
 -> SOP @Type I ((':) @[Type] x xs))
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) xs
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[Type] (NP @Type I) xs
x)

      handlers' :: TagMatchHandler s b struct
      handlers' :: TagMatchHandler s b struct
handlers' = Proxy @([Type] -> Constraint) (IsEmpty @Type)
-> TagMatchHandler s b ('[] @[Type])
-> (forall (y :: [Type]) (ys :: [[Type]]).
    (IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
    TagMatchHandler s b ys -> TagMatchHandler s b ((':) @[Type] y ys))
-> TagMatchHandler s b struct
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (r :: [k] -> Type).
All @k c xs =>
proxy c
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, All @k c ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (proxy :: ([Type] -> Constraint) -> Type)
       (r :: [[Type]] -> Type).
proxy (IsEmpty @Type)
-> r ('[] @[Type])
-> (forall (y :: [Type]) (ys :: [[Type]]).
    (IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
    r ys -> r ((':) @[Type] y ys))
-> r struct
SOP.cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [Type] -> Constraint). Proxy @([Type] -> Constraint) t
Proxy @IsEmpty) ((Integer
 -> (SOP @Type I ('[] @[Type]) -> Term s b)
 -> NP @[Type] (K @[Type] (Integer, Term s b)) ('[] @[Type]))
-> TagMatchHandler s b ('[] @[Type])
forall (s :: S) (b :: S -> Type) (struct :: [[Type]]).
(Integer
 -> (SOP @Type I struct -> Term s b)
 -> NP @[Type] (K @[Type] (Integer, Term s b)) struct)
-> TagMatchHandler s b struct
TagMatchHandler ((Integer
  -> (SOP @Type I ('[] @[Type]) -> Term s b)
  -> NP @[Type] (K @[Type] (Integer, Term s b)) ('[] @[Type]))
 -> TagMatchHandler s b ('[] @[Type]))
-> (Integer
    -> (SOP @Type I ('[] @[Type]) -> Term s b)
    -> NP @[Type] (K @[Type] (Integer, Term s b)) ('[] @[Type]))
-> TagMatchHandler s b ('[] @[Type])
forall a b. (a -> b) -> a -> b
$ \Integer
_ SOP @Type I ('[] @[Type]) -> Term s b
_ -> NP @[Type] (K @[Type] (Integer, Term s b)) ('[] @[Type])
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) TagMatchHandler s b ys -> TagMatchHandler s b ((':) @[Type] y ys)
forall (y :: [Type]) (ys :: [[Type]]).
(IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
TagMatchHandler s b ys -> TagMatchHandler s b ((':) @[Type] y ys)
forall (x :: [Type]) (xs :: [[Type]]).
IsEmpty @Type x =>
TagMatchHandler s b xs -> TagMatchHandler s b ((':) @[Type] x xs)
go

      handlers :: [(Integer, Term s b)]
      handlers :: [(Integer, Term s b)]
handlers = NP @[Type] (K @[Type] (Integer, Term s b)) struct
-> CollapseTo @[Type] @[[Type]] (NP @[Type]) (Integer, Term s b)
forall (xs :: [[Type]]) a.
SListIN @[Type] @[[Type]] (NP @[Type]) xs =>
NP @[Type] (K @[Type] a) xs
-> CollapseTo @[Type] @[[Type]] (NP @[Type]) a
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
SOP.hcollapse (NP @[Type] (K @[Type] (Integer, Term s b)) struct
 -> CollapseTo @[Type] @[[Type]] (NP @[Type]) (Integer, Term s b))
-> NP @[Type] (K @[Type] (Integer, Term s b)) struct
-> CollapseTo @[Type] @[[Type]] (NP @[Type]) (Integer, Term s b)
forall a b. (a -> b) -> a -> b
$ TagMatchHandler s b struct
-> Integer
-> (SOP @Type I struct -> Term s b)
-> NP @[Type] (K @[Type] (Integer, Term s b)) struct
forall (s :: S) (b :: S -> Type) (struct :: [[Type]]).
TagMatchHandler s b struct
-> Integer
-> (SOP @Type I struct -> Term s b)
-> NP @[Type] (K @[Type] (Integer, Term s b)) struct
unTagMatchHandler TagMatchHandler s b struct
handlers' Integer
0 SOP @Type I struct -> Term s b
SOP @Type I (Code (a s)) -> Term s b
g

    Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s b -> TermCont @b s (Term s b))
-> Term s b -> TermCont @b s (Term s b)
forall a b. (a -> b) -> a -> b
$ [(Integer, Term s b)] -> Term s PInteger -> Term s b
forall (s :: S) (r :: S -> Type).
[(Integer, Term s r)] -> Term s PInteger -> Term s r
groupHandlers [(Integer, Term s b)]
handlers Term s PInteger
tag'

-- | @since 1.10.0
newtype TagLiftHelper r struct = TagLiftHelper
  { forall r (struct :: [[Type]]).
TagLiftHelper r struct -> Integer -> (SOP @Type I struct -> r) -> r
unTagLiftHelper :: Integer -> (SOP I struct -> r) -> r
  -- ^ @since 1.10.0
  }

-- Helpers

class x ~ '[] => IsEmpty (x :: [k])

instance x ~ '[] => IsEmpty '[]

type family TagTypePrettyError' n (xs :: [[Type]]) :: Bool where
  TagTypePrettyError' n ('[] ': rest) = TagTypePrettyError' (n + 1) rest
  TagTypePrettyError' n (invalid ': _) =
    TypeError
      ( 'Text "DeriveTagPlutusType only supports constructors without arguments. However, at constructor #"
          ':<>: 'ShowType n
          ':<>: 'Text ", I got:"
          ':$$: 'ShowType invalid
      )
  TagTypePrettyError' _ '[] = 'True

type TagTypePrettyError struct = TagTypePrettyError' 1 struct ~ 'True

class (SOP.Generic (a s), TagTypePrettyError (Code (a s)), Code (a s) ~ struct, All IsEmpty struct) => TagTypeConstraints s a struct | s a -> struct
instance (SOP.Generic (a s), TagTypePrettyError (Code (a s)), Code (a s) ~ struct, All IsEmpty struct) => TagTypeConstraints s a struct

newtype TagMatchHandler s b struct = TagMatchHandler
  { forall (s :: S) (b :: S -> Type) (struct :: [[Type]]).
TagMatchHandler s b struct
-> Integer
-> (SOP @Type I struct -> Term s b)
-> NP @[Type] (K @[Type] (Integer, Term s b)) struct
unTagMatchHandler :: Integer -> (SOP I struct -> Term s b) -> NP (K (Integer, Term s b)) struct
  }

-- | @since WIP
newtype DeriveTagPLiftable (a :: S -> Type) (h :: Type) s = DeriveTagPLiftable
  { forall (a :: S -> Type) h (s :: S). DeriveTagPLiftable a h s -> a s
unDeriveTagPLiftable :: a s
  -- ^ @since WIP
  }
  deriving stock ((forall x.
 DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s) x)
-> (forall x.
    Rep (DeriveTagPLiftable a h s) x -> DeriveTagPLiftable a h s)
-> Generic (DeriveTagPLiftable a h s)
forall x.
Rep (DeriveTagPLiftable a h s) x -> DeriveTagPLiftable a h s
forall x.
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) h (s :: S) x.
Rep (DeriveTagPLiftable a h s) x -> DeriveTagPLiftable a h s
forall (a :: S -> Type) h (s :: S) x.
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s) x
$cfrom :: forall (a :: S -> Type) h (s :: S) x.
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s) x
from :: forall x.
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s) x
$cto :: forall (a :: S -> Type) h (s :: S) x.
Rep (DeriveTagPLiftable a h s) x -> DeriveTagPLiftable a h s
to :: forall x.
Rep (DeriveTagPLiftable a h s) x -> DeriveTagPLiftable a h s
GHC.Generic)
  deriving anyclass (All @[Type] (SListI @Type) (Code (DeriveTagPLiftable a h s))
All @[Type] (SListI @Type) (Code (DeriveTagPLiftable a h s)) =>
(DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s))
-> (Rep (DeriveTagPLiftable a h s) -> DeriveTagPLiftable a h s)
-> Generic (DeriveTagPLiftable a h s)
Rep (DeriveTagPLiftable a h s) -> DeriveTagPLiftable a h s
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) h (s :: S).
All @[Type] (SListI @Type) (Code (DeriveTagPLiftable a h s))
forall (a :: S -> Type) h (s :: S).
Rep (DeriveTagPLiftable a h s) -> DeriveTagPLiftable a h s
forall (a :: S -> Type) h (s :: S).
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s)
$cfrom :: forall (a :: S -> Type) h (s :: S).
DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s)
from :: DeriveTagPLiftable a h s -> Rep (DeriveTagPLiftable a h s)
$cto :: forall (a :: S -> Type) h (s :: S).
Rep (DeriveTagPLiftable a h s) -> DeriveTagPLiftable a h s
to :: Rep (DeriveTagPLiftable a h s) -> DeriveTagPLiftable a h s
SOP.Generic)
  deriving
    ( -- | @since WIP
      (forall (s :: S).
 DeriveTagPLiftable a h s
 -> Term s (PInner (DeriveTagPLiftable a h)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (DeriveTagPLiftable a h))
    -> (DeriveTagPLiftable a h s -> Term s b) -> Term s b)
-> PlutusType (DeriveTagPLiftable a h)
forall (s :: S).
DeriveTagPLiftable a h s
-> Term s (PInner (DeriveTagPLiftable a h))
forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveTagPLiftable a h))
-> (DeriveTagPLiftable a h s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) h (s :: S).
DeriveTagPLiftable a h s
-> Term s (PInner (DeriveTagPLiftable a h))
forall (a :: S -> Type) h (s :: S) (b :: S -> Type).
Term s (PInner (DeriveTagPLiftable a h))
-> (DeriveTagPLiftable a h s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) h (s :: S).
DeriveTagPLiftable a h s
-> Term s (PInner (DeriveTagPLiftable a h))
pcon' :: forall (s :: S).
DeriveTagPLiftable a h s
-> Term s (PInner (DeriveTagPLiftable a h))
$cpmatch' :: forall (a :: S -> Type) h (s :: S) (b :: S -> Type).
Term s (PInner (DeriveTagPLiftable a h))
-> (DeriveTagPLiftable a h s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveTagPLiftable a h))
-> (DeriveTagPLiftable a h s -> Term s b) -> Term s b
PlutusType
    )
    via (DeriveFakePlutusType (DeriveTagPLiftable a h))

instance
  ( PlutusType a
  , SOP.Generic h
  , TagTypeConstraints Any a (Code h)
  ) =>
  PLiftable (DeriveTagPLiftable a h)
  where
  type AsHaskell (DeriveTagPLiftable a h) = h
  type PlutusRepr (DeriveTagPLiftable a h) = Integer

  haskToRepr :: AsHaskell (DeriveTagPLiftable a h)
-> PlutusRepr (DeriveTagPLiftable a h)
haskToRepr = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer)
-> (AsHaskell (DeriveTagPLiftable a h) -> Int)
-> AsHaskell (DeriveTagPLiftable a h)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP @Type I (Code (AsHaskell (DeriveTagPLiftable a h))) -> Int
forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
forall (f :: Type -> Type) (xs :: [[Type]]). SOP @Type f xs -> Int
SOP.hindex (SOP @Type I (Code (AsHaskell (DeriveTagPLiftable a h))) -> Int)
-> (AsHaskell (DeriveTagPLiftable a h)
    -> SOP @Type I (Code (AsHaskell (DeriveTagPLiftable a h))))
-> AsHaskell (DeriveTagPLiftable a h)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsHaskell (DeriveTagPLiftable a h)
-> SOP @Type I (Code (AsHaskell (DeriveTagPLiftable a h)))
forall a. Generic a => a -> Rep a
SOP.from

  reprToHask :: PlutusRepr (DeriveTagPLiftable a h)
-> Either LiftError (AsHaskell (DeriveTagPLiftable a h))
reprToHask PlutusRepr (DeriveTagPLiftable a h)
idx =
    let
      go :: IsEmpty x => TagLiftHelper r xs -> TagLiftHelper r (x ': xs)
      go :: forall (x :: [Type]) r (xs :: [[Type]]).
IsEmpty @Type x =>
TagLiftHelper r xs -> TagLiftHelper r ((':) @[Type] x xs)
go (TagLiftHelper Integer -> (SOP @Type I xs -> r) -> r
rest) =
        (Integer -> (SOP @Type I ((':) @[Type] x xs) -> r) -> r)
-> TagLiftHelper r ((':) @[Type] x xs)
forall r (struct :: [[Type]]).
(Integer -> (SOP @Type I struct -> r) -> r)
-> TagLiftHelper r struct
TagLiftHelper ((Integer -> (SOP @Type I ((':) @[Type] x xs) -> r) -> r)
 -> TagLiftHelper r ((':) @[Type] x xs))
-> (Integer -> (SOP @Type I ((':) @[Type] x xs) -> r) -> r)
-> TagLiftHelper r ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ \Integer
n SOP @Type I ((':) @[Type] x xs) -> r
f ->
          if PlutusRepr (DeriveTagPLiftable a h)
idx PlutusRepr (DeriveTagPLiftable a h)
-> PlutusRepr (DeriveTagPLiftable a h) -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
PlutusRepr (DeriveTagPLiftable a h)
n
            then SOP @Type I ((':) @[Type] x xs) -> r
f (SOP @Type I ((':) @[Type] x xs) -> r)
-> SOP @Type I ((':) @[Type] x xs) -> r
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) ((':) @[Type] x xs)
 -> SOP @Type I ((':) @[Type] x xs))
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ NP @Type I ('[] @Type)
-> NS @[Type] (NP @Type I) ((':) @[Type] ('[] @Type) xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil
            else Integer -> (SOP @Type I xs -> r) -> r
rest (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) \(SOP NS @[Type] (NP @Type I) xs
s) -> SOP @Type I ((':) @[Type] x xs) -> r
f (SOP @Type I ((':) @[Type] x xs) -> r)
-> SOP @Type I ((':) @[Type] x xs) -> r
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) ((':) @[Type] x xs)
 -> SOP @Type I ((':) @[Type] x xs))
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
-> SOP @Type I ((':) @[Type] x xs)
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) xs
-> NS @[Type] (NP @Type I) ((':) @[Type] x xs)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[Type] (NP @Type I) xs
s

      helper :: TagLiftHelper (Maybe h) (Code h)
      helper :: TagLiftHelper (Maybe h) (Code h)
helper = Proxy @([Type] -> Constraint) (IsEmpty @Type)
-> TagLiftHelper (Maybe h) ('[] @[Type])
-> (forall (y :: [Type]) (ys :: [[Type]]).
    (IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
    TagLiftHelper (Maybe h) ys
    -> TagLiftHelper (Maybe h) ((':) @[Type] y ys))
-> TagLiftHelper (Maybe h) (Code h)
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (r :: [k] -> Type).
All @k c xs =>
proxy c
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, All @k c ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (proxy :: ([Type] -> Constraint) -> Type)
       (r :: [[Type]] -> Type).
proxy (IsEmpty @Type)
-> r ('[] @[Type])
-> (forall (y :: [Type]) (ys :: [[Type]]).
    (IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
    r ys -> r ((':) @[Type] y ys))
-> r (Code h)
SOP.cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [Type] -> Constraint). Proxy @([Type] -> Constraint) t
Proxy @IsEmpty) ((Integer -> (SOP @Type I ('[] @[Type]) -> Maybe h) -> Maybe h)
-> TagLiftHelper (Maybe h) ('[] @[Type])
forall r (struct :: [[Type]]).
(Integer -> (SOP @Type I struct -> r) -> r)
-> TagLiftHelper r struct
TagLiftHelper \Integer
_ SOP @Type I ('[] @[Type]) -> Maybe h
_ -> Maybe h
forall a. Maybe a
Nothing) TagLiftHelper (Maybe h) ys
-> TagLiftHelper (Maybe h) ((':) @[Type] y ys)
forall (y :: [Type]) (ys :: [[Type]]).
(IsEmpty @Type y, All @[Type] (IsEmpty @Type) ys) =>
TagLiftHelper (Maybe h) ys
-> TagLiftHelper (Maybe h) ((':) @[Type] y ys)
forall (x :: [Type]) r (xs :: [[Type]]).
IsEmpty @Type x =>
TagLiftHelper r xs -> TagLiftHelper r ((':) @[Type] x xs)
go
     in
      Either LiftError (AsHaskell (DeriveTagPLiftable a h))
-> (AsHaskell (DeriveTagPLiftable a h)
    -> Either LiftError (AsHaskell (DeriveTagPLiftable a h)))
-> Maybe (AsHaskell (DeriveTagPLiftable a h))
-> Either LiftError (AsHaskell (DeriveTagPLiftable a h))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (LiftError -> Either LiftError (AsHaskell (DeriveTagPLiftable a h))
forall a b. a -> Either a b
Left (Text -> LiftError
OtherLiftError Text
"Invalid index")) AsHaskell (DeriveTagPLiftable a h)
-> Either LiftError (AsHaskell (DeriveTagPLiftable a h))
forall a b. b -> Either a b
Right (Maybe (AsHaskell (DeriveTagPLiftable a h))
 -> Either LiftError (AsHaskell (DeriveTagPLiftable a h)))
-> Maybe (AsHaskell (DeriveTagPLiftable a h))
-> Either LiftError (AsHaskell (DeriveTagPLiftable a h))
forall a b. (a -> b) -> a -> b
$ TagLiftHelper (Maybe h) (Code h)
-> Integer -> (SOP @Type I (Code h) -> Maybe h) -> Maybe h
forall r (struct :: [[Type]]).
TagLiftHelper r struct -> Integer -> (SOP @Type I struct -> r) -> r
unTagLiftHelper TagLiftHelper (Maybe h) (Code h)
helper Integer
0 (h -> Maybe h
forall a. a -> Maybe a
Just (h -> Maybe h)
-> (SOP @Type I (Code h) -> h) -> SOP @Type I (Code h) -> Maybe h
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SOP @Type I (Code h) -> h
forall a. Generic a => Rep a -> a
SOP.to)

  -- NOTE: Do we need index boudns checking in these two?

  reprToPlut :: forall (s :: S).
PlutusRepr (DeriveTagPLiftable a h)
-> PLifted s (DeriveTagPLiftable a h)
reprToPlut PlutusRepr (DeriveTagPLiftable a h)
idx = Term s POpaque -> PLifted s (DeriveTagPLiftable a h)
forall (s :: S) (a :: S -> Type). Term s POpaque -> PLifted s a
PLifted (Term s POpaque -> PLifted s (DeriveTagPLiftable a h))
-> Term s POpaque -> PLifted s (DeriveTagPLiftable a h)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s PInteger -> Term s POpaque)
-> Term s PInteger -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PInteger PlutusRepr (DeriveTagPLiftable a h)
AsHaskell PInteger
idx

  plutToRepr :: (forall (s :: S). PLifted s (DeriveTagPLiftable a h))
-> Either LiftError (PlutusRepr (DeriveTagPLiftable a h))
plutToRepr forall (s :: S). PLifted s (DeriveTagPLiftable a h)
p = forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @PInteger ((forall (s :: S). PLifted s PInteger)
 -> Either LiftError (PlutusRepr PInteger))
-> (forall (s :: S). PLifted s PInteger)
-> Either LiftError (PlutusRepr PInteger)
forall a b. (a -> b) -> a -> b
$ PLifted s (DeriveTagPLiftable a h) -> PLifted s PInteger
forall a b. Coercible @Type a b => a -> b
coerce PLifted s (DeriveTagPLiftable a h)
forall (s :: S). PLifted s (DeriveTagPLiftable a h)
p