K-user mailing list

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

The latest from  http://k-framework.googlecode.com/svn/tags/latest/
gives me the same error.  I will move on to trying this on another
platform.

Thanks,
Brandon



On Thu, Sep 27, 2012 at 4:02 PM, Brandon Hill 
<bgh.list.reader AT gmail.com>
 wrote:
> 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