diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 6c692b9b..a9c347e4 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -53,6 +53,18 @@ ASP: - .aspx - .axd +ATS: + type: programming + color: "#1ac620" + primary_extension: .dats + lexer: OCaml + aliases: + - ats2 + extensions: + - .atxt + - .hats + - .sats + ActionScript: type: programming lexer: ActionScript 3 @@ -214,6 +226,7 @@ C: color: "#555" primary_extension: .c extensions: + - .cats - .w C#: diff --git a/samples/ATS/CoYonedaLemma.dats b/samples/ATS/CoYonedaLemma.dats new file mode 100644 index 00000000..aeac8bb1 --- /dev/null +++ b/samples/ATS/CoYonedaLemma.dats @@ -0,0 +1,110 @@ +(* ****** ****** *) +// +// HX-2014-01 +// CoYoneda Lemma: +// +(* ****** ****** *) +// +#include +"share/atspre_staload.hats" +// +(* ****** ****** *) + +staload +"libats/ML/SATS/basis.sats" +staload +"libats/ML/SATS/list0.sats" + +(* ****** ****** *) + +staload _ = "libats/ML/DATS/list0.dats" + +(* ****** ****** *) + +sortdef ftype = type -> type + +(* ****** ****** *) + +infixr (->) ->> +typedef ->> (a:type, b:type) = a - b + +(* ****** ****** *) + +typedef +functor(F:ftype) = + {a,b:type} (a ->> b) ->> F(a) ->> F(b) + +(* ****** ****** *) + +typedef +list0 (a:type) = list0 (a) +extern +val functor_list0 : functor (list0) + +(* ****** ****** *) + +implement +functor_list0{a,b} + (f) = lam xs => list0_map (xs, f) + +(* ****** ****** *) + +datatype +CoYoneda + (F:ftype, r:type) = {a:type} CoYoneda of (a ->> r, F(a)) +// end of [CoYoneda] + +(* ****** ****** *) +// +extern +fun CoYoneda_phi + : {F:ftype}functor(F) -> {r:type} (F (r) ->> CoYoneda (F, r)) +extern +fun CoYoneda_psi + : {F:ftype}functor(F) -> {r:type} (CoYoneda (F, r) ->> F (r)) +// +(* ****** ****** *) + +implement +CoYoneda_phi(ftor) = lam (fx) => CoYoneda (lam x => x, fx) +implement +CoYoneda_psi(ftor) = lam (CoYoneda(f, fx)) => ftor (f) (fx) + +(* ****** ****** *) + +datatype int0 = I of (int) +datatype bool = True | False // boxed boolean + +(* ****** ****** *) +// +fun bool2string + (x:bool): string = +( + case+ x of True() => "True" | False() => "False" +) +// +implement +fprint_val (out, x) = fprint (out, bool2string(x)) +// +(* ****** ****** *) + +fun int2bool (i: int0): bool = + let val+I(i) = i in if i > 0 then True else False end + +(* ****** ****** *) + +val myintlist0 = g0ofg1($list{int0}((I)1, (I)0, (I)1, (I)0, (I)0)) +val myboolist0 = CoYoneda{list0,bool}{int0}(lam (i) => int2bool(i), myintlist0) +val myboolist0 = CoYoneda_psi{list0}(functor_list0){bool}(myboolist0) + +(* ****** ****** *) + +val ((*void*)) = fprintln! (stdout_ref, "myboolist0 = ", myboolist0) + +(* ****** ****** *) + +implement main0 () = () + +(* ****** ****** *) + +(* end of [CoYonedaLemma.dats] *) diff --git a/samples/ATS/DiningPhil2.dats b/samples/ATS/DiningPhil2.dats new file mode 100644 index 00000000..55c39654 --- /dev/null +++ b/samples/ATS/DiningPhil2.dats @@ -0,0 +1,178 @@ +(* ****** ****** *) +// +// HX-2013-11 +// +// Implementing a variant of +// the problem of Dining Philosophers +// +(* ****** ****** *) +// +#include +"share/atspre_define.hats" +#include +"share/atspre_staload.hats" +// +(* ****** ****** *) + +staload +UN = "prelude/SATS/unsafe.sats" + +(* ****** ****** *) + +staload "libc/SATS/stdlib.sats" +staload "libc/SATS/unistd.sats" + +(* ****** ****** *) + +staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" + +(* ****** ****** *) + +staload _ = "libats/DATS/deqarray.dats" +staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats" + +(* ****** ****** *) + +staload "./DiningPhil2.sats" + +(* ****** ****** *) + +implement phil_left (n) = n +implement phil_right (n) = (n+1) \nmod NPHIL + +(* ****** ****** *) +// +extern +fun randsleep (n: intGte(1)): void +// +implement +randsleep (n) = + ignoret (sleep($UN.cast{uInt}(rand() mod n + 1))) +// end of [randsleep] +// +(* ****** ****** *) + +implement +phil_think (n) = +{ +val () = println! ("phil_think(", n, ") starts") +val () = randsleep (6) +val () = println! ("phil_think(", n, ") finishes") +} + +(* ****** ****** *) + +implement +phil_dine (n, lf, rf) = +{ +val () = println! ("phil_dine(", n, ") starts") +val () = randsleep (3) +val () = println! ("phil_dine(", n, ") finishes") +} + +(* ****** ****** *) + +implement +phil_loop (n) = let +// +val () = phil_think (n) +// +val nl = phil_left (n) +val nr = phil_right (n) +// +val ch_lfork = fork_changet (nl) +val ch_rfork = fork_changet (nr) +// +val lf = channel_takeout (ch_lfork) +val () = println! ("phil_loop(", n, ") picks left fork") +// +val () = randsleep (2) // HX: try to actively induce deadlock +// +val rf = channel_takeout (ch_rfork) +val () = println! ("phil_loop(", n, ") picks right fork") +// +val () = phil_dine (n, lf, rf) +// +val ch_forktray = forktray_changet () +val () = channel_insert (ch_forktray, lf) +val () = channel_insert (ch_forktray, rf) +// +in + phil_loop (n) +end // end of [phil_loop] + +(* ****** ****** *) + +implement +cleaner_wash (f) = +{ +val f = fork_get_num (f) +val () = println! ("cleaner_wash(", f, ") starts") +val () = randsleep (1) +val () = println! ("cleaner_wash(", f, ") finishes") +} + +(* ****** ****** *) + +implement +cleaner_return (f) = +{ + val n = fork_get_num (f) + val ch = fork_changet (n) + val () = channel_insert (ch, f) +} + +(* ****** ****** *) + +implement +cleaner_loop () = let +// +val ch = forktray_changet () +val f0 = channel_takeout (ch) +// +val () = cleaner_wash (f0) +val () = cleaner_return (f0) +// +in + cleaner_loop () +end // end of [cleaner_loop] + +(* ****** ****** *) + +dynload "DiningPhil2.sats" +dynload "DiningPhil2_fork.dats" +dynload "DiningPhil2_thread.dats" + +(* ****** ****** *) + +local +// +staload +"{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats" +// +in (* in of [local] *) +// +val () = mythread_create_cloptr (llam () => phil_loop (0)) +val () = mythread_create_cloptr (llam () => phil_loop (1)) +val () = mythread_create_cloptr (llam () => phil_loop (2)) +val () = mythread_create_cloptr (llam () => phil_loop (3)) +val () = mythread_create_cloptr (llam () => phil_loop (4)) +// +val () = mythread_create_cloptr (llam () => cleaner_loop ()) +// +end // end of [local] + +(* ****** ****** *) + +implement +main0 () = +{ +// +val () = println! ("DiningPhil2: starting") +val ((*void*)) = while (true) ignoret (sleep(1)) +// +} (* end of [main0] *) + +(* ****** ****** *) + +(* end of [DiningPhil2.dats] *) diff --git a/samples/ATS/DiningPhil2.sats b/samples/ATS/DiningPhil2.sats new file mode 100644 index 00000000..bc7e96be --- /dev/null +++ b/samples/ATS/DiningPhil2.sats @@ -0,0 +1,71 @@ +(* ****** ****** *) +// +// HX-2013-11 +// +// Implementing a variant of +// the problem of Dining Philosophers +// +(* ****** ****** *) + +#include +"share/atspre_define.hats" + +(* ****** ****** *) + +staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" + +(* ****** ****** *) + +%{# +#define NPHIL 5 +%} // end of [%{#] +#define NPHIL 5 + +(* ****** ****** *) + +typedef nphil = natLt(NPHIL) + +(* ****** ****** *) + +fun phil_left (n: nphil): nphil +fun phil_right (n: nphil): nphil + +(* ****** ****** *) +// +fun phil_loop (n: nphil): void +// +(* ****** ****** *) + +fun cleaner_loop ((*void*)): void + +(* ****** ****** *) + +absvtype fork_vtype = ptr +vtypedef fork = fork_vtype + +(* ****** ****** *) + +fun fork_get_num (!fork): nphil + +(* ****** ****** *) + +fun phil_dine + (n: nphil, lf: !fork, rf: !fork): void +// end of [phil_dine] + +fun phil_think (n: nphil): void + +(* ****** ****** *) + +fun cleaner_wash (f: !fork): void +fun cleaner_return (f: fork): void + +(* ****** ****** *) +// +fun fork_changet (n: nphil): channel(fork) +// +fun forktray_changet ((*void*)): channel(fork) +// +(* ****** ****** *) + +(* end of [DiningPhil2.sats] *) diff --git a/samples/ATS/DiningPhil2_fork.dats b/samples/ATS/DiningPhil2_fork.dats new file mode 100644 index 00000000..a6a8d4df --- /dev/null +++ b/samples/ATS/DiningPhil2_fork.dats @@ -0,0 +1,89 @@ +(* ****** ****** *) +// +// HX-2013-11 +// +// Implementing a variant of +// the problem of Dining Philosophers +// +(* ****** ****** *) +// +#include +"share/atspre_define.hats" +#include +"share/atspre_staload.hats" +// +(* ****** ****** *) + +staload +UN = "prelude/SATS/unsafe.sats" + +(* ****** ****** *) + +staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats" + +(* ****** ****** *) + +staload _ = "libats/DATS/deqarray.dats" +staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats" + +(* ****** ****** *) + +staload "./DiningPhil2.sats" + +(* ****** ****** *) + +datavtype fork = FORK of (nphil) + +(* ****** ****** *) + +assume fork_vtype = fork + +(* ****** ****** *) + +implement +fork_get_num (f) = let val FORK(n) = f in n end + +(* ****** ****** *) + +local + +val +the_forkarray = let +// +typedef t = channel(fork) +// +implement +array_tabulate$fopr + (n) = ch where +{ + val n = $UN.cast{nphil}(n) + val ch = channel_create_exn (i2sz(2)) + val () = channel_insert (ch, FORK (n)) +} +// +in + arrayref_tabulate (i2sz(NPHIL)) +end // end of [val] + +in (* in of [local] *) + +implement fork_changet (n) = the_forkarray[n] + +end // end of [local] + +(* ****** ****** *) + +local + +val the_forktray = + channel_create_exn (i2sz(NPHIL+1)) + +in (* in of [local] *) + +implement forktray_changet () = the_forktray + +end // end of [local] + +(* ****** ****** *) + +(* end of [DiningPhil2_fork.dats] *) diff --git a/samples/ATS/DiningPhil2_thread.dats b/samples/ATS/DiningPhil2_thread.dats new file mode 100644 index 00000000..be73840b --- /dev/null +++ b/samples/ATS/DiningPhil2_thread.dats @@ -0,0 +1,43 @@ +(* ****** ****** *) +// +// HX-2013-11 +// +// Implementing a variant of +// the problem of Dining Philosophers +// +(* ****** ****** *) +// +#include "share/atspre_define.hats" +#include "share/atspre_staload.hats" +// +(* ****** ****** *) + +staload "{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats" + +(* ****** ****** *) + +local +// +#include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread.dats" +// +in (* in of [local] *) +// +// HX: it is intentionally left to be empty +// +end // end of [local] + +(* ****** ****** *) + +local +// +#include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread_posix.dats" +// +in (* in of [local] *) +// +// HX: it is intentionally left to be empty +// +end // end of [local] + +(* ****** ****** *) + +(* end of [DiningPhil2_thread.dats] *) diff --git a/samples/ATS/YonedaLemma.dats b/samples/ATS/YonedaLemma.dats new file mode 100644 index 00000000..cd3c31e6 --- /dev/null +++ b/samples/ATS/YonedaLemma.dats @@ -0,0 +1,178 @@ +(* ****** ****** *) +// +// HX-2014-01 +// Yoneda Lemma: +// The hardest "trivial" theorem :) +// +(* ****** ****** *) +// +#include +"share/atspre_staload.hats" +// +(* ****** ****** *) + +staload +"libats/ML/SATS/basis.sats" +staload +"libats/ML/SATS/list0.sats" +staload +"libats/ML/SATS/option0.sats" + +(* ****** ****** *) + +staload _ = "libats/ML/DATS/list0.dats" +staload _ = "libats/ML/DATS/option0.dats" + +(* ****** ****** *) + +sortdef ftype = type -> type + +(* ****** ****** *) + +infixr (->) ->> +typedef ->> (a:type, b:type) = a - b + +(* ****** ****** *) + +typedef +functor(F:ftype) = + {a,b:type} (a ->> b) ->> F(a) ->> F(b) + +(* ****** ****** *) + +typedef +list0 (a:type) = list0 (a) +extern +val functor_list0 : functor (list0) + +(* ****** ****** *) + +implement +functor_list0{a,b} + (f) = lam xs => list0_map (xs, f) + +(* ****** ****** *) + +typedef +option0 (a:type) = option0 (a) +extern +val functor_option0 : functor (option0) + +(* ****** ****** *) + +implement +functor_option0{a,b} + (f) = lam opt => option0_map (opt, f) + +(* ****** ****** *) + +extern +val functor_homres + : {c:type} functor (lam(r:type) => c ->> r) + +(* ****** ****** *) + +implement +functor_homres{c}{a,b} (f) = lam (r) => lam (x) => f (r(x)) + +(* ****** ****** *) +// +extern +fun Yoneda_phi : {F:ftype}functor(F) -> + {a:type}F(a) ->> ({r:type}(a ->> r) ->> F(r)) +extern +fun Yoneda_psi : {F:ftype}functor(F) -> + {a:type}({r:type}(a ->> r) ->> F(r)) ->> F(a) +// +(* ****** ****** *) +// +implement +Yoneda_phi + (ftor) = lam(fx) => lam (m) => ftor(m)(fx) +// +implement +Yoneda_psi (ftor) = lam(mf) => mf(lam x => x) +// +(* ****** ****** *) + +(* + +(* ****** ****** *) +// +// HX-2014-01-05: +// Another version based on Natural Transformation +// +(* ****** ****** *) + +typedef +natrans(F:ftype, G:ftype) = {x:type} (F(x) ->> G(x)) + +(* ****** ****** *) +// +extern +fun Yoneda_phi_nat : {F:ftype}functor(F) -> + {a:type} F(a) ->> natrans(lam (r:type) => (a ->> r), F) +extern +fun Yoneda_psi_nat : {F:ftype}functor(F) -> + {a:type} natrans(lam (r:type) => (a ->> r), F) ->> F(a) +// +(* ****** ****** *) +// +implement +Yoneda_phi_nat + (ftor) = lam(fx) => lam (m) => ftor(m)(fx) +// +implement +Yoneda_psi_nat (ftor) = lam(mf) => mf(lam x => x) +// +(* ****** ****** *) + +*) + +(* ****** ****** *) + +datatype bool = True | False // boxed boolean + +(* ****** ****** *) +// +fun bool2string + (x:bool): string = +( + case+ x of True() => "True" | False() => "False" +) +// +implement +fprint_val (out, x) = fprint (out, bool2string(x)) +// +(* ****** ****** *) +// +val myboolist0 = + $list_t{bool}(True, False, True, False, False) +val myboolist0 = g0ofg1_list (myboolist0) +// +(* ****** ****** *) +// +extern +val Yoneda_bool_list0 : {r:type} (bool ->> r) ->> list0(r) +// +implement +Yoneda_bool_list0 = + Yoneda_phi(functor_list0){bool}(myboolist0) +// +(* ****** ****** *) +// +val myboolist1 = + Yoneda_psi(functor_list0){bool}(Yoneda_bool_list0) +// +(* ****** ****** *) + +val () = fprintln! (stdout_ref, "myboolist0 = ", myboolist0) +val () = fprintln! (stdout_ref, "myboolist1 = ", myboolist1) + +(* ****** ****** *) + +implement main0 () = () + +(* ****** ****** *) + +(* end of [YonedaLemma.dats] *) diff --git a/samples/ATS/linset.hats b/samples/ATS/linset.hats new file mode 100644 index 00000000..29e44c44 --- /dev/null +++ b/samples/ATS/linset.hats @@ -0,0 +1,187 @@ +(***********************************************************************) +(* *) +(* Applied Type System *) +(* *) +(***********************************************************************) + +(* +** ATS/Postiats - Unleashing the Potential of Types! +** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. +** 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 *) +(* Authoremail: hwxi AT cs DOT bu DOT edu *) +(* Start time: December, 2012 *) + +(* ****** ****** *) +// +// HX: shared by linset_listord (* ordered list *) +// HX: shared by linset_avltree (* AVL-tree-based *) +// +(* ****** ****** *) +// +// HX-2013-02: +// for sets of nonlinear elements +// +absvtype set_vtype (a:t@ype+) = ptr +// +(* ****** ****** *) + +vtypedef set (a:t0p) = set_vtype (a) + +(* ****** ****** *) + +fun{a:t0p} +compare_elt_elt (x1: a, x2: a):<> int + +(* ****** ****** *) + +fun{} linset_nil{a:t0p} ():<> set(a) +fun{} linset_make_nil{a:t0p} ():<> set(a) + +(* ****** ****** *) + +fun{a:t0p} linset_sing (x: a): set(a) +fun{a:t0p} linset_make_sing (x: a): set(a) + +(* ****** ****** *) + +fun{a:t0p} +linset_make_list (xs: List(INV(a))): set(a) + +(* ****** ****** *) + +fun{} +linset_is_nil {a:t0p} (xs: !set(INV(a))):<> bool +fun{} +linset_isnot_nil {a:t0p} (xs: !set(INV(a))):<> bool + +(* ****** ****** *) + +fun{a:t0p} linset_size (!set(INV(a))): size_t + +(* ****** ****** *) + +fun{a:t0p} +linset_is_member (xs: !set(INV(a)), x0: a):<> bool +fun{a:t0p} +linset_isnot_member (xs: !set(INV(a)), x0: a):<> bool + +(* ****** ****** *) + +fun{a:t0p} +linset_copy (!set(INV(a))): set(a) +fun{a:t0p} +linset_free (xs: set(INV(a))): void + +(* ****** ****** *) +// +fun{a:t0p} +linset_insert + (xs: &set(INV(a)) >> _, x0: a): bool +// +(* ****** ****** *) +// +fun{a:t0p} +linset_takeout +( + &set(INV(a)) >> _, a, res: &(a?) >> opt(a, b) +) : #[b:bool] bool(b) // endfun +fun{a:t0p} +linset_takeout_opt (&set(INV(a)) >> _, a): Option_vt(a) +// +(* ****** ****** *) +// +fun{a:t0p} +linset_remove + (xs: &set(INV(a)) >> _, x0: a): bool +// +(* ****** ****** *) +// +// HX: choosing an element in an unspecified manner +// +fun{a:t0p} +linset_choose +( + xs: !set(INV(a)), x: &a? >> opt (a, b) +) : #[b:bool] bool(b) +// +fun{a:t0p} +linset_choose_opt (xs: !set(INV(a))): Option_vt(a) +// +(* ****** ****** *) + +fun{a:t0p} +linset_takeoutmax +( + xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) +) : #[b:bool] bool (b) +fun{a:t0p} +linset_takeoutmax_opt (xs: &set(INV(a)) >> _): Option_vt(a) + +(* ****** ****** *) + +fun{a:t0p} +linset_takeoutmin +( + xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) +) : #[b:bool] bool (b) +fun{a:t0p} +linset_takeoutmin_opt (xs: &set(INV(a)) >> _): Option_vt(a) + +(* ****** ****** *) +// +fun{} +fprint_linset$sep (FILEref): void // ", " +// +fun{a:t0p} +fprint_linset (out: FILEref, xs: !set(INV(a))): void +// +overload fprint with fprint_linset +// +(* ****** ****** *) +// +fun{ +a:t0p}{env:vt0p +} linset_foreach$fwork + (x: a, env: &(env) >> _): void +// +fun{a:t0p} +linset_foreach (set: !set(INV(a))): void +fun{ +a:t0p}{env:vt0p +} linset_foreach_env + (set: !set(INV(a)), env: &(env) >> _): void +// end of [linset_foreach_env] +// +(* ****** ****** *) + +fun{a:t0p} +linset_listize (xs: set(INV(a))): List0_vt (a) + +(* ****** ****** *) + +fun{a:t0p} +linset_listize1 (xs: !set(INV(a))): List0_vt (a) + +(* ****** ****** *) + +(* end of [linset.hats] *) diff --git a/samples/ATS/linset_listord.dats b/samples/ATS/linset_listord.dats new file mode 100644 index 00000000..eb7dd642 --- /dev/null +++ b/samples/ATS/linset_listord.dats @@ -0,0 +1,504 @@ +(***********************************************************************) +(* *) +(* Applied Type System *) +(* *) +(***********************************************************************) + +(* +** ATS/Postiats - Unleashing the Potential of Types! +** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. +** 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 *) +(* Authoremail: hwxi AT cs DOT bu DOT edu *) +(* Start time: February, 2013 *) + +(* ****** ****** *) +// +// HX-2013-08: +// a set is represented as a sorted list in descending order; +// note that descending order is chosen to faciliate set comparison +// +(* ****** ****** *) + +staload +UN = "prelude/SATS/unsafe.sats" + +(* ****** ****** *) + +staload "libats/SATS/linset_listord.sats" + +(* ****** ****** *) + +#include "./SHARE/linset.hats" // code reuse +#include "./SHARE/linset_node.hats" // code reuse + +(* ****** ****** *) + +assume +set_vtype (elt:t@ype) = List0_vt (elt) + +(* ****** ****** *) + +implement{} +linset_nil () = list_vt_nil () +implement{} +linset_make_nil () = list_vt_nil () + +(* ****** ****** *) + +implement +{a}(*tmp*) +linset_sing + (x) = list_vt_cons{a}(x, list_vt_nil) +// end of [linset_sing] +implement{a} +linset_make_sing + (x) = list_vt_cons{a}(x, list_vt_nil) +// end of [linset_make_sing] + +(* ****** ****** *) + +implement{} +linset_is_nil (xs) = list_vt_is_nil (xs) +implement{} +linset_isnot_nil (xs) = list_vt_is_cons (xs) + +(* ****** ****** *) + +implement{a} +linset_size (xs) = + let val n = list_vt_length(xs) in i2sz(n) end +// end of [linset_size] + +(* ****** ****** *) + +implement{a} +linset_is_member + (xs, x0) = let +// +fun aux + {n:nat} .. +( + xs: !list_vt (a, n) +) :<> bool = let +in +// +case+ xs of +| list_vt_cons (x, xs) => let + val sgn = compare_elt_elt (x0, x) in + if sgn > 0 then false else (if sgn < 0 then aux (xs) else true) + end // end of [list_vt_cons] +| list_vt_nil ((*void*)) => false +// +end // end of [aux] +// +in + aux (xs) +end // end of [linset_is_member] + +(* ****** ****** *) + +implement{a} +linset_copy (xs) = list_vt_copy (xs) +implement{a} +linset_free (xs) = list_vt_free (xs) + +(* ****** ****** *) + +implement{a} +linset_insert + (xs, x0) = let +// +fun +mynode_cons + {n:nat} .<>. +( + nx: mynode1 (a), xs: list_vt (a, n) +) : list_vt (a, n+1) = let +// +val xs1 = +$UN.castvwtp0{List1_vt(a)}(nx) +val+@list_vt_cons (_, xs2) = xs1 +prval () = $UN.cast2void (xs2); val () = (xs2 := xs) +// +in + fold@ (xs1); xs1 +end // end of [mynode_cons] +// +fun ins + {n:nat} .. // tail-recursive +( + xs: &list_vt (a, n) >> list_vt (a, n1) +) : #[n1:nat | n <= n1; n1 <= n+1] bool = +( +case+ xs of +| @list_vt_cons + (x, xs1) => let + val sgn = + compare_elt_elt (x0, x) + // end of [val] + in + if sgn > 0 then let + prval () = fold@ (xs) + val nx = mynode_make_elt (x0) + val ((*void*)) = xs := mynode_cons (nx, xs) + in + false + end else if sgn < 0 then let + val ans = ins (xs1) + prval () = fold@ (xs) + in + ans + end else let // [x0] is found + prval () = fold@ (xs) + in + true (* [x0] in [xs] *) + end (* end of [if] *) + end // end of [list_vt_cons] +| list_vt_nil () => let + val nx = mynode_make_elt (x0) + val ((*void*)) = xs := mynode_cons (nx, xs) + in + false + end // end of [list_vt_nil] +) (* end of [ins] *) +// +in + $effmask_all (ins (xs)) +end // end of [linset_insert] + +(* ****** ****** *) + +(* +// +HX-2013-08: +[linset_remove] moved up +// +implement{a} +linset_remove + (xs, x0) = let +// +fun rem + {n:nat} .. // tail-recursive +( + xs: &list_vt (a, n) >> list_vt (a, n1) +) : #[n1:nat | n1 <= n; n <= n1+1] bool = +( +case+ xs of +| @list_vt_cons + (x, xs1) => let + val sgn = + compare_elt_elt (x0, x) + // end of [val] + in + if sgn > 0 then let + prval () = fold@ (xs) + in + false + end else if sgn < 0 then let + val ans = rem (xs1) + prval () = fold@ (xs) + in + ans + end else let // x0 = x + val xs1_ = xs1 + val ((*void*)) = free@{a}{0}(xs) + val () = xs := xs1_ + in + true // [x0] in [xs] + end (* end of [if] *) + end // end of [list_vt_cons] +| list_vt_nil () => false +) (* end of [rem] *) +// +in + $effmask_all (rem (xs)) +end // end of [linset_remove] +*) + +(* ****** ****** *) +(* +** By Brandon Barker +*) +implement +{a}(*tmp*) +linset_choose + (xs, x0) = let +in +// +case+ xs of +| list_vt_cons + (x, xs1) => let + val () = x0 := x + prval () = opt_some{a}(x0) + in + true + end // end of [list_vt_cons] +| list_vt_nil () => let + prval () = opt_none{a}(x0) + in + false + end // end of [list_vt_nil] +// +end // end of [linset_choose] + +(* ****** ****** *) + +implement +{a}{env} +linset_foreach_env (xs, env) = let +// +implement +list_vt_foreach$fwork + (x, env) = linset_foreach$fwork (x, env) +// +in + list_vt_foreach_env (xs, env) +end // end of [linset_foreach_env] + +(* ****** ****** *) + +implement{a} +linset_listize (xs) = xs + +(* ****** ****** *) + +implement{a} +linset_listize1 (xs) = list_vt_copy (xs) + +(* ****** ****** *) +// +// HX: functions for processing mynodes +// +(* ****** ****** *) + +implement{ +} mynode_null{a} () = + $UN.castvwtp0{mynode(a,null)}(the_null_ptr) +// end of [mynode_null] + +(* ****** ****** *) + +implement +{a}(*tmp*) +mynode_make_elt + (x) = let +// +val nx = list_vt_cons{a}{0}(x, _ ) +// +in + $UN.castvwtp0{mynode1(a)}(nx) +end // end of [mynode_make_elt] + +(* ****** ****** *) + +implement{ +} mynode_free + {a}(nx) = () where { +val nx = + $UN.castvwtp0{List1_vt(a)}(nx) +// +val+~list_vt_cons (_, nx2) = nx +// +prval ((*void*)) = $UN.cast2void (nx2) +// +} (* end of [mynode_free] *) + +(* ****** ****** *) + +implement +{a}(*tmp*) +mynode_get_elt + (nx) = (x) where { +// +val nx1 = + $UN.castvwtp1{List1_vt(a)}(nx) +// +val+list_vt_cons (x, _) = nx1 +// +prval ((*void*)) = $UN.cast2void (nx1) +// +} (* end of [mynode_get_elt] *) + +(* ****** ****** *) + +implement +{a}(*tmp*) +mynode_set_elt + {l} (nx, x0) = +{ +// +val nx1 = + $UN.castvwtp1{List1_vt(a)}(nx) +// +val+@list_vt_cons (x, _) = nx1 +// +val () = x := x0 +// +prval () = fold@ (nx1) +prval () = $UN.cast2void (nx1) +// +prval () = __assert (nx) where +{ + extern praxi __assert (nx: !mynode(a?, l) >> mynode (a, l)): void +} (* end of [prval] *) +// +} (* end of [mynode_set_elt] *) + +(* ****** ****** *) + +implement +{a}(*tmp*) +mynode_getfree_elt + (nx) = (x) where { +// +val nx = + $UN.castvwtp0{List1_vt(a)}(nx) +// +val+~list_vt_cons (x, nx2) = nx +// +prval ((*void*)) = $UN.cast2void (nx2) +// +} (* end of [mynode_getfree_elt] *) + +(* ****** ****** *) + +(* +fun{a:t0p} +linset_takeout_ngc + (set: &set(INV(a)) >> _, x0: a): mynode0 (a) +// end of [linset_takeout_ngc] +*) +implement +{a}(*tmp*) +linset_takeout_ngc + (set, x0) = let +// +fun takeout +( + xs: &List0_vt (a) >> _ +) : mynode0(a) = let +in +// +case+ xs of +| @list_vt_cons + (x, xs1) => let + prval pf_x = view@x + prval pf_xs1 = view@xs1 + val sgn = + compare_elt_elt (x0, x) + // end of [val] + in + if sgn > 0 then let + prval () = fold@ (xs) + in + mynode_null{a}((*void*)) + end else if sgn < 0 then let + val res = takeout (xs1) + prval ((*void*)) = fold@ (xs) + in + res + end else let // x0 = x + val xs1_ = xs1 + val res = $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs)) + val () = xs := xs1_ + in + res // [x0] in [xs] + end (* end of [if] *) + end // end of [list_vt_cons] +| list_vt_nil () => mynode_null{a}((*void*)) +// +end (* end of [takeout] *) +// +in + $effmask_all (takeout (set)) +end // end of [linset_takeout_ngc] + +(* ****** ****** *) + +implement +{a}(*tmp*) +linset_takeoutmax_ngc + (xs) = let +in +// +case+ xs of +| @list_vt_cons + (x, xs1) => let + prval pf_x = view@x + prval pf_xs1 = view@xs1 + val xs_ = xs + val () = xs := xs1 + in + $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs_)) + end // end of [list_vt_cons] +| @list_vt_nil () => let + prval () = fold@ (xs) + in + mynode_null{a}((*void*)) + end // end of [list_vt_nil] +// +end // end of [linset_takeoutmax_ngc] + +(* ****** ****** *) + +implement +{a}(*tmp*) +linset_takeoutmin_ngc + (xs) = let +// +fun unsnoc + {n:pos} .. +( + xs: &list_vt (a, n) >> list_vt (a, n-1) +) : mynode1 (a) = let +// +val+@list_vt_cons (x, xs1) = xs +// +prval pf_x = view@x and pf_xs1 = view@xs1 +// +in +// +case+ xs1 of +| list_vt_cons _ => + let val res = unsnoc(xs1) in fold@xs; res end + // end of [list_vt_cons] +| list_vt_nil () => let + val xs_ = xs + val () = xs := list_vt_nil{a}() + in + $UN.castvwtp0{mynode1(a)}((pf_x, pf_xs1 | xs_)) + end // end of [list_vt_nil] +// +end // end of [unsnoc] +// +in +// +case+ xs of +| list_vt_cons _ => unsnoc (xs) +| list_vt_nil () => mynode_null{a}((*void*)) +// +end // end of [linset_takeoutmin_ngc] + +(* ****** ****** *) + +(* end of [linset_listord.dats] *) diff --git a/samples/ATS/linset_listord.sats b/samples/ATS/linset_listord.sats new file mode 100644 index 00000000..468a534f --- /dev/null +++ b/samples/ATS/linset_listord.sats @@ -0,0 +1,51 @@ +(***********************************************************************) +(* *) +(* Applied Type System *) +(* *) +(***********************************************************************) + +(* +** ATS/Postiats - Unleashing the Potential of Types! +** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. +** 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 +// Authoremail: hwxiATcsDOTbuDOTedu +// Time: October, 2010 +// +(* ****** ****** *) + +#define ATS_PACKNAME "ATSLIB.libats.linset_listord" +#define ATS_STALOADFLAG 0 // no static loading at run-time + +(* ****** ****** *) + +#include "./SHARE/linset.hats" +#include "./SHARE/linset_node.hats" + +(* ****** ****** *) + +castfn +linset2list {a:t0p} (xs: set (INV(a))):<> List0_vt (a) + +(* ****** ****** *) + +(* end of [linset_listord.sats] *) diff --git a/samples/ATS/main.atxt b/samples/ATS/main.atxt new file mode 100644 index 00000000..3bba35f0 --- /dev/null +++ b/samples/ATS/main.atxt @@ -0,0 +1,215 @@ +%{ +#include "./../ATEXT/atextfun.hats" +%} + + + + + + +EFFECTIVATS-DiningPhil2 +#patscode_style() + + + + +

