NOTES

######
#
# HX:
#
# for myself to remember some significant features
# added into ATS2:
#
######

(*
** HX-2011-summer:
**
** Say that we have the following declared templates:
**
extern
fun
{a:t@ype}
{b,c:t@ype}
foo (x: a, y: b, z: c): void
**
** This is a style that is already supported in ATS:
**
implement{a}{b,c} foo (x, y, z) = ()
**
** This is a new style that is not available in ATS:
**
implement(b,c) foo<int><b,c> (x, y, z) = ()
**
** This style is added into ATS2 to support partial
** template instantiation.
**
*)

######

(*
** HX-2012-05:
**
** In ATS2, pattern matching involving linear types is
** re-designed. For instance, computing the length of a
** linear list can now be implemented as follows:
**
fun{a:viewt@ype}
length {n:int}
  (xs: !list_vt (a, n)): int (n) =
  case+ xs of
  | list_vt_cons (x, xs) => 1 + length (xs)
  | list_vt_nil () => 0
// end of [length]
**
** As another example, reverse-append on linear lists
** can now be implemented as follows:
//
fun{a:viewt@ype}
revapp {m,n:nat} .<m>. (
  xs: list_vt (a, m), ys: list_vt (a, n)
) :<> list_vt (a, m+n) =
  case xs of
  | @list_vt_cons
      (_, xs1) => let
      val xs1_ = xs1
      val () = xs1 := ys; prval () = fold@ (xs)
    in
      revapp (xs1_, xs)
    end
  | ~list_vt_nil () => ys
(* end of [revapp] *)
//
**
*)

######

(*
**
** HX-2012-05:
**
** Say we have a type
**
** absviewt@ype T (l:addr)
**
** Let T0 be defined as follows:
** 
** typedef T0 = [l:addr] T(l)
**
** The difference between the following two function decs
** is somewhat subtle:
**
** fun f1 (x: &T0): void
** fun f2 (x: &T0 >> T0): void
**
** The dec for function [f1] is essentially equivalent to
** the following one:
**
** fun f1 {l:addr} (x: &T(l) >> T(l)): void
**
** So if [f1] is called on a left-value of the type T(L)
** for some L, then the type of the left-value is still T(L)
** after the call. On the other hand, if [f2] is called,
** the type of the left-value may be T(L') for some L' != L.
**
*)

######

(*
**
** HX-2012-05-24:
**
** for synthesizing the second arg of S1Etrans:
** T  >> _   stands for T >> T
** T  >> _?  stands for T >> T?
** T  >> _?! stands for T >> T?!
** T? >> _   stands for T? >> T
**
*)

######

(*
**
** HX-2012:
**
** The skeleton of a type is computed by erasing all
** quatifiers and predicative indexes; type skeletons
** are primarily employed to support overloading.
**
** The size of each boxed type equals that of a pointer.
** The size of each unboxed type is only determined by
** its skeleton. In other words, predicative indexes are
** ignored for the purpose of comparing type sizes.
**
*)

######

(*
**
** HX-2012-05:
**
** Dynamic expressions like A[i,j][k] are referred to as
** arrsub-expressions in ATS; for such expressions, grouping
** is entirely cosmetic; for example, both A[i,j][k] and
** A[i][j,k] are the same, and they are the same as A[i,j,k].
**
*)

######

(*
**
** HX-2012-06-01:
**
** Introducing the following syntax to support typechecking:
**
** lam {} => ...
**
** 'lam {}' means an indefinite number of static lam-abstractions.
**
** Actually, the first of the following two lines is the same as
** the second of them:
**
** lam (...) => ...
** lam {} => lam (...) => ...
**
** Hence, 'lam {}' is only needed in a case where its body is not
** a dynamic lambda-abstraction. A good example involving 'lam {}'
** can be found in doc/EXAMPLE/ATSLF/SMI.dats.
**
*)

######
#
# The following was in the old README
#
######

Project Title: ATS/Postiats

Project Description:
Another Implementation of ATS!

######

//
// HX-2011-03-07: syntax design:
//

&? >> T for &T? >> T
This can be &set(T)

&T >> ?! for &T >> T?! 
This can be &get(T)

&T >> ? for &T >> T?
This can be &clr(T)

######
//
// HX-2011-03-13
//
Optmizing pattern matching compilation

######
//
// HX-2011-03-14
//
Each type should be given a generic name as well as a specific name;
the former for generic template instantiation and the latter for specific
template implementation.

######
//
// HX-2011-03-16
//
Handling read-only access.

fun f (x: &READ(Int)): bool

######
//
// HX-2011-03-20
//
Some kind of sort inferencing (for impredicative sorts).

######
//
// HX-2011-03-21
//
Supporting user-defined effects

######
//
// HX-2011-03-30
//
Supporting invariant types:

fun{a1,a2:t@ype} f (x: INV(a1), y: INV(a2)): (a1, a2)

######
//
// HX-2011-04-15
//
Macro support for patterns.
(*
HX-2011-04-27:
there is now support for functional C-like macros. For instance,
the following declaration is now available, which I plan to turn
into limited macro support for patterns:
//
#define list_sing (x) list_cons (x, list_nil ())
//
*)

######
//
// HX-2011-08
//
fold/unfold are proof functions
encode/decode are casting functions (castfn)

ifbrk $test then $exp

for

if $test then ($exp; break)

ifcnt $test then $exp

for

if $test then ($exp; continue)

######
//
// HX-2011-08
//

logging errors of lib functions of the names *_exn?

######
//
// HX-2011-08
//

mutability: 

structbox = '{
  name= string, width= !int, height= !int
} // it is just like a ref!

