== is not defined for terms of datasort chss. Don't define chss as a datasort. Try:
sortdef chss = int #define chss_init 0 #define chss_ilock ... On Wed, Jun 15, 2016 at 12:07 AM, Kiwamu Okabe <[email protected]> wrote: > Hi Hongwei, > I have more questions... > > If `chEvtBroadcastI` should be only called from both S-Locked and > I-Locked state, > then the code is written with following: > > ``` > datasort chss = > | chss_init | chss_thread | chss_irqsusp | chss_irqdisable | > chss_irqwait | chss_isr | chss_slock | chss_ilock > absvtype chss(s:chss) > vtypedef chss_anylock = [s:chss | s == chss_slock || s == chss_ilock] > chss(s) > > extern fun chEvtBroadcastI (!chss_anylock | cPtr0(event_source_t)): > void = "mac#" > > extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#" > implement tmrfunc (pss | p) = { > val () = chSysLockFromISR (pss | ) > val () = chEvtBroadcastI (pss | removed_event_p) > val () = chSysUnlockFromISR (pss | ) > } > > extern fun tmr_init (!chss(chss_thread) | ptr): void = "mac#" > implement tmr_init (pss | p) = { > val () = chSysLock (pss | ) > val () = chEvtBroadcastI (pss | removed_event_p) > val () = chSysUnlock (pss | ) > } > ``` > > But the code can't be type-checked: > > ``` > patsopt -o build/obj/main.c -d main.dats > > /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: > 3392(line=98, offs=28) -- 3415(line=98, offs=51): error(3): unsolved > constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(||); > S2Eapp(S2Ecst(==); S2EVar(4505->S2Eapp(S2Ecst(chss_ilock); )), > S2Eapp(S2Ecst(chss_slock); )), S2Eapp(S2Ecst(==); > S2EVar(4505->S2Eapp(S2Ecst(chss_ilock); )), S2Eapp(S2Ecst(chss_ilock); > )))) > 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) > ``` > > How to define linear type as `chss_anylock`? > > 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/CAEvX6dkn15HFdDQ8zW9Yav3mqMk9hKJgc-333D2_U4byqx2qnw%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/CAPPSPLqMTqP12Ftb4CN4N9kM16EjyF1sy4T_F9B9WXXCHJe%3Dxg%40mail.gmail.com.
