githwxi / ats-xanadu

Bootstrapping ATS3

ATS3 - ATS/Xanadu

A Programming Language System to Unleash the Potentials of Types and Templates

Build Status

Project Description

ATS3 is an attempt to greatly improve upon ATS2.

Probably the biggest problem with ATS2 is the very steep learning curve associated with it. Very few programmers were able to ever overcome it to reach the point where they could truly start enjoying the tremendous power of (advanced) type-checking and (embeddable) templates.

When DML (the predecessor of ATS) was designed nearly 20 years ago, a two-layered approach to type-checking was taken: ML-like type-checking first and dependent type-checking second. This approach was later abandoned in the design of ATS. Instead, there is only dependent type-checking in ATS1 and ATS2. In ATS3, DML's two-layered approach is to be adopted. In particular, a program in ATS3 that passes ML-like type-checking can be compiled and executed. So one can skip dependent type-checking in ATS3 if one so chooses. In this way, the learning curve is expected to be greatly leveled. But there is much more than just leveling the learning curve.

ML-like types are algebraic (involving no explicit quantifiers). Such types are so much friendlier than dependent types (which often involve explicit quantifiers) for supporting type-based meta-programming. It seems that a chance has finally arrived to properly address the problem of template instance resolution that causes so much annoyance in ATS2 (due to the very use of dependent types for template selection).

In short, ATS3 adds an extra layer to ATS2 for supporting ML-like algebraic type-checking. Type-based meta-programming in ATS3 solely uses algebraic types (while ATS2 uses dependent types).

Installing ATS3

ATS3 is not ready for release yet.

Please see http://www.ats-lang.org/Downloads.html for instructions after it is officially released.

Developing ATS3

Documenting ATS3

Licenses for ATS/Xanadu

• The Compiler (ATS/Xanadu): GPLv3
• The ATS source for the Libraries (ATSLIB/{prelude,xatslib}): LGPLv3.
• As a special exception, any C code generated by the Compiler based on the Libraries source is not considered by default to be licensed under GPLv3/LGPLv3. If you use such C code together with other code to create an executable, then the C code by itself does not cause the executable to be covered by GPLv3/LGPLv3. However, there may be reasons unrelated to using ATS that can result in the executable being covered by GPLv3/LGPLv3.
• The contributed portion (ATS/Xanadu/contrib) is released under the MIT license.
• There is also a release under the MIT license for the C header files of the Libraries, which one can, for instance, freely insert into any C code generated from ATS source code.

ats-xanadu's Issues

Separate exn types

It would be helpful to have two separate types for exceptions, with one type for recoverable exceptions and the other type for unrecoverable exceptions (i.e., fatal exceptions). The cleanest approach of this idea appears to be the Java class hierarchy with https://docs.oracle.com/javase/8/docs/api/java/lang/Exception.html for recoverable exceptions and https://docs.oracle.com/javase/8/docs/api/java/lang/Error.html for unrecoverable exceptions. Having that clear delineation helps to communicate the intent in the source code for potential failures.

My impression is that at least the ATS2 exceptions AssertExn and IllegalArgExn are unrecoverable because they represent a broken constraint in the source code.

If you didn't want to have exceptions in ATS3, that would be good too. That approach should be better for compiler optimizations like inlining.

Release process

We should automate releases (let's use the releases feature of GitHub).

Features worth having

Hi.
I read there that targeting LLVM is the plan.
If that is the case, we would probably need the following features in order to replace inline C:

• inline assembly (for doing stuff like syscalls).
• attribute to specify the ABI of a function.
• maybe something for alignment and packing of records.

I can't think of any other features worth having, but I'll add them to this post as I think of them.

Thanks.

Setup CI

I thinks this merits attention.

How do we setup CI such that all tests run on every commit?

Parsing error for block surrounded by curly braces

Will there be support for blocks surrounded by curly braces (that is for blocks with void return type)?

For example:

implfun main0() = 
{
  val () = println!()
}

The error:

the_fxtyenv = 

[the_fixity_load] is finished.
the_basics_load: prelude/basics.sats
the_prelude_load: prelude/SATS/gbas.sats
synread_d0ecl: d0c0 = D0Cimpdecl(IMPLMNT(IMPfun); DECLMODnone(); ; ; DQ0EIDnone(I0DNTsome(IDENT_alp(main0))); ; F0ARGsome_dyn(D0Pparen(LPAREN; ; d0pat_RPAREN_cons0(RPAREN))); EFFS0EXPnone(); EQ; D0Esqarg(LBRACE; ; VAL(VLKval)))
synread_d0ecl: d0c0 = D0Cvaldecl(VAL(VLKval); DECLMODnone(); V0ALDECL@{, pat=D0Pparen(LPAREN; ; d0pat_RPAREN_cons0(RPAREN)), teq=EQ, def=D0Eapps(D0Eid(I0DNTsome(IDENT_alp(println))), D0Eid(I0DNTsome(IDENT_sym(!))), D0Eparen(LPAREN; ; d0exp_RPAREN_cons0(RPAREN))), wtp=WTHS0EXPnone()})
43(line=4, offs=1) -- 44(line=4, offs=2): SYNERR(d0ecl): RBRACE
synread_top: nxerr = 1
synread_top: there is one synerr!
exit(ATS): uncaught exception at run-time:
Xanadu/srcgen/xats/SATS/xerrory.sats:XATSOPT_SYNERR_EXN(1027)

The parser seems to be looking for quantifiers after encountering the opening brace.

Why not talk about proof component at overview.txt?

I believe ATS3 also stands on:

• Dynamics
• Proofs
• Statics

http://cs.likai.org/ats/ml-programmers-guide-to-ats

location of xatsopt

Hi, Just curious - why is xatsopt not located at $XATSOME/bin/xatsopt currently? Would it simplify things to make a simple makefile to just run srcgen/xats/Makefile and move the resulting binary?

please add a guide on how to contribute

detailed roadmap , may be

Road map and how to contribute

What do you need help with in terms of development? What are you working on now and what is coming next? Is there a place with a (somewhat) detailed road map of what needs to get done. Would love to help but not sure where to start :)

