K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

Hi,

These are needed because of how we parse concrete syntax in rules.

Let's look at a simple example:

syntax Int ::= Int "+" Int [klabel(PlusInt)]

syntax String ::= String "+" String [klabel(PlusString)]

syntax Exp ::= Int | String

syntax Stm ::= Exp ";"

rule A + B => .K

In this case, there is no way possible to automatically infer what operation is wanted there, since there is no context.

The sort annotations are supposed to allow the users to reintroduce the context and avoid parsing ambiguities.

Exp ::= Exp ":Exp" 

Exp ::= Exp "::Exp" // equivalent to "<:>"

Exp ::= K ":>Exp"

KBott  ::= Exp "<:Exp"

These are the four annotation types. The first one is special since it adds a runtime check on any annotated variable.

For the example above, saying:

rule A:String + B:String => .K

would remove the ambiguity warning.

The second one is exactly like the first, but it doesn't add the runtime check.

The third can be used as a wrapper for any type of term, and be forcefully inserted in a place where an Exp is expected.

rule 1 ; + 2 => .K  // would normally fail

rule 1 ; :>Int + 2 => .K // now works.

The fourth one is the opposite. Can take a term of sort Exp, and forcefully insert it anywhere.

rule 1 ; <:Stm + 2 => .K // now works.

The arrow points to where the type checker is going to be strict.

Using the last two is not recommended, but can be useful sometimes.

Hope this clarifies things a bit.

Radu

On Wed, Nov 23, 2016 at 4:05 PM, Mihály Palenik <palenik.mihaly AT gmail.com> wrote:

Hello,

I hope this is the appropriate places to write my question. I read a lot of things in github's wiki about K. I found Sort Annotation part of Manual but for me it is not clearly what means these signs: :,::,<:,:>,<:>. Somebody can explain to me?

Thank you your help in advance.

Best regards,

Mihály Palenik