plutus-core-1.36.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.Check.Scoping

Synopsis

Documentation

data Stays Source #

Staying names.

Constructors

StaysOutOfScopeVariable

An out-of-scope variable does not get renamed and hence stays.

StaysFreeVariable

A free variable does not get renamed and hence stays.

Instances

Instances details
Show Stays Source # 
Instance details

Defined in PlutusCore.Check.Scoping

data Disappears Source #

Changing names.

Constructors

DisappearsBinding

A binding gets renamed and hence the name that it binds disappears.

DisappearsVariable

A bound variable gets renamed and hence its name disappears.

Instances

Instances details
Show Disappears Source # 
Instance details

Defined in PlutusCore.Check.Scoping

data NameAction Source #

A name either stays or disappears.

Instances

Instances details
Show NameAction Source # 
Instance details

Defined in PlutusCore.Check.Scoping

data NameAnn Source #

Instances

Instances details
Show NameAnn Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Pretty NameAnn Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

prettyNameAnnDoc ann Source #

prettyList ∷ [NameAnn] → Doc ann Source #

class ToScopedName name where Source #

Methods

toScopedName ∷ name → ScopedName Source #

Instances

Instances details
ToScopedName Name Source # 
Instance details

Defined in PlutusCore.Check.Scoping

ToScopedName TyName Source # 
Instance details

Defined in PlutusCore.Check.Scoping

introduceBoundToScopedName name ⇒ name → NameAnn Source #

Annotation for a binding saying "supposed to disappear".

registerBoundToScopedName name ⇒ name → NameAnn Source #

Annotation for a bound variable saying "supposed to disappear".

registerOutOfScopeToScopedName name ⇒ name → NameAnn Source #

Annotation for an out-of-scope variable saying "supposed to stay out of scope".

registerFreeToScopedName name ⇒ name → NameAnn Source #

Annotation for a free variable saying "supposed to stay free".

class Reference n t where Source #

Methods

referenceVia ∷ (∀ name. ToScopedName name ⇒ name → NameAnn) → n → t NameAnn → t NameAnn Source #

Take a registering function, apply it to the provided name, create a type/term variable out of the resulting annotation and the original name and reference that variable in the provided type/term by prepending a constructor to it mentioning the variable.

Instances

Instances details
tyname ~ TyNameReference TyName (Type tyname uni) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia ∷ (∀ name. ToScopedName name ⇒ name → NameAnn) → TyNameType tyname uni NameAnnType tyname uni NameAnn Source #

