You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Sometimes the presence of feedback messages as per Spoofax 2 docs causes drastic changes in the type checking.
For example, if typeOfExp(s, e) == _ works, then typeOfExp(s, e) == _ | error $[Invalid expression] breaks (as in returns an error for the same input).
What you did
I ran into this when defining static semantics for the chocopy language.
I played around with making the basic types such as int etc. part of the class hierarchy and modelled them using scopes as types. This broke my type checking and it turned out that feedback messages were the cause of this.
What you expected to happen
I would expect 1 * 1 to type check given this syntax definition
module start
context-free start-symbols
Start
context-free sorts
Start
Exp
context-free syntax
Exp.Int = NUM
Exp.Mul = <<Exp> * <Exp>> {left}
Start.Exp = Exp
lexical sorts ID NUM
lexical syntax
ID = [a-zA-Z]+
NUM = [0-9]+
LAYOUT = [\ \n\v\f\r\t]
lexical restrictions
ID -/- [a-zA-Z]
NUM -/- [0-9]
context-free restrictions
LAYOUT? -/- [\ \n\v\f\r\t\#]
and this static code
module main
imports
signatures/start-sig
signature
sorts
TYPE
constructors
CLASS : scope * ID -> TYPE
INT : TYPE
relations
type : ID -> TYPE
rules
int : scope -> TYPE
int(s) = T :-
typeOfType(s, "int") == T@CLASS(_, "int").
rules
typeOfExp : scope * Exp -> TYPE
typeOfExp(s, e@Int(_)) = I :-
int(s) == I,
@e.type := I.
typeOfExp(s, e@Mul(l, r)) = int(s) :-
typeOfExp(s, l) == int(s), // adding error feedback here breaks things too
typeOfExp(s, r) == int(s), // | error $[Expected "int"],
@e.type := int(s).
// not having class types works, but defeats the purpose
/*
typeOfExp(s, e@Int(_)) = INT() :-
@e.type := INT().
typeOfExp(s, e@Mul(l, r)) = INT() :-
typeOfExp(s, l) == INT() | error $[Expected [INT()]]@l,
typeOfExp(s, r) == INT() | error $[Expected [INT()]]@r,
@e.type := INT().
*/
rules
programOk : Start
programOk(Exp(e)) :- {s int}
new s int,
declareClass(s, "int", int),
// no message works
// typeOfExp(s, e) == _.
// this fails
typeOfExp(s, e) == _ | error $[Invalid expression].
// fails too
// try { typeOfExp(s, e) == _ } | error $[Invalid expression].
rules
declareClass : scope * ID * scope
declareClass(s, id, c) :- {C}
!type[id, C@CLASS(c, id)] in s,
resolveType(s, id) == [(_, (_, C))]
| error $[Duplicate declaration of type [id]],
@id.type := C.
resolveType : scope * ID -> list((path * (ID * TYPE)))
resolveType(s, id) = ps :-
query type
filter e and {id' :- id' == id}
min and true
in s |-> ps.
typeOfType : scope * ID -> TYPE
typeOfType(s, id) = T :- {id'}
resolveType(s, id) == [(_, (id', T))]
| error $[Undefined type [id]],
@id.type := T, @id.ref := id'.
Thanks for reporting. Indeed there is an issue that properties cannot be assigned to non-AST terms, such as the "int" in your int() predicate. These are ignored by default, setting a custom message on a parent constraint incorrectly overrides that. See also the announcement on Mattermost.
@Gohla I'd prefer to keep this issue open, because some error message code is duplicated, and perhaps I need to update the Spoofax 3 implementation as well.
Spoofax 3 correctly reuses these results (either by direct invocation or via the STX_extract_messages primitive), so the issue can be closed once the changes are merged in.
Summary
Sometimes the presence of feedback messages as per Spoofax 2 docs causes drastic changes in the type checking.
For example, if
typeOfExp(s, e) == _
works, thentypeOfExp(s, e) == _ | error $[Invalid expression]
breaks (as in returns an error for the same input).What you did
I ran into this when defining static semantics for the chocopy language.
I played around with making the basic types such as
int
etc. part of the class hierarchy and modelled them using scopes as types. This broke my type checking and it turned out that feedback messages were the cause of this.What you expected to happen
I would expect
1 * 1
to type check given this syntax definitionand this static code
What actually happened
I got the error
However, without error feedback, the outcome is as expected.
Context
Additional information
The example Spoofax project can be found here and another version with more cases of hopefully the same bug here.
The text was updated successfully, but these errors were encountered: