Hi all, A real-time OS, ChibiOS/RT, has system state as following:
http://www.chibios.org/dokuwiki/doku.php?id=chibios:book:kernel#system_states I wrote following code to capture the state by ATS statics: https://github.com/fpiot/chibios-ats-2/blob/b1445489b6a3d55a4cf39e74770fdb50ffb71c57/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L65 which `chss(chss_thread)` means the system state "Thread". And there are some utility functions: https://github.com/fpiot/chibios-ats-2/blob/b1445489b6a3d55a4cf39e74770fdb50ffb71c57/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L84 And then I wrote following "ISR" function, that is type-checked: ``` extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#" implement tmrfunc (pss | p) = { val () = chSysLockFromISR (pss | ) val () = chEvtBroadcastI (pss | inserted_event_p) val () = chSysUnlockFromISR (pss | ) } ``` However the other function is not type-checked: ```extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#" implement tmrfunc (pss | p) = { val () = chSysLockFromISR (pss | ) val () = if true then chEvtBroadcastI (pss | inserted_event_p) val () = chSysUnlockFromISR (pss | ) } ``` ``` $ 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: 3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): mismatch of static terms (equal): The actual term is: S2Eapp(S2Ecst(chss_ilock); ) The needed term is: S2Eapp(S2Ecst(chss_isr); ) /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): mismatch of static terms (tyleq): The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); )) The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); )) /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): the dynamic variable [pss$3868(-1)] is retained but with a type that fails to merge. /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): mismatch of static terms (equal): The actual term is: S2Eapp(S2Ecst(chss_ilock); ) The needed term is: S2Eapp(S2Ecst(chss_isr); ) /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): mismatch of static terms (tyleq): The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); )) The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); )) /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): the dynamic variable [pss$3868(-1)] is retained but with a type that fails to merge. /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); ))]. /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): mismatch of static terms (equal): The actual term is: S2Eapp(S2Ecst(chss_isr); ) The needed term is: S2Eapp(S2Ecst(chss_ilock); ) /home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats: 3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): mismatch of static terms (tyleq): The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); )) The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); )) patsopt(TRANS3): there are [3] errors in total. ``` What happens? I think I miss-understand linear type... 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/CAEvX6dknZ0JP2XscJG-X1eD1L5W7K824gXSPaXan_YprX%2BwMdg%40mail.gmail.com.
