{-# 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)
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
}
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
}
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')
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
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
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
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"
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"
_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
[([Integer], Term s r)] -> Term s r
pgo [([Integer], Term s r)]
groupedHandlers
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
type family UnTermRec (struct :: [Type]) :: [S -> Type] where
UnTermRec '[] = '[]
UnTermRec (Term _ a ': rest) = a ': UnTermRec rest
type UnTermStruct x = UnTermStruct' (Code x)
type RecTypePrettyError struct = RecTypePrettyError' struct ~ 'True
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)