# Bitwise operations

**URL:** <https://discourse.ats-lang.org/t/bitwise-operations/471>\
**Category:** Google Group\
**Created:** [September 1, 2014, 5:18am UTC](https://discourse.ats-lang.org/t/bitwise-operations/471 "2014-09-01T05:18:52Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [September 1, 2014, 5:18am UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/1 "2014-09-01T05:18:52Z")

</div>

Hi all,

Does ATS support any bitwise operations on ints in the statics?

~Shea

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [September 2, 2014, 1:56pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/2 "2014-09-02T13:56:12Z")

</div>

Hi Will,

This sounds great! Let me know if you need any help testing.

~SheaOn Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:

> > Hm, how do I spell the operations? I’ve got something like this to  
> > represent the arguments to the ‘socket’ function, which on Linux allows  
> > the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> > prefix indicates a macro taken from a C include):
> 
> Right now using bitwise operators in the statics is a bit experimental with an  
> external constraint solver. I’m working on getting the solver into the main  
> ATS contrib repo so others may use it as well.
> 
> As far as syntax goes, you probably won’t want to use the “int” sort  
> since any static int  
> term is considered a natural number without bound. Instead, we can use  
> a new sort  
> called a bit vector that models machine integers. This sort is  
> provided by most SMT  
> solvers so we can use it in the ATS statics.
> 
> If I understand your requirement correctly, suppose we have the  
> following type at our  
> disposal. This is hardly official, but it illustrates how I think you  
> could implement the example  
> you provided. This currently won’t work in ATS right now.
> 
> ```
> abst@ype int (bv:bv16) = int
> 
> ```
> 
> This associates a static signed 16 bit vector with the normal integer  
> type. Of course, the choice of  
> what size bit vector to use is machine dependent, but that’s a  
> separate issue. We can rewrite your  
> example using the new bv16 sort in the statics using the lor operator  
> described by Hongwei.
> 
> dataprop domain(bv16) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> address families \*)
> 
> dataprop type\_base(bv16) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> include other socket types \*)
> 
> dataprop type\_modifier(bv16) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> 
> dataprop type(bv16) =  
> | {t: bv16} base (t) of (type\_base(bv16))  
> | {t, m: bv16} or ((t lor m)) of (type(t), type\_modifier(m))
> 
> fn socket {d, t: bv16} (domain d, type t | int d, int t): [fd: int]  
> (filedes fd | int fd)
> 
> I need to finish adding more support for bit vectors in the external  
> constraint solver, but I’ll post an announcement when  
> it’s ready to use.
> 
> Thanks,  
> Will
> 
> On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> 
> > Hm, how do I spell the operations? I’ve got something like this to  
> > represent the arguments to the ‘socket’ function, which on Linux allows  
> > the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> > prefix indicates a macro taken from a C include):
> > 
> > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other address families \*)
> > > 
> > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include other socket types \*)
> > > 
> > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) | SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > 
> > > dataprop type(int) =  
> > > | {t: int} base (t) of (type\_base(t))  
> > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > 
> > > (\* TODO include protocol argument _)  
> > > (_ TODO error handling \*)  
> > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int] (filedes fd | int fd)
> > 
> > This fails with:
> > 
> > > the static expression needs to be impredicative but is assigned the sort [S2RTbas(S2RTBASpre(int))]
> > 
> > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > semantics, of course).
> > 
> > ~Shea
> > 
> > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > 
> > > Right now, constraints involving bitwise operations can be  
> > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > such constraints.
> > > 
> > > Will Blair should have something to say on this issue. He has managed  
> > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > readily handle bitwise operations.
> > > 
> > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> > > 
> > > > Hi all,
> > > > 
> > > > Does ATS support any bitwise operations on ints in the statics?
> > > > 
> > > > ~Shea
> > > > 
> > > > –  
> > > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)  
> > > > .
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [September 1, 2014, 5:33am UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/3 "2014-09-01T05:33:32Z")

