module PlutusCore.Compiler.Erase (eraseTerm, eraseProgram) where

import Data.Vector (fromList)
import PlutusCore.Core
import PlutusCore.Name.Unique
import UntypedPlutusCore.Core qualified as UPLC

{-| Erase a Typed Plutus Core term to its untyped counterpart.

Restricted to Plc terms with `Name`s, because erasing a (Named-)Debruijn term will
mess up its debruijn indexing and thus break scope-checking.
-- FIXME: Lift this restriction of `eraseTerm` for (Named-)DeBruijn terms.
-}
eraseTerm :: HasUnique name TermUnique
          => Term tyname name uni fun ann
          -> UPLC.Term name uni fun ann
eraseTerm :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm (Var ann
ann name
name)           = ann -> name -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
UPLC.Var ann
ann name
name
eraseTerm (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
UPLC.Delay ann
ann (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
body)
eraseTerm (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
UPLC.LamAbs ann
ann name
name (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
body)
eraseTerm (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
UPLC.Apply ann
ann (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
fun) (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
arg)
eraseTerm (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
UPLC.Constant ann
ann Some (ValueOf uni)
con
eraseTerm (Builtin ann
ann fun
bn)         = ann -> fun -> Term name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
UPLC.Builtin ann
ann fun
bn
eraseTerm (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
UPLC.Force ann
ann (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
term)
eraseTerm (Unwrap ann
_ Term tyname name uni fun ann
term)          = Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
term
eraseTerm (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 name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
term
eraseTerm (Error ann
ann Type tyname uni ann
_)            = ann -> Term name uni fun ann
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
UPLC.Error ann
ann
eraseTerm (Constr ann
ann Type tyname uni ann
_ Word64
i [Term tyname 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
UPLC.Constr ann
ann Word64
i ((Term tyname name uni fun ann -> Term name uni fun ann)
-> [Term tyname name uni fun ann] -> [Term name uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm [Term tyname name uni fun ann]
args)
eraseTerm (Case ann
ann Type tyname uni ann
_ Term tyname name uni fun ann
arg [Term tyname 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
UPLC.Case ann
ann (Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname 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] -> Vector (Term name uni fun ann))
-> [Term name uni fun ann] -> Vector (Term name uni fun ann)
forall a b. (a -> b) -> a -> b
$ (Term tyname name uni fun ann -> Term name uni fun ann)
-> [Term tyname name uni fun ann] -> [Term name uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term tyname name uni fun ann -> Term name uni fun ann
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm [Term tyname name uni fun ann]
cs)

eraseProgram :: HasUnique name TermUnique
             => Program tyname name uni fun ann
             -> UPLC.Program name uni fun ann
eraseProgram :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Program tyname name uni fun ann -> Program name uni fun ann
eraseProgram (Program ann
a Version
v Term tyname name uni fun ann
t) = ann -> Version -> Term name uni fun ann -> Program name uni fun ann
forall name (uni :: * -> *) fun ann.
ann -> Version -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program ann
a Version
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 name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Term tyname name uni fun ann -> Term name uni fun ann
eraseTerm Term tyname name uni fun ann
t