Converting an int to a byte?

Google Group
1

Here goes a simple question: I need a function to convert an int to a byte.

Either I’m not searching hard enough, or there is no such function in the
prelude. Which is it?

2

I added several casting functions for bytes. See the end of the following
file:

http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html

The type byte is treated in ATS as a completely opaque type whose size
equals that of a char.

Is there a praxi or prfun somewhere that indicates that sizeof(byte) ==
sizeof(char)?

I added some lemmas in char.sats. For instance,

praxi
lemma_char_size () : [sizeof(char)==sizeof(byte)] void

However, the names of these lemmas are difficult to remember. So be
“programmer-centric” :slight_smile:

prval () = $UN.prop_assert{sizeof(char)==sizeof(byte)}()

3

My guess is that there may not be such a function, other than $UN.cast. But
I hardly know for sure. I feel like this was talked about recently: does
int size still vary from platform to platform according to the C standard?
But in ATS you can specify the size of the int if you really need to, so I
guess it isn’t an issue if you go this route.On Fri, Feb 13, 2015 at 6:52 AM, Artyom Shalkhakov < artyom.s...@gmail.com> wrote:

Here goes a simple question: I need a function to convert an int to a byte.

Either I’m not searching hard enough, or there is no such function in the
prelude. Which is it?

–
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/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

4

I added several casting functions for bytes. See the end of the following
file:

http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html

The type byte is treated in ATS as a completely opaque type whose size
equals that of a char.

If you want to manipulate/modify bytes, try to use types like int8 and
uint8.On Friday, February 13, 2015 at 6:52:12 AM UTC-5, Artyom Shalkhakov wrote:

Here goes a simple question: I need a function to convert an int to a byte.

Either I’m not searching hard enough, or there is no such function in the
prelude. Which is it?

5

I added several casting functions for bytes. See the end of the following
file:

http://ats-lang.sourceforge.net/DOCUMENT/ATS-Postiats/prelude/HTML/SATS/char_sats.html

The type byte is treated in ATS as a completely opaque type whose size
equals that of a char.

Is there a praxi or prfun somewhere that indicates that sizeof(byte) ==
sizeof(char)?

If you want to manipulate/modify bytes, try to use types like int8 and
uint8.

Thanks! I switched to uint8 + unsafe casts for now.> On Friday, February 13, 2015 at 6:52:12 AM UTC-5, Artyom Shalkhakov wrote:

Here goes a simple question: I need a function to convert an int to a
byte.

Either I’m not searching hard enough, or there is no such function in the
prelude. Which is it?

6

Actually, $UN.cast may not be the exact function you want since I guess
byte will have some views that need to be constructed, but something in $UN
would hopefully work.On Fri, Feb 13, 2015 at 8:36 AM, Brandon Barker brandon...@gmail.com wrote:

My guess is that there may not be such a function, other than $UN.cast.
But I hardly know for sure. I feel like this was talked about recently:
does int size still vary from platform to platform according to the C
standard? But in ATS you can specify the size of the int if you really need
to, so I guess it isn’t an issue if you go this route.

On Fri, Feb 13, 2015 at 6:52 AM, Artyom Shalkhakov < artyom.s...@gmail.com> wrote:

Here goes a simple question: I need a function to convert an int to a
byte.

Either I’m not searching hard enough, or there is no such function in the
prelude. Which is it?

–
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/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/6fb403c5-b024-4c84-bca5-ec2c2dd48c04%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brandon...@gmail.com

Brandon Barker
brandon...@gmail.com

7

Actually, $UN.cast may not be the exact function you want since I guess
byte will have some views that need to be constructed, but something in $UN
would hopefully work.

Well, I could always implement it in C. I guess that it would be quite
useful to have it included in the prelude, though.