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 <[email protected]
> <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
>
--
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/159b8fb2-51f1-441d-b66d-7af993ee4759%40googlegroups.com.
