K-user mailing list

[Emmanuel Castro <emmanuel.castro AT laposte.net>]

Thank you for the light you shed on this problem. Your mails are worth copy-and-pasting to K tutorials ;-)

Emmanuel

2013/4/5 Rosu, Grigore <grosu AT illinois.edu>

Hi Emanuel,

 

This is a feature :)  In fact, a quite important one.

 

Although you define your concrete syntax in K, in fact, semantically speaking, all syntax is only a user convenience in K for defining what we call "sort membership predicates" that you are free to use in your definitions explicitly (the isA predicate you used in your rule).

 

There are very good reasons why you don't want to enforce constructs to take arguments of the declared types in a definition.  For example, imagine that you want to define a type system in K which works like in the tutorial: rewrite a program iteratively until you get a type, its type.  The rule for addition is then

 

rule int + int => int

 

Since in K all syntax gets eventually sunk into the K top-level syntactic category, by default, K assumes that any variables which are not typed explicitly have the type K.  So in your case,

 

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

A and B have the types K (meaning that they can be syntactically anything), while the side condition will make sure that the rule will only apply if, at runtime, the first subtern of + has the type A (which may not always be the case, precisely because in K you can potentially disobey the syntax during the rewriting process).

 

That being said, note that K's parser is making hard efforts to catch typing errors in your definitions.  For example, semantically speaking, your rule is equivalent to the following:

 

  rule A:A + B => B + A                                                        

where you type A with its sort in place, not in the side condition.  Now the K parser will report an error here:

 

[Error] Critical: Type error detected. Expected sort B, but found A
 File: /home/grosu/try/try.k
 Location: (6,23,6,24)

That's because in addition to the semantic membership condition it also assumes that A has the syntactic type A, which should make sense statically everywhere in the rule.

 

All these variations came from needs that K users have and because we do not want to restrict people due to syntactic reasons.

 

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Emmanuel Castro [emmanuel.castro AT laposte.net]
Sent: Friday, April 05, 2013 10:04 AM
To: k-user AT cs.uiuc.edu
Subject: [K-user] Typing bug of feature

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