plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
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.

FIXME: downside of using newtype+Num instead of type-synonym is that `-Woverflowed-literals` does not work, e.g.: `DeBruijn (-1)` has no warning. To trigger the warning you have to bypass the Num and write `DeBruijn (Index -1)`. This can be revisited when we implement PLT-1053.

Constructors

Index Word64 

Instances

Instances details
Enum Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep IndexTypeType Source #

Methods

fromIndexRep Index x Source #

toRep Index x → Index Source #

Num Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Read Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Integral 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

NFData Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfIndex → () Source #

Flat Index 
Instance details

Defined in PlutusCore.Flat

Methods

encodeIndex → Encoding

decode ∷ Get Index

sizeIndex → NumBits → NumBits

Eq Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

(==)IndexIndexBool Source #

(/=)IndexIndexBool Source #

Ord Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

compareIndexIndexOrdering Source #

(<)IndexIndexBool Source #

(<=)IndexIndexBool Source #

(>)IndexIndexBool Source #

(>=)IndexIndexBool Source #

maxIndexIndexIndex Source #

minIndexIndexIndex Source #

Hashable Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

hashWithSaltIntIndexInt

hashIndexInt

Pretty Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyIndexDoc ann #

prettyList ∷ [Index] → Doc ann #

type Rep Index Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep Index = D1 ('MetaData "Index" "PlutusCore.DeBruijn.Internal" "plutus-core-1.30.0.0-inplace" 'True) (C1 ('MetaCons "Index" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64)))

newtype Level Source #

An absolute level in the program.

Constructors

Level Integer 

Instances

Instances details
Enum Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Num Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Integral Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Real Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Eq Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

(==)LevelLevelBool Source #

(/=)LevelLevelBool Source #

Ord Level Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

compareLevelLevelOrdering Source #

(<)LevelLevelBool Source #

(<=)LevelLevelBool Source #

(>)LevelLevelBool Source #

(>=)LevelLevelBool Source #

maxLevelLevelLevel Source #

minLevelLevelLevel Source #

data LevelInfo Source #

During visiting the AST we hold a reader "state" of current level and a current scoping (levelMapping). Invariant-A: the current level is positive and greater than all levels in the levelMapping. Invariant-B: only positive levels are stored in the levelMapping.

Constructors

LevelInfo 

Fields

newtype DeBruijn Source #

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

Constructors

DeBruijn 

Fields

Instances

Instances details
Generic DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep DeBruijnTypeType Source #

Show DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfDeBruijn → () Source #

Flat DeBruijn 
Instance details

Defined in PlutusCore.Flat

Methods

encodeDeBruijn → Encoding

decode ∷ Get DeBruijn

sizeDeBruijn → NumBits → NumBits

Eq DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Hashable DeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

hashWithSaltIntDeBruijnInt

hashDeBruijnInt

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 → DeBruijnDoc ann Source #

prettyListBy ∷ config → [DeBruijn] → Doc ann Source #

Flat (Binder DeBruijn) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeBinder DeBruijn → Encoding

decode ∷ Get (Binder DeBruijn)

sizeBinder DeBruijn → NumBits → NumBits

(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 #

HashableTermConstraints uni fun ann ⇒ Hashable (Term DeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

hashWithSaltIntTerm DeBruijn uni fun ann → Int

hashTerm DeBruijn uni fun ann → Int

(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-1.30.0.0-inplace" '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 

Fields

Instances

Instances details
Generic NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep NamedDeBruijnTypeType Source #

Read NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Show NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfNamedDeBruijn → () Source #

Flat NamedDeBruijn 
Instance details

Defined in PlutusCore.Flat

Methods

encodeNamedDeBruijn → Encoding

decode ∷ Get NamedDeBruijn

sizeNamedDeBruijn → NumBits → NumBits

Eq NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Hashable NamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

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 → NamedDeBruijnDoc ann Source #

prettyListBy ∷ config → [NamedDeBruijn] → Doc ann Source #

Flat (Binder NamedDeBruijn) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeBinder NamedDeBruijn → Encoding

decode ∷ Get (Binder NamedDeBruijn)

sizeBinder NamedDeBruijn → NumBits → NumBits

ThrowableBuiltins uni fun ⇒ MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) 
Instance details

Defined in UntypedPlutusCore.Evaluation.Machine.Cek.Internal

Methods

throwErrorCekEvaluationException NamedDeBruijn uni fun → CekM uni fun s a

catchErrorCekM uni fun s a → (CekEvaluationException NamedDeBruijn uni fun → CekM uni fun s a) → CekM uni fun s a

(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 #

HashableTermConstraints uni fun ann ⇒ Hashable (Term NamedDeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

hashWithSaltIntTerm NamedDeBruijn uni fun ann → Int

hashTerm NamedDeBruijn uni fun ann → Int

(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-1.30.0.0-inplace" 'False) (C1 ('MetaCons "NamedDeBruijn" 'PrefixI 'True) (S1 ('MetaSel ('Just "ndbnString") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text) :*: S1 ('MetaSel ('Just "ndbnIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Index)))

data FakeNamedDeBruijn Source #

A wrapper around NamedDeBruijn that *must* hold the invariant of name=fakeName.

We do not export the FakeNamedDeBruijn constructor: the projection `FND->ND` is safe but injection `ND->FND` is unsafe, thus they are not isomorphic.

See Note [Why newtype FakeNamedDeBruijn]

Instances

Instances details
Show FakeNamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData FakeNamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfFakeNamedDeBruijn → () Source #

Flat FakeNamedDeBruijn 
Instance details

Defined in PlutusCore.Flat

Methods

encodeFakeNamedDeBruijn → Encoding

decode ∷ Get FakeNamedDeBruijn

sizeFakeNamedDeBruijn → NumBits → NumBits

Eq FakeNamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Hashable FakeNamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

HasPrettyConfigName config ⇒ PrettyBy config FakeNamedDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyBy ∷ config → FakeNamedDeBruijnDoc ann Source #

prettyListBy ∷ config → [FakeNamedDeBruijn] → Doc ann Source #

Flat (Binder FakeNamedDeBruijn) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeBinder FakeNamedDeBruijn → Encoding

decode ∷ Get (Binder FakeNamedDeBruijn)

sizeBinder FakeNamedDeBruijn → NumBits → NumBits

(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) ⇒ Eq (Term FakeNamedDeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

(==)Term FakeNamedDeBruijn uni fun ann → Term FakeNamedDeBruijn uni fun ann → Bool Source #

(/=)Term FakeNamedDeBruijn uni fun ann → Term FakeNamedDeBruijn uni fun ann → Bool Source #

HashableTermConstraints uni fun ann ⇒ Hashable (Term FakeNamedDeBruijn uni fun ann) Source # 
Instance details

Defined in UntypedPlutusCore.Core.Instance.Eq

Methods

hashWithSaltIntTerm FakeNamedDeBruijn uni fun ann → Int

hashTerm FakeNamedDeBruijn uni fun ann → Int

newtype TyDeBruijn Source #

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

Constructors

TyDeBruijn DeBruijn 

Instances

Instances details
Generic TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep TyDeBruijnTypeType Source #

Show TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfTyDeBruijn → () Source #

Flat TyDeBruijn 
Instance details

Defined in PlutusCore.Flat

Methods

encodeTyDeBruijn → Encoding

decode ∷ Get TyDeBruijn

sizeTyDeBruijn → NumBits → NumBits

Eq TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Wrapped TyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Unwrapped TyDeBruijn

Methods

_Wrapped' ∷ Iso' TyDeBruijn (Unwrapped TyDeBruijn)

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 → TyDeBruijnDoc 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-1.30.0.0-inplace" 'True) (C1 ('MetaCons "TyDeBruijn" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe 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
Generic NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep NamedTyDeBruijnTypeType Source #

Show NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfNamedTyDeBruijn → () Source #

Flat NamedTyDeBruijn 
Instance details

Defined in PlutusCore.Flat

Methods

encodeNamedTyDeBruijn → Encoding

decode ∷ Get NamedTyDeBruijn

sizeNamedTyDeBruijn → NumBits → NumBits

Eq NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Wrapped NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Unwrapped NamedTyDeBruijn

Methods

_Wrapped' ∷ Iso' NamedTyDeBruijn (Unwrapped NamedTyDeBruijn)

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 → NamedTyDeBruijnDoc ann Source #

prettyListBy ∷ config → [NamedTyDeBruijn] → Doc ann Source #

Flat (Binder NamedTyDeBruijn) 
Instance details

Defined in PlutusCore.Flat

Methods

encodeBinder NamedTyDeBruijn → Encoding

decode ∷ Get (Binder NamedTyDeBruijn)

sizeBinder NamedTyDeBruijn → NumBits → NumBits

(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-1.30.0.0-inplace" 'True) (C1 ('MetaCons "NamedTyDeBruijn" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NamedDeBruijn)))
type Unwrapped NamedTyDeBruijn Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Unwrapped NamedTyDeBruijn = GUnwrapped (Rep NamedTyDeBruijn)

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.

Constructors

FreeUnique !Unique 
FreeIndex !Index 

Instances

Instances details
Exception FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Generic FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Associated Types

type Rep FreeVariableErrorTypeType Source #

Show FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

NFData FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

rnfFreeVariableError → () Source #

Eq FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Ord FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

AsFreeVariableError FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Pretty FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

Methods

prettyFreeVariableErrorDoc ann #

prettyList ∷ [FreeVariableError] → Doc ann #

type Rep FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

type Rep FreeVariableError = D1 ('MetaData "FreeVariableError" "PlutusCore.DeBruijn.Internal" "plutus-core-1.30.0.0-inplace" 'False) (C1 ('MetaCons "FreeUnique" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Unique)) :+: C1 ('MetaCons "FreeIndex" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Index)))

class AsFreeVariableError r where Source #

Minimal complete definition

_FreeVariableError

Instances

Instances details
AsFreeVariableError FreeVariableError Source # 
Instance details

Defined in PlutusCore.DeBruijn.Internal

AsFreeVariableError (Error uni fun ann) Source # 
Instance details

Defined in PlutusCore.Error

Methods

_FreeVariableError ∷ Prism' (Error uni fun ann) FreeVariableError Source #

_FreeUnique ∷ Prism' (Error uni fun ann) Unique Source #

_FreeIndex ∷ Prism' (Error uni fun ann) Index Source #

deBruijnTy ∷ (AsFreeVariableError e, MonadError e m) ⇒ Type TyName uni ann → m (Type NamedTyDeBruijn uni ann) Source #

Convert a Kind with TyNames into a Kind 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 Kind with NamedTyDeBruijns into a Kind 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

deBruijnTyWithMonad m ⇒ (Unique → ReaderT LevelInfo m Index) → Type TyName uni ann → m (Type NamedTyDeBruijn uni ann) Source #

deBruijnTermWithMonad m ⇒ (Unique → ReaderT LevelInfo m Index) → Term TyName Name uni fun ann → m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source #

unDeBruijnTyWithMonadQuote m ⇒ (Index → ReaderT LevelInfo m Unique) → Type NamedTyDeBruijn uni ann → m (Type TyName uni ann) Source #

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

unDeBruijnTermWithMonadQuote m ⇒ (Index → ReaderT LevelInfo 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 LevelInfo 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).

deBruijnInitIndexIndex Source #

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