K-user mailing list

[Philip Daian <phil AT linux.com>]

If you have two lists, it looks like the comma operation is hooking List:__ (two underscores in K means two anonymous arguments).  That means for the list type, L1 L2 should concatenate L1 and L2 (whitespace doesn't matter in K parsing unless explicitly requested as a literal).  This works associatively, so L1 L2 L3 will be the concatenation of those three lists.

I'm not going to say much about the relationship between the List and MyList datatypes, as I don't want to say anything wrong or imprecise (so a K developer should comment).  When I write definitions I think of List as the syntactic category/AST label of the builtin List datatype, and MyList as the datatype used "under the hood" for internally representing operations on lists.  You should pretty much always be using List in your programs unless you want to be working with the intermediate representation of your program under the hood.  In that case you will need to require explicitly the builtin file where MyList is defined (list.k).  Again, this gets me through writing definitions, but may be wildly inaccurate :).

Hope that helps.

- Phil

On Mon, Mar 24, 2014 at 10:21 PM, Omar Duhaiby <3omarz AT gmail.com> wrote:

Thanks Philip. Here is what I did. I used the comma operator to try to concatenate two Lists. However, K gave an error that it expected the sort MyMap. I thought MyMap is somehow overriding List because they both use the comma operator. So I changed the comma in the builtins files (list.k and io.k) to a unique operator that I made up: "+List". Now the error I get is that my variables are of sort List but are expected to be of sort MyList.

I don't understand the relation between List and MyList.

On Tue, Mar 25, 2014 at 2:10 AM, Philip Daian <phil AT linux.com> wrote:

Hello Omar,

There is a manual being worked on right now, but as the framework is still in an early stage and even the core is still constantly changing, there is nothing complete currently out.  Right now the best resources are the K Tutorials, related exercises, publications on the KFramework site, and the source code of the related builtins.  Once learning the basics of K definitions, you can check something like https://github.com/kframework/k/blob/master/include/builtins/list.k for what you need.  It looks like the comma operation does what you seek. 

  /*@ Construct a List using two Lists. This is similar to the "Cons" operation

   in many functional programming languages.*/

  syntax MyList ::= MyList "," MyList [left, function, hook(List:__), klabel('_List_)]

I hope that helps. The K developers definitely do recognize the need for better documentation for widespread user adoption, and it is something that should be nailed down as the framework matures.  It's also worth noting that I am not a K core developer, so anything I said may be wrong and corrected in the future :).

- Philip Daian

On Mon, Mar 24, 2014 at 6:56 AM, Omar Duhaiby <3omarz AT gmail.com> wrote:

Hello,

Is there a K reference manual that I'm not aware of? I couldn't find anything in the wiki.

Currently I'm looking for a built-in function to concatenate Lists.

Thank you

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