</div>

Right now, constraints involving bitwise operations can be  
generated., but the built-in constraint-solver in ATS cannot handle  
such constraints.

Will Blair should have something to say on this issue. He has managed  
to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
readily handle bitwise operations.On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> Hi all,
> 
> Does ATS support any bitwise operations on ints in the statics?
> 
> ~Shea
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [September 1, 2014, 6:31pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/4 "2014-09-01T18:31:08Z")

</div>

lor is already given the infix status. So write (t lor m) instead.On Mon, Sep 1, 2014 at 2:25 PM, Hongwei Xi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> You can introduce a static function as follows:
> 
> // lor for bitwise or  
> stacst lor\_int\_int : (int, int) → int  
> stadef lor = lor\_int\_int // aliasing
> 
> dataprop type(int) =  
> | {t: int} base (t) of (type\_base(t))  
> | {t, m: int} or (lor(t, m)) of (type(t), type\_modifier(m))
> 
> Here is some code that may be helpful:
> 
> [https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics\_pre.sats](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_pre.sats)
> 
> On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> 
> > Hm, how do I spell the operations? I’ve got something like this to  
> > represent the arguments to the ‘socket’ function, which on Linux allows  
> > the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> > prefix indicates a macro taken from a C include):
> > 
> > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > address families \*)
> > > 
> > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include  
> > > other socket types \*)
> > > 
> > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > 
> > > dataprop type(int) =  
> > > | {t: int} base (t) of (type\_base(t))  
> > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > 
> > > (\* TODO include protocol argument _)  
> > > (_ TODO error handling \*)  
> > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > > (filedes fd | int fd)
> > 
> > This fails with:
> > 
> > > the static expression needs to be impredicative but is assigned the  
> > > sort [S2RTbas(S2RTBASpre(int))]
> > 
> > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > semantics, of course).
> > 
> > ~Shea
> > 
> > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > 
> > > Right now, constraints involving bitwise operations can be  
> > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > such constraints.
> > > 
> > > Will Blair should have something to say on this issue. He has managed  
> > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > readily handle bitwise operations.
> > > 
> > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> > > 
> > > > Hi all,
> > > > 
> > > > Does ATS support any bitwise operations on ints in the statics?
> > > > 
> > > > ~Shea
> > > > 
> > > > –  
> > > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit
> > 
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> > 
> > > > .
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net)  
> > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [September 1, 2014, 6:25pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/5 "2014-09-01T18:25:07Z")

</div>

You can introduce a static function as follows:

// lor for bitwise or  
stacst lor\_int\_int : (int, int) → int  
stadef lor = lor\_int\_int // aliasing

dataprop type(int) =  
| {t: int} base (t) of (type\_base(t))  
| {t, m: int} or (lor(t, m)) of (type(t), type\_modifier(m))

Here is some code that may be helpful:

[https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics\_pre.satsOn](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_pre.satsOn) Mon, Sep 1, 2014 at 2:08 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> Hm, how do I spell the operations? I’ve got something like this to  
> represent the arguments to the ‘socket’ function, which on Linux allows  
> the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> prefix indicates a macro taken from a C include):
> 
> > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > address families \*)
> > 
> > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include  
> > other socket types \*)
> > 
> > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > 
> > dataprop type(int) =  
> > | {t: int} base (t) of (type\_base(t))  
> > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > 
> > (\* TODO include protocol argument _)  
> > (_ TODO error handling \*)  
> > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > (filedes fd | int fd)
> 
> This fails with:
> 
> > the static expression needs to be impredicative but is assigned the sort  
> > [S2RTbas(S2RTBASpre(int))]
> 
> twice (apparently one for the t and one for the m in ((t | m)). If I  
> replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> semantics, of course).
> 
> ~Shea
> 
> On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> 
> > Right now, constraints involving bitwise operations can be  
> > generated., but the built-in constraint-solver in ATS cannot handle  
> > such constraints.
> > 
> > Will Blair should have something to say on this issue. He has managed  
> > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > readily handle bitwise operations.
> > 
> > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> > 
> > > Hi all,
> > > 
> > > Does ATS support any bitwise operations on ints in the statics?
> > > 
> > > ~Shea
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit
> 
> [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> 
> > > .
> > 
> > –  
> > 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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net)  
> .

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [September 1, 2014, 7:29pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/6 "2014-09-01T19:29:38Z")