+Effective ATS: Dining Philosophers +

+ +In this article, I present an implementation of a slight variant of the +famous problem of 5-Dining-Philosophers by Dijkstra that makes simple but +convincing use of linear types. + +

+The Original Problem +

+ +There are five philosophers sitting around a table and there are also 5 +forks placed on the table such that each fork is located between the left +hand of a philosopher and the right hand of another philosopher. Each +philosopher does the following routine repeatedly: thinking and dining. In +order to dine, a philosopher needs to first acquire two forks: one located +on his left-hand side and the other on his right-hand side. After +finishing dining, a philosopher puts the two acquired forks onto the table: +one on his left-hand side and the other on his right-hand side. + +

+A Variant of the Original Problem +

+ +The following twist is added to the original version: + +

+ +After a fork is used, it becomes a "dirty" fork and needs to be put in a +tray for dirty forks. There is a cleaner who cleans dirty forks and then +puts them back on the table. + +

+Channels for Communication +

+ +A channel is just a shared queue of fixed capacity. The following two +functions are for inserting an element into and taking an element out of a +given channel: + +
+#pats2xhtml_sats("\
+fun{a:vt0p} channel_insert (channel (a), a): void
+fun{a:vt0p} channel_takeout (chan: channel (a)): (a) 
+")
+ +If [channel_insert] is called on a channel that is full, then the caller is +blocked until an element is taken out of the channel. If [channel_takeout] +is called on a channel that is empty, then the caller is blocked until an +element is inserted into the channel. + +

+A Channel for Each Fork +

+ +Forks are resources given a linear type. Each fork is initially stored in a +channel, which can be obtained by calling the following function: + +
+#pats2xhtml_sats("\
+fun fork_changet (n: nphil): channel(fork)
+")
+ +where the type [nphil] is defined to be [natLt(5)] (for natural numbers +less than 5). The channels for storing forks are chosen to be of capacity +2. The reason that channels of capacity 2 are chosen to store at most one +element (in each of them) is to guarantee that these channels can never be +full (so that there is no attempt made to send signals to awake callers +supposedly being blocked due to channels being full). + + +

+A Channel for the Fork Tray +

+ +A tray for storing "dirty" forks is also a channel, which can be obtained +by calling the following function: + +
+#pats2xhtml_sats("\
+fun forktray_changet ((*void*)): channel(fork)
+")
+ +The capacity chosen for the channel is 6 (instead of 5) so that it can +never become full (as there are only 5 forks in total). + +

+Philosopher Loop +

+ +Each philosopher is implemented as a loop: + +
+#pats2xhtml_dats('\
+implement
+phil_loop (n) = let
+//
+val () = phil_think (n)
+//
+val nl = phil_left (n) // = n
+val nr = phil_right (n) // = (n+1) % 5
+//
+val ch_lfork = fork_changet (nl)
+val ch_rfork = fork_changet (nr)
+//
+val lf = channel_takeout (ch_lfork)
+val () = println! ("phil_loop(", n, ") picks left fork")
+//
+val () = randsleep (2) // sleep up to 2 seconds
+//
+val rf = channel_takeout (ch_rfork)
+val () = println! ("phil_loop(", n, ") picks right fork")
+//
+val () = phil_dine (n, lf, rf)
+//
+val ch_forktray = forktray_changet ()
+val () = channel_insert (ch_forktray, lf) // left fork to dirty tray
+val () = channel_insert (ch_forktray, rf) // right fork to dirty tray
+//
+in
+  phil_loop (n)
+end // end of [phil_loop]
+')
+ +It should be straighforward to follow the code for [phil_loop]. + +

