{-# 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 (..))

-- | The information we need to work with a builtin that is like a datatype matcher.
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

-- | All non-static information about builtins that the compiler might want.
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)
  -- See Note [Unserializable constants]
  , 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
        }

-- | Get the arity of a builtin function from the 'PLC.BuiltinInfo'.
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)

-- | Split a builtin 'match'.
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

-- | Get the branch arities for a builtin 'match'.
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
      -- Okay to use the default semantics variant here as we're assuming the
      -- type never changes
      | 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)
      -- 1. No ty vars
      -- 2. Result type comes first
      -- 3. Scrutinee next
      -- 4. Then branches
      , (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)
    -- both branches have no args
    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
      -- Okay to use the default semantics variant here as we're assuming the
      -- type never changes
      | 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)
      -- 1. No ty vars
      -- 2. Result type comes first
      -- 3. Scrutinee next
      -- 4. Then branches
      , (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)
    -- only branch has no args
    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
      -- Okay to use the default semantics variant here as we're assuming the
      -- type never changes
      | 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)
      -- 1. One type variable
      -- 2. Then the result type
      -- 3. Scrutinee next
      -- 4. Then branches
      , (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)
    -- both branches have no args
    chooseListBranchArities :: [[a]]
chooseListBranchArities = [[], []]

-- See Note [Unserializable constants]
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

{- Note [Unserializable constants]
Generally we require that programs are (de-)serializable, which requires that all constants
in the program are (de-)serializable. This is enforced by the type system, we have to
have instances for all builtin types in the universe.

However, in practice we have to limit this somewhat. In particular, some builtin types
have no _cheap_ (de-)serialization method. This notably applies to the BLS constants, where
both BLS "deserialization" and "uncompression" do some sanity checks that take a non-trivial
amount of time.

This is a problem: in our time budgeting for validating transactions we generally assume
that deserialization is proportional to input size with low constant factors. But for a
malicious program made up of only BLS points, this would not be true!

So pragmatically we disallow (de-)serialization of constants of such types (the instances
still exist, but they will fail at runtime). The problem then is that we need to make
sure that we don't accidentally create any such constants. It's one thing if the _user_
does it - then we can just tell them not to (there are usually workarounds). But the
compiler should also not do it! Notably, the EvaluateBuiltins pass can produce _new_
constants.

To deal with this problem we pass around a predicate that tells us which constants are
bad, so we can just refuse to perform a transformation if it would produce unrepresentable
constants.

An alternative approach would be to instead add a pass to rewrite the problematic
constants into a non-problematic form (e.g. conversion from a bytestring instead of a constant).
This would be better for optimization, since we wouldn't be blocking EvaluateBuiltins
from working, even if it was good, but it has two problems:
1. It would fight with EvaluateBuiltins, which each undoing the other.
2. It can't work generically, since we don't always have a way to do the transformation. In
particular, there isn't a way to do this for the ML-result BLS type.
-}