mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Merge pull request #911 from bbarker/master
Added ATS to language list and several samples (try #2).
This commit is contained in:
Ted Nyman
110
samples/ATS/CoYonedaLemma.dats
Normal file
110
samples/ATS/CoYonedaLemma.dats
Normal file
@@ -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 -<cloref1> 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<a><b> (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<bool> (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] *)
|
||||
178
samples/ATS/DiningPhil2.dats
Normal file
178
samples/ATS/DiningPhil2.dats
Normal file
@@ -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] *)
|
||||
71
samples/ATS/DiningPhil2.sats
Normal file
71
samples/ATS/DiningPhil2.sats
Normal file
@@ -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] *)
|
||||
89
samples/ATS/DiningPhil2_fork.dats
Normal file
89
samples/ATS/DiningPhil2_fork.dats
Normal file
@@ -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<t>
|
||||
(n) = ch where
|
||||
{
|
||||
val n = $UN.cast{nphil}(n)
|
||||
val ch = channel_create_exn<fork> (i2sz(2))
|
||||
val () = channel_insert (ch, FORK (n))
|
||||
}
|
||||
//
|
||||
in
|
||||
arrayref_tabulate<t> (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<fork> (i2sz(NPHIL+1))
|
||||
|
||||
in (* in of [local] *)
|
||||
|
||||
implement forktray_changet () = the_forktray
|
||||
|
||||
end // end of [local]
|
||||
|
||||
(* ****** ****** *)
|
||||
|
||||
(* end of [DiningPhil2_fork.dats] *)
|
||||
43
samples/ATS/DiningPhil2_thread.dats
Normal file
43
samples/ATS/DiningPhil2_thread.dats
Normal file
@@ -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] *)
|
||||
178
samples/ATS/YonedaLemma.dats
Normal file
178
samples/ATS/YonedaLemma.dats
Normal file
@@ -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 -<cloref1> 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<a><b> (xs, f)
|
||||
|
||||
(* ****** ****** *)
|
||||
|
||||
typedef
|
||||
option0 (a:type) = option0 (a)
|
||||
extern
|
||||
val functor_option0 : functor (option0)
|
||||
|
||||
(* ****** ****** *)
|
||||
|
||||
implement
|
||||
functor_option0{a,b}
|
||||
(f) = lam opt => option0_map<a><b> (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<bool> (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] *)
|
||||
187
samples/ATS/linset.hats
Normal file
187
samples/ATS/linset.hats
Normal file
@@ -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):<!wrt> set(a)
|
||||
fun{a:t0p} linset_make_sing (x: a):<!wrt> set(a)
|
||||
|
||||
(* ****** ****** *)
|
||||
|
||||
fun{a:t0p}
|
||||
linset_make_list (xs: List(INV(a))):<!wrt> 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))):<!wrt> set(a)
|
||||
fun{a:t0p}
|
||||
linset_free (xs: set(INV(a))):<!wrt> void
|
||||
|
||||
(* ****** ****** *)
|
||||
//
|
||||
fun{a:t0p}
|
||||
linset_insert
|
||||
(xs: &set(INV(a)) >> _, x0: a):<!wrt> bool
|
||||
//
|
||||
(* ****** ****** *)
|
||||
//
|
||||
fun{a:t0p}
|
||||
linset_takeout
|
||||
(
|
||||
&set(INV(a)) >> _, a, res: &(a?) >> opt(a, b)
|
||||
) :<!wrt> #[b:bool] bool(b) // endfun
|
||||
fun{a:t0p}
|
||||
linset_takeout_opt (&set(INV(a)) >> _, a):<!wrt> Option_vt(a)
|
||||
//
|
||||
(* ****** ****** *)
|
||||
//
|
||||
fun{a:t0p}
|
||||
linset_remove
|
||||
(xs: &set(INV(a)) >> _, x0: a):<!wrt> bool
|
||||
//
|
||||
(* ****** ****** *)
|
||||
//
|
||||
// HX: choosing an element in an unspecified manner
|
||||
//
|
||||
fun{a:t0p}
|
||||
linset_choose
|
||||
(
|
||||
xs: !set(INV(a)), x: &a? >> opt (a, b)
|
||||
) :<!wrt> #[b:bool] bool(b)
|
||||
//
|
||||
fun{a:t0p}
|
||||
linset_choose_opt (xs: !set(INV(a))):<!wrt> Option_vt(a)
|
||||
//
|
||||
(* ****** ****** *)
|
||||
|
||||
fun{a:t0p}
|
||||
linset_takeoutmax
|
||||
(
|
||||
xs: &set(INV(a)) >> _, res: &a? >> opt(a, b)
|
||||
) :<!wrt> #[b:bool] bool (b)
|
||||
fun{a:t0p}
|
||||
linset_takeoutmax_opt (xs: &set(INV(a)) >> _):<!wrt> Option_vt(a)
|
||||
|
||||
(* ****** ****** *)
|
||||
|
||||
fun{a:t0p}
|
||||
linset_takeoutmin
|
||||
(
|
||||
xs: &set(INV(a)) >> _, res: &a? >> opt(a, b)
|
||||
) :<!wrt> #[b:bool] bool (b)
|
||||
fun{a:t0p}
|
||||
linset_takeoutmin_opt (xs: &set(INV(a)) >> _):<!wrt> 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] *)
|
||||
504
samples/ATS/linset_listord.dats
Normal file
504
samples/ATS/linset_listord.dats
Normal file
@@ -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} .<n>.
|
||||
(
|
||||
xs: !list_vt (a, n)
|
||||
) :<> bool = let
|
||||
in
|
||||
//
|
||||
case+ xs of
|
||||
| list_vt_cons (x, xs) => let
|
||||
val sgn = compare_elt_elt<a> (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<a> (xs)
|
||||
implement{a}
|
||||
linset_free (xs) = list_vt_free<a> (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} .<n>. // 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<a> (x0, x)
|
||||
// end of [val]
|
||||
in
|
||||
if sgn > 0 then let
|
||||
prval () = fold@ (xs)
|
||||
val nx = mynode_make_elt<a> (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<a> (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} .<n>. // 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<a> (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<a><env>
|
||||
(x, env) = linset_foreach$fwork<a><env> (x, env)
|
||||
//
|
||||
in
|
||||
list_vt_foreach_env<a><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):<!wrt> 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<a> (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} .<n>.
|
||||
(
|
||||
xs: &list_vt (a, n) >> list_vt (a, n-1)
|
||||
) :<!wrt> 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] *)
|
||||
51
samples/ATS/linset_listord.sats
Normal file
51
samples/ATS/linset_listord.sats
Normal file
@@ -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] *)
|
||||
215
samples/ATS/main.atxt
Normal file
215
samples/ATS/main.atxt
Normal file
@@ -0,0 +1,215 @@
|
||||
%{
|
||||
#include "./../ATEXT/atextfun.hats"
|
||||
%}
|
||||
|
||||
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
|
||||
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
|
||||
<html xmlns="http://www.w3.org/1999/xhtml">
|
||||
|
||||
<head>
|
||||
<meta http-equiv="content-type" content="text/html; charset=UTF-8" />
|
||||
<title>EFFECTIVATS-DiningPhil2</title>
|
||||
#patscode_style()
|
||||
</head>
|
||||
|
||||
<body>
|
||||
|
||||
<h1>
|
||||
Effective ATS: Dining Philosophers
|
||||
</h1>
|
||||
|
||||
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.
|
||||
|
||||
<h2>
|
||||
The Original Problem
|
||||
</h2>
|
||||
|
||||
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.
|
||||
|
||||
<h2>
|
||||
A Variant of the Original Problem
|
||||
</h2>
|
||||
|
||||
The following twist is added to the original version:
|
||||
|
||||
<p>
|
||||
|
||||
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.
|
||||
|
||||
<h2>
|
||||
Channels for Communication
|
||||
</h2>
|
||||
|
||||
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:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#pats2xhtml_sats("\
|
||||
fun{a:vt0p} channel_insert (channel (a), a): void
|
||||
fun{a:vt0p} channel_takeout (chan: channel (a)): (a)
|
||||
")</pre>
|
||||
|
||||
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.
|
||||
|
||||
<h2>
|
||||
A Channel for Each Fork
|
||||
</h2>
|
||||
|
||||
Forks are resources given a linear type. Each fork is initially stored in a
|
||||
channel, which can be obtained by calling the following function:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#pats2xhtml_sats("\
|
||||
fun fork_changet (n: nphil): channel(fork)
|
||||
")</pre>
|
||||
|
||||
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).
|
||||
|
||||
|
||||
<h2>
|
||||
A Channel for the Fork Tray
|
||||
</h2>
|
||||
|
||||
A tray for storing "dirty" forks is also a channel, which can be obtained
|
||||
by calling the following function:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#pats2xhtml_sats("\
|
||||
fun forktray_changet ((*void*)): channel(fork)
|
||||
")</pre>
|
||||
|
||||
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).
|
||||
|
||||
<h2>
|
||||
Philosopher Loop
|
||||
</h2>
|
||||
|
||||
Each philosopher is implemented as a loop:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#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]
|
||||
')</pre>
|
||||
|
||||
It should be straighforward to follow the code for [phil_loop].
|
||||
|
||||
<h2>
|
||||
Fork Cleaner Loop
|
||||
</h2>
|
||||
|
||||
A cleaner is implemented as a loop:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#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]
|
||||
')</pre>
|
||||
|
||||
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:
|
||||
|
||||
<pre
|
||||
class="patsyntax">
|
||||
#pats2xhtml_dats('\
|
||||
implement
|
||||
cleaner_return (f) =
|
||||
{
|
||||
val n = fork_get_num (f)
|
||||
val ch = fork_changet (n)
|
||||
val () = channel_insert (ch, f)
|
||||
}
|
||||
')</pre>
|
||||
|
||||
It should now be straighforward to follow the code for [cleaner_loop].
|
||||
|
||||
<h2>
|
||||
Testing
|
||||
</h2>
|
||||
|
||||
The entire code of this implementation is stored in the following files:
|
||||
|
||||
<pre>
|
||||
DiningPhil2.sats
|
||||
DiningPhil2.dats
|
||||
DiningPhil2_fork.dats
|
||||
DiningPhil2_thread.dats
|
||||
</pre>
|
||||
|
||||
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.
|
||||
|
||||
<hr size="2">
|
||||
|
||||
This article is written by <a href="http://www.cs.bu.edu/~hwxi/">Hongwei Xi</a>.
|
||||
|
||||
</body>
|
||||
</html>
|
||||
|
||||
%{
|
||||
implement main () = fprint_filsub (stdout_ref, "main_atxt.txt")
|
||||
%}
|
||||
56
samples/C/dynarray.cats
Normal file
56
samples/C/dynarray.cats
Normal file
@@ -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 <string.h>
|
||||
|
||||
/* ****** ****** */
|
||||
|
||||
#define atslib_dynarray_memcpy memcpy
|
||||
#define atslib_dynarray_memmove memmove
|
||||
|
||||
/* ****** ****** */
|
||||
|
||||
#endif // ifndef ATSHOME_LIBATS_DYNARRAY_CATS
|
||||
|
||||
/* ****** ****** */
|
||||
|
||||
/* end of [dynarray.cats] */
|
||||
47
samples/C/readline.cats
Normal file
47
samples/C/readline.cats
Normal file
@@ -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 <readline/readline.h>
|
||||
|
||||
/* ****** ****** */
|
||||
//
|
||||
#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] */
|
||||
Reference in New Issue
Block a user