Grammar definition

After seeing the info on this issue githwxi/ATS-Postiats#208 (comment) I tweaked the gammar to be able to view it at https://www.bottlecaps.de/rr/ui as a railroad diagram (paste the tweaked grammar bellow in the Edit Grammar tab then switch to the View Diagram tab and you can also download the diagram from threre).

There is a way to have a grammar to what this project is trying to build ?

/************************************************************************/
/*                                                                      */
/*                         Applied Type System                          */
/*                                                                      */
/*                              Hongwei Xi                              */
/*                                                                      */
/************************************************************************/

/*
** ATS/Anairiats - Unleashing the Potential of Types!
**
** Copyright (C) 2002-2008 Hongwei Xi.
**
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*/

/* ****** ****** */
//
// Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
// Start time: July 2007
//
// This version is prepared together with
// Sylvain Nahas (sylvain.nahas AT googlemail DOT com)
//
/* ****** ****** */
/*

Grammar for ATS/Anairiats


Some Explanation on the EBNF Notation

"..."   : terminal string

::=     : nonterminal definition

a , b   : concatenation

(...)   : grouping

{a}     : 0 or more a (Kleene's star closure)

{a}+    : 1 or more a (this is an extension to the standard EBNF)

[a]     : 0 or 1 a (option)

a | b   : a or b (alternation)
*/

/*...*/ //: comment

program ::=
  /*|*/ YYBEG_d0ecseq_sta d0ecseq_sta TOKEN_eof
  | YYBEG_d0ecseq_dyn d0ecseq_dyn TOKEN_eof
  | YYBEG_i0de i0de TOKEN_eof
  | YYBEG_s0rtid s0rtid TOKEN_eof
  | YYBEG_si0de si0de TOKEN_eof
  | YYBEG_di0de di0de TOKEN_eof
  | YYBEG_s0exp s0exp TOKEN_eof
  | YYBEG_d0exp d0exp TOKEN_eof
/* program */

abskind ::=
  /*|*/ "absprop"
  | "abstype"
  | "abst@ype"
  | "absview"
  | "absviewtype"
  | "absviewt@ype"
/* abskind */

dcstkind ::=
  /*|*/ "fun"
  | "val"
  | "castfn"
  | "praxi"
  | "prfun"
  | "prval"
/* dcstkind */

datakind ::=
  /*|*/ "dataprop"
  | "datatype"
  | "dataview"
  | "dataviewtype"
/* datakind */

stadefkind ::=
  /*|*/ "stadef"
  | "propdef"
  | "typedef"
  | "viewdef"
  | "viewtypedef"
/* stadefkind */

valkind ::=
  /*|*/ "val"
  | "val-"
  | "val+"
  | "prval"
/* valkind */

funkind ::=
  /*|*/ "fn"
  | "fn*"
  | "fun"
  | "castfn"
  | "prfn"
  | "prfun"
/* funkind */

lamkind ::=
  /*|*/ "lam"
  | "@lam"
  | "llam"
  | "@llam"
/* lamkind */

fixkind ::=
  /*|*/ "fix"
  | "@fix"
/* fixkind */

srpifkind ::=
  /*|*/ "#if"
  | "#ifdef"
  | "#ifndef"
/* srpifkind */

srpelifkind ::=
  /*|*/ "#elif"
  | "#elifdef"
  | "#elifndef"
/* srpelifkind */

srpthenopt ::=
  /*|*/ "#then"?
/* srpthenopt */

i0de ::=
  /*|*/ ALNUMRIC_IDENTIFIER
  | SYMBOLIC_IDENTIFIER
  | "&"
  | "\"
  | "!"
  | "="
  | ">"
  | "><"
  | "<"
  | "->"
  | "-<>"
  | "~"
/* i0de */

i0de_dlr ::=
  /*|*/ IDENTIFIER_dlr
/* i0de_dlr */

i0deseq ::=
  /*|*/ i0de*
/* i0deseq */

i0dext ::=
  /*|*/ EXTERNAL_IDENTIFIER
  | "do"
  | "while"
/* i0dext */

l0ab ::=
  /*|*/ i0de
  | LITERAL_int
  | "(" l0ab ")"
/* l0ab */

stai0de ::=
  /*|*/ ALNUMRIC_IDENTIFIER
/* stai0de */

p0rec ::=
  //| /*(empty)*/
  (
  /*|*/ LITERAL_int
  | "(" i0de ")"
  | "(" i0de SYMBOLIC_IDENTIFIER LITERAL_int ")"
  )?
/* p0rec */

e0xp ::=
  /*|*/ atme0xp+
/* e0xp */

atme0xp ::=
  /*|*/ LITERAL_char
  | LITERAL_float
  | LITERAL_int
  | LITERAL_string
  | "#FILENAME"
  | "#LOCATION"
  | i0de
  | "(" e0xpseq ")"
  | "%(" e0xp ")"
/* atme0xp */

e0xpseq ::=
  //| /*(empty)*/
  /*|*/ (e0xp commae0xpseq)?
/* e0xpseq */

commae0xpseq ::=
  /*|*/ (","  e0xp)*
/* commae0xpseq */

e0xpopt ::=
  /*|*/ e0xp?
/* e0xpopt */

e0ffid ::=
  /*|*/ ALNUMRIC_IDENTIFIER
/* e0ffid */

e0fftag ::=
  /*|*/ "!" e0ffid
  | "~" e0ffid
  | e0ffid
  | "fun"
  | LITERAL_int
/* e0fftag */

e0fftagseq ::=
  //| /*(empty)*/
  /*|*/ (e0fftag commae0fftagseq)?
/* e0fftagseq */

commae0fftagseq ::=
  /*|*/ (","  e0fftag)*
/* commae0fftagseq */

colonwith ::=
  /*|*/ ":"
  | ":<>"
  | ":<" e0fftagseq ">"
/* colonwith */

s0rt ::=
  /*|*/ atms0rt+
/* s0rt */

s0rtq ::=
  /*|*/ i0de_dlr "."
  | "$" LITERAL_string "."
/* s0rtq */

s0rtid ::=
  /*|*/ ALNUMRIC_IDENTIFIER
  | SYMBOLIC_IDENTIFIER
  | "t@ype"
  | "viewt@ype"
  | "\"
  | "->"
  | "-<>"
/* s0rtid */

atms0rt ::=
  /*|*/ s0rtid
  | s0rtq s0rtid
  | "(" s0rtseq ")"
  | "@(" s0rtseq ")"
/* atms0rt */

s0rtseq ::=
  //| /*(empty)*/
  /*|*/ (s0rt commas0rtseq)?
/* s0rtseq */

commas0rtseq ::=
  /*|*/ ("," s0rt)*
/* commas0rtseq */

s0rtpol ::=
  /*|*/ s0rt
  | "prop-"
  | "prop+"
  | "type-"
  | "type+"
  | "t@ype-"
  | "t@ype+"
  | "view-"
  | "view+"
  | "viewtype-"
  | "viewtype+"
  | "viewt@ype-"
  | "viewt@ype+"
/* s0rtpol */

d0atsrtcon ::=
  /*|*/ i0de
  | i0de "of" s0rt
/* d0atsrtcon */

d0atsrtconseq ::=
  /*|*/ bard0atsrtconseq
  | d0atsrtcon bard0atsrtconseq
/* d0atsrtconseq */

bard0atsrtconseq ::=
  /*|*/ ("|" d0atsrtcon)*
/* bard0atsrtconseq */

d0atsrtdec ::=
  /*|*/ i0de "=" d0atsrtconseq
/* d0atsrtdec */

andd0atsrtdecseq ::=
  /*|*/ ("and" d0atsrtdec)*
/* andd0atsrtdecseq */

s0taq ::=
  /*|*/ i0de_dlr "."
  | i0de_dlr ":"
  | "$" LITERAL_string "."
/* s0taq */

d0ynq ::=
  /*|*/ i0de_dlr "."
  | i0de_dlr ":"
  | i0de_dlr i0de_dlr ":"
  | "$" LITERAL_string "."
  | "$" LITERAL_string i0de_dlr ":"
/* d0ynq */

si0de ::=
  /*|*/ ALNUMRIC_IDENTIFIER
  | SYMBOLIC_IDENTIFIER
  | "r@ead"
  | "&"
  | "\"
  | "!"
  | ">"
  | "<"
  | "->"
  | "~"
/* si0de */

sqi0de ::=
  /*|*/ si0de
  | s0taq si0de
/* sqi0de */

commasi0deseq ::=
  /*|*/ ("," si0de)*
/* commasi0deseq */

di0de ::=
  /*|*/ ALNUMRIC_IDENTIFIER
  | SYMBOLIC_IDENTIFIER
  | "\"
  | "!"
  | "="
  | ">"
  | "><"
  | "<"
  | "~"
/* di0de */

dqi0de ::=
  /*|*/ di0de
  | d0ynq di0de
/* dqi0de */

pi0de ::=
  /*|*/ ALNUMRIC_IDENTIFIER
  | SYMBOLIC_IDENTIFIER
/* pi0de */

fi0de ::=
  /*|*/ di0de
  | "op" di0de
/* fi0de */

arri0de ::=
  /*|*/ ARRAY_IDENTIFIER
/* arri0de */

arrqi0de ::=
  /*|*/ arri0de
  | d0ynq arri0de
/* arrqi0de */

tmpi0de ::=
  /*|*/ TEMPLATE_IDENTIFIER
/* tmpi0de */

tmpqi0de ::=
  /*|*/ tmpi0de
  | d0ynq tmpi0de
/* tmpqi0de */

colons0rtopt ::=
  /*|*/ (":" s0rt)?
/* colons0rtopt */

s0arg ::=
  /*|*/ si0de colons0rtopt
/* s0arg */

s0argseq ::=
  //| /*(empty)*/
  /*|*/ (s0arg commas0argseq)?
