K-user mailing list

[Frederico Zica <fredzica AT gmail.com>]

Hello Dwight.

I got the code from the "unified-builtins2" branch. I couldn't determine if the mint part  worked or not because apparently lot of things changed, including pattern matching and the output from krun. I tried to change my definitions accordingly, at some I was succesful, but got stuck at one point and couldn't proceed. As I didn't know if this new behaviour or just things that will still be changed, I preferred to stay with the nightly build.

Thanks,

Frederico Zica

2014-07-31 14:44 GMT+02:00 Dwight Guth <dwight.guth AT runtimeverification.com>:

This is actually fixed in the development version of K which will be
released in the next couple days. You can download it now if you want
by cloning the repository on github and checking out the
"unified-builtins2" branch.

On Wed, Jul 30, 2014 at 7:13 PM, Frederico Zica <fredzica AT gmail.com> wrote:
> Hello.
>
> I'm using the K Framework for some time now. Also in my project I'm using
> the MInt builtin, because I need to represent 8-bit wide numbers.
>
> Initially I was using the stable version. From some point on, as I realized
> the stable was not so recent already, I decided to use the nightly build.
> The MInt type source files changed and I refactored the code according to
> those changes. The problem I have with is with the functions overflowMInt
> and miMInt. They are supposed to only take the overflow and MInt values, as
> seem in the mint.k builtin:
>
>
>
>   rule miMInt(MyListItem(MI:MInt), MyListItem(_:Bool)) => MI
>
>   rule overflowMInt(MyListItem(_:MInt), MyListItem(B:Bool)) => B
>
>
> But when I run then they don't reduce (part of krun output):
>
>         <rc>
>             overflowMInt ( ListItem(mi ( 8 , 300 )) ListItem(true) )
>         </rc>
>
> However, if I remove from the rules the explicit mention of the MInt type,
> both functions start working:
>
>
>
>   rule miMInt(MyListItem(mi(N, I)), MyListItem(_:Bool)) => mi(N, I)
>   rule overflowMInt(MyListItem(_), MyListItem(B:Bool)) => B
>
>
>
>
>
> The operation I used was the uaddMInt.
>
>
> Am I doing something wrong? Is that a bug in MInt the builtin?
>
>
>
>
>
> Thanks,
>
> Frederico Zica
>
>

> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>