K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Until we have a manual, the best thing to do in order to see what is available and what needs to be defined by you is to look into the include folder, in the .k files.  Just search for BagItem, for example, and look at the operations/functions that are defined there.

Also, operations like the "search" that you defined should be tagged with "function", because you want them to apply everywhere, not only on top of the k cell.

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Saha, Shambwaditya [ssaha6 AT illinois.edu]
Sent: Thursday, December 26, 2013 9:56 PM
To: Philip Daian
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Bags

Hi, 

Thanks a lot for your detailed explanation about Bags and the suggestions to modify the code, it really helped. The code kompiles, but unfortunately, I was not able to krun something like  search (BagItem(5) BagItem(8)) 5 or 5 in ( BagItem(5) BagItem(8) ) . It complained about a syntax error. Do you have any quick tip. 

Thanks in advance!

Regards,

Shambwaditya

On Thu, Dec 26, 2013 at 9:05 PM, Philip Daian <phil AT linux.com> wrote:

As far as I know there is no way to specifically mention in the syntax that you want a bag of ints.  A bag is simply .Bag, BagItem(K), or Bag Bag.   Your code is failing because in your side condition, you are using an equality operator that expects a comparison of two items of sort K on a BagItem.

To fix your code, change it to:

  syntax Bool ::= "search" Bag Int

  rule search ( BagItem(V) Bg:Bag) V1:Int => true when V ==K V1

  rule search (BagItem(V1) Bg:Bag) V:Int => search Bg V when V1 =/=K V 

  rule search .Bag V:Int => false

BagItem is simply a wrapper around values stored in the bag meant to distinguish bag items from items in other builtins.  Note that now you are comparing the values in the bag to those passed into the search function.  If you want to require bags of ints and get stuck otherwise, you can ask for the K items stored in the bags to be of sort int.

  syntax Bool ::= "search" Bag Int

  rule search ( BagItem(V:Int) Bg:Bag) V1:Int => true when V ==K V1
  rule search (BagItem(V1:Int) Bg:Bag) V:Int => search Bg V when V1 =/=K V

  rule search .Bag V:Int => false

Now, if you call search on a nonempty noninteger bag, no rules will match and your rewriting will get stuck (unless you do something like search (BagItem(5) BagItem("hi")) 5, which will still evaluate to true.  To fix this change the second rule to match BagItem(V:Int) .Bag instead of Bg:Bag and add another rule moving any found item to the end of your bag). 

 See the K code in include/builtins/bag.k for the best documentation of bags there is at the moment to my knowledge.

That code includes "in" function, which is a more general version of your search construct for all bultins which have equality in K.

Hope that helps!

- Phil

On Thu, Dec 26, 2013 at 4:06 PM, Saha, Shambwaditya <ssaha6 AT illinois.edu> wrote:

Hi,

I want to define a search function on Bag of Ints. I tried to write something of the form :

  syntax Bool ::= "search" Bag Int

  rule search ( V:BagItem Bg:Bag) V1:Int => true when V ==K V1

  rule search (V1:BagItem Bg:Bag) V:Int => search Bg V when V1 =/=K V 

  rule search .Bag V:Int => false 

This definition is obviously not correct, and I have a few questions about it : 

1. How do we specifically mention in the syntax that we want Bag of Ints. 

2. It is showing an error : "Variable V is contextually expected to have sort K but it has been declared (or infered) of sort BagItem", how should we solve it. 

3. And what should be a valid instance of this program. i.e. how should we specify a bag, in krun.

Thanks in Advance!

Regards,

Shambwaditya

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user