conditional expressions and branches

[Dambaev Alexander]

Hi,

We know, that ATS is able to keep information about check in appropriate branch of 'if' expression, like:

```

fn foo( i: int): int =

  if i < 1

  then (* here typechecker knows, that i < 1*)

  else (* here typechecker knows, that i >= 1*)

```

But sometimes, you need to use more conditions and case expressions is more convenient in this case, but currently, typechecker is not always able to keep such info in branches of 'case', like:

```

fn foo( a: int, b: int): int =

  case+ 0 of

  | _ when a > 10 => ...

  | _ when a > 5 => ...

  | _ when b > 10 => ...

  | _ when b > 5 => ...

  | _ => (* 1 *)

```

It will be great, if, at least in ATS3, at mark 1 typechecker will know, that a <= 5 and b <= 5, because currently, as far as I got, condition like:

```

if a <= 5 && b <= 5

then (* 1 *)

else (* 2 *)

```

will tell typechecker, that there is a proof 'a <= 5 && b <= 5', but there are no separate proofs 'a <= 5' and 'b<=5' so you have to make a nested if-expressions to get them, which is not so compact as 'case' expressions

[Hongwei Xi]

Please use ifcase-expressions:

fun
foo
{n:int}
(n:int(n)): void =
ifcase
| n = 0 => () where {prval () = prop_verify{n == 0}()}
| n = 1 => () where {prval () = prop_verify{n == 1}()}
| _ (*else*) => () where {prval () = prop_verify{n != 0 && n != 1}()}

######

Also, you can use '+' and '*' for || and &&, respectively. For instance,

if a <= 5 * b <= 5 then ... else ...

And '+' and '*' have the types expected by you.

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KxS8iGdxHRjVU2MJu_%2B5g143Lq6HKFo%2BRta06aF3ENdgg%40mail.gmail.com.

[Hongwei Xi]

Forgot to mention that you need parentheses:

(a <= 5) * (b <= 5)

[Dambaev Alexander]

Oh, that is actually very helpful! Thanks a lot. Looks like I am using too little tutorials to search for ATS's syntax :)