| Safe Haskell | Safe-Inferred |
|---|---|
| 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 (Map ScopeEntry (Set ScopedName))
- unScopeInfo :: ScopeInfo -> Map ScopeEntry (Set ScopedName)
- to :: ScopeEntry -> ScopeInfo -> Set ScopedName
- emptyScopeInfo :: ScopeInfo
- checkEmptyOn :: (Set ScopedName -> Set ScopedName -> Set ScopedName) -> (Set ScopedName -> Set ScopedName -> ScopeError) -> Set ScopedName -> Set ScopedName -> Either ScopeError ()
- mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo
- newtype ScopeErrorOrInfo = ScopeErrorOrInfo (Either ScopeError ScopeInfo)
- unScopeErrorOrInfo :: ScopeErrorOrInfo -> Either ScopeError ScopeInfo
- data BindingRemoval
- 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, EstablishScoping sort, EstablishScoping value) => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn) -> name -> sort ann -> value ann -> Quote (value NameAnn)
- data ScopeError
- = UnannotatedName !ScopedName
- | NameChangedItsScope {
- _oldName :: !ScopedName
- _newName :: !ScopedName
- | NameUnexpectedlyDisappeared {
- _oldName :: !ScopedName
- _newName :: !ScopedName
- | NameUnexpectedlyStayed !ScopedName
- | DuplicateBindersInTheInput { }
- | DuplicateBindersInTheOutput !(Set ScopedName) !(Set ScopedName)
- | DisappearedBindingsDiscordWithBoundVariables {
- _disappearedBindings :: !(Set ScopedName)
- _boundVariables :: !(Set ScopedName)
- | DisappearedBindingsDiscordWithOutOfScopeVariables { }
- | AppearedBindingsDiscordWithBoundVariables {
- _appearedBindings :: !(Set ScopedName)
- _boundVariables :: !(Set ScopedName)
- | DisappearedBindingsClashWithFreeVariables {
- _disappearedBindings :: !(Set ScopedName)
- _freeVariables :: !(Set ScopedName)
- | DisappearedBindingsClashWithAppearedBindings {
- _disppearedBindings :: !(Set ScopedName)
- _appearedBindings :: !(Set ScopedName)
- | AppearedBindingsClashWithFreeVariabes {
- _appearedBindings :: !(Set ScopedName)
- _freeVariables :: !(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 :: BindingRemoval -> ScopeInfo -> Either ScopeError ()
- data ScopeCheckError t = ScopeCheckError {}
- checkRespectsScoping :: Scoping t => BindingRemoval -> (t NameAnn -> t NameAnn) -> (t NameAnn -> t NameAnn) -> t ann -> Either (ScopeCheckError t) ()
Documentation
data ScopedName #
Instances
| Show ScopedName # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> ScopedName -> ShowS # show :: ScopedName -> String # showList :: [ScopedName] -> ShowS # | |
| Eq ScopedName # | |
Defined in PlutusCore.Check.Scoping | |
| Ord ScopedName # | |
Defined in PlutusCore.Check.Scoping Methods compare :: ScopedName -> ScopedName -> Ordering # (<) :: ScopedName -> ScopedName -> Bool # (<=) :: ScopedName -> ScopedName -> Bool # (>) :: ScopedName -> ScopedName -> Bool # (>=) :: ScopedName -> ScopedName -> Bool # max :: ScopedName -> ScopedName -> ScopedName # min :: ScopedName -> ScopedName -> ScopedName # | |
isSameScope :: ScopedName -> ScopedName -> Bool #
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 #
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 # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> Disappears -> ShowS # show :: Disappears -> String # showList :: [Disappears] -> ShowS # | |
| Eq Disappears # | |
Defined in PlutusCore.Check.Scoping | |
data NameAction #
A name either stays or disappears.
Constructors
| Stays Stays | |
| Disappears Disappears |
Instances
| Show NameAction # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> NameAction -> ShowS # show :: NameAction -> String # showList :: [NameAction] -> ShowS # | |
| Eq NameAction # | |
Defined in PlutusCore.Check.Scoping | |
Constructors
| NameAction NameAction ScopedName | |
| NotAName |
class ToScopedName name where #
Methods
toScopedName :: name -> ScopedName #
Instances
| ToScopedName Name # | |
Defined in PlutusCore.Check.Scoping Methods toScopedName :: Name -> ScopedName # | |
| ToScopedName TyName # | |
Defined in PlutusCore.Check.Scoping Methods toScopedName :: TyName -> ScopedName # | |
introduceBound :: ToScopedName name => name -> NameAnn #
Annotation for a binding saying "supposed to disappear".
registerBound :: ToScopedName name => name -> NameAnn #
Annotation for a bound variable saying "supposed to disappear".
registerOutOfScope :: ToScopedName name => name -> NameAnn #
Annotation for an out-of-scope variable saying "supposed to stay out of scope".
registerFree :: ToScopedName name => name -> NameAnn #
Annotation for a free variable saying "supposed to stay free".
Methods
referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> n -> t NameAnn -> t NameAnn #
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) # | |
Defined in PlutusCore.Core.Instance.Scoping Methods referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> TyName -> Type tyname uni NameAnn -> Type tyname uni NameAnn # | |
| name ~ Name => Reference Name (Term name uni fun) # | |
Defined in UntypedPlutusCore.Core.Instance.Scoping Methods referenceVia :: (forall name0. ToScopedName name0 => name0 -> NameAnn) -> Name -> Term name uni fun NameAnn -> Term name uni fun NameAnn # | |
| name ~ Name => Reference Name (Term tyname name uni fun) # | |
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 # | |
| tyname ~ TyName => Reference TyName (Term tyname name uni fun) # | |
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 # | |
| Reference n t => Reference (NonEmpty n) t # | |
Defined in PlutusCore.Check.Scoping Methods referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> NonEmpty n -> t NameAnn -> t NameAnn # | |
| Reference n t => Reference [n] t # | |
Defined in PlutusCore.Check.Scoping Methods referenceVia :: (forall name. ToScopedName name => name -> NameAnn) -> [n] -> t NameAnn -> t NameAnn # | |
referenceBound :: Reference n t => n -> t NameAnn -> t NameAnn #
Reference the provided variable in the provided type/term as an in-scope one.
referenceOutOfScope :: Reference n t => n -> t NameAnn -> t NameAnn #
Reference the provided variable in the provided type/term as an out-of-scope one.
data ScopeEntry #
Each kind of old and new names.
Constructors
| DisappearedBindings | |
| DisappearedVariables | |
| AppearedBindings | |
| AppearedVariables | |
| StayedOutOfScopeVariables | |
| StayedFreeVariables |
Instances
| Show ScopeEntry # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> ScopeEntry -> ShowS # show :: ScopeEntry -> String # showList :: [ScopeEntry] -> ShowS # | |
| Eq ScopeEntry # | |
Defined in PlutusCore.Check.Scoping | |
| Ord ScopeEntry # | |
Defined in PlutusCore.Check.Scoping Methods compare :: ScopeEntry -> ScopeEntry -> Ordering # (<) :: ScopeEntry -> ScopeEntry -> Bool # (<=) :: ScopeEntry -> ScopeEntry -> Bool # (>) :: ScopeEntry -> ScopeEntry -> Bool # (>=) :: ScopeEntry -> ScopeEntry -> Bool # max :: ScopeEntry -> ScopeEntry -> ScopeEntry # min :: ScopeEntry -> ScopeEntry -> ScopeEntry # | |
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 (Map ScopeEntry (Set ScopedName)) |
unScopeInfo :: ScopeInfo -> Map ScopeEntry (Set ScopedName) #
to :: ScopeEntry -> ScopeInfo -> Set ScopedName #
Extract the set stored in the provided ScopeInfo at the provided ScopeEntry.
checkEmptyOn :: (Set ScopedName -> Set ScopedName -> Set ScopedName) -> (Set ScopedName -> Set ScopedName -> ScopeError) -> Set ScopedName -> Set ScopedName -> Either ScopeError () #
Check if a set is empty and report an error with the set embedded in it otherwise.
mergeScopeInfo :: ScopeInfo -> ScopeInfo -> Either ScopeError ScopeInfo #
Merge two ScopeInfos checking that binders in them do not intersect along the way.
newtype ScopeErrorOrInfo #
Constructors
| ScopeErrorOrInfo (Either ScopeError ScopeInfo) |
Instances
| Monoid ScopeErrorOrInfo # | |
Defined in PlutusCore.Check.Scoping Methods mappend :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo # mconcat :: [ScopeErrorOrInfo] -> ScopeErrorOrInfo # | |
| Semigroup ScopeErrorOrInfo # | |
Defined in PlutusCore.Check.Scoping Methods (<>) :: ScopeErrorOrInfo -> ScopeErrorOrInfo -> ScopeErrorOrInfo # sconcat :: NonEmpty ScopeErrorOrInfo -> ScopeErrorOrInfo # stimes :: Integral b => b -> ScopeErrorOrInfo -> ScopeErrorOrInfo # | |
data BindingRemoval #
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.
Constructors
| BindingRemovalOk | |
| BindingRemovalNotOk |
Instances
| Show BindingRemoval # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> BindingRemoval -> ShowS # show :: BindingRemoval -> String # showList :: [BindingRemoval] -> ShowS # | |
| Eq BindingRemoval # | |
Defined in PlutusCore.Check.Scoping Methods (==) :: BindingRemoval -> BindingRemoval -> Bool # (/=) :: BindingRemoval -> BindingRemoval -> Bool # | |
class EstablishScoping t where #
Methods
establishScoping :: t ann -> Quote (t NameAnn) #
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 +
Applicativestuff
Instances
| EstablishScoping Kind # | |
Defined in PlutusCore.Core.Instance.Scoping | |
| EstablishScoping (Proxy :: Type -> Type) # | |
Defined in PlutusCore.Check.Scoping | |
| tyname ~ TyName => EstablishScoping (Type tyname uni) # | |
Defined in PlutusCore.Core.Instance.Scoping | |
| name ~ Name => EstablishScoping (Program name uni fun) # | |
Defined in UntypedPlutusCore.Core.Instance.Scoping | |
| name ~ Name => EstablishScoping (Term name uni fun) # | |
Defined in UntypedPlutusCore.Core.Instance.Scoping | |
| (tyname ~ TyName, name ~ Name) => EstablishScoping (Program tyname name uni fun) # | |
Defined in PlutusCore.Core.Instance.Scoping | |
| (tyname ~ TyName, name ~ Name) => EstablishScoping (Term tyname name uni fun) # | |
Defined in PlutusCore.Core.Instance.Scoping | |
class CollectScopeInfo t where #
Methods
collectScopeInfo :: t NameAnn -> ScopeErrorOrInfo #
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 +
Monoidstuff
Instances
type Scoping t = (EstablishScoping t, CollectScopeInfo t) #
establishScopingBinder :: (Reference name value, ToScopedName name, EstablishScoping sort, EstablishScoping value) => (NameAnn -> name -> sort NameAnn -> value NameAnn -> value NameAnn) -> name -> sort ann -> value ann -> Quote (value NameAnn) #
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 #
Every kind of error thrown by the scope checking machinery at different stages.
Constructors
Instances
| Show ScopeError # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> ScopeError -> ShowS # show :: ScopeError -> String # showList :: [ScopeError] -> ShowS # | |
| Pretty ScopeError # | |
Defined in PlutusCore.Check.Scoping | |
overrideSname :: ScopeEntry -> ScopedName -> ScopeInfo -> ScopeInfo #
Override the set at the provided ScopeEntry to contain only the provided ScopedName.
applyStays :: Stays -> ScopedName -> ScopeInfo #
Use a Stays to handle an unchanged old name.
applyDisappears :: Disappears -> ScopedName -> ScopedName -> ScopeInfo #
Use a Disappears to handle differing old and new names.
applyNameAction :: NameAction -> ScopedName -> ScopedName -> Either ScopeError ScopeInfo #
Use a NameAction to handle an old and a new name.
handleSname :: ToScopedName name => NameAnn -> name -> ScopeErrorOrInfo #
Use a NameAnn to handle a new name.
checkScopeInfo :: BindingRemoval -> ScopeInfo -> Either ScopeError () #
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 (ensures that old bindings disappear via renaming and not via removal)
- 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.
data ScopeCheckError t #
The type of errors that the scope checking machinery returns.
Constructors
| ScopeCheckError | |
Instances
| PrettyBy config (t NameAnn) => PrettyBy config (ScopeCheckError t) # | |
Defined in PlutusCore.Check.Scoping Methods prettyBy :: config -> ScopeCheckError t -> Doc ann # prettyListBy :: config -> [ScopeCheckError t] -> Doc ann # | |
| Show (t NameAnn) => Show (ScopeCheckError t) # | |
Defined in PlutusCore.Check.Scoping Methods showsPrec :: Int -> ScopeCheckError t -> ShowS # show :: ScopeCheckError t -> String # showList :: [ScopeCheckError t] -> ShowS # | |
Arguments
| :: Scoping t | |
| => BindingRemoval | |
| -> (t NameAnn -> t NameAnn) | For preparation before running the scoping tests.
Commonly, either |
| -> (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.