+Fork Cleaner Loop +

+ +A cleaner is implemented as a loop: + +
+#pats2xhtml_dats('\
+implement
+cleaner_loop () = let
+//
+val ch = forktray_changet ()
+val f0 = channel_takeout (ch) // [f0] is dirty
+//
+val () = cleaner_wash (f0) // washes dirty [f0]
+val () = cleaner_return (f0) // puts back cleaned [f0]
+//
+in
+  cleaner_loop ()
+end // end of [cleaner_loop]
+')
+ +The function [cleaner_return] first finds out the number of a given fork +and then uses the number to locate the channel for storing the fork. Its +actual implementation is given as follows: + +
+#pats2xhtml_dats('\
+implement
+cleaner_return (f) =
+{
+  val n = fork_get_num (f)
+  val ch = fork_changet (n)
+  val () = channel_insert (ch, f)
+}
+')
+ +It should now be straighforward to follow the code for [cleaner_loop]. + +

+Testing +

+ +The entire code of this implementation is stored in the following files: + +
+DiningPhil2.sats
+DiningPhil2.dats
+DiningPhil2_fork.dats
+DiningPhil2_thread.dats
+
+ +There is also a Makefile available for compiling the ATS source code into +an excutable for testing. One should be able to encounter a deadlock after +running the simulation for a while. + +
+ +This article is written by Hongwei Xi. + + + + +%{ +implement main () = fprint_filsub (stdout_ref, "main_atxt.txt") +%} diff --git a/samples/C/dynarray.cats b/samples/C/dynarray.cats new file mode 100644 index 00000000..95ee54ba --- /dev/null +++ b/samples/C/dynarray.cats @@ -0,0 +1,56 @@ +/* ******************************************************************* */ +/* */ +/* Applied Type System */ +/* */ +/* ******************************************************************* */ + +/* +** ATS/Postiats - Unleashing the Potential of Types! +** Copyright (C) 2011-20?? Hongwei Xi, ATS Trustful Software, Inc. +** 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 *) +(* Authoremail: hwxi AT cs DOT bu DOT edu *) +(* Start time: March, 2013 *) +*/ + +/* ****** ****** */ + +#ifndef ATSHOME_LIBATS_DYNARRAY_CATS +#define ATSHOME_LIBATS_DYNARRAY_CATS + +/* ****** ****** */ + +#include + +/* ****** ****** */ + +#define atslib_dynarray_memcpy memcpy +#define atslib_dynarray_memmove memmove + +/* ****** ****** */ + +#endif // ifndef ATSHOME_LIBATS_DYNARRAY_CATS + +/* ****** ****** */ + +/* end of [dynarray.cats] */ diff --git a/samples/C/readline.cats b/samples/C/readline.cats new file mode 100644 index 00000000..3fad326b --- /dev/null +++ b/samples/C/readline.cats @@ -0,0 +1,47 @@ +/* +** API in ATS for GNU-readline +*/ + +/* ****** ****** */ + +/* +** Permission to use, copy, modify, and distribute this software for any +** purpose with or without fee is hereby granted, provided that the above +** copyright notice and this permission notice appear in all copies. +** +** THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +** WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +** MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +** ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +** WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +** ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +** OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +*/ + +/* ****** ****** */ + +#ifndef READLINE_READLINE_CATS +#define READLINE_READLINE_CATS + +/* ****** ****** */ + +#include + +/* ****** ****** */ +// +#define \ +atscntrb_readline_rl_library_version() ((char*)rl_library_version) +// +#define atscntrb_readline_rl_readline_version() (rl_readline_version) +// +/* ****** ****** */ + +#define atscntrb_readline_readline readline + +/* ****** ****** */ + +#endif // ifndef READLINE_READLINE_CATS + +/* ****** ****** */ + +/* end of [readline.cats] */