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 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 <[email protected]> wrote: > Hi Hongwei, > sorry for my waywardness. > > On Sun, Jun 19, 2016 at 12:38 AM, gmhwxi <[email protected]> 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 [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/CAEvX6d%3D-v%3DO8YNpRCzz6pSG7ouTthQzbG9479hotsfoG35F-ZQ%40mail.gmail.com > . > -- 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/CAPPSPLoxks98cd-2%2B5MgovgV9m-o56A7CMWWVsDb_fKEu3mEUQ%40mail.gmail.com.
