Driving out the casts

Google Group
1

I’m trying to drive out all the casts in my code related to uint8 and
similar. Basically, I have types based on:

{n:int | n > …

and

uint8

And when I mix them I have a couple of problems.

  1. Passing a constant into a function requires a cast like u8(10) or
    u73(12)
  2. Passing a uint8 into a function with a parameter like {n:int | …)
    requires a cast like u73(u8(20))

In some cases the constraints, as I like to call them, are equivalent in
that they they represent a number from 0 to 0xFF, but from a type point of
view they are not the same.

So, for example, with a function like this:

macdef packetOutCount =
$extval(ref(uint8),“packetOutCount”)

extern fun{} set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void
implement{} set_n {n0} (count) = let
val () = !packetOutCount := count
…
in
…
end

the line below fails to compile:

val () = !packetOutCount := count

but this compiles:

val () = !packetOutCount := u8(count)

count is restricted to values between 3 and 127, so it can’t violate a
uint8 which is restricted to values between 0 and 255.

So I tried to pick apart uint8 to see what might be the problem:

sortdef uint8 =
{ i:int | 0 <= i; i < 256 }

tkindef
uint8_kind = "atstype_uint8"
typedef
uint8_0 = g0uint (uint8_kind)
typedef
uint8_1
(i:int) = g1uint (uint8_kind, i)
//
stadef uint8 = uint8_1 // 2nd-select
stadef uint8 = uint8_0 // 1st-select
stadef uInt8 = [i:nat] uint8_1 (i)

I think it has something to do with the meaning of uint8 in:

macdef packetOutCount =
$extval(ref(uint8),“packetOutCount”)

In the above, what overloaded uint8 is getting used? Is it the uint8_kind
or uint8_0?

Is there a way to setup the macdef in such a way that I don’t have to keep
casting things?

2

I’m having problems compile the example. I also tried:

castfn
u8_safe {n: nat | n < 256} (i: int(n)):<> uint8(n)

Then I copied an example from the distribution and it failed.

Is there a compiler option or an include I need to use to make castfn
compile? Anything about the arduino_ats system that might cause a problem?

3

In the following code, a cast is necessary as ‘count’ and ‘u8(count)’ have
different C-types: int vs. uint8.

Casting can be safely done. For instance, the following cast function
u8_safe
is completely safe:

castfn u8_safe: {n: nat | n < 256} int(n) → uint8(n)

Maybe what you really want to do is to replace u8 with u8_safe.

val () = !packetOutCount := u8(count)On Monday, November 2, 2015 at 9:25:05 AM UTC-5, Mike Jones wrote:

I’m trying to drive out all the casts in my code related to uint8 and
similar. Basically, I have types based on:

{n:int | n > …

and

uint8

And when I mix them I have a couple of problems.

  1. Passing a constant into a function requires a cast like u8(10) or
    u73(12)
  2. Passing a uint8 into a function with a parameter like {n:int | …)
    requires a cast like u73(u8(20))

In some cases the constraints, as I like to call them, are equivalent in
that they they represent a number from 0 to 0xFF, but from a type point of
view they are not the same.

So, for example, with a function like this:

macdef packetOutCount =
$extval(ref(uint8),“packetOutCount”)

extern fun{} set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void
implement{} set_n {n0} (count) = let
val () = !packetOutCount := count
…
in
…
end

the line below fails to compile:

val () = !packetOutCount := count

but this compiles:

val () = !packetOutCount := u8(count)

count is restricted to values between 3 and 127, so it can’t violate a
uint8 which is restricted to values between 0 and 255.

So I tried to pick apart uint8 to see what might be the problem:

sortdef uint8 =
{ i:int | 0 <= i; i < 256 }

tkindef
uint8_kind = “atstype_uint8”
typedef
uint8_0 = g0uint (uint8_kind)
typedef
uint8_1
(i:int) = g1uint (uint8_kind, i)
//
stadef uint8 = uint8_1 // 2nd-select
stadef uint8 = uint8_0 // 1st-select
stadef uInt8 = [i:nat] uint8_1 (i)

I think it has something to do with the meaning of uint8 in:

macdef packetOutCount =
$extval(ref(uint8),“packetOutCount”)

In the above, what overloaded uint8 is getting used? Is it the uint8_kind
or uint8_0?

Is there a way to setup the macdef in such a way that I don’t have to keep
casting things?

4

You need to have the ‘extern’ keyword if the code is in a DATS file:

extern
castfn
u8_safe {n:nat | n < 256} (int(n)):<> uint8(n)On Monday, November 2, 2015 at 9:54:57 PM UTC-5, Mike Jones wrote:

I’m having problems compile the example. I also tried:

castfn
u8_safe {n: nat | n < 256} (i: int(n)):<> uint8(n)

Then I copied an example from the distribution and it failed.

Is there a compiler option or an include I need to use to make castfn
compile? Anything about the arduino_ats system that might cause a problem?