-
Notifications
You must be signed in to change notification settings - Fork 54
keywords
rodolphito edited this page Dec 12, 2019
·
26 revisions
Note: probably a great way to fill in and curate this page is to grep for 'keyword' in the ATS Book, as they are often described as such there.
-
absprop
- introduce a named abstract proposition definition; a specialized form ofsta
[1]; see type. -
abstype
- introduce a named abstract type definition; a specialized form ofsta
[1]; see type. -
absview
- introduce a named abstract view definition; a specialized form ofsta
[1]; see type. -
absviewtype
- introduce a named abstract view type definition; a specialized form ofsta
[1]; see type. -
absvtype
- shorter name forabsviewtype
; see type. -
addr@
- unary operator that takes a variable (seevar
below) and returns a pointer; the view at this address can be obtained usingview@
(see below). -
assertloc
- a dynamic assertion (boolean), which prints out its location whenever it evaluates to false; see migrating a c project to ats on ats.lang.users. -
case
- used withof
to pattern-match on a value. The first clause that matches the value is used. If there is no match, then case evaluation aborts. Pattern matching can bind a value to a name much likeval
. In fact,val
can be seen as a special case ofcase
where there is only one clause that always matches. Compiling a non-exhaustivecase
emits a warning. -
case-
- is the same ascase
, except it suppresses a potential warning message that would otherwise be emitted when it is a non-exhaustive pattern match. -
case+
- is the same ascase
, except it emits an error message instead of a warning message when it is a non-exhaustive pattern match. -
castfn
- a function (fn
) that changes the type, both dynamically and statically, of its argument. The converted value is returned. When only a staticcastfn
is needed, one can use thecast
and related functions inunsafe.sats
to save time (a common use is converting a pointer from C to some other viewtype). -
dataprop
- introduce a named algebraic proposition definition [2]; see type. -
datatype
- introduce a named algebraic type definition [2]; see type. -
dataview
- introduce a named algebraic view definition [2]; see type. -
dataviewtype
- introduce a named algebraic view type definition [2], a linear data‑type; see type and dataviewtype. -
datavtype
- shorter name fordataviewtype
; see dataviewtype. -
dynload
- declare a module initialization dependency, typically from the module definingmain
; see dynload. -
extern
- declare an entity / definition as extern; the defined item may be a macro or an element in a separate compilation unit; see Writing interfaces to C libraries and C interface. -
fn
- non-recursive function (fun
). Used in place offun
for optimization purposes (is this true?) and as well as to check against the possibility of an accidental infinite loop. -
fun
- a function that can be recursive. -
infix
- likesymintr
, but with fixity; see overload. -
infixr
- likesymintr
, but with fixity; see overload. -
infixl
- likesymintr
, but with fixity; see overload. -
implement
- used to implement a function that has been defined usingfun
orfn
-
of
- has several purposes. Most commonly, it is used as a type specifier in an algebraic constructor (e.g. in adatatype
). It also can specify the type in some other contexts such as specifying what the ATS type is for an external type ($extype
; see C interface). Finally, it can denote operator overloading precedence (see overload). -
overload
- overloads a symbol previously introduced withsymintr
; this tells what is overloaded; see overload. -
postfix
- likesymintr
, but with fixity; see overload. -
prefix
- likesymintr
, but with fixity; see overload. -
primplement
- implement a proof function; see prfun, extern and implement at ats.lang.users; see alsoprimplmnt
. -
primplmnt
- implement a proof function; see prfun, extern and implement at ats.lang.users; see alsoprimplement
. -
propdef
- introduce an alias / name for a proposition definition; a specialized form ofstadef
[1]; see type. -
sif
- like the conditional statementif
, for static conditional expression (in proofs) ; see Constructing Proofs as Total Functions, in Intro to ATS. -
sta
- introduce an alias / name for an abstract static definition; there are specialized form of it; see type. -
stadef
- introduce an alias / name for a concrete static definition;stadef
is to static whatval
is to dynamic; there are specialized form of it; see type and Example: Proving Properties on Braun Trees, in Intro to ATS. -
staload
- either loads a name‑space assigning it to a named prefix or opens a name‑space (anonymously, without a prefix); see staload. -
symintr
- introduce the name of a symbol (without fixity) to be overloaded (this does not introduce the overloading), with the later help ofoverload
andwith
; see overload. -
tkindef
-tkindef k = "t"
is the same asstadef k = $extkind "t"
; see filebasics_sta.sats
. -
typedef
- introduce an alias / name for a concrete type definition; a specialized form ofstadef
[1]; see type. -
val
- introduces a val-declaration, which binds a value to a name. This is the most common way of making "variables" in ATS; but seevar
for an alternative. -
val-
- introduces a val-declaration with additional meaning; if names in a datatype constuctor are being bound (e.g.val-list_cons(x,xs) = some_list
) then it will suppress a warning message in the case that the pattern matching is non-exhaustive. If instead a value is being matched (e.g.val-8 = n*4
), this will perform dynamic checking and will error (in this example, the program will exist if n is not equal to 2). -
val+
- introduces a val-declaration with additional meaning; if names in a datatype constuctor are being bound (e.g.val+list_cons(x,xs) = some_list
) the warning message about non-exhaustiveness for the pattern matching will be converted into an error. Ifval+
is matching a value (as in theval-
example above, it is similar toval-
, but will do static checking. This is useful for things like indexed types, but cannot be used in all the cases where dynamic checking can be used. -
var
- introduces a stack-allocated (local) variable. In contrast to a val-declaration (seeval
above), these variables may be updated or may be declared without being initialized. Note, however, that it is fine to overwrite aval
name with anotherval
of the same name. -
view@
- unary operator that gives the linear proof (an at-view) of its argument, which should be a variable (var
); seeaddr@
above. -
viewdef
- introduce an alias / name for a concrete view definition; a specialized form ofstadef
[1]; see type. -
viewtypedef
- introduce an alias / name for a concrete view type definition; a specialized form ofstadef
[1]; see type. -
with
- Has several uses. It can add an overloading to a symbol introduced withsymintr
; this tells with what it is overloaded; see overload. Also, it is frequently used for certain kinds of aliasing. For instance, it can give an alias to a linear proof:var y: int with pfy // pfy is an alias of view@(y): int? @ y
-
withtype
- initiate a style of type annotation. This is a still supported “old” keyword inherited from DML. For more, see: withtype keyword on ats.lang.users, withtype.dats sample and JFPmp.pdf.
[1]: The latter may be substituted for the former.
[2]: Algebraic à la SML.
These are not syntactically keywords, but may informally be seen as such. Like keywords, new items can't be created (see Creating new effects?) and thus form a fixed set (may still vary with future ATS versions).