######
//
// HX-2011-09
//

A flag for allocation-only GCATS.

######

From matthias_berndt@gmx.de Sun Sep  4 16:50:34 2011
Date: Sun, 4 Sep 2011 22:50:19 +0200
From: Matthias Berndt <matthias_berndt@gmx.de>
To:  <ats-lang-users@lists.sourceforge.net>
Subject: Re: [ats-lang-users] Error code checking with linear types

Hi Hongwei, 

> >>Wouldn't it be possible to just DWIM in that case? For example, an
> >>expression like
> >>case x of
> >>
> >>  | (a | b) => ...
> >>  | (c | d) => ...
> >>
> >>could automatically be transformed into something like
> >>let val+ (x1 | x2) = x in
> >>
> >>  case x2 of
> >>  
> >>  | b => let prval a = x1 in ... end
> >>  | d => let prval c = x1 in ... end
> 
> When [b] matches [x2], [a] may not be the only pattern that matches x1;
> if it is the only one, then yes.
Yes, this would be a shorthand for the (common?) case where the fact that 
x2 matches b also implies that x1 matches a. For all other cases, one needs 
to resort to the solution we have now. 

> By the way, what does 'DWIM' stand for?
"Do What I Mean".

######
//
// HX: this form of pseudo abstract type can also be useful
//
abst@ype
E (a:t@ype, x:elt) = !a
assume E (a:t@ype, x:elt) = top // ignored

######
//
// HX-2011-10-01: supporting offsetof?
//
######

######
//
// HX-2011-10-18: proof management?
//

#proof (?@l)
#proof (array_v(?, ?, l))
#typeof (exp)

let

prfun tyeq {a:t@ype} (x: INV(a)): void
prfun tyeq_vt {a:t@ype} (x: !INV(a)): void

prval pf = #proof(?@l)
prval pf = #proof(free_v_gc(?, l))
stavar i: int and j: int
prval () = tyeq {int(i)} (x+y)
val x = ptrget (pf | p)

in

end // end of [

######
//
// HX-2012-02-08: caseof-expressions
//
fun fact
  (x: int): int =
  caseof x > 0 => x * f (x-1) | (*else*) => 1
// end of [fact]

######

explicit wthtype syntax:

(int? >> opt (int i, b)) -> #[i:nat;b:bool] bool (b)

######

A convenient syntax for handling folding/unfolding:

fun{
a:viewt@ype
} list_vt_length
  (xs: !list_vt (a, n)): int n =
  case+ xs of
  | list_vt_cons (x, xs) => 1 + list_vt_length (xs)
  | list_vt_nil () => 0
// end of [list_vt_length]

fun{
a:viewt@ype
} list_vt_append
  {m,n:int | m > 0}
(
  xs: !list_vt (a, m) >> list_vt (a, m+n)
, ys: list_vt (a, n)
) : void = let
  val @list_vt_cons (_, xs1) = xs
in
  case+ xs1 of
  | list_cons _ => let
      val () = list_vt_append (xs1, ys) in fold@ (xs)
    end // end of [list_cons]
  | ~list_vt_nil () => xs1 := ys
end // end of [list_vt_append]

######

HX-2013-06-20:

Is it a good practice to allow the use of wildcards (_ or ...)
for discarding resources:

Pro: Very easy to use
Con: Maybe it is too easy to allow unintentional leak of resources 

###### end of [NOTES] ######