plutus-core-0.1.0.0: Language library for Plutus Core
Safe HaskellNone
LanguageHaskell2010

PlutusCore.DeBruijn

Description

Support for using de Bruijn indices for term and type names.

Synopsis

Documentation

newtype Index Source #

A relative index used for de Bruijn identifiers.

Constructors

Index Word64 

Instances

Instances details
Enum Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Eq Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

(==) :: Index -> Index -> Bool Source #

(/=) :: Index -> Index -> Bool Source #

Integral Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Num Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Ord Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Real Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep Index :: Type -> Type Source #

Methods

from :: Index -> Rep Index x Source #

to :: Rep Index x -> Index Source #

NFData Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: Index -> () Source #

Flat Index Source # 
Instance details

Defined in PlutusCore.Flat

Pretty Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

pretty :: Index -> Doc ann Source #

prettyList :: [Index] -> Doc ann Source #

type Rep Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep Index = D1 ('MetaData "Index" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'True) (C1 ('MetaCons "Index" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64)))

newtype DeBruijn Source #

A term name as a de Bruijn index, without the name string.

Constructors

DeBruijn 

Fields

Instances

Instances details
Eq DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep DeBruijn :: Type -> Type Source #

NFData DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: DeBruijn -> () Source #

Flat DeBruijn Source # 
Instance details

Defined in PlutusCore.Flat

HasIndex DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasPrettyConfigName config => PrettyBy config DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyBy :: config -> DeBruijn -> Doc ann Source #

prettyListBy :: config -> [DeBruijn] -> Doc ann Source #

Flat (Binder DeBruijn) Source # 
Instance details

Defined in PlutusCore.Flat

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term DeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

(==) :: Term DeBruijn uni fun ann -> Term DeBruijn uni fun ann -> Bool Source #

(/=) :: Term DeBruijn uni fun ann -> Term DeBruijn uni fun ann -> Bool Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term TyDeBruijn DeBruijn uni fun ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

Methods

(==) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source #

(/=) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source #

type Rep DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep DeBruijn = D1 ('MetaData "DeBruijn" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'True) (C1 ('MetaCons "DeBruijn" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbnIndex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Index)))

data NamedDeBruijn Source #

A term name as a de Bruijn index.

Constructors

NamedDeBruijn 

Instances

Instances details
Eq NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep NamedDeBruijn :: Type -> Type Source #

NFData NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: NamedDeBruijn -> () Source #

Flat NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.Flat

HasIndex NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasPrettyConfigName config => PrettyBy config NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyBy :: config -> NamedDeBruijn -> Doc ann Source #

prettyListBy :: config -> [NamedDeBruijn] -> Doc ann Source #

Flat (Binder NamedDeBruijn) Source # 
Instance details

Defined in PlutusCore.Flat

PrettyUni uni fun => MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) Source # 
Instance details

Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal

Methods

throwError :: CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a Source #

catchError :: CekM uni fun s a -> (CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a) -> CekM uni fun s a Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term NamedDeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

(==) :: Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann -> Bool Source #

(/=) :: Term NamedDeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann -> Bool Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

type Rep NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep NamedDeBruijn = D1 ('MetaData "NamedDeBruijn" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'False) (C1 ('MetaCons "NamedDeBruijn" 'PrefixI 'True) (S1 ('MetaSel ('Just "ndbnString") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Just "ndbnIndex") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Index)))

newtype TyDeBruijn Source #

A type name as a de Bruijn index, without the name string.

Constructors

TyDeBruijn DeBruijn 

Instances

Instances details
Eq TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep TyDeBruijn :: Type -> Type Source #

NFData TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: TyDeBruijn -> () Source #

Flat TyDeBruijn Source # 
Instance details

Defined in PlutusCore.Flat

Wrapped TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Unwrapped TyDeBruijn Source #

HasIndex TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasPrettyConfigName config => PrettyBy config TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyBy :: config -> TyDeBruijn -> Doc ann Source #

prettyListBy :: config -> [TyDeBruijn] -> Doc ann Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq ann) => Eq (Type TyDeBruijn uni ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

Methods

(==) :: Type TyDeBruijn uni ann -> Type TyDeBruijn uni ann -> Bool Source #

(/=) :: Type TyDeBruijn uni ann -> Type TyDeBruijn uni ann -> Bool Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term TyDeBruijn DeBruijn uni fun ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

Methods

(==) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source #

(/=) :: Term TyDeBruijn DeBruijn uni fun ann -> Term TyDeBruijn DeBruijn uni fun ann -> Bool Source #

type Rep TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep TyDeBruijn = D1 ('MetaData "TyDeBruijn" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'True) (C1 ('MetaCons "TyDeBruijn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeBruijn)))
type Unwrapped TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Unwrapped TyDeBruijn = GUnwrapped (Rep TyDeBruijn)

newtype NamedTyDeBruijn Source #

A type name as a de Bruijn index.

Instances

Instances details
Eq NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep NamedTyDeBruijn :: Type -> Type Source #

NFData NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: NamedTyDeBruijn -> () Source #

Flat NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.Flat

Wrapped NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Unwrapped NamedTyDeBruijn Source #

HasIndex NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasPrettyConfigName config => PrettyBy config NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyBy :: config -> NamedTyDeBruijn -> Doc ann Source #

prettyListBy :: config -> [NamedTyDeBruijn] -> Doc ann Source #

Flat (Binder NamedTyDeBruijn) Source # 
Instance details

Defined in PlutusCore.Flat

(GEq uni, Closed uni, Everywhere uni Eq, Eq ann) => Eq (Type NamedTyDeBruijn uni ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

Methods

(==) :: Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann -> Bool Source #

(/=) :: Type NamedTyDeBruijn uni ann -> Type NamedTyDeBruijn uni ann -> Bool Source #

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) => Eq (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Eq

type Rep NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep NamedTyDeBruijn = D1 ('MetaData "NamedTyDeBruijn" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'True) (C1 ('MetaCons "NamedTyDeBruijn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamedDeBruijn)))
type Unwrapped NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

data FreeVariableError Source #

We cannot do a correct translation to or from de Bruijn indices if the program is not well-scoped. So we throw an error in such a case.

Instances

Instances details
Eq FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Ord FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep FreeVariableError :: Type -> Type Source #

Exception FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnf :: FreeVariableError -> () Source #

Pretty FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasErrorCode FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

AsFreeVariableError FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep FreeVariableError = D1 ('MetaData "FreeVariableError" "PlutusCore.DeBruijn.Internal" "plutus-core-0.1.0.0-75cTOscXcmAHq1cwUst1Y0" 'False) (C1 ('MetaCons "FreeUnique" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Unique)) :+: C1 ('MetaCons "FreeIndex" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Index)))

deBruijnTy :: (AsFreeVariableError e, MonadError e m) => Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann) Source #

Convert a Type with TyNames into a Type with NamedTyDeBruijns. Will throw an error if a free variable is encountered.

deBruijnTerm :: (AsFreeVariableError e, MonadError e m) => Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source #

Convert a Term with TyNames and Names into a Term with NamedTyDeBruijns and NamedDeBruijns. Will throw an error if a free variable is encountered.

unDeBruijnTy :: (MonadQuote m, AsFreeVariableError e, MonadError e m) => Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann) Source #

Convert a Type with NamedTyDeBruijns into a Type with TyNames. Will throw an error if a free variable is encountered.

unDeBruijnTerm :: (MonadQuote m, AsFreeVariableError e, MonadError e m) => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) Source #

Convert a Term with NamedTyDeBruijns and NamedDeBruijns into a Term with TyNames and Names. Will throw an error if a free variable is encountered.

unsafe api, use with care

deBruijnTyWith :: Monad m => (Unique -> ReaderT Levels m Index) -> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann) Source #

deBruijnTermWith :: Monad m => (Unique -> ReaderT Levels m Index) -> Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source #

unDeBruijnTyWith :: MonadQuote m => (Index -> ReaderT Levels m Unique) -> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann) Source #

Takes a "handler" function to execute when encountering free variables.

unDeBruijnTermWith :: MonadQuote m => (Index -> ReaderT Levels m Unique) -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) Source #

Takes a "handler" function to execute when encountering free variables.

freeIndexAsConsistentLevel :: (MonadReader Levels m, MonadState (Map Level Unique) m, MonadQuote m) => Index -> m Unique Source #

A different implementation of a handler, where "free" debruijn indices do not throw an error but are instead gracefully converted to fresh uniques. These generated uniques remain free; i.e. if the original term was open, it will remain open after applying this handler. These generated free uniques are consistent across the open term (by using a state cache).

deBruijnInitIndex :: Index Source #

The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad