new KAST

[cos]

We use this issue to track the development of the new KAST syntax and data structures.

The idea is to have two versions of KAST. The first is is meant to blend well with the full K syntax (i.e. outer with concrete syntax). It's outer syntax is the same as the one for parsing concrete definitions, and its inner syntax has some sugar to make things easier to write (e.g., it has requires and ensures). The second version, which we call "KAST core", has only the minimal syntax necessary to express everything, and it is meant to have a direct correspondence with the underlying data structures, i.e., to the KAST API.

The KAST regular syntax is here: https://github.com/kframework/k/blob/kast-in-K/samples/kast/kast-new.k

The KAST core syntax is here: https://github.com/kframework/k/blob/kast-in-K/samples/kast/kast-core.k

Radu is preparing the two-stage parser in the parseInModule branch.

This is a work in progress. We will bug everybody once things get close to a stable version.

A short summary of the issues we discussed so far, and their resolutions (where there is one):

• [x] merging KItem with K -- discussion postponed for after we have a stable version of the new KAST
• [x] syntax for KAttribute
• [ ] syntax for adding KAttributes to any KItem
• [x] syntactic sugar for KAST -- solved by having a "KORE" version of KAST
• [ ] syntax for priorities over previously-defined productions -- likely will postpone discussion

[cos]

@grosu , in core, since we already flattened the various sentences, should we also flatten the Import. Is it particularly important that all imports are put in the beginning of the file?

[cos]

Highlighted several other issues, and put hook attributes. See: https://github.com/cos/k/blob/new-kast/samples/kast/kast-core.k

The Scala implementation of the hooks is here: https://github.com/cos/k/blob/new-kast/src/main/scala/org/kframework/kast/outer/outer.scala

[grosu]

@cos what do you mean to flatten the imports? We want to keep the module structure, and not flatten the modules anymore, but I guess you did not mean that.

[grosu]

OK, thanks! I'm going to start working on this in about 1h, so please push everything you have, send suggestions, etc., so I can take it over in one hour and hopefully be done with it in the afternoon some time.

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Wednesday, September 17, 2014 9:45 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

Highlighted several other issues, and put hook attributes. See: https://github.com/cos/k/blob/new-kast/samples/kast/kast-core.k

The Scala implementation of the hooks is here: https://github.com/cos/k/blob/new-kast/src/main/scala/org/kframework/kast/outer/outer.scala

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

[cos]

@grosu, no, I mean syntax, configuration, etc. put under the KSentence sort, while the import is left separately, i.e., not considered a KSentence

[radumereuta]

You could consider this only as a parsing restriction, since we want users to put the imports at the beginning. For the internal representation you can use the same sort.

[grosu]

Here is a hopefully very close to final attempt to nail down KORE:

https://github.com/kframework/k/blob/kast-in-K/samples/kast/kore.k

@cos @radumereuta Please review and fill in the dots (the attribute dots are the hooks). Let us not sleep tonight until the three of us agree that this is it, we are done with KORE. :)

For those who read this and are not updated with the current discussions: we've decided that there are 3, and not 2, versions of K, namely:

1) Full K, as we know it, which mixes concrete and abstract syntax, and thus it needs a two-phase parser: first extract the defined language syntax, and then generate a parser for the semantics.

2) KAST, which is full K minus the concrete syntax of the user-defined language. For example, you can have

syntax Sort ::= Prod1 [Att]  |  Prod2

in KAST, which is just syntactic sugar for two syntactic declarations in KORE. The advantage of KAST is that we need a one-phase parser for it, so it is expected to be much much faster to parse than Full K.

3) KORE, which is the minimal subset of K and KAST which is powerful enough to express everything we want. For example, the KAST syntax declaration above becomes

syntax Sort ::= Prod1 [Att]
syntax Sort ::= Prod2 []

The advantage of KORE is that it is going to be a perfect textual clone of the internal data-structures that we will use to store K definitions. Those data-structures will also become the "K API", which will allow people to define languages in K using directly Java, skipping completely any textual representation if they choose to.

[cos]

I do like that we don't have a defined syntax for attributes anymore. Still, I would rather have it be a K then a KList. KList enforces that the attributes are an associative list of things. Why are they associative? If we are to keep close to their current semantics, they should be also commutative. Leaving the attributes as K would say that we are not saying anything about them.

[cos]

Ok. I think I finally get it. I committed some larger changes to kore.k. You can take a look at it now, or wait until tomorrow for an in-depth explanation.

[grosu]

Guys, please do not make radical changes to kore.k!!! Because of the critical nature of this definition, I'd rather be fully responsible for it. As said in my message 2 days ago, @radumereuta and @cos, please only fill in the dots and provide comments.

@cos The reason the attributes are a list is because we want to avoid an additional klabel only to wrap them. The fact that they are semantically a set is irrelevant at this stage, for the same reason for which the K sentences are also parsed as a list in spite of semantically being a set.

[cos]

@grosu, in my proposal we simply do not parse the attributes with the outer parser, i.e., we leave them as a bubble. We can then parse them with their own very simple module, something along the lines of:

module K-ATTRIBUTES
  import KAST
  KAttributeList ::= List{K}{","}{".::KAttributeList"}
endmodule

This would allow us to keep the labeled form syntax from leaking into the OUTER definition, in case we agree on the separation in commit discussion .

Also, I can easily revert any of the changes. Let me know if you want me to do so.

[grosu]

Yes, I think you should revert the changes and make your proposal in prose/comments, so I'll think about it. Right now I have to board an airplane and may not be able to answer until tonight.

Cheers, Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Sunday, September 21, 2014 8:52 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

@grosuhttps://github.com/grosu, in my proposal we simply do not parse the attributes with the outer parser, i.e., we leave them as a bubble. We can then parse them with their own very simple module, something along the lines of:

module K-ATTRIBUTES import KAST KAttributeList ::= List{K}{","}{".::KAttributeList"} endmodule

This would allow us to keep the labeled form syntax from leaking into the OUTER definition, in case we agree on the separation in commit discussionhttps://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81 .

Also, I can easily revert any of the changes. Let me know if you want me to do so.

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

[cos]

Ok. I've reverted all my changes.

The proposed changes are now on my k fork: https://github.com/cos/k/blob/kast-in-K/samples/kast/kore.k The changes are documented by separate commits. The discussion regarding the more important change is here: https://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81

[grosu]

But it looks like you have reverted the hooks as well. I wish you included the hooks, because that woulds make you think whether certain constructs are really needed or not. For example, I noticed that the functional notation for production, operation(Sort1, ..., Sortn) was not needed in KORE, because the production notation is more general. But fine, you can include them afterwards, when we are done with the syntax of KORE.

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Sunday, September 21, 2014 4:47 PM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

Ok. I've reverted all my changes.

The proposed changes are now on my k fork: https://github.com/cos/k/blob/kast-in-K/samples/kast/kore.k The changes are documented by separate commits. The discussion regarding the more important change is here: 51ae9d8#diff-805bc26fb25d50ef3c1f020b863f4674R81https://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81

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

[grosu]

Cosmin,

Do I understand it correctly that you have essentially proposed two changes to the existing kore.k:

1) moving things around in different modules, which from your point of view make more sense;

2) Requiring KAttributes to be a K instead of a KList. I assume this based on our discussion, not on your definition, because in your definition you still have

syntax KAttributes ::= "[" KList "]" [...]

which does not even compile, because you do not have KList available in BASIC-K.

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Sunday, September 21, 2014 4:47 PM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

Ok. I've reverted all my changes.

The proposed changes are now on my k fork: https://github.com/cos/k/blob/kast-in-K/samples/kast/kore.k The changes are documented by separate commits. The discussion regarding the more important change is here: 51ae9d8#diff-805bc26fb25d50ef3c1f020b863f4674R81https://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81

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

[cos]

Actually, I am proposing three things:

