Skip to content

Rules

User-defined constraints and their rules make up the main part of a Statix specification. In this section, we describe the definition and usage of user-defined constraints and their rules.

Constraint Definitions

In order to define a custom constraint, its type must be declared first. A constraint can be declared in a rules section, or in a constraints subsection of a signature section.

A constraint is declared by specifying its name and argument type. For more information on types, please refer to the Terms section. Note that the name of the constraint must be unique within a specification.

$ConstraintName : {$Type "*"}*

Terminology

In this reference manual, we consistently use the term 'constraint declaration' for the introduction of new user-defined constraints. However, in practise, these are sometimes also referred to as 'predicate' or just simply 'constraint'.

When a constraint declaration is provided this way, it can be used as a constraint by providing concrete arguments, separated by comma's.

$ConstraintName({$Term ","}*) $Message?

The sorts of the argument terms should be equal to the sorts in the constraint declaration.

Rule Definitions

When solving a user-defined constraint, a rule for that constraint is unfolded in order to infer a model satisfying the constraint.

[$RuleName]$ConstraintName({$Pattern ","}*) :- $Constraint.

The part before the turnstile (:-) is often referred to as the head of the rule, while the $Constraint after the turnstile is denoted as body. When applying a rule, each head pattern (which is just a term) will be matched with its corresponding actual argument.

Statically, the sorts of the terms in $Patterns are type-checked based on the constraint declaration. Any variables in patterns are implicitly introduced in the scope of the rule. Patterns can be non-linear. That is, a variable may occur multiple times in a pattern. Operationally, the subterms at these positions are then required to be structurally equal.

Note that multiple rules for a single constraint can, and often will, be provided. For each constraint, the rule that is used for simplification is determined by the guard of the rule. This guard is derived from the head pattern: a rule can only be applied when the constraint arguments match the patterns.

During constraint solving, Statix will try at most one rule for each constraint. The appropriate rule is selected by applying the following heuristics in order: 1. Rules with a smaller domain are preferred over rules with a larger domain. 2. When pairwise comparing rules, the rule for which, in left-to-right order, a more specific pattern is encountered first is preferred over the other. For all cases where these heuristics do not decide which rule to use for a constraint, compile time "Overlapping patterns" errors will be emitted.

The $RuleName is just a name that can be used for documentation purposes. It cannot be referenced from any position in the specification, and may be omitted altogether.

Axiom rules

In some cases, a constraint trivially holds for particular inputs. For such constraints, an axiom rule can be specified.

[$RuleName]$ConstraintName({$Pattern ","}*).

This rule is similar to a regular rule, but lacks a body. When applying such a rule, no new constraints are introduced, reflecting the fact that the constraint trivially holds for these arguments.

Functional Rules

Some user-defined constraints can be thought of more naturally as a function: a constraint where a particular term is inferred by the constraint, rather than validated. Statix allows to write constraints in a functional idiom as follows:

First, a constraint declaration for such 'functional constraints' must be provided as follows:

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

In addition to the regular list of input sorts, a sort for the output term is provided to the constraint declaration.

Rule definitions for a functional constraint look as follows:

[$RuleName]$ConstraintName({$Pattern ","}*) = $Term :- $Constraint.

Compared to predicative rule definitions as introduced earlier in this section, an additional term after an equality-sign is appended to the rule head. This term denotes the output term (the term inferred by the rule).

A functional constraint can be used in a term position, as opposed to a constraint position for predicative rules. Otherwise, their syntax is the same.

$ConstraintName({$Term ","}*)

Semantically, the output term of applying the constraint is substituted at the position of the application of the functional predicate.

Terminology: Functional vs. Predicative

When we want to make the distinction between these two forms of constraints explicit, we usually refer to either groups with 'predicative constraint declarations' and 'predicative constraints', versus 'functional constraint declarations' and 'functional constraints', respectively.

Normalization

Every specification with functional predicates is normalized to a form with only regular predicates. To show the normal form of a specification in Eclipse, use the Spoofax ‣ Syntax ‣ Format normalized AST menu action.

Mapping rules

Another common pattern in Statix is defining a predicate that instantiates a predicate for all elements in a list. Statix allows derive such mapping rules using the maps keyword as follows:

$MappingConstraintName maps $MappedConstraintName({$Lift ","}*)

A lift specifier ($Lift) can be one of the following:

  • *: The identity lift. This lift specifier indicates that this argument is passed to the mapped constraint unchanged.
  • list(*): The list lift: This lift specifier indicates that the mapped constraint will be instantiated for each element in the list at that argument position. Each constraint defined with maps, must contain at least one list lift. Otherwise, the mapping would be a no-op.
  • ({$Lift ","}+): The tuple lift: This lift specifier indicates that arguments are extracted from a tuple. For each tuple argument, a corresponding lifting is applied afterwards.

The type of $MappingConstraintName is inferred by inverse application of the lift specifiers to the type of $MappedConstraintName. Therefore, no explicit declaration of the type of the mapping constraint is required.

Similar to predicative constraints, functional mapping constraints can be derived:

$MappingConstraintName maps $MappedConstraintName({$Lift ","}) = $Lift

In addition to lift specifiers of the input arguments, a lift specifier for the inferred term must be provided as well. This lift specifier indicates how the inferred terms from the mapped constraints are aggregated and returned by the mapping constraint.

Example. A common example where mapping rules are used is when type-checking a list of declarations. A specification snippet for that could look as follows:

rules

  declOk: scope * Decl
  declsOk maps declOk(*, list(*))

  // rules for declOk

In this snippet, the declsOk constraint instantiates declOk for each declaration in a list of declaration. Its inferred type is scope * list(Decl).

When mapping functional constraints, a lift specifier for the inferred term must be provided as well. This lift specifier indicates how the inferred values of the mapped constraint are returned by the mapping constraint.

When using multiple list lifts in the input, the resulting constraint will zip the arguments. This implicitly requires the input lists to be of equal length. The creation of a cartesian product can be achieved by repeated application of the maps construct for each argument.

Normalization

Similar to functional constraints, constraints derived using the maps construct are normalized to regular predicative constraints. This normalization can be inspected using the Spoofax ‣ Syntax ‣ Format normalized AST menu action.

Injections of Namespaces and Relations

For convenience, it is possible to declare namespaces, namespace queries (both deprecated) and relations in a rules section as well.

rules

  namespace Var: string
  resolve Var
    filter P* I*

  relations
    var: string -> TYPE
Last update: October 17, 2024
Created: October 17, 2024