mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
adding more varied examples, including an .atxt file
This commit is contained in:
Brandon
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] *)
|
||||||
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")
|
||||||
|
%}
|
||||||
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