{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Plutarch.Repr.Internal (
  RecAsHaskell,
  StructAsHaskell,
  PStruct (PStruct, unPStruct),
  PRec (PRec, unPRec),
  pletL,
  grecEq,
  gstructEq,
  groupHandlers,
  StructSameRepr,
  UnTermRec,
  UnTermStruct,
  UnTermStruct',
  RecTypePrettyError,
) where

import Control.Arrow (Arrow (..))
import Data.HashMap.Strict qualified as HM
import Data.Hashable (Hashed)
import Data.Kind (Type)
import Data.List (sort, sortBy)
import Data.Ord (comparing)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeError (ErrorMessage (Text), TypeError)
import Generics.SOP (
  All,
  All2,
  AllZipN,
  Code,
  I,
  K (K),
  LiftedCoercible,
  NP (Nil, (:*)),
  NS (S, Z),
  Prod,
  SListI,
  SOP (SOP),
  ccompare_SOP,
  hcliftA2,
  hcollapse,
  para_SList,
 )
import Generics.SOP qualified as SOP
import Plutarch.Builtin.Bool (PBool, pif)
import Plutarch.Builtin.Integer (PInteger, pconstantInteger)
import Plutarch.Internal.Eq (PEq, (#==))
import Plutarch.Internal.Lift (AsHaskell, pconstant)
import Plutarch.Internal.Term (RawTerm, S, Term, plet)
import Plutarch.Internal.TermCont (hashOpenTerm, unTermCont)

-- | @since 1.10.0
newtype PStruct (struct :: [[S -> Type]]) (s :: S) = PStruct
  { forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> SOP @(S -> Type) (Term s) struct
unPStruct :: SOP (Term s) struct
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
newtype PRec (struct :: [S -> Type]) (s :: S) = PRec
  { forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> NP @(S -> Type) (Term s) struct
unPRec :: NP (Term s) struct
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
pletL :: All SListI as => SOP (Term s) as -> (SOP (Term s) as -> Term s r) -> Term s r
pletL :: forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
All @[S -> Type] (SListI @(S -> Type)) as =>
SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL (SOP (Z NP @(S -> Type) (Term s) x
x)) SOP @(S -> Type) (Term s) as -> Term s r
f = NP @(S -> Type) (Term s) x
-> (NP @(S -> Type) (Term s) x -> Term s r) -> Term s r
forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL' NP @(S -> Type) (Term s) x
x \NP @(S -> Type) (Term s) x
x' -> SOP @(S -> Type) (Term s) as -> Term s r
f (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
 -> SOP @(S -> Type) (Term s) as)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) x
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] x xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @(S -> Type) (Term s) x
x')
pletL (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs)) SOP @(S -> Type) (Term s) as -> Term s r
f = SOP @(S -> Type) (Term s) xs
-> (SOP @(S -> Type) (Term s) xs -> Term s r) -> Term s r
forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
All @[S -> Type] (SListI @(S -> Type)) as =>
SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL (NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
-> SOP @(S -> Type) (Term s) xs
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs) \(SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs') -> SOP @(S -> Type) (Term s) as -> Term s r
f (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
 -> SOP @(S -> Type) (Term s) as)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] x xs)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs')

-- NOTE/TODO: These will generate large blob code, not too efficient unfortunately.
-- We are stuck with this for SOP and Scott however. Need some benchmark
-- reason: https://github.com/IntersectMBO/plutus/pull/5440

-- | @since 1.10.0
grecEq ::
  forall (s :: S) (struct :: [S -> Type]).
  All PEq struct =>
  NP (Term s) struct ->
  NP (Term s) struct ->
  Term s PBool
grecEq :: forall (s :: S) (struct :: [S -> Type]).
All @(S -> Type) PEq struct =>
NP @(S -> Type) (Term s) struct
-> NP @(S -> Type) (Term s) struct -> Term s PBool
grecEq NP @(S -> Type) (Term s) struct
x NP @(S -> Type) (Term s) struct
y = [Term s PBool] -> Term s PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands ([Term s PBool] -> Term s PBool) -> [Term s PBool] -> Term s PBool
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (K @(S -> Type) (Term s PBool)) struct
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool)
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> 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
hcollapse (NP @(S -> Type) (K @(S -> Type) (Term s PBool)) struct
 -> CollapseTo
      @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool))
