Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.MkPlc

Synopsis

class TermLike term tyname name uni fun | term -> tyname name uni fun where
- var :: ann -> name -> term ann
- tyAbs :: ann -> tyname -> Kind ann -> term ann -> term ann
- lamAbs :: ann -> name -> Type tyname uni ann -> term ann -> term ann
- apply :: ann -> term ann -> term ann -> term ann
- constant :: ann -> Some (ValueOf uni) -> term ann
- builtin :: ann -> fun -> term ann
- tyInst :: ann -> term ann -> Type tyname uni ann -> term ann
- unwrap :: ann -> term ann -> term ann
- iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> term ann -> term ann
- error :: ann -> Type tyname uni ann -> term ann
- constr :: ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
- kase :: ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
- termLet :: ann -> TermDef term tyname name uni ann -> term ann -> term ann
- typeLet :: ann -> TypeDef tyname uni ann -> term ann -> term ann
type family UniOf a :: Type -> Type
type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x)
type HasTermLevel uni = Includes uni
type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x)
mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltin :: forall a (x :: a) uni ann tyname. uni `HasTypeLevel` x => ann -> Type tyname uni ann
mkConstantOf :: forall a uni fun term tyname name ann. TermLike term tyname name uni fun => ann -> uni (Esc a) -> a -> term ann
mkConstant :: forall a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `HasTermLevel` a) => ann -> a -> term ann
data VarDecl tyname name uni ann = VarDecl {
- _varDeclAnn :: ann
- _varDeclName :: name
- _varDeclType :: Type tyname uni ann
}
data TyVarDecl tyname ann = TyVarDecl {
- _tyVarDeclAnn :: ann
- _tyVarDeclName :: tyname
- _tyVarDeclKind :: Kind ann
}
data TyDecl tyname uni ann = TyDecl {
- _tyDeclAnn :: ann
- _tyDeclType :: Type tyname uni ann
- _tyDeclKind :: Kind ann
}
mkVar :: TermLike term tyname name uni fun => ann -> VarDecl tyname name uni ann -> term ann
mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann
tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann
data Def var val = Def {
- defVar :: var
- defVal :: val
}
embedTerm :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
type TermDef term tyname name uni ann = Def (VarDecl tyname name uni ann) (term ann)
type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann)
data FunctionType tyname uni ann = FunctionType {
- _functionTypeAnn :: ann
- _functionTypeDom :: Type tyname uni ann
- _functionTypeCod :: Type tyname uni ann
}
data FunctionDef term tyname name uni fun ann = FunctionDef {
- _functionDefAnn :: ann
- _functionDefName :: name
- _functionDefType :: FunctionType tyname uni ann
- _functionDefTerm :: term ann
}
functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann
functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefVarDecl :: FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni ann
mkFunctionDef :: ann -> name -> Type tyname uni ann -> term ann -> Maybe (FunctionDef term tyname name uni fun ann)
mkImmediateLamAbs :: TermLike term tyname name uni fun => ann -> TermDef term tyname name uni ann -> term ann -> term ann
mkImmediateTyAbs :: TermLike term tyname name uni fun => ann -> TypeDef tyname uni ann -> term ann -> term ann
mkIterTyForall :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterApp :: TermLike term tyname name uni fun => term ann -> [(ann, term ann)] -> term ann
mkIterAppNoAnn :: TermLike term tyname name uni fun => term () -> [term ()] -> term ()
(@@) :: TermLike term tyname name uni fun => term () -> [term ()] -> term ()
mkIterTyFun :: ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann
mkIterLamAbs :: TermLike term tyname name uni fun => [VarDecl tyname name uni ann] -> term ann -> term ann
mkIterInst :: TermLike term tyname name uni fun => term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInstNoAnn :: TermLike term tyname name uni fun => term () -> [Type tyname uni ()] -> term ()
mkIterTyAbs :: TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyApp :: Type tyname uni ann -> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyAppNoAnn :: Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann
mkFreshTermLet :: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a) => Type tyname uni a -> t a -> m (t a, t a -> t a)

Documentation

class TermLike term tyname name uni fun | term -> tyname name uni fun where Source #

A final encoding for Term, to allow PLC terms to be used transparently as PIR terms.

Minimal complete definition

var, tyAbs, lamAbs, apply, constant, builtin, tyInst, unwrap, iWrap, error, constr, kase

Methods

var :: ann -> name -> term ann Source #

tyAbs :: ann -> tyname -> Kind ann -> term ann -> term ann Source #

