Why need `assertloc` for already branched condition?

[Kiwamu Okabe]

Dear all,

I wrote following code:

https://github.com/metasepi/uemacs-bohai/blob/b39da70375f9c7e7d2f8bc0a34e39c4c8efaa958/DATS/utf8.dats#L63

```
if (bytes' > 6 || bytes' > len + index)
then 1U
else
let
(* Ok, do the bytes *)
val () = assertloc (index + bytes' <= len) // xxx Why need me?
val value = loop2 (line, index, len, bytes', 1U,
($UN.cast{uint}{char} c) land (mask - 1U))
```

The code already filter `bytes' > len + index` case, but needs
`assertloc` to be compiled.

Why need `assertloc` for already branched condition?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Chris Double]

On Fri, Nov 9, 2018 at 7:23 PM Kiwamu Okabe <kiw...@debian.or.jp> wrote:
>
> Why need `assertloc` for already branched condition?

I think for the same reason described here:
https://groups.google.com/d/msg/ats-lang-users/GLsPNt-aDzM/7AzKnaFzwr0J

'||' is a macro and not given a dependent type.

--
http://bluishcoder.co.nz

[Kiwamu Okabe]

On Fri, Nov 9, 2018 at 5:38 PM Chris Double <chris....@double.co.nz> wrote:
> I think for the same reason described here:
> https://groups.google.com/d/msg/ats-lang-users/GLsPNt-aDzM/7AzKnaFzwr0J
>
> '||' is a macro and not given a dependent type.

I try to just write `if (bytes' > len + index)` as following:

```
if ($UN.cast{int}{char} c < 0xc0)
then 1U else
let
(* Ok, it's 11xxxxxx, do a stupid decode *)
val (mask, bytes') = loop1 (c, 0x20U, 0x2U)
in
(* Invalid? Do it as a single byte Latin1 *)
if (bytes' > len + index)

then 1U
else
let
(* Ok, do the bytes *)

val value = loop2 (line, index, len, bytes', 1U,
($UN.cast{uint}{char} c) land (mask - 1U))
```

But above causes following error:

```
$ make
ATS utf8.dats.c
/home/kiwamu/src/uemacs-bohai/DATS/utf8.dats: 2179(line=63, offs=30)
-- 2179(line=63, offs=30): error(3): unsolved constraint:
C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); S2Eapp(S2Ecst(+);
S2EVar(5287->S2Evar(i$3343(8455))),
S2EVar(5286->S2Evar(n$8684$8685(14342)))),
S2EVar(5289->S2Evar(m$3344(8456)))))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```

[Hongwei Xi]

There might be a logical error in your code:

bytes' > len + index

should be changed to

bytes' + index > len // or bytes' > len - index

--
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 https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkbDJu1TumPn-zwT-50USCPbg25Zhmcqz-05R9jfE8kKQ%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei and Chris,

On Fri, Nov 9, 2018 at 9:54 PM Hongwei Xi <gmh...@gmail.com> wrote:
> There might be a logical error in your code:
>
> bytes' > len + index
>
> should be changed to
>
> bytes' + index > len // or bytes' > len - index

Oh... You are right. I'm sorry.
https://www.flickr.com/photos/masterq/44005780290/

And also Chris's advise is useful. I can fix it as following:

https://github.com/metasepi/uemacs-bohai/commit/d543d5f73b14ba74fa7672e06a10d7e854727cc8
```
if ((bytes' > 6) + (bytes' > len - index))

then 1U
else
let
(* Ok, do the bytes *)
val value = loop2 (line, index, len, bytes', 1U,
($UN.cast{uint}{char} c) land (mask - 1U))

val () = !res := $UN.cast{unicode_t}{uint} value
in
bytes'
end
```


Hongwei said...

> '&&' is a macro (due to shortcut evaluation); it is not given a dependent type.
> Replacing '&&' with * (bmul) should work, though.

I have some questions:

A. I also believe we should replace `||` with + (badd). Is this correct?
B. How to write `not` in dependent type?
C. How to find such replacement between macro `&&` and `*`?

I try to grep ATS-Postiats to find `C`. But...

