githwxi/ats-postiats

ATS2: Unleashing the Potentials of Types and Templates

ats-postiats's Issues

Run CI on Mac OS X.

Assign me.

Allow the build process to be parallelized

This is recommended practice for the Homebrew platform :)

==> make GCFLAG=-D_ATS_NGC all
\
make -j4 -C src/CBOOT \
  CCOMP=gcc GCFLAG=-D_ATS_NGC \
  CFLAGS= LDFLAGS= patsopt
make -C utils/atscc patscc
make -C ccomp/atslib atslib
make[1]: warning: -jN forced in submake: disabling jobserver mode.
gcc -O2 -I. -I./ccomp/runtime  -c -o pats_main_dats.o pats_main_dats.c
gcc -O2 -I. -I./ccomp/runtime  -c -o pats_error_sats.o pats_error_sats.c
gcc -O2 -I. -I./ccomp/runtime  -c -o pats_intinf_sats.o pats_intinf_sats.c
gcc -O2 -I. -I./ccomp/runtime  -c -o pats_counter_sats.o pats_counter_sats.c
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt --output patscc_dats.c --dynamic patscc.dats
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt --output atscc_main_dats.c --dynamic atscc_main.dats
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt --output atscc_print_dats.c --dynamic atscc_print.dats
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt -o output/atslib_prelude_bool_dats.c --dynamic ../../prelude/DATS/bool.dats
make[1]: *** [patscc_dats.c] Error 127
make[1]: *** Waiting for unfinished jobs....
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt -o output/atslib_prelude_char_dats.c --dynamic ../../prelude/DATS/char.dats
make[1]: *** [atscc_main_dats.c] Error 127
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
make[1]: *** [atscc_print_dats.c] Error 127
"/private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0"/bin/patsopt -o output/atslib_prelude_integer_dats.c --dynamic ../../prelude/DATS/integer.dats
make: *** [utl_atscc] Error 2
make: *** Waiting for unfinished jobs....
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
make[1]: *** [output/atslib_prelude_bool_dats.c] Error 127
make[1]: *** Waiting for unfinished jobs....
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
make[1]: *** [output/atslib_prelude_char_dats.c] Error 127
/bin/sh: /private/tmp/ats2-postiats-tGRg/ATS2-Postiats-0.1.0/bin/patsopt: No such file or directory
make[1]: *** [output/atslib_prelude_integer_dats.c] Error 127
make: *** [ccomp/atslib/lib/libatslib.a] Error 2

Run CI with Cygwin.

Assign me.

Arrays of Records Produce Invalid C Code

The following program uses arrays of records. When individual records are changed within the array, the program's corresponding C code contains syntax errors.

For example, compile the following program with patscc

#include "share/atspre_staload.hats"

typedef planet = @{
   x= double,
   y= double,
   z= double
}

implement main0 () = let
  var solar_system = @[planet][8](@{x=0.0, y=0.0,z=0.0})
in
  (* The C compiler encounters a syntax error when reaching these. *)
  solar_system.[0].x := 1.0;
  solar_system.[0].y := 1.0;
  solar_system.[0].z := 1.0;
end

The line of C code that causes the syntax error is given below.

ATSINSstore(ATSSELfltrec(ATSSELfltrec(ATSPMVptrof(tmpref1[0]), postiats_tyrec_0, [ATSPMVi0nt(0)]), postiats_tyrec_0, atslab__x), ATSPMVf0loat(1.0)) ;

Can't compile atslex?

$ pwd
/home/kiwamu/src/ATS-Postiats/utils/atslex
$ make
\
  "/home/kiwamu/src/ATS-Postiats"/bin/patscc -cleanaft -I"/home/kiwamu/src/ATS-Postiats" -I"/home/kiwamu/src/ATS-Postiats"/ccomp/runtime -I"/home/kiwamu/src/ATS-Postiats-contrib"/contrib -IATS "/home/kiwamu/src/ATS-Postiats-contrib"/contrib -D_GNU_SOURCE -o atslex_sats.o -c atslex.sats
\
  "/home/kiwamu/src/ATS-Postiats"/bin/patscc -cleanaft -I"/home/kiwamu/src/ATS-Postiats" -I"/home/kiwamu/src/ATS-Postiats"/ccomp/runtime -I"/home/kiwamu/src/ATS-Postiats-contrib"/contrib -IATS "/home/kiwamu/src/ATS-Postiats-contrib"/contrib -DATS_MEMALLOC_LIBC -D_GNU_SOURCE -o atslex_main_dats.o -c atslex_main.dats
\
  "/home/kiwamu/src/ATS-Postiats"/bin/patscc -cleanaft -I"/home/kiwamu/src/ATS-Postiats" -I"/home/kiwamu/src/ATS-Postiats"/ccomp/runtime -I"/home/kiwamu/src/ATS-Postiats-contrib"/contrib -IATS "/home/kiwamu/src/ATS-Postiats-contrib"/contrib -DATS_MEMALLOC_LIBC -D_GNU_SOURCE -o atslex_charset_dats.o -c atslex_charset.dats
\
  "/home/kiwamu/src/ATS-Postiats"/bin/patscc -I"/home/kiwamu/src/ATS-Postiats" -I"/home/kiwamu/src/ATS-Postiats"/ccomp/runtime -I"/home/kiwamu/src/ATS-Postiats-contrib"/contrib -D_GNU_SOURCE -o atslex atslex_sats.o atslex_main_dats.o atslex_charset_dats.o -L"/home/kiwamu/src/ATS-Postiats"/ccomp/atslib/lib -latslib 
atslex_main_dats.o: In function `_057_home_057_kiwamu_057_src_057_ATS_055_Postiats_057_utils_057_atslex_057_atslex_main_056_dats__dynload':
atslex_main_dats.c:(.text+0x185): undefined reference to `_057_home_057_kiwamu_057_src_057_ATS_055_Postiats_057_utils_057_atslex_057_atslex_056_sats__dynload'
atslex_charset_dats.o: In function `_057_home_057_kiwamu_057_src_057_ATS_055_Postiats_057_utils_057_atslex_057_atslex_056_sats__charset_comp':
atslex_charset_dats.c:(.text+0x53d): undefined reference to `_057_home_057_kiwamu_057_src_057_ATS_055_Postiats_057_utils_057_atslex_057_atslex_056_sats__charset_diff'
collect2: error: ld returned 1 exit status
/home/kiwamu/src/ATS-Postiats/share/atsmake-post.mk:33: recipe for target 'atslex' failed
make: *** [atslex] Error 1

patscc -ccats appears to be undocumented in patscc --help

PMVtmpltcstmat undeclared

When building $PATSHOME/doc/EXAMPLE/fprtuple.dats, I get:

gcc -std=c99 -I"/home/admin/postiats" -I"/home/admin/postiats"/ccomp/runtime -o fprtuple.exe fprtuple_dats.c
fprtuple_dats.c: In function ‘ATSLIB_056$prelude_fprint_val$16$1’:
fprtuple_dats.c:594:1: error: ‘PMVtmpltcstmat’ undeclared (first use in this function)
fprtuple_dats.c:594:1: note: each undeclared identifier is reported only once for each function it appears in
fprtuple_dats.c:594:1: error: ‘tostrptr_val’ undeclared (first use in this function)
fprtuple_dats.c:594:1: warning: implicit declaration of function ‘S2Etyrec’ [-Wimplicit-function-declaration]
fprtuple_dats.c:594:1: error: ‘flt0’ undeclared (first use in this function)
fprtuple_dats.c:594:1: error: expected ‘)’ before ‘;’ token
fprtuple_dats.c:594:1: error: expected expression before ‘)’ token
Makefile:142: recipe for target `fprtuple.exe' failed
make: *** [fprtuple.exe] Error 1

Is it a missing/unimplemented feature?

Can't use free variable on closure?

Can't use free variable on closure?

$ cat test.dats 
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

implement main0 () = {
  val msg = "Hello!"
  val () = (fix f(): void => (println! msg; f()))()
}
$ patscc test.dats
/home/kiwamu/tmp/test.dats: 131(line=6, offs=13) -- 167(line=6, offs=49): error(ccomp): the function is expected to be envless but it is not.
test_dats.c: In function 'mainats_void_0':
test_dats.c:313:1: warning: implicit declaration of function 'ATSERRORnotenvless' [-Wimplicit-function-declaration]
 ATSINSmove_void(tmpret0, ATSfunclo_fun(ATSERRORnotenvless(ATSPMVfunlab(__patsfun_1)), (), atsvoid_t0ype)()) ;
 ^
In file included from test_dats.c:15:0:
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:193:34: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
 ATSfunclo_fun(pmv, targs, tres) ((tres(*)targs)(pmv))
                                  ^
/home/kiwamu/src/ATS-Postiats/ccomp/runtime/pats_ccomp_instrset.h:274:39: note: in definition of macro 'ATSINSmove_void'
 #define ATSINSmove_void(tmp, command) command
                                       ^
test_dats.c:313:26: note: in expansion of macro 'ATSfunclo_fun'
 ATSINSmove_void(tmpret0, ATSfunclo_fun(ATSERRORnotenvless(ATSPMVfunlab(__patsfun_1)), (), atsvoid_t0ype)()) ;
                          ^
/tmp/cchHJAEB.o: In function `mainats_void_0':
test_dats.c:(.text+0xcd): undefined reference to `ATSERRORnotenvless'
collect2: error: ld returned 1 exit status

Do CI more.

Assign me.

exit(ATS): /home/brand_000/ATS-Postiats/src/pats_trans2_staexp.dats: 65342(line=2598, offs=9) -- 65370(line=2598, offs=37): match failure.

Wasn't sure if this was a bug or a basically satisfactory and intentional error message (either way it probably doesn't matter); think my code should have TESTPROP not TESTPROP().

(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)

%{^
  int do_adding() {
  volatile unsigned int i = 1;
  while(i >= 0) {
    i = i + 1;
  }
  return -1;
  }
%}


extern
fun do_adding():int = "mac#"


// Now with proofs:

dataprop TESTPROP() =
  | TEST of ()

extern
fun do_adding_usepf(pf: TESTPROP):int = "mac#"

implement main0() = let

// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()

//prval a
//val x = do_adding1()


in
println!(x)
end

Add inline/inl# function definition

It would be nice to have inline fn foo(): void or fn foo(): void = "inl#" result in an inline C function being emitted. I tried to add this myself but I don't know the codebase well enough.

Using Github's "Release" Feature in favor of Sourceforge.net

Hi, will you consider using the github release feature in favor of sourceforge.net?

1. it is integrated into github, which means everything is in one place
2. release file and log can be put right into the release page
3. commits and issues among versions are automatically included using the version comparing features.

More info here at Github Official Blog

The ats2-postiats 0.1.6 has build waring on Mac OS X.

Homebrew/legacy-homebrew#35630

There's a weird testing error that exists in this version and the one prior:

ld: warning: directory not found for option '-L/usr/local/Cellar/ats2-postiats/0.1.6/lib/ats2-postiats-0.1.6/ccomp/atslib/lib64'

It's correct, that directory does not exist. But why is it expecting it to in the first place? Moving it to libexec seems to resolve the issue, and create that directory, so we may wish to do that.

Case matching on void type can defeat constraint solving

It looks like case matching on void type always succeed regardless of when-guard.

That is in the following example the clause C1 will be selected whether predicate P1 is true or not. This is not the case if I replace () with some other constant, say 1.

case () of
| () when P1 => C1
| () when P2 => C2
...

However the constraints implied by P1 are introduced to the type-checker state as if P1 was actually true. This can easily lead to contradictions between the compile-time constraints and run-time values.
Here is a somewhat silly example exploiting this bug.

I observe this behaviour in the stable version (0.2.6).

GC/seg fault issue with $extval

I was trying to work out a concise way to use a #define'd value in both ATS and C, and found that the following code will produce either 'GC: Warning: the maximal chunk count limit is reached!" which doesn't terminate, or an immediate segmentation fault when run in emacs. This happens when macdef a = $extval(@[int?][N], "a") is uncommented.

(* ****** ****** *)

#include
"share/atspre_staload.hats"


(* ****** ****** *)

staload UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)


implement
main0 () =
{
//

%{^
#define N 100
int a[N];
int varTest = 8888;
%}

//#define N $extval(size_t, "N")
macdef N = $extval(size_t, "N")
#define N N
// the following line is problematic:
macdef a = $extval(@[int?][N], "a")
}

matrixptr problem?

I don't see why this would be the case, after inspecting matrixptr.dats and unsafe.sats, they look right to me. I suppose it is possible my build is corrupted, but, I did a:

cd src
make cleanall

before rebuilding.

I get the following when building anything involving matrixptr.dats (and somehow I think even building atscc failed):

the_effenv_check_sexp: s2e0 = S2Evar(fe$1361(5303))
/media/RAID5/share/ATS_learning/ATS-Postiats/prelude/DATS/matrixptr.dats: 3459(line=133, offs=7) -- 3472(line=135, offs=2): error(3): proof arity mismatch:
The actual proof arity is: -1
The needed proof arity is: 2
/media/RAID5/share/ATS_learning/ATS-Postiats/prelude/DATS/matrixptr.dats: 3459(line=133, offs=7) -- 3472(line=135, offs=2): error(3): [/media/RAID5/share/ATS_learning/ATS-Postiats/src/pats_trans3_p2at.dats]: labp2atlst_trdn: there is no component of the label [2]
TRANS3: there are [2] errors in total.
exit(ATS): uncaught exception: _2media_2RAID5_2share_2ATS_learning_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorException(1025)
exec(patsopt -IATS /media/RAID5/share/ATS_learning/ATS-Postiats/contrib --output test_gemm_dats.c --dynamic test_gemm.dats) = 256

Support BSD make.

BSD user's GNU make command name is "gmake". But ATS's Makefile use "make" name directly.

$ grep make Makefile
MAKE=make -j4
src_patsopt: ; make -j4 -C src patsopt
utl_atscc: ; make -C utils/atscc patscc
ccomp/atslib/lib/libatslib.a: ; make -C ccomp/atslib atslib
clean:: ; make -C src/CBOOT -f Makefile clean
cleanall:: ; make -C src -f Makefile cleanall
cleanall:: ; make -C src/CBOOT -f Makefile cleanall
cleanall:: ; make -C utils/atscc -f Makefile cleanall

Could you use "$(MAKE)" instead of "make"? The "$(MAKE)" automatically chooses BSD make or GNU make.

Is it correct that patsopt creates .c file while the .dats file occurs type error?

Assign me.

The ats2-mode eats 100% CPU resource

Emacs eats 100% CPU resource, while open dats file.

top - 16:12:15 up 7 days,  2:33, 10 users,  load average: 0.51, 0.69, 0.66
Tasks: 242 total,   2 running, 240 sleeping,   0 stopped,   0 zombie
%Cpu(s): 27.3 us,  1.8 sy,  0.0 ni, 70.6 id,  0.3 wa,  0.0 hi,  0.0 si,  0.0 st
KiB Mem:   7989500 total,  7459736 used,   529764 free,   345220 buffers
KiB Swap:  8235004 total,    15040 used,  8219964 free.  3682208 cached Mem

  PID USER      PR  NI    VIRT    RES    SHR S  %CPU %MEM     TIME+ COMMAND                
16222 kiwamu    20   0  455764  39152  19304 R  99.7  0.5   0:15.90 emacs                  
 8484 kiwamu    20   0 2296160 996660  48636 S   4.0 12.5 109:59.82 iceweasel              

local-in-end and recursive function with template

The following code doesn't compile due to "syntax error". However I think it should not be treated as syntax error. Would you please take a look?

local 

fun {a:t@ype} even (int): bool = true
and {b:t@ype} odd (int): bool = false

in 
end

line 4: error(parsing): the keyword [in] is needed 
line 4: error(parsing): the token is discarded.

Trouble Doing Multiple Pattern Matching

In the following program, I cannot unwrap a "pair" type while doing pattern matching on a list of pairs.

#include "share/atspre_staload.hats"

typedef pair = @(string, int)
typedef pairlst = List pair

fun print_pairs (ps: pairlst): void =
  case+ ps of 
    | list_nil () => ()
    | list_cons ((lab, cnt), pss) => let
      (* lab and cnt have garbage values *)
      val () = println! (lab, ":", cnt)
    in
      print_pairs (pss)
    end

implement main0 () = let
  val p1 = @("a", 0)
  val p2 = @("b", 1)
  val p3 = @("c", 2)
  val ps = cons{pair} (p1, cons{pair}(p2, cons{pair}( p3, nil{pair}())))
in
  print_pairs (ps)
end

By changing the pattern match for ps from list_cons((lab, cnt), pss) to list_cons(p, pss) and then pattern matching on p, the problem does not occur.

Segmentation fault in non-template functions

Suppose you want to compute the length of a list that contains element of some flat type. Since the length of the list doesn't depend on the type of elements stored inside of it, you could write this as a non-templated function, like in the following sample code.

https://gist.github.com/wdblair/90444f1850b196409927

This file compiles fine with patscc, but when you run it, a segmentation fault occurs inside the length function.

https://gist.github.com/wdblair/2e0b7d1d56fcc395930d
See line 65 of the outputted C code.

I suspect the issue is that the length function cannot be implemented for all types because the list(a) datatype is compiled into a struct like the following

struct {
     atstype_var data;
     void *next;
} list_a;

Where atstype_var is a array of bytes of fixed size.

typedef
struct{char _[_ATSTYPE_VAR_SIZE];} atstype_var[0] ;

This breaks down when the list type gets instantiated on some type like int and is represented by the following C struct.

struct {
    int data;
    void *next;
} list_int;

Now, if I pass a pointer to list_int to the length function, I am certainly going to get a segmentation fault because it expects the *next pointer to be at a different offset in the struct. That is, the size of atstype_var and any other flat type are likely not going to be the same.

Of course, this behavior highlights one of the reasons I really like ATS; it's very flexible. The list datatype does not need to be a complicated boxed type like in other languages, it can literally just be a struct that holds data and a pointer to the next struct in the list.

My question is, "how could we have this create an error for the user, instead of causing a segmentation fault in the code?"

Modulo of negative numbers

The given implementation of modulo does not correspond with the generally accepted version when the input is a negative number. In ATS, it will currently return a negative number instead of the remainder. Example: -1 mod 26 will yield -1, not 25.

Type-influencer can't know the type of conditional branch?

Following code occurs compile error.

#include "share/atspre_staload.hats"

fun f (x:int): int = 10 + x * (if x < 30 then 10 else 100)

implement main0 () = println! (f 20)

$ patscc no_duplicate_code.dats
/home/kiwamu/doc/ATS_Foundations/source/code/conditional/no_duplicate_code.dats: 97(line=4, offs=27) -- 128(line=4, offs=58): error(3): the symbol [*] cannot be resolved due to too many matches:
D2ITMcst(mul_int_double) of 0
D2ITMcst(mul_int_float) of 0
/home/kiwamu/doc/ATS_Foundations/source/code/conditional/no_duplicate_code.dats: 97(line=4, offs=27) -- 128(line=4, offs=58): error(3): the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(g1uint_int_t0ype); S2Ecst(size_kind), S2EVar(4143))].
/home/kiwamu/doc/ATS_Foundations/source/code/conditional/no_duplicate_code.dats: 97(line=4, offs=27) -- 128(line=4, offs=58): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eerr()
The needed term is: S2Eapp(S2Ecst(g1uint_int_t0ype); S2Ecst(size_kind), S2EVar(4143))
/home/kiwamu/doc/ATS_Foundations/source/code/conditional/no_duplicate_code.dats: 92(line=4, offs=22) -- 128(line=4, offs=58): error(3): the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind))].
/home/kiwamu/doc/ATS_Foundations/source/code/conditional/no_duplicate_code.dats: 92(line=4, offs=22) -- 128(line=4, offs=58): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(g1uint_int_t0ype); S2Ecst(size_kind), S2Eapp(S2Ecst(add_int_int); S2EVar(4142->S2Eintinf(10)), S2EVar(4143)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind))
patsopt(TRANS3): there are [3] errors in total.
exit(ATS): uncaught exception: _2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Type-influencer can't know the type of conditional branch?

GPL license for libraries

ATS looks very interesting.
However, using the GPL license for the standard library restricts its usage to writing GPLv3 programs.

• Do you confirm this?
• Would a change to a more permissive license (for libraries only) be considered?

Can't build doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/brauntest.dats

$ pwd
/home/kiwamu/src/ATS-Postiats/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL
$ patsopt --version
Hello from ATS2(ATS/Postiats)!
ATS/Postiats version 0.0.8 with Copyright (c) 2011-2014 Hongwei Xi
$ make cleanall
$ make brauntest
--snip--
The 1st translation (fixity) of [brauntest.dats] is successfully completed!
The 2nd translation (binding) of [brauntest.dats] is successfully completed!
/home/kiwamu/src/ATS-Postiats.masterq/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/brauntest.dats: 3993(line=180, offs=27) -- 3995(line=180, offs=29): error(3): [/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn: the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(list_vt0ype_int_vtype); S2Eapp(S2Ecst(INV); S2EVar(4087)), S2EVar(4088))].
/home/kiwamu/src/ATS-Postiats.masterq/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/brauntest.dats: 3993(line=180, offs=27) -- 3995(line=180, offs=29): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(list_t0ype_int_type); S2Ecst(T), S2EVar(4086->S2Eintinf(57)))
The needed term is: S2Eapp(S2Ecst(list_vt0ype_int_vtype); S2Eapp(S2Ecst(INV); S2EVar(4087)), S2EVar(4088))
/home/kiwamu/src/ATS-Postiats.masterq/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/brauntest.dats: 4142(line=186, offs=27) -- 4144(line=186, offs=29): error(3): [/home/hwxi/research/Postiats/git/src/pats_trans3_util.dats]: d3exp_trdn: the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(list_vt0ype_int_vtype); S2Eapp(S2Ecst(INV); S2EVar(4093)), S2EVar(4094))].
/home/kiwamu/src/ATS-Postiats.masterq/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/brauntest.dats: 4142(line=186, offs=27) -- 4144(line=186, offs=29): error(3): mismatch of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(list_t0ype_int_type); S2Ecst(T), S2EVar(4092->S2Eintinf(1000)))
The needed term is: S2Eapp(S2Ecst(list_vt0ype_int_vtype); S2Eapp(S2Ecst(INV); S2EVar(4093)), S2EVar(4094))
TRANS3: there are [2] errors in total.
exit(ATS): uncaught exception: _2home_2hwxi_2research_2Postiats_2git_2src_2pats_error_2esats__FatalErrorException(1025)
brauntest_dats.c : ERROR!!!
\
  "/usr/local/lib/ats2-postiats-0.0.8"/bin/patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I/usr/local/lib/ats2-postiats-0.0.8 -I/usr/local/lib/ats2-postiats-0.0.8/ccomp/runtime -O2 -o brauntest brauntest_dats.c || echo brauntest ": ERROR!!!"
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I/usr/local/lib/ats2-postiats-0.0.8 -I/usr/local/lib/ats2-postiats-0.0.8/ccomp/runtime -O2 -o brauntest brauntest_dats.c)
/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crt1.o: In function `_start':
/build/eglibc-GQ9ljS/eglibc-2.18/csu/../sysdeps/x86_64/start.S:118: undefined reference to `main'
collect2: error: ld returned 1 exit status
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I/usr/local/lib/ats2-postiats-0.0.8 -I/usr/local/lib/ats2-postiats-0.0.8/ccomp/runtime -O2 -o brauntest brauntest_dats.c) = 256
brauntest : ERROR!!!

Negating predicates on reals

The constraint solver doesn't seem to be aware of relations between constraints on reals.
E.g. it doesn't know that (a == b) is equivalent to ~(a != b). This is not the case with integer constraints, of course.
I observe this behaviour on the today's git version of Potsiats.

Consider the following signature:

extern
fun iszero_real
{a: real}
(a: real(a)):
bool(a != i2r(0))

The following implementation fails to compile due to unsolved constraint:

implement iszero_real{a}(a) =
  if eq_real_int(a, 0)
  then 
    false
  else
    true

But this one is fine:

implement iszero_real{a}(a) =
  if ~neq_real_int(a, 0)
  then 
    false
  else
    true

ATS2 Compiler Encounters Segmentation Fault After 2nd Phase

In my project I have the following in a file called mission.sats

abstype sensors = ptr
abstype actuators = ptr

absvt@ype mission (l:addr) = ptr
abst@ype mission_rec = @{
  samples= ptr,
  satisfied= ptr
}

vtypedef Mission = [l:agz] mission (l)
typedef event = (sensors, actuators) -> Mission

fun make_mission (stream(bool), event): Mission

And the following inside mission.dats

staload "./mission.sats"

extern
praxi b0ytes2type {a:t@ype} {l:addr} (
  pfat: b0ytes(sizeof(a)) @ l
): a? @ l

assume mission_rec = @{
  samples= stream (bool),
  satisfied= event
}

assume mission (l:addr) = @{
  pf= mission_rec @ l,
  free= mfree_gc_v (l),
  p= ptr l
}

implement make_mission (samples, action) = let
  val (pf, fpf | p) = malloc_gc (sizeof<mission_rec>)
  prval pf = b0ytes2type {mission_rec} (pf)
  val () = p->samples := samples
  val () = p->satisfied := action
  val mission = @{
    pf= pf,
    free= fpf,
    p= p
  }
in
  mission
end

When I try to type-check the mission.dats file I get a segmentation fault after the second phase of compiling. Am I using abstract types incorrectly here?

Github missing Makefile

This github repository appears to be missing Makefile at the top level, causing the instructions in INSTALL to fail. It is present in the sourceforge, where it is a link to Makefile_dist. This file is also not present in the top level of the github version.

[Question] What is a good coding style on ATS2 language?

A. ATS1 style: https://github.com/githwxi/ATS-Postiats/blob/master/src/pats_lexing.dats
B. ATS2 prelude style: https://github.com/githwxi/ATS-Postiats/blob/master/prelude/DATS/CODEGEN/arrayptr.atxt
C. My style: https://github.com/fpiot/chopstx-ats/blob/fsm55-ats/example-fsm-55-ats/DATS/hacker-emblem.dats

A has some good indents, however B has less. Both have many "//" comments. C has more indents and no "//" comments.

Indent is a bad thing on ATS2 culture?

String is not boxed type?

Following document said "String is boxed type".

ATS-Postiats/doc/BOOK/INT2PROGINATS/CHAP_POLYMORPH/main.atxt

Line 188 in 1778f3d

#atscode('\

However, following sample code has an error.

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

fun swap_boxed{a,b:type} (xy: (a, b)): (b, a) = (xy.1, xy.0)

implement main0 () = {
  val AB = ( "A", "B" )
  val BA1 = swap_boxed{string,string} (AB)
}

String is not boxed type?

Trouble compiling some c-code inclusion examples ("mac#")

Here is an example:

(* ****** ****** *)
//

include

"share/atspre_define.hats"

include

"share/atspre_staload.hats"
//
(* ****** ****** *)

%{^
int do_adding() {
unsigned int i = 1;
while(i < 1) {
i = i + 1;
}
return -1;
}
%}

extern
fun do_adding():int = "mac#%"

(* extern )
( fun do_adding():int *)

(* implement )
( do_adding() = "mac#%" *)

implement main0() = let

val x = do_adding() and y = do_adding()

in
println!(x)
end

All versions should be tagged, not just the pre-release

Currently the repo has a single available tag, 0.2.11.

As a feature request, please tag all releases with their version number, and pre-releases as, e.g. 0.2.11pre

This allows much easier comparisons between releases, e.g. for locating regressions.

Type Checker Misses Misuse of Linear Types

When I type check the following file using ATS1, it warns me that "solve" must be preserved but is consumed instead on line 18. With ATS2, no error is reported, but only if I assume that solver is a record.

https://gist.github.com/wdblair/5427541

Is their any plans for making a Vim mode?

Compile issue with ATS Github (cygwin 64 build)

I'm guessing this is possibly an issue with my ATS being "too new", but just in case ...:

/home/brand_000/ats-lang-anairiats-0.2.11/bin/atsopt -DATS C3NSTRINTKND=gmpknd --output pats_symenv_sats.c --static pats_symenv.sats
/home/brand_000/ATS-Postiats/src/pats_symenv.sats: 1590(line=48, offs=1) -- 1595(line=48, offs=6): error(2): the static identifier [absvt] is unrecognized.
exit(ATS): uncaught exception: ATS_2d0_2e2_2e11_2src_2ats_error_2esats__FatalErrorException(1027)
Makefile:799: recipe for target 'pats_symenv_sats.c' failed
make[1]: *** [pats_symenv_sats.c] Error 1

Improve compatibility for OS X

For OS X, there are lack of compatibility.

• Homebrew's gtk+3 pkg-config dose not work correctly with default setting.

  • It needs to install XQuartz and add /opt/X11/lib/pkgconfig into PKG_CONFIG_PATH

• OS X dose not have pthread_spinlock_t type.

  • OS X has OSSpinlock.

• Also CLOCK_REALTIME is missing in OS X.

  • OS X does not have clock_gettime, use clock_get_time instead.

• It seems to be used clang instead of gcc in test under OS X Travis CI worker environment.

  • In test, it also needs specify CC=${GCC}?

  Because, following output is clang style:

mandelbrot_v2df_dats.c:224:10: error: use of unknown builtin '__builtin_ia32_cmplepd' [-Wimplicit-function-declaration]
lte2 = __builtin_ia32_cmplepd(x, y) ;
       ^
mandelbrot_v2df_dats.c:224:8: error: assigning to 'v2df' from incompatible type 'int'
lte2 = __builtin_ia32_cmplepd(x, y) ;
     ^ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

2 errors generated.

Using andalso leads to "pattern match is non-exhaustive" error

Suppose I have the following program where I want to perform some action when a condition is true and a list is empty.

extern
fun
check (): bool

fun{a:t@ype}
foo (xs: List0_vt(a)): void =
  if check() andalso length(xs) = 0 then let
    val ~list_vt_nil() = xs
  in
    ()
  end
  else
    list_vt_free(xs)

Inside the if statement, I assume the list is empty, since it has a length of 0. This creates a type checking error. If I omit the "andalso" and just have the if statement check for an empty list, type checking passes.

Of course, I could just call list_vt_free instead of doing pattern matching, but I was curious pattern matching could be supported in this case.

Template Instantiation Error When staloading .sats Files.

In the following program, the template for "ref" is not fully instantiated in the C output if the staload declaration is made for reference.sats

staload _ = "prelude/DATS/integer.dats"
staload _ = "prelude/DATS/pointer.dats"
staload _ = "prelude/DATS/reference.dats"

(* 
    Template instantiation works fine when the following 
    declaration is removed.
*)
staload "prelude/SATS/reference.sats"

val i = ref<int> (0)

implement main0() = ()

Compile with
patscc -DATS_MEMALLOC_LIBC test.dats

Emacs mode, sats and hats

A major advantage of ATS is being able to catch errors very quickly due to automated or regular typechecking in one's editor.

I realize this is not the repo for ATS emacs mode, but, there are issues that may need to be addressed here first, such as the ambiguity of the .hats extension and automatic recognition of extension by patsopt.

Currently, emacs mode uses patsopt -tc -d filename, for .sats or .dats.

One solution, which seems favorable, would be for patsopt to automatically typecheck according to the extension (perhaps by using a flag like patsopt - tc -auto filename. This seems great except for .hats, which can be either. So, in addition to this functionality, it might be desirable to update the convention of renaming, where appropriate, .hats to either _h.dats or _h.sats. I advocate not having too many file extensions, as certain 3rd party applications (like github's source code recognizer) may become more problematic to support with an increasing number of extensions.

Could you release ats2-mode.el at next version?

Could you release ats2-mode.el at next version?

This git repo has ats2 mode for Emacs. However, I think the release tar ball doesn't.

$ find ATS-Postiats -name "*.el"
ATS-Postiats/utils/emacs/ats2-mode.el
ATS-Postiats/utils/emacs/ats2-flymake.el

I would like to create Debian package "ats2-mode".

polymorphic and function template confusion

It seems like the issue described here should be caught before runtime, probably before invocation of a c-compiler:

https://groups.google.com/forum/#!topic/ats-lang-users/oQBjTwgOvoY

Overloaded Symbol + Cannot be Resolved

The following program fails to compile, as the addition operator cannot be resolved between

D2ITMcst(add_ptr1_bsz) of 20
D2ITMcst(add_ptr1_bsz) of 20

The code needed to produce this error is given below

#include "share/atspre_staload.hats"

fun {a:t@ype}
loop {n:nat} {l:addr} (
  pf: !(@[a][n]) @ l | p: ptr l, n: int n
): void =
  if n = 0 then 
    ()
  else let
    prval (pfh, pftail) = array_v_uncons {a} (pf)
    val () = print_val<a> (!p)
    val () = print_newline ()
  in
    (* ATS can't resolve the overloaded + symbol *)
    loop (pftail | p + sizeof<a>, pred (n));
    pf := array_v_cons {a} (pfh, pftail);
  end

Problem Accessing Arrays Within Records

Accessing an array stored within a record produces a C compiler error. This error can be reproduced by compiling the following program

#include "share/atspre_staload.hats"

%{^                                                                                                                                                                                                            
typedef struct {                                                                                                                                                                                               
  double dx[3];                                                                                                                                                                                                
} point_t;                                                                                                                                                                                                     
%}

typedef point = $extype_struct "point_t" of {                                                                                                                                                                  
  dx= @[double][3]                                                                                                                                                                                             
}

extern praxi initialized_lemma {a:t@ype} (_: &(a?) >> a): void

local
  var points = @[point][1000]()

  // Static variables are initialized                                                                                                                                                                          
  prval () = initialized_lemma (points)
in
  val the_points = ref_make_viewptr (view@ points | addr@ points)
end

implement main0 () = {
  val (vbox (pf) | p) = ref_get_viewptr {@[point][1000]} (the_points)
  val () = $effmask_all (
    println!(!p.[0].dx.[0])
  )
}

a couple of issues with building from git master

I've verified the problem exists on both Linux and Cygwin.

After a fresh install of ats-lang-anairiats-0.2.11 and building Postiats from the github repo using the command

make -f Makefile_devl all

results in:

gcc -I/home1/03135/bebarker/ats-lang-anairiats-0.2.11/ -I/home1/03135/bebarker/ats-lang-anairiats-0.2.11/ccomp/runtime/ -L/home1/03135/bebarker/ats-lang-anairiats-0.2.11/ccomp/lib64/ /home1/03135/bebarker/ats-lang-anairiats-0.2.11/ccomp/runtime/ats_prelude.c -g -O2 -D_ATS_GCATS -o patsopt pats_main_dats.o pats_error_sats.o pats_error_dats.o pats_intinf_sats.o pats_intinf_dats.o pats_counter_sats.o pats_counter_dats.o pats_utils_sats.o pats_utils_dats.o pats_global_sats.o pats_global_dats.o pats_basics_sats.o pats_basics_dats.o pats_comarg_sats.o pats_comarg_dats.o pats_stamp_sats.o pats_stamp_dats.o pats_symbol_sats.o pats_symbol_dats.o pats_filename_sats.o pats_filename_dats.o pats_filename_reloc_dats.o pats_location_sats.o pats_location_dats.o pats_jsonize_sats.o pats_jsonize_dats.o pats_errmsg_sats.o pats_errmsg_dats.o pats_reader_sats.o pats_reader_dats.o pats_lexbuf_sats.o pats_lexbuf_dats.o pats_lexing_sats.o pats_lexing_dats.o pats_lexing_print_dats.o pats_lexing_error_dats.o pats_lexing_token_dats.o pats_label_sats.o pats_label_dats.o pats_effect_sats.o pats_effect_dats.o pats_fixity_sats.o pats_fixity_prec_dats.o pats_fixity_fxty_dats.o pats_syntax_sats.o pats_syntax_dats.o pats_syntax_print_dats.o pats_depgen_sats.o pats_depgen_dats.o pats_taggen_sats.o pats_taggen_dats.o pats_tokbuf_sats.o pats_tokbuf_dats.o pats_parsing_sats.o pats_parsing_dats.o pats_parsing_error_dats.o pats_parsing_util_dats.o pats_parsing_kwds_dats.o pats_parsing_base_dats.o pats_parsing_e0xp_dats.o pats_parsing_sort_dats.o pats_parsing_staexp_dats.o pats_parsing_p0at_dats.o pats_parsing_dynexp_dats.o pats_parsing_decl_dats.o pats_parsing_toplevel_dats.o pats_symmap_sats.o pats_symmap_dats.o pats_symenv_sats.o pats_symenv_dats.o pats_staexp1_sats.o pats_staexp1_dats.o pats_staexp1_print_dats.o pats_dynexp1_sats.o pats_dynexp1_dats.o pats_dynexp1_print_dats.o pats_trans1_sats.o pats_trans1_env_sats.o pats_trans1_env_dats.o pats_e1xpval_sats.o pats_e1xpval_dats.o pats_e1xpval_error_dats.o pats_trans1_error_dats.o pats_trans1_e0xp_dats.o pats_trans1_effect_dats.o pats_trans1_sort_dats.o pats_trans1_staexp_dats.o pats_trans1_p0at_dats.o pats_trans1_syndef_dats.o pats_trans1_dynexp_dats.o pats_trans1_decl_dats.o pats_staexp2_sats.o pats_staexp2_dats.o pats_stacst2_sats.o pats_stacst2_dats.o pats_staexp2_print_dats.o pats_staexp2_pprint_dats.o pats_staexp2_jsonize_dats.o pats_staexp2_sort_dats.o pats_staexp2_scst_dats.o pats_staexp2_svar_dats.o pats_staexp2_svvar_dats.o pats_staexp2_hole_dats.o pats_staexp2_ctxt_dats.o pats_staexp2_dcon_dats.o pats_staexp2_skexp_dats.o pats_staexp2_szexp_dats.o pats_staexp2_util_sats.o pats_staexp2_util1_dats.o pats_staexp2_util2_dats.o pats_staexp2_util3_dats.o pats_staexp2_error_sats.o pats_staexp2_error_dats.o pats_staexp2_solve_sats.o pats_staexp2_solve_dats.o pats_patcst2_sats.o pats_patcst2_dats.o pats_dynexp2_sats.o pats_dynexp2_dats.o pats_dyncst2_sats.o pats_dyncst2_dats.o pats_dynexp2_print_dats.o pats_dynexp2_jsonize_dats.o pats_dynexp2_dcst_dats.o pats_dynexp2_dvar_dats.o pats_dynexp2_dmac_dats.o pats_dynexp2_util_dats.o pats_trans2_sats.o pats_namespace_sats.o pats_namespace_dats.o pats_trans2_env_sats.o pats_trans2_env_dats.o pats_trans2_error_dats.o pats_trans2_sort_dats.o pats_trans2_staexp_dats.o pats_trans2_p1at_dats.o pats_trans2_dynexp_dats.o pats_trans2_impdec_dats.o pats_trans2_decl_dats.o pats_dynexp3_sats.o pats_dynexp3_dats.o pats_dynexp3_print_dats.o pats_trans3_sats.o pats_trans3_error_dats.o pats_trans3_util_dats.o pats_trans3_env_sats.o pats_trans3_env_dats.o pats_trans3_env_print_dats.o pats_trans3_env_scst_dats.o pats_trans3_env_svar_dats.o pats_trans3_env_termet_dats.o pats_trans3_env_effect_dats.o pats_trans3_env_dvar_dats.o pats_trans3_env_lamlp_dats.o pats_trans3_env_pfman_dats.o pats_trans3_env_lstate_dats.o pats_dmacro2_sats.o pats_dmacro2_dats.o pats_dmacro2_print_dats.o pats_dmacro2_eval0_dats.o pats_dmacro2_eval1_dats.o pats_trans3_p2at_dats.o pats_trans3_patcon_dats.o pats_trans3_syncst_dats.o pats_trans3_dynexp_up_dats.o pats_trans3_dynexp_dn_dats.o pats_trans3_appsym_dats.o pats_trans3_caseof_dats.o pats_trans3_selab_dats.o pats_trans3_ptrof_dats.o pats_trans3_viewat_dats.o pats_trans3_deref_dats.o pats_trans3_assgn_dats.o pats_trans3_xchng_dats.o pats_trans3_lvalres_dats.o pats_trans3_fldfrat_dats.o pats_trans3_looping_dats.o pats_trans3_decl_dats.o pats_lintprgm_sats.o pats_lintprgm_dats.o pats_lintprgm_print_dats.o pats_lintprgm_myint_dats.o pats_lintprgm_solve_dats.o pats_constraint3_sats.o pats_constraint3_dats.o pats_constraint3_init_dats.o pats_constraint3_print_dats.o pats_constraint3_jsonize_dats.o pats_constraint3_simplify_dats.o pats_constraint3_icnstr_dats.o pats_constraint3_solve_dats.o pats_histaexp_sats.o pats_histaexp_dats.o pats_histaexp_print_dats.o pats_histaexp_funlab_dats.o pats_hidynexp_sats.o pats_hidynexp_dats.o pats_hidynexp_print_dats.o pats_hidynexp_util_dats.o pats_typerase_sats.o pats_typerase_error_dats.o pats_typerase_staexp_dats.o pats_typerase_dynexp_dats.o pats_typerase_decl_dats.o pats_ccomp_sats.o pats_ccomp_dats.o pats_ccomp_print_dats.o pats_ccomp_hitype_dats.o pats_ccomp_tmplab_dats.o pats_ccomp_tmpvar_dats.o pats_ccomp_d2env_dats.o pats_ccomp_funlab_dats.o pats_ccomp_funent_dats.o pats_ccomp_util_dats.o pats_ccomp_ccompenv_dats.o pats_ccomp_instrseq_dats.o pats_ccomp_hipat_dats.o pats_ccomp_dynexp_dats.o pats_ccomp_caseof_dats.o pats_ccomp_claulst_dats.o pats_ccomp_lazyeval_dats.o pats_ccomp_trywith_dats.o pats_ccomp_looping_dats.o pats_ccomp_decl_dats.o pats_ccomp_subst_dats.o pats_ccomp_environ_dats.o pats_ccomp_template_dats.o pats_ccomp_emit_dats.o pats_ccomp_emit2_dats.o pats_ccomp_emit3_dats.o pats_ccomp_main_dats.o -lats -lgmp /home1/03135/bebarker/ats-lang-anairiats-0.2.11/ccomp/runtime/GCATS/gc.o
make[1]: Leaving directory `/home1/03135/bebarker/ATS-Postiats/src'
cp -f src/patsopt bin/patsopt
make -C utils/atscc -f Makefile all
make[1]: Entering directory `/home1/03135/bebarker/ATS-Postiats/utils/atscc'
"/home1/03135/bebarker/ATS-Postiats"/bin/patsopt --output patscc_dats.c --dynamic patscc.dats
fopen: No such file or directory
exit(ATS): [fopen("/home1/03135/bebarker/ATS-Postiats/prelude/SATS/arith_prf.sats", "r")] failed
make[1]: *** [patscc_dats.c] Error 1
make[1]: Leaving directory `/home1/03135/bebarker/ATS-Postiats/utils/atscc'
make: *** [src_patscc] Error 2

