From 98518e5c8c952d4e601b0a5d19abb98e7e4cd7af Mon Sep 17 00:00:00 2001 From: Steinway Wu Date: Fri, 30 Jan 2015 12:52:38 -0500 Subject: [PATCH 1/5] add ats mode from sublime package --- .gitmodules | 6 ++++++ grammars.yml | 2 ++ lib/linguist/languages.yml | 3 +-- vendor/grammars/ats.sublime | 1 + 4 files changed, 10 insertions(+), 2 deletions(-) create mode 160000 vendor/grammars/ats.sublime diff --git a/.gitmodules b/.gitmodules index 1816e097..3c729ffa 100644 --- a/.gitmodules +++ b/.gitmodules @@ -555,3 +555,9 @@ [submodule "vendor/grammars/liquid.tmbundle"] path = vendor/grammars/liquid.tmbundle url = https://github.com/bastilian/validcode-textmate-bundles +[submodule "ats-mode-sublimetext"] + path = ats-mode-sublimetext + url = https://github.com/steinwaywhw/ats-mode-sublimetext +[submodule "vendor/grammars/ats.sublime"] + path = vendor/grammars/ats.sublime + url = https://github.com/steinwaywhw/ats-mode-sublimetext diff --git a/grammars.yml b/grammars.yml index 9c9d7e35..e06ddde6 100644 --- a/grammars.yml +++ b/grammars.yml @@ -128,6 +128,8 @@ vendor/grammars/assembly.tmbundle: vendor/grammars/atom-salt: - source.python.salt - source.yaml.salt +vendor/grammars/ats.sublime: +- source.ats vendor/grammars/autoitv3-tmbundle: - source.autoit.3 vendor/grammars/awk-sublime: diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index f02c0c3c..050b9a26 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -82,10 +82,9 @@ ATS: - ats2 extensions: - .dats - - .atxt - .hats - .sats - tm_scope: source.ocaml + tm_scope: source.ats ace_mode: ocaml ActionScript: diff --git a/vendor/grammars/ats.sublime b/vendor/grammars/ats.sublime new file mode 160000 index 00000000..64f1abc7 --- /dev/null +++ b/vendor/grammars/ats.sublime @@ -0,0 +1 @@ +Subproject commit 64f1abc71df139b1050ed68f2487dde7fe69829d From c80d085e335d711faa632ab4a3c35b2cae43fc5a Mon Sep 17 00:00:00 2001 From: Steinway Wu Date: Fri, 30 Jan 2015 12:56:17 -0500 Subject: [PATCH 2/5] revise git module --- .gitmodules | 3 --- 1 file changed, 3 deletions(-) diff --git a/.gitmodules b/.gitmodules index 3c729ffa..5905dd62 100644 --- a/.gitmodules +++ b/.gitmodules @@ -555,9 +555,6 @@ [submodule "vendor/grammars/liquid.tmbundle"] path = vendor/grammars/liquid.tmbundle url = https://github.com/bastilian/validcode-textmate-bundles -[submodule "ats-mode-sublimetext"] - path = ats-mode-sublimetext - url = https://github.com/steinwaywhw/ats-mode-sublimetext [submodule "vendor/grammars/ats.sublime"] path = vendor/grammars/ats.sublime url = https://github.com/steinwaywhw/ats-mode-sublimetext From 7d9a47b7c3bad2478f87e7556d2e5f64a92b7799 Mon Sep 17 00:00:00 2001 From: Steinway Wu Date: Fri, 30 Jan 2015 13:02:37 -0500 Subject: [PATCH 3/5] remove atxt support --- samples/ATS/main.atxt | 215 ------------------------------------------ 1 file changed, 215 deletions(-) delete mode 100644 samples/ATS/main.atxt diff --git a/samples/ATS/main.atxt b/samples/ATS/main.atxt deleted file mode 100644 index 3bba35f0..00000000 --- a/samples/ATS/main.atxt +++ /dev/null @@ -1,215 +0,0 @@ -%{ -#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") -%} From 513347911e17908e8b670584f00b7e9cae68bddc Mon Sep 17 00:00:00 2001 From: Steinway Wu Date: Fri, 30 Jan 2015 13:25:22 -0500 Subject: [PATCH 4/5] update ats grammar to the latest commits --- vendor/grammars/ats.sublime | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/grammars/ats.sublime b/vendor/grammars/ats.sublime index 64f1abc7..e42cbf65 160000 --- a/vendor/grammars/ats.sublime +++ b/vendor/grammars/ats.sublime @@ -1 +1 @@ -Subproject commit 64f1abc71df139b1050ed68f2487dde7fe69829d +Subproject commit e42cbf651152f4f3ada7502cf8002aa8729e147f From da7b3182e8d5cb26d0a382b9cb32f219da65c9ad Mon Sep 17 00:00:00 2001 From: Steinway Wu Date: Sat, 31 Jan 2015 16:00:00 -0500 Subject: [PATCH 5/5] update to newer ats-mode-sublime --- vendor/grammars/ats.sublime | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/grammars/ats.sublime b/vendor/grammars/ats.sublime index e42cbf65..1e49e0b7 160000 --- a/vendor/grammars/ats.sublime +++ b/vendor/grammars/ats.sublime @@ -1 +1 @@ -Subproject commit e42cbf651152f4f3ada7502cf8002aa8729e147f +Subproject commit 1e49e0b7e00b7be2b971c4ac3b247d7255e09603