| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
PlutusCore.DeBruijn
Contents
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 NamedDeBruijn
- newtype TyDeBruijn = TyDeBruijn DeBruijn
- newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
- data FreeVariableError
-
class
AsFreeVariableError
r
where
- _FreeVariableError :: Prism' r FreeVariableError
- _FreeUnique :: Prism' r Unique
- _FreeIndex :: Prism' r Index
- unNameDeBruijn :: NamedDeBruijn -> DeBruijn
- unNameTyDeBruijn :: NamedTyDeBruijn -> TyDeBruijn
- fakeNameDeBruijn :: DeBruijn -> NamedDeBruijn
- deBruijnTy :: ( AsFreeVariableError e, MonadError e m) => Type TyName uni ann -> m ( Type NamedTyDeBruijn uni ann)
- deBruijnTerm :: ( AsFreeVariableError e, MonadError e m) => Term TyName Name uni fun ann -> m ( Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
- unDeBruijnTy :: ( MonadQuote m, AsFreeVariableError e, MonadError e m) => Type NamedTyDeBruijn uni ann -> m ( Type TyName uni ann)
- unDeBruijnTerm :: ( MonadQuote m, AsFreeVariableError e, MonadError e m) => Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m ( Term TyName Name uni fun ann)
- deBruijnTyWith :: Monad m => ( Unique -> ReaderT Levels m Index ) -> Type TyName uni ann -> m ( Type NamedTyDeBruijn uni ann)
- deBruijnTermWith :: Monad m => ( Unique -> ReaderT Levels m Index ) -> Term TyName Name uni fun ann -> m ( Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
- unDeBruijnTyWith :: MonadQuote m => ( Index -> ReaderT Levels m Unique ) -> Type NamedTyDeBruijn uni ann -> m ( Type TyName uni ann)
- unDeBruijnTermWith :: MonadQuote m => ( Index -> ReaderT Levels m Unique ) -> Term NamedTyDeBruijn NamedDeBruijn uni fun ann -> m ( Term TyName Name uni fun ann)
- freeIndexAsConsistentLevel :: ( MonadReader Levels m, MonadState ( Map Level Unique ) m, MonadQuote m) => Index -> m Unique
- deBruijnInitIndex :: Index
- fromFake :: FakeNamedDeBruijn -> DeBruijn
- toFake :: DeBruijn -> FakeNamedDeBruijn
Documentation
A relative index used for de Bruijn identifiers.
Instances
| Enum Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal Methods succ :: Index -> Index Source # pred :: Index -> Index Source # toEnum :: Int -> Index Source # fromEnum :: Index -> Int Source # enumFrom :: Index -> [ Index ] Source # enumFromThen :: Index -> Index -> [ Index ] Source # enumFromTo :: Index -> Index -> [ Index ] Source # enumFromThenTo :: Index -> Index -> Index -> [ Index ] Source # |
|
| Eq Index Source # | |
| Integral Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| Num Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| Ord Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| Real Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal Methods toRational :: Index -> Rational Source # |
|
| Show Index Source # | |
| Generic Index Source # | |
| NFData Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| Flat Index Source # | |
| Pretty Index Source # | |
| type Rep Index Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
class HasIndex a where Source #
Instances
| HasIndex TyDeBruijn Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| HasIndex NamedTyDeBruijn Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| HasIndex DeBruijn Source # | |
| HasIndex NamedDeBruijn Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
A term name as a de Bruijn index, without the name string.
Instances
| Eq DeBruijn Source # | |
| Show DeBruijn Source # | |
| Generic DeBruijn Source # | |
| NFData DeBruijn Source # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
| Flat DeBruijn Source # | |
| HasIndex DeBruijn Source # | |
| HasPrettyConfigName config => PrettyBy config DeBruijn Source # | |
| Flat ( Binder DeBruijn ) Source # | |
| ( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term DeBruijn uni fun ann) Source # | |
| ( GEq uni, Closed uni, Everywhere uni Eq , Eq fun, Eq ann) => Eq ( Term TyDeBruijn DeBruijn uni fun ann) Source # | |
|
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 # | |
|
Defined in PlutusCore.DeBruijn.Internal |
|
data NamedDeBruijn Source #
A term name as a de Bruijn index.
Constructors
| NamedDeBruijn | |
|
Fields
|
|
Instances
newtype FakeNamedDeBruijn Source #
A wrapper around nameddebruijn that must hold the invariant of name=
fakeName
.
Constructors
| FakeNamedDeBruijn NamedDeBruijn |
Instances
newtype TyDeBruijn Source #
A type name as a de Bruijn index, without the name string.
Constructors
| TyDeBruijn DeBruijn |
Instances
newtype NamedTyDeBruijn Source #
A type name as a de Bruijn index.
Constructors
| NamedTyDeBruijn NamedDeBruijn |
Instances
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
class AsFreeVariableError r where Source #
Minimal complete definition
Methods
_FreeVariableError :: Prism' r FreeVariableError Source #
_FreeUnique :: Prism' r Unique Source #
_FreeIndex :: Prism' r Index Source #
Instances
| AsFreeVariableError FreeVariableError Source # | |
| AsFreeVariableError ( Error uni fun ann) Source # | |
|
Defined in PlutusCore.Error Methods _FreeVariableError :: Prism' ( Error uni fun ann) FreeVariableError Source # |
|
| AsFreeVariableError ( Error uni fun a) Source # | |
|
Defined in PlutusIR.Error Methods _FreeVariableError :: Prism' ( Error uni fun a) FreeVariableError Source # |
|
deBruijnTy :: ( AsFreeVariableError e, MonadError e m) => Type TyName uni ann -> m ( Type NamedTyDeBruijn uni ann) Source #
Convert a
Type
with
TyName
s into a
Type
with
NamedTyDeBruijn
s.
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
TyName
s and
Name
s into a
Term
with
NamedTyDeBruijn
s and
NamedDeBruijn
s.
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
NamedTyDeBruijn
s into a
Type
with
TyName
s.
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
NamedTyDeBruijn
s and
NamedDeBruijn
s into a
Term
with
TyName
s and
Name
s.
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
fromFake :: FakeNamedDeBruijn -> DeBruijn Source #
toFake :: DeBruijn -> FakeNamedDeBruijn Source #