</div>

Ah, I see. How do I implement the static function? All of the ones in  
the prelude appear to be built in.

~SheaOn Mon, Sep 01, 2014 at 02:25:07PM -0400, Hongwei Xi wrote:

> You can introduce a static function as follows:
> 
> // lor for bitwise or  
> stacst lor\_int\_int : (int, int) → int  
> stadef lor = lor\_int\_int // aliasing
> 
> dataprop type(int) =  
> | {t: int} base (t) of (type\_base(t))  
> | {t, m: int} or (lor(t, m)) of (type(t), type\_modifier(m))
> 
> Here is some code that may be helpful:
> 
> [https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics\_pre.sats](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_pre.sats)
> 
> On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> 
> > Hm, how do I spell the operations? I’ve got something like this to  
> > represent the arguments to the ‘socket’ function, which on Linux allows  
> > the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> > prefix indicates a macro taken from a C include):
> > 
> > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > address families \*)
> > > 
> > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include  
> > > other socket types \*)
> > > 
> > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > 
> > > dataprop type(int) =  
> > > | {t: int} base (t) of (type\_base(t))  
> > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > 
> > > (\* TODO include protocol argument _)  
> > > (_ TODO error handling \*)  
> > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > > (filedes fd | int fd)
> > 
> > This fails with:
> > 
> > > the static expression needs to be impredicative but is assigned the sort  
> > > [S2RTbas(S2RTBASpre(int))]
> > 
> > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > semantics, of course).
> > 
> > ~Shea
> > 
> > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > 
> > > Right now, constraints involving bitwise operations can be  
> > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > such constraints.
> > > 
> > > Will Blair should have something to say on this issue. He has managed  
> > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > readily handle bitwise operations.
> > > 
> > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> > > 
> > > > Hi all,
> > > > 
> > > > Does ATS support any bitwise operations on ints in the statics?
> > > > 
> > > > ~Shea
> > > > 
> > > > –  
> > > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit
> > 
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> > 
> > > > .
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net)  
> > .
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB\_tUqXkYXGVA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB_tUqXkYXGVA%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 12, 2015, 2:25pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/7 "2015-12-12T14:25:41Z")

</div>

There is no sort for unsigned integers.On Saturday, December 12, 2015 at 9:21:43 AM UTC-5, Yannick Duchêne wrote:

> I just had the same question and just read this thread.
> 
> So for now, it seems better to do it with classical arithmetic operations:  
> additions and subtractions, and appropriates tests with lower than, greater  
> than, etc, and constants (as #define) for bits sets.
> 
> By the way, I also wondered if there is a sort for unsigned integers. I  
> mean a sort, not a subset sort.
> 
> Le lundi 1 septembre 2014 07:18:57 UTC+2, Shea Levy a écrit :
> 
> > Hi all,
> > 
> > Does ATS support any bitwise operations on ints in the statics?
> > 
> > ~Shea

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [September 1, 2014, 7:36pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/8 "2014-09-01T19:36:58Z")

</div>

No, static functions cannot be implemented in ATS.  
You need a constraint-solver to interpret them. The built-in  
constraint-solver for ATS does not handle bitwise operations.  
Z3 does. Maybe Will Blair will let us know how to do it when  
he is back.On Monday, September 1, 2014 3:29:41 PM UTC-4, Shea Levy wrote:

> Ah, I see. How do I implement the static function? All of the ones in  
> the prelude appear to be built in.
> 
> ~Shea
> 
> On Mon, Sep 01, 2014 at 02:25:07PM -0400, Hongwei Xi wrote:
> 
> > You can introduce a static function as follows:
> > 
> > // lor for bitwise or  
> > stacst lor\_int\_int : (int, int) → int  
> > stadef lor = lor\_int\_int // aliasing
> > 
> > dataprop type(int) =  
> > | {t: int} base (t) of (type\_base(t))  
> > | {t, m: int} or (lor(t, m)) of (type(t), type\_modifier(m))
> > 
> > Here is some code that may be helpful:
> 
> [https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics\_pre.sats](https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_pre.sats)
> 
> > On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > 
> > > Hm, how do I spell the operations? I’ve got something like this to  
> > > represent the arguments to the ‘socket’ function, which on Linux  
> > > allows  
> > > the ‘type’ argument to be bitwise-ored with certain modifiers (the  
> > > ATS\_  
> > > prefix indicates a macro taken from a C include):
> > > 
> > > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > > address families \*)
> > > > 
> > > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> > > > include  
> > > > other socket types \*)
> > > > 
> > > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > > 
> > > > dataprop type(int) =  
> > > > | {t: int} base (t) of (type\_base(t))  
> > > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > > 
> > > > (\* TODO include protocol argument _)  
> > > > (_ TODO error handling \*)  
> > > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > > > (filedes fd | int fd)
> > > 
> > > This fails with:
> > > 
> > > > the static expression needs to be impredicative but is assigned the  
> > > > sort  
> > > > [S2RTbas(S2RTBASpre(int))]
> > > 
> > > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > > semantics, of course).
> > > 
> > > ~Shea
> > > 
> > > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > > 
> > > > Right now, constraints involving bitwise operations can be  
> > > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > > such constraints.
> > > > 
> > > > Will Blair should have something to say on this issue. He has  
> > > > managed  
> > > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > > readily handle bitwise operations.
> > > > 
> > > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > > 
> > > > > Hi all,
> > > > > 
> > > > > Does ATS support any bitwise operations on ints in the statics?
> > > > > 
> > > > > ~Shea
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).
> 
> > > > > To view this discussion on the web visit
> 
> [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> 
> > > > > .
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit
> 
> [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > \<javascript:\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit
> 
> [https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901180806.GA2216%40nixos.hsd1.nh.comcast.net)
> 
> > > .
> > 
> > –  
> > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB\_tUqXkYXGVA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqSbU0L6b%3DsoCfKrV3yTPrzsxZNjodf6nB_tUqXkYXGVA%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [September 2, 2014, 6:57pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/9 "2014-09-02T18:57:34Z")

</div>

Sounds good! Note that for now I’ve replaced the dataprops with subset  
sorts [1](https://github.com/shlevy/socket-activate/blob/5617383608ac67cdc6e7d9e9f81f45914fb3fa3b/static/fd.sats#L20-L22) to avoid having to pass explicit proofs [2](https://github.com/shlevy/socket-activate/blob/5617383608ac67cdc6e7d9e9f81f45914fb3fa3b/dynamic/socket-activate.dats#L15), but I suppose  
there’s no way to define subset sorts recursively, right? I’d need that  
when adding back in the lor operator.

~SheaOn Tue, Sep 02, 2014 at 11:42:10AM -0700, William Blair wrote:

> Hi Shea,
> 
> That would be great. We can maybe try an example with the socket interface  
> like you gave when it’s ready.
> 
> Thanks,  
> Will
> 
> On Tuesday, September 2, 2014 9:56:20 AM UTC-4, Shea Levy wrote:
> 
> > Hi Will,
> > 
> > This sounds great! Let me know if you need any help testing.
> > 
> > ~Shea
> > 
> > On Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:
> > 
> > > > Hm, how do I spell the operations? I’ve got something like this to  
> > > > represent the arguments to the ‘socket’ function, which on Linux  
> > > > allows  
> > > > the ‘type’ argument to be bitwise-ored with certain modifiers (the  
> > > > ATS\_  
> > > > prefix indicates a macro taken from a C include):
> > > 
> > > Right now using bitwise operators in the statics is a bit experimental  
> > > with an  
> > > external constraint solver. I’m working on getting the solver into the  
> > > main  
> > > ATS contrib repo so others may use it as well.
> > > 
> > > As far as syntax goes, you probably won’t want to use the “int” sort  
> > > since any static int  
> > > term is considered a natural number without bound. Instead, we can use  
> > > a new sort  
> > > called a bit vector that models machine integers. This sort is  
> > > provided by most SMT  
> > > solvers so we can use it in the ATS statics.
> > > 
> > > If I understand your requirement correctly, suppose we have the  
> > > following type at our  
> > > disposal. This is hardly official, but it illustrates how I think you  
> > > could implement the example  
> > > you provided. This currently won’t work in ATS right now.
> > > 
> > > ```
> > > abst@ype int (bv:bv16) = int 
> > > 
> > > ```
> > > 
> > > This associates a static signed 16 bit vector with the normal integer  
> > > type. Of course, the choice of  
> > > what size bit vector to use is machine dependent, but that’s a  
> > > separate issue. We can rewrite your  
> > > example using the new bv16 sort in the statics using the lor operator  
> > > described by Hongwei.
> > > 
> > > dataprop domain(bv16) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > address families \*)
> > > 
> > > dataprop type\_base(bv16) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> > > include other socket types \*)
> > > 
> > > dataprop type\_modifier(bv16) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > 
> > > dataprop type(bv16) =  
> > > | {t: bv16} base (t) of (type\_base(bv16))  
> > > | {t, m: bv16} or ((t lor m)) of (type(t), type\_modifier(m))
> > > 
> > > fn socket {d, t: bv16} (domain d, type t | int d, int t): [fd: int]  
> > > (filedes fd | int fd)
> > > 
> > > I need to finish adding more support for bit vectors in the external  
> > > constraint solver, but I’ll post an announcement when  
> > > it’s ready to use.
> > > 
> > > Thanks,  
> > > Will
> > > 
> > > On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > 
> > > > Hm, how do I spell the operations? I’ve got something like this to  
> > > > represent the arguments to the ‘socket’ function, which on Linux  
> > > > allows  
> > > > the ‘type’ argument to be bitwise-ored with certain modifiers (the  
> > > > ATS\_  
> > > > prefix indicates a macro taken from a C include):
> > > > 
> > > > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > > > address families \*)
> > > > > 
> > > > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> > > > > include other socket types \*)
> > > > > 
> > > > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > > > 
> > > > > dataprop type(int) =  
> > > > > | {t: int} base (t) of (type\_base(t))  
> > > > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > > > 
> > > > > (\* TODO include protocol argument _)  
> > > > > (_ TODO error handling \*)  
> > > > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > > > > (filedes fd | int fd)
> > > > 
> > > > This fails with:
> > > > 
> > > > > the static expression needs to be impredicative but is assigned the  
> > > > > sort [S2RTbas(S2RTBASpre(int))]
> > > > 
> > > > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > > > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > > > semantics, of course).
> > > > 
> > > > ~Shea
> > > > 
> > > > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > > > 
> > > > > Right now, constraints involving bitwise operations can be  
> > > > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > > > such constraints.
> > > > > 
> > > > > Will Blair should have something to say on this issue. He has managed  
> > > > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > > > readily handle bitwise operations.
> > > > > 
> > > > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > > > 
> > > > > > Hi all,
> > > > > > 
> > > > > > Does ATS support any bitwise operations on ints in the statics?
> > > > > > 
> > > > > > ~Shea
> > > > > > 
> > > > > > –  
> > > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > > \<javascript:\>.  
> > > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > > > To view this discussion on the web visit
> > 
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> > 
> > > > > > .
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > > To view this discussion on the web visit  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > \<javascript:\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/8f8b84f6-72e6-49d3-bfdd-f99863e29430%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/8f8b84f6-72e6-49d3-bfdd-f99863e29430%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 12, 2015, 2:21pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/10 "2015-12-12T14:21:42Z")