1. Yes. Move things around in modules as outlined in the commit thread.
2. Yes, there was a bug in the definition -- it should be K instead of KList. The main reason for the change is that we would avoid using KList in a case where it doesn't have anything to do with the labeled form. Thus, we would also avoid the slightly forced step of moving the definition of the KList to a different module than the definition of KLabel. Another reason is that the KAttributes would be parsed as bubbles, thus possibly avoiding ambiguities and allowing us to easily slightly alter attribute syntax if we ever choose to.
3. That we have special syntax for attaching KAttributes to a KItem. I know we can always simulate this using a wrapper, but I think the KAttributes are important enough that they deserve their own syntax. All data structure constructors, both in the old version (KIL) and in the new version (KAST) have attributes. They are used heavily for piggybacking information between compiler steps. Not having them would make kast definitions harder to read by a human. I know KAST/KORE's primary purpose is to be easy to read by a machine, but we do care about its readability somewhat. Otherwise, we would have everything in labeled form, including the K stuff.

[grosu]

1. OK, will think about it. Maybe modularize even further if we go this path, such as ~> and => in different modules. For example, the former may appear in terms to be pretty printed during execution, while the latter does not, so we may want to generate a pretty-printer including only the former. However, the good thing is that this modularization of syntax is completely orthogonal to the data-structures that it hooks to, so you can go ahead with the later while we can still play with separating things in modules.
2. I also wanted to parse the KAttributes as bubbles, but the problem with making the entire KAttribute a K is that KORE then is not backwards compatible if we consider the comma that separates the attributes as the KList comma. If we don't, then we'll need a comma for attributes defined in the front end, and have a klabel #attributes associated to that comma, or a similar one that we use in KORE to wrap the attributes. It is doable, I'll think about it.
3. Recall the very important design convention that we want KORE to be a subset of KAST to be a subset of Full K. That is, I should be able to parse a KORE definition using the Full K parser. I don't think we'll be able to keep the same syntax KItem KAttributes for adding attributes to KItems, as you imply, because of unavoidable syntactic conflicts. Imagine that you have arrays in your language. Then a[i] can be interpreted either as element i of array a, or the KItem a with attribute i. I know how to deal with this in the case of rule, e.g., rule a[i], but I don't know how to achieve the same for a[i] alone unless we add brackets for KAttributes, e.g., a[i], but then you can also run into conflicts if you have lists a la OCAML, because [i] can be parsed as the list containing only element i. I kind of think that we are looking for trouble if we try to extend the same syntax of rule attributes to arbitrary K terms. Besides, I believe you may also want to match on K-term attributes, especially if you want to implement K in K, in which case the current data-structures that hold the meta-data of a KItem as "something else" may need to change anyway, to keep the meta-data as part of the K term itself. In that case, I believe it is cleaner at the level of KORE to just have a special KLabel for holding term attributes/meta-data, e.g., #metadata(a,i), and then let the front end decide on a particular syntax for it.

Let me know what you think about the above. If we are in agreement, it should take very little until we are done with this KORE.

Cheers, Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Sunday, September 21, 2014 8:53 PM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

Actually, I am proposing three things:

1. Yes. Move things around in modules as outlined in the commit thread.
2. Yes, there was a bug in the definition -- it should be K instead of KList. The main reason for the change is that we would avoid using KList in a case where it doesn't have anything to do with the labeled form. Thus, we would also avoid the slightly forced step of moving the definition of the KList to a different module than the definition of KLabel. Another reason is that the KAttributes would be parsed as bubbles, thus possibly avoiding ambiguities and allowing us to easily slightly alter attribute syntax if we ever choose to.
3. That we have special syntax for attaching KAttributes to a KItem. I know we can always simulate this using a wrapper, but I think the KAttributes are important enough that they deserve their own syntax. All data structure constructors, both in the old version (KIL) and in the new version (KAST) have attributes. They are used heavily for piggybacking information between compiler steps. Not having them would make kast definitions harder to read by a human. I know KAST/KORE's primary purpose is to be easy to read by a machine, but we do care about its readability somewhat. Otherwise, we would have everything in labeled form, including the K stuff.

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

[grosu]

@yilongli @andreistefanescu @traiansf A question for you: Do we really need the sort membership syntax K ":" KSort in KORE, or we can just replace it with requires isSort(K)? I mean, do you do anything special for sort memberships t:Sort when you rewrite that is different from requires isSort(t), so that you would prefer to have the sort membership construct in the K term itself instead of in the side condition? If the answer is NO, then I'd like to remove the sort membership construct from KORE.

Again, KORE is meant to be the minimal subset of K through which we want to go when we kompile.

[cos]