/* s0argseq */

commas0argseq ::=
  /*|*/ ("," s0arg)*
/* commas0argseq */

s0argseqseq ::=
  //| /*(empty)*/
  (
  /*|*/ si0de s0argseqseq
  | "(" s0argseq ")" s0argseqseq
  )?
/* s0argseqseq */

decs0argseq ::=
  //| /*(empty)*/
  /*|*/ (s0arg commadecs0argseq)?
/* decs0argseq */

commadecs0argseq ::=
  /*|*/ ("," s0arg)*
/* commadecs0argseq */

decs0argseqseq ::=
  //| /*(empty)*/
  /*|*/ ("{" decs0argseq "}" decs0argseqseq)?
/* decs0argseqseq */

sp0at ::=
  /*|*/ sqi0de "(" s0argseq ")"
/* sp0at */

s0exp ::=
  /*|*/ apps0exp
  | exts0exp
  | s0exp ":" s0rt
  | "lam" s0argseqseq colons0rtopt "=>" s0exp
/* s0exp */

atms0exp ::=
  /*|*/ LITERAL_char
  | LITERAL_int
  | LITERAL_intsp
  | si0de
  | "op" si0de
  | s0taq si0de
  | "(" s0expseq ")"
  | "(" s0expseq "|" s0expseq ")"
  | "@(" s0expseq ")"
  | "'(" s0expseq ")"
  | "$tup_t" "(" s0expseq ")"
  | "$tup_vt" "(" s0expseq ")"
  | "@(" s0expseq "|" s0expseq ")"
  | "'(" s0expseq "|" s0expseq ")"
  | "$tup_t" "(" s0expseq "|" s0expseq ")"
  | "$tup_vt" "(" s0expseq "|" s0expseq ")"
  | "@{" labs0expseq "}"
  | "'{" labs0expseq "}"
  | "$rec_t" "{" labs0expseq "}"
  | "$rec_vt" "{" labs0expseq "}"
  | "$extype_struct" LITERAL_string "of" "{" labs0expseq "}"
  | "@[" s0exp "]" "[" s0arrind
  | "-<" e0fftagseq ">"
  | "-<>"
  | "{" s0quaseq "}"
  | "[" s0quaseq "]"
  | "#[" s0quaseq "]"
/* atms0exp */

apps0exp ::=
  /*|*/ atms0exp+
/* apps0exp */

exts0exp ::=
  /*|*/ "$extype" LITERAL_string
  | exts0exp atms0exp
/* exts0exp */

s0expelt ::=
  //| /*(empty)*/
  (
  /*|*/ "{" s0exp "}"
  | "[" s0exp "]"
  )?
/* s0expelt */

s0arrind ::=
  /*|*/ s0expseq "]"
  | s0expseq "]" "[" s0arrind
/* s0arrind */

s0qua ::=
  /*|*/ apps0exp
  | si0de commasi0deseq ":" s0rtext
/* s0qua */

s0quaseq ::=
  //| /*(empty)*/
  /*|*/ (s0qua barsemis0quaseq)?
/* s0quaseq */

barsemis0quaseq ::=
  /*|*/ (("|" | ";") s0qua)*
/* barsemis0quaseq */

s0rtext ::=
  /*|*/ s0rt
  | "{" si0de ":" s0rtext "|" s0exp barsemis0expseq "}"
/* s0rtext */

s0expseq ::=
  //| /*(empty)*/
  /*|*/ s0expseq1?
/* s0expseq */

barsemis0expseq ::=
  /*|*/ (("|" | ";") s0exp)*
/* barsemis0expseq */

commas0expseq ::=
  /*|*/ (","  s0exp)*
/* commas0expseq */

s0expseq1 ::=
  /*|*/ s0exp commas0expseq
/* s0expseq1 */

labs0expseq ::=
  //| /*(empty)*/
  /*|*/ (l0ab "=" s0exp commalabs0expseq)?
/* labs0expseq */

commalabs0expseq ::=
  /*|*/ (","  l0ab  "="  s0exp)*
/* commalabs0expseq */

t0mps0exp ::=
  /*|*/ atms0exp+
/* t0mps0exp */

t1mps0exp ::=
  /*|*/ t0mps0exp
/* t1mps0exp */

t1mps0expseq ::=
  //| /*(empty)*/
  /*|*/ (t1mps0exp commat1mps0expseq)?
/* t1mps0expseq */

commat1mps0expseq ::=
  /*|*/ ("," t1mps0exp)*
/* commat1mps0expseq */

gtlt_t1mps0expseqseq ::=
  //| /*(empty)*/
  /*|*/ ("><" t1mps0expseq gtlt_t1mps0expseqseq)?
/* gtlt_t1mps0expseqseq */

impqi0de ::=
  /*|*/ dqi0de
  | tmpqi0de t1mps0expseq gtlt_t1mps0expseqseq ">"
/* impqi0de */

s0rtdef ::=
  /*|*/ s0rtid "=" s0rtext
/* s0rtdef */

ands0rtdefseq ::=
  /*|*/ ("and"  s0rtdef)*
/* ands0rtdefseq */

d0atarg ::=
  /*|*/ s0rtpol
  | i0de ":" s0rtpol
/* d0atarg */

d0atargseq ::=
  //| /*(empty)*/
  /*|*/ (d0atarg commad0atargseq)?
