Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 ∷ (∀ 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
- 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 { }
- | NameUnexpectedlyDisappeared { }
- | NameUnexpectedlyStayed !ScopedName
- | DuplicateBindersInTheInput { }
- | DuplicateBindersInTheOutput !(Set ScopedName) !(Set ScopedName)
- | DisappearedBindingsDiscordWithBoundVariables { }
- | DisappearedBindingsDiscordWithOutOfScopeVariables { }
- | AppearedBindingsDiscordWithBoundVariables { }
- | DisappearedBindingsClashWithFreeVariables { }
- | DisappearedBindingsClashWithAppearedBindings { }
- | AppearedBindingsClashWithFreeVariabes { }
- 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 Source #
Instances
Show ScopedName Source # | |
Defined in PlutusCore.Check.Scoping | |
Eq ScopedName Source # | |
Defined in PlutusCore.Check.Scoping (==) ∷ ScopedName → ScopedName → Bool Source # (/=) ∷ ScopedName → ScopedName → Bool Source # | |
Ord ScopedName Source # | |
Defined in PlutusCore.Check.Scoping 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 # |
isSameScope ∷ ScopedName → ScopedName → Bool Source #
Staying names.
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.
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.
Instances
Show NameAction Source # | |
Defined in PlutusCore.Check.Scoping |
class ToScopedName name where Source #
toScopedName ∷ name → ScopedName Source #
Instances
ToScopedName Name Source # | |
Defined in PlutusCore.Check.Scoping | |
ToScopedName TyName Source # | |
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 #
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
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.
DisappearedBindings | |
DisappearedVariables | |
AppearedBindings | |
AppearedVariables | |
StayedOutOfScopeVariables | |
StayedFreeVariables |
Instances
Show ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping | |
Eq ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping (==) ∷ ScopeEntry → ScopeEntry → Bool Source # (/=) ∷ ScopeEntry → ScopeEntry → Bool Source # | |
Ord ScopeEntry Source # | |
Defined in PlutusCore.Check.Scoping 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 # |
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.
to ∷ ScopeEntry → ScopeInfo → Set ScopedName Source #
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 () 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 binders in them do not intersect along the way.
newtype ScopeErrorOrInfo Source #
Instances
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.
Instances
Show BindingRemoval Source # | |
Defined in PlutusCore.Check.Scoping | |
Eq BindingRemoval Source # | |
Defined in PlutusCore.Check.Scoping (==) ∷ BindingRemoval → BindingRemoval → Bool Source # (/=) ∷ BindingRemoval → BindingRemoval → Bool Source # |
class EstablishScoping t where Source #
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 |
class CollectScopeInfo t where Source #
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
CollectScopeInfo Kind Source # | |
Defined in PlutusCore.Core.Instance.Scoping | |
tyname ~ TyName ⇒ CollectScopeInfo (Type tyname uni) Source # | |
Defined in PlutusCore.Core.Instance.Scoping collectScopeInfo ∷ Type tyname uni NameAnn → ScopeErrorOrInfo Source # | |
(tyname ~ TyName, name ~ Name) ⇒ CollectScopeInfo (Program tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping collectScopeInfo ∷ Program tyname name uni fun NameAnn → ScopeErrorOrInfo Source # | |
(tyname ~ TyName, name ~ Name) ⇒ CollectScopeInfo (Term tyname name uni fun) Source # | |
Defined in PlutusCore.Core.Instance.Scoping collectScopeInfo ∷ Term tyname name uni fun NameAnn → ScopeErrorOrInfo Source # |
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.
Instances
Show ScopeError Source # | |
Defined in PlutusCore.Check.Scoping | |
Pretty ScopeError Source # | |
Defined in PlutusCore.Check.Scoping pretty ∷ ScopeError → Doc ann Source # prettyList ∷ [ScopeError] → Doc ann Source # |
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 ∷ BindingRemoval → 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 (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 Source #
The type of errors that the scope checking machinery returns.
Instances
PrettyBy config (t NameAnn) ⇒ PrettyBy config (ScopeCheckError t) Source # | |
Defined in PlutusCore.Check.Scoping prettyBy ∷ config → ScopeCheckError t → Doc ann Source # prettyListBy ∷ config → [ScopeCheckError t] → Doc ann Source # | |
Show (t NameAnn) ⇒ Show (ScopeCheckError t) Source # | |
Defined in PlutusCore.Check.Scoping |
∷ 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.