1. From my perspective, further modularization sounds great. I will put in the hooks this morning.
2. Ok. I think it is a small price to pay for not polluting the BASIC-K (and implicitly OUTER) with the KList definition.
3. I have not attended all the discussions regarding disambiguating concrete syntax from labeled form, but it seems the problem of disambiguating brackets is similar to the one of disambiguating the labeled form's parentheses. Using a wrapper solves the problem, but our KORE (and maybe KAST) programs will end up looking like #metadata(a,#metadata(b, #metadata(...))). Metadata is this prevalent.

[yilongli]

@grosu We treat sort membership differently in the Java backend for now. In short, since we split pattern match and side condition evaluation in two steps, sort membership will be checked in the first step and isSort(K) will be evaluated in the second step. However, I plan to change this in the near future, that is, to evaluate the side condition immediately after all its arguments become available. Therefore, from my perspective, I would like to have K ":" KSort eliminated from KORE to make things uniform.

[cos]

I've added hook attributes to kore.k.

[grosu]

@cos

1. how about subsorts, don't we want to have hooks for them, too?
2. don't we want to have differently named constructors for different constructs? For example, instead of

  syntax KSentence ::= "syntax" KSort                         KAttributes   [ hook(Syntax) ]
  syntax KSentence ::= "syntax" KSort "::=" KProduction       KAttributes   [ hook(Syntax) ]

to have

  syntax KSentence ::= "syntax" KSort                         KAttributes   [ hook(SyntaxSort) ]
  syntax KSentence ::= "syntax" KSort "::=" KProduction       KAttributes   [ hook(SyntaxProduction) ]

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Monday, September 22, 2014 8:52 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

I've added hook attributes to kore.k.

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

[traiansf]

For Maude sort info can be on the requires part from the beginning; however, a backend tacking advantage of sorting might benefit from having the sorts attached to the variables, the alternative being they should be inferred from parsing the condition.

If we decide to only having them in the requires part, it would be nice to provide more structure to the requires part, like requiring it to be a List of conjuncts.

[andreistefanescu]

@grosu I want to keep the sorting information. For example I want to translate sorted variables from K to sorted variables in the SMT solver, and probably @bmmoore wants to translate them to sorted variables in Coq.

[grosu]

And is it so inconvenient to extract that information from the side condition? Note that one can always write a definition with sorting information in the side condition only; are we going to have a different semantics for those? So we need a way to reconcile rule Cxt[T:Sort] and rule Cxt[T] requires isSort(T) anyway ...

Grigore

---

From: Andrei Stefanescu [notifications@github.com] Sent: Monday, September 22, 2014 10:20 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

@grosuhttps://github.com/grosu I want to keep the sorting information. For example I want to translate sorted variables from K to sorted variables in the SMT solver, and probably @bmmoorehttps://github.com/bmmoore wants to translate them to sorted variables in Coq.

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

[cos]

@grosu

1. No. Their approximate equivalent in the data structures are interfaces. But those are implemented directly in Java/Scala, not hooked. We could try to figure out a way to automatically convert an entire K definition into an equivalent Scala/Java program, but this is beyond our current goal.
2. The constructor can be polymorphic. We could make the names different but we would not gain much. On the K side it is obvious the syntax refers to the KSort, while on the Java/Scala side the signature is Syntax(KSort sort), which is also pretty clear.

[yilongli]

@grosu It could be a little bit more inconvenient than it is right now for high-level stuffs such as Andrei's prover. However, since I consider this issue in the level of abstract machine, it actually makes things simpler for me.

[cos]

Regarding sort information, we could also attach it to Terms through wrapping: #withCondition(myTerm, isSort(T))

[grosu]

But again, it makes no sense to have different behaviors for a definition using T:Sort versus one using isSort(T), so there should be some place in the kompilation sequence where the two are made identical. If we agree on that, then I would prefer in KORE to pick the notationally simpler approach, which is the one with the side condition, because that requires no additional syntax to KORE for that.

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Monday, September 22, 2014 10:36 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

Regarding sort information, we could also attach them to Terms through wrapping: #withCondition(myTerm, isSort(T))

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

[cos]

It's very easy for a compilation step to unify them.

[cos]