</div>

I just had the same question and just read this thread.

So for now, it seems better to do it with classical arithmetic operations:  
additions and subtractions, and appropriates tests with lower than, greater  
than, etc, and constants (as #define) for bits sets.

By the way, I also wondered if there is a sort for unsigned integers. I  
mean a sort, not a subset sort.Le lundi 1 septembre 2014 07:18:57 UTC+2, Shea Levy a écrit :

> Hi all,
> 
> Does ATS support any bitwise operations on ints in the statics?
> 
> ~Shea

---

<div class="post-metadata">

**Author:** ![William\_Blair](https://avatars.discourse-cdn.com/v4/letter/w/c68b51/32.png) [@William\_Blair](https://discourse.ats-lang.org/u/William_Blair)\
**Post date:** [September 2, 2014, 1:44pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/11 "2014-09-02T13:44:02Z")

</div>

> Hm, how do I spell the operations? I’ve got something like this to  
> represent the arguments to the ‘socket’ function, which on Linux allows  
> the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> prefix indicates a macro taken from a C include):

Right now using bitwise operators in the statics is a bit experimental with an  
external constraint solver. I’m working on getting the solver into the main  
ATS contrib repo so others may use it as well.

As far as syntax goes, you probably won’t want to use the “int” sort  
since any static int  
term is considered a natural number without bound. Instead, we can use  
a new sort  
called a bit vector that models machine integers. This sort is  
provided by most SMT  
solvers so we can use it in the ATS statics.

If I understand your requirement correctly, suppose we have the  
following type at our  
disposal. This is hardly official, but it illustrates how I think you  
could implement the example  
you provided. This currently won’t work in ATS right now.

```
abst@ype int (bv:bv16) = int

```

This associates a static signed 16 bit vector with the normal integer  
type. Of course, the choice of  
what size bit vector to use is machine dependent, but that’s a  
separate issue. We can rewrite your  
example using the new bv16 sort in the statics using the lor operator  
described by Hongwei.

dataprop domain(bv16) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
address families \*)

