| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore.DeBruijn.Internal
Description
Support for using de Bruijn indices for term and type names.
Synopsis
- newtype Index = Index Word64
- class HasIndex a where
- newtype DeBruijn = DeBruijn {}
- data NamedDeBruijn = NamedDeBruijn {
- ndbnString :: !Text
- ndbnIndex :: !Index
- newtype FakeNamedDeBruijn = FakeNamedDeBruijn {}
- newtype TyDeBruijn = TyDeBruijn DeBruijn
- newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
- data FreeVariableError
- = FreeUnique !Unique
- | FreeIndex !Index
- newtype Level = Level Integer
- data LevelInfo = LevelInfo {
- currentLevel :: Level
- levelMapping :: Bimap Unique Level
- declareUnique :: (MonadReader LevelInfo m, HasUnique name unique) => name -> m a -> m a
- declareBinder :: (MonadReader LevelInfo m, MonadQuote m) => m a -> m a
- withScope :: MonadReader LevelInfo m => m a -> m a
- getIndex :: MonadReader LevelInfo m => Unique -> (Unique -> m Index) -> m Index
- getUnique :: MonadReader LevelInfo m => Index -> (Index -> m Unique) -> m Unique
- unNameDeBruijn :: NamedDeBruijn -> DeBruijn
- unNameTyDeBruijn :: NamedTyDeBruijn -> TyDeBruijn
- fakeNameDeBruijn :: DeBruijn -> NamedDeBruijn
- fakeTyNameDeBruijn :: TyDeBruijn -> NamedTyDeBruijn
- nameToDeBruijn :: MonadReader LevelInfo m => (Unique -> m Index) -> Name -> m NamedDeBruijn
- tyNameToDeBruijn :: MonadReader LevelInfo m => (Unique -> m Index) -> TyName -> m NamedTyDeBruijn
- deBruijnToName :: MonadReader LevelInfo m => (Index -> m Unique) -> NamedDeBruijn -> m Name
- deBruijnToTyName :: MonadReader LevelInfo m => (Index -> m Unique) -> NamedTyDeBruijn -> m TyName
- freeIndexThrow :: MonadError FreeVariableError m => Index -> m Unique
- freeIndexAsConsistentLevel :: (MonadReader LevelInfo m, MonadState (Map Level Unique) m, MonadQuote m) => Index -> m Unique
- freeUniqueThrow :: MonadError FreeVariableError m => Unique -> m Index
- runDeBruijnT :: ReaderT LevelInfo m a -> m a
- deBruijnInitIndex :: Index
- toFake :: DeBruijn -> FakeNamedDeBruijn
- fromFake :: FakeNamedDeBruijn -> DeBruijn
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
| Text) :*: S1 ('MetaSel ('Just "ndbnIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Index))) |
newtype 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]
Constructors
| FakeNamedDeBruijn | |
Fields | |
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
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
| |
declareUnique :: (MonadReader LevelInfo m, HasUnique name unique) => name -> m a -> m a #
Declare a name with a unique, recording the mapping to a Level.
declareBinder :: (MonadReader LevelInfo m, MonadQuote m) => m a -> m a #
Declares a new binder by assigning a fresh unique to the *current level*.
Maintains invariant-B of LevelInfo (that only positive levels are stored),
since current level is always positive (invariant-A).
See Note [DeBruijn indices of Binders]
withScope :: MonadReader LevelInfo m => m a -> m a #
Enter a scope, incrementing the current Level by one
Maintains invariant-A (that the current level is positive).
unNameDeBruijn :: NamedDeBruijn -> DeBruijn #
nameToDeBruijn :: MonadReader LevelInfo m => (Unique -> m Index) -> Name -> m NamedDeBruijn #
tyNameToDeBruijn :: MonadReader LevelInfo m => (Unique -> m Index) -> TyName -> m NamedTyDeBruijn #
deBruijnToName :: MonadReader LevelInfo m => (Index -> m Unique) -> NamedDeBruijn -> m Name #
deBruijnToTyName :: MonadReader LevelInfo m => (Index -> m Unique) -> NamedTyDeBruijn -> m TyName #
freeIndexThrow :: MonadError FreeVariableError m => Index -> m Unique #
The default handler of throwing an error upon encountering a free debruijn index.
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).
freeUniqueThrow :: MonadError FreeVariableError m => Unique -> m Index #
The default handler of throwing an error upon encountering a free name (unique).
runDeBruijnT :: ReaderT LevelInfo m a -> m a #
The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad
toFake :: DeBruijn -> FakeNamedDeBruijn #
fromFake :: FakeNamedDeBruijn -> DeBruijn #