{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusIR.Core.Type (
TyName (..),
Name (..),
VarDecl (..),
TyVarDecl (..),
varDeclNameString,
tyVarDeclNameString,
Kind (..),
Type (..),
Datatype (..),
datatypeNameString,
Recursivity (..),
Strictness (..),
Binding (..),
Term (..),
Program (..),
applyProgram,
termAnn,
progAnn,
progTerm,
) where
import PlutusPrelude
import Control.Lens.TH
import PlutusCore (Kind, Name, TyName, Type (..))
import PlutusCore qualified as PLC
import PlutusCore.Builtin (HasConstant (..), throwNotAConstant)
import PlutusCore.Core (UniOf)
import PlutusCore.Flat ()
import PlutusCore.MkPlc (Def (..), TermLike (..), TyVarDecl (..), VarDecl (..))
import PlutusCore.Name qualified as PLC
import Data.Text qualified as T
data Datatype tyname name uni fun a = Datatype a (TyVarDecl tyname a) [TyVarDecl tyname a] name [VarDecl tyname name uni fun a]
deriving stock (a
-> Datatype tyname name uni fun b -> Datatype tyname name uni fun a
(a -> b)
-> Datatype tyname name uni fun a -> Datatype tyname name uni fun b
(forall a b.
(a -> b)
-> Datatype tyname name uni fun a
-> Datatype tyname name uni fun b)
-> (forall a b.
a
-> Datatype tyname name uni fun b
-> Datatype tyname name uni fun a)
-> Functor (Datatype tyname name uni fun)
forall a b.
a
-> Datatype tyname name uni fun b -> Datatype tyname name uni fun a
forall a b.
(a -> b)
-> Datatype tyname name uni fun a -> Datatype tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a
-> Datatype tyname name uni fun b -> Datatype tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Datatype tyname name uni fun a -> Datatype tyname 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
-> Datatype tyname name uni fun b -> Datatype tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a
-> Datatype tyname name uni fun b -> Datatype tyname name uni fun a
fmap :: (a -> b)
-> Datatype tyname name uni fun a -> Datatype tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Datatype tyname name uni fun a -> Datatype tyname name uni fun b
Functor, Int -> Datatype tyname name uni fun a -> ShowS
[Datatype tyname name uni fun a] -> ShowS
Datatype tyname name uni fun a -> String
(Int -> Datatype tyname name uni fun a -> ShowS)
-> (Datatype tyname name uni fun a -> String)
-> ([Datatype tyname name uni fun a] -> ShowS)
-> Show (Datatype tyname name uni fun a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
Int -> Datatype tyname name uni fun a -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
[Datatype tyname name uni fun a] -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
Datatype tyname name uni fun a -> String
showList :: [Datatype tyname name uni fun a] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
[Datatype tyname name uni fun a] -> ShowS
show :: Datatype tyname name uni fun a -> String
$cshow :: forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
Datatype tyname name uni fun a -> String
showsPrec :: Int -> Datatype tyname name uni fun a -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun a.
(Show a, Show tyname, Show name, GShow uni) =>
Int -> Datatype tyname name uni fun a -> ShowS
Show, (forall x.
Datatype tyname name uni fun a
-> Rep (Datatype tyname name uni fun a) x)
-> (forall x.
Rep (Datatype tyname name uni fun a) x
-> Datatype tyname name uni fun a)
-> Generic (Datatype tyname name uni fun a)
forall x.
Rep (Datatype tyname name uni fun a) x
-> Datatype tyname name uni fun a
forall x.
Datatype tyname name uni fun a
-> Rep (Datatype tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Datatype tyname name uni fun a) x
-> Datatype tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Datatype tyname name uni fun a
-> Rep (Datatype tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Datatype tyname name uni fun a) x
-> Datatype tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Datatype tyname name uni fun a
-> Rep (Datatype tyname name uni fun a) x
Generic)
varDeclNameString :: VarDecl tyname Name uni fun a -> String
varDeclNameString :: VarDecl tyname Name uni fun a -> String
varDeclNameString = Text -> String
T.unpack (Text -> String)
-> (VarDecl tyname Name uni fun a -> Text)
-> VarDecl tyname Name uni fun a
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Text
PLC.nameString (Name -> Text)
-> (VarDecl tyname Name uni fun a -> Name)
-> VarDecl tyname Name uni fun a
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname Name uni fun a -> Name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName
tyVarDeclNameString :: TyVarDecl TyName a -> String
tyVarDeclNameString :: TyVarDecl TyName a -> String
tyVarDeclNameString = Text -> String
T.unpack (Text -> String)
-> (TyVarDecl TyName a -> Text) -> TyVarDecl TyName a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Text
PLC.nameString (Name -> Text)
-> (TyVarDecl TyName a -> Name) -> TyVarDecl TyName a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Name
PLC.unTyName (TyName -> Name)
-> (TyVarDecl TyName a -> TyName) -> TyVarDecl TyName a -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl TyName a -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName
datatypeNameString :: Datatype TyName Name uni fun a -> String
datatypeNameString :: Datatype TyName Name uni fun a -> String
datatypeNameString (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
_ Name
_ [VarDecl TyName Name uni fun a]
_) = TyVarDecl TyName a -> String
forall a. TyVarDecl TyName a -> String
tyVarDeclNameString TyVarDecl TyName a
tn
data Recursivity = NonRec | Rec
deriving stock (Int -> Recursivity -> ShowS
[Recursivity] -> ShowS
Recursivity -> String
(Int -> Recursivity -> ShowS)
-> (Recursivity -> String)
-> ([Recursivity] -> ShowS)
-> Show Recursivity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Recursivity] -> ShowS
$cshowList :: [Recursivity] -> ShowS
show :: Recursivity -> String
$cshow :: Recursivity -> String
showsPrec :: Int -> Recursivity -> ShowS
$cshowsPrec :: Int -> Recursivity -> ShowS
Show, Recursivity -> Recursivity -> Bool
(Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool) -> Eq Recursivity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Recursivity -> Recursivity -> Bool
$c/= :: Recursivity -> Recursivity -> Bool
== :: Recursivity -> Recursivity -> Bool
$c== :: Recursivity -> Recursivity -> Bool
Eq, (forall x. Recursivity -> Rep Recursivity x)
-> (forall x. Rep Recursivity x -> Recursivity)
-> Generic Recursivity
forall x. Rep Recursivity x -> Recursivity
forall x. Recursivity -> Rep Recursivity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Recursivity x -> Recursivity
$cfrom :: forall x. Recursivity -> Rep Recursivity x
Generic, Eq Recursivity
Eq Recursivity
-> (Recursivity -> Recursivity -> Ordering)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Bool)
-> (Recursivity -> Recursivity -> Recursivity)
-> (Recursivity -> Recursivity -> Recursivity)
-> Ord Recursivity
Recursivity -> Recursivity -> Bool
Recursivity -> Recursivity -> Ordering
Recursivity -> Recursivity -> Recursivity
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Recursivity -> Recursivity -> Recursivity
$cmin :: Recursivity -> Recursivity -> Recursivity
max :: Recursivity -> Recursivity -> Recursivity
$cmax :: Recursivity -> Recursivity -> Recursivity
>= :: Recursivity -> Recursivity -> Bool
$c>= :: Recursivity -> Recursivity -> Bool
> :: Recursivity -> Recursivity -> Bool
$c> :: Recursivity -> Recursivity -> Bool
<= :: Recursivity -> Recursivity -> Bool
$c<= :: Recursivity -> Recursivity -> Bool
< :: Recursivity -> Recursivity -> Bool
$c< :: Recursivity -> Recursivity -> Bool
compare :: Recursivity -> Recursivity -> Ordering
$ccompare :: Recursivity -> Recursivity -> Ordering
$cp1Ord :: Eq Recursivity
Ord)
instance Semigroup Recursivity where
Recursivity
NonRec <> :: Recursivity -> Recursivity -> Recursivity
<> Recursivity
x = Recursivity
x
Recursivity
Rec <> Recursivity
_ = Recursivity
Rec
data Strictness = NonStrict | Strict
deriving stock (Int -> Strictness -> ShowS
[Strictness] -> ShowS
Strictness -> String
(Int -> Strictness -> ShowS)
-> (Strictness -> String)
-> ([Strictness] -> ShowS)
-> Show Strictness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Strictness] -> ShowS
$cshowList :: [Strictness] -> ShowS
show :: Strictness -> String
$cshow :: Strictness -> String
showsPrec :: Int -> Strictness -> ShowS
$cshowsPrec :: Int -> Strictness -> ShowS
Show, Strictness -> Strictness -> Bool
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: Strictness -> Strictness -> Bool
Eq, (forall x. Strictness -> Rep Strictness x)
-> (forall x. Rep Strictness x -> Strictness) -> Generic Strictness
forall x. Rep Strictness x -> Strictness
forall x. Strictness -> Rep Strictness x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Strictness x -> Strictness
$cfrom :: forall x. Strictness -> Rep Strictness x
Generic)
data Binding tyname name uni fun a = TermBind a Strictness (VarDecl tyname name uni fun a) (Term tyname name uni fun a)
| TypeBind a (TyVarDecl tyname a) (Type tyname uni a)
| DatatypeBind a (Datatype tyname name uni fun a)
deriving stock (a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
(forall a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b)
-> (forall a b.
a
-> Binding tyname name uni fun b -> Binding tyname name uni fun a)
-> Functor (Binding tyname name uni fun)
forall a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
forall a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname 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 -> Binding tyname name uni fun b -> Binding tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Binding tyname name uni fun b -> Binding tyname name uni fun a
fmap :: (a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Binding tyname name uni fun a -> Binding tyname name uni fun b
Functor, Int -> Binding tyname name uni fun a -> ShowS
[Binding tyname name uni fun a] -> ShowS
Binding tyname name uni fun a -> String
(Int -> Binding tyname name uni fun a -> ShowS)
-> (Binding tyname name uni fun a -> String)
-> ([Binding tyname name uni fun a] -> ShowS)
-> Show (Binding tyname name uni fun a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Int -> Binding tyname name uni fun a -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
[Binding tyname name uni fun a] -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Binding tyname name uni fun a -> String
showList :: [Binding tyname name uni fun a] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
[Binding tyname name uni fun a] -> ShowS
show :: Binding tyname name uni fun a -> String
$cshow :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Binding tyname name uni fun a -> String
showsPrec :: Int -> Binding tyname name uni fun a -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Int -> Binding tyname name uni fun a -> ShowS
Show, (forall x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x)
-> (forall x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a)
-> Generic (Binding tyname name uni fun a)
forall x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
forall x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Binding tyname name uni fun a) x
-> Binding tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Binding tyname name uni fun a
-> Rep (Binding tyname name uni fun a) x
Generic)
data Term tyname name uni fun a =
Let a Recursivity (NonEmpty (Binding tyname name uni fun a)) (Term tyname name uni fun a)
| Var a name
| TyAbs a tyname (Kind a) (Term tyname name uni fun a)
| LamAbs a name (Type tyname uni a) (Term tyname name uni fun a)
| Apply a (Term tyname name uni fun a) (Term tyname name uni fun a)
| Constant a (PLC.Some (PLC.ValueOf uni))
| Builtin a fun
| TyInst a (Term tyname name uni fun a) (Type tyname uni a)
| Error a (Type tyname uni a)
| IWrap a (Type tyname uni a) (Type tyname uni a) (Term tyname name uni fun a)
| Unwrap a (Term tyname name uni fun a)
deriving stock (a -> Term tyname name uni fun b -> Term tyname name uni fun a
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
(forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b)
-> (forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a)
-> Functor (Term tyname name uni fun)
forall a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname 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 tyname name uni fun b -> Term tyname name uni fun a
$c<$ :: forall tyname name (uni :: * -> *) fun a b.
a -> Term tyname name uni fun b -> Term tyname name uni fun a
fmap :: (a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
$cfmap :: forall tyname name (uni :: * -> *) fun a b.
(a -> b)
-> Term tyname name uni fun a -> Term tyname name uni fun b
Functor, Int -> Term tyname name uni fun a -> ShowS
[Term tyname name uni fun a] -> ShowS
Term tyname name uni fun a -> String
(Int -> Term tyname name uni fun a -> ShowS)
-> (Term tyname name uni fun a -> String)
-> ([Term tyname name uni fun a] -> ShowS)
-> Show (Term tyname name uni fun a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Int -> Term tyname name uni fun a -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
[Term tyname name uni fun a] -> ShowS
forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Term tyname name uni fun a -> String
showList :: [Term tyname name uni fun a] -> ShowS
$cshowList :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
[Term tyname name uni fun a] -> ShowS
show :: Term tyname name uni fun a -> String
$cshow :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Term tyname name uni fun a -> String
showsPrec :: Int -> Term tyname name uni fun a -> ShowS
$cshowsPrec :: forall tyname name (uni :: * -> *) fun a.
(Everywhere uni Show, GShow uni, Closed uni, Show a, Show name,
Show tyname, Show fun) =>
Int -> Term tyname name uni fun a -> ShowS
Show, (forall x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x)
-> (forall x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a)
-> Generic (Term tyname name uni fun a)
forall x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
forall x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun a x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun a x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
$cto :: forall tyname name (uni :: * -> *) fun a x.
Rep (Term tyname name uni fun a) x -> Term tyname name uni fun a
$cfrom :: forall tyname name (uni :: * -> *) fun a x.
Term tyname name uni fun a -> Rep (Term tyname name uni fun a) x
Generic)
type instance UniOf (Term tyname name uni fun ann) = uni
instance HasConstant (Term tyname name uni fun ()) where
asConstant :: Maybe cause
-> Term tyname name uni fun ()
-> Either
(ErrorWithCause err cause)
(Some (ValueOf (UniOf (Term tyname 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 tyname 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
throwNotAConstant Maybe cause
mayCause
fromConstant :: Some (ValueOf (UniOf (Term tyname name uni fun ())))
-> Term tyname name uni fun ()
fromConstant = () -> Some (ValueOf uni) -> Term tyname name uni fun ()
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant ()
instance TermLike (Term tyname name uni fun) tyname name uni fun where
var :: ann -> name -> Term tyname name uni fun ann
var = ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var
tyAbs :: ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
tyAbs = ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs
lamAbs :: ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
lamAbs = ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs
apply :: ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
apply = ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply
constant :: ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
constant = ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant
builtin :: ann -> fun -> Term tyname name uni fun ann
builtin = ann -> fun -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin
tyInst :: ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
tyInst = ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst
unwrap :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
unwrap = ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap
iWrap :: ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
iWrap = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap
error :: ann -> Type tyname uni ann -> Term tyname name uni fun ann
error = ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error
termLet :: ann
-> TermDef (Term tyname name uni fun) tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
termLet ann
x (Def VarDecl tyname name uni fun ann
vd Term tyname name uni fun ann
bind) = ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
NonRec (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni fun ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
Strict VarDecl tyname name uni fun ann
vd Term tyname name uni fun ann
bind)
typeLet :: ann
-> TypeDef tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
typeLet ann
x (Def TyVarDecl tyname ann
vd Type tyname uni ann
bind) = ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
NonRec (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> NonEmpty (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
vd Type tyname uni ann
bind)
data Program tyname name uni fun ann = Program
{ Program tyname name uni fun ann -> ann
_progAnn :: ann
, Program tyname name uni fun ann -> Term tyname name uni fun ann
_progTerm :: Term tyname name uni fun ann
}
deriving stock (forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x)
-> (forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann)
-> Generic (Program tyname name uni fun ann)
forall x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
$cto :: forall tyname name (uni :: * -> *) fun ann x.
Rep (Program tyname name uni fun ann) x
-> Program tyname name uni fun ann
$cfrom :: forall tyname name (uni :: * -> *) fun ann x.
Program tyname name uni fun ann
-> Rep (Program tyname name uni fun ann) x
Generic
makeLenses ''Program
type instance PLC.HasUniques (Term tyname name uni fun ann) = (PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique)
type instance PLC.HasUniques (Program tyname name uni fun ann) = PLC.HasUniques (Term tyname name uni fun ann)
applyProgram
:: Monoid a
=> Program tyname name uni fun a
-> Program tyname name uni fun a
-> Program tyname name uni fun a
applyProgram :: Program tyname name uni fun a
-> Program tyname name uni fun a -> Program tyname name uni fun a
applyProgram (Program a
a1 Term tyname name uni fun a
t1) (Program a
a2 Term tyname name uni fun a
t2) = a -> Term tyname name uni fun a -> Program tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
Program (a
a1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a2) (a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply a
forall a. Monoid a => a
mempty Term tyname name uni fun a
t1 Term tyname name uni fun a
t2)
termAnn :: Term tyname name uni fun a -> a
termAnn :: Term tyname name uni fun a -> a
termAnn Term tyname name uni fun a
t = case Term tyname name uni fun a
t of
Let a
a Recursivity
_ NonEmpty (Binding tyname name uni fun a)
_ Term tyname name uni fun a
_ -> a
a
Var a
a name
_ -> a
a
TyAbs a
a tyname
_ Kind a
_ Term tyname name uni fun a
_ -> a
a
LamAbs a
a name
_ Type tyname uni a
_ Term tyname name uni fun a
_ -> a
a
Apply a
a Term tyname name uni fun a
_ Term tyname name uni fun a
_ -> a
a
Constant a
a Some (ValueOf uni)
_ -> a
a
Builtin a
a fun
_ -> a
a
TyInst a
a Term tyname name uni fun a
_ Type tyname uni a
_ -> a
a
Error a
a Type tyname uni a
_ -> a
a
IWrap a
a Type tyname uni a
_ Type tyname uni a
_ Term tyname name uni fun a
_ -> a
a
Unwrap a
a Term tyname name uni fun a
_ -> a
a