Migrate to Statix from NaBL2¶
Signature¶
All sorts and constructors must be explicitly defined in Statix in
sorts
and constructors
signatures. Sorts in Statix
are mostly similar to terms in NaBL2. Notable differences:
- There is no catch-all sort
term
in Statix. - There are no sort variables in Statix.
- List sorts in Statix are written as
list(X)
for some sortX
.
Statix signatures for language syntax can be generated from SDF3 definitions with the signature generator.
Name-resolution¶
Name resolution in NaBL2 heavily relies on occurrences and their unique identity. In Statix, the notion of a stand-alone reference is replaced by the notion of a query. Therefore, the use of occurrences is now discouraged in favour of regular terms, relations, and and predicates for the different namespaces.
signature
namespaces
Var
name resolution
labels P
well-formedness P*
order D < P
rules
[[ Def(x, T) ^ (s) ]] :=
Var{x} <- s,
Var{x} : T.
[[ Var(x) ^ (s) : T ]] :=
Var{x} -> s,
Var{x} |-> d,
d : T.
signature
relations
var : string * TYPE
name-resolution
labels P
rules
declareVar : scope * string * TYPE
declareVar(s, x, T) :-
!var[x, T] in s.
resolveVar : scope * string -> TYPE
resolveVar(s, x) = T :-
{x'}
query var
filter P* and { x' :- x' == x}
min $ < P and true
in s |-> [(_, (x, T))],
@x.ref := x'.
rules
stmtOk : scope * Stmt
stmtOk(s, Def(x, T)) :-
declareVar(s, x, T);
typeOfExp : scope * Exp -> TYPE
typeOfExp(s, Var(x)) = T :-
T == resolveVar(s, x).
Things to note:
- Each namespace gets its own relation, and set of predicates to
declare and resolve in that namespace (
declareXXX
andresolveXXX
). - The regular expression and order on labels is not global anymore,
but part of the query in the
resolveXXX
rules. - If a declaration should have a type associated with it, it is now
part of the relation. The fact that it appears after the arrow
->
indicates that each declaration has a single type. As a result,declareXXX
combines the constraintsXXX{...} <- s, XXX{...} : T
. Similarly,resolveXXX
combines the constraintsXXX{...} -> s, XXX{...} |-> d, d : T
. - The end-of-path label, called
D
in NaBL2, now has a special symbol$
, instead of the reserved name.
Functions¶
NaBL2 functions can be translated to Statix predicates in a straight-forward manner. Note that if the function was used overloaded,it is necessary to defined different predicates for the different argument types.
signature
functions
plusType : (Type * Type) -> Type {
(IntTy() , IntTy() ) -> IntTy(),
(StrTy() , _ ) -> StrTy(),
(ListTy(a), a ) -> ListTy(a),
(ListTy(a), ListTy(a)) -> ListTy(a)
}
plusType : Type * Type -> Type
plusType(IntTy() , IntTy() ) = IntTy().
plusType(StrTy() , _ ) = StrTy().
plusType(ListTy(a), a ) = ListTy(a).
plusType(ListTy(a), ListTy(a)) = ListTy(a).
Relations¶
Relations as they exist in NaBL2 are not supported in Statix.
An example of a subtyping relation in NaBl2 would translate as follows:
signature
relations
reflexive, transitive, anti-symmetric sub : Type * Type {
FunT(-sub, +sub),
ListT(+sub)
}
rules
[[ Class(x, superX, _) ^ (s) ]] :=
... more constraints ...,
ClassT(x) <sub! ClassT(superX).
[[ Def(x, T, e) ^ (s) ]] :=
[[ e ^ (s) : T' ]],
T1 <sub? T2.
rules
subType : TYPE * TYPE
subType(FunT(T1, T2), FunT(U1, U2)) :-
subType(U1, T1),
subType(T2, T1).
subType(ListT(T), ListT(U)) :-
subType(T, U).
subType(ClassT(s1), ClassT(s2)) :-
... check connectivity of s1 and s2 in the scope graph ...
In this case implementing the subType
rule for ClassT
requires
changing the encoding of class types. Instead of using names, we use
the class scope to identify the class type. This pattern is know as
Scopes as Types. Subtyping between class scopes can be checked by
checking if one scope is reachable from the other.
Rules¶
NaBL2 constraint generation rules must be translated to Statix predicates and corresponding rules. Predicates in Statix are explcitly typed, and a predicate has to be defined for each sort for which constraint generation rules are defined.
Here are some example rules for expressions in NaBL2:
[[ Let(binds, body) ^ (s) : T ]] :=
new s_let, s_let -P-> s,
Map1[[ binds ^ (s, s_let) ]],
[[ body ^ (s_let) : T ]].
[[ Bind(x, e) ^ (s, s_let) ]] :-
[[ e ^ (s) : T ]],
Var{x} <- s_let,
Var{x} : T.
In Statix these would be encoded as:
typeOfExp : scope * Exp -> TYPE
typeOfExp(s, e@Let(binds, body)) = T :- {s_let}
new s_let, s_let -P-> s,
bindsOk(s, binds, s_let),
T == typeOfExp(s_let, body),
@e.type := T.
bindOk : scope * Bind * scope
bindsOk maps bindOk(*, list(*))
bindOk(s, Bind(x, e), s_let) :- {T}
T == typeOfExp(s, e),
declareVar(s_let, x, T).
Created: October 1, 2024