{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
module PlutusIR.Analysis.Builtins
( BuiltinMatcherLike (..)
, bmlSplitMatchContext
, bmlBranchArities
, defaultUniMatcherLike
, BuiltinsInfo (..)
, biSemanticsVariant
, biMatcherLike
, biUnserializableConstants
, builtinArityInfo
, constantIsSerializable
, termIsSerializable
, asBuiltinDatatypeMatch
, builtinDatatypeMatchBranchArities
, defaultUniUnserializableConstants
) where
import Control.Lens hiding (parts)
import Data.Functor (void)
import Data.Kind
import Data.Map qualified as Map
import Data.Proxy
import PlutusCore.Arity
import PlutusCore.Builtin
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Default
import PlutusCore.MkPlc (mkIterTyAppNoAnn)
import PlutusIR.Contexts
import PlutusIR.Core (Term)
import PlutusIR.Core.Plated (_Constant, termSubtermsDeep)
import PlutusPrelude (Default (..))
data BuiltinMatcherLike uni fun = BuiltinMatcherLike
{ forall (uni :: * -> *) fun.
BuiltinMatcherLike uni fun
-> forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a))
_bmlSplitMatchContext :: forall tyname name a .
Prism' (AppContext tyname name uni fun a) (SplitMatchContext tyname name uni fun a)
, forall (uni :: * -> *) fun. BuiltinMatcherLike uni fun -> [Arity]
_bmlBranchArities :: [Arity]
}
makeLenses ''BuiltinMatcherLike
data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo
{ forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> BuiltinSemanticsVariant fun
_biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun
, forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> Map fun (BuiltinMatcherLike uni fun)
_biMatcherLike :: Map.Map fun (BuiltinMatcherLike uni fun)
, forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
_biUnserializableConstants :: Some (ValueOf uni) -> Bool
}
makeLenses ''BuiltinsInfo
instance Default (BuiltinsInfo DefaultUni DefaultFun) where
def :: BuiltinsInfo DefaultUni DefaultFun
def = BuiltinsInfo
{ _biSemanticsVariant :: BuiltinSemanticsVariant DefaultFun
_biSemanticsVariant = BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def
, _biMatcherLike :: Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
_biMatcherLike = Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
defaultUniMatcherLike
, _biUnserializableConstants :: Some (ValueOf DefaultUni) -> Bool
_biUnserializableConstants = Some (ValueOf DefaultUni) -> Bool
defaultUniUnserializableConstants
}
builtinArityInfo
:: forall uni fun
. ToBuiltinMeaning uni fun
=> BuiltinsInfo uni fun
-> fun
-> Arity
builtinArityInfo :: forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
BuiltinsInfo uni fun -> fun -> Arity
builtinArityInfo BuiltinsInfo uni fun
binfo = Proxy uni -> BuiltinSemanticsVariant fun -> fun -> Arity
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> Arity
builtinArity (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @uni) (BuiltinsInfo uni fun
binfo BuiltinsInfo uni fun
-> Getting
(BuiltinSemanticsVariant fun)
(BuiltinsInfo uni fun)
(BuiltinSemanticsVariant fun)
-> BuiltinSemanticsVariant fun
forall s a. s -> Getting a s a -> a
^. Getting
(BuiltinSemanticsVariant fun)
(BuiltinsInfo uni fun)
(BuiltinSemanticsVariant fun)
forall (uni :: * -> *) fun (f :: * -> *).
Functor f =>
(BuiltinSemanticsVariant fun -> f (BuiltinSemanticsVariant fun))
-> BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun)
biSemanticsVariant)
constantIsSerializable
:: forall uni fun
. BuiltinsInfo uni fun
-> Some (ValueOf uni)
-> Bool
constantIsSerializable :: forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
constantIsSerializable BuiltinsInfo uni fun
bi Some (ValueOf uni)
v = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
_biUnserializableConstants BuiltinsInfo uni fun
bi Some (ValueOf uni)
v
termIsSerializable :: BuiltinsInfo uni fun -> Term tyname name uni fun a -> Bool
termIsSerializable :: forall (uni :: * -> *) fun tyname name a.
BuiltinsInfo uni fun -> Term tyname name uni fun a -> Bool
termIsSerializable BuiltinsInfo uni fun
binfo =
Getting All (Term tyname name uni fun a) (a, Some (ValueOf uni))
-> ((a, Some (ValueOf uni)) -> Bool)
-> Term tyname name uni fun a
-> Bool
forall s a. Getting All s a -> (a -> Bool) -> s -> Bool
allOf
((Term tyname name uni fun a
-> Const All (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> Const All (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtermsDeep ((Term tyname name uni fun a
-> Const All (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> Const All (Term tyname name uni fun a))
-> Getting All (Term tyname name uni fun a) (a, Some (ValueOf uni))
-> Getting All (Term tyname name uni fun a) (a, Some (ValueOf uni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting All (Term tyname name uni fun a) (a, Some (ValueOf uni))
forall tyname name (uni :: * -> *) fun a (p :: * -> * -> *)
(f :: * -> *).
(Choice p, Applicative f) =>
p (a, Some (ValueOf uni)) (f (a, Some (ValueOf uni)))
-> p (Term tyname name uni fun a) (f (Term tyname name uni fun a))
_Constant)
(BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
forall (uni :: * -> *) fun.
BuiltinsInfo uni fun -> Some (ValueOf uni) -> Bool
constantIsSerializable BuiltinsInfo uni fun
binfo (Some (ValueOf uni) -> Bool)
-> ((a, Some (ValueOf uni)) -> Some (ValueOf uni))
-> (a, Some (ValueOf uni))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Some (ValueOf uni)) -> Some (ValueOf uni)
forall a b. (a, b) -> b
snd)
asBuiltinDatatypeMatch ::
Ord fun
=> BuiltinsInfo uni fun
-> fun
-> Maybe (APrism' (AppContext tyname name uni fun a) (SplitMatchContext tyname name uni fun a))
asBuiltinDatatypeMatch :: forall fun (uni :: * -> *) tyname name a.
Ord fun =>
BuiltinsInfo uni fun
-> fun
-> Maybe
(APrism'
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a))
asBuiltinDatatypeMatch BuiltinsInfo uni fun
binfo fun
f
| Just (BuiltinMatcherLike forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a))
p [Arity]
_) <- fun
-> Map fun (BuiltinMatcherLike uni fun)
-> Maybe (BuiltinMatcherLike uni fun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup fun
f (BuiltinsInfo uni fun
binfo BuiltinsInfo uni fun
-> Getting
(Map fun (BuiltinMatcherLike uni fun))
(BuiltinsInfo uni fun)
(Map fun (BuiltinMatcherLike uni fun))
-> Map fun (BuiltinMatcherLike uni fun)
forall s a. s -> Getting a s a -> a
^. Getting
(Map fun (BuiltinMatcherLike uni fun))
(BuiltinsInfo uni fun)
(Map fun (BuiltinMatcherLike uni fun))
forall (uni :: * -> *) fun (f :: * -> *).
Functor f =>
(Map fun (BuiltinMatcherLike uni fun)
-> f (Map fun (BuiltinMatcherLike uni fun)))
-> BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun)
biMatcherLike)
= APrism'
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
-> Maybe
(APrism'
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a))
forall a. a -> Maybe a
Just APrism'
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a)
forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a))
p
| Bool
otherwise = Maybe
(APrism'
(AppContext tyname name uni fun a)
(SplitMatchContext tyname name uni fun a))
forall a. Maybe a
Nothing
builtinDatatypeMatchBranchArities ::
Ord fun
=> BuiltinsInfo uni fun
-> fun
-> Maybe [Arity]
builtinDatatypeMatchBranchArities :: forall fun (uni :: * -> *).
Ord fun =>
BuiltinsInfo uni fun -> fun -> Maybe [Arity]
builtinDatatypeMatchBranchArities BuiltinsInfo uni fun
binfo fun
f
| Just (BuiltinMatcherLike forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a))
_ [Arity]
arities) <- fun
-> Map fun (BuiltinMatcherLike uni fun)
-> Maybe (BuiltinMatcherLike uni fun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup fun
f (BuiltinsInfo uni fun
binfo BuiltinsInfo uni fun
-> Getting
(Map fun (BuiltinMatcherLike uni fun))
(BuiltinsInfo uni fun)
(Map fun (BuiltinMatcherLike uni fun))
-> Map fun (BuiltinMatcherLike uni fun)
forall s a. s -> Getting a s a -> a
^. Getting
(Map fun (BuiltinMatcherLike uni fun))
(BuiltinsInfo uni fun)
(Map fun (BuiltinMatcherLike uni fun))
forall (uni :: * -> *) fun (f :: * -> *).
Functor f =>
(Map fun (BuiltinMatcherLike uni fun)
-> f (Map fun (BuiltinMatcherLike uni fun)))
-> BuiltinsInfo uni fun -> f (BuiltinsInfo uni fun)
biMatcherLike)
= [Arity] -> Maybe [Arity]
forall a. a -> Maybe a
Just [Arity]
arities
| Bool
otherwise = Maybe [Arity]
forall a. Maybe a
Nothing
defaultUniMatcherLike :: Map.Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
defaultUniMatcherLike :: Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
defaultUniMatcherLike = [(DefaultFun, BuiltinMatcherLike DefaultUni DefaultFun)]
-> Map DefaultFun (BuiltinMatcherLike DefaultUni DefaultFun)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ (DefaultFun
IfThenElse,
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name DefaultUni DefaultFun a)
(f (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> p (AppContext tyname name DefaultUni DefaultFun a)
(f (AppContext tyname name DefaultUni DefaultFun a)))
-> [Arity] -> BuiltinMatcherLike DefaultUni DefaultFun
forall (uni :: * -> *) fun.
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a)))
-> [Arity] -> BuiltinMatcherLike uni fun
BuiltinMatcherLike ((SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a)
-> (AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> Prism
(AppContext tyname name DefaultUni DefaultFun a)
(AppContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
SplitMatchContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
reconstructIfThenElse AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitIfThenElse) [Arity]
forall {a}. [[a]]
ifThenElseBranchArities)
, (DefaultFun
ChooseUnit,
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name DefaultUni DefaultFun a)
(f (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> p (AppContext tyname name DefaultUni DefaultFun a)
(f (AppContext tyname name DefaultUni DefaultFun a)))
-> [Arity] -> BuiltinMatcherLike DefaultUni DefaultFun
forall (uni :: * -> *) fun.
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a)))
-> [Arity] -> BuiltinMatcherLike uni fun
BuiltinMatcherLike ((SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a)
-> (AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> Prism
(AppContext tyname name DefaultUni DefaultFun a)
(AppContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
SplitMatchContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
reconstructChooseUnit AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseUnit) [Arity]
forall {a}. [[a]]
chooseUnitBranchArities)
, (DefaultFun
ChooseList,
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name DefaultUni DefaultFun a)
(f (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> p (AppContext tyname name DefaultUni DefaultFun a)
(f (AppContext tyname name DefaultUni DefaultFun a)))
-> [Arity] -> BuiltinMatcherLike DefaultUni DefaultFun
forall (uni :: * -> *) fun.
(forall tyname name a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (SplitMatchContext tyname name uni fun a)
(f (SplitMatchContext tyname name uni fun a))
-> p (AppContext tyname name uni fun a)
(f (AppContext tyname name uni fun a)))
-> [Arity] -> BuiltinMatcherLike uni fun
BuiltinMatcherLike ((SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a)
-> (AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a))
-> Prism
(AppContext tyname name DefaultUni DefaultFun a)
(AppContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
(SplitMatchContext tyname name DefaultUni DefaultFun a)
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' SplitMatchContext tyname name DefaultUni DefaultFun a
-> AppContext tyname name DefaultUni DefaultFun a
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
SplitMatchContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
reconstructChooseList AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseList) [Arity]
forall {a}. [[a]]
chooseListBranchArities)
]
where
splitIfThenElse
:: AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitIfThenElse :: forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitIfThenElse AppContext tyname name DefaultUni DefaultFun a
args
| Just Saturation
Saturated <- AppContext tyname name DefaultUni DefaultFun a
-> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name DefaultUni DefaultFun a
args (Proxy DefaultUni
-> BuiltinSemanticsVariant DefaultFun -> DefaultFun -> Arity
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> Arity
builtinArity Proxy DefaultUni
forall {k} (t :: k). Proxy t
Proxy BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def DefaultFun
IfThenElse)
, (TypeAppContext Type tyname DefaultUni a
resTy a
resTyAnn (TermAppContext Term tyname name DefaultUni DefaultFun a
scrut a
scrutAnn AppContext tyname name DefaultUni DefaultFun a
branches)) <- AppContext tyname name DefaultUni DefaultFun a
args
=
let
scrutTy :: Type tyname DefaultUni ()
scrutTy = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Bool ()
sm :: SplitMatchContext tyname name DefaultUni DefaultFun a
sm = AppContext tyname name DefaultUni DefaultFun a
-> (Term tyname name DefaultUni DefaultFun a,
Type tyname DefaultUni (), a)
-> (Type tyname DefaultUni a, a)
-> AppContext tyname name DefaultUni DefaultFun a
-> SplitMatchContext tyname name DefaultUni DefaultFun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname name uni fun a
-> SplitMatchContext tyname name uni fun a
SplitMatchContext AppContext tyname name DefaultUni DefaultFun a
forall a. Monoid a => a
mempty (Term tyname name DefaultUni DefaultFun a
scrut, Type tyname DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
scrutTy, a
scrutAnn) (Type tyname DefaultUni a
resTy, a
resTyAnn) AppContext tyname name DefaultUni DefaultFun a
branches
in SplitMatchContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. a -> Maybe a
Just SplitMatchContext tyname name DefaultUni DefaultFun a
sm
| Bool
otherwise = Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. Maybe a
Nothing
reconstructIfThenElse :: SplitMatchContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
reconstructIfThenElse (SplitMatchContext AppContext tyname name uni fun ann
_ (Term tyname name uni fun ann
scrut, Type tyname uni ()
_, ann
scrutAnn) (Type tyname uni ann
resTy, ann
resTyAnn) AppContext tyname name uni fun ann
branches) =
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni ann
resTy ann
resTyAnn (Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext Term tyname name uni fun ann
scrut ann
scrutAnn AppContext tyname name uni fun ann
branches)
ifThenElseBranchArities :: [[a]]
ifThenElseBranchArities = [[], []]
splitChooseUnit
:: AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseUnit :: forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseUnit AppContext tyname name DefaultUni DefaultFun a
args
| Just Saturation
Saturated <- AppContext tyname name DefaultUni DefaultFun a
-> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name DefaultUni DefaultFun a
args (Proxy DefaultUni
-> BuiltinSemanticsVariant DefaultFun -> DefaultFun -> Arity
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> Arity
builtinArity Proxy DefaultUni
forall {k} (t :: k). Proxy t
Proxy BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def DefaultFun
ChooseUnit)
, (TypeAppContext Type tyname DefaultUni a
resTy a
resTyAnn (TermAppContext Term tyname name DefaultUni DefaultFun a
scrut a
scrutAnn AppContext tyname name DefaultUni DefaultFun a
branches)) <- AppContext tyname name DefaultUni DefaultFun a
args
=
let
scrutTy :: Type tyname DefaultUni ()
scrutTy = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()
sm :: SplitMatchContext tyname name DefaultUni DefaultFun a
sm = AppContext tyname name DefaultUni DefaultFun a
-> (Term tyname name DefaultUni DefaultFun a,
Type tyname DefaultUni (), a)
-> (Type tyname DefaultUni a, a)
-> AppContext tyname name DefaultUni DefaultFun a
-> SplitMatchContext tyname name DefaultUni DefaultFun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname name uni fun a
-> SplitMatchContext tyname name uni fun a
SplitMatchContext AppContext tyname name DefaultUni DefaultFun a
forall a. Monoid a => a
mempty (Term tyname name DefaultUni DefaultFun a
scrut, Type tyname DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
scrutTy, a
scrutAnn) (Type tyname DefaultUni a
resTy, a
resTyAnn) AppContext tyname name DefaultUni DefaultFun a
branches
in SplitMatchContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. a -> Maybe a
Just SplitMatchContext tyname name DefaultUni DefaultFun a
sm
| Bool
otherwise = Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. Maybe a
Nothing
reconstructChooseUnit :: SplitMatchContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
reconstructChooseUnit (SplitMatchContext AppContext tyname name uni fun ann
_ (Term tyname name uni fun ann
scrut, Type tyname uni ()
_, ann
scrutAnn) (Type tyname uni ann
resTy, ann
resTyAnn) AppContext tyname name uni fun ann
branches) =
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni ann
resTy ann
resTyAnn (Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext Term tyname name uni fun ann
scrut ann
scrutAnn AppContext tyname name uni fun ann
branches)
chooseUnitBranchArities :: [[a]]
chooseUnitBranchArities = [[]]
splitChooseList
:: AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseList :: forall tyname name a.
AppContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
splitChooseList AppContext tyname name DefaultUni DefaultFun a
args
| Just Saturation
Saturated <- AppContext tyname name DefaultUni DefaultFun a
-> Arity -> Maybe Saturation
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Arity -> Maybe Saturation
saturates AppContext tyname name DefaultUni DefaultFun a
args (Proxy DefaultUni
-> BuiltinSemanticsVariant DefaultFun -> DefaultFun -> Arity
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> Arity
builtinArity Proxy DefaultUni
forall {k} (t :: k). Proxy t
Proxy BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def DefaultFun
ChooseList)
, (AppContext tyname name DefaultUni DefaultFun a
vars, TypeAppContext Type tyname DefaultUni a
resTy a
resTyAnn (TermAppContext Term tyname name DefaultUni DefaultFun a
scrut a
scrutAnn AppContext tyname name DefaultUni DefaultFun a
branches)) <-
Int
-> AppContext tyname name DefaultUni DefaultFun a
-> (AppContext tyname name DefaultUni DefaultFun a,
AppContext tyname name DefaultUni DefaultFun a)
forall tyname name (uni :: * -> *) fun a.
Int
-> AppContext tyname name uni fun a
-> (AppContext tyname name uni fun a,
AppContext tyname name uni fun a)
splitAppContext Int
1 AppContext tyname name DefaultUni DefaultFun a
args
= do
[Type tyname DefaultUni a]
tyArgs <- AppContext tyname name DefaultUni DefaultFun a
-> Maybe [Type tyname DefaultUni a]
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a -> Maybe [Type tyname uni a]
extractTyArgs AppContext tyname name DefaultUni DefaultFun a
vars
let scrutTy :: Type tyname DefaultUni ()
scrutTy = Type tyname DefaultUni ()
-> [Type tyname DefaultUni ()] -> Type tyname DefaultUni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @[] ()) ((Type tyname DefaultUni a -> Type tyname DefaultUni ())
-> [Type tyname DefaultUni a] -> [Type tyname DefaultUni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type tyname DefaultUni a -> Type tyname DefaultUni ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Type tyname DefaultUni a]
tyArgs)
sm :: SplitMatchContext tyname name DefaultUni DefaultFun a
sm = AppContext tyname name DefaultUni DefaultFun a
-> (Term tyname name DefaultUni DefaultFun a,
Type tyname DefaultUni (), a)
-> (Type tyname DefaultUni a, a)
-> AppContext tyname name DefaultUni DefaultFun a
-> SplitMatchContext tyname name DefaultUni DefaultFun a
forall tyname name (uni :: * -> *) fun a.
AppContext tyname name uni fun a
-> (Term tyname name uni fun a, Type tyname uni (), a)
-> (Type tyname uni a, a)
-> AppContext tyname name uni fun a
-> SplitMatchContext tyname name uni fun a
SplitMatchContext AppContext tyname name DefaultUni DefaultFun a
vars (Term tyname name DefaultUni DefaultFun a
scrut, Type tyname DefaultUni ()
scrutTy, a
scrutAnn) (Type tyname DefaultUni a
resTy, a
resTyAnn) AppContext tyname name DefaultUni DefaultFun a
branches
SplitMatchContext tyname name DefaultUni DefaultFun a
-> Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SplitMatchContext tyname name DefaultUni DefaultFun a
sm
| Bool
otherwise = Maybe (SplitMatchContext tyname name DefaultUni DefaultFun a)
forall a. Maybe a
Nothing
reconstructChooseList :: SplitMatchContext tyname name uni fun a
-> AppContext tyname name uni fun a
reconstructChooseList (SplitMatchContext AppContext tyname name uni fun a
vars (Term tyname name uni fun a
scrut, Type tyname uni ()
_, a
scrutAnn) (Type tyname uni a
resTy, a
resTyAnn) AppContext tyname name uni fun a
branches) =
AppContext tyname name uni fun a
vars AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall a. Semigroup a => a -> a -> a
<> Type tyname uni a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Type tyname uni ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TypeAppContext Type tyname uni a
resTy a
resTyAnn (Term tyname name uni fun a
-> a
-> AppContext tyname name uni fun a
-> AppContext tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> ann
-> AppContext tyname name uni fun ann
-> AppContext tyname name uni fun ann
TermAppContext Term tyname name uni fun a
scrut a
scrutAnn AppContext tyname name uni fun a
branches)
chooseListBranchArities :: [[a]]
chooseListBranchArities = [[], []]
defaultUniUnserializableConstants :: Some (ValueOf DefaultUni) -> Bool
defaultUniUnserializableConstants :: Some (ValueOf DefaultUni) -> Bool
defaultUniUnserializableConstants = \case
Some (ValueOf DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element a
_) -> Bool
True
Some (ValueOf DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element a
_) -> Bool
True
Some (ValueOf DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult a
_) -> Bool
True
Some (ValueOf DefaultUni)
_ -> Bool
False