I'm going out on a limb here... if we are looking at things this way, the inner KORE may simply be just labeled form. We are now left with just _~>_ and _=>_. We can have them in labeled form also, and have them "downmoduled" to the right data structures the same way we do with the user-defined language part of the bubble. From the perspective of the data structures, there is no difficulty in this.

[cos]

Maybe we don't gain much from it, but it is doable.

[andreistefanescu]

@grosu from a practical perspective, T:Sort is much easier to work with than isSort(T). As far as I know, isSort(T) is not used much, with the exception of notBool isKResult(T) in cooling rules. If someone wants to write a pass to switch isSort(T) into T:Sort, I'm fine with that.

[grosu]

But Andrei, do you agree that we need that pass anyway? Otherwise we have different behaviors for the two equivalent forms, which is inadequate at best. So do you agree that this step is needed anyway?

Grigore

---

From: Andrei Stefanescu [notifications@github.com] Sent: Monday, September 22, 2014 11:10 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

@grosuhttps://github.com/grosu from a practical perspective, T:Sort is much easier to work with than isSort(T). As far as I know, isSort(T) is not used much, with the exception of notBool isKResult(T) in cooling rules. If someone wants to write a pass to switch isSort(T) into T:Sort, I'm fine with that.

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

[cos]

Hm...sorry, scratch that. We don't want to use labeled from for ~> and => because we then lose an easy to make the distinction between K and the K meta-level. This is useful when rewriting definitions. E.g.,

`_=>_`(A, B) => `_=>_`(A, A)

[andreistefanescu]

@grosu While in theory we could have different behaviors (some things may not be proved with isSort(T)), in practice this is not an issue, because isSort(T) is not really used in definitions, and there is no reason for it to be used.

[grosu]