-> NP @(S -> Type) (K @(S -> Type) (Term s PBool)) struct
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PEq
-> (forall (a :: S -> Type).
    PEq a =>
    Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a)
-> Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s) struct
-> NP @(S -> Type) (Term s) struct
-> NP @(S -> Type) (K @(S -> Type) (Term s PBool)) struct
forall {k} {l} (h :: (k -> Type) -> l -> Type)
       (c :: k -> Constraint) (xs :: l)
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
       (f' :: k -> Type) (f'' :: k -> Type).
(AllN @k @l (Prod @k @l h) c xs, HAp @k @l h,
 HAp @k @l (Prod @k @l h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod @k @l h f xs
-> h f' xs
-> h f'' xs
hcliftA2 (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PEq) (\Term s a
a Term s a
b -> Term s PBool -> K @(S -> Type) (Term s PBool) a
forall k a (b :: k). a -> K @k a b
K (Term s a
a Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
b)) Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s) struct
NP @(S -> Type) (Term s) struct
x NP @(S -> Type) (Term s) struct
y

-- | @since 1.10.0
gstructEq ::
  forall (s :: S) (struct :: [[S -> Type]]).
  All2 PEq struct =>
  SOP (Term s) struct ->
  SOP (Term s) struct ->
  Term s PBool
gstructEq :: forall (s :: S) (struct :: [[S -> Type]]).
All2 @(S -> Type) PEq struct =>
SOP @(S -> Type) (Term s) struct
-> SOP @(S -> Type) (Term s) struct -> Term s PBool
gstructEq SOP @(S -> Type) (Term s) struct
x SOP @(S -> Type) (Term s) struct
y =
  let
    f :: forall xs. All PEq xs => NP (Term _) xs -> NP (Term _) xs -> Term _ PBool
    f :: NP @(S -> Type) (Term w) xs
-> NP @(S -> Type) (Term w) xs -> Term w PBool
f NP @(S -> Type) (Term w) xs
a NP @(S -> Type) (Term w) xs
b = [Term w PBool] -> Term w PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands ([Term w PBool] -> Term w PBool) -> [Term w PBool] -> Term w PBool
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (K @(S -> Type) (Term w PBool)) xs
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term w PBool)
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> 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
hcollapse (NP @(S -> Type) (K @(S -> Type) (Term w PBool)) xs
 -> CollapseTo
      @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term w PBool))
-> NP @(S -> Type) (K @(S -> Type) (Term w PBool)) xs
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term w PBool)
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PEq
-> (forall (a :: S -> Type).
    PEq a =>
    Term w a -> Term w a -> K @(S -> Type) (Term w PBool) a)
-> Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term w) xs
-> NP @(S -> Type) (Term w) xs
-> NP @(S -> Type) (K @(S -> Type) (Term w PBool)) xs
forall {k} {l} (h :: (k -> Type) -> l -> Type)
       (c :: k -> Constraint) (xs :: l)
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
       (f' :: k -> Type) (f'' :: k -> Type).
(AllN @k @l (Prod @k @l h) c xs, HAp @k @l h,
 HAp @k @l (Prod @k @l h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod @k @l h f xs
-> h f' xs
-> h f'' xs
hcliftA2 (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PEq) (\Term w a
a' Term w a
b' -> Term w PBool -> K @(S -> Type) (Term w PBool) a
forall k a (b :: k). a -> K @k a b
K (Term w a
a' Term w a -> Term w a -> Term w PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term w a
b')) Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term w) xs
NP @(S -> Type) (Term w) xs
a NP @(S -> Type) (Term w) xs
b
   in
    Proxy @((S -> Type) -> Constraint) PEq
-> Term s PBool
-> (forall (xs :: [S -> Type]).
    All @(S -> Type) PEq xs =>
    NP @(S -> Type) (Term s) xs
    -> NP @(S -> Type) (Term s) xs -> Term s PBool)
-> Term s PBool
-> SOP @(S -> Type) (Term s) struct
-> SOP @(S -> Type) (Term s) struct
-> Term s PBool
forall {k} (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> Type) r (f :: k -> Type)
       (g :: k -> Type) (xss :: [[k]]).
All2 @k c xss =>
proxy c
-> r
-> (forall (xs :: [k]).
    All @k c xs =>
    NP @k f xs -> NP @k g xs -> r)
-> r
-> SOP @k f xss
-> SOP @k g xss
-> r
ccompare_SOP
      (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PEq)
      (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PBool Bool
AsHaskell PBool
False)
      NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (Term s) xs -> Term s PBool
forall (xs :: [S -> Type]).
All @(S -> Type) PEq xs =>
NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (Term s) xs -> Term s PBool
forall (xs :: [S -> Type]) {w :: S}.
All @(S -> Type) PEq xs =>
NP @(S -> Type) (Term w) xs
-> NP @(S -> Type) (Term w) xs -> Term w PBool
f
      (forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PBool Bool
AsHaskell PBool
False)
      SOP @(S -> Type) (Term s) struct
x
      SOP @(S -> Type) (Term s) struct
y

{- | This function handles optimization of function that require multiple handlers by checking hashes of each
| handler item and merging them in a way it will minimize size and cost of all computation

@since 1.10.0
-}
groupHandlers :: forall (s :: S) (r :: S -> Type). [(Integer, Term s r)] -> Term s PInteger -> Term s r
groupHandlers :: forall (s :: S) (r :: S -> Type).
[(Integer, Term s r)] -> Term s PInteger -> Term s r
groupHandlers [(Integer, Term s r)]
handlers Term s PInteger
idx = TermCont @r s (Term s r) -> Term s r
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @r s (Term s r) -> Term s r)
-> TermCont @r s (Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ do
  [(Integer, (Term s r, Hashed RawTerm))]
handlersWithHash :: [(Integer, (Term s b, Hashed RawTerm))] <-
    ((Integer, Term s r)
 -> TermCont @r s (Integer, (Term s r, Hashed RawTerm)))
-> [(Integer, Term s r)]
-> TermCont @r s [(Integer, (Term s r, Hashed RawTerm))]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Integer
i, Term s r
t) -> (\Hashed RawTerm
hash -> (Integer
i, (Term s r
t, Hashed RawTerm
hash))) (Hashed RawTerm -> (Integer, (Term s r, Hashed RawTerm)))
-> TermCont @r s (Hashed RawTerm)
-> TermCont @r s (Integer, (Term s r, Hashed RawTerm))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s r -> TermCont @r s (Hashed RawTerm)
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s (Hashed RawTerm)
hashOpenTerm Term s r
t) [(Integer, Term s r)]
handlers

  let
    groupedHandlers :: [([Integer], Term s b)]
    groupedHandlers :: [([Integer], Term s r)]
groupedHandlers =
      (([Integer], Term s r) -> ([Integer], Term s r) -> Ordering)
-> [([Integer], Term s r)] -> [([Integer], Term s r)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((([Integer], Term s r) -> (Int, [Integer]))
-> ([Integer], Term s r) -> ([Integer], Term s r) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (([Integer] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length ([Integer] -> Int)
-> (([Integer], Term s r) -> [Integer])
-> ([Integer], Term s r)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Integer], Term s r) -> [Integer]
forall a b. (a, b) -> a
fst) (([Integer], Term s r) -> Int)
-> (([Integer], Term s r) -> [Integer])
-> ([Integer], Term s r)
-> (Int, [Integer])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ([Integer], Term s r) -> [Integer]
forall a b. (a, b) -> a
fst))
        ([([Integer], Term s r)] -> [([Integer], Term s r)])
-> ([(Hashed RawTerm, [(Integer, Term s r)])]
    -> [([Integer], Term s r)])
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> [([Integer], Term s r)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Integer], Term s r) -> ([Integer], Term s r))
-> [([Integer], Term s r)] -> [([Integer], Term s r)]
forall a b. (a -> b) -> [a] -> [b]
map (([Integer] -> [Integer])
-> ([Integer], Term s r) -> ([Integer], Term s r)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first [Integer] -> [Integer]
forall a. Ord a => [a] -> [a]
sort)
        ([([Integer], Term s r)] -> [([Integer], Term s r)])
