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