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 `*`

Best regards,
-- 
Kiwamu Okabe at METASEPI DESIGN

-- 
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 post to this group, send email to ats-lang-users@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.

Reply via email to