mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Merge pull request #2057 from steinwaywhw/master
Adding ATS language support by converting existing SublimeText syntax def
This commit is contained in:
Arfon Smith
3
.gitmodules
vendored
3
.gitmodules
vendored
@@ -555,6 +555,9 @@
|
|||||||
[submodule "vendor/grammars/liquid.tmbundle"]
|
[submodule "vendor/grammars/liquid.tmbundle"]
|
||||||
path = vendor/grammars/liquid.tmbundle
|
path = vendor/grammars/liquid.tmbundle
|
||||||
url = https://github.com/bastilian/validcode-textmate-bundles
|
url = https://github.com/bastilian/validcode-textmate-bundles
|
||||||
|
[submodule "vendor/grammars/ats.sublime"]
|
||||||
|
path = vendor/grammars/ats.sublime
|
||||||
|
url = https://github.com/steinwaywhw/ats-mode-sublimetext
|
||||||
[submodule "vendor/grammars/Modelica"]
|
[submodule "vendor/grammars/Modelica"]
|
||||||
path = vendor/grammars/Modelica
|
path = vendor/grammars/Modelica
|
||||||
url = https://github.com/BorisChumichev/modelicaSublimeTextPackage
|
url = https://github.com/BorisChumichev/modelicaSublimeTextPackage
|
||||||
|
|||||||
@@ -130,6 +130,8 @@ vendor/grammars/assembly.tmbundle:
|
|||||||
vendor/grammars/atom-salt:
|
vendor/grammars/atom-salt:
|
||||||
- source.python.salt
|
- source.python.salt
|
||||||
- source.yaml.salt
|
- source.yaml.salt
|
||||||
|
vendor/grammars/ats.sublime:
|
||||||
|
- source.ats
|
||||||
vendor/grammars/autoitv3-tmbundle:
|
vendor/grammars/autoitv3-tmbundle:
|
||||||
- source.autoit.3
|
- source.autoit.3
|
||||||
vendor/grammars/awk-sublime:
|
vendor/grammars/awk-sublime:
|
||||||
|
|||||||
@@ -82,10 +82,9 @@ ATS:
|
|||||||
- ats2
|
- ats2
|
||||||
extensions:
|
extensions:
|
||||||
- .dats
|
- .dats
|
||||||
- .atxt
|
|
||||||
- .hats
|
- .hats
|
||||||
- .sats
|
- .sats
|
||||||
tm_scope: source.ocaml
|
tm_scope: source.ats
|
||||||
ace_mode: ocaml
|
ace_mode: ocaml
|
||||||
|
|
||||||
ActionScript:
|
ActionScript:
|
||||||
|
|||||||
@@ -1,215 +0,0 @@
|
|||||||
%{
|
|
||||||
#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")
|
|
||||||
%}
|
|
||||||
1
vendor/grammars/ats.sublime
vendored
Submodule
1
vendor/grammars/ats.sublime
vendored
Submodule
Submodule vendor/grammars/ats.sublime added at 1e49e0b7e0
Reference in New Issue
Block a user