-- editorconfig-checker-disable-file
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

module UntypedPlutusCore.Core.Type
    ( TPLC.UniOf
    , TPLC.Version (..)
    , TPLC.Binder (..)
    , Term (..)
    , Program (..)
    , progAnn
    , progVer
    , progTerm
    , bindFunM
    , bindFun
    , mapFun
    , termAnn
    , UVarDecl(..)
    , uvarDeclName
    , uvarDeclAnn
    ) where

import Control.Lens
import PlutusPrelude

import Data.Vector
import Data.Word
import PlutusCore.Builtin qualified as TPLC
import PlutusCore.Core qualified as TPLC
import PlutusCore.MkPlc
import PlutusCore.Name.Unique qualified as TPLC
import Universe

{- Note [Term constructor ordering and numbers]
Ordering of constructors has a small but real effect on efficiency.
It's slightly more efficient to hit the earlier constructors, so it's better to put the more
common ones first.

The current ordering is based on their *empirically observed* frequency. We should check this
occasionally.

Additionally, the first 7 (or 3 on 32-bit systems) constructors will get *pointer tags*, which allows
more efficient access when casing on them. So we ideally want to keep the number of constructors
at 7 or fewer.

We've got 8 constructors, *but* the last one is Error, which is only going to be seen at most
once per program, so it's not too big a deal if it doesn't get a tag.

See the GHC Notes "Tagging big families" and "Double switching for big families" in
GHC.StgToCmm.Expr for more details.
-}

