Integral constants for unsigned integer types?

Hi all,

I’m wrapping a C struct that has an unsigned short member with certain
constraints on its values, and I’ve represented the member as having an
appropriately-constrained existential type over the usint function. When
initializing the value with an integral constant, I get:

The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind), S2Eintinf(16))
The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype); S2Ecst(usint_kind), S2EVar(3864))

How can I use the integral constant appropriately?

Some test code that quickly reproduces the issue:

typedef foo = [i: int | i == 0] usint i
val x = 0 : foo

~Shea

Here are some quick solutions:

$UNcast{usint(16)}(16) or $extval(usint(16), “16”)On Sun, Sep 7, 2014 at 9:12 PM, Shea Levy sh...@shealevy.com wrote:

Hi all,

I’m wrapping a C struct that has an unsigned short member with certain
constraints on its values, and I’ve represented the member as having an
appropriately-constrained existential type over the usint function. When
initializing the value with an integral constant, I get:

The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind),
S2Eintinf(16))
The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype); S2Ecst(usint_kind),
S2EVar(3864))

How can I use the integral constant appropriately?

Some test code that quickly reproduces the issue:

typedef foo = [i: int | i == 0] usint i
val x = 0 : foo

~Shea


You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/20140908011228.GA2286%40nixos.hsd1.nh.comcast.net
.

Here is something that is a little bit safer:

extern
castfn i2us{i:nat}(int(i)): usint(i)

typedef
foo = [i: int | i == 0] usint i
val x = i2us(0) : foo

Of course, if you want something that is safe, then we have
to find out what USINT_MAX is, and then use the following one:

extern
castfn i2us{i:nat | i <= USINT_MAX}(int(i)): usint(i)On Sun, Sep 7, 2014 at 9:23 PM, Hongwei Xi gmh...@gmail.com wrote:

Here are some quick solutions:

$UNcast{usint(16)}(16) or $extval(usint(16), “16”)

On Sun, Sep 7, 2014 at 9:12 PM, Shea Levy sh...@shealevy.com wrote:

Hi all,

I’m wrapping a C struct that has an unsigned short member with certain
constraints on its values, and I’ve represented the member as having an
appropriately-constrained existential type over the usint function. When
initializing the value with an integral constant, I get:

The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind),
S2Eintinf(16))
The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
S2Ecst(usint_kind), S2EVar(3864))

How can I use the integral constant appropriately?

Some test code that quickly reproduces the issue:

typedef foo = [i: int | i == 0] usint i
val x = 0 : foo

~Shea


You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/20140908011228.GA2286%40nixos.hsd1.nh.comcast.net
.

Ah ha! Thanks, this gives me enough to get going.

~SheaOn Sun, Sep 07, 2014 at 09:30:53PM -0400, Hongwei Xi wrote:

Here is something that is a little bit safer:

extern
castfn i2us{i:nat}(int(i)): usint(i)

typedef
foo = [i: int | i == 0] usint i
val x = i2us(0) : foo

Of course, if you want something that is safe, then we have
to find out what USINT_MAX is, and then use the following one:

extern
castfn i2us{i:nat | i <= USINT_MAX}(int(i)): usint(i)

On Sun, Sep 7, 2014 at 9:23 PM, Hongwei Xi gmh...@gmail.com wrote:

Here are some quick solutions:

$UNcast{usint(16)}(16) or $extval(usint(16), “16”)

On Sun, Sep 7, 2014 at 9:12 PM, Shea Levy sh...@shealevy.com wrote:

Hi all,

I’m wrapping a C struct that has an unsigned short member with certain
constraints on its values, and I’ve represented the member as having an
appropriately-constrained existential type over the usint function. When
initializing the value with an integral constant, I get:

The actual term is: S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind),
S2Eintinf(16))
The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype);
S2Ecst(usint_kind), S2EVar(3864))

How can I use the integral constant appropriately?

Some test code that quickly reproduces the issue:

typedef foo = [i: int | i == 0] usint i
val x = 0 : foo

~Shea


You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/20140908011228.GA2286%40nixos.hsd1.nh.comcast.net
.


You received this message because you are subscribed to the Google Groups “ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqJp7E0fKfkW5YQwyANtXvYWUd-MKdTuxTo165FoPmoKw%40mail.gmail.com.