lamAbs :: ann -> name -> Type tyname uni ann -> term ann -> term ann Source #

apply :: ann -> term ann -> term ann -> term ann Source #

constant :: ann -> Some (ValueOf uni) -> term ann Source #

builtin :: ann -> fun -> term ann Source #

tyInst :: ann -> term ann -> Type tyname uni ann -> term ann Source #

unwrap :: ann -> term ann -> term ann Source #

iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> term ann -> term ann Source #

error :: ann -> Type tyname uni ann -> term ann Source #

constr :: ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann Source #

kase :: ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann Source #

termLet :: ann -> TermDef term tyname name uni ann -> term ann -> term ann Source #

typeLet :: ann -> TypeDef tyname uni ann -> term ann -> term ann Source #

Instances

Instances details

TermLike (Term name uni fun) TyName name uni fun Source #
Instance details Defined in UntypedPlutusCore.Core.Type Methods var :: ann -> name -> Term name uni fun ann Source # tyAbs :: ann -> TyName -> Kind ann -> Term name uni fun ann -> Term name uni fun ann Source # lamAbs :: ann -> name -> Type TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source # apply :: ann -> Term name uni fun ann -> Term name uni fun ann -> Term name uni fun ann Source # constant :: ann -> Some (ValueOf uni) -> Term name uni fun ann Source # builtin :: ann -> fun -> Term name uni fun ann Source # tyInst :: ann -> Term name uni fun ann -> Type TyName uni ann -> Term name uni fun ann Source # unwrap :: ann -> Term name uni fun ann -> Term name uni fun ann Source # iWrap :: ann -> Type TyName uni ann -> Type TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source # error :: ann -> Type TyName uni ann -> Term name uni fun ann Source # constr :: ann -> Type TyName uni ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann Source # kase :: ann -> Type TyName uni ann -> Term name uni fun ann -> [Term name uni fun ann] -> Term name uni fun ann Source # termLet :: ann -> TermDef (Term name uni fun) TyName name uni ann -> Term name uni fun ann -> Term name uni fun ann Source # typeLet :: ann -> TypeDef TyName uni ann -> Term name uni fun ann -> Term name uni fun ann Source #
TermLike (Term tyname name uni fun) tyname name uni fun Source #
Instance details Defined in PlutusCore.MkPlc Methods var :: ann -> name -> Term tyname name uni fun ann Source # tyAbs :: ann -> tyname -> Kind ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # lamAbs :: ann -> name -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # apply :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # constant :: ann -> Some (ValueOf uni) -> Term tyname name uni fun ann Source # builtin :: ann -> fun -> Term tyname name uni fun ann Source # tyInst :: ann -> Term tyname name uni fun ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # unwrap :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # iWrap :: ann -> Type tyname uni ann -> Type tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # error :: ann -> Type tyname uni ann -> Term tyname name uni fun ann Source # constr :: ann -> Type tyname uni ann -> Word64 -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann Source # kase :: ann -> Type tyname uni ann -> Term tyname name uni fun ann -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann Source # termLet :: ann -> TermDef (Term tyname name uni fun) tyname name uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source # typeLet :: ann -> TypeDef tyname uni ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann Source #

type family UniOf a :: Type -> Type Source #

Extract the universe from a type.

Instances

Instances details

type UniOf (Opaque val rep) Source #
Instance details Defined in PlutusCore.Builtin.Polymorphism type UniOf (Opaque val rep) = UniOf val
type UniOf (SomeConstant uni rep) Source #
Instance details Defined in PlutusCore.Builtin.Polymorphism type UniOf (SomeConstant uni rep) = uni
type UniOf (CkValue uni fun) Source #
Instance details Defined in PlutusCore.Evaluation.Machine.Ck type UniOf (CkValue uni fun) = uni
type UniOf (CekValue uni fun ann) Source #
Instance details Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal type UniOf (CekValue uni fun ann) = uni
type UniOf (Term name uni fun ann) Source #
Instance details Defined in UntypedPlutusCore.Core.Type type UniOf (Term name uni fun ann) = uni
type UniOf (Term tyname name uni fun ann) Source #
Instance details Defined in PlutusCore.Core.Type type UniOf (Term tyname name uni fun ann) = uni

type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x) Source #

Specifies that the given type is a built-in one and can be embedded into a Kind.

type HasTermLevel uni = Includes uni Source #

Specifies that the given type is a built-in one and its values can be embedded into a Term.

type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x) Source #

The product of HasTypeLevel and HasTermLevel.

mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann Source #

Embed a type (given its explicit type tag) into a PLC type.

