Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Support for using de Bruijn indices for term and type names.
Synopsis
- newtype Index = Index Word64
- newtype Level = Level Integer
- data LevelInfo = LevelInfo {
- currentLevel ∷ Level
- levelMapping ∷ Bimap Unique Level
- class HasIndex a where
- newtype DeBruijn = DeBruijn {}
- data NamedDeBruijn = NamedDeBruijn {
- ndbnString ∷ !Text
- ndbnIndex ∷ !Index
- data FakeNamedDeBruijn
- newtype TyDeBruijn = TyDeBruijn DeBruijn
- newtype NamedTyDeBruijn = NamedTyDeBruijn NamedDeBruijn
- data FreeVariableError
- = FreeUnique !Unique
- | FreeIndex !Index
- 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
- fakeTyNameDeBruijn ∷ TyDeBruijn → NamedTyDeBruijn
- 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 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)
- unDeBruijnTermWith ∷ MonadQuote m ⇒ (Index → ReaderT LevelInfo m Unique) → Term NamedTyDeBruijn NamedDeBruijn uni fun ann → m (Term TyName Name uni fun ann)
- freeIndexAsConsistentLevel ∷ (MonadReader LevelInfo 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.
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.
Instances
Enum Index Source # | |
Generic Index Source # | |
Num Index Source # | |
Read Index Source # | |
Integral Index Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
Real Index Source # | |
Defined in PlutusCore.DeBruijn.Internal toRational ∷ Index → Rational Source # | |
Show Index Source # | |
NFData Index Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
Flat Index Source # | |
Eq Index Source # | |
Ord Index Source # | |
Hashable Index Source # | |
Pretty Index Source # | |
type Rep Index Source # | |
Defined in PlutusCore.DeBruijn.Internal |
An absolute level in the program.
Instances
Enum Level Source # | |
Num Level Source # | |
Integral Level Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
Real Level Source # | |
Defined in PlutusCore.DeBruijn.Internal toRational ∷ Level → Rational Source # | |
Eq Level Source # | |
Ord Level 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.
LevelInfo | |
|
class HasIndex a where Source #
Instances
HasIndex DeBruijn Source # | |
HasIndex NamedDeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
HasIndex NamedTyDeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
HasIndex TyDeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal |
A term name as a de Bruijn index, without the name string.
Instances
Generic DeBruijn Source # | |
Show DeBruijn Source # | |
NFData DeBruijn Source # | |
Defined in PlutusCore.DeBruijn.Internal | |
Flat DeBruijn Source # | |
Eq DeBruijn Source # | |
Hashable 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 # | |
HashableTermConstraints uni fun ann ⇒ Hashable (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 (==) ∷ 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.
Instances
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
newtype TyDeBruijn Source #
A type name as a de Bruijn index, without the name string.
Instances
newtype NamedTyDeBruijn Source #
A type name as a de Bruijn index.
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.
Instances
class AsFreeVariableError r where Source #
_FreeVariableError ∷ Prism' r FreeVariableError Source #
_FreeUnique ∷ Prism' r Unique Source #
_FreeIndex ∷ Prism' r Index Source #
Instances
AsFreeVariableError FreeVariableError Source # | |
Defined in PlutusCore.DeBruijn.Internal _FreeVariableError ∷ Prism' FreeVariableError FreeVariableError Source # _FreeUnique ∷ Prism' FreeVariableError Unique Source # _FreeIndex ∷ Prism' FreeVariableError Index Source # | |
AsFreeVariableError (Error uni fun ann) Source # | |
Defined in PlutusCore.Error _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 TyName
s into a Kind
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 Kind
with NamedTyDeBruijn
s into a Kind
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 LevelInfo m Index) → Type TyName uni ann → m (Type NamedTyDeBruijn uni ann) Source #
deBruijnTermWith ∷ Monad m ⇒ (Unique → ReaderT LevelInfo m Index) → Term TyName Name uni fun ann → m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann) Source #
unDeBruijnTyWith ∷ MonadQuote 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.
unDeBruijnTermWith ∷ MonadQuote 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).
deBruijnInitIndex ∷ Index Source #
The LamAbs index (for debruijn indices) and the starting level of DeBruijn monad