-> ([(Hashed RawTerm, [(Integer, Term s r)])]
    -> [([Integer], Term s r)])
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> [([Integer], Term s r)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap (Hashed RawTerm) ([Integer], Term s r)
-> [([Integer], Term s r)]
forall k v. HashMap k v -> [v]
HM.elems
        (HashMap (Hashed RawTerm) ([Integer], Term s r)
 -> [([Integer], Term s r)])
-> ([(Hashed RawTerm, [(Integer, Term s r)])]
    -> HashMap (Hashed RawTerm) ([Integer], Term s r))
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> [([Integer], Term s r)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Integer, Term s r)] -> ([Integer], Term s r))
-> HashMap (Hashed RawTerm) [(Integer, Term s r)]
-> HashMap (Hashed RawTerm) ([Integer], Term s r)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HM.map (\[(Integer, Term s r)]
xs -> (((Integer, Term s r) -> Integer)
-> [(Integer, Term s r)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, Term s r) -> Integer
forall a b. (a, b) -> a
fst [(Integer, Term s r)]
xs, (Integer, Term s r) -> Term s r
forall a b. (a, b) -> b
snd ((Integer, Term s r) -> Term s r)
-> (Integer, Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ [(Integer, Term s r)] -> (Integer, Term s r)
forall a. HasCallStack => [a] -> a
head [(Integer, Term s r)]
xs))
        (HashMap (Hashed RawTerm) [(Integer, Term s r)]
 -> HashMap (Hashed RawTerm) ([Integer], Term s r))
-> ([(Hashed RawTerm, [(Integer, Term s r)])]
    -> HashMap (Hashed RawTerm) [(Integer, Term s r)])
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> HashMap (Hashed RawTerm) ([Integer], Term s r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Integer, Term s r)]
 -> [(Integer, Term s r)] -> [(Integer, Term s r)])
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> HashMap (Hashed RawTerm) [(Integer, Term s r)]
forall k v. Hashable k => (v -> v -> v) -> [(k, v)] -> HashMap k v
HM.fromListWith (([(Integer, Term s r)]
 -> [(Integer, Term s r)] -> [(Integer, Term s r)])
-> [(Integer, Term s r)]
-> [(Integer, Term s r)]
-> [(Integer, Term s r)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [(Integer, Term s r)]
-> [(Integer, Term s r)] -> [(Integer, Term s r)]
forall a. [a] -> [a] -> [a]
(++))
        ([(Hashed RawTerm, [(Integer, Term s r)])]
 -> [([Integer], Term s r)])
-> [(Hashed RawTerm, [(Integer, Term s r)])]
-> [([Integer], Term s r)]
forall a b. (a -> b) -> a -> b
$ [(Hashed RawTerm
h, [(Integer
i, Term s r
t)]) | (Integer
i, (Term s r
t, Hashed RawTerm
h)) <- [(Integer, (Term s r, Hashed RawTerm))]
handlersWithHash]

  Term s r -> TermCont @r s (Term s r)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s r -> TermCont @r s (Term s r))
