K-user mailing list

[Gurvan Le Guernic <gleguern AT gmail.com>]

   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, K stops (without error messages) and output a configuration where the cell <k> still contains "getNextMsg".

 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 ?

   Thanks,

   Gurvan Le Guernic