{-| The type of Untyped Plutus Core terms. Mirrors the type of Typed Plutus Core terms except

1. all types are removed
2. 'IWrap' and 'Unwrap' are removed
3. type abstractions are replaced with 'Delay'
4. type instantiations are replaced with 'Force'

The latter two are due to the fact that we don't have value restriction in Typed Plutus Core
and hence a computation can be stuck expecting only a single type argument for the computation
to become unstuck. Therefore we can't just silently remove type abstractions and instantiations and
need to replace them with something else that also blocks evaluation (in order for the semantics
of an erased program to match with the semantics of the original typed one). 'Delay' and 'Force'
serve exactly this purpose.
-}
-- Making all the fields strict gives us a couple of percent in benchmarks
-- See Note [Term constructor ordering and numbers]
data Term name uni fun ann
    = Var !ann !name
    | LamAbs !ann !name !(Term name uni fun ann)
    | Apply !ann !(Term name uni fun ann) !(Term name uni fun ann)
    | Force !ann !(Term name uni fun ann)
    | Delay !ann !(Term name uni fun ann)
    | Constant !ann !(Some (ValueOf uni))
    | Builtin !ann !fun
    -- This is the cutoff at which constructors won't get pointer tags
    -- See Note [Term constructor ordering and numbers]
    | Error !ann
    -- TODO: worry about overflow, maybe use an Integer
    -- TODO: try spine-strict list or strict list or vector
    -- See Note [Constr tag type]
    | Constr !ann !Word64 ![Term name uni fun ann]
    | Case !ann !(Term name uni fun ann) !(Vector (Term name uni fun ann))
    deriving stock ((forall a b.
 (a -> b) -> Term name uni fun a -> Term name uni fun b)
-> (forall a b. a -> Term name uni fun b -> Term name uni fun a)
-> Functor (Term name uni fun)
forall a b. a -> Term name uni fun b -> Term name uni fun a
forall a b. (a -> b) -> Term name uni fun a -> Term name uni fun b
forall name (uni :: * -> *) fun a b.
a -> Term name uni fun b -> Term name uni fun a
forall name (uni :: * -> *) fun a b.
(a -> b) -> Term name uni fun a -> Term name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall name (uni :: * -> *) fun a b.
(a -> b) -> Term name uni fun a -> Term name uni fun b
fmap :: forall a b. (a -> b) -> Term name uni fun a -> Term name uni fun b
$c<$ :: forall name (uni :: * -> *) fun a b.
a -> Term name uni fun b -> Term name uni fun a
<$ :: forall a b. a -> Term name uni fun b -> Term name uni fun a
Functor, (forall x. Term name uni fun ann -> Rep (Term name uni fun ann) x)
-> (forall x.
    Rep (Term name uni fun ann) x -> Term name uni fun ann)
-> Generic (Term name uni fun ann)
forall x. Rep (Term name uni fun ann) x -> Term name uni fun ann
forall x. Term name uni fun ann -> Rep (Term name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name (uni :: * -> *) fun ann x.
Rep (Term name uni fun ann) x -> Term name uni fun ann
forall name (uni :: * -> *) fun ann x.
Term name uni fun ann -> Rep (Term name uni fun ann) x
$cfrom :: forall name (uni :: * -> *) fun ann x.
Term name uni fun ann -> Rep (Term name uni fun ann) x
from :: forall x. Term name uni fun ann -> Rep (Term name uni fun ann) x
$cto :: forall name (uni :: * -> *) fun ann x.
Rep (Term name uni fun ann) x -> Term name uni fun ann
to :: forall x. Rep (Term name uni fun ann) x -> Term name uni fun ann
Generic)

deriving stock instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (Term name uni fun ann)

deriving anyclass instance (NFData name, NFData fun, NFData ann, Everywhere uni NFData, Closed uni)
    => NFData (Term name uni fun ann)

-- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language.
data Program name uni fun ann = Program
    { forall name (uni :: * -> *) fun ann.
Program name uni fun ann -> ann
_progAnn  :: ann
    , forall name (uni :: * -> *) fun ann.
Program name uni fun ann -> Version
_progVer  :: TPLC.Version
    , forall name (uni :: * -> *) fun ann.
Program name uni fun ann -> Term name uni fun ann
_progTerm :: Term name uni fun ann
    }
    deriving stock ((forall a b.
 (a -> b) -> Program name uni fun a -> Program name uni fun b)
-> (forall a b.
    a -> Program name uni fun b -> Program name uni fun a)
-> Functor (Program name uni fun)
forall a b. a -> Program name uni fun b -> Program name uni fun a
forall a b.
(a -> b) -> Program name uni fun a -> Program name uni fun b
forall name (uni :: * -> *) fun a b.
a -> Program name uni fun b -> Program name uni fun a
forall name (uni :: * -> *) fun a b.
(a -> b) -> Program name uni fun a -> Program name uni fun b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall name (uni :: * -> *) fun a b.
(a -> b) -> Program name uni fun a -> Program name uni fun b
fmap :: forall a b.
(a -> b) -> Program name uni fun a -> Program name uni fun b
$c<$ :: forall name (uni :: * -> *) fun a b.
a -> Program name uni fun b -> Program name uni fun a
<$ :: forall a b. a -> Program name uni fun b -> Program name uni fun a
Functor, (forall x.
 Program name uni fun ann -> Rep (Program name uni fun ann) x)
-> (forall x.
    Rep (Program name uni fun ann) x -> Program name uni fun ann)
-> Generic (Program name uni fun ann)
forall x.
Rep (Program name uni fun ann) x -> Program name uni fun ann
forall x.
Program name uni fun ann -> Rep (Program name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name (uni :: * -> *) fun ann x.
Rep (Program name uni fun ann) x -> Program name uni fun ann
forall name (uni :: * -> *) fun ann x.
Program name uni fun ann -> Rep (Program name uni fun ann) x
$cfrom :: forall name (uni :: * -> *) fun ann x.
Program name uni fun ann -> Rep (Program name uni fun ann) x
from :: forall x.
Program name uni fun ann -> Rep (Program name uni fun ann) x
$cto :: forall name (uni :: * -> *) fun ann x.
Rep (Program name uni fun ann) x -> Program name uni fun ann
to :: forall x.
Rep (Program name uni fun ann) x -> Program name uni fun ann
Generic)
makeLenses ''Program

deriving stock instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
    => Show (Program name uni fun ann)

deriving anyclass instance (NFData name, Everywhere uni NFData, NFData fun, NFData ann, Closed uni)
    => NFData (Program name uni fun ann)

type instance TPLC.UniOf (Term name uni fun ann) = uni

instance TermLike (Term name uni fun) TPLC.TyName name uni fun where
    var :: forall ann. ann -> name -> Term name uni fun ann
var      = ann -> name -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var
    tyAbs :: forall ann.
ann
-> TyName
-> Kind ann
-> Term name uni fun ann
-> Term name uni fun ann
tyAbs    = \ann
ann TyName
_ Kind ann
_ -> ann -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ann
ann
    lamAbs :: forall ann.
ann
-> name
-> Type TyName uni ann
-> Term name uni fun ann
-> Term name uni fun ann
lamAbs   = \ann
ann name
name Type TyName uni ann
_ -> ann -> name -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ann
ann name
name
    apply :: forall ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
apply    = ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
    constant :: forall ann. ann -> Some (ValueOf uni) -> Term name uni fun ann
constant = ann -> Some (ValueOf uni) -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant
    builtin :: forall ann. ann -> fun -> Term name uni fun ann
builtin  = ann -> fun -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin
    tyInst :: forall ann.
ann
-> Term name uni fun ann
-> Type TyName uni ann
-> Term name uni fun ann
tyInst   = \ann
ann Term name uni fun ann
term Type TyName uni ann
_ -> ann -> Term name uni fun ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ann
ann Term name uni fun ann
term
    unwrap :: forall ann. ann -> Term name uni fun ann -> Term name uni fun ann
unwrap   = (Term name uni fun ann -> Term name uni fun ann)
-> ann -> Term name uni fun ann -> Term name uni fun ann
forall a b. a -> b -> a
const Term name uni fun ann -> Term name uni fun ann
forall a. a -> a
id
    iWrap :: forall ann.
ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Term name uni fun ann
-> Term name uni fun ann
iWrap    = \ann
_ Type TyName uni ann
_ Type TyName uni ann
_ -> Term name uni fun ann -> Term name uni fun ann
forall a. a -> a
id
    error :: forall ann. ann -> Type TyName uni ann -> Term name uni fun ann
error    = \ann
ann Type TyName uni ann
_ -> ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ann
ann
    constr :: forall ann.
ann
-> Type TyName uni ann
-> Word64
-> [Term name uni fun ann]
-> Term name uni fun ann
constr   = \ann
ann Type TyName uni ann
_ Word64
i [Term name uni fun ann]
es -> ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr ann
ann Word64
i [Term name uni fun ann]
es
    kase :: forall ann.
ann
-> Type TyName uni ann
-> Term name uni fun ann
-> [Term name uni fun ann]
-> Term name uni fun ann
kase     = \ann
ann Type TyName uni ann
_ Term name uni fun ann
arg [Term name uni fun ann]
cs -> ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case ann
ann Term name uni fun ann
arg ([Term name uni fun ann] -> Vector (Term name uni fun ann)
forall a. [a] -> Vector a
fromList [Term name uni fun ann]
cs)

instance TPLC.HasConstant (Term name uni fun ()) where
    asConstant :: Term name uni fun ()
-> Either
     BuiltinError (Some (ValueOf (UniOf (Term name uni fun ()))))
asConstant (Constant ()
_ Some (ValueOf uni)
val) = Some (ValueOf uni) -> Either BuiltinError (Some (ValueOf uni))
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant Term name uni fun ()
_                = Either BuiltinError (Some (ValueOf uni))
Either BuiltinError (Some (ValueOf (UniOf (Term name uni fun ()))))
forall (m :: * -> *) void. MonadError BuiltinError m => m void
TPLC.throwNotAConstant

    fromConstant :: Some (ValueOf (UniOf (Term name uni fun ())))
-> Term name uni fun ()
fromConstant = () -> Some (ValueOf uni) -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant ()

type instance TPLC.HasUniques (Term name uni fun ann) = TPLC.HasUnique name TPLC.TermUnique
type instance TPLC.HasUniques (Program name uni fun ann) = TPLC.HasUniques (Term name uni fun ann)

-- | An untyped "variable declaration", i.e. a name for a variable.
data UVarDecl name ann = UVarDecl
    { forall name ann. UVarDecl name ann -> ann
_uvarDeclAnn  :: ann
    , forall name ann. UVarDecl name ann -> name
_uvarDeclName :: name
    } deriving stock ((forall a b. (a -> b) -> UVarDecl name a -> UVarDecl name b)
-> (forall a b. a -> UVarDecl name b -> UVarDecl name a)
-> Functor (UVarDecl name)
forall a b. a -> UVarDecl name b -> UVarDecl name a
forall a b. (a -> b) -> UVarDecl name a -> UVarDecl name b
forall name a b. a -> UVarDecl name b -> UVarDecl name a
forall name a b. (a -> b) -> UVarDecl name a -> UVarDecl name b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall name a b. (a -> b) -> UVarDecl name a -> UVarDecl name b
fmap :: forall a b. (a -> b) -> UVarDecl name a -> UVarDecl name b
$c<$ :: forall name a b. a -> UVarDecl name b -> UVarDecl name a
<$ :: forall a b. a -> UVarDecl name b -> UVarDecl name a
Functor, Int -> UVarDecl name ann -> ShowS
[UVarDecl name ann] -> ShowS
UVarDecl name ann -> String
(Int -> UVarDecl name ann -> ShowS)
-> (UVarDecl name ann -> String)
-> ([UVarDecl name ann] -> ShowS)
-> Show (UVarDecl name ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall name ann.
(Show ann, Show name) =>
Int -> UVarDecl name ann -> ShowS
forall name ann.
(Show ann, Show name) =>
[UVarDecl name ann] -> ShowS
forall name ann.
(Show ann, Show name) =>
UVarDecl name ann -> String
$cshowsPrec :: forall name ann.
(Show ann, Show name) =>
Int -> UVarDecl name ann -> ShowS
showsPrec :: Int -> UVarDecl name ann -> ShowS
$cshow :: forall name ann.
(Show ann, Show name) =>
UVarDecl name ann -> String
show :: UVarDecl name ann -> String
$cshowList :: forall name ann.
(Show ann, Show name) =>
[UVarDecl name ann] -> ShowS
showList :: [UVarDecl name ann] -> ShowS
Show, (forall x. UVarDecl name ann -> Rep (UVarDecl name ann) x)
-> (forall x. Rep (UVarDecl name ann) x -> UVarDecl name ann)
-> Generic (UVarDecl name ann)
forall x. Rep (UVarDecl name ann) x -> UVarDecl name ann
forall x. UVarDecl name ann -> Rep (UVarDecl name ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall name ann x. Rep (UVarDecl name ann) x -> UVarDecl name ann
forall name ann x. UVarDecl name ann -> Rep (UVarDecl name ann) x
$cfrom :: forall name ann x. UVarDecl name ann -> Rep (UVarDecl name ann) x
from :: forall x. UVarDecl name ann -> Rep (UVarDecl name ann) x
$cto :: forall name ann x. Rep (UVarDecl name ann) x -> UVarDecl name ann
to :: forall x. Rep (UVarDecl name ann) x -> UVarDecl name ann
Generic)
makeLenses ''UVarDecl

-- | Return the outermost annotation of a 'Term'.
termAnn :: Term name uni fun ann -> ann
termAnn :: forall name (uni :: * -> *) fun ann. Term name uni fun ann -> ann
termAnn (Constant ann
ann Some (ValueOf uni)
_) = ann
ann
termAnn (Builtin ann
ann fun
_)  = ann
ann
termAnn (Var ann
ann name
_)      = ann
ann
termAnn (LamAbs ann
ann name
_ Term name uni fun ann
_) = ann
ann
termAnn (Apply ann
ann Term name uni fun ann
_ Term name uni fun ann
_)  = ann
ann
termAnn (Delay ann
ann Term name uni fun ann
_)    = ann
ann
termAnn (Force ann
ann Term name uni fun ann
_)    = ann
ann
termAnn (Error ann
ann)      = ann
ann
termAnn (Constr ann
ann Word64
_ [Term name uni fun ann]
_) = ann
ann
termAnn (Case ann
ann Term name uni fun ann
_ Vector (Term name uni fun ann)
_)   = ann
ann

bindFunM
    :: Monad m
    => (ann -> fun -> m (Term name uni fun' ann))
    -> Term name uni fun ann
    -> m (Term name uni fun' ann)
bindFunM :: forall (m :: * -> *) ann fun name (uni :: * -> *) fun'.
Monad m =>
(ann -> fun -> m (Term name uni fun' ann))
-> Term name uni fun ann -> m (Term name uni fun' ann)
bindFunM ann -> fun -> m (Term name uni fun' ann)
f = Term name uni fun ann -> m (Term name uni fun' ann)
go where
    go :: Term name uni fun ann -> m (Term name uni fun' ann)
go (Constant ann
ann Some (ValueOf uni)
val)     = Term name uni fun' ann -> m (Term name uni fun' ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term name uni fun' ann -> m (Term name uni fun' ann))
-> Term name uni fun' ann -> m (Term name uni fun' ann)
forall a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant ann
ann Some (ValueOf uni)
val
    go (Builtin ann
ann fun
fun)      = ann -> fun -> m (Term name uni fun' ann)
f ann
ann fun
fun
    go (Var ann
ann name
name)         = Term name uni fun' ann -> m (Term name uni fun' ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term name uni fun' ann -> m (Term name uni fun' ann))
-> Term name uni fun' ann -> m (Term name uni fun' ann)
forall a b. (a -> b) -> a -> b
$ ann -> name -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var ann
ann name
name
    go (LamAbs ann
ann name
name Term name uni fun ann
body) = ann -> name -> Term name uni fun' ann -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ann
ann name
name (Term name uni fun' ann -> Term name uni fun' ann)
-> m (Term name uni fun' ann) -> m (Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
body
    go (Apply ann
ann Term name uni fun ann
fun Term name uni fun ann
arg)    = ann
-> Term name uni fun' ann
-> Term name uni fun' ann
-> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ann
ann (Term name uni fun' ann
 -> Term name uni fun' ann -> Term name uni fun' ann)
-> m (Term name uni fun' ann)
-> m (Term name uni fun' ann -> Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
fun m (Term name uni fun' ann -> Term name uni fun' ann)
-> m (Term name uni fun' ann) -> m (Term name uni fun' ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
arg
    go (Delay ann
ann Term name uni fun ann
term)       = ann -> Term name uni fun' ann -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ann
ann (Term name uni fun' ann -> Term name uni fun' ann)
-> m (Term name uni fun' ann) -> m (Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
term
    go (Force ann
ann Term name uni fun ann
term)       = ann -> Term name uni fun' ann -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ann
ann (Term name uni fun' ann -> Term name uni fun' ann)
-> m (Term name uni fun' ann) -> m (Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
term
    go (Error ann
ann)            = Term name uni fun' ann -> m (Term name uni fun' ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term name uni fun' ann -> m (Term name uni fun' ann))
-> Term name uni fun' ann -> m (Term name uni fun' ann)
forall a b. (a -> b) -> a -> b
$ ann -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ann
ann
    go (Constr ann
ann Word64
i [Term name uni fun ann]
args)    = ann -> Word64 -> [Term name uni fun' ann] -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr ann
ann Word64
i ([Term name uni fun' ann] -> Term name uni fun' ann)
-> m [Term name uni fun' ann] -> m (Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term name uni fun ann -> m (Term name uni fun' ann))
-> [Term name uni fun ann] -> m [Term name uni fun' ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Term name uni fun ann -> m (Term name uni fun' ann)
go [Term name uni fun ann]
args
    go (Case ann
ann Term name uni fun ann
arg Vector (Term name uni fun ann)
cs)      = ann
-> Term name uni fun' ann
-> Vector (Term name uni fun' ann)
-> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case ann
ann (Term name uni fun' ann
 -> Vector (Term name uni fun' ann) -> Term name uni fun' ann)
-> m (Term name uni fun' ann)
-> m (Vector (Term name uni fun' ann) -> Term name uni fun' ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term name uni fun ann -> m (Term name uni fun' ann)
go Term name uni fun ann
arg m (Vector (Term name uni fun' ann) -> Term name uni fun' ann)
-> m (Vector (Term name uni fun' ann))
-> m (Term name uni fun' ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term name uni fun ann -> m (Term name uni fun' ann))
-> Vector (Term name uni fun ann)
-> m (Vector (Term name uni fun' ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Term name uni fun ann -> m (Term name uni fun' ann)
go Vector (Term name uni fun ann)
cs

bindFun
    :: (ann -> fun -> Term name uni fun' ann)
    -> Term name uni fun ann
    -> Term name uni fun' ann
bindFun :: forall ann fun name (uni :: * -> *) fun'.
(ann -> fun -> Term name uni fun' ann)
-> Term name uni fun ann -> Term name uni fun' ann
bindFun ann -> fun -> Term name uni fun' ann
f = Identity (Term name uni fun' ann) -> Term name uni fun' ann
forall a. Identity a -> a
runIdentity (Identity (Term name uni fun' ann) -> Term name uni fun' ann)
-> (Term name uni fun ann -> Identity (Term name uni fun' ann))
-> Term name uni fun ann
-> Term name uni fun' ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ann -> fun -> Identity (Term name uni fun' ann))
-> Term name uni fun ann -> Identity (Term name uni fun' ann)
forall (m :: * -> *) ann fun name (uni :: * -> *) fun'.
Monad m =>
(ann -> fun -> m (Term name uni fun' ann))
-> Term name uni fun ann -> m (Term name uni fun' ann)
bindFunM ((ann -> fun -> Term name uni fun' ann)
-> ann -> fun -> Identity (Term name uni fun' ann)
forall a b. Coercible a b => a -> b
coerce ann -> fun -> Term name uni fun' ann
f)

mapFun :: (ann -> fun -> fun') -> Term name uni fun ann -> Term name uni fun' ann
mapFun :: forall ann fun fun' name (uni :: * -> *).
(ann -> fun -> fun')
-> Term name uni fun ann -> Term name uni fun' ann
mapFun ann -> fun -> fun'
f = (ann -> fun -> Term name uni fun' ann)
-> Term name uni fun ann -> Term name uni fun' ann
forall ann fun name (uni :: * -> *) fun'.
(ann -> fun -> Term name uni fun' ann)
-> Term name uni fun ann -> Term name uni fun' ann
bindFun ((ann -> fun -> Term name uni fun' ann)
 -> Term name uni fun ann -> Term name uni fun' ann)
-> (ann -> fun -> Term name uni fun' ann)
-> Term name uni fun ann
-> Term name uni fun' ann
forall a b. (a -> b) -> a -> b
$ \ann
ann fun
fun -> ann -> fun' -> Term name uni fun' ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ann
ann (ann -> fun -> fun'
f ann
ann fun
fun)