dataprop type\_base(bv16) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
include other socket types \*)

dataprop type\_modifier(bv16) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)

dataprop type(bv16) =  
| {t: bv16} base (t) of (type\_base(bv16))  
| {t, m: bv16} or ((t lor m)) of (type(t), type\_modifier(m))

fn socket {d, t: bv16} (domain d, type t | int d, int t): [fd: int]  
(filedes fd | int fd)

I need to finish adding more support for bit vectors in the external  
constraint solver, but I’ll post an announcement when  
it’s ready to use.

Thanks,  
WillOn Mon, Sep 1, 2014 at 2:08 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> Hm, how do I spell the operations? I’ve got something like this to  
> represent the arguments to the ‘socket’ function, which on Linux allows  
> the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
> prefix indicates a macro taken from a C include):
> 
> > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other address families \*)
> > 
> > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include other socket types \*)
> > 
> > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) | SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > 
> > dataprop type(int) =  
> > | {t: int} base (t) of (type\_base(t))  
> > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > 
> > (\* TODO include protocol argument _)  
> > (_ TODO error handling \*)  
> > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int] (filedes fd | int fd)
> 
> This fails with:
> 
> > the static expression needs to be impredicative but is assigned the sort [S2RTbas(S2RTBASpre(int))]
> 
> twice (apparently one for the t and one for the m in ((t | m)). If I  
> replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> semantics, of course).
> 
> ~Shea
> 
> On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> 
> > Right now, constraints involving bitwise operations can be  
> > generated., but the built-in constraint-solver in ATS cannot handle  
> > such constraints.
> > 
> > Will Blair should have something to say on this issue. He has managed  
> > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > readily handle bitwise operations.
> > 
> > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> > 
> > > Hi all,
> > > 
> > > Does ATS support any bitwise operations on ints in the statics?
> > > 
> > > ~Shea
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > To view this discussion on the web visit  
> > > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)  
> > > .
> > 
> > –  
> > 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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![William\_Blair](https://avatars.discourse-cdn.com/v4/letter/w/c68b51/32.png) [@William\_Blair](https://discourse.ats-lang.org/u/William_Blair)\
**Post date:** [September 2, 2014, 6:42pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/12 "2014-09-02T18:42:10Z")

</div>

Hi Shea,

That would be great. We can maybe try an example with the socket interface  
like you gave when it’s ready.

Thanks,  
WillOn Tuesday, September 2, 2014 9:56:20 AM UTC-4, Shea Levy wrote:

> Hi Will,
> 
> This sounds great! Let me know if you need any help testing.
> 
> ~Shea
> 
> On Tue, Sep 02, 2014 at 09:44:02AM -0400, Blair, William wrote:
> 
> > > Hm, how do I spell the operations? I’ve got something like this to  
> > > represent the arguments to the ‘socket’ function, which on Linux  
> > > allows  
> > > the ‘type’ argument to be bitwise-ored with certain modifiers (the  
> > > ATS\_  
> > > prefix indicates a macro taken from a C include):
> > 
> > Right now using bitwise operators in the statics is a bit experimental  
> > with an  
> > external constraint solver. I’m working on getting the solver into the  
> > main  
> > ATS contrib repo so others may use it as well.
> > 
> > As far as syntax goes, you probably won’t want to use the “int” sort  
> > since any static int  
> > term is considered a natural number without bound. Instead, we can use  
> > a new sort  
> > called a bit vector that models machine integers. This sort is  
> > provided by most SMT  
> > solvers so we can use it in the ATS statics.
> > 
> > If I understand your requirement correctly, suppose we have the  
> > following type at our  
> > disposal. This is hardly official, but it illustrates how I think you  
> > could implement the example  
> > you provided. This currently won’t work in ATS right now.
> > 
> > ```
> > abst@ype int (bv:bv16) = int 
> > 
> > ```
> > 
> > This associates a static signed 16 bit vector with the normal integer  
> > type. Of course, the choice of  
> > what size bit vector to use is machine dependent, but that’s a  
> > separate issue. We can rewrite your  
> > example using the new bv16 sort in the statics using the lor operator  
> > described by Hongwei.
> > 
> > dataprop domain(bv16) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > address families \*)
> > 
> > dataprop type\_base(bv16) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> > include other socket types \*)
> > 
> > dataprop type\_modifier(bv16) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > 
> > dataprop type(bv16) =  
> > | {t: bv16} base (t) of (type\_base(bv16))  
> > | {t, m: bv16} or ((t lor m)) of (type(t), type\_modifier(m))
> > 
> > fn socket {d, t: bv16} (domain d, type t | int d, int t): [fd: int]  
> > (filedes fd | int fd)
> > 
> > I need to finish adding more support for bit vectors in the external  
> > constraint solver, but I’ll post an announcement when  
> > it’s ready to use.
> > 
> > Thanks,  
> > Will
> > 
> > On Mon, Sep 1, 2014 at 2:08 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > 
> > > Hm, how do I spell the operations? I’ve got something like this to  
> > > represent the arguments to the ‘socket’ function, which on Linux  
> > > allows  
> > > the ‘type’ argument to be bitwise-ored with certain modifiers (the  
> > > ATS\_  
> > > prefix indicates a macro taken from a C include):
> > > 
> > > > dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other  
> > > > address families \*)
> > > > 
> > > > dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO  
> > > > include other socket types \*)
> > > > 
> > > > dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) |  
> > > > SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> > > > 
> > > > dataprop type(int) =  
> > > > | {t: int} base (t) of (type\_base(t))  
> > > > | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> > > > 
> > > > (\* TODO include protocol argument _)  
> > > > (_ TODO error handling \*)  
> > > > fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int]  
> > > > (filedes fd | int fd)
> > > 
> > > This fails with:
> > > 
> > > > the static expression needs to be impredicative but is assigned the  
> > > > sort [S2RTbas(S2RTBASpre(int))]
> > > 
> > > twice (apparently one for the t and one for the m in ((t | m)). If I  
> > > replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
> > > semantics, of course).
> > > 
> > > ~Shea
> > > 
> > > On Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:
> > > 
> > > > Right now, constraints involving bitwise operations can be  
> > > > generated., but the built-in constraint-solver in ATS cannot handle  
> > > > such constraints.
> > > > 
> > > > Will Blair should have something to say on this issue. He has managed  
> > > > to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> > > > readily handle bitwise operations.
> > > > 
> > > > On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > > 
> > > > > Hi all,
> > > > > 
> > > > > Does ATS support any bitwise operations on ints in the statics?
> > > > > 
> > > > > ~Shea
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > > To view this discussion on the web visit
> 
> [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)
> 
> > > > > .
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%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 [ats-lang...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAEuDxfTb7QXJd4TvwcVAF70gMwZ3Rdsv%3D%3DwVOKDaJqOTs1vJOQ%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [September 1, 2014, 6:08pm UTC](https://discourse.ats-lang.org/t/bitwise-operations/471/13 "2014-09-01T18:08:06Z")

</div>

Hm, how do I spell the operations? I’ve got something like this to  
represent the arguments to the ‘socket’ function, which on Linux allows  
the ‘type’ argument to be bitwise-ored with certain modifiers (the ATS\_  
prefix indicates a macro taken from a C include):

> dataprop domain(int) = AF\_UNIX (ATS\_AF\_UNIX) (\* TODO include other address families \*)
> 
> dataprop type\_base(int) = SOCK\_STREAM (ATS\_SOCK\_STREAM) (\* TODO include other socket types \*)
> 
> dataprop type\_modifier(int) = SOCK\_NONBLOCK (ATS\_SOCK\_NONBLOCK) | SOCK\_CLOEXEC (ATS\_SOCK\_CLOEXEC)
> 
> dataprop type(int) =  
> | {t: int} base (t) of (type\_base(t))  
> | {t, m: int} or ((t | m)) of (type(t), type\_modifier(m))
> 
> (\* TODO include protocol argument _)  
> (_ TODO error handling \*)  
> fn socket {d, t: int} (domain d, type t | int d, int t): [fd: int] (filedes fd | int fd)

This fails with:

> the static expression needs to be impredicative but is assigned the sort [S2RTbas(S2RTBASpre(int))]

twice (apparently one for the t and one for the m in ((t | m)). If I  
replace ‘t | m’ with ‘t \* m’, it compiles fine (though with the wrong  
semantics, of course).

~SheaOn Mon, Sep 01, 2014 at 01:33:32AM -0400, Hongwei Xi wrote:

> Right now, constraints involving bitwise operations can be  
> generated., but the built-in constraint-solver in ATS cannot handle  
> such constraints.
> 
> Will Blair should have something to say on this issue. He has managed  
> to use Microsoft’s Z3 to do constraint-solving for ATS. Z3 can  
> readily handle bitwise operations.
> 
> On Mon, Sep 1, 2014 at 1:18 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> 
> > Hi all,
> > 
> > Does ATS support any bitwise operations on ints in the statics?
> > 
> > ~Shea
> > 
> > –  
> > 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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > To view this discussion on the web visit  
> > [https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140901051852.GE2219%40nixos.hsd1.nh.comcast.net)  
> > .
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit [https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrdCOS8MuVo9zs6d4gQXe3a%2BFB3TKAu5k1s0zA622VcZw%40mail.gmail.com).