>>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. On Sun, Nov 11, 2018 at 2:14 AM Kiwamu Okabe <[email protected]> wrote: > Dear Hongwei and Chris, > > On Fri, Nov 9, 2018 at 9:54 PM Hongwei Xi <[email protected]> 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 [email protected]. > To post to this group, send email to [email protected]. > 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 > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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/CAPPSPLoVmvHALnYAE%2BS%2BrRVi0e1Je78NAZb8ODfEa%2B9OZgCaiw%40mail.gmail.com.
