search

eclipse / xsemantics

Xsemantics is a DSL (implemented in Xtext itself) for writing type systems, reduction rules, interpreters (and in general relation rules) for languages implemented in Xtext. It then generates Java code that can be used in your language implemented in Xtext for scoping and validation (it can also generate a validator in Java).
Eclipse Public License 1.0
32 stars 19 forks source link

Closely related rules and checkrules are far away #150

Open SimonCockx opened 2 years ago

SimonCockx commented 2 years ago

Following the guidelines of Type errors for the IDE with Xtext and Xsemantics of a certain Lorenzo Bettini, I noticed that when I want to implement a typing rule using XSemantics, the rule gets split up in one rule statement for inference and (at least) one checkrule statement for validation. However, currently in XSemantics one must first specify all the rules, and only then all of the checkrules, so these rules/checkrules that belong to each other tend to be far away, which makes it easy to lose overview.

I would suggest to allow mixing rules and checkrules, e.g.,

rule TAddition ... // infer that an addition such as `1 + 2` results in an `integer`
checkrule CheckAddition ... // check that both arguments of an addition are of type `integer`

rule TNot ... // infer that a boolean `not` operator results in a `boolean`
checkrule CheckNot ... // check that the argument of a boolean `not` is of type `boolean`

I guess this would only need a minimal change to the grammar definition.

LorenzoBettini commented 2 years ago

A minimal change in the grammar, but on the compilation side, it requires a few adjustments due to the new abstraction... I'll see what I can do, but I can't promise I can handle this ASAP ;)