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
On Wed, Jun 15, 2016 at 3:52 AM, Kiwamu Okabe <[email protected]> wrote:
> Hi Hongwei,
>
> On Wed, Jun 15, 2016 at 1:23 PM, Hongwei Xi <[email protected]> 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 [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/CAEvX6dnX68Ryu0SzSYuGRfj4xgMjr6OWXTGPndaLFXMFaL0Vbw%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/CAPPSPLrDazPqi6eTN1L-urhmL_x13S797xembRrOP6Q2rMe0Cg%40mail.gmail.com.
