mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Merge branch 'master' of https://github.com/github/linguist into pro
This commit is contained in:
Paul Chaignon
@@ -53,6 +53,18 @@ ASP:
|
|||||||
- .aspx
|
- .aspx
|
||||||
- .axd
|
- .axd
|
||||||
|
|
||||||
|
ATS:
|
||||||
|
type: programming
|
||||||
|
color: "#1ac620"
|
||||||
|
primary_extension: .dats
|
||||||
|
lexer: OCaml
|
||||||
|
aliases:
|
||||||
|
- ats2
|
||||||
|
extensions:
|
||||||
|
- .atxt
|
||||||
|
- .hats
|
||||||
|
- .sats
|
||||||
|
|
||||||
ActionScript:
|
ActionScript:
|
||||||
type: programming
|
type: programming
|
||||||
lexer: ActionScript 3
|
lexer: ActionScript 3
|
||||||
@@ -92,6 +104,8 @@ AppleScript:
|
|||||||
primary_extension: .applescript
|
primary_extension: .applescript
|
||||||
extensions:
|
extensions:
|
||||||
- .scpt
|
- .scpt
|
||||||
|
interpreters:
|
||||||
|
- osascript
|
||||||
|
|
||||||
Arc:
|
Arc:
|
||||||
type: programming
|
type: programming
|
||||||
@@ -214,6 +228,7 @@ C:
|
|||||||
color: "#555"
|
color: "#555"
|
||||||
primary_extension: .c
|
primary_extension: .c
|
||||||
extensions:
|
extensions:
|
||||||
|
- .cats
|
||||||
- .w
|
- .w
|
||||||
|
|
||||||
C#:
|
C#:
|
||||||
@@ -832,6 +847,13 @@ JSON5:
|
|||||||
lexer: JavaScript
|
lexer: JavaScript
|
||||||
primary_extension: .json5
|
primary_extension: .json5
|
||||||
|
|
||||||
|
JSONLD:
|
||||||
|
type: data
|
||||||
|
group: JavaScript
|
||||||
|
ace_mode: json
|
||||||
|
lexer: JavaScript
|
||||||
|
primary_extension: .jsonld
|
||||||
|
|
||||||
Jade:
|
Jade:
|
||||||
group: HTML
|
group: HTML
|
||||||
type: markup
|
type: markup
|
||||||
@@ -1389,6 +1411,7 @@ R:
|
|||||||
primary_extension: .r
|
primary_extension: .r
|
||||||
extensions:
|
extensions:
|
||||||
- .R
|
- .R
|
||||||
|
- .rsx
|
||||||
filenames:
|
filenames:
|
||||||
- .Rprofile
|
- .Rprofile
|
||||||
interpreters:
|
interpreters:
|
||||||
@@ -1553,6 +1576,7 @@ Scheme:
|
|||||||
color: "#1e4aec"
|
color: "#1e4aec"
|
||||||
primary_extension: .scm
|
primary_extension: .scm
|
||||||
extensions:
|
extensions:
|
||||||
|
- .sld
|
||||||
- .sls
|
- .sls
|
||||||
- .ss
|
- .ss
|
||||||
interpreters:
|
interpreters:
|
||||||
|
|||||||
@@ -20,6 +20,12 @@
|
|||||||
".asc",
|
".asc",
|
||||||
".asciidoc"
|
".asciidoc"
|
||||||
],
|
],
|
||||||
|
"ATS": [
|
||||||
|
".atxt",
|
||||||
|
".dats",
|
||||||
|
".hats",
|
||||||
|
".sats"
|
||||||
|
],
|
||||||
"AutoHotkey": [
|
"AutoHotkey": [
|
||||||
".ahk"
|
".ahk"
|
||||||
],
|
],
|
||||||
@@ -37,6 +43,7 @@
|
|||||||
],
|
],
|
||||||
"C": [
|
"C": [
|
||||||
".c",
|
".c",
|
||||||
|
".cats",
|
||||||
".h"
|
".h"
|
||||||
],
|
],
|
||||||
"C#": [
|
"C#": [
|
||||||
@@ -52,6 +59,9 @@
|
|||||||
"Ceylon": [
|
"Ceylon": [
|
||||||
".ceylon"
|
".ceylon"
|
||||||
],
|
],
|
||||||
|
"Cirru": [
|
||||||
|
".cirru"
|
||||||
|
],
|
||||||
"Clojure": [
|
"Clojure": [
|
||||||
".cl2",
|
".cl2",
|
||||||
".clj",
|
".clj",
|
||||||
@@ -176,6 +186,9 @@
|
|||||||
"JSON5": [
|
"JSON5": [
|
||||||
".json5"
|
".json5"
|
||||||
],
|
],
|
||||||
|
"JSONLD": [
|
||||||
|
".jsonld"
|
||||||
|
],
|
||||||
"Julia": [
|
"Julia": [
|
||||||
".jl"
|
".jl"
|
||||||
],
|
],
|
||||||
@@ -330,6 +343,7 @@
|
|||||||
".pde"
|
".pde"
|
||||||
],
|
],
|
||||||
"Prolog": [
|
"Prolog": [
|
||||||
|
".ecl",
|
||||||
".pl",
|
".pl",
|
||||||
".prolog"
|
".prolog"
|
||||||
],
|
],
|
||||||
@@ -342,6 +356,7 @@
|
|||||||
],
|
],
|
||||||
"R": [
|
"R": [
|
||||||
".R",
|
".R",
|
||||||
|
".rsx",
|
||||||
".script!"
|
".script!"
|
||||||
],
|
],
|
||||||
"Racket": [
|
"Racket": [
|
||||||
@@ -535,8 +550,8 @@
|
|||||||
".gemrc"
|
".gemrc"
|
||||||
]
|
]
|
||||||
},
|
},
|
||||||
"tokens_total": 445429,
|
"tokens_total": 450519,
|
||||||
"languages_total": 523,
|
"languages_total": 547,
|
||||||
"tokens": {
|
"tokens": {
|
||||||
"ABAP": {
|
"ABAP": {
|
||||||
"*/**": 1,
|
"*/**": 1,
|
||||||
@@ -2032,6 +2047,561 @@
|
|||||||
".Section": 1,
|
".Section": 1,
|
||||||
"list": 1
|
"list": 1
|
||||||
},
|
},
|
||||||
|
"ATS": {
|
||||||
|
"//": 211,
|
||||||
|
"#include": 16,
|
||||||
|
"staload": 25,
|
||||||
|
"_": 25,
|
||||||
|
"sortdef": 2,
|
||||||
|
"ftype": 13,
|
||||||
|
"type": 30,
|
||||||
|
"-": 49,
|
||||||
|
"infixr": 2,
|
||||||
|
"(": 562,
|
||||||
|
")": 567,
|
||||||
|
"typedef": 10,
|
||||||
|
"a": 200,
|
||||||
|
"b": 26,
|
||||||
|
"<cloref1>": 2,
|
||||||
|
"functor": 12,
|
||||||
|
"F": 34,
|
||||||
|
"{": 142,
|
||||||
|
"}": 141,
|
||||||
|
"list0": 9,
|
||||||
|
"extern": 13,
|
||||||
|
"val": 95,
|
||||||
|
"functor_list0": 7,
|
||||||
|
"implement": 55,
|
||||||
|
"f": 22,
|
||||||
|
"lam": 20,
|
||||||
|
"xs": 82,
|
||||||
|
"list0_map": 2,
|
||||||
|
"<a>": 14,
|
||||||
|
"<b>": 3,
|
||||||
|
"datatype": 4,
|
||||||
|
"CoYoneda": 7,
|
||||||
|
"r": 25,
|
||||||
|
"of": 59,
|
||||||
|
"fun": 56,
|
||||||
|
"CoYoneda_phi": 2,
|
||||||
|
"CoYoneda_psi": 3,
|
||||||
|
"ftor": 9,
|
||||||
|
"fx": 8,
|
||||||
|
"x": 48,
|
||||||
|
"int0": 4,
|
||||||
|
"I": 8,
|
||||||
|
"int": 2,
|
||||||
|
"bool": 27,
|
||||||
|
"True": 7,
|
||||||
|
"|": 22,
|
||||||
|
"False": 8,
|
||||||
|
"boxed": 2,
|
||||||
|
"boolean": 2,
|
||||||
|
"bool2string": 4,
|
||||||
|
"string": 2,
|
||||||
|
"case": 9,
|
||||||
|
"+": 20,
|
||||||
|
"fprint_val": 2,
|
||||||
|
"<bool>": 2,
|
||||||
|
"out": 8,
|
||||||
|
"fprint": 3,
|
||||||
|
"int2bool": 2,
|
||||||
|
"i": 6,
|
||||||
|
"let": 34,
|
||||||
|
"in": 48,
|
||||||
|
"if": 7,
|
||||||
|
"then": 11,
|
||||||
|
"else": 7,
|
||||||
|
"end": 73,
|
||||||
|
"myintlist0": 2,
|
||||||
|
"g0ofg1": 1,
|
||||||
|
"list": 1,
|
||||||
|
"myboolist0": 9,
|
||||||
|
"fprintln": 3,
|
||||||
|
"stdout_ref": 4,
|
||||||
|
"main0": 3,
|
||||||
|
"UN": 3,
|
||||||
|
"phil_left": 3,
|
||||||
|
"n": 51,
|
||||||
|
"phil_right": 3,
|
||||||
|
"nmod": 1,
|
||||||
|
"NPHIL": 6,
|
||||||
|
"randsleep": 6,
|
||||||
|
"intGte": 1,
|
||||||
|
"void": 14,
|
||||||
|
"ignoret": 2,
|
||||||
|
"sleep": 2,
|
||||||
|
"UN.cast": 2,
|
||||||
|
"uInt": 1,
|
||||||
|
"rand": 1,
|
||||||
|
"mod": 1,
|
||||||
|
"phil_think": 3,
|
||||||
|
"println": 9,
|
||||||
|
"phil_dine": 3,
|
||||||
|
"lf": 5,
|
||||||
|
"rf": 5,
|
||||||
|
"phil_loop": 10,
|
||||||
|
"nl": 2,
|
||||||
|
"nr": 2,
|
||||||
|
"ch_lfork": 2,
|
||||||
|
"fork_changet": 5,
|
||||||
|
"ch_rfork": 2,
|
||||||
|
"channel_takeout": 4,
|
||||||
|
"HX": 1,
|
||||||
|
"try": 1,
|
||||||
|
"to": 16,
|
||||||
|
"actively": 1,
|
||||||
|
"induce": 1,
|
||||||
|
"deadlock": 2,
|
||||||
|
"ch_forktray": 3,
|
||||||
|
"forktray_changet": 4,
|
||||||
|
"channel_insert": 5,
|
||||||
|
"[": 49,
|
||||||
|
"]": 48,
|
||||||
|
"cleaner_wash": 3,
|
||||||
|
"fork_get_num": 4,
|
||||||
|
"cleaner_return": 4,
|
||||||
|
"ch": 7,
|
||||||
|
"cleaner_loop": 6,
|
||||||
|
"f0": 3,
|
||||||
|
"dynload": 3,
|
||||||
|
"local": 10,
|
||||||
|
"mythread_create_cloptr": 6,
|
||||||
|
"llam": 6,
|
||||||
|
"while": 1,
|
||||||
|
"true": 5,
|
||||||
|
"%": 7,
|
||||||
|
"#": 7,
|
||||||
|
"#define": 4,
|
||||||
|
"nphil": 13,
|
||||||
|
"natLt": 2,
|
||||||
|
"absvtype": 2,
|
||||||
|
"fork_vtype": 3,
|
||||||
|
"ptr": 2,
|
||||||
|
"vtypedef": 2,
|
||||||
|
"fork": 16,
|
||||||
|
"channel": 11,
|
||||||
|
"datavtype": 1,
|
||||||
|
"FORK": 3,
|
||||||
|
"assume": 2,
|
||||||
|
"the_forkarray": 2,
|
||||||
|
"t": 1,
|
||||||
|
"array_tabulate": 1,
|
||||||
|
"fopr": 1,
|
||||||
|
"<t>": 2,
|
||||||
|
"where": 6,
|
||||||
|
"channel_create_exn": 2,
|
||||||
|
"<fork>": 2,
|
||||||
|
"i2sz": 4,
|
||||||
|
"arrayref_tabulate": 1,
|
||||||
|
"the_forktray": 2,
|
||||||
|
"set_vtype": 3,
|
||||||
|
"t@ype": 2,
|
||||||
|
"set": 34,
|
||||||
|
"t0p": 31,
|
||||||
|
"compare_elt_elt": 4,
|
||||||
|
"x1": 1,
|
||||||
|
"x2": 1,
|
||||||
|
"<": 14,
|
||||||
|
"linset_nil": 2,
|
||||||
|
"linset_make_nil": 2,
|
||||||
|
"linset_sing": 2,
|
||||||
|
"<!wrt>": 16,
|
||||||
|
"linset_make_sing": 2,
|
||||||
|
"linset_make_list": 1,
|
||||||
|
"List": 1,
|
||||||
|
"INV": 24,
|
||||||
|
"linset_is_nil": 2,
|
||||||
|
"linset_isnot_nil": 2,
|
||||||
|
"linset_size": 2,
|
||||||
|
"size_t": 1,
|
||||||
|
"linset_is_member": 3,
|
||||||
|
"x0": 22,
|
||||||
|
"linset_isnot_member": 1,
|
||||||
|
"linset_copy": 2,
|
||||||
|
"linset_free": 2,
|
||||||
|
"linset_insert": 3,
|
||||||
|
"&": 17,
|
||||||
|
"linset_takeout": 1,
|
||||||
|
"res": 9,
|
||||||
|
"opt": 6,
|
||||||
|
"endfun": 1,
|
||||||
|
"linset_takeout_opt": 1,
|
||||||
|
"Option_vt": 4,
|
||||||
|
"linset_remove": 2,
|
||||||
|
"linset_choose": 3,
|
||||||
|
"linset_choose_opt": 1,
|
||||||
|
"linset_takeoutmax": 1,
|
||||||
|
"linset_takeoutmax_opt": 1,
|
||||||
|
"linset_takeoutmin": 1,
|
||||||
|
"linset_takeoutmin_opt": 1,
|
||||||
|
"fprint_linset": 3,
|
||||||
|
"sep": 1,
|
||||||
|
"FILEref": 2,
|
||||||
|
"overload": 1,
|
||||||
|
"with": 1,
|
||||||
|
"env": 11,
|
||||||
|
"vt0p": 2,
|
||||||
|
"linset_foreach": 3,
|
||||||
|
"fwork": 3,
|
||||||
|
"linset_foreach_env": 3,
|
||||||
|
"linset_listize": 2,
|
||||||
|
"List0_vt": 5,
|
||||||
|
"linset_listize1": 2,
|
||||||
|
"code": 6,
|
||||||
|
"reuse": 2,
|
||||||
|
"elt": 2,
|
||||||
|
"list_vt_nil": 16,
|
||||||
|
"list_vt_cons": 17,
|
||||||
|
"list_vt_is_nil": 1,
|
||||||
|
"list_vt_is_cons": 1,
|
||||||
|
"list_vt_length": 1,
|
||||||
|
"aux": 4,
|
||||||
|
"nat": 4,
|
||||||
|
".": 14,
|
||||||
|
"<n>": 3,
|
||||||
|
"list_vt": 7,
|
||||||
|
"sgn": 9,
|
||||||
|
"false": 6,
|
||||||
|
"list_vt_copy": 2,
|
||||||
|
"list_vt_free": 1,
|
||||||
|
"mynode_cons": 4,
|
||||||
|
"nx": 22,
|
||||||
|
"mynode1": 6,
|
||||||
|
"xs1": 15,
|
||||||
|
"UN.castvwtp0": 8,
|
||||||
|
"List1_vt": 5,
|
||||||
|
"@list_vt_cons": 5,
|
||||||
|
"xs2": 3,
|
||||||
|
"prval": 20,
|
||||||
|
"UN.cast2void": 5,
|
||||||
|
";": 4,
|
||||||
|
"fold@": 8,
|
||||||
|
"ins": 3,
|
||||||
|
"tail": 1,
|
||||||
|
"recursive": 1,
|
||||||
|
"n1": 4,
|
||||||
|
"<=>": 1,
|
||||||
|
"1": 3,
|
||||||
|
"mynode_make_elt": 4,
|
||||||
|
"ans": 2,
|
||||||
|
"is": 26,
|
||||||
|
"found": 1,
|
||||||
|
"effmask_all": 3,
|
||||||
|
"free@": 1,
|
||||||
|
"xs1_": 3,
|
||||||
|
"rem": 1,
|
||||||
|
"*": 2,
|
||||||
|
"opt_some": 1,
|
||||||
|
"opt_none": 1,
|
||||||
|
"list_vt_foreach": 1,
|
||||||
|
"<env>": 3,
|
||||||
|
"list_vt_foreach_env": 1,
|
||||||
|
"mynode_null": 5,
|
||||||
|
"mynode": 3,
|
||||||
|
"null": 1,
|
||||||
|
"the_null_ptr": 1,
|
||||||
|
"mynode_free": 1,
|
||||||
|
"nx2": 4,
|
||||||
|
"mynode_get_elt": 1,
|
||||||
|
"nx1": 7,
|
||||||
|
"UN.castvwtp1": 2,
|
||||||
|
"mynode_set_elt": 1,
|
||||||
|
"l": 3,
|
||||||
|
"__assert": 2,
|
||||||
|
"praxi": 1,
|
||||||
|
"mynode_getfree_elt": 1,
|
||||||
|
"linset_takeout_ngc": 2,
|
||||||
|
"takeout": 3,
|
||||||
|
"mynode0": 1,
|
||||||
|
"pf_x": 6,
|
||||||
|
"view@x": 3,
|
||||||
|
"pf_xs1": 6,
|
||||||
|
"view@xs1": 3,
|
||||||
|
"linset_takeoutmax_ngc": 2,
|
||||||
|
"xs_": 4,
|
||||||
|
"@list_vt_nil": 1,
|
||||||
|
"linset_takeoutmin_ngc": 2,
|
||||||
|
"unsnoc": 4,
|
||||||
|
"pos": 1,
|
||||||
|
"and": 10,
|
||||||
|
"fold@xs": 1,
|
||||||
|
"ATS_PACKNAME": 1,
|
||||||
|
"ATS_STALOADFLAG": 1,
|
||||||
|
"no": 2,
|
||||||
|
"static": 1,
|
||||||
|
"loading": 1,
|
||||||
|
"at": 2,
|
||||||
|
"run": 1,
|
||||||
|
"time": 1,
|
||||||
|
"castfn": 1,
|
||||||
|
"linset2list": 1,
|
||||||
|
"<!DOCTYPE>": 1,
|
||||||
|
"html": 1,
|
||||||
|
"PUBLIC": 1,
|
||||||
|
"W3C": 1,
|
||||||
|
"DTD": 2,
|
||||||
|
"XHTML": 1,
|
||||||
|
"EN": 1,
|
||||||
|
"http": 2,
|
||||||
|
"www": 1,
|
||||||
|
"w3": 1,
|
||||||
|
"org": 1,
|
||||||
|
"TR": 1,
|
||||||
|
"xhtml11": 2,
|
||||||
|
"dtd": 1,
|
||||||
|
"<html>": 1,
|
||||||
|
"xmlns=": 1,
|
||||||
|
"<head>": 1,
|
||||||
|
"<meta>": 1,
|
||||||
|
"equiv=": 1,
|
||||||
|
"content=": 1,
|
||||||
|
"<title>": 1,
|
||||||
|
"EFFECTIVATS": 1,
|
||||||
|
"DiningPhil2": 1,
|
||||||
|
"</title>": 1,
|
||||||
|
"#patscode_style": 1,
|
||||||
|
"</head>": 1,
|
||||||
|
"<body>": 1,
|
||||||
|
"<h1>": 1,
|
||||||
|
"Effective": 1,
|
||||||
|
"ATS": 2,
|
||||||
|
"Dining": 2,
|
||||||
|
"Philosophers": 2,
|
||||||
|
"</h1>": 1,
|
||||||
|
"In": 2,
|
||||||
|
"this": 2,
|
||||||
|
"article": 2,
|
||||||
|
"present": 1,
|
||||||
|
"an": 6,
|
||||||
|
"implementation": 3,
|
||||||
|
"slight": 1,
|
||||||
|
"variant": 1,
|
||||||
|
"the": 30,
|
||||||
|
"famous": 1,
|
||||||
|
"problem": 1,
|
||||||
|
"by": 4,
|
||||||
|
"Dijkstra": 1,
|
||||||
|
"that": 8,
|
||||||
|
"makes": 1,
|
||||||
|
"simple": 1,
|
||||||
|
"but": 1,
|
||||||
|
"convincing": 1,
|
||||||
|
"use": 1,
|
||||||
|
"linear": 2,
|
||||||
|
"types.": 1,
|
||||||
|
"<h2>": 8,
|
||||||
|
"The": 8,
|
||||||
|
"Original": 2,
|
||||||
|
"Problem": 2,
|
||||||
|
"</h2>": 8,
|
||||||
|
"There": 3,
|
||||||
|
"are": 7,
|
||||||
|
"five": 1,
|
||||||
|
"philosophers": 1,
|
||||||
|
"sitting": 1,
|
||||||
|
"around": 1,
|
||||||
|
"table": 3,
|
||||||
|
"there": 3,
|
||||||
|
"also": 3,
|
||||||
|
"forks": 7,
|
||||||
|
"placed": 1,
|
||||||
|
"on": 8,
|
||||||
|
"such": 1,
|
||||||
|
"each": 2,
|
||||||
|
"located": 2,
|
||||||
|
"between": 1,
|
||||||
|
"left": 3,
|
||||||
|
"hand": 6,
|
||||||
|
"philosopher": 5,
|
||||||
|
"right": 3,
|
||||||
|
"another": 1,
|
||||||
|
"philosopher.": 1,
|
||||||
|
"Each": 4,
|
||||||
|
"does": 1,
|
||||||
|
"following": 6,
|
||||||
|
"routine": 1,
|
||||||
|
"repeatedly": 1,
|
||||||
|
"thinking": 1,
|
||||||
|
"dining.": 1,
|
||||||
|
"order": 1,
|
||||||
|
"dine": 1,
|
||||||
|
"needs": 2,
|
||||||
|
"first": 2,
|
||||||
|
"acquire": 1,
|
||||||
|
"two": 3,
|
||||||
|
"one": 3,
|
||||||
|
"his": 4,
|
||||||
|
"side": 2,
|
||||||
|
"other": 2,
|
||||||
|
"side.": 2,
|
||||||
|
"After": 2,
|
||||||
|
"finishing": 1,
|
||||||
|
"dining": 1,
|
||||||
|
"puts": 2,
|
||||||
|
"acquired": 1,
|
||||||
|
"onto": 1,
|
||||||
|
"A": 6,
|
||||||
|
"Variant": 1,
|
||||||
|
"twist": 1,
|
||||||
|
"added": 1,
|
||||||
|
"original": 1,
|
||||||
|
"version": 1,
|
||||||
|
"<p>": 1,
|
||||||
|
"used": 1,
|
||||||
|
"it": 2,
|
||||||
|
"becomes": 1,
|
||||||
|
"be": 9,
|
||||||
|
"put": 1,
|
||||||
|
"tray": 2,
|
||||||
|
"for": 15,
|
||||||
|
"dirty": 2,
|
||||||
|
"forks.": 1,
|
||||||
|
"cleaner": 2,
|
||||||
|
"who": 1,
|
||||||
|
"cleans": 1,
|
||||||
|
"them": 2,
|
||||||
|
"back": 1,
|
||||||
|
"table.": 1,
|
||||||
|
"Channels": 1,
|
||||||
|
"Communication": 1,
|
||||||
|
"just": 1,
|
||||||
|
"shared": 1,
|
||||||
|
"queue": 1,
|
||||||
|
"fixed": 1,
|
||||||
|
"capacity.": 1,
|
||||||
|
"functions": 1,
|
||||||
|
"inserting": 1,
|
||||||
|
"element": 5,
|
||||||
|
"into": 3,
|
||||||
|
"taking": 1,
|
||||||
|
"given": 4,
|
||||||
|
"<pre>": 7,
|
||||||
|
"class=": 6,
|
||||||
|
"#pats2xhtml_sats": 3,
|
||||||
|
"</pre>": 7,
|
||||||
|
"If": 2,
|
||||||
|
"called": 2,
|
||||||
|
"full": 4,
|
||||||
|
"caller": 2,
|
||||||
|
"blocked": 3,
|
||||||
|
"until": 2,
|
||||||
|
"taken": 1,
|
||||||
|
"channel.": 2,
|
||||||
|
"empty": 1,
|
||||||
|
"inserted": 1,
|
||||||
|
"Channel": 2,
|
||||||
|
"Fork": 3,
|
||||||
|
"Forks": 1,
|
||||||
|
"resources": 1,
|
||||||
|
"type.": 1,
|
||||||
|
"initially": 1,
|
||||||
|
"stored": 2,
|
||||||
|
"which": 2,
|
||||||
|
"can": 4,
|
||||||
|
"obtained": 2,
|
||||||
|
"calling": 2,
|
||||||
|
"function": 3,
|
||||||
|
"defined": 1,
|
||||||
|
"natural": 1,
|
||||||
|
"numbers": 1,
|
||||||
|
"less": 1,
|
||||||
|
"than": 1,
|
||||||
|
"channels": 4,
|
||||||
|
"storing": 3,
|
||||||
|
"chosen": 3,
|
||||||
|
"capacity": 3,
|
||||||
|
"reason": 1,
|
||||||
|
"store": 1,
|
||||||
|
"most": 1,
|
||||||
|
"guarantee": 1,
|
||||||
|
"these": 1,
|
||||||
|
"never": 2,
|
||||||
|
"so": 2,
|
||||||
|
"attempt": 1,
|
||||||
|
"made": 1,
|
||||||
|
"send": 1,
|
||||||
|
"signals": 1,
|
||||||
|
"awake": 1,
|
||||||
|
"callers": 1,
|
||||||
|
"supposedly": 1,
|
||||||
|
"being": 2,
|
||||||
|
"due": 1,
|
||||||
|
"Tray": 1,
|
||||||
|
"instead": 1,
|
||||||
|
"become": 1,
|
||||||
|
"as": 4,
|
||||||
|
"only": 1,
|
||||||
|
"total": 1,
|
||||||
|
"Philosopher": 1,
|
||||||
|
"Loop": 2,
|
||||||
|
"implemented": 2,
|
||||||
|
"loop": 2,
|
||||||
|
"#pats2xhtml_dats": 3,
|
||||||
|
"It": 2,
|
||||||
|
"should": 3,
|
||||||
|
"straighforward": 2,
|
||||||
|
"follow": 2,
|
||||||
|
"Cleaner": 1,
|
||||||
|
"finds": 1,
|
||||||
|
"number": 2,
|
||||||
|
"uses": 1,
|
||||||
|
"locate": 1,
|
||||||
|
"fork.": 1,
|
||||||
|
"Its": 1,
|
||||||
|
"actual": 1,
|
||||||
|
"follows": 1,
|
||||||
|
"now": 1,
|
||||||
|
"Testing": 1,
|
||||||
|
"entire": 1,
|
||||||
|
"files": 1,
|
||||||
|
"DiningPhil2.sats": 1,
|
||||||
|
"DiningPhil2.dats": 1,
|
||||||
|
"DiningPhil2_fork.dats": 1,
|
||||||
|
"DiningPhil2_thread.dats": 1,
|
||||||
|
"Makefile": 1,
|
||||||
|
"available": 1,
|
||||||
|
"compiling": 1,
|
||||||
|
"source": 1,
|
||||||
|
"excutable": 1,
|
||||||
|
"testing.": 1,
|
||||||
|
"One": 1,
|
||||||
|
"able": 1,
|
||||||
|
"encounter": 1,
|
||||||
|
"after": 1,
|
||||||
|
"running": 1,
|
||||||
|
"simulation": 1,
|
||||||
|
"while.": 1,
|
||||||
|
"<hr>": 1,
|
||||||
|
"size=": 1,
|
||||||
|
"This": 1,
|
||||||
|
"written": 1,
|
||||||
|
"href=": 1,
|
||||||
|
"Hongwei": 1,
|
||||||
|
"Xi": 1,
|
||||||
|
"</a>": 1,
|
||||||
|
"</body>": 1,
|
||||||
|
"</html>": 1,
|
||||||
|
"main": 1,
|
||||||
|
"fprint_filsub": 1,
|
||||||
|
"option0": 3,
|
||||||
|
"functor_option0": 2,
|
||||||
|
"option0_map": 1,
|
||||||
|
"functor_homres": 2,
|
||||||
|
"c": 3,
|
||||||
|
"Yoneda_phi": 3,
|
||||||
|
"Yoneda_psi": 3,
|
||||||
|
"m": 4,
|
||||||
|
"mf": 4,
|
||||||
|
"natrans": 3,
|
||||||
|
"G": 2,
|
||||||
|
"Yoneda_phi_nat": 2,
|
||||||
|
"Yoneda_psi_nat": 2,
|
||||||
|
"list_t": 1,
|
||||||
|
"g0ofg1_list": 1,
|
||||||
|
"Yoneda_bool_list0": 3,
|
||||||
|
"myboolist1": 2
|
||||||
|
},
|
||||||
"AutoHotkey": {
|
"AutoHotkey": {
|
||||||
"MsgBox": 1,
|
"MsgBox": 1,
|
||||||
"Hello": 1,
|
"Hello": 1,
|
||||||
@@ -2961,7 +3531,7 @@
|
|||||||
"buttons": 1
|
"buttons": 1
|
||||||
},
|
},
|
||||||
"C": {
|
"C": {
|
||||||
"#include": 152,
|
"#include": 154,
|
||||||
"const": 358,
|
"const": 358,
|
||||||
"char": 530,
|
"char": 530,
|
||||||
"*blob_type": 2,
|
"*blob_type": 2,
|
||||||
@@ -2969,10 +3539,10 @@
|
|||||||
"struct": 360,
|
"struct": 360,
|
||||||
"blob": 6,
|
"blob": 6,
|
||||||
"*lookup_blob": 2,
|
"*lookup_blob": 2,
|
||||||
"(": 6238,
|
"(": 6243,
|
||||||
"unsigned": 140,
|
"unsigned": 140,
|
||||||
"*sha1": 16,
|
"*sha1": 16,
|
||||||
")": 6240,
|
")": 6245,
|
||||||
"{": 1531,
|
"{": 1531,
|
||||||
"object": 41,
|
"object": 41,
|
||||||
"*obj": 9,
|
"*obj": 9,
|
||||||
@@ -3001,11 +3571,11 @@
|
|||||||
"size": 120,
|
"size": 120,
|
||||||
"item": 24,
|
"item": 24,
|
||||||
"object.parsed": 4,
|
"object.parsed": 4,
|
||||||
"#ifndef": 87,
|
"#ifndef": 89,
|
||||||
"BLOB_H": 2,
|
"BLOB_H": 2,
|
||||||
"#define": 913,
|
"#define": 920,
|
||||||
"extern": 38,
|
"extern": 38,
|
||||||
"#endif": 241,
|
"#endif": 243,
|
||||||
"BOOTSTRAP_H": 2,
|
"BOOTSTRAP_H": 2,
|
||||||
"<stdio.h>": 8,
|
"<stdio.h>": 8,
|
||||||
"__GNUC__": 8,
|
"__GNUC__": 8,
|
||||||
@@ -3086,7 +3656,7 @@
|
|||||||
"hash": 12,
|
"hash": 12,
|
||||||
"*node": 2,
|
"*node": 2,
|
||||||
"*result": 1,
|
"*result": 1,
|
||||||
"memcpy": 34,
|
"memcpy": 35,
|
||||||
"oid": 17,
|
"oid": 17,
|
||||||
"id": 13,
|
"id": 13,
|
||||||
"git_mutex_lock": 2,
|
"git_mutex_lock": 2,
|
||||||
@@ -3885,6 +4455,13 @@
|
|||||||
"diff_delta__merge_like_cgit": 1,
|
"diff_delta__merge_like_cgit": 1,
|
||||||
"git_vector_swap": 1,
|
"git_vector_swap": 1,
|
||||||
"git_pool_swap": 1,
|
"git_pool_swap": 1,
|
||||||
|
"ATSHOME_LIBATS_DYNARRAY_CATS": 3,
|
||||||
|
"<string.h>": 5,
|
||||||
|
"atslib_dynarray_memcpy": 1,
|
||||||
|
"atslib_dynarray_memmove": 1,
|
||||||
|
"memmove": 2,
|
||||||
|
"//": 262,
|
||||||
|
"ifndef": 2,
|
||||||
"git_usage_string": 2,
|
"git_usage_string": 2,
|
||||||
"git_more_info_string": 2,
|
"git_more_info_string": 2,
|
||||||
"N_": 1,
|
"N_": 1,
|
||||||
@@ -4121,7 +4698,6 @@
|
|||||||
"<stddef.h>": 2,
|
"<stddef.h>": 2,
|
||||||
"<ctype.h>": 3,
|
"<ctype.h>": 3,
|
||||||
"<stdlib.h>": 3,
|
"<stdlib.h>": 3,
|
||||||
"<string.h>": 4,
|
|
||||||
"<limits.h>": 2,
|
"<limits.h>": 2,
|
||||||
"ULLONG_MAX": 10,
|
"ULLONG_MAX": 10,
|
||||||
"MIN": 3,
|
"MIN": 3,
|
||||||
@@ -4817,6 +5393,15 @@
|
|||||||
"rb_define_class": 1,
|
"rb_define_class": 1,
|
||||||
"rb_cObject": 1,
|
"rb_cObject": 1,
|
||||||
"rb_define_method": 2,
|
"rb_define_method": 2,
|
||||||
|
"READLINE_READLINE_CATS": 3,
|
||||||
|
"<readline/readline.h>": 1,
|
||||||
|
"atscntrb_readline_rl_library_version": 1,
|
||||||
|
"char*": 167,
|
||||||
|
"rl_library_version": 1,
|
||||||
|
"atscntrb_readline_rl_readline_version": 1,
|
||||||
|
"rl_readline_version": 1,
|
||||||
|
"atscntrb_readline_readline": 1,
|
||||||
|
"readline": 1,
|
||||||
"<time.h>": 1,
|
"<time.h>": 1,
|
||||||
"<signal.h>": 1,
|
"<signal.h>": 1,
|
||||||
"<stdarg.h>": 1,
|
"<stdarg.h>": 1,
|
||||||
@@ -5072,7 +5657,6 @@
|
|||||||
"key": 9,
|
"key": 9,
|
||||||
"dictGenHashFunction": 5,
|
"dictGenHashFunction": 5,
|
||||||
"dictSdsHash": 4,
|
"dictSdsHash": 4,
|
||||||
"char*": 166,
|
|
||||||
"dictSdsCaseHash": 2,
|
"dictSdsCaseHash": 2,
|
||||||
"dictGenCaseHashFunction": 1,
|
"dictGenCaseHashFunction": 1,
|
||||||
"dictEncObjKeyCompare": 4,
|
"dictEncObjKeyCompare": 4,
|
||||||
@@ -5695,7 +6279,6 @@
|
|||||||
"<rf_io.h>": 1,
|
"<rf_io.h>": 1,
|
||||||
"<rf_utils.h>": 2,
|
"<rf_utils.h>": 2,
|
||||||
"<String/rfc_string.h>": 2,
|
"<String/rfc_string.h>": 2,
|
||||||
"//": 257,
|
|
||||||
"rfUTF8_IsContinuationbyte": 1,
|
"rfUTF8_IsContinuationbyte": 1,
|
||||||
"e.t.c.": 1,
|
"e.t.c.": 1,
|
||||||
"rfFReadLine_UTF8": 5,
|
"rfFReadLine_UTF8": 5,
|
||||||
@@ -6172,7 +6755,6 @@
|
|||||||
"use": 1,
|
"use": 1,
|
||||||
"determine": 1,
|
"determine": 1,
|
||||||
"backs": 1,
|
"backs": 1,
|
||||||
"memmove": 1,
|
|
||||||
"by": 1,
|
"by": 1,
|
||||||
"contiuing": 1,
|
"contiuing": 1,
|
||||||
"make": 3,
|
"make": 3,
|
||||||
@@ -12715,6 +13297,43 @@
|
|||||||
"<=>": 1,
|
"<=>": 1,
|
||||||
"other.name": 1
|
"other.name": 1
|
||||||
},
|
},
|
||||||
|
"Cirru": {
|
||||||
|
"print": 38,
|
||||||
|
"array": 14,
|
||||||
|
"int": 36,
|
||||||
|
"string": 7,
|
||||||
|
"set": 12,
|
||||||
|
"f": 3,
|
||||||
|
"block": 1,
|
||||||
|
"(": 20,
|
||||||
|
"a": 22,
|
||||||
|
"b": 7,
|
||||||
|
"c": 9,
|
||||||
|
")": 20,
|
||||||
|
"call": 1,
|
||||||
|
"bool": 6,
|
||||||
|
"true": 1,
|
||||||
|
"false": 1,
|
||||||
|
"yes": 1,
|
||||||
|
"no": 1,
|
||||||
|
"map": 8,
|
||||||
|
"m": 3,
|
||||||
|
"float": 1,
|
||||||
|
"require": 1,
|
||||||
|
"./stdio.cr": 1,
|
||||||
|
"self": 2,
|
||||||
|
"child": 1,
|
||||||
|
"under": 2,
|
||||||
|
"parent": 1,
|
||||||
|
"get": 4,
|
||||||
|
"x": 2,
|
||||||
|
"just": 4,
|
||||||
|
"-": 4,
|
||||||
|
"code": 4,
|
||||||
|
"eval": 2,
|
||||||
|
"nothing": 1,
|
||||||
|
"container": 3
|
||||||
|
},
|
||||||
"Clojure": {
|
"Clojure": {
|
||||||
"(": 83,
|
"(": 83,
|
||||||
"defn": 4,
|
"defn": 4,
|
||||||
@@ -25467,6 +26086,13 @@
|
|||||||
"type": 1,
|
"type": 1,
|
||||||
"url": 1
|
"url": 1
|
||||||
},
|
},
|
||||||
|
"JSONLD": {
|
||||||
|
"{": 7,
|
||||||
|
"}": 7,
|
||||||
|
"[": 1,
|
||||||
|
"null": 2,
|
||||||
|
"]": 1
|
||||||
|
},
|
||||||
"Julia": {
|
"Julia": {
|
||||||
"##": 5,
|
"##": 5,
|
||||||
"Test": 1,
|
"Test": 1,
|
||||||
@@ -39026,12 +39652,56 @@
|
|||||||
"TWO_PI": 1
|
"TWO_PI": 1
|
||||||
},
|
},
|
||||||
"Prolog": {
|
"Prolog": {
|
||||||
"-": 38,
|
"-": 52,
|
||||||
|
"lib": 1,
|
||||||
|
"(": 49,
|
||||||
|
"ic": 1,
|
||||||
|
")": 49,
|
||||||
|
".": 25,
|
||||||
|
"vabs": 2,
|
||||||
|
"Val": 8,
|
||||||
|
"AbsVal": 10,
|
||||||
|
"#": 9,
|
||||||
|
";": 1,
|
||||||
|
"labeling": 2,
|
||||||
|
"[": 21,
|
||||||
|
"]": 21,
|
||||||
|
"vabsIC": 1,
|
||||||
|
"or": 1,
|
||||||
|
"faitListe": 3,
|
||||||
|
"_": 2,
|
||||||
|
"First": 2,
|
||||||
|
"|": 12,
|
||||||
|
"Rest": 6,
|
||||||
|
"Taille": 2,
|
||||||
|
"Min": 2,
|
||||||
|
"Max": 2,
|
||||||
|
"Min..Max": 1,
|
||||||
|
"Taille1": 2,
|
||||||
|
"suite": 3,
|
||||||
|
"Xi": 5,
|
||||||
|
"Xi1": 7,
|
||||||
|
"Xi2": 7,
|
||||||
|
"checkRelation": 3,
|
||||||
|
"VabsXi1": 2,
|
||||||
|
"Xi.": 1,
|
||||||
|
"checkPeriode": 3,
|
||||||
|
"ListVar": 2,
|
||||||
|
"length": 1,
|
||||||
|
"Length": 2,
|
||||||
|
"<": 1,
|
||||||
|
"X1": 2,
|
||||||
|
"X2": 2,
|
||||||
|
"X3": 2,
|
||||||
|
"X4": 2,
|
||||||
|
"X5": 2,
|
||||||
|
"X6": 2,
|
||||||
|
"X7": 2,
|
||||||
|
"X8": 2,
|
||||||
|
"X9": 2,
|
||||||
|
"X10": 3,
|
||||||
"male": 3,
|
"male": 3,
|
||||||
"(": 29,
|
|
||||||
"john": 2,
|
"john": 2,
|
||||||
")": 29,
|
|
||||||
".": 17,
|
|
||||||
"peter": 3,
|
"peter": 3,
|
||||||
"female": 2,
|
"female": 2,
|
||||||
"vick": 2,
|
"vick": 2,
|
||||||
@@ -39047,8 +39717,6 @@
|
|||||||
"Tape": 2,
|
"Tape": 2,
|
||||||
"perform": 4,
|
"perform": 4,
|
||||||
"q0": 1,
|
"q0": 1,
|
||||||
"[": 12,
|
|
||||||
"]": 12,
|
|
||||||
"Ls": 12,
|
"Ls": 12,
|
||||||
"Rs": 16,
|
"Rs": 16,
|
||||||
"reverse": 1,
|
"reverse": 1,
|
||||||
@@ -39067,7 +39735,6 @@
|
|||||||
"NewSym": 2,
|
"NewSym": 2,
|
||||||
"Action": 2,
|
"Action": 2,
|
||||||
"action": 4,
|
"action": 4,
|
||||||
"|": 7,
|
|
||||||
"Rs1": 2,
|
"Rs1": 2,
|
||||||
"b": 2,
|
"b": 2,
|
||||||
"left": 4,
|
"left": 4,
|
||||||
@@ -40070,9 +40737,9 @@
|
|||||||
"<": 12,
|
"<": 12,
|
||||||
"-": 12,
|
"-": 12,
|
||||||
"function": 3,
|
"function": 3,
|
||||||
"(": 28,
|
"(": 29,
|
||||||
"lines": 4,
|
"lines": 4,
|
||||||
")": 28,
|
")": 29,
|
||||||
"{": 3,
|
"{": 3,
|
||||||
"dates": 3,
|
"dates": 3,
|
||||||
"matrix": 2,
|
"matrix": 2,
|
||||||
@@ -40082,8 +40749,8 @@
|
|||||||
"byrow": 2,
|
"byrow": 2,
|
||||||
"TRUE": 3,
|
"TRUE": 3,
|
||||||
"days": 2,
|
"days": 2,
|
||||||
"[": 3,
|
"[": 4,
|
||||||
"]": 3,
|
"]": 4,
|
||||||
"times": 2,
|
"times": 2,
|
||||||
"hours": 2,
|
"hours": 2,
|
||||||
"all.days": 2,
|
"all.days": 2,
|
||||||
@@ -40118,7 +40785,22 @@
|
|||||||
"width": 1,
|
"width": 1,
|
||||||
"height": 1,
|
"height": 1,
|
||||||
"hello": 2,
|
"hello": 2,
|
||||||
"print": 1
|
"print": 1,
|
||||||
|
"##polyg": 1,
|
||||||
|
"vector": 2,
|
||||||
|
"##numpoints": 1,
|
||||||
|
"number": 1,
|
||||||
|
"##output": 1,
|
||||||
|
"output": 1,
|
||||||
|
"##": 1,
|
||||||
|
"Example": 1,
|
||||||
|
"scripts": 1,
|
||||||
|
"group": 1,
|
||||||
|
"pts": 1,
|
||||||
|
"spsample": 1,
|
||||||
|
"polyg": 1,
|
||||||
|
"numpoints": 1,
|
||||||
|
"type": 1
|
||||||
},
|
},
|
||||||
"Racket": {
|
"Racket": {
|
||||||
";": 3,
|
";": 3,
|
||||||
@@ -47790,15 +48472,17 @@
|
|||||||
"AppleScript": 1862,
|
"AppleScript": 1862,
|
||||||
"Arduino": 20,
|
"Arduino": 20,
|
||||||
"AsciiDoc": 103,
|
"AsciiDoc": 103,
|
||||||
|
"ATS": 4558,
|
||||||
"AutoHotkey": 3,
|
"AutoHotkey": 3,
|
||||||
"Awk": 544,
|
"Awk": 544,
|
||||||
"BlitzBasic": 2065,
|
"BlitzBasic": 2065,
|
||||||
"Bluespec": 1298,
|
"Bluespec": 1298,
|
||||||
"Brightscript": 579,
|
"Brightscript": 579,
|
||||||
"C": 59004,
|
"C": 59053,
|
||||||
"C#": 278,
|
"C#": 278,
|
||||||
"C++": 31181,
|
"C++": 31181,
|
||||||
"Ceylon": 50,
|
"Ceylon": 50,
|
||||||
|
"Cirru": 244,
|
||||||
"Clojure": 510,
|
"Clojure": 510,
|
||||||
"COBOL": 90,
|
"COBOL": 90,
|
||||||
"CoffeeScript": 2951,
|
"CoffeeScript": 2951,
|
||||||
@@ -47834,6 +48518,7 @@
|
|||||||
"JavaScript": 76934,
|
"JavaScript": 76934,
|
||||||
"JSON": 183,
|
"JSON": 183,
|
||||||
"JSON5": 57,
|
"JSON5": 57,
|
||||||
|
"JSONLD": 18,
|
||||||
"Julia": 247,
|
"Julia": 247,
|
||||||
"Kotlin": 155,
|
"Kotlin": 155,
|
||||||
"KRL": 25,
|
"KRL": 25,
|
||||||
@@ -47880,10 +48565,10 @@
|
|||||||
"PostScript": 107,
|
"PostScript": 107,
|
||||||
"PowerShell": 12,
|
"PowerShell": 12,
|
||||||
"Processing": 74,
|
"Processing": 74,
|
||||||
"Prolog": 267,
|
"Prolog": 468,
|
||||||
"Protocol Buffer": 63,
|
"Protocol Buffer": 63,
|
||||||
"Python": 5715,
|
"Python": 5715,
|
||||||
"R": 175,
|
"R": 195,
|
||||||
"Racket": 331,
|
"Racket": 331,
|
||||||
"Ragel in Ruby Host": 593,
|
"Ragel in Ruby Host": 593,
|
||||||
"RDoc": 279,
|
"RDoc": 279,
|
||||||
@@ -47932,15 +48617,17 @@
|
|||||||
"AppleScript": 7,
|
"AppleScript": 7,
|
||||||
"Arduino": 1,
|
"Arduino": 1,
|
||||||
"AsciiDoc": 3,
|
"AsciiDoc": 3,
|
||||||
|
"ATS": 10,
|
||||||
"AutoHotkey": 1,
|
"AutoHotkey": 1,
|
||||||
"Awk": 1,
|
"Awk": 1,
|
||||||
"BlitzBasic": 3,
|
"BlitzBasic": 3,
|
||||||
"Bluespec": 2,
|
"Bluespec": 2,
|
||||||
"Brightscript": 1,
|
"Brightscript": 1,
|
||||||
"C": 27,
|
"C": 29,
|
||||||
"C#": 2,
|
"C#": 2,
|
||||||
"C++": 27,
|
"C++": 27,
|
||||||
"Ceylon": 1,
|
"Ceylon": 1,
|
||||||
|
"Cirru": 9,
|
||||||
"Clojure": 7,
|
"Clojure": 7,
|
||||||
"COBOL": 4,
|
"COBOL": 4,
|
||||||
"CoffeeScript": 9,
|
"CoffeeScript": 9,
|
||||||
@@ -47976,6 +48663,7 @@
|
|||||||
"JavaScript": 20,
|
"JavaScript": 20,
|
||||||
"JSON": 4,
|
"JSON": 4,
|
||||||
"JSON5": 2,
|
"JSON5": 2,
|
||||||
|
"JSONLD": 1,
|
||||||
"Julia": 1,
|
"Julia": 1,
|
||||||
"Kotlin": 1,
|
"Kotlin": 1,
|
||||||
"KRL": 1,
|
"KRL": 1,
|
||||||
@@ -48022,10 +48710,10 @@
|
|||||||
"PostScript": 1,
|
"PostScript": 1,
|
||||||
"PowerShell": 2,
|
"PowerShell": 2,
|
||||||
"Processing": 1,
|
"Processing": 1,
|
||||||
"Prolog": 2,
|
"Prolog": 3,
|
||||||
"Protocol Buffer": 1,
|
"Protocol Buffer": 1,
|
||||||
"Python": 7,
|
"Python": 7,
|
||||||
"R": 2,
|
"R": 3,
|
||||||
"Racket": 2,
|
"Racket": 2,
|
||||||
"Ragel in Ruby Host": 3,
|
"Ragel in Ruby Host": 3,
|
||||||
"RDoc": 1,
|
"RDoc": 1,
|
||||||
@@ -48066,5 +48754,5 @@
|
|||||||
"Xtend": 2,
|
"Xtend": 2,
|
||||||
"YAML": 1
|
"YAML": 1
|
||||||
},
|
},
|
||||||
"md5": "a46f14929a6e9e4356fda95beb035439"
|
"md5": "8815515b1699aba1650cc4e4b81587fd"
|
||||||
}
|
}
|
||||||
@@ -47,6 +47,9 @@
|
|||||||
# Debian packaging
|
# Debian packaging
|
||||||
- ^debian/
|
- ^debian/
|
||||||
|
|
||||||
|
# Haxelib projects often contain a neko bytecode file named run.n
|
||||||
|
- run.n$
|
||||||
|
|
||||||
## Commonly Bundled JavaScript frameworks ##
|
## Commonly Bundled JavaScript frameworks ##
|
||||||
|
|
||||||
# jQuery
|
# jQuery
|
||||||
|
|||||||
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] */
|
||||||
30
samples/JSONLD/sample.jsonld
Normal file
30
samples/JSONLD/sample.jsonld
Normal file
@@ -0,0 +1,30 @@
|
|||||||
|
{
|
||||||
|
"@context": {
|
||||||
|
"property": "http://example.com/vocab#property"
|
||||||
|
},
|
||||||
|
"@id": "../document-relative",
|
||||||
|
"@type": "#document-relative",
|
||||||
|
"property": {
|
||||||
|
"@context": {
|
||||||
|
"@base": "http://example.org/test/"
|
||||||
|
},
|
||||||
|
"@id": "../document-base-overwritten",
|
||||||
|
"@type": "#document-base-overwritten",
|
||||||
|
"property": [
|
||||||
|
{
|
||||||
|
"@context": null,
|
||||||
|
"@id": "../document-relative",
|
||||||
|
"@type": "#document-relative",
|
||||||
|
"property": "context completely reset, drops property"
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"@context": {
|
||||||
|
"@base": null
|
||||||
|
},
|
||||||
|
"@id": "../document-relative",
|
||||||
|
"@type": "#document-relative",
|
||||||
|
"property": "only @base is cleared"
|
||||||
|
}
|
||||||
|
]
|
||||||
|
}
|
||||||
|
}
|
||||||
5
samples/R/R-qgis-extension.rsx
Normal file
5
samples/R/R-qgis-extension.rsx
Normal file
@@ -0,0 +1,5 @@
|
|||||||
|
##polyg=vector
|
||||||
|
##numpoints=number 10
|
||||||
|
##output=output vector
|
||||||
|
##[Example scripts]=group
|
||||||
|
pts=spsample(polyg,numpoints,type="regular")
|
||||||
7
samples/Scheme/basic.sld
Normal file
7
samples/Scheme/basic.sld
Normal file
@@ -0,0 +1,7 @@
|
|||||||
|
(define-library (libs basic)
|
||||||
|
(export list2 x)
|
||||||
|
(begin
|
||||||
|
(define (list2 . objs) objs)
|
||||||
|
(define x 'libs-basic)
|
||||||
|
(define not-exported 'should-not-be-exported)
|
||||||
|
))
|
||||||
Reference in New Issue
Block a user