K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Hi Gurvan,

Please find the answer below.

On Jan 20, 2016, at 10:55 AM, Gurvan Le Guernic 
<gleguern AT gmail.com>
 wrote:

>    Hi,
> 
>  I'm using K to specify the semantics of a "message" filtering language. In 
> order to evaluate the semantics, the "filtering program" is the program 
> parsed by K at start up and the "messages" to filter are retrieved from 
> stdin, i.e. the configuration contains the following fragment :
> 
>       <streams color="yellow">
>         <in stream="stdin"> .List </in>
>         <out stream="stdout"> .List </out>
>       </streams>
>  
>  I first tried a version where messages are a simple 'String'. Messages are 
> then loaded withe the following 2 rules :
> 
>   syntax Holder ::= "getNextMsg"
> 
>   rule
>     <k> . => getNextMsg </k>
>     <out> ... .List => ListItem("> ") </out>
>     [structural]
> 
>   rule
>     <filter> F:Filter </filter>
>     <k> getNextMsg => F </k>
>     <in> ListItem(Msg:String) => .List ...</in>
>     <input>
>       ...
>       <msg>
>         <ctt> _ => replaceAll(Msg, "\n", "") </ctt>
>       </msg>
>     </input>
>     [structural]
> 
>  Everything worked fine. I would now like to extend messages to be a 
> triplet (timestamp, port, data).
>  I defined a new syntax in the *-SYNTAX module :
>    syntax MsgTimeStp ::= Int
>    syntax MsgPortId ::= String
>    syntax MsgData ::= String
>    syntax Msg ::= "(" MsgTimeStp "," MsgPortId "," MsgData ")"
> 
>  I modified the configuration :
>       syntax Msg ::= "NullMsg"
> 
>         <rawInput> NullMsg:Msg </rawInput>
> 
>  and tried to replace the last rule with the following one :
>   rule
>     <filter> F:Filter </filter>
>     <k> getNextMsg => parseInputMsg </k>
>     <in> ListItem(Msg:Msg) => .List ...</in>
>     <rawInput> Msg </rawInput>
>     [structural]
> 
>  It does compile and start runing. However, when I provide the following 
> string "( 3 , IN, 000000000000100001000 )" on stdin,

First of all, strings should be enclosed with quotes ("). So, a valid input 
would be:
        ( 3, "IN", "000000000000100001000" )

> K stops (without error messages) and output a configuration where the cell 
> <k> still contains "getNextMsg".

Unfortunately, K currently supports IO-stream for only primitive values such 
as ints or strings. In your example, `Msg` is not primitive, and thus the 
last rule is not applied. (Indeed, an warning should have been reported in 
this case. We'll fix that.)

>  Is there a way to parse the piece of data retrieved from stdin into a K 
> term on which to apply further rules ? Or do I have no other way than to 
> add to the program the messages to parse and do the parsing at load time ?

A workaround would be to read the input as a plain string and parse them 
later. For example,

        <k> getNextMsg => #parse(Input, "Msg") ... </k>
        <in> ListItem(Input:String) => .List ... </in>

where `#parse` is a builtin function in K which takes as inputs a string to 
parse and its sort, and returns the parsed term.

This should work for K 3.6.

Let me know if you still have the problem. I can help you more if you provide 
the full definition.

Best,
Daejun

>    Thanks,
>    Gurvan Le Guernic
>