Real-time OS system state captured by ATS language (and questions)

Google Group
1

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:

ChibiOS free embedded RTOS - This topic does not exist yet

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:

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

2

Or you can turn chss_p into a predicate:

stacst chss_p : (int) → bool

Please take a look at the following code:

There are many ways to address this issue. I don’t feel it is worth the
effort right now because
I don’t see that anyone would be using a type like chss(10). If it turns
out to be a real problem,
then you can always try to fix it later. Right now, this is all imaginary.On Wed, Jun 22, 2016 at 12:06 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei,
sorry for my waywardness.

On Sun, Jun 19, 2016 at 12:38 AM, gmhwxi gmh...@gmail.com wrote:

What you need can be captured in ATS as follows:

(* ****** ****** )
//
dataprop
chss_p(int) = {s:int | s <= 7} CHSS(s) of ()
//
( ****** ****** *)
//
abst@ype event_source_t
//
extern
fun
chEvtObjectInit
{s:int}
(!chss(s), chss_p(s) | cPtr0(event_source_t)): void = “mac#”

I feed the using chss_p on every function is messy, because every
function needs two proof value…

Is it able to define absvtype chss(s:int) as private definition?
Please imagine following:

absvtype chss(s:int)
vtypedef chss_sinit = chss(chss_init)
vtypedef chss_any = [s:int | chss_init <= s; s <= chss_ilock] chss(s)
vtypedef chss_iclass = [s:int | s == chss_slock || s == chss_ilock] chss(s)

I think threre are no miss calling like chss(10) in application
code, if application programmer is
permitted to access chss_sinit / chss_any / chss_iclass and
prohibited to access chss,

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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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/CAEvX6d%3D-v%3DO8YNpRCzz6pSG7ouTthQzbG9479hotsfoG35F-ZQ%40mail.gmail.com
.

3

foofunc cannot be used as long as there is no way
to produce a value of the type chss(10).

You can form the type chss(10), but you should allow
a value of this type to be formed.

For instance, list(string, ~1) is a valid type but there is
no value of such a type.On Wed, Jun 15, 2016 at 4:13 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei,

On Wed, Jun 15, 2016 at 4:55 PM, Hongwei Xi gmh...@gmail.com wrote:

chss is not a sort; it is a subset sort, which can not be
used to index a type. Try:

abstype chss(int)

praxi lemma_chss{n:int} (!chss(n)): [0 <= n; n <= 7] void

I wrote following code:

#define chss_init       0
#define chss_ilock      7
absvtype chss(s:int)
extern praxi lemma_chss {n:int} (!chss(n)): [chss_init <= n; n <=
chss_ilock] void

fun foofunc (pss: !chss(10) | p: ptr): void = {
}

However it’s type-checked…
How to avoid out of bound over the chss’s int?
How to use lemma_chss?

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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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/CAEvX6dktUiGvAz40Qi_wDgoHazyYuSAKNMPXEUbS%3Dok7reDm%2BQ%40mail.gmail.com
.

4

You need to the following annotation:

if :(pss: chss(chss_ilock)) =>
true then chEvtBroadcastI (pss | inserted_event_p)

If no annotation is given, then the following default is assumed:

if :(pss: chss(chss_isr)) =>
true then chEvtBroadcastI (pss | inserted_event_p)

This is due to ‘pss’ being originally given the type chss(chss_isr)

If you do:

prval pss2 = pss

then the ‘original’ type for pss2 is chss(chss_isr). So if you use
pss2, you do not need to provide an explicit state type annotation.On Sunday, June 12, 2016 at 11:37:13 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Sun, Jun 12, 2016 at 9:38 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

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:

Redirecting to Google Groups

Sorry. I can’t imagine how to apply the state type annotation to my
situation…
Could you show more detail in the example?

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)

Your code is type-checked.
However, why is renaming pss needed? I think simple renaming is not
hint for ATS2 compiler…

Best regards,

Kiwamu Okabe at METASEPI DESIGN

5

What you need can be captured in ATS as follows:

