K-user mailing list

[Philip Daian <phil AT linux.com>]

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