Re: conditional expressions and branches
Oh, that is actually very helpful! Thanks a lot. Looks like I am using too little tutorials to search for ATS's syntax :) -- 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-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KyRt8y-W3tKDR6j7iifRCqwZnc88zkSFBahMpUwN%3DTYTQ%40mail.gmail.com.
Re: conditional expressions and branches
Forgot to mention that you need parentheses:
(a <= 5) * (b <= 5)
On Sat, Jul 25, 2020 at 10:55 PM Hongwei Xi wrote:
>
> 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.
>
>
>
>
> On Sat, Jul 25, 2020 at 10:35 PM Dambaev Alexander
> wrote:
>
>> 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
>>
>> --
>> 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-users+unsubscr...@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
>>
>> .
>>
>
--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLpks-nnuS8yd_6QfasOQP2dN%2B7LyC%2BDAbXPA5HEdf%3DShg%40mail.gmail.com.
Re: conditional expressions and branches
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.
On Sat, Jul 25, 2020 at 10:35 PM Dambaev Alexander
wrote:
> 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
>
> --
> 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-users+unsubscr...@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
>
> .
>
--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoAtWmL0kRe1Hpd5P%3DPMazOkzg5VeZr2pVAn%2B%3D%3DF2teEQ%40mail.gmail.com.
conditional expressions and branches
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 -- 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-users+unsubscr...@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.
