k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] Typing bug of feature

From: Emmanuel Castro <emmanuel.castro AT laposte.net>
To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: [K-user] Typing bug of feature
Date: Fri, 5 Apr 2013 17:04:15 +0200
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

Transformation can produce syntactically invalid terms.
Consider the K language below. It transforms a+b into b+a, without complaining but only a+b is syntactically valid.

Is it a bug or is it a feature?

Note:
If Kompile was able to infer types from syntax, it would produce:
rule A:A + B:B => B + A when isA(A)
And it would end into a type error.

-------------------

module T

syntax Expr ::= A "+" B

syntax A ::= "a"
syntax B ::= "b"

rule A + B => B + A when isA(A)

configuration
    <T>
      <k> $PGM:Expr </k>
    </T>

endmodule

[K-user] Typing bug of feature, Emmanuel Castro, 04/05/2013
- Re: [K-user] Typing bug of feature, Traian Florin Șerbănuță, 04/05/2013
- Re: [K-user] Typing bug of feature, Rosu, Grigore, 04/05/2013
  - Re: [K-user] Typing bug of feature, Emmanuel Castro, 04/05/2013