/* d0atargseq */

commad0atargseq ::=
  /*|*/ (","  d0atarg)*
/* commad0atargseq */

s0tacon ::=
  /*|*/ si0de
  | si0de "(" d0atargseq ")"
  | si0de "=" s0exp
  | si0de "(" d0atargseq ")" "=" s0exp
/* s0tacon */

ands0taconseq ::=
  /*|*/ ("and"  s0tacon)*
/* ands0taconseq */

s0tacst ::=
  /*|*/ si0de ":" s0rt
  | si0de "(" d0atargseq ")" ":" s0rt
/* s0tacst */

ands0tacstseq ::=
  /*|*/ ("and"  s0tacst)*
/* ands0tacstseq */

s0tavar ::=
  /*|*/ si0de ":" s0rt
/* s0tavar */

ands0tavarseq ::=
  /*|*/ ("and"  s0tavar)*
/* ands0tavarseq */

s0expdef ::=
  /*|*/ si0de s0argseqseq colons0rtopt "=" s0exp
/* s0expdef */

ands0expdefseq ::=
  /*|*/ ("and"  s0expdef)*
/* ands0expdefseq */

s0aspdec ::=
  /*|*/ sqi0de s0argseqseq colons0rtopt "=" s0exp
/* s0aspdec */

conq0uaseq ::=
  //| /*(empty)*/
  /*|*/ ("{" s0quaseq "}" conq0uaseq)?
/* conq0uaseq */

coni0ndopt ::=
  //| /*(empty)*/
  /*|*/ ("(" s0expseq ")")?
/* coni0ndopt */

cona0rgopt ::=
  //| /*(empty)*/
  /*|*/ ("of" s0exp)?
/* cona0rgopt */

d0atcon ::=
  /*|*/ conq0uaseq di0de coni0ndopt cona0rgopt
/* d0atcon */

d0atconseq ::=
  /*|*/ bard0atconseq
  | d0atcon bard0atconseq
/* d0atconseq */

bard0atconseq ::=
  /*|*/ ("|"  d0atcon)*
/* bard0atconseq */

d0atdec ::=
  /*|*/ si0de "=" d0atconseq
  | si0de "(" d0atargseq ")" "=" d0atconseq
/* d0atdec */

andd0atdecseq ::=
  /*|*/ ("and"  d0atdec)*
/* andd0atdecseq */

s0expdefseqopt ::=
  //| /*(empty)*/
  /*|*/ ("where" s0expdef ands0expdefseq)?
/* s0expdefseqopt */

e0xndec ::=
  /*|*/ conq0uaseq di0de cona0rgopt
/* e0xndec */

ande0xndecseq ::=
  /*|*/ ("and"  e0xndec)*
/* ande0xndecseq */

p0arg ::=
  /*|*/ pi0de
  | pi0de ":" s0exp
/* p0arg */

p0argseq ::=
  //| /*(empty)*/
  /*|*/ (p0arg commap0argseq)?
/* p0argseq */

commap0argseq ::=
  /*|*/ (","  p0arg)*
/* commap0argseq */

d0arg ::=
  /*|*/ pi0de
  | "(" p0argseq ")"
  | "(" p0argseq "|" p0argseq ")"
  | "{" s0quaseq "}"
/* d0arg */

d0argseq ::=
  /*|*/ d0arg*
/* d0argseq */

extnamopt ::=
  //| /*(empty)*/
  /*|*/ ("=" LITERAL_string)?
/* extnamopt */

d0cstdec ::=
  /*|*/ di0de d0argseq colonwith s0exp extnamopt
/* d0cstdec */

andd0cstdecseq ::=
  /*|*/ ("and"  d0cstdec)*
/* andd0cstdecseq */

s0vararg ::=
  /*|*/ ".."
  | "..."
  | s0argseq
/* s0vararg */

s0exparg ::=
  /*|*/ ".."
  | "..."
  | s0expseq1
/* s0exparg */

s0elop ::=
  /*|*/ "."
  | "->"
/* s0elop */

witht0ype ::=
  //| /*(empty)*/
  (
  /*|*/ "withprop" s0exp
  | "withtype" s0exp
  | "withview" s0exp
  | "withviewtype" s0exp
  )?
/* witht0ype */

p0at ::=
  /*|*/ atmp0at argp0atseq
  | p0at ":" s0exp
  | pi0de "as" p0at
  | "!" pi0de "as" p0at
  | "~" p0at
/* p0at */

atmp0at ::=
  /*|*/ LITERAL_char
  | LITERAL_int
  | LITERAL_float
  | LITERAL_string
  | pi0de
  | "!" pi0de
  | "op" pi0de
  | d0ynq pi0de
  | "(" p0atseq ")"
  | "(" p0atseq "|" p0atseq ")"
  | "'[" p0atseq "]"
  | "@(" p0atseq ")"
  | "'(" p0atseq ")"
  | "@(" p0atseq "|" p0atseq ")"
  | "'(" p0atseq "|" p0atseq ")"
  | "@{" labp0atseq "}"
  | "'{" labp0atseq "}"
  | "[" s0argseq "]"
/* atmp0at */

argp0at ::=
  /*|*/ atmp0at
  | "{" s0vararg "}"
/* argp0at */

argp0atseq ::=
  /*|*/ argp0at*
/* argp0atseq */