-> Term s r -> TermCont @r s (Term s r)
forall a b. (a -> b) -> a -> b
$
    let
      -- This one builds chain of #&& condition, making if one per groups
      pgo :: [([Integer], Term s b)] -> Term s b
      pgo :: [([Integer], Term s r)] -> Term s r
pgo [([Integer]
_, Term s r
t)] = Term s r
t
      pgo [([Integer]
is, Term s r
t), ([Integer]
_, Term s r
t')] =
        Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif ([Term s PBool] -> Term s PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands ([Term s PBool] -> Term s PBool) -> [Term s PBool] -> Term s PBool
forall a b. (a -> b) -> a -> b
$ (\Integer
i -> Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
idx) (Integer -> Term s PBool) -> [Integer] -> [Term s PBool]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer]
is) Term s r
t Term s r
t'
      pgo (([Integer]
is, Term s r
t) : [([Integer], Term s r)]
rest) =
        Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif ([Term s PBool] -> Term s PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands ([Term s PBool] -> Term s PBool) -> [Term s PBool] -> Term s PBool
forall a b. (a -> b) -> a -> b
$ (\Integer
i -> Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
idx) (Integer -> Term s PBool) -> [Integer] -> [Term s PBool]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer]
is) Term s r
t ([([Integer], Term s r)] -> Term s r
pgo [([Integer], Term s r)]
rest)
      pgo [] = [Char] -> Term s r
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

      -- This one builds if one per every entry. This is bad because it duplicates handler
      buildIfs :: [Integer] -> Term s b -> (Term s b -> Term s b)
      buildIfs :: [Integer] -> Term s r -> Term s r -> Term s r
buildIfs [] Term s r
_ = Term s r -> Term s r
forall a. a -> a
id
      buildIfs (Integer
i : [Integer]
is) Term s r
t =
        [Integer] -> Term s r -> Term s r -> Term s r
buildIfs [Integer]
is Term s r
t (Term s r -> Term s r)
-> (Term s r -> Term s r) -> Term s r -> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
idx) Term s r
t

      pgo' :: [([Integer], Term s b)] -> Term s b
      pgo' :: [([Integer], Term s r)] -> Term s r
