Java rewrite engine4

delete all klabels and change all when -> requires
I confess that I do not like this!   We should not make functions things which are not meant to be functions only to trick the engine execute them as anywhere rules.  Please keep comments in the semantics where you've done that, so we can come back and change them later.  This "easiest solution" now will hurt us later when we kompile to other backends, for example Coq, and realize that they are actually not functions.

Please see my previous message about [anywhere] rules as a reply to Cosmin's message.  I think what we need is a slightly more general mechanism to deal with anywhere rules, without radical changes to the engine and which includes the current function annotations.  Basically, what I hope, is that we can apply the anywhere rules the same way we apply the function rules, immediately after every rewrite, the only difference between functions and other operations being that the functions are supposed to disappear from the term once evaluated, while other operations may remain.  Hopefully that is possible without a huge performance hit.

Grigore


________________________________
From: Liyi Li [notifications@github.com]
Sent: Saturday, July 26, 2014 5:50 PM
To: kframework/c-semantics
Cc: Rosu, Grigore
Subject: Re: [c-semantics] Java rewrite engine4 (#30)


In semantics/language/common/syntax.k:

>
> -     syntax Constant ::= NoSuffix(K) [klabel('NoSuffix)]
> +     syntax Constant ::= NoSuffix(K) [function]


I make it a function to solve the [anywhere] issue. It is the easiest solution.

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/c-semantics/pull/30/files#r15436291>.