K-user mailing list

[Brandon Hill <bgh.list.reader AT gmail.com>]

Interesting.  I just made sure I was using the 28-Sep-2012 release.  I
cut and pasted the code above into a file.  I kompiled it, but my test
case of:

x <- 5;
x;

Still gives:

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

I even uninstalled any pre-existing Maude because it was a year newer
than what is in your binary, and I wanted to be sure the system wasn't
using it instead.  I also tried it with the earlier recommended
changes, but they gave the same result.  I am running on Ubuntu 12.04
64-bits.  Does that imply that some other environment variable could
be making our runs differ?  I can try getting the latest from SVN and
building that as a sanity check.  Sorry for any hassle.

My intention was for assignments to print nothing, but reductions of
all other expressions to print.  That was why I had assignments reduce
to void so I could capture and ignore those expressions.

Thank you,
-Brandon

P.S.  Thanks for the tutorial videos, they are really helpful.
On Thu, Sep 27, 2012 at 3:11 PM, Rosu, Grigore 
<grosu AT illinois.edu>
 wrote:
> 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