p0atseq ::=
  //| /*(empty)*/
  /*|*/ (p0at commap0atseq)?
/* p0atseq */

commap0atseq ::=
  /*|*/ (","  p0at)*
/* commap0atseq */

labp0atseq ::=
  /*|*/ "..."
  | l0ab "=" p0at commalabp0atseq
/* labp0atseq */

commalabp0atseq ::=
  /*|*/ (","  l0ab  "="  p0at)*
/* commalabp0atseq */

f0arg1 ::=
  /*|*/ "{" s0quaseq "}"
  | atmp0at
  | ".<" s0expseq ">."
  | ".<>."
/* f0arg1 */

f0arg1seq ::=
  /*|*/ f0arg1*
/* f0arg1seq */

f0arg2 ::=
  /*|*/ "{" s0argseq "}"
  | atmp0at
/* f0arg2 */

f0arg2seq ::=
  /*|*/ f0arg2*
/* f0arg2seq */

d0exp ::=
  /*|*/ atmd0exp argd0expseq
  | d0exp ":" s0exp
  | ifhead d0exp "then" d0exp
  | ifhead d0exp "then" d0exp "else" d0exp
  | sifhead s0exp "then" d0exp "else" d0exp
  | casehead d0exp "of" c0lauseq
  | scasehead s0exp "of" sc0lauseq
  | lamkind f0arg1seq colons0expopt funarrow d0exp
  | fixkind di0de f0arg1seq colons0expopt funarrow d0exp
  | forhead initestpost d0exp
  | whilehead atmd0exp d0exp
  | "$raise" d0exp
  | tryhead d0expsemiseq0 "with" c0lauseq
  | d0exp "where" "{" d0ecseq_dyn "}"
/* d0exp */

atmd0exp ::=
  /*|*/ LITERAL_char
  | LITERAL_float
  | LITERAL_floatsp
  | LITERAL_int
  | LITERAL_intsp
  | LITERAL_string
  | "#FILENAME"
  | "#LOCATION"
  | di0de
  | "op" di0de
  | d0ynq i0de
  | i0dext
  | "&"
  | "break"
  | "continue"
  | "fold@" s0expdargseq
  | "free@" s0expdargseq
  | "view@"
  | "$decrypt"
  | "$encrypt"
  | "$delay"
  | "$ldelay"
  | "$dynload"
  | "$effmask_all"
  | "$effmask_exn"
  | "$effmask_ntm"
  | "$effmask_ref"
  | "@[" s0exp "]" "(" d0expcommaseq ")"
  | "@[" s0exp "]" "[" d0exp "]" "(" d0expcommaseq ")"
  | "$arrsz" s0expelt "(" d0expcommaseq ")"
  | arrqi0de d0arrind
  | s0elop l0ab
  | s0elop "[" d0arrind
  | tmpqi0de t1mps0expseq gtlt_t1mps0expseqseq ">"
  | "#[" s0exparg "|" d0exp "]"
  | "(" d0expcommaseq ")"
  | "(" d0expcommaseq "|" d0expcommaseq ")"
  | "$lst_t" s0expelt "(" d0expcommaseq ")"
  | "$lst_vt" s0expelt "(" d0expcommaseq ")"
  | "'[" d0expcommaseq "]"
  | "begin" d0expsemiseq0 "end"
  | "(" d0expsemiseq1 ")"
  | "@(" d0expcommaseq ")"
  | "'(" d0expcommaseq ")"
  | "$tup_t" "(" d0expcommaseq ")"
  | "$tup_vt" "(" d0expcommaseq ")"
  | "@(" d0expcommaseq "|" d0expcommaseq ")"
  | "'(" d0expcommaseq "|" d0expcommaseq ")"
  | "@{" labd0expseq "}"
  | "'{" labd0expseq "}"
  | "$rec_t" "{" labd0expseq "}"
  | "$rec_vt" "{" labd0expseq "}"
  | "$extval" "(" s0exp "," LITERAL_string ")"
  | "%(" d0exp ")"
  | ",(" d0exp ")"
  | "`(" d0expsemiseq0 ")"
  | "let" d0ecseq_dyn "in" d0expsemiseq0 "end"
  | "{" d0ecseq_dyn "}"
/* atmd0exp */

s0expdarg ::=
  /*|*/ "{" s0exparg "}"
/* s0expdarg */

s0expdargseq ::=
  /*|*/ s0expdarg*
/* s0expdargseq */

argd0exp ::=
  /*|*/ atmd0exp
  | s0expdarg
/* argd0exp */

argd0expseq ::=
  /*|*/ argd0exp*
/* argd0expseq */

d0arrind ::=
  /*|*/ d0expcommaseq "]"
  | d0expcommaseq "]" "[" d0arrind
/* d0arrind */

colons0expopt ::=
  //| /*(empty)*/
  /*|*/ (":" s0exp)?
/* colons0expopt */

funarrow ::=
  /*|*/ "=>"
  | "=<>"
  | "=<" e0fftagseq ">"
/* funarrow */

caseinv ::=
  //| /*(empty)*/
  /*|*/ (i0nvresstate "=>")?
/* caseinv */

ifhead ::=
  /*|*/ "if" caseinv
/* ifhead */

sifhead ::=
  /*|*/ "sif" caseinv
/* sifhead */

casehead ::=
  /*|*/ "case" caseinv
  | "case-" caseinv
  | "case+" caseinv
