state type annotation

[gmhwxi]

Sometimes, one needs to add a state type annotation
to an if-then-else expression in ATS. Here is a simple example:

//
fun
foo{i:nat}
  (x: int(i), y: int(i+1)): void = ()
//
(* ****** ****** *)

implement
main0 () = () where
{
//
var x: int
var y: int
//
val i = (1: intGte(0))
//
val () = (
//
if: [i:nat]
(
  x: int(i), y: int(i+1)
) => (i >= 1)
  then (x := i; y := x+1)
  else (x := 10; y := 11)
//
) : void // end of [val]
//
val () = foo(x, y)
//
val () = println! ("x = ", x, "and y = ", y)
//
} (* end of [main0] *)

Without the annotation, foo(x, y) cannot pass typechecking in ATS.

You can also use state type annotation with case-expressions as well.

Here are some examples:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/ifhead.dats
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/casehead.dats

[gmhwxi]

I forgot that the new trend should be using glot.io :)

https://glot.io/snippets/eex5kpwvqd