| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore.DeBruijn
Contents
Description
Support for using de Bruijn indices for term and type names.
Synopsis
}- = FreeUnique !Unique
- | FreeIndex !Index
Documentation
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. Tracked by: https://github.com/IntersectMBO/plutus-private/issues/1552
Instances
| NumBits # | |
| Pretty Index # | |
Defined in PlutusCore.DeBruijn.Internal | |
| type Rep Index # | |
Defined in PlutusCore.DeBruijn.Internal | |
An absolute level in the program.
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
| |
Instances
| HasIndex DeBruijn # | |
| HasIndex NamedDeBruijn # | |
Defined in PlutusCore.DeBruijn.Internal Methods | |
| HasIndex NamedTyDeBruijn # | |
Defined in PlutusCore.DeBruijn.Internal Methods | |
| HasIndex TyDeBruijn # | |
Defined in PlutusCore.DeBruijn.Internal Methods index :: Lens' TyDeBruijn Index # | |
A term name as a de Bruijn index, without the name string.
Instances
| Generic DeBruijn # | |
Defined in PlutusCore.DeBruijn.Internal Associated Types type Text) :*: S1 ('MetaSel ('Just "ndbnIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Index))) | |
data FakeNamedDeBruijn #
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
data FreeVariableError #
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
unNameDeBruijn :: NamedDeBruijn -> DeBruijn #
deBruijnTy :: MonadError FreeVariableError m => Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann) #
Convert a Kind with TyNames into a Kind with NamedTyDeBruijns.
Will throw an error if a free variable is encountered.
deBruijnTerm :: MonadError FreeVariableError m => Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) #
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, MonadError FreeVariableError m) => Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann) #
Convert a Kind with NamedTyDeBruijns into a Kind with TyNames.
Will throw an error if a free variable is encountered.
unDeBruijnTerm :: (MonadQuote m, MonadError FreeVariableError m) => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) #
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 LevelInfo m Index) -> Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann) #
deBruijnTermWith :: Monad m => (Unique -> ReaderT LevelInfo m Index) -> Term TyName Name uni fun ann -> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) #
unDeBruijnTyWith :: MonadQuote m => (Index -> ReaderT LevelInfo m Unique) -> Type NamedTyDeBruijn uni ann -> m (Type TyName uni ann) #
Takes a "handler" function to execute when encountering free variables.
unDeBruijnTermWith :: MonadQuote m => (Index -> ReaderT LevelInfo m Unique) -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m (Term TyName Name uni fun ann) #
Takes a "handler" function to execute when encountering free variables.
freeIndexAsConsistentLevel :: (MonadReader LevelInfo m, MonadState (Map Level Unique) m, MonadQuote m) => Index -> m Unique #
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).
The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad
fromFake :: FakeNamedDeBruijn -> DeBruijn #
toFake :: DeBruijn -> FakeNamedDeBruijn #