This issue can be avoided by starting afresh with Postiats and breaking up the build command as follows:

make -f codegen/Makefile_atslib # this is only needed for the first time
make -f Makefile_devl

However, at this point, we will get an issue with certain .c files for patscc not being generated (exactly which .c files among the three seems to be somewhat random; see here for more info). This can be fixed by doing the following:

cd utils/atscc/
rm *.c
make
cd ../..
make -f Makefile_devl

The build should now complete (at least on Linux; there appear to be other problems on Cygwin, at least for my installation of it).

Unbox array @[T][N] doesn't construct memory. It causes SEGV.

$ patscc main.dats
exec(patsopt --output main_dats.c --dynamic main.dats)
exec(patsopt --output main_dats.c --dynamic main.dats) = 0
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  main_dats.c)
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64  main_dats.c) = 0
casper$ ./a.out
9191/9191
1/9191
zsh: segmentation fault  ./a.out

// main.dats
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

vtypedef mystruct = @{
  m0 = int
, m1 = @[int][128]
}

implement main0 () = {
  var stA: mystruct
  var stB: mystruct
  val () = stA.m0 := 9191
  val () = stB.m0 := 9191
  val () = println! (stA.m0, "/", stB.m0)
  val () = stA.m1.[0] := 0
  val () = stA.m1.[1] := 0
  val () = stA.m1.[2] := 0
  val () = stA.m1.[3] := 0
  val () = stA.m1.[4] := 0
  val () = stB.m1.[0] := 1
  val () = stB.m1.[1] := 1
  val () = stB.m1.[2] := 1
  val () = stB.m1.[3] := 1
  val () = stB.m1.[4] := 1
  val () = println! (stA.m0, "/", stB.m0)
}

