defining map, fold, etc., operations in K

[grosu]

I'd like to open this issue now to make sure we keep track of it, because it happened twice in the last 2 days that this has been brought up to my attention.

There should be no problem to define higher-order-style list operations in K, such as map, fold, etc. For example:

syntax KList ::= map(KLabel, KList)
rule map(_, .) => .
rule map(F, (K,Kl)) => F(K), map(F,Kl)

Or, if you want a specialized map for your particular user-defined list construct, then you can do something similar:

syntax SortList ::= List{Sort,":"}
syntax SortList ::= map(KLabel,SortList)
// same rules of map as above
// or, if you prefer to take advantage of the generic map above, then
rule map(F,Ss) => getKLabel(Ss)(map(F,getKList(Ss)))

[grosu]

The clean solution for user defined lists, though, will come when we add proper modularization to K. Lists should be defined either using parametric modules, or renaming. The latter would look something like this (actually Maude supports that, btw! but in Maude you need to explicitly go to the meta-level to pass KLabels around):

module LIST
    syntax Sort
    syntax List{Sort} ::= Sort "," List{Sort} | "."  // these are cons-lists, assoc lists would be defined differently
endmodule

module LIST-MAP
    imports LIST * (Sort to Sort1)
    imports LIST * (Sort to Sort2)
    syntax List{Sort2} ::= map(KLabel,List{Sort1})
    rule map(_, .) => .
    rule map(F,(S,L)) => F(S)::Sort2, map(F,L)
endmodule

module EXAMPLE
  imports INT
  imports LIST-MAP * (Sort1 to Int, Sort2 to List{Int})
  syntax List{Int} ::= mkList(Int)
  rule mkList(I) => I,.
  syntax List{List{Int}} ::= mkListList(List{Int})
  rule mkListList(L) => map(mkList, L)
endmodule