mkTyBuiltin :: forall a (x :: a) uni ann tyname. uni `HasTypeLevel` x => ann -> Type tyname uni ann Source #

Convert a Haskell representation of a possibly 0-ary application of a built-in type to arbitrary types implementing KnownTypeAst.

mkConstantOf :: forall a uni fun term tyname name ann. TermLike term tyname name uni fun => ann -> uni (Esc a) -> a -> term ann Source #

Embed a Haskell value (given its explicit type tag) into a PLC term.

mkConstant :: forall a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `HasTermLevel` a) => ann -> a -> term ann Source #

Embed a Haskell value (provided its type is in the universe) into a PLC term.

data VarDecl tyname name uni ann Source #

A "variable declaration", i.e. a name and a type for a variable.

Constructors

VarDecl
Fields _varDeclAnn :: ann _varDeclName :: name _varDeclType :: Type tyname uni ann

Instances

Instances details

(PrettyReadableBy configName tyname, PrettyReadableBy configName name, PrettyUni uni) => PrettyBy (PrettyConfigReadable configName) (VarDecl tyname name uni ann) Source #
Instance details Defined in PlutusCore.Core.Instance.Pretty.Readable Methods prettyBy :: PrettyConfigReadable configName -> VarDecl tyname name uni ann -> Doc ann0 # prettyListBy :: PrettyConfigReadable configName -> [VarDecl tyname name uni ann] -> Doc ann0 #
Functor (VarDecl tyname name uni) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> VarDecl tyname name uni a -> VarDecl tyname name uni b Source # (<$) :: a -> VarDecl tyname name uni b -> VarDecl tyname name uni a Source #
Generic (VarDecl tyname name uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (VarDecl tyname name uni ann) :: Type -> Type Source # Methods from :: VarDecl tyname name uni ann -> Rep (VarDecl tyname name uni ann) x Source # to :: Rep (VarDecl tyname name uni ann) x -> VarDecl tyname name uni ann Source #
(GShow uni, Show ann, Show name, Show tyname) => Show (VarDecl tyname name uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> VarDecl tyname name uni ann -> ShowS Source # show :: VarDecl tyname name uni ann -> String Source # showList :: [VarDecl tyname name uni ann] -> ShowS Source #
(Closed uni, Flat ann, Flat tyname, Flat name) => Flat (VarDecl tyname name uni ann)
Instance details Defined in PlutusCore.Flat Methods encode :: VarDecl tyname name uni ann -> Encoding decode :: Get (VarDecl tyname name uni ann) size :: VarDecl tyname name uni ann -> NumBits -> NumBits
HasUnique name TermUnique => HasUnique (VarDecl tyname name uni ann) TermUnique Source #
Instance details Defined in PlutusCore.Core.Type Methods unique :: Lens' (VarDecl tyname name uni ann) TermUnique Source #
type Rep (VarDecl tyname name uni ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (VarDecl tyname name uni ann) = D1 ('MetaData "VarDecl" "PlutusCore.Core.Type" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "VarDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_varDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_varDeclName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name) :: S1 ('MetaSel ('Just "_varDeclType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type tyname uni ann)))))

data TyVarDecl tyname ann Source #

A "type variable declaration", i.e. a name and a kind for a type variable.

Constructors

TyVarDecl
Fields _tyVarDeclAnn :: ann _tyVarDeclName :: tyname _tyVarDeclKind :: Kind ann

Instances

Instances details

Functor (TyVarDecl tyname) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> TyVarDecl tyname a -> TyVarDecl tyname b Source # (<$) :: a -> TyVarDecl tyname b -> TyVarDecl tyname a Source #
PrettyReadableBy configName tyname => PrettyBy (PrettyConfigReadable configName) (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Instance.Pretty.Readable Methods prettyBy :: PrettyConfigReadable configName -> TyVarDecl tyname ann -> Doc ann0 # prettyListBy :: PrettyConfigReadable configName -> [TyVarDecl tyname ann] -> Doc ann0 #
Generic (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (TyVarDecl tyname ann) :: Type -> Type Source # Methods from :: TyVarDecl tyname ann -> Rep (TyVarDecl tyname ann) x Source # to :: Rep (TyVarDecl tyname ann) x -> TyVarDecl tyname ann Source #
(Show ann, Show tyname) => Show (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> TyVarDecl tyname ann -> ShowS Source # show :: TyVarDecl tyname ann -> String Source # showList :: [TyVarDecl tyname ann] -> ShowS Source #
(Flat ann, Flat tyname) => Flat (TyVarDecl tyname ann)
Instance details Defined in PlutusCore.Flat Methods encode :: TyVarDecl tyname ann -> Encoding decode :: Get (TyVarDecl tyname ann) size :: TyVarDecl tyname ann -> NumBits -> NumBits
HasUnique tyname TypeUnique => HasUnique (TyVarDecl tyname ann) TypeUnique Source #
Instance details Defined in PlutusCore.Core.Type Methods unique :: Lens' (TyVarDecl tyname ann) TypeUnique Source #
type Rep (TyVarDecl tyname ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (TyVarDecl tyname ann) = D1 ('MetaData "TyVarDecl" "PlutusCore.Core.Type" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "TyVarDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tyVarDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_tyVarDeclName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 tyname) :: S1 ('MetaSel ('Just "_tyVarDeclKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Kind ann)))))

data TyDecl tyname uni ann Source #

A "type declaration", i.e. a kind for a type.

Constructors

TyDecl
Fields _tyDeclAnn :: ann _tyDeclType :: Type tyname uni ann _tyDeclKind :: Kind ann

Instances

Instances details

Functor (TyDecl tyname uni) Source #
Instance details Defined in PlutusCore.Core.Type Methods fmap :: (a -> b) -> TyDecl tyname uni a -> TyDecl tyname uni b Source # (<$) :: a -> TyDecl tyname uni b -> TyDecl tyname uni a Source #
Generic (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Associated Types type Rep (TyDecl tyname uni ann) :: Type -> Type Source # Methods from :: TyDecl tyname uni ann -> Rep (TyDecl tyname uni ann) x Source # to :: Rep (TyDecl tyname uni ann) x -> TyDecl tyname uni ann Source #
(GShow uni, Show ann, Show tyname) => Show (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type Methods showsPrec :: Int -> TyDecl tyname uni ann -> ShowS Source # show :: TyDecl tyname uni ann -> String Source # showList :: [TyDecl tyname uni ann] -> ShowS Source #
type Rep (TyDecl tyname uni ann) Source #
Instance details Defined in PlutusCore.Core.Type type Rep (TyDecl tyname uni ann) = D1 ('MetaData "TyDecl" "PlutusCore.Core.Type" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "TyDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tyDeclAnn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ann) :: (S1 ('MetaSel ('Just "_tyDeclType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type tyname uni ann)) :: S1 ('MetaSel ('Just "_tyDeclKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Kind ann)))))

mkVar :: TermLike term tyname name uni fun => ann -> VarDecl tyname name uni ann -> term ann Source #

Make a Var referencing the given VarDecl.

mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann Source #

Make a TyVar referencing the given TyVarDecl.

tyDeclVar :: TyVarDecl tyname ann -> TyDecl tyname uni ann Source #

data Def var val Source #

A definition. Pretty much just a pair with more descriptive names.

Constructors

Def
Fields defVar :: var defVal :: val

Instances

Instances details

Generic (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Associated Types type Rep (Def var val) :: Type -> Type Source # Methods from :: Def var val -> Rep (Def var val) x Source # to :: Rep (Def var val) x -> Def var val Source #
(Show var, Show val) => Show (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods showsPrec :: Int -> Def var val -> ShowS Source # show :: Def var val -> String Source # showList :: [Def var val] -> ShowS Source #
(Eq var, Eq val) => Eq (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods (==) :: Def var val -> Def var val -> Bool Source # (/=) :: Def var val -> Def var val -> Bool Source #
(Ord var, Ord val) => Ord (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc Methods compare :: Def var val -> Def var val -> Ordering Source # (<) :: Def var val -> Def var val -> Bool Source # (<=) :: Def var val -> Def var val -> Bool Source # (>) :: Def var val -> Def var val -> Bool Source # (>=) :: Def var val -> Def var val -> Bool Source # max :: Def var val -> Def var val -> Def var val Source # min :: Def var val -> Def var val -> Def var val Source #
type Rep (Def var val) Source #
Instance details Defined in PlutusCore.MkPlc type Rep (Def var val) = D1 ('MetaData "Def" "PlutusCore.MkPlc" "plutus-core-1.36.0.0-7ehJj5tIPqoJIiiivXkX9N" 'False) (C1 ('MetaCons "Def" 'PrefixI 'True) (S1 ('MetaSel ('Just "defVar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 var) :*: S1 ('MetaSel ('Just "defVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 val)))

embedTerm :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann Source #

type TermDef term tyname name uni ann = Def (VarDecl tyname name uni ann) (term ann) Source #

A term definition as a variable.

type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann) Source #

A type definition as a type variable.

data FunctionType tyname uni ann Source #

The type of a PLC function.

Constructors

FunctionType
Fields _functionTypeAnn :: ann An annotation. _functionTypeDom :: Type tyname uni ann The domain of a function. _functionTypeCod :: Type tyname uni ann The codomain of the function.

data FunctionDef term tyname name uni fun ann Source #

A PLC function.

Constructors

FunctionDef
Fields _functionDefAnn :: ann An annotation. _functionDefName :: name The name of a function. _functionDefType :: FunctionType tyname uni ann The type of the function. _functionDefTerm :: term ann The definition of the function.

functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann Source #

Convert a FunctionType to the corresponding Kind.

functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann Source #

Get the type of a FunctionDef.

functionDefVarDecl :: FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni ann Source #

Convert a FunctionDef to a VarDecl. I.e. ignore the actual term.

mkFunctionDef :: ann -> name -> Type tyname uni ann -> term ann -> Maybe (FunctionDef term tyname name uni fun ann) Source #

Make a FunctionDef. Return Nothing if the provided type is not functional.

mkImmediateLamAbs Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> TermDef term tyname name uni ann
-> term ann	The body of the let, possibly referencing the name.
-> term ann

Make a "let-binding" for a term as an immediately applied lambda abstraction.

mkImmediateTyAbs Source #

Arguments

:: TermLike term tyname name uni fun
=> ann
-> TypeDef tyname uni ann
-> term ann	The body of the let, possibly referencing the name.
-> term ann

Make a "let-binding" for a type as an immediately instantiated type abstraction. Note: the body must be a value.

mkIterTyForall :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Universally quantify a list of names.

mkIterTyLam :: [TyVarDecl tyname ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Lambda abstract a list of names.

mkIterApp :: TermLike term tyname name uni fun => term ann -> [(ann, term ann)] -> term ann Source #

Make an iterated application. Each apply node uses the annotation associated with the corresponding argument.

mkIterAppNoAnn Source #

Arguments

:: TermLike term tyname name uni fun
=> term ()	f
-> [term ()]	[ x0 ... xn ]
-> term ()	[f x0 ... xn ]

Make an iterated application with no annotation.

(@@) Source #

Arguments

:: TermLike term tyname name uni fun
=> term ()	f
-> [term ()]	[ x0 ... xn ]
-> term ()	[f x0 ... xn ]

An infix synonym for mkIterAppNoAnn

mkIterTyFun :: ann -> [Type tyname uni ann] -> Type tyname uni ann -> Type tyname uni ann Source #

Make an iterated function type.

mkIterLamAbs :: TermLike term tyname name uni fun => [VarDecl tyname name uni ann] -> term ann -> term ann Source #

Lambda abstract a list of names.

mkIterInst Source #

Arguments

:: TermLike term tyname name uni fun
=> term ann	a
-> [(ann, Type tyname uni ann)]	[ x0 ... xn ]
-> term ann	{ a x0 ... xn }

Make an iterated instantiation. Each tyInst node uses the annotation associated with the corresponding argument.

mkIterInstNoAnn Source #

Arguments

:: TermLike term tyname name uni fun
=> term ()	a
-> [Type tyname uni ()]	[ x0 ... xn ]
-> term ()	{ a x0 ... xn }

Make an iterated instantiation with no annotation.

mkIterTyAbs :: TermLike term tyname name uni fun => [TyVarDecl tyname ann] -> term ann -> term ann Source #

Type abstract a list of names.

mkIterTyApp Source #

Arguments

:: Type tyname uni ann	f
-> [(ann, Type tyname uni ann)]	[ x0 ... xn ]
-> Type tyname uni ann	[ f x0 ... xn ]

Make an iterated type application. Each TyApp node uses the annotation associated with the corresponding argument.

mkIterTyAppNoAnn Source #

Arguments

:: Type tyname uni ()	f
-> [Type tyname uni ()]	[ x0 ... xn ]
-> Type tyname uni ()	[ f x0 ... xn ]

Make an iterated type application with no annotation.

mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann Source #

Make an iterated function kind.

mkFreshTermLet Source #

Arguments

:: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a)
=> Type tyname uni a	the type of binding
-> t a	the term bound to the fresh variable
-> m (t a, t a -> t a)	the fresh Var and a function that takes an "in" term to construct the Let

A helper to create a single, fresh strict binding; It returns the fresh bound Variable and a function `Term -> Term`, expecting an "in-Term" to form a let-expression.