>>val () = if true then chEvtBroadcastI (pss | inserted_event_p) 

The system does not know what type should be given to pss. You
need state type annotation:

https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!topic/ats-lang-users/WfatF27cyDc

if chEvtBroachcastI does not change the type of pss, you may just do

prval pss2 = pss
val () = if true then chEvtBroadcastI (pss2 | inserted_event_p)
...
prval () = (pss := pss2)



On Sunday, June 12, 2016 at 6:42:43 AM UTC-4, Kiwamu Okabe wrote:
>
> 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/2ea20179-c8c4-4ad5-8006-d0ac89b40b25%40googlegroups.com.

Reply via email to