Is there a way to change i:int to i:uint8 and make the matching compile?
uint8 has a kindef but that does not appear to be enough.
fun to_digit (i: int) : char =
case+ i of
| 0 => '0'
| 1 => '1'
| 2 => '2'
| 3 => '3'
| 4 => '4'
| 5 => '5'
| 6 => '6'
| 7 => '7'
| 8 => '8'
| 9 => '9'
| 10 => 'A'
| 11 => 'B'
| 12 => 'C'
| 13 => 'D'
| 14 => 'E'
| 15 => 'F'
| _ => '0'I need to clarify a couple of things.
fun
u8{i:uint8}
(i: int(i)): uint8(i) = cast{uint8(i)}(i)I interpret this to mean:
for all i:uint8 I can pass in an int that is restricted to a value 0-255
and it returns a uint8 with the same 0-255 restriction.Pretty nice actually.
Yes, the sort uint8 is defined as follows:
sortdef uint8 = {i:nat | i < 256}
But, when I call like this:
val value = 2: uint8
val _ = to_digit(u8_(value >> 4))It can’t seem to check that a shifted value is within the constraint.
That just means to me the constraint solver does not handle shifts. So as
the caller to to_digit, I would need to certify that the value meets the
requirement with some kind of cast. Is there a general form of cast that
can include something like cast{i:uint8 | i < 16}(value >> 4)?
The type for ‘>>’ is not accurate enough to capture what you want here.
val value = 2
val value2 = value >> 4
val value3 = g1ofg0(value3)
val () = ckastloc_gintBtw(value3, 0, 16)
// at this point, the compiler knows 0 <= value3 < 16
As an alternative, I suppose I could create a function that does the
conversion, with either a run time check that aborts, or with some range
clamping, etc. But if I do that, all I did was move the original clamping,
the side effect of a pattern match on anything that returns 0, to another
place in the code.
In general, you want errors to be reported as early as possible. For
instance, we could return 0 (instead of raising an exception) if the index
used to access an integer array is
out-of-bounds, but this can complicate debugging so much!
I know there is no ultimate escape if bytes are given the program via USB
and they must be interpreted as hex, it is more a matter of where they are
checked, clamped, or cause an error to be returned by USB. But I would like
to know how you would handle this. Would you make a function to get from
byte to constrained hex byte, use a cast, etc.
I would try to identify and report errors as soon as possible.
I need to clarify a couple of things.
fun
u8{i:uint8}
(i: int(i)): uint8(i) = cast{uint8(i)}(i)
I interpret this to mean:
for all i:uint8 I can pass in an int that is restricted to a value 0-255
and it returns a uint8 with the same 0-255 restriction.
Pretty nice actually.
But, when I call like this:
val value = 2: uint8
val _ = to_digit(u8_(value >> 4))
It can’t seem to check that a shifted value is within the constraint.
That just means to me the constraint solver does not handle shifts. So as
the caller to to_digit, I would need to certify that the value meets the
requirement with some kind of cast. Is there a general form of cast that
can include something like cast{i:uint8 | i < 16}(value >> 4)?
As an alternative, I suppose I could create a function that does the
conversion, with either a run time check that aborts, or with some range
clamping, etc. But if I do that, all I did was move the original clamping,
the side effect of a pattern match on anything that returns 0, to another
place in the code.
I know there is no ultimate escape if bytes are given the program via USB
and they must be interpreted as hex, it is more a matter of where they are
checked, clamped, or cause an error to be returned by USB. But I would like
to know how you would handle this. Would you make a function to get from
byte to constrained hex byte, use a cast, etc.
How about writing something like:
fun
to_digit
(
i: uint8
) : char = let
val i = $UN.cast2int(i)
in
case+ i of …
end // end of [to_digit]
Currently, only integers of the type ‘int’ and ‘uint’ can be used as
patterns.On Sun, Oct 11, 2015 at 9:58 AM, Mike Jones proc...@gmail.com wrote:
Is there a way to change i:int to i:uint8 and make the matching compile?
uint8 has a kindef but that does not appear to be enough.fun to_digit (i: int) : char = case+ i of | 0 => '0' | 1 => '1' | 2 => '2' | 3 => '3' | 4 => '4' | 5 => '5' | 6 => '6' | 7 => '7' | 8 => '8' | 9 => '9' | 10 => 'A' | 11 => 'B' | 12 => 'C' | 13 => 'D' | 14 => 'E' | 15 => 'F' | _ => '0'–
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/a2804806-8898-45d5-8b82-df5e43dc4aca%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a2804806-8898-45d5-8b82-df5e43dc4aca%40googlegroups.com?utm_medium=email&utm_source=footer
.
In general, it is a good idea to provide a to_digit of the following type:
fun to_digit {i:nat | i < 16} (uint8(i)): char
See:
In this way, the caller has the responsibility to make sure that to_digit
can only be applied to
natural numbers less than 16.On Sunday, October 11, 2015 at 11:20:10 AM UTC-4, gmhwxi wrote:
How about writing something like:
fun
to_digit
(
i: uint8
) : char = let
val i = $UN.cast2int(i)
in
case+ i of …
end // end of [to_digit]Currently, only integers of the type ‘int’ and ‘uint’ can be used as
patterns.On Sun, Oct 11, 2015 at 9:58 AM, Mike Jones wrote:
Is there a way to change i:int to i:uint8 and make the matching compile?
uint8 has a kindef but that does not appear to be enough.fun to_digit (i: int) : char = case+ i of | 0 => '0' | 1 => '1' | 2 => '2' | 3 => '3' | 4 => '4' | 5 => '5' | 6 => '6' | 7 => '7' | 8 => '8' | 9 => '9' | 10 => 'A' | 11 => 'B' | 12 => 'C' | 13 => 'D' | 14 => 'E' | 15 => 'F' | _ => '0'