plutus-core-1.0.0.1: Language library for Plutus Core
Safe HaskellNone
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

class ToScopedName name where Source #

Methods

toScopedName :: name -> ScopedName Source #

Instances

Instances details
ToScopedName TyName Source # 
Instance details

Defined in PlutusCore.Check.Scoping

ToScopedName Name Source # 
Instance details

Defined in PlutusCore.Check.Scoping

introduceBound :: ToScopedName name => name -> NameAnn Source #

Annotation for a binding saying "supposed to disappear".

registerBound :: ToScopedName name => name -> NameAnn Source #

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

registerOutOfScope :: ToScopedName name => name -> NameAnn Source #

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

registerFree :: ToScopedName name => name -> NameAnn Source #

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

class Reference n t where Source #

Methods

referenceVia :: (forall 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 ~ TyName => Reference TyName (Type tyname uni) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn Source #

tyname ~ TyName => Reference TyName (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source #

tyname ~ TyName => Reference TyName (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source #

tyname ~ TyName => Reference TyName (Binding tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> Binding tyname name uni fun NameAnn -> Binding tyname name uni fun NameAnn Source #

tyname ~ TyName => Reference TyName (Datatype tyname name uni fun) Source #

Scoping for data types is hard, so we employ some extra paranoia and reference the provided TyName in the type of every single constructor, and also apply the final head to that TyName.

Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> Datatype tyname name uni fun NameAnn -> Datatype tyname name uni fun NameAnn Source #

name ~ Name => Reference Name (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> Name -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source #

name ~ Name => Reference Name (Term tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> Name -> Term tyname name uni fun NameAnn -> Term tyname name uni fun NameAnn Source #

name ~ Name => Reference Name (Binding tyname name uni fun) Source #

Unlike other Reference instances this one does not guarantee that the name will actually be referenced, but it's too convenient to have this instance to give up on it, without it would be awkward to express "reference this binding in this thing".

Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> Name -> Binding tyname name uni fun NameAnn -> Binding tyname name uni fun NameAnn Source #

tyname ~ TyName => Reference TyName (VarDecl tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> TyName -> VarDecl tyname name uni fun NameAnn -> VarDecl tyname name uni fun NameAnn Source #

Reference n t => Reference [n] t Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> [n] -> t NameAnn -> t NameAnn Source #

Reference n t => Reference (NonEmpty n) t Source # 
Instance details

Defined in PlutusCore.Check.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> NonEmpty n -> t NameAnn -> t NameAnn Source #

Reference tyname t => Reference (TyVarDecl tyname ann) t Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> TyVarDecl tyname ann -> t NameAnn -> t NameAnn Source #

(Reference TyName t, Reference Name t) => Reference (Binding TyName Name uni fun ann) t Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> Binding TyName Name uni fun ann -> t NameAnn -> t NameAnn Source #

(Reference TyName t, Reference Name t) => Reference (Datatype TyName Name uni fun ann) t Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> Datatype TyName Name uni fun ann -> t NameAnn -> t NameAnn Source #

Reference name t => Reference (VarDecl tyname name uni fun ann) t Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> VarDecl tyname name uni fun ann -> t NameAnn -> t NameAnn Source #

referenceBound :: Reference n t => n -> t NameAnn -> t NameAnn Source #

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

referenceOutOfScope :: Reference 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.

Constructors

ScopeInfo 

Fields

Instances

Instances details
Show ScopeInfo Source # 
Instance details

Defined in PlutusCore.Check.Scoping

to :: ScopeEntry -> ScopeInfo -> Set ScopedName Source #

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

checkEmpty :: (Set ScopedName -> ScopeError) -> Set ScopedName -> Either ScopeError () Source #

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

mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo Source #

Merge two ScopeInfos checking that they do not intersect along the way.

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 ~ TyName => EstablishScoping (Type tyname uni) Source # 
Instance details

Defined in PlutusCore.Core.Instance.Scoping

Methods

establishScoping :: Type 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

establishScoping :: Program 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

establishScoping :: Term tyname name uni fun ann -> Quote (Term tyname name uni fun NameAnn) Source #

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

Defined in PlutusIR.Core.Instance.Scoping

Methods

establishScoping :: Program 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 PlutusIR.Core.Instance.Scoping

Methods

establishScoping :: Term tyname name uni fun ann -> Quote (Term tyname name uni fun NameAnn) Source #

class CollectScopeInfo t where Source #

Methods

collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo 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 ~ TyName => CollectScopeInfo (TyVarDecl tyname) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

tyname ~ TyName => CollectScopeInfo (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

collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

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

Defined in PlutusCore.Core.Instance.Scoping

Methods

collectScopeInfo :: Term tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

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

Defined in PlutusIR.Core.Instance.Scoping

Methods

collectScopeInfo :: Program tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

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

Defined in PlutusIR.Core.Instance.Scoping

Methods

collectScopeInfo :: Term tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

(tyname ~ TyName, name ~ Name) => CollectScopeInfo (Binding tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

collectScopeInfo :: Binding tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

(tyname ~ TyName, name ~ Name) => CollectScopeInfo (Datatype tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

collectScopeInfo :: Datatype tyname name uni fun NameAnn -> ScopeErrorOrInfo Source #

(tyname ~ TyName, name ~ Name) => CollectScopeInfo (VarDecl tyname name uni fun) Source # 
Instance details

Defined in PlutusIR.Core.Instance.Scoping

Methods

collectScopeInfo :: VarDecl tyname name uni fun NameAnn -> ScopeErrorOrInfo 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.

overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo Source #

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

applyStays :: Stays -> ScopedName -> ScopeInfo Source #

Use a Stays to handle an unchanged old name.

applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo Source #

Use a Disappears to handle differing old and new names.

applyNameAction :: NameAction -> ScopedName -> ScopedName -> Either ScopeError ScopeInfo Source #

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

handleSname :: ToScopedName name => NameAnn -> name -> ScopeErrorOrInfo Source #

Use a NameAnn to handle a new name.

symmetricDifference :: Ord a => Set a -> Set a -> Set a Source #

checkScopeInfo :: ScopeInfo -> Either 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 (an internal sanity check)
  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.

checkRespectsScoping :: Scoping t => (t NameAnn -> t NameAnn) -> t ann -> Either ScopeError () Source #

Check if a renamer respects scoping.