K-user mailing list

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

Ok, my flight is late, so I tried your example.  It works on my machine, I 
mean, it kompiles.  Also, it kruns, or at least on the program test.rt, which 
is  

x <- 10;

However, it does not do what you want, which is to print 10, because your 
definition is actually not correct.
(if you get compilation errors, then please make sure you downloaded the k 
latest built).

You have two competing rules that can apply when a value is on top of K: the 
cooling rule for your assignment, and the printing rule.  It happens that the 
first one applies, so the value V is moved back into its context, and then 
the printing rule gets no chance to apply anymore, since there is no value 
for it on the computation.  If the printing rule applied first, then things 
would be a lot worse!  That's because you are also consuming the value once 
you print it, so the cooling rule of assignment would get no value to cool, 
so it would get stuck.

The above does not give you a solution for your problem, but hopefully makes 
you think through these interesting issues.

Grigore



________________________________________
From: Brandon Hill 
[bgh.list.reader AT gmail.com]
Sent: Thursday, September 27, 2012 4:47 PM
To: Rosu, Grigore
Cc: 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] Printing

Thank you for the pointer on the better rules.  I thought I had tried
something like that and got errors, but it seems to work currently.

The cleaner rules don't seem to solve the printing issue, even when I
change the sort to I:Int and eliminate the side rule.  I was going
with V because it will contain more sorts in the future, but making
different rules for each result sort will be fine if that can be made
to work.

Thanks,
Brandon

On Thu, Sep 27, 2012 at 2:25 PM, Rosu, Grigore 
<grosu AT illinois.edu>
 wrote:
> 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