name ~ NameReference Name (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia ∷ (∀ name0. ToScopedName name0 ⇒ name0 → NameAnn) → NameTerm tyname name uni fun NameAnnTerm tyname name uni fun NameAnn Source #

tyname ~ TyNameReference TyName (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia ∷ (∀ name0. ToScopedName name0 ⇒ name0 → NameAnn) → TyNameTerm tyname name uni fun NameAnnTerm tyname name uni fun NameAnn Source #

Reference n t ⇒ Reference (NonEmpty n) t Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

referenceVia ∷ (∀ name. ToScopedName name ⇒ name → NameAnn) → NonEmpty n → t NameAnn → t NameAnn Source #

Reference n t ⇒ Reference [n] t Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

referenceVia ∷ (∀ name. ToScopedName name ⇒ name → NameAnn) → [n] → t NameAnn → t NameAnn Source #

referenceBoundReference n t ⇒ n → t NameAnn → t NameAnn Source #

Reference the provided variable in the provided type/term as an in-scope one.

referenceOutOfScopeReference n t ⇒ n → t NameAnn → t NameAnn Source #

Reference the provided variable in the provided type/term as an out-of-scope one.

newtype ScopeInfo Source #

A ScopeInfo is a set of ScopedNames for each of the ScopeEntry. If a ScopeEntry is not present in the map, the corresponding set of ScopeNames is considered to be empty.

Instances

Instances details
Show ScopeInfo Source # 
Instance details

Defined in PlutusCore.Check.Scoping

toScopeEntryScopeInfoSet ScopedName Source #

Extract the set stored in the provided ScopeInfo at the provided ScopeEntry.

checkEmptyOn ∷ (Set ScopedNameSet ScopedNameSet ScopedName) → (Set ScopedNameSet ScopedNameScopeError) → Set ScopedNameSet ScopedNameEither ScopeError () Source #

Check if a set is empty and report an error with the set embedded in it otherwise.

mergeScopeInfoScopeInfoScopeInfoEither ScopeError ScopeInfo Source #

Merge two ScopeInfos checking that binders in them do not intersect along the way.

data BindingRemoval Source #

Whether it's OK if the pass removes bindings. A renamer isn't supposed to do that, but for example an inliner may do it, since it's basically the entire point of an inliner.

class EstablishScoping t where Source #

Methods

establishScoping ∷ t ann → Quote (t NameAnn) Source #

Traverse a t freshening every name (both at the binding and the use sites) and annotating the freshened names with either DisappearsBinding or StaysFreeVariable depending on whether the name occurs at the binding or the use site.

In addition to that every binder should be decorated with one out-of-scope variable (annotated with StaysOutOfScopeVariable) and one in-scope one (annotated with DisappearsVariable).

Note that no original name occurring in t should survive this procedure (and hence we don't care if any of the freshened names clashes with an original one as all original ones are supposed to be gone).

How to provide an implementation:

  1. handle bindings with 'freshen*Name' + establishScopingBinder (or similar)
  2. handle variables with 'freshen*Name' + registerFree
  3. everything else is direct recursion + Applicative stuff

Instances

Instances details
EstablishScoping Kind Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

tyname ~ TyNameEstablishScoping (Type tyname uni) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

establishScopingType tyname uni ann → Quote (Type tyname uni NameAnn) Source #

(tyname ~ TyName, name ~ Name) ⇒ EstablishScoping (Program tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

establishScopingProgram tyname name uni fun ann → Quote (Program tyname name uni fun NameAnn) Source #

(tyname ~ TyName, name ~ Name) ⇒ EstablishScoping (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

establishScopingTerm tyname name uni fun ann → Quote (Term tyname name uni fun NameAnn) Source #

class CollectScopeInfo t where Source #

Methods

collectScopeInfo ∷ t NameAnnScopeErrorOrInfo Source #

Collect scoping information after scoping was established and renaming was performed.

How to provide an implementation:

  1. handle names (both bindings and variables) with handleSname
  2. everything else is direct recursion + Monoid stuff

Instances

Instances details
CollectScopeInfo Kind Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

tyname ~ TyNameCollectScopeInfo (Type tyname uni) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

(tyname ~ TyName, name ~ Name) ⇒ CollectScopeInfo (Program tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

collectScopeInfoProgram tyname name uni fun NameAnnScopeErrorOrInfo Source #

(tyname ~ TyName, name ~ Name) ⇒ CollectScopeInfo (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

collectScopeInfoTerm tyname name uni fun NameAnnScopeErrorOrInfo Source #

establishScopingBinder ∷ (Reference name value, ToScopedName name, Scoping sort, Scoping value) ⇒ (NameAnn → name → sort NameAnn → value NameAnn → value NameAnn) → name → sort ann → value ann → Quote (value NameAnn) Source #

Take a constructor for a binder, a name bound by it, a sort (kind/type), a value of that sort (type/term) and call establishScoping on both the sort and its value and reassemble the original binder with the annotated sort and its value, but also decorate the reassembled binder with one out-of-scope variable and one in-scope one.

data ScopeError Source #

Every kind of error thrown by the scope checking machinery at different stages.

Instances

Instances details
Show ScopeError Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Pretty ScopeError Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

prettyScopeErrorDoc ann Source #

prettyList ∷ [ScopeError] → Doc ann Source #

overrideSnameScopeEntryScopedNameScopeInfoScopeInfo Source #

Override the set at the provided ScopeEntry to contain only the provided ScopedName.

applyStaysStaysScopedNameScopeInfo Source #

Use a Stays to handle an unchanged old name.

applyDisappearsDisappearsScopedNameScopedNameScopeInfo Source #

Use a Disappears to handle differing old and new names.

applyNameActionNameActionScopedNameScopedNameEither ScopeError ScopeInfo Source #

Use a NameAction to handle an old and a new name.

handleSnameToScopedName name ⇒ NameAnn → name → ScopeErrorOrInfo Source #

Use a NameAnn to handle a new name.

symmetricDifferenceOrd a ⇒ Set a → Set a → Set a Source #

checkScopeInfoBindingRemovalScopeInfoEither ScopeError () Source #

Check that each kind of Set from ScopeInfo relates to all other ones in a certain way. We start with these three relations that are based on the assumption that for each binder we add at least one out-of-scope variable and at least one in-scope one:

  1. disappeared bindings should be the same as stayed out of scope variables (ensures that old bindings disappear via renaming and not via removal)
  2. disappeared bindings should be the same as disappeared variables (ensures that old names consistently disappear at the binding and use sites)
  3. appeared bindings should be the same as appeared variables (ensures that new names consistently appear at the binding and use sites)

Once we've ensured all of that, we're left with only three sets and 3C2 equals 3, so we only need to consider three more relations:

  1. disappeared bindings should not intersect with free variables (an internal sanity check)
  2. appeared bindings should not intersect with disappeared bindings
  3. appeared bindings should not intersect with free variables

The last two ensure that no new name has an old name's unique.

data ScopeCheckError t Source #

The type of errors that the scope checking machinery returns.

Constructors

ScopeCheckError 

Fields

Instances

Instances details
PrettyBy config (t NameAnn) ⇒ PrettyBy config (ScopeCheckError t) Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

prettyBy ∷ config → ScopeCheckError t → Doc ann Source #

prettyListBy ∷ config → [ScopeCheckError t] → Doc ann Source #

Show (t NameAnn) ⇒ Show (ScopeCheckError t) Source # 
Instance details

Defined in PlutusCore.Check.Scoping

checkRespectsScoping Source #

Arguments

Scoping t 
BindingRemoval 
→ (t NameAnn → t NameAnn)

For preparation before running the scoping tests. Commonly, either runQuote . rename or id.

→ (t NameAnn → t NameAnn)

The runner of the pass.

→ t ann 
Either (ScopeCheckError t) () 

Check if a pass respects scoping.

Returns the thing that the scoping tests run on, the result of the pass and the scope checking outcome, respectively.