option for strict kompilation

[grosu]

I've met many people who prefer to define languages purely syntactically, that is, where each term that appears at any moment during the application of their rules parse correctly according to their defined grammar. For such people, allowing a term of a certain sort on a position where a different sort is expected during rewriting indicates a serious problem, one that they would like to be aware of. For example, if in their definition they have sorts Exp and Val then they add closures to Val but forget to subsort Val to Exp, then they would be happy to see their computations get stuck with terms of the form closure(...) 7. That would be a good reminder for them that they should add Exp ::= Val.

I therefore propose a strict kompilation mode, where all the inferred sorts for all the variables that appear in all rules are checked at runtime. We may go even further with this, and have a kompiler step which adds these runtime checks to any K definition, based entirely on the declared sorts in the productions corresponding to KLabels.

[laurayuwen]

Added to K Wish List, BTW, I think it would be good to add a link from list items to issues if they are extracted from issues.

[andreistefanescu]

I think the tool already checks all in inferred variable sorts at runtime in the rule left-hand side. @grosu can you add a concrete example to this issue?

[grosu]

Hm, are you saying that if I have

syntax Stmt ::= Id "=" Exp 

and write

rule <k> X = I:Int => . ...</k> <state>... X |-> (_ => I) ...</state>

then a runtime check for X:Int will take place, while if I write

rule <k> X::Id = I:Int => . ...</k> <state>... X |-> (_ => I) ...</state>

then a runtime check will not take place?

An example could be the above as part of some definition, where for some reason one may want to extend the Id without adding to the existing syntactic category, but doing something like

rule (X:Id => mkMyId(X)) = _

where

syntax MyId ::= "mkMyId" Id   [function]
...

[andreistefanescu]

@grosu you are correct regarding the 2 rules you wrote above. Another example is rule I1 + I2 => I1 +Int I2 which is correct because I1 and I2 are inferred as Int.

Regarding the second part, right now if you change Id to MyId, then the first rule will not apply, while the second will.

[grosu]

Can you guys explain this in the Manual? Maybe have @radumereuta do it. This is contrast to what we say in the Tutorial (lambda, lesson 2):

Variables may be explicitly tagged with their syntactic category (also called sort). If tagged, the matching term will be checked at run-time for membership to the claimed sort. If not tagged, then no check will be made. The former is safer, but involves the generation of a side condition to the rule, so the resulting definition may execute slightly slower overall.

I remember we wanted to avoid writing sorts in

rule I1 + I2 => I1 +Int I2

but on the other hand we now always pay the runtime overhead of sort checking, which may be non-negligible, especially when people write their own rules for isSort.

[radumereuta]

Well... I don't know what happens in the backend, but all the variables that leave the front end, have two fields: sort:Sort and userTyped:boolean.

I do this for all variables because I need to disambiguate and type check, but I don't know how this information is being used in the backend. I think in the maude-backend an inferred variable was ignored, and only the user specified ones were checked at runtime, but the java-backend may be doing something else.

[dwightguth]

@grosu are you still interested in pursuing something here? it's not entirely clear what the correct intended use case is in the new parser for this.