(* ****** ****** )
//
dataprop
chss_p(int) = {s:int | s <= 7} CHSS(s) of ()
//
( ****** ****** )
//
abst@ype event_source_t
//
extern
fun
chEvtObjectInit
{s:int}
(!chss(s), chss_p(s) | cPtr0(event_source_t)): void = “mac#”
//
( ****** ****** *)On Saturday, June 18, 2016 at 6:38:40 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Thu, Jun 16, 2016 at 12:58 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

Typechecking can only be perfomed on ATS code.

If you call foofunc in C, there is no safety guarantee.

By the way, the example does not seem to be interesting because
barfunc cannot make any real use of pss.

With your advice, my code is finally shaped as following:

https://github.com/fpiot/chibios-ats-2/blob/720847a31b9417ee267a34bf1746802e916ce03b/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L64

The code is type-checked, and captures system state for ch* function well.
However the code can’t catch the error such like following:

extern fun chEvtObjectInit (!chss(10) | cPtr0(event_source_t)): void = 
"mac#"

I think ATS compiler can capture the error, if it supports int’s
bounds depended by absvtype chss.
I hope the supporting becomes in future.

Best regards,

Kiwamu Okabe at METASEPI DESIGN

6

Great!

Posted as a news piece at http://www.ats-lang.org/Community.htmlFrom: Kiwamu Okabe kiw...@debian.or.jp
Date: Fri, Jul 8, 2016 at 10:38 AM
Subject: Re: Real-time OS system state captured by ATS language (and
questions)
To: ats-lang-users ats-lan...@googlegroups.com

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:

Today, I talk about this topic at ML study meeting.
The slide is found at following:

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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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/CAEvX6dnSJp%2BsvQMESv19bVrFvZGUT_to7JrXOUwALC44F2Ya_A%40mail.gmail.com
.

7

Such use of initial types only involves if-expressions and case-expressions.On Tuesday, June 14, 2016 at 11:49:24 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Mon, Jun 13, 2016 at 1:04 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

You need to the following annotation:

if :(pss: chss(chss_ilock)) =>
true then chEvtBroadcastI (pss | inserted_event_p)

If no annotation is given, then the following default is assumed:

if :(pss: chss(chss_isr)) =>
true then chEvtBroadcastI (pss | inserted_event_p)

This is due to ‘pss’ being originally given the type chss(chss_isr)

Umm…
The pss is introduced as chss(chss_isr) at the tmrfunc function.
However the chEvtBroadcastI function doesn’t know that it was
changed into chss(chss_ilock)?
If so, how does chSysUnlockFromISR function know the changing?

If you do:

prval pss2 = pss

then the ‘original’ type for pss2 is chss(chss_isr). So if you use
pss2, you do not need to provide an explicit state type annotation.

I think it makes sense.
Does it mean that ‘initial’ type of linear type is only used in if
expression?

Best regards,

Kiwamu Okabe at METASEPI DESIGN

8

Typechecking can only be perfomed on ATS code.

If you call foofunc in C, there is no safety guarantee.

By the way, the example does not seem to be interesting because
barfunc cannot make any real use of pss.On Wed, Jun 15, 2016 at 11:36 PM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei,

On Wed, Jun 15, 2016 at 10:19 PM, Hongwei Xi gmh...@gmail.com wrote:

foofunc cannot be used as long as there is no way
to produce a value of the type chss(10).

You can form the type chss(10), but you should allow
a value of this type to be formed.

For instance, list(string, ~1) is a valid type but there is
no value of such a type.

Ah, I understand it.

However I can write following code:

extern praxi lemma_chss {n:int} (!chss(n)): [chss_init <= n; n <=
chss_ilock] void

fun barfunc (pss: !chss(10) | p: ptr): void = {}

extern fun foofunc (!chss(10) | ptr): void = "mac#"
implement foofunc (pss | p) = barfunc (pss | p)

The code is type-checked. And the foofunc function can be called
from C language.
What kind of error does it avoid?

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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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/CAEvX6dm%3D7BRN%3DN8EssYOtX5gH6E9ZbzO8im676zrcD5fVMjJkg%40mail.gmail.com
.

9

You can introduce it, but the constraint solver does not understand it.

You need to introduce a dataprop:

dataprop EQCHSS(chss, chss) = EQCHSS of ()

But this is not easy to use. I think the easiest way is to define chss as
int.On Wednesday, June 15, 2016 at 3:42:25 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Wed, Jun 15, 2016 at 1:23 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