@andreistef Your answer is a bit imprecise. We need to obey some semantics of K. The semantics of the two notations should be the same. Do you agree with that? Also, the isSort in side condition is semantically more general, for example you can have

    rule C[T] requires isSort(C'[T])

and

    rule C[T] requires isSort1(T) /\ isSort2(T)

etc. Do you agree with that?

I'm not saying that we will ask people write definitions like this, all I want is to find a minimal and semantically complete KORE, both textual and in terms of data-structures. And since we need to unify the two different ways to express sort memberships anyway, it looks like we can get rid of the notation K ":" KSort from KORE.

Grigore

---

From: Andrei Stefanescu [notifications@github.com] Sent: Monday, September 22, 2014 11:22 AM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

@grosuhttps://github.com/grosu While in theory we could have different behaviors (some things may not be proved with isSort(T)), in practice this is not an issue, because isSort(T) is not really used in definitions, and there is no reason for it to be used.

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

[yilongli]

@andreistefanescu But we have the following rule in fun-untyped.k: rule isVal(cons V:Val) => true Right now, I am already dealing with this kind of rules in an ad-hoc way.

[andreistefanescu]

@yilongli I am only discussing how to represent the sort information on terms. How we compute that information is orthogonal (and I agree with you that it is a little adhoc now). @grosu I agree that that in theory the two notations should be equivalent. The complications can occur in practice because there is no structure for the clauses of requires and ensures. If you want to enforce a certain practice, for instance T:Sort to become T requires isSort(T) than it might be feasible.

[traiansf]

I restate my suggestion: that is, to have them in the condition, but to require the condition to be a list of basic conjuncts (like done in Conditonal Equational logic, for example) and not a generic K term.

2014-09-22 19:42 GMT+03:00 Yilong Li notifications@github.com:

@andreistefanescu https://github.com/andreistefanescu But we have the following rule in fun-untyped.k: rule isVal(cons V:Val) => true Right now, I am already dealing with this kind of rules in an ad-hoc way.

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

[andreistefanescu]

@traiansf how about variables that occur only in the condition (and not in the body of the rule). Should their sort be located immediately after?

[yilongli]

@andreistefanescu yes, but I am just saying that isSort(T) is used in some cases.

[cos]

This post is in the context of the discussion here: https://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81

I think we can also get rid of the #klabel injection from the KORE/KAST definitions. If we see the labeled form as a meta-level, then moving an expression to the meta-level simply means writing it in labeled form. This principle can apply to the labeled form itself. So, if we add some helper names to the labeled form productions we can have (an equivalent of) everything described on the Kore Design wiki page for free.

The only change is that the syntax for labeled form will need klabel attributes, along these lines:

syntax KLabel   ::= r"([^`]|\+`)*" [ klabel(#label), token ]
syntax KItem   ::= KLabel "(" KList ")" [ klabel(#apply) ]
syntax KList    ::= KList "," KList [ klabel(#klist) ]

I said "equivalent of" above because there are some difference. Mainly, this approach wouldn't allow some types of mixing between regular and meta level. The following line from Kore Design:

test(#label(L)) => L(1,2)

becomes:

test(#label(L)) => #apply(#label(L), #klist(1,2))

It needs to be done this way because L is just a token/constant now. 1 and 2 are ok because they are already KItems.

The translation of the next two examples from the Kore Design page illustrate this:

   test2(true) => #label('label1)
   test2(false) => #label('label2)

become:

   test2(true) => #label("'label1")
   test2(false) => #label("'label2")

Going further...

 #apply(#label(L),#klist(KL)) => L(KL)

is not needed as a function because the left-hand side simply "means" the right hand side by hooking. Actually, the right-hand side of the above line is incorrect in this approach as it would means "string ( some user list )"

Bottom line, again, we simply use the labeled form of the labeled form as the meta-level. Here is another example:

rule `foo`(A, B) => `foo`(A)
rule `bar`(A, B) => `bar`(A)

The first line is equivalent to:

rule #apply(#label("`foo`"), #klist(A, B)) => #apply(#label("`foo`"), #klist(A))

but we can replace both lines with the general rule:

rule #apply(#label(L), #klist(A, B)) => #apply(#label(L), #klist(A)) requires L == "`foo`" orBool L == "`bar`"

(I may update this comment as I find errors, so please read the online version)

[cos]

hmm.... I should have put the last line of the previous comment at the beginning of the post. again, please read the online version of the comment above.

[cos]

I now see the KAST wiki page has another proposal for the meta-level. Still, it seems that the approach presented in Kore Design, and implicitly the above, is nicer.

[grosu]

@cos I have mixed feelings about this.

syntax KLabel   ::= r"([^`]|\+`)*" [ klabel(#label) ]

is non-uniform, like a very peculiar special case. Imagine that you don't have the r in front, so you have something like this: syntax KLabel ::= "_+_" [klabel(plus)]. You would not expect to write it as plus("_+_") as your definition implies, by any stretch of imagination. For any other sort different from KLabel, you would just end up writing plus(.::KList) instead of _+_(.::KList).

I believe that this problem can be solved using the token attribute:

syntax KLabel   ::= r"([^`]|\+`)*" [token]
syntax KItem    ::= KLabel "(" KList ")" [ klabel(#kapply) ]  // #kapply is better than #apply
syntax KList    ::= KList "," KList [ klabel(#klist) ]

and now you can write #apply(#token("_+_","KLabel"), #klist(1,3)).

But before I comment more on this, I want to make sure that you are not proposing to get rid of the notation L(K1,K2) for KItems, which was the whole point of labels. For example, I hope that instead of _+_(1,3) you are not enforcing our users to now write #apply(#label("_+_"), #klist(1,3)), which would be overkill. Recall that we want KORE to be a subset of KAST to be a subset of Full K. We offered the abstract syntax notation for people like Denis or Chucky who didn't want to rely on the concrete syntax parser. Asking these people to go one meta-level higher is a bit harsh. I want to make sure that #apply(#label("_+_"), #klist(1,3)) is an equivalent way for writing _+_(1,3), the same way _+_(1,3) is an equivalent way for writing 1+3 in KAST.

[grosu]

@traiansf :

I restate my suggestion: that is, to have them in the condition, but to require the condition to be a list of basic conjuncts (like done in Conditonal Equational logic, for example) and not a generic K term.

Why? The condition can just as well just be a generic K term, but have kompilation steps that look for an andBool conjunction of things in the condition, and then optimize accordingly. For reasoning we want the requires and ensures conditions to be just bool terms anyway.

[grosu]

Added more structure and all klabels to kore.k.

@cos please review and let me know what you think asap. As you can see, I am not yet sold with your idea to use the meta-level notation for KLabels. Recall that with the new approach to define KORE/KAST in K, the KORE/KAST definitions become programs, so they will be parsed with the program parser. The program parser knows nothing about parsing the meta-level level notation. Of course, we can now craft our parsers however we wish, in particular we can use a parser that adds the meta-level notation to the program syntax, but that is not immediately clear.

Grigore

---

From: Cosmin Radoi [notifications@github.com] Sent: Monday, September 22, 2014 6:58 PM To: kframework/k Cc: Rosu, Grigore Subject: Re: [k] new KAST (#950)

This post is in the context of the discussion here: 51ae9d8#diff-805bc26fb25d50ef3c1f020b863f4674R81https://github.com/kframework/k/commit/51ae9d80f96eedacfd0b5e6029c7f672965eeca5#diff-805bc26fb25d50ef3c1f020b863f4674R81

I think we can also get rid of the #klabel injection from the KORE/KAST definitions. If we see the labeled form as a meta-level, then moving an expression to the meta-level simply means writing it in labeled form. This principle can apply to the labeled form itself. So, if we add some helper names to the labeled form productions we can have (an equivalent of) everything described on the Kore Designhttps://github.com/kframework/k/wiki/Kore-Design wiki page for free.

The syntax for labeled form will need to be changed along these lines:

syntax KLabel ::= r"([^]|\+)*" [ klabel(#label) ] syntax KItem ::= KLabel "(" KList ")" [ klabel(#apply) ] syntax KList ::= KList "," KList [ klabel(#klist) ]

I said "equivalent of" above because there are some difference. Mainly, this approach wouldn't allow some types of mixing between regular and meta level. The following line from Kore Design:

test(#label(L)) => L(1,2)

becomes:

test(#label(L)) => #apply(#label(L), klist(1,2))

It needs to be done this way because L is just a string now. 1 and 2 are ok because they are already KItems.

The translation of the next two examples from the Kore Design page illustrate this:

test2(true) => #label('label1) test2(false) => #label('label2)

become:

test2(true) => #label("'label1") test2(false) => #label("'label2")

Going further...

apply(#label(L),#klist(KL)) => L(KL)

is not needed as a function because the left-hand side simply "means" the right hand side by hooking. Actually, the right-hand side of the above line is incorrect in this approach as it would means "string ( some user list )"

Bottom line, again, we simply use the labeled form of the labeled form as the meta-level. Here is another example:

rule foo(A, B) => foo(A) rule bar(A, B) => bar(A)

The first line is equivalent to:

rule #apply(#label("foo"), #klist(A, B)) => #apply(#label("foo"), #klist(A))

but we can replace both lines with the general rule:

rule #apply(#label(L), #klist(A, B)) => #apply(#label(L), #klist(A)) requires L == "foo" orBool L == "bar"

(I may update this comment as I find errors, so please read the online version)

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

[cos]

But before I comment more on this, I want to make sure that you are not proposing to get rid of the notation L(K1,K2) for KItems, which was the whole point of labels. For example, I hope that instead of _+_(1,3) you are not enforcing our users to now write #apply(#label("_+_"), #klist(1,3)), which would be overkill. Recall that we want KORE to be a subset of KAST to be a subset of Full K. We offered the abstract syntax notation for people like Denis or Chucky who didn't want to rely on the concrete syntax parser. Asking these people to go one meta-level higher is a bit harsh. I want to make sure that #apply(#label("_+_"), #klist(1,3)) is an equivalent way for writing _+_(1,3), the same way _+_(1,3) is an equivalent way for writing 1+3 in KAST.

I am definitely not suggesting to get rid of the L(K1,K2) notation. Your last sentence is the core of my observation. To reiterate, starting with 1+3 we can choose to go one meta-level (labeled-form) up and get _+_(1,3). Then we can choose to go another meta-level (labeled-form) up and get #apply(#label("_+_"), #klist(1,3)). Starting with this observation, my proposal is that we use this mechanism to get the meta-level functionality for K.

[grosu]

@cos So your proposal here really is to allow not only core syntax and meta-level syntax together, but also meta-meta-level and why not meta-meta-meta-level, etc., all together. Is that correct? In fact, this is something we always advocated for, so I am not against it at all.