/* casehead */

scasehead ::=
  /*|*/ "scase" caseinv
/* scasehead */

forhead ::=
  /*|*/ "for"
  | "for*" loopi0nv "=>"
/* forhead */

whilehead ::=
  /*|*/ "while*" loopi0nv "=>"
/* whilehead */

tryhead ::=
  /*|*/ "try"
/* tryhead */

d0expcommaseq ::=
  //| /*(empty)*/
  /*|*/ (d0exp commad0expseq)?
/* d0expcommaseq */

commad0expseq ::=
  | (","  d0exp)*
/* commad0expseq */

d0expsemiseq0 ::=
  //| /*(empty)*/
  (
  /*|*/ d0exp
  | d0exp ";" d0expsemiseq0
  )?
/* d0expsemiseq0 */

d0expsemiseq1 ::=
  /*|*/ d0exp ";" d0expsemiseq0
/* d0expsemiseq1 */

labd0expseq ::=
  //| /*(empty)*/
  /*|*/ (l0ab "=" d0exp commalabd0expseq)?
/* labd0expseq */

commalabd0expseq ::=
  /*|*/ (","  l0ab  "="  d0exp)*
/* commalabd0expseq */

m0atch ::=
  /*|*/ d0exp
  | d0exp "as" p0at
/* m0atch */

m0atchseq ::=
  /*|*/ m0atch andm0atchseq
/* m0atchseq */

andm0atchseq ::=
  /*|*/ ("and" m0atch)*
/* andm0atchseq */

guap0at ::=
  /*|*/ p0at
  | p0at "when" m0atchseq
/* guap0at */

c0lau ::=
  /*|*/ guap0at "=>" d0exp
  | guap0at "=>>" d0exp
  | guap0at "=/=>" d0exp
  | guap0at "=/=>>" d0exp
/* c0lau */

c0lauseq ::=
  /*|*/ barc0lauseq
  | c0lau barc0lauseq
/* c0lauseq */

barc0lauseq ::=
  /*|*/ ("|"  c0lau)*
/* barc0lauseq */

sc0lau ::=
  /*|*/ sp0at "=>" d0exp
/* sc0lau */

sc0lauseq ::=
  /*|*/ barsc0lauseq
  | sc0lau barsc0lauseq
/* sc0lauseq */

barsc0lauseq ::=
  /*|*/ ("|" sc0lau)*
/* barsc0lauseq */

i0nvqua ::=
  //| /*(empty)*/
  /*|*/ ("{" s0quaseq "}")?
/* i0nvqua */

i0nvmet ::=
  //| /*(empty)*/
  (
  /*|*/ ".<" s0expseq ">."
  | ".<>."
  )?
/* i0nvmet */

i0nvarg ::=
  /*|*/ di0de ":"
  | di0de ":" s0exp
/* i0nvarg */

i0nvargseq ::=
  //| /*(empty)*/
  /*|*/ (i0nvarg commai0nvargseq)?
/* i0nvargseq */

commai0nvargseq ::=
  /*|*/ (","  i0nvarg)*
/* commai0nvargseq */

i0nvargstate ::=
  /*|*/ "(" i0nvargseq ")"
/* i0nvargstate */

i0nvresqua ::=
  //| /*(empty)*/
  /*|*/ ("[" s0quaseq "]")?
/* i0nvresqua */

i0nvresstate ::=
  //| /*(empty)*/
  /*|*/ (":" i0nvresqua "(" i0nvargseq ")")?
/* i0nvresstate */

loopi0nv ::=
  /*|*/ i0nvqua i0nvmet i0nvargstate i0nvresstate
/* loopi0nv */

initestpost ::=
  /*|*/ "(" d0expcommaseq ";" d0expcommaseq ";" d0expcommaseq ")"
/* initestpost */

m0arg ::=
  /*|*/ pi0de
/* m0arg */

m0argseq ::=
  //| /*(empty)*/
  /*|*/ (m0arg commam0argseq)?
/* m0argseq */

commam0argseq ::=
  /*|*/ (","  m0arg)*
/* commam0argseq */

m0acarg ::=
  /*|*/ m0arg
  | "(" m0argseq ")"
/* m0acarg */

m0acargseq ::=
  /*|*/ m0acarg*
/* m0acargseq */

m0acdef ::=
  /*|*/ di0de m0acargseq "=" d0exp
/* m0acdef */

andm0acdefseq ::=
  /*|*/ ("and"  m0acdef)*
/* andm0acdefseq */

v0aldec ::=
  /*|*/ p0at "=" d0exp witht0ype
/* v0aldec */

andv0aldecseq ::=
  /*|*/ ("and"  v0aldec)*
/* andv0aldecseq */

f0undec ::=
  /*|*/ fi0de f0arg1seq "=" d0exp witht0ype
  | fi0de f0arg1seq colonwith s0exp "=" d0exp witht0ype
/* f0undec */

andf0undecseq ::=
  /*|*/ ("and"  f0undec)*
/* andf0undecseq */

v0arwth ::=
  //| /*(empty)*/
  /*|*/ ("with" pi0de)*
/* v0arwth */

v0ardec ::=
  /*|*/ pi0de v0arwth "=" d0exp
  | "!" pi0de v0arwth "=" d0exp
  | pi0de ":" s0exp v0arwth
  | pi0de ":" s0exp v0arwth "=" d0exp
