Safe Haskell | None |
---|---|
Language | Haskell2010 |
PlutusCore.Check.Scoping
Synopsis
- data ScopedName
- isSameScope :: ScopedName -> ScopedName -> Bool
- data Stays
- data Disappears
- data NameAction
- data NameAnn
-
class
ToScopedName
name
where
- toScopedName :: name -> ScopedName
- introduceBound :: ToScopedName name => name -> NameAnn
- registerBound :: ToScopedName name => name -> NameAnn
- registerOutOfScope :: ToScopedName name => name -> NameAnn
- registerFree :: ToScopedName name => name -> NameAnn
-
class
Reference
n t
where
- referenceVia :: ( forall name. ToScopedName name => name -> NameAnn ) -> n -> t NameAnn -> t NameAnn
- referenceBound :: Reference n t => n -> t NameAnn -> t NameAnn
- referenceOutOfScope :: Reference n t => n -> t NameAnn -> t NameAnn
- data ScopeEntry
-
newtype
ScopeInfo
=
ScopeInfo
{
- unScopeInfo :: Map ScopeEntry ( Set ScopedName )
- to :: ScopeEntry -> ScopeInfo -> Set ScopedName
- emptyScopeInfo :: ScopeInfo
- checkEmpty :: ( Set ScopedName -> ScopeError ) -> Set ScopedName -> Either ScopeError ()
- mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
- newtype ScopeErrorOrInfo = ScopeErrorOrInfo { }
-
class
EstablishScoping
t
where
- establishScoping :: t ann -> Quote (t NameAnn )
-
class
CollectScopeInfo
t
where
- collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo
- type Scoping t = ( EstablishScoping t, CollectScopeInfo t)
- 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 )
-
data
ScopeError
- = UnannotatedName ScopedName
- | NameChangedItsScope ScopedName ScopedName
- | NameUnexpectedlyDisappeared ScopedName ScopedName
- | NameUnexpectedlyStayed ScopedName
- | DuplicateBindersInTheInput ( Set ScopedName )
- | DuplicateBindersInTheOutput ( Set ScopedName )
- | OldBindingsDiscordWithBoundVariables ( Set ScopedName )
- | OldBindingsDiscordWithOutOfScopeVariables ( Set ScopedName )
- | NewBindingsDiscordWithBoundVariables ( Set ScopedName )
- | OldBindingsClashWithFreeVariables ( Set ScopedName )
- | OldBindingsClashWithNewBindings ( Set ScopedName )
- | NewBindingsClashWithFreeVariabes ( Set ScopedName )
- overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo
- applyStays :: Stays -> ScopedName -> ScopeInfo
- applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo
- applyNameAction :: NameAction -> ScopedName -> ScopedName -> Either ScopeError ScopeInfo
- handleSname :: ToScopedName name => NameAnn -> name -> ScopeErrorOrInfo
- symmetricDifference :: Ord a => Set a -> Set a -> Set a
- checkScopeInfo :: ScopeInfo -> Either ScopeError ()
- checkRespectsScoping :: Scoping t => (t NameAnn -> t NameAnn ) -> t ann -> Either ScopeError ()
Documentation
data ScopedName Source #
Instances
Eq ScopedName Source # | |
Defined in PlutusCore.Check.Scoping Methods (==) :: ScopedName -> ScopedName -> Bool Source # (/=) :: ScopedName -> ScopedName -> Bool Source # |
|
Ord ScopedName Source # | |
Defined in PlutusCore.Check.Scoping Methods compare :: ScopedName -> ScopedName -> Ordering Source # (<) :: ScopedName -> ScopedName -> Bool Source # (<=) :: ScopedName -> ScopedName -> Bool Source # (>) :: ScopedName -> ScopedName -> Bool Source # (>=) :: ScopedName -> ScopedName -> Bool Source # max :: ScopedName -> ScopedName -> ScopedName Source # min :: ScopedName -> ScopedName -> ScopedName Source # |
|
Show ScopedName Source # | |
Defined in PlutusCore.Check.Scoping |
isSameScope :: ScopedName -> ScopedName -> Bool 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. |
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
Show Disappears Source # | |
Defined in PlutusCore.Check.Scoping |
data NameAction Source #
A name either stays or disappears.
Constructors
Stays Stays | |
Disappears Disappears |
Instances
Show NameAction Source # | |
Defined in PlutusCore.Check.Scoping |
Constructors
NameAction NameAction ScopedName | |
NotAName |
class ToScopedName name where Source #
Methods
toScopedName :: name -> ScopedName Source #
Instances
ToScopedName TyName Source # | |
Defined in PlutusCore.Check.Scoping Methods toScopedName :: TyName -> ScopedName Source # |
|
ToScopedName Name Source # | |
Defined in PlutusCore.Check.Scoping Methods toScopedName :: Name -> ScopedName Source # |
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
tyname ~ TyName => Reference TyName ( Type tyname uni) Source # | |
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 # | |
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 # | |
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 # | |
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
|
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 # | |
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 # | |
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
|
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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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.
data ScopeEntry Source #
Each kind of old and new names.
Constructors
DisappearedBindings | |
DisappearedVariables | |
AppearedBindings | |
AppearedVariables | |
StayedOutOfScopeVariables | |
StayedFreeVariables |
Instances
Eq ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping Methods (==) :: ScopeEntry -> ScopeEntry -> Bool Source # (/=) :: ScopeEntry -> ScopeEntry -> Bool Source # |
|
Ord ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping Methods compare :: ScopeEntry -> ScopeEntry -> Ordering Source # (<) :: ScopeEntry -> ScopeEntry -> Bool Source # (<=) :: ScopeEntry -> ScopeEntry -> Bool Source # (>) :: ScopeEntry -> ScopeEntry -> Bool Source # (>=) :: ScopeEntry -> ScopeEntry -> Bool Source # max :: ScopeEntry -> ScopeEntry -> ScopeEntry Source # min :: ScopeEntry -> ScopeEntry -> ScopeEntry Source # |
|
Show ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping |
A
ScopeInfo
is a set of
ScopedName
s for each of the
ScopeEntry
.
If a
ScopeEntry
is not present in the map, the corresponding set of
ScopeName
s is considered
to be empty.
Constructors
ScopeInfo | |
Fields
|
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
ScopeInfo
s checking that they do not intersect along the way.
newtype ScopeErrorOrInfo Source #
Constructors
ScopeErrorOrInfo | |
Fields |
Instances
Semigroup ScopeErrorOrInfo Source # | |
Defined in PlutusCore.Check.Scoping Methods (<>) :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo Source # sconcat :: NonEmpty ScopeErrorOrInfo -> ScopeErrorOrInfo Source # stimes :: Integral b => b -> ScopeErrorOrInfo -> ScopeErrorOrInfo Source # |
|
Monoid ScopeErrorOrInfo Source # | |
Defined in PlutusCore.Check.Scoping Methods mempty :: ScopeErrorOrInfo Source # mappend :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo Source # mconcat :: [ ScopeErrorOrInfo ] -> ScopeErrorOrInfo Source # |
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:
-
handle bindings with 'freshen*Name' +
establishScopingBinder
(or similar) -
handle variables with 'freshen*Name' +
registerFree
-
everything else is direct recursion +
Applicative
stuff
Instances
EstablishScoping Kind Source # | |
Defined in PlutusCore.Core.Instance.Scoping |
|
tyname ~ TyName => EstablishScoping ( Type tyname uni) Source # | |
Defined in PlutusCore.Core.Instance.Scoping |
|
(tyname ~ TyName , name ~ Name ) => EstablishScoping ( Program tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping |
|
(tyname ~ TyName , name ~ Name ) => EstablishScoping ( Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping |
|
(tyname ~ TyName , name ~ Name ) => EstablishScoping ( Program tyname name uni fun) Source # | |
Defined in PlutusIR.Core.Instance.Scoping |
|
(tyname ~ TyName , name ~ Name ) => EstablishScoping ( Term tyname name uni fun) Source # | |
Defined in PlutusIR.Core.Instance.Scoping |
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:
-
handle names (both bindings and variables) with
handleSname
-
everything else is direct recursion +
Monoid
stuff
Instances
type Scoping t = ( EstablishScoping t, CollectScopeInfo t) 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.
Constructors
Instances
Show ScopeError Source # | |
Defined in PlutusCore.Check.Scoping |
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.
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:
- disappeared bindings should be the same as stayed out of scope variables (an internal sanity check)
- disappeared bindings should be the same as disappeared variables (ensures that old names consistently disappear at the binding and use sites)
- 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:
- disappeared bindings should not intersect with free variables (an internal sanity check)
- appeared bindings should not intersect with disappeared bindings
- 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.