Scope Graph Constraints¶

One of the core concepts of Statix is modelling name binding structures using scope graphs. Scope graphs consist of three different components, summarized in the following table.

Component	Description	Textual Notation	Graphical notation
Scope	Region in a program with uniform behavior wrt. name resolution. Represented as nodes in a graph.	`#1`	Circular node
Edge	Directed edges with upper-case labels model reachability between scopes.	`#1 -L-> #2`	Labeled arrow
Declaration	Declarations associate data terms with a particular scope under a particular relation.	`#1 \|-r-> d`	Labeled block arrow

Using these components, and leveraging the fact that scopes are regular terms, many name-binding patterns can be modelled. In the remainder of this section, we will explain how scope graph constraints can be expressed in the Statix language.

Scopes¶

First, scopes can be created using the new keyword:

new $Var+

For each var in the list of variables provided to the new constraint, a fresh scope is generated, and bound to that particular variable. Note that the $Vars are not introduced by this constraints, but rather have to be introduced earlier in a rule head or using an existential constraint.

Statix guarantees that each scope has a unique identity. Scopes that are generated by different new constraints can never be equal under the equality constraint.

Edges¶

The existence of edges in a scope graph can be asserted using edge assertion constraints:

$Term -$Label-> $Term

This constraint ensures that an edge from the first term argument to the last argument (which must have type scope) with a label $Label exists.

Edge Assertions not Idempotent

Edge constraints are not idempotent. That is, repeated edge assertions will result in multiple equivalent edges in a scope graph. However, because query results have set semantics, and edges have structural identity, declarations reached via such a duplicated edge will not be duplicated in a query answer.

For example (assuming familiarity with queries and tests), the constraint:

{R s1 s2}
  new s1 s2,
  s1 -P-> s2,
  s1 -P-> s2,
  query () filter P in s1 |-> R

will give the following (slightly simplified) result:

substitution
  R |-> [(PathStep(PathEmpty(#s1), P, #s2), #s2)]

analysis
  scope graph
    #s1 {
      edges {
        P : #s2
            #s2
      }
    }

In this result, the P edge is duplicated in the scope graph, but there is still only a single query result.

It is required to declare edge labels in a signature section:

signature

  name-resolution
    labels
      $Label+

Label are just uppercase identifiers. They must adhere to the following regular expression: [A-Z] [A-Za-z0-9\_]. It is not allowed to shadow label names, nor may modules import equivalent label names from different modules.

Declarations¶

Declarations in a scope graph can be asserted as follows:

!$Relation[$Term*] in $Scope

This constraint asserts that the terms inside the square brackets are associated with scope $Scope under relation $Relation.

Regarding the static semantics of this constraint, $Scope is a term which should have type scope. Additionally, the term arguments must adhere to the signature of the relation. The signature of a relation must be provided in a signature section:

signature

  relations
    $Relation : {$Type "*"}*

Just as rules, relations can alternatively be declared in a functional style:

$Relation : {$Type "*"}* -> $Type

The style of declaration is importand when doing queries, but asserting declarations is similar for both types of relations. When asserting a declaration for a functional relation, the terms that the relation maps to should be provided as the last term in the square brackets.

Instead of in a signature section, relations can be declared in a rules section as well.

It is allowed to have multiple declaration assertions for a single relation in the same scope, even when the data of the different relations are equivalent. In the latter case, multiple equivalent declarations will be inserted in the scope graph.

Permission to Extend¶

In order to make query execution sound, Statix statically limits to which scopes new edges or declarations may be added (adding a edge or declaration is often called extending). Scope extension is only allowed in the following cases:

Scopes that are freshly instantiated in a rule using new constraints may be extended by that rule, and any user-defined constraint that is instantiated by that rule.
Scopes that are passed as direct argument to a rule may be extended by that rule, given that the scope may be extended by rule that instantiated that constraint. This property is validated at the instantiation site.
Uninstantiated scope variables that are passed directly to a user-defined constraint in which they are instantiated may be extended by the outer constraint as well. However, this does not hold for input/output values of functional rules

These rules prevent extension of scopes that are obtained by pattern matching/ deconstruction.

Namespaces and Occurrences¶

Warning

Since Spoofax 2.5.15, namespaces and occurrences are deprecated.

Last update: October 17, 2024
Created: October 17, 2024