Converting an int to a byte?

[Artyom Shalkhakov]

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?

[Brandon Barker]

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.

--

Brandon Barker
brandon...@gmail.com

[Brandon Barker]

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.

--

Brandon Barker
brandon...@gmail.com

[Artyom Shalkhakov]

On Friday, February 13, 2015 at 7:40:43 PM UTC+6, Brandon Barker wrote:

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.
 

[gmhwxi]

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.

[Artyom Shalkhakov]

On Friday, February 13, 2015 at 10:43:30 PM UTC+6, gmhwxi wrote:

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.

[gmhwxi]

On Monday, February 16, 2015 at 3:11:21 AM UTC-5, Artyom Shalkhakov wrote:

On Friday, February 13, 2015 at 10:43:30 PM UTC+6, gmhwxi wrote:

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" :)

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