{-# 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
, 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
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
| 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)
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.HasConstant (Term name uni fun ()) where
asConstant :: Maybe cause
-> Term name uni fun ()
-> Either
(ErrorWithCause err cause)
(Some (ValueOf (UniOf (Term name uni fun ()))))
asConstant Maybe cause
_ (Constant ()
_ Some (ValueOf uni)
val) = Some (ValueOf uni)
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
asConstant Maybe cause
mayCause Term name uni fun ()
_ = Maybe cause
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall err cause (m :: * -> *) r.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause -> m r
TPLC.throwNotAConstant Maybe cause
mayCause
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)
data UVarDecl name ann = UVarDecl
{ UVarDecl name ann -> ann
_uvarDeclAnn :: ann
, UVarDecl name ann -> name
_uvarDeclName :: name
} deriving stock (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
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 :: 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
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