Stack Overflow
Stack Overflow

Questions tagged [ats]

ATS is a statically typed programming language that unifies implementation with formal specification. The core of ATS is ML-like, and its type system is rooted in the Applied Type System framework, which in turn gives the language its name. ATS is feature-rich and it supports dependent types (of DML-style), linear types, (embeddable) templates, programming with theorem-proving (PwTP), and more.

Welcome to #ats@stackoverflow!

ATS is a statically typed programming language that unifies implementation with formal specification. The core of ATS is ML-like, and its type system is rooted in the Applied Type System framework, which supports dependent types (of DML-style), linear types, theorem-proving and more.

As of now, the community of ATS is relatively small. We recommend that any questions pertinent to the ATS programming language be given the tag #ats. Doing so can undoubtedly benefit everyone trying to learn and use ATS. In general, questions about ATS concerning syntax, library, type system, and application should be tagged under #ats. On the other hand, suggestions, bug reports, and various discussions on language features should probably be brought to the official google-group for ATS.

Links

105 questions
6
votes
1 answer

Typechecking error involving the andalso macro in ATS

Here are two pieces of code I think are equivalent aside from the second one having more lines then it should: fun move_ul {i:nat} ( p: int(i) , ms: list0(Int) ): list0(Int) = if p - 5 >= 0 andalso p % 4 != 0 then move_ul(p - 5, cons0(p - 5,…
Daren McCulley
  • 73
  • 4
6
votes
1 answer

Why was the ATS language dropped from the Computer Language Benchmarks Game?

Not too long ago the "ATS" programming language was removed from the Computer Language Benchmarks Game. You can still view the old pages via the way back machine. Why is the ATS programming language no longer included in the Computer Language…
mrsteve
  • 4,082
  • 1
  • 26
  • 63
5
votes
2 answers

How to use the funset_avltree library?

I am trying to use the funset_avltree library, but the compiler generates invalid C code. I am using ATS/Postiats version 0.2.10. My code is fairly straightforward: (* ast.sats *) staload "libats/SATS/funset_avltree.sats" datatype ast = | ast_var…
user1804599
5
votes
2 answers

Turning recursive function into tail recursion

I am coding in ATS and am trying to make a function that finds the square root of a given integer. Provided here is code that properly meets my requirments other than it not being tail-recursion. implement intsqrt(n) = if(n >= 1) then let val…
rmw
  • 119
  • 2
  • 10
4
votes
3 answers

How do you read in and access arguments from a main function in ATS2?

This is a common, basic task, so it would be good to know an appropriate way to do this. A similar program in C++ might look like this (ref): #include using namespace std; int main(int argc, char** argv) { for (int i = 0; i < argc;…
bbarker
  • 11,636
  • 9
  • 38
  • 62
4
votes
1 answer

What is the meaning of $effmask_all in ATS?

I have seen quasi-function symbols $effmask_all and $effmask_ref many times in the ATS library code. What is the meaning of these symbols? When should they be called?
user7039610
4
votes
2 answers

How to read user input in ATS?

In my ATS application, I am trying to read a input string from a user. Is there any function in ATS that performs similar functionality as scanf function in C.. If not how to get the input from user without integrating ATS with JS or HTML.
Himanir
  • 41
  • 1
  • 4
4
votes
2 answers

Is there a priority queue implementation in ATS?

I need to do some sort of priority-based search. Could someone point me to a priority queue implementation in ATS?
user7042412
4
votes
1 answer

How to construct a 2-dimensional array in ATS?

For instance, I am looking for an example in ATS that does more or less what the following C code does: int *theMultable[10][10]; void theMultable_initialize() { int i, j; for (i = 0; i < 10; i++) { for (j = 0; j < 10; j++)…
user7039610
4
votes
1 answer

What is the symbol for the exponentiation operation in ATS?

For instance, how can I write an expression in ATS for the 10th power of x? I tried both x^10 and x^^10, but neither worked.
user7039610
4
votes
2 answers

How to create a global variable in ATS?

Basically, I am looking for something more or less equivalent to the following C code: int theGlobalCount = 0; int theGlobalCount_get() { return theGlobalCount; } void theGlobalCount_set(int n) { theGlobalCount = n; return; }
user7039610
4
votes
1 answer

How to allocate a closure-function on the call stack?

When using higher-order functions like list_map, one needs to build closure-functions and pass them as arguments. Afterwards, the built closures become garbage. Is there a way to build such closure-functions on the call stack (so that they are…
user7042412
4
votes
4 answers

What is the syntax for constructing a list-value in ATS?

For instance, how can I construct a list consisting of all the digits: 0, 1, 2, 3, 4, 5, 6, 7, 8, and 9.
user7039610
4
votes
1 answer

What does :<> mean in a function declaration?

The declaration of funset_nil in the file libats/ML/SATS/funset.sats reads: fun{} funset_nil{a:t0p} ():<> set(a) What does :<> mean?
user1804599
3
votes
1 answer

ATS Proof: Why does this static if need greater than or equal to?

I was writing a proof of a*0=0 and I stumbled on some strangeness. Why does the sif a >= 0 on line 7 need to be a >=, and does not compile when its just sif > 0? prfn mul_ax0_0 {a:int} () : MUL(a,0,0) = let prfun auxnat {a:nat} .. () :…
vero
  • 243
  • 1
  • 4
  • 12
1
2 3 4 5 6 7