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

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

import Data.Kind (Type)
import Data.List (groupBy, sortBy)
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 (pconstant)
import Plutarch.Internal.Term (Dig, S, Term, plet)
import Plutarch.Internal.TermCont (hashOpenTerm, unTermCont)

-- | @since WIP
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 WIP
  }

-- | @since WIP
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 WIP
  }

-- | @since WIP
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 WIP
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 WIP
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 WIP
-}
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, Dig))]
handlersWithHash :: [(Integer, (Term s b, Dig))] <-
    ((Integer, Term s r) -> TermCont @r s (Integer, (Term s r, Dig)))
-> [(Integer, Term s r)]
-> TermCont @r s [(Integer, (Term s r, Dig))]
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) -> (\Dig
hash -> (Integer
i, (Term s r
t, Dig
hash))) (Dig -> (Integer, (Term s r, Dig)))
-> TermCont @r s Dig -> TermCont @r s (Integer, (Term s r, Dig))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s r -> TermCont @r s Dig
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s Dig
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)
g1 ([Integer], Term s r)
g2 -> [Integer] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length (([Integer], Term s r) -> [Integer]
forall a b. (a, b) -> a
fst ([Integer], Term s r)
g1) Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [Integer] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length (([Integer], Term s r) -> [Integer]
forall a b. (a, b) -> a
fst ([Integer], Term s r)
g2)) ([([Integer], Term s r)] -> [([Integer], Term s r)])
-> [([Integer], Term s r)] -> [([Integer], Term s r)]
forall a b. (a -> b) -> a -> b
$
        (\[(Integer, (Term s r, Dig))]
g -> ((Integer, (Term s r, Dig)) -> Integer
forall a b. (a, b) -> a
fst ((Integer, (Term s r, Dig)) -> Integer)
-> [(Integer, (Term s r, Dig))] -> [Integer]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Integer, (Term s r, Dig))]
g, (Term s r, Dig) -> Term s r
forall a b. (a, b) -> a
fst ((Term s r, Dig) -> Term s r) -> (Term s r, Dig) -> Term s r
forall a b. (a -> b) -> a -> b
$ (Integer, (Term s r, Dig)) -> (Term s r, Dig)
forall a b. (a, b) -> b
snd ((Integer, (Term s r, Dig)) -> (Term s r, Dig))
-> (Integer, (Term s r, Dig)) -> (Term s r, Dig)
forall a b. (a -> b) -> a -> b
$ [(Integer, (Term s r, Dig))] -> (Integer, (Term s r, Dig))
forall a. HasCallStack => [a] -> a
head [(Integer, (Term s r, Dig))]
g))
          ([(Integer, (Term s r, Dig))] -> ([Integer], Term s r))
-> [[(Integer, (Term s r, Dig))]] -> [([Integer], Term s r)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Integer, (Term s r, Dig)) -> (Integer, (Term s r, Dig)) -> Bool)
-> [(Integer, (Term s r, Dig))] -> [[(Integer, (Term s r, Dig))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy
            (\(Integer, (Term s r, Dig))
x1 (Integer, (Term s r, Dig))
x2 -> (Term s r, Dig) -> Dig
forall a b. (a, b) -> b
snd ((Integer, (Term s r, Dig)) -> (Term s r, Dig)
forall a b. (a, b) -> b
snd (Integer, (Term s r, Dig))
x1) Dig -> Dig -> Bool
forall a. Eq a => a -> a -> Bool
== (Term s r, Dig) -> Dig
forall a b. (a, b) -> b
snd ((Integer, (Term s r, Dig)) -> (Term s r, Dig)
forall a b. (a, b) -> b
snd (Integer, (Term s r, Dig))
x2))
            (((Integer, (Term s r, Dig))
 -> (Integer, (Term s r, Dig)) -> Ordering)
-> [(Integer, (Term s r, Dig))] -> [(Integer, (Term s r, Dig))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(Integer
_, (Term s r
_, Dig
h1)) (Integer
_, (Term s r
_, Dig
h2)) -> Dig
h1 Dig -> Dig -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Dig
h2) [(Integer, (Term s r, Dig))]
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 WIP
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 a struct

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 WIP
type family UnTermRec (struct :: [Type]) :: [S -> Type] where
  UnTermRec '[] = '[]
  UnTermRec (Term _ a ': rest) = a ': UnTermRec rest

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

-- | @since WIP
type RecTypePrettyError struct = 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 {k} (xs :: [k]) (r :: [k] -> Type).
SListI @k xs =>
r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    SListI @k ys =>
    r ys -> r ((':) @k 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)