Integral constants for unsigned integer types?

[Shea Levy]

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

[Hongwei Xi]

Here are some quick solutions:

 $UNcast{usint(16)}(16) or $extval(usint(16), "16")

~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.

[Hongwei Xi]

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)

[Shea Levy]

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

~Shea

> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqJp7E0fKfkW5YQwyANtXvYWUd-MKdTuxTo165FoPmoKw%40mail.gmail.com.