```
$ pwd
/home/kiwamu/src/ATS-Postiats
$ git grep bmul src | head
src/CBOOT/libc/CATS/gmp.cats:// addmul and submul compibination
src/CBOOT/libc/CATS/gmp.cats:#define atslib_mpz_submul3_mpz mpz_submul
src/CBOOT/libc/CATS/gmp.cats:#define atslib_mpz_submul3_uint mpz_submul_ui
src/CBOOT/libc/CATS/gmp.cats:#define atslib_mpz_submul3_ulint mpz_submul_ui
src/pats_constraint3.dats:| S3Ebmul _ => s2rt_bool
src/pats_constraint3.dats:| S3Ebmul (s3e1, s3e2) => let
src/pats_constraint3.dats: end // end of [S3Ebmul]
src/pats_constraint3.dats:| S3Ebmul (x11, x12) => (
src/pats_constraint3.dats: | S3Ebmul (x21, x22) =>
src/pats_constraint3.dats: ) (* end of [S3Ebmul] *)
```

Above result is hard to understand following:

* relationship between `&&` and `bmul`
* relationship between `bmul` and `*`

[Hongwei Xi]

>>A. I also believe we should replace `||` with + (badd). Is this correct?
>>B. How to write `not` in dependent type?
>>C. How to find such replacement between macro `&&` and `*`?

Yes, using '+' for '||' is correct. Many boolean functions of dependent types

are declared in the following file:

https://github.com/ats-lang/ats-lang.github.io/blob/master/ATS-Postiats/prelude/SATS/bool.sats

In practice, it is usually not about 'finding' the function you need; instead, you can always declare

it on your own.

--
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 https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkOTN3oWrTCRTLgsSZUjj4seBa5mds%2Bsd891zJqn_r5aw%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei,

On Sun, Nov 11, 2018 at 11:33 PM Hongwei Xi <gmh...@gmail.com> wrote:
> >>A. I also believe we should replace `||` with + (badd). Is this correct?
>

> Yes, using '+' for '||' is correct.

Thanks. Clear for me.

> >>B. How to write `not` in dependent type?
> >>C. How to find such replacement between macro `&&` and `*`?
>

> Many boolean functions of dependent types
> are declared in the following file:
>
> https://github.com/ats-lang/ats-lang.github.io/blob/master/ATS-Postiats/prelude/SATS/bool.sats

```
macdef || (b1, b2) = (if ,(b1) then true else ,(b2)): bool
macdef && (b1, b2) = (if ,(b1) then ,(b2) else false): bool

fun
neg_bool0
(b: bool):<> bool = "mac#%"
//
overload ~ with neg_bool0 of 0
overload not with neg_bool0 of 0

fun
add_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
fun
mul_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
//
overload + with add_bool0_bool0 of 0
overload * with mul_bool0_bool0 of 0
```

Does it mean the operators introduced with `macdef` don't provide
dependent type,
ones introduced with `overload` provide dependent type?

Also I panic on the operators with `overload`, which are just mapped
to dynamic function.

You said:

> Replacing '&&' with * (bmul) should work, though.

Where is the relationship between operator `*` and function `bmul`?

> In practice, it is usually not about 'finding' the function you need; instead, you can always declare
> it on your own.

I think above comment doesn't make sense...

I would like to use dependent types, which is well defined at prelude
or base library.
Because it makes manner of code, which is more human readable.

Why do I declare my own operator for dependent type?

[Hongwei Xi]

>>Where is the relationship between operator `*` and function `bmul`?

I misremembered. 'bmul' should be 'mul_bool1_bool1'.

--
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 https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DBp-Ntd_FACF90SucYup%2Boxpki5M%2BEufX1MmhPe%3D%3D%2BGg%40mail.gmail.com.

[Kiwamu Okabe]

On Mon, Nov 12, 2018 at 12:36 PM Hongwei Xi <gmh...@gmail.com> wrote:
> >>Where is the relationship between operator `*` and function `bmul`?
>
> I misremembered. 'bmul' should be 'mul_bool1_bool1'.

Thanks. Clear for me.

```
fun
mul_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool(b1 && b2) = "mac#%"
overload * with mul_bool1_bool1 of 20
```

Dynamics of `mul_bool1_bool1` is implemented on C code
"prelude/CATS/bool.cats", but also has statics with dependent type.

Also the implementation can be shaped on JS code
"contrib/libatscc2js/CATS/bool_cats.js".

Fantastic!!!

Thanks,