Pattern match on uint8

[Mike Jones]

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'

[Hongwei Xi]

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.

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

[gmhwxi]

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:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST10/test18.dats

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.

[Mike Jones]

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.

[gmhwxi]

On Tuesday, October 13, 2015 at 9:31:27 AM UTC-4, Mike Jones wrote:

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.