K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Did you try I:Int instead of V:Val and remove the side condition?

Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Brandon Hill 
[bgh.list.reader AT gmail.com]
Sent: Thursday, September 27, 2012 4:09 PM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] Printing

I am trying to model a language that prints the resulting value from
each expression.  The examples show how to explicitly print with an
explicit print function, a Printable sort, and an output list.  I'm
not entirely clear how that Printable works.

Without it, I get:

[Fatal Error] :1:1: Premature end of file.
Error: Error while reading XML:Premature end of file.

or

(#ostream( 1 ))  (#buffer( (.) ))

as output.  Here is a trimmed down version of what I tried:


module RT-SYNTAX
  imports BUILTIN-SYNTAX-HOOKS

  syntax Val ::= Int

  syntax Expr ::= Id | Val
        > Id "<-" Expr  [right, strict(2)]

  syntax Stmt ::= Expr ";" [strict]
        | Stmt Stmt    [left]

  syntax Pgm ::= Stmt

endmodule

module RT
  imports RT-SYNTAX

  syntax Val ::= "void"

  syntax KResult ::= Val

  configuration <T color="yellow">
                  <k color="green"> $PGM:Pgm </k>
                  <env color="LightSkyBlue"> .Map </env>
                  <heap color="white"> .Map </heap>
                  <nextLoc color="gray"> 0 </nextLoc>
                  <out color="Orchid" stream="stdout"> .List </out>
                </T>

  rule [declaration]:
       <k> X:Id <- V:Val => void ...</k>
       <env>... Rho => Rho[L/X] ...</env>
       <heap>... . => L |-> V ...</heap>
       <nextLoc> L => L +Int 1 </nextLoc>
       when notBool(X in keys(Rho)) [transition]

  rule [lookup]: <k> X => V ...</k>
       <env>... X |-> L ...</env>
       <heap>... L |-> V ...</heap> [supercool, transition]

  rule [sequential]: (S1:Stmt S2:Stmt) => (S1 ~> S2)  [structural]

  rule <k> (V:Val; ~> K:K) => K ...</k>
       <out>... . => ListItem(V) </out>
       when  V =/=K void

  rule <k> (void; ~> K:K) => K ...</k>

endmodule


I also tried ListItem(Int2String(V)) but that doesn't work either.

Any pointers would be appreciated.

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