pgo' [([Integer]
is, Term s r
t), ([Integer]
_, Term s r
t')] = [Integer] -> Term s r -> Term s r -> Term s r
buildIfs [Integer]
is Term s r
t Term s r
t'
      pgo' (([Integer]
is, Term s r
t) : [([Integer], Term s r)]
rest) = [Integer] -> Term s r -> Term s r -> Term s r
buildIfs [Integer]
is Term s r
t (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ [([Integer], Term s r)] -> Term s r
pgo' [([Integer], Term s r)]
rest
      pgo' [] = [Char] -> Term s r
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

      -- So that GHC doesn't complain
      _a :: [([Integer], Term s r)] -> Term s r
_a = [([Integer], Term s r)] -> Term s r
pgo'
      _b :: [([Integer], Term s r)] -> Term s r
_b = [([Integer], Term s r)] -> Term s r
pgo
     in
      -- first one seems to be faster
      [([Integer], Term s r)] -> Term s r
pgo [([Integer], Term s r)]
groupedHandlers

-- | @since 1.10.0
class
  ( SOP.Generic (a s)
  , AllZipN @Type (Prod SOP) (LiftedCoercible I (Term s)) (Code (a s)) struct
  , AllZipN @Type (Prod SOP) (LiftedCoercible (Term s) I) struct (Code (a s))
  ) =>
  StructSameRepr (s :: S) (a :: S -> Type) (struct :: [k])

instance
  ( SOP.Generic (a s)
  , AllZipN @Type (Prod SOP) (LiftedCoercible I (Term s)) (Code (a s)) struct
  , AllZipN @Type (Prod SOP) (LiftedCoercible (Term s) I) struct (Code (a s))
  ) =>
  StructSameRepr s a struct

-- | @since 1.10.0
type family UnTermRec (struct :: [Type]) :: [S -> Type] where
  UnTermRec '[] = '[]
  UnTermRec (Term _ a ': rest) = a ': UnTermRec rest

-- | @since 1.10.0
type UnTermStruct x = UnTermStruct' (Code x)

-- | @since 1.10.0
type RecTypePrettyError (struct :: [[k]]) = RecTypePrettyError' struct ~ 'True

-- Helpers

newtype PLetL s r as = PLetL {forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
unPLetL :: NP (Term s) as -> (NP (Term s) as -> Term s r) -> Term s r}

pletL' :: SListI as => NP (Term s) as -> (NP (Term s) as -> Term s r) -> Term s r
pletL' :: forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL' = PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
unPLetL (PLetL s r as
 -> NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r)
 -> Term s r)
-> PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ PLetL s r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PLetL s r ys -> PLetL s r ((':) @(S -> Type) y ys))
-> PLetL s r as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    SListI @a ys =>
    r ys -> r ((':) @a y ys))
-> r xs
para_SList
  ((NP @(S -> Type) (Term s) ('[] @(S -> Type))
 -> (NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r)
 -> Term s r)
-> PLetL s r ('[] @(S -> Type))
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r)
-> PLetL s r as
PLetL \NP @(S -> Type) (Term s) ('[] @(S -> Type))
Nil NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r
f -> NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil)
  \(PLetL NP @(S -> Type) (Term s) ys
-> (NP @(S -> Type) (Term s) ys -> Term s r) -> Term s r
prev) -> (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
 -> (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r)
 -> Term s r)
-> PLetL s r ((':) @(S -> Type) y ys)
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r)
-> PLetL s r as
PLetL \(Term s x
x :* NP @(S -> Type) (Term s) xs
xs) NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
f -> Term s x -> (Term s x -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s x
x \Term s x
x' ->
    NP @(S -> Type) (Term s) ys
-> (NP @(S -> Type) (Term s) ys -> Term s r) -> Term s r
prev NP @(S -> Type) (Term s) ys
NP @(S -> Type) (Term s) xs
xs (\NP @(S -> Type) (Term s) ys
xs' -> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
f (Term s x
x' Term s x
-> NP @(S -> Type) (Term s) ys
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) x ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @(S -> Type) (Term s) ys
xs'))

type family UnTermStruct' (struct :: [[Type]]) :: [[S -> Type]] where
  UnTermStruct' '[] = '[]
  UnTermStruct' (x ': rest) = UnTermRec x ': UnTermStruct' rest

type RecTypePrettyError' :: forall {k}. [[k]] -> Bool
type family RecTypePrettyError' (xs :: [[k]]) :: Bool where
  RecTypePrettyError' (_ ': '[]) = 'True
  RecTypePrettyError' (_ ': _) =
    TypeError
      ('Text "Deriving record encoding only works with types with single constructor. More than one constructor is found.")

--------------------------------------------------------------------------------

pands :: [Term s PBool] -> Term s PBool
pands :: forall (s :: S). [Term s PBool] -> Term s PBool
pands [] = AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
pands [Item [Term s PBool]
x'] = Item [Term s PBool]
Term s PBool
x'
pands (Term s PBool
x' : [Term s PBool]
xs') = Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
x' ([Term s PBool] -> Term s PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands [Term s PBool]
xs') (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False)

--------------------------------------------------------------------------------

type family RecAsHaskell (x :: [S -> Type]) where
  RecAsHaskell (x ': xs) = AsHaskell x ': RecAsHaskell xs
  RecAsHaskell '[] = '[]

type family StructAsHaskell (x :: [[S -> Type]]) where
  StructAsHaskell (x ': xs) = RecAsHaskell x ': StructAsHaskell xs
  StructAsHaskell '[] = '[]