/* v0ardec */

andv0ardecseq ::=
  /*|*/ ("and"  v0ardec)*
/* andv0ardecseq */

i0mpdec ::=
  /*|*/ impqi0de f0arg2seq colons0expopt "=" d0exp
/* i0mpdec */

d0ec ::=
  /*|*/ "infix" p0rec i0deseq
  | "infixl" p0rec i0deseq
  | "infixr" p0rec i0deseq
  | "prefix" p0rec i0deseq
  | "postfix" p0rec i0deseq
  | "nonfix" i0deseq
  | "symintr" i0deseq
  | "#undef" i0de
  | "#define" i0de e0xpopt
  | "#assert" e0xp
  | "#error" e0xp
  | "#print" e0xp
  | "sortdef" s0rtdef ands0rtdefseq
  | "datasort" d0atsrtdec andd0atsrtdecseq
  | "dataparasort" d0atsrtdec andd0atsrtdecseq
  | abskind s0tacon ands0taconseq
  | "stacst" s0tacst ands0tacstseq
  | "stavar" s0tavar ands0tavarseq
  | stadefkind s0expdef ands0expdefseq
  | "assume" s0aspdec
  | datakind d0atdec andd0atdecseq s0expdefseqopt
  | "exception" e0xndec ande0xndecseq
  | "classdec" si0de
  | "classdec" si0de ":" s0exp
  | "overload" di0de "with" dqi0de
  | "overload" "[" "]" "with" dqi0de
  | "macdef" m0acdef andm0acdefseq
  | "macdef" "rec" m0acdef andm0acdefseq
  | "macrodef" m0acdef andm0acdefseq
  | "macrodef" "rec" m0acdef andm0acdefseq
  | "staload" LITERAL_string
  | "staload" stai0de "=" LITERAL_string
/* d0ec */

d0ecarg ::=
  /*|*/ "{" s0quaseq "}"
/* d0ecarg */

d0ecargseq ::=
  /*|*/ d0ecarg*
/* d0ecargseq */

semicolonseq ::=
  /*|*/ ";"*
/* semicolonseq */

d0ec_sta ::=
  /*|*/ d0ec
  | dcstkind d0ecargseq d0cstdec andd0cstdecseq
  | LITERAL_extcode
  | srpifkind guad0ec_sta
  | "#include" LITERAL_string
  | "local" d0ecseq_sta "in" d0ecseq_sta "end"
/* d0ec_sta */

guad0ec_sta ::=
  /*|*/ e0xp srpthenopt d0ecseq_sta "#endif"
  | e0xp srpthenopt d0ecseq_sta "#else" d0ecseq_sta "#endif"
  | e0xp srpthenopt d0ecseq_sta srpelifkind guad0ec_sta
/* guad0ec_sta */

d0ecseq_sta ::=
  /*|*/ d0ecseq_sta_rev
/* d0ecseq_sta */

d0ecseq_sta_rev ::=
  //| /*(empty)*/
  /*|*/ (d0ecseq_sta_rev d0ec_sta semicolonseq)?
/* d0ecseq_sta_rev */

d0ec_dyn ::=
  /*|*/ d0ec
  | "extern" dcstkind d0ecargseq d0cstdec andd0cstdecseq
  | "extern" "typedef" LITERAL_string "=" s0exp
  | "extern" "val" LITERAL_string "=" d0exp
  | valkind v0aldec andv0aldecseq
  | "val" "par" v0aldec andv0aldecseq
  | "val" "rec" v0aldec andv0aldecseq
  | funkind d0ecargseq f0undec andf0undecseq
  | "var" v0ardec andv0ardecseq
  | "implement" decs0argseqseq i0mpdec
  | "local" d0ecseq_dyn "in" d0ecseq_dyn "end"
  | LITERAL_extcode
  | srpifkind guad0ec_dyn
  | "#include" LITERAL_string
  | "dynload" LITERAL_string
/* d0ec_dyn */

guad0ec_dyn ::=
  /*|*/ e0xp srpthenopt d0ecseq_dyn "#endif"
  | e0xp srpthenopt d0ecseq_dyn "#else" d0ecseq_dyn "#endif"
  | e0xp srpthenopt d0ecseq_dyn srpelifkind guad0ec_dyn
/* guad0ec_dyn */

d0ecseq_dyn ::=
  /*|*/ d0ecseq_dyn_rev
/* d0ecseq_dyn */

d0ecseq_dyn_rev ::=
  //| /*(empty)*/
  /*|*/ (d0ecseq_dyn_rev d0ec_dyn semicolonseq)?
/* d0ecseq_dyn_rev */

/* ****** ****** */

/* end of [ats_grammar.desc] */

Why not talk about proofs at overview.txt?

I believe ATS3 stands on:

• Dynamics
• Proofs
• Statics

http://cs.likai.org/ats/ml-programmers-guide-to-ats

Parsing implementation declarations

The parser for implementation declarations (D0Cimpdecl, ptok_impdecl) seems to suggest that the following is valid,

impltmp {a}<b> ident (funargs) = ... 

First question:

What is the reason for parsing both {...} and the new syntax for function templates <...>
here?

Just for comparison

This is how ATS2/Temptory parses such declerations here

Second question:

One can write an expression such as,

impltmp(a:tflt) foo<container(a)>(...) = ... 

Will this syntax be supported in ATS3?

make debug info optional

See #24