== 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 …

There are no method to introduce == operation over my datasort?
May I use stacst for it?

Best regards,

Kiwamu Okabe at METASEPI DESIGN

10

I want to use this occasion to mention a bit of experience I gathered in
the past.
In my opinion, one should avoid trying to over-use types to capture
programming errors.
It rarely pays if you try to target imaginary programming errors.

Many programmers think that program verification means to verify that a
program is “100%”
correct (whatever it means). I thought likewise but I now think that
program verification is just
some form of static debugging; it is meant to make a programmer more
productive than if one
solely relies on dynamic debugging.

Too many programmers gave up ATS because they tried to do too much with
types. Instead of
relying on typechecking to flush out potential bugs, they fought against
typechecking futilely.On Wednesday, June 22, 2016 at 11:59:53 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Wed, Jun 22, 2016 at 1:33 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

Or you can turn chss_p into a predicate:

stacst chss_p : (int) → bool

Please take a look at the following code:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/test37.dats

Thanks. However this style needs injecting {s:int | chss_p(s)} into
every function…

There are many ways to address this issue. I don’t feel it is worth the
effort right now because
I don’t see that anyone would be using a type like chss(10). If it turns
out
to be a real problem,
then you can always try to fix it later. Right now, this is all
imaginary.

Yes, you are right. This issue should occur when following:

  • Application’s function is introduced with a bad state number such
    like chss(10), and…
  • All of system API called by the function has a bad state number.

Then I think that such error caused by bad state number is rare case.

Thanks,

Kiwamu Okabe at METASEPI DESIGN

11

chss is not a sort; it is a subset sort, which can not be
used to index a type. Try:

abstype chss(int)

praxi lemma_chss{n:int} (!chss(n)): [0 <= n; n <= 7] voidOn Wed, Jun 15, 2016 at 3:52 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei,

On Wed, Jun 15, 2016 at 1:23 PM, Hongwei Xi gmh...@gmail.com wrote:

== 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 …

It’s type-checked.

Next, I would like to specify bound of sort chss.
However following code is not type-checked…

#define chss_init       0
#define chss_thread     1
#define chss_irqsusp    2
#define chss_irqdisable 3
#define chss_irqwait    4
#define chss_isr        5
#define chss_slock      6
#define chss_ilock      7
sortdef chss = { i:int | chss_init <= i; i <= chss_ilock }
absvtype chss(s:chss)


/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
1952(line=74, offs=17) -- 1956(line=74, offs=21): error(2): the
identifier [chss] is expected to refer to a sort (instead of a subset
sort).

I found above style in ATS-Postiats-contrib.
The style can’t be used with absvtype?

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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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/CAEvX6dnX68Ryu0SzSYuGRfj4xgMjr6OWXTGPndaLFXMFaL0Vbw%40mail.gmail.com
.

12

== 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 kiw...@debian.or.jp 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 ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
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
.

13

I do not understand this question.

Why can’t you define vtfunc_t as follows:

typedef
vtfunc_t = (!chss(chss_isr) | ptr) → voidOn Saturday, June 18, 2016 at 6:48:48 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

I have the other question. Following code has chVTSetI function:

https://github.com/fpiot/chibios-ats-2/blob/720847a31b9417ee267a34bf1746802e916ce03b/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L84

The chVTSetI function has following type:

typedef vtfunc_t = ptr -> void 
extern fun chVTSetI (!chss_iclass | cPtr0(virtual_timer_t), systime_t, 
vtfunc_t, cPtr0(BaseBlockDevice)): void = "mac#"

The chVTSetI uses following tmrfunc as 3rd argument:

extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"

I would like to write the chVTSetI applying as following:

val () = chVTSetI (pss | tmr_p, MS2ST (POLLING_DELAY), tmrfunc, bbdp)

However the above code can’t be shaped and I should use cast as following,
because typedef keyword can’t define proof argument in the definition:

val () = chVTSetI (pss | tmr_p, MS2ST (POLLING_DELAY), 
$UN.cast{vtfunc_t}(tmrfunc), bbdp)

Are there methods to define envless function typedef includes proof
argument?

Best regards,

Kiwamu Okabe