{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

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

import Control.Lens
import PlutusPrelude

import PlutusCore.Builtin qualified as TPLC
import PlutusCore.Core qualified as TPLC
import PlutusCore.MkPlc
import PlutusCore.Name 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.
-}

{-| 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
    deriving stock (Int -> Term name uni fun ann -> ShowS
[Term name uni fun ann] -> ShowS
Term name uni fun ann -> String
(Int -> Term name uni fun ann -> ShowS)
-> (Term name uni fun ann -> String)
-> ([Term name uni fun ann] -> ShowS)
-> Show (Term name uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Int -> Term name uni fun ann -> ShowS
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
[Term name uni fun ann] -> ShowS
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Term name uni fun ann -> String
showList :: [Term name uni fun ann] -> ShowS
$cshowList :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
[Term name uni fun ann] -> ShowS
show :: Term name uni fun ann -> String
$cshow :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Term name uni fun ann -> String
showsPrec :: Int -> Term name uni fun ann -> ShowS
$cshowsPrec :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Int -> Term name uni fun ann -> ShowS
Show, a -> Term name uni fun b -> Term name uni fun a
(a -> b) -> Term name uni fun a -> Term name uni fun b
(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
<$ :: a -> Term name uni fun b -> Term name uni fun a
$c<$ :: forall name (uni :: * -> *) fun a b.
a -> Term name uni fun b -> Term name uni fun a
fmap :: (a -> b) -> Term name uni fun a -> Term name uni fun b
$cfmap :: forall name (uni :: * -> *) fun a b.
(a -> b) -> Term name uni fun a -> Term name uni fun b
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
$cto :: forall name (uni :: * -> *) fun ann x.
Rep (Term name uni fun ann) x -> Term name uni fun ann
$cfrom :: forall name (uni :: * -> *) fun ann x.
Term name uni fun ann -> Rep (Term name uni fun ann) x
Generic)
    deriving anyclass (Term name uni fun ann -> ()
(Term name uni fun ann -> ()) -> NFData (Term name uni fun ann)
forall a. (a -> ()) -> NFData a
forall name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData fun) =>
Term name uni fun ann -> ()
rnf :: Term name uni fun ann -> ()
$crnf :: forall name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData fun) =>
Term name uni fun ann -> ()
NFData)

-- | A 'Program' is simply a 'Term' coupled with a 'Version' of the core language.
data Program name uni fun ann = Program
    { Program name uni fun ann -> ann
_progAnn  :: ann
    , Program name uni fun ann -> Version ann
_progVer  :: TPLC.Version ann
    , Program name uni fun ann -> Term name uni fun ann
_progTerm :: Term name uni fun ann
    }
    deriving stock (Int -> Program name uni fun ann -> ShowS
[Program name uni fun ann] -> ShowS
Program name uni fun ann -> String
(Int -> Program name uni fun ann -> ShowS)
-> (Program name uni fun ann -> String)
-> ([Program name uni fun ann] -> ShowS)
-> Show (Program name uni fun ann)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Int -> Program name uni fun ann -> ShowS
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
[Program name uni fun ann] -> ShowS
forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Program name uni fun ann -> String
showList :: [Program name uni fun ann] -> ShowS
$cshowList :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
[Program name uni fun ann] -> ShowS
show :: Program name uni fun ann -> String
$cshow :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Program name uni fun ann -> String
showsPrec :: Int -> Program name uni fun ann -> ShowS
$cshowsPrec :: forall name (uni :: * -> *) fun ann.
(Everywhere uni Show, GShow uni, Closed uni, Show ann, Show name,
 Show fun) =>
Int -> Program name uni fun ann -> ShowS
Show, a -> Program name uni fun b -> Program name uni fun a
(a -> b) -> Program name uni fun a -> Program name uni fun b
(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
<$ :: a -> Program name uni fun b -> Program name uni fun a
$c<$ :: forall name (uni :: * -> *) fun a b.
a -> Program name uni fun b -> Program name uni fun a
fmap :: (a -> b) -> Program name uni fun a -> Program name uni fun b
$cfmap :: forall name (uni :: * -> *) fun a b.
(a -> b) -> Program name uni fun a -> Program name uni fun b
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
$cto :: forall name (uni :: * -> *) fun ann x.
Rep (Program name uni fun ann) x -> Program name uni fun ann
$cfrom :: forall name (uni :: * -> *) fun ann x.
Program name uni fun ann -> Rep (Program name uni fun ann) x
Generic)
    deriving anyclass (Program name uni fun ann -> ()
(Program name uni fun ann -> ())
-> NFData (Program name uni fun ann)
forall a. (a -> ()) -> NFData a
forall name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData fun) =>
Program name uni fun ann -> ()
rnf :: Program name uni fun ann -> ()
$crnf :: forall name (uni :: * -> *) fun ann.
(Everywhere uni NFData, Closed uni, NFData ann, NFData name,
 NFData fun) =>
Program name uni fun ann -> ()
NFData)
makeLenses ''Program

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

instance TermLike (Term name uni fun) TPLC.TyName name uni fun where
    var :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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

instance TPLC.AsConstant (Term name uni fun ann) where
    asConstant :: Maybe cause
-> Term name uni fun ann
-> m (Some (ValueOf (UniOf (Term name uni fun ann))))
asConstant Maybe cause
_        (Constant ann
_ Some (ValueOf uni)
val) = Some (ValueOf uni) -> m (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant Maybe cause
mayCause Term name uni fun ann
_                = Maybe cause -> m (Some (ValueOf uni))
forall err cause (m :: * -> *) r.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause -> m r
TPLC.throwNotAConstant Maybe cause
mayCause

instance TPLC.FromConstant (Term name uni fun ()) where
    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
    { UVarDecl name ann -> ann
_uvarDeclAnn  :: ann
    , UVarDecl name ann -> name
_uvarDeclName :: name
    } deriving (a -> UVarDecl name b -> UVarDecl name a
(a -> b) -> UVarDecl name a -> UVarDecl name b
(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
<$ :: a -> UVarDecl name b -> UVarDecl name a
$c<$ :: forall name a b. a -> UVarDecl name b -> UVarDecl name a
fmap :: (a -> b) -> UVarDecl name a -> UVarDecl name b
$cfmap :: forall name a b. (a -> b) -> UVarDecl name a -> UVarDecl name b
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
showList :: [UVarDecl name ann] -> ShowS
$cshowList :: forall name ann.
(Show ann, Show name) =>
[UVarDecl name ann] -> ShowS
show :: UVarDecl name ann -> String
$cshow :: forall name ann.
(Show ann, Show name) =>
UVarDecl name ann -> String
showsPrec :: Int -> UVarDecl name ann -> ShowS
$cshowsPrec :: forall name ann.
(Show ann, Show name) =>
Int -> 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
$cto :: forall name ann x. Rep (UVarDecl name ann) x -> UVarDecl name ann
$cfrom :: forall name ann x. UVarDecl name ann -> Rep (UVarDecl name ann) x
Generic)
makeLenses ''UVarDecl

-- | Return the outermost annotation of a 'Term'.
termAnn :: Term name uni fun ann -> ann
termAnn :: 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

bindFunM
    :: 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))
-> 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 (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 (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 (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 (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

bindFun
    :: (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
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)
coerce ann -> fun -> Term name uni fun' ann
f)

mapFun :: (ann -> fun -> fun') -> Term name uni fun ann -> Term name uni fun' ann
mapFun :: (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)

-- | Erase a Typed Plutus Core term to its untyped counterpart.
erase :: TPLC.Term tyname name uni fun ann -> Term name uni fun ann
erase :: Term tyname name uni fun ann -> Term name uni fun ann
erase (TPLC.Var ann
ann name
name)           = ann -> name -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var ann
ann name
name
erase (TPLC.TyAbs ann
ann tyname
_ Kind ann
_ Term tyname name uni fun ann
body)     = 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 tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
body)
erase (TPLC.LamAbs ann
ann name
name Type tyname uni ann
_ Term tyname 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 tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
body)
erase (TPLC.Apply ann
ann Term tyname name uni fun ann
fun Term tyname 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 tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
fun) (Term tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
arg)
erase (TPLC.Constant ann
ann Some (ValueOf uni)
con)       = 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)
con
erase (TPLC.Builtin ann
ann fun
bn)         = ann -> fun -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ann
ann fun
bn
erase (TPLC.TyInst ann
ann Term tyname 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 tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
term)
erase (TPLC.Unwrap ann
_ Term tyname name uni fun ann
term)          = Term tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
term
erase (TPLC.IWrap ann
_ Type tyname uni ann
_ Type tyname uni ann
_ Term tyname name uni fun ann
term)       = Term tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
term
erase (TPLC.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

-- | Erase a Typed Plutus Core Program to its untyped counterpart.
eraseProgram :: TPLC.Program tyname name uni fun ann -> Program name uni fun ann
eraseProgram :: Program tyname name uni fun ann -> Program name uni fun ann
eraseProgram (TPLC.Program ann
a Version ann
v Term tyname name uni fun ann
t) = ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
forall name (uni :: * -> *) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
Program ann
a Version ann
v (Term name uni fun ann -> Program name uni fun ann)
-> Term name uni fun ann -> Program name uni fun ann
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann -> Term name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann -> Term name uni fun ann
erase Term tyname name uni fun ann
t