K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Dear Omer,

welcome to the K users group. Please find my answers below.


On 8/17/13 11:17 PM, Ömer Sinan Ağacan wrote:
> Dear K users and developers,
>
> I hope this is the right place to ask user questions.
Correct, this list is the right place to ask questions regarding the use 
of K.
>   I just started
> learning K and I'm having trouble understanding some parts. I actually
> have a huge list of questions in mind but for now I want to ask only a
> portion of them. Please excuse me if I'm sending this to an
> inappropriate list.
It is fine, please do not hesitate to send us your questions.
> Let's say I have this K program: (btw, sorry if I'm using some
> terminology wrong and please correct me if I'm wrong. this is my first
> K code ever)
>
>
>      module CONCAT-SYNTAX
>
>        syntax Concat ::= Concat1 ";" Concat
>                        | "end"
>
>        syntax Concat1 ::= Id
>                        |  "[" Concat "]" // quotation
>                        |  Int
>                        |  "printSomethingRandom"
>
>      endmodule
>
>      module CONCAT
>
>        imports CONCAT-SYNTAX
>
>        configuration
>          <k> $PGM:Concat </k>
>          <out stream="stdout"> .List </out>
>          <someList> .List </someList>
>          <someMap> .Map </someMap>
>
>        rule <k> (printSomethingRandom;Cs) => Cs </k>
>             <out> ... . => ListItem(N) </out>
>             <someList> ... . => ListItem(N) </someList>
>               when fresh(N:Nat)
1. First just a suggestion: if you add a rule like

    rule C:Concat1 ; Cs:Concat => C ~> Cs

which transform a concatenation into a sequence of computation tasks, 
then you may write rules like the above one in a slightly simpler form:

      rule <k> printSomethingRandom => . ...</k>
           <out> ... . => ListItem(N) </out>
           <someList> ... . => ListItem(N) </someList>
             when fresh(N:Nat)

2. The function "fresh(N:Nat)" generates a symbolic natural numbers 
written as "#symNat(1)". The current version of I/O server from K is not 
able to send to the standard output symbolic values. You may easily fix 
that by adding to your definition the following constructs:

      syntax String ::= Nat2String(Nat)

      rule Nat2String(#symNat(I:Int)) => "#symNat(" +String 
Int2String(I) +String ")" [anywhere]

 and change your rule with

     rule <k> (printSomethingRandom;Cs) => Cs </k>
           <out> ... . => ListItem(Nat2String(N)) </out>
           <someList> ... . => ListItem(N) </someList>
             when fresh(N:Nat)


>        rule <k> (I:Id;Cs) => Cs </k>
>             <someList> ... . => ListItem(I) </someList>
>
>        rule <k> (I:Int;Cs) => Cs </k>
>             // if I remove the part below this rule works fine
>             <someMap> ... I |-> (_ => N) ... </someMap>
>              when fresh(N:Nat)
This rule does not work when the content of the cell "someMap" is empty 
(.Map).
Therefore you must use the "update" operator:

      rule <k> (I:Int;Cs) => Cs </k>
           <someMap> M:Map => M[N/I] </someMap>
            when fresh(N:Nat)

>        rule <k> end => . </k>
>
>      endmodule
>
>
> (this is going to be a concatenative language like Forth, PostScript,
> Joy, Cat, Factor etc. when it's done)
>
> Now let me list my questions about this program:
>
>    * Let's say I changed the separator in Concat syntax from ";" to "
> ". Now how can I match it in rules? Simply changing ; characters with
> ` ` (space character) fails with "syntax error". Interestingly, if I
> change it with "-" instead of " ", it works fine. I don't understand
> how to use space character in patterns in rules.
You have to replace the syntax for Concat with

   syntax Concat ::= Concat1  Concat
                            | "end"

and repalce the rule

    rule C:Concat1 ; Cs:Concat => C ~> Cs

with

    rule C:Concat1 Cs:Concat => C ~> Cs

Note that the use of this suggested rule minimizes the number of 
transformations you have to make in the definition.
>    * Is there a reference manual etc. for matching rules to manipulate
> data structures like Map/List/Bag etc.? In this code, for some reason
> 3. rule doesn't work. This is probably because of a mistake in
> matching syntax in <someMap> part of the rule. (because removing that
> part makes it work) I copied that code from Imp implementation which
> is defined in K tutorials, but for some reason same syntax doesn't
> work for me.
Unfortunately the manual is "work in progress". We hope to have one as 
soon as possible.
My comments following this rule explain why it doesn't work as expected.
>    * Let's say I'm running this program:
>
>          ➜  concat  cat test.con
>          printSomethingRandom;thisIsAnIdentifier;10;end
>          ➜  concat  krun --no-config test.con
>          ➜  concat  krun test.con
>          <k>
>              10 ; end
>          </k>
>          <someList>
>              ListItem(#symNat(1))
>              ListItem(thisIsAnIdentifier)
>          </someList>
>          <out>
>              ListItem(#ostream ( 1 ))
>              ListItem(#buffer ( "" ))
>              ListItem(#symNat(1))
>          </out>
>          <someMap>
>              .Map
>          </someMap>
>
>      as you can see, even though I'm adding some elements to out list,
> and out configuration is marked as an output stream, this program
> doesn't really print anything. Why is that?
Do the changes I suggested above and it will work after that.
>    * Let's say I'm using built-in list syntax instead of `Concat1 ";"
> Concat` syntax I used in first syntax declaration: `List{Concat1,
> ";"}`. Now how should I change my rules in order to match this new
> syntax?
The only change you have to do it is to replace the rule

    rule <k> end => . </k>

with

    rule <k> .Concat => . </k>

Note that this rule can be written in a simpler form:

    rule  .Concat => .

(the cell "k" is automatically added for such rules).

I hope my comments help you to advance in learning K.

Bests,
Dorel
> Thanks,
>
>
> ---
> Ömer Sinan Ağacan
> http://osa1.net
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user