Pattern match failure in pats_typerase_dynexp.dats

With the following code:

fn foo (): void = let
  val buf_sz = i2sz(10)
  var buf = @[byte][buf_sz]()
in () end

I get:

exit(ATS): /home/shlevy/src/ATS-Postiats/src/pats_typerase_dynexp.dats: 18567(line=820, offs=9) -- 18619(line=820, offs=61): match failure.

If I replace the second buf_sz with a literal 10 it all works.

0.0.8, latest osx :: "bus error: 10" during make

I'm probably doing something wrong...

Error

make -C utils/atscc patscc
"/private/tmp/ats-pP0a/ATS2-Postiats-0.0.8"/bin/patsopt --output patscc_dats.c --dynamic patscc.dats
Hello from ATS2(ATS/Postiats)!
make[1]: *** [patscc_dats.c] Bus error: 10
make[1]: *** Deleting file `patscc_dats.c'
make: *** [utl_atscc] Error 2

More ...

Installation command

0 ~ ❯❯❯ brew install ats -v

Ad-hoc Homebrew formula (could be incorrect)

# /usr/local/Library/Formula/ats.rb
require "formula"

class Ats < Formula
  homepage "http://www.ats-lang.org"
  url "http://sourceforge.net/projects/ats2-lang/files/ats2-lang/ats2-postiats-0.0.8/ATS2-Postiats-0.0.8.tgz"
  sha1 "016c306c73ffd110c5dba59ca93b32eb9cbfa898"

  depends_on "gmp"

  def install
    ENV.deparallelize
    system "./configure", "--prefix=#{prefix}"
    system "make", "CCOMP=clang", "all"
    system "make", "install"
  end
end

Add tags for each release

Hi,

Is it ok for you to add tags for every new release? Tags will help docker easily find a specific version to build.

error: unknown type name ‘atstyarr_type’

My understanding based on a previous e-mail is that var my_array2 = @[int][arr_len](1)
is OK, and is a writable array. However, perhaps I'm specifying types incorrectly below.

Also note a different error occurs if the contents of main are uncommented.

(* ****** ****** *)
//
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)


staload
UN = "prelude/SATS/unsafe.sats"


fun loop {n: nat} (n: int n, a1: @[int][n], a2: @[int][n]): void = (
println!($UN.cast{int}(a1));
println!($UN.cast{int}(a2));

) // end of loop(...)


implement main0 () = {

(* val arr_len = 5 *)
(* var my_array1 = @[int][arr_len](1) *)
(* var my_array2 = @[int][arr_len](1,2,3,4) *)
(* var my_array2 = @[int][arr_len](1,2,3,4,5) *)
(* var my_array2 = @[int][arr_len](1,2,3,4,5,6) *)

(* val () = loop(arr_len, my_array1, my_array2) *)

val x = 5
} // end of main0()