Re: Defining constraints -- datasorts and stacst

2018-04-08 Thread Hongwei Xi
There are two styles of theorem-proving in ATS: http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP- bool-vs-prop/index.html To avoid explicit quantifier elimination performed by the following code, prval () = isCA1_praxi{cB_1}() prval () = isCA1_praxi{cB_2}() prval () =

Re: Shared memory IPC in ATS

2018-04-08 Thread Artyom Shalkhakov
Hi Andrew, Great to see some C-style ATS code in the wild. Definitelly following this development! Make C great again. :-) 2018-04-09 11:11 GMT+06:00 Andrew Knapp : > Hi all, > > I've extracted some ipc code from a larger codebase. > >

Functions from datasorts to datasorts

2018-04-08 Thread Andrew Knapp
Is it possible to write (proof) functions from datasorts to datasorts? For example, if we have datasort tlist = | tnil | tcons(t0ype, tlist) it would be nice to write something equivalent to tlist_append : (tlist, tlist) -> tlist tlist_filter: (tlist, (tlist) -> bool) -> tlist that could

Re: Shared memory IPC in ATS

2018-04-08 Thread Andrew Knapp
Nanomq is as bare-bones as you can possibly get. Unlike zeromq, it only works for a small number of local processes, and makes every possible tradeoff for low latency. Nanomq (in the ATS port and original C++) only offers blocking reads in the public interface (I'll probably change this),

Shared memory IPC in ATS

2018-04-08 Thread Andrew Knapp
Hi all, I've extracted some ipc code from a larger codebase. https://github.com/ajknapp/ats-nanomq It's basically a bunch of SPSC ring buffers in shared memory, and is ported from a C++ library https://github.com/rigtorp/nanomq Fair warning: there aren't many scenarios where this design is a

Re: Shared memory IPC in ATS

2018-04-08 Thread gmhwxi
Thanks! I once tried to use zeromq. For instance, the myserver2 example is the following directory is based on zeromq: http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/http-server/ >>Fair warning: there aren't many scenarios where this design is a good idea Could you elaborate? Also, how

Re: Functions from datasorts to datasorts

2018-04-08 Thread gmhwxi
Could you show an example of intended use of tlist_append? On Monday, April 9, 2018 at 1:35:44 AM UTC-4, Andrew Knapp wrote: > > Is it possible to write (proof) functions from datasorts to datasorts? For > example, if we have > > datasort tlist = > | tnil > | tcons(t0ype, tlist) > > it would