support for generalized heating/cooling for contexts

[denis-bogdanas]

Please add support for generalized heating/cooling with the same features and syntax that currently exist for generalized strictness. I need this for java semantics.

The most pressing feature that I need is the ability to specify a result predicate for cooling other than KResult.

[grosu]

But don't we have it already? I thought that Traian and Dorel added, with Radu's support.

[traiansf]

I think we have it. But perhaps we should document how it can be used with contexts and with heating/cooling rules.

[denis-bogdanas]

Looks like extended contexts work, but the syntax of attributes is not entirely clear.

First I tried the following:

context elab('Catch(HOLE,, )) when getKLabel(HOLE) =/=KLabel 'elabRes`(`) [context(result(Int))]

This one don't work. Second, I tried Traian's suggestion:

context elab('Catch(HOLE,, )) when getKLabel(HOLE) =/=KLabel 'elabRes`(`) [result(Int)]

this one works. Traian, can you please copy-paste and adapt the examples for strictness from to-be-processed.txt?

[denis-bogdanas]

I'm trying to define the following sort to be used as a result sort:

syntax ElabRes ::= "elabRes" "(" K ")" syntax ElabRes ::= TypedExp | KResult

kompile error: [Error] Compiler: KResult is only allowed in the left hand side of syntax.

How can I define a sort that includes KResult?

[traiansf]

Short answer: you cannot define a sort that includes KResult.

Long answer: you can define a sort and then extend its predicate to include KResult:

syntax ElabRes ::= "elabRes" "(" K ")" syntax ElabRes ::= TypedExp

rule isElabRes(K:KResult) => true

but you will be going "where no one has gone before"...

2014-02-08 Denis Bogdanas notifications@github.com:

I'm trying to define the following sort to be used as a result sort:

syntax ElabRes ::= "elabRes" "(" K ")" syntax ElabRes ::= TypedExp | KResult

kompile error: [Error] Compiler: KResult is only allowed in the left hand side of syntax.

How can I define a sort that includes KResult?

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/241#issuecomment-34540479 .

[dlucanu]

Denis, you say that tou are "trying to define the ElabRes to be used as a result sort". I think if this is you really want, you should write

syntax KResult ::= ElabRes

For the opposite, Traian's suggestion is the only solution. Dorel

On 2/8/14 12:34 PM, traiansf wrote:

Short answer: you cannot define a sort that includes KResult.

Long answer: you can define a sort and then extend its predicate to include KResult:

syntax ElabRes ::= "elabRes" "(" K ")" syntax ElabRes ::= TypedExp

rule isElabRes(K:KResult) => true

but you will be going "where no one has gone before"...

2014-02-08 Denis Bogdanas notifications@github.com:

I'm trying to define the following sort to be used as a result sort:

syntax ElabRes ::= "elabRes" "(" K ")" syntax ElabRes ::= TypedExp | KResult

kompile error: [Error] Compiler: KResult is only allowed in the left hand side of syntax.

How can I define a sort that includes KResult?

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/241#issuecomment-34540479 .

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/241#issuecomment-34540634.

[denis-bogdanas]

I tested the following context rule:

context elab(KL:KLabel(HeadKs:KList,, (HOLE:K => elab(HOLE)),, _:KList)) [result(ElabKResult), transition-strictness]

It get stuck on a term like:

elabRes (blah) ~> elab ( (foo( HOLE, ...)))

Here elabRes(blah) is of sort ElabKResult, so it should be cooled. But the maude rule indicate that it expects the ElabKResult to be wrapped into elab() in order to be cooled. The maude cooling rule wants a term like:

elab(elabRes (blah)) ~> elab ( (foo( HOLE, ...)))

Traian, is this the intended behavior or something is wrong?

[traiansf]

Yes, this is the intended behavior. The heat/cooling rules are/ should be always symmetrical.

Therefore, if your heating rule is rule elab(KL:KLabel(HeadKs:KList,, (H:K),, :KList)) => elab(H) ~> elab(KL:KLabel(HeadKs:KList,, (HOLE),, :KList)) then your cooling rule will be rule elab(H) ~> elab(KL:KLabel(HeadKs:KList,, (HOLE),, :KList)) => elab(KL:KLabel(HeadKs:KList,, (H:K),, :KList))

2014-02-08 Denis Bogdanas notifications@github.com:

I tested the following context rule:

context elab(KL:KLabel(HeadKs:KList,, (HOLE:K => elab(HOLE)),, _:KList)) [result(ElabKResult), transition-strictness]

It get stuck on a term like:

elabRes (blah) ~> elab ( (foo( HOLE, ...)))

Here elabRes(blah) is of sort ElabKResult, so it should be cooled. But the maude rule indicate that it expects the ElabKResult to be wrapped into elab() in order to be cooled. The maude cooling rule wants a term like:

elab(elabRes (blah)) ~> elab ( (foo( HOLE, ...)))

Traian, is this the intended behavior or something is wrong?

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/241#issuecomment-34546398 .

[denis-bogdanas]

Regarding the example above. I need to be able to write syntax ElabRes ::= TypedExp | KResult

Can someone explain me why KResult is forbidden to appear in the RHS of a syntax declaration? I guess since we have generalized strictness this should no longer be useful in any way. KResult is just like any other sort.

[denis-bogdanas]

By the way, here is a lengthy post in my task management application, explaining why in the end I cannot use context rules in the main part of java elaboration phase. Short answer: context rules with rewrites require the result to be wrapped in the same wrapper as the heating rule. This is too restrictive to my usage scenario.

http://java-semantics.myjetbrains.com/youtrack/issue/KJ-14#comment=87-3

[denis-bogdanas]

Since I gave up using generalized contexts for the semantics, I'm closing this bug. Soon I might write a mail about the design pattern that I used.