diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 82cc4be4..fcc42188 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -53,6 +53,18 @@ ASP: - .aspx - .axd +ATS: + type: programming + color: "#1ac620" + primary_extension: .dats + lexer: OCaml + aliases: + - ats2 + extensions: + - .atxt + - .hats + - .sats + ActionScript: type: programming lexer: ActionScript 3 @@ -92,6 +104,8 @@ AppleScript: primary_extension: .applescript extensions: - .scpt + interpreters: + - osascript Arc: type: programming @@ -214,6 +228,7 @@ C: color: "#555" primary_extension: .c extensions: + - .cats - .w C#: @@ -832,6 +847,13 @@ JSON5: lexer: JavaScript primary_extension: .json5 +JSONLD: + type: data + group: JavaScript + ace_mode: json + lexer: JavaScript + primary_extension: .jsonld + Jade: group: HTML type: markup @@ -1389,6 +1411,7 @@ R: primary_extension: .r extensions: - .R + - .rsx filenames: - .Rprofile interpreters: @@ -1553,6 +1576,7 @@ Scheme: color: "#1e4aec" primary_extension: .scm extensions: + - .sld - .sls - .ss interpreters: diff --git a/lib/linguist/samples.json b/lib/linguist/samples.json index ed92145a..67f6e90e 100644 --- a/lib/linguist/samples.json +++ b/lib/linguist/samples.json @@ -20,6 +20,12 @@ ".asc", ".asciidoc" ], + "ATS": [ + ".atxt", + ".dats", + ".hats", + ".sats" + ], "AutoHotkey": [ ".ahk" ], @@ -37,6 +43,7 @@ ], "C": [ ".c", + ".cats", ".h" ], "C#": [ @@ -52,6 +59,9 @@ "Ceylon": [ ".ceylon" ], + "Cirru": [ + ".cirru" + ], "Clojure": [ ".cl2", ".clj", @@ -176,6 +186,9 @@ "JSON5": [ ".json5" ], + "JSONLD": [ + ".jsonld" + ], "Julia": [ ".jl" ], @@ -330,6 +343,7 @@ ".pde" ], "Prolog": [ + ".ecl", ".pl", ".prolog" ], @@ -342,6 +356,7 @@ ], "R": [ ".R", + ".rsx", ".script!" ], "Racket": [ @@ -535,8 +550,8 @@ ".gemrc" ] }, - "tokens_total": 445429, - "languages_total": 523, + "tokens_total": 450519, + "languages_total": 547, "tokens": { "ABAP": { "*/**": 1, @@ -2032,6 +2047,561 @@ ".Section": 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, + "": 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, + "": 14, + "": 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, + "": 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, + "": 2, + "where": 6, + "channel_create_exn": 2, + "": 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, + "": 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, + "": 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, + "": 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, + "": 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, + "": 1, + "xmlns=": 1, + "": 1, + "": 1, + "equiv=": 1, + "content=": 1, + "": 1, + "EFFECTIVATS": 1, + "DiningPhil2": 1, + "": 1, + "#patscode_style": 1, + "": 1, + "": 1, + "

": 1, + "Effective": 1, + "ATS": 2, + "Dining": 2, + "Philosophers": 2, + "

": 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, + "

": 8, + "The": 8, + "Original": 2, + "Problem": 2, + "

": 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, + "

": 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, + "

": 7,
+      "class=": 6,
+      "#pats2xhtml_sats": 3,
+      "
": 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, + "
": 1, + "size=": 1, + "This": 1, + "written": 1, + "href=": 1, + "Hongwei": 1, + "Xi": 1, + "": 1, + "": 1, + "": 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": { "MsgBox": 1, "Hello": 1, @@ -2961,7 +3531,7 @@ "buttons": 1 }, "C": { - "#include": 152, + "#include": 154, "const": 358, "char": 530, "*blob_type": 2, @@ -2969,10 +3539,10 @@ "struct": 360, "blob": 6, "*lookup_blob": 2, - "(": 6238, + "(": 6243, "unsigned": 140, "*sha1": 16, - ")": 6240, + ")": 6245, "{": 1531, "object": 41, "*obj": 9, @@ -3001,11 +3571,11 @@ "size": 120, "item": 24, "object.parsed": 4, - "#ifndef": 87, + "#ifndef": 89, "BLOB_H": 2, - "#define": 913, + "#define": 920, "extern": 38, - "#endif": 241, + "#endif": 243, "BOOTSTRAP_H": 2, "": 8, "__GNUC__": 8, @@ -3086,7 +3656,7 @@ "hash": 12, "*node": 2, "*result": 1, - "memcpy": 34, + "memcpy": 35, "oid": 17, "id": 13, "git_mutex_lock": 2, @@ -3885,6 +4455,13 @@ "diff_delta__merge_like_cgit": 1, "git_vector_swap": 1, "git_pool_swap": 1, + "ATSHOME_LIBATS_DYNARRAY_CATS": 3, + "": 5, + "atslib_dynarray_memcpy": 1, + "atslib_dynarray_memmove": 1, + "memmove": 2, + "//": 262, + "ifndef": 2, "git_usage_string": 2, "git_more_info_string": 2, "N_": 1, @@ -4121,7 +4698,6 @@ "": 2, "": 3, "": 3, - "": 4, "": 2, "ULLONG_MAX": 10, "MIN": 3, @@ -4817,6 +5393,15 @@ "rb_define_class": 1, "rb_cObject": 1, "rb_define_method": 2, + "READLINE_READLINE_CATS": 3, + "": 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, "": 1, "": 1, "": 1, @@ -5072,7 +5657,6 @@ "key": 9, "dictGenHashFunction": 5, "dictSdsHash": 4, - "char*": 166, "dictSdsCaseHash": 2, "dictGenCaseHashFunction": 1, "dictEncObjKeyCompare": 4, @@ -5695,7 +6279,6 @@ "": 1, "": 2, "": 2, - "//": 257, "rfUTF8_IsContinuationbyte": 1, "e.t.c.": 1, "rfFReadLine_UTF8": 5, @@ -6172,7 +6755,6 @@ "use": 1, "determine": 1, "backs": 1, - "memmove": 1, "by": 1, "contiuing": 1, "make": 3, @@ -12715,6 +13297,43 @@ "<=>": 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": { "(": 83, "defn": 4, @@ -25467,6 +26086,13 @@ "type": 1, "url": 1 }, + "JSONLD": { + "{": 7, + "}": 7, + "[": 1, + "null": 2, + "]": 1 + }, "Julia": { "##": 5, "Test": 1, @@ -39026,12 +39652,56 @@ "TWO_PI": 1 }, "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, - "(": 29, "john": 2, - ")": 29, - ".": 17, "peter": 3, "female": 2, "vick": 2, @@ -39047,8 +39717,6 @@ "Tape": 2, "perform": 4, "q0": 1, - "[": 12, - "]": 12, "Ls": 12, "Rs": 16, "reverse": 1, @@ -39067,7 +39735,6 @@ "NewSym": 2, "Action": 2, "action": 4, - "|": 7, "Rs1": 2, "b": 2, "left": 4, @@ -40070,9 +40737,9 @@ "<": 12, "-": 12, "function": 3, - "(": 28, + "(": 29, "lines": 4, - ")": 28, + ")": 29, "{": 3, "dates": 3, "matrix": 2, @@ -40082,8 +40749,8 @@ "byrow": 2, "TRUE": 3, "days": 2, - "[": 3, - "]": 3, + "[": 4, + "]": 4, "times": 2, "hours": 2, "all.days": 2, @@ -40118,7 +40785,22 @@ "width": 1, "height": 1, "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": { ";": 3, @@ -47790,15 +48472,17 @@ "AppleScript": 1862, "Arduino": 20, "AsciiDoc": 103, + "ATS": 4558, "AutoHotkey": 3, "Awk": 544, "BlitzBasic": 2065, "Bluespec": 1298, "Brightscript": 579, - "C": 59004, + "C": 59053, "C#": 278, "C++": 31181, "Ceylon": 50, + "Cirru": 244, "Clojure": 510, "COBOL": 90, "CoffeeScript": 2951, @@ -47834,6 +48518,7 @@ "JavaScript": 76934, "JSON": 183, "JSON5": 57, + "JSONLD": 18, "Julia": 247, "Kotlin": 155, "KRL": 25, @@ -47880,10 +48565,10 @@ "PostScript": 107, "PowerShell": 12, "Processing": 74, - "Prolog": 267, + "Prolog": 468, "Protocol Buffer": 63, "Python": 5715, - "R": 175, + "R": 195, "Racket": 331, "Ragel in Ruby Host": 593, "RDoc": 279, @@ -47932,15 +48617,17 @@ "AppleScript": 7, "Arduino": 1, "AsciiDoc": 3, + "ATS": 10, "AutoHotkey": 1, "Awk": 1, "BlitzBasic": 3, "Bluespec": 2, "Brightscript": 1, - "C": 27, + "C": 29, "C#": 2, "C++": 27, "Ceylon": 1, + "Cirru": 9, "Clojure": 7, "COBOL": 4, "CoffeeScript": 9, @@ -47976,6 +48663,7 @@ "JavaScript": 20, "JSON": 4, "JSON5": 2, + "JSONLD": 1, "Julia": 1, "Kotlin": 1, "KRL": 1, @@ -48022,10 +48710,10 @@ "PostScript": 1, "PowerShell": 2, "Processing": 1, - "Prolog": 2, + "Prolog": 3, "Protocol Buffer": 1, "Python": 7, - "R": 2, + "R": 3, "Racket": 2, "Ragel in Ruby Host": 3, "RDoc": 1, @@ -48066,5 +48754,5 @@ "Xtend": 2, "YAML": 1 }, - "md5": "a46f14929a6e9e4356fda95beb035439" + "md5": "8815515b1699aba1650cc4e4b81587fd" } \ No newline at end of file diff --git a/lib/linguist/vendor.yml b/lib/linguist/vendor.yml index ca00b057..3609b466 100644 --- a/lib/linguist/vendor.yml +++ b/lib/linguist/vendor.yml @@ -47,6 +47,9 @@ # Debian packaging - ^debian/ +# Haxelib projects often contain a neko bytecode file named run.n +- run.n$ + ## Commonly Bundled JavaScript frameworks ## # jQuery diff --git a/samples/ATS/CoYonedaLemma.dats b/samples/ATS/CoYonedaLemma.dats new file mode 100644 index 00000000..aeac8bb1 --- /dev/null +++ b/samples/ATS/CoYonedaLemma.dats @@ -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 - 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 (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 (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] *) diff --git a/samples/ATS/DiningPhil2.dats b/samples/ATS/DiningPhil2.dats new file mode 100644 index 00000000..55c39654 --- /dev/null +++ b/samples/ATS/DiningPhil2.dats @@ -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] *) diff --git a/samples/ATS/DiningPhil2.sats b/samples/ATS/DiningPhil2.sats new file mode 100644 index 00000000..bc7e96be --- /dev/null +++ b/samples/ATS/DiningPhil2.sats @@ -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] *) diff --git a/samples/ATS/DiningPhil2_fork.dats b/samples/ATS/DiningPhil2_fork.dats new file mode 100644 index 00000000..a6a8d4df --- /dev/null +++ b/samples/ATS/DiningPhil2_fork.dats @@ -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 + (n) = ch where +{ + val n = $UN.cast{nphil}(n) + val ch = channel_create_exn (i2sz(2)) + val () = channel_insert (ch, FORK (n)) +} +// +in + arrayref_tabulate (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 (i2sz(NPHIL+1)) + +in (* in of [local] *) + +implement forktray_changet () = the_forktray + +end // end of [local] + +(* ****** ****** *) + +(* end of [DiningPhil2_fork.dats] *) diff --git a/samples/ATS/DiningPhil2_thread.dats b/samples/ATS/DiningPhil2_thread.dats new file mode 100644 index 00000000..be73840b --- /dev/null +++ b/samples/ATS/DiningPhil2_thread.dats @@ -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] *) diff --git a/samples/ATS/YonedaLemma.dats b/samples/ATS/YonedaLemma.dats new file mode 100644 index 00000000..cd3c31e6 --- /dev/null +++ b/samples/ATS/YonedaLemma.dats @@ -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 - 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 (xs, f) + +(* ****** ****** *) + +typedef +option0 (a:type) = option0 (a) +extern +val functor_option0 : functor (option0) + +(* ****** ****** *) + +implement +functor_option0{a,b} + (f) = lam opt => option0_map (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 (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] *) diff --git a/samples/ATS/linset.hats b/samples/ATS/linset.hats new file mode 100644 index 00000000..29e44c44 --- /dev/null +++ b/samples/ATS/linset.hats @@ -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): set(a) +fun{a:t0p} linset_make_sing (x: a): set(a) + +(* ****** ****** *) + +fun{a:t0p} +linset_make_list (xs: List(INV(a))): 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))): set(a) +fun{a:t0p} +linset_free (xs: set(INV(a))): void + +(* ****** ****** *) +// +fun{a:t0p} +linset_insert + (xs: &set(INV(a)) >> _, x0: a): bool +// +(* ****** ****** *) +// +fun{a:t0p} +linset_takeout +( + &set(INV(a)) >> _, a, res: &(a?) >> opt(a, b) +) : #[b:bool] bool(b) // endfun +fun{a:t0p} +linset_takeout_opt (&set(INV(a)) >> _, a): Option_vt(a) +// +(* ****** ****** *) +// +fun{a:t0p} +linset_remove + (xs: &set(INV(a)) >> _, x0: a): bool +// +(* ****** ****** *) +// +// HX: choosing an element in an unspecified manner +// +fun{a:t0p} +linset_choose +( + xs: !set(INV(a)), x: &a? >> opt (a, b) +) : #[b:bool] bool(b) +// +fun{a:t0p} +linset_choose_opt (xs: !set(INV(a))): Option_vt(a) +// +(* ****** ****** *) + +fun{a:t0p} +linset_takeoutmax +( + xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) +) : #[b:bool] bool (b) +fun{a:t0p} +linset_takeoutmax_opt (xs: &set(INV(a)) >> _): Option_vt(a) + +(* ****** ****** *) + +fun{a:t0p} +linset_takeoutmin +( + xs: &set(INV(a)) >> _, res: &a? >> opt(a, b) +) : #[b:bool] bool (b) +fun{a:t0p} +linset_takeoutmin_opt (xs: &set(INV(a)) >> _): 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] *) diff --git a/samples/ATS/linset_listord.dats b/samples/ATS/linset_listord.dats new file mode 100644 index 00000000..eb7dd642 --- /dev/null +++ b/samples/ATS/linset_listord.dats @@ -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} .. +( + xs: !list_vt (a, n) +) :<> bool = let +in +// +case+ xs of +| list_vt_cons (x, xs) => let + val sgn = compare_elt_elt (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 (xs) +implement{a} +linset_free (xs) = list_vt_free (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} .. // 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 (x0, x) + // end of [val] + in + if sgn > 0 then let + prval () = fold@ (xs) + val nx = mynode_make_elt (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 (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} .. // 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 (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 + (x, env) = linset_foreach$fwork (x, env) +// +in + list_vt_foreach_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): 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 (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} .. +( + xs: &list_vt (a, n) >> list_vt (a, n-1) +) : 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] *) diff --git a/samples/ATS/linset_listord.sats b/samples/ATS/linset_listord.sats new file mode 100644 index 00000000..468a534f --- /dev/null +++ b/samples/ATS/linset_listord.sats @@ -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] *) diff --git a/samples/ATS/main.atxt b/samples/ATS/main.atxt new file mode 100644 index 00000000..3bba35f0 --- /dev/null +++ b/samples/ATS/main.atxt @@ -0,0 +1,215 @@ +%{ +#include "./../ATEXT/atextfun.hats" +%} + + + + + + +EFFECTIVATS-DiningPhil2 +#patscode_style() + + + + +

+Effective ATS: Dining Philosophers +

+ +In this article, I present an implementation of a slight variant of the +famous problem of 5-Dining-Philosophers by Dijkstra that makes simple but +convincing use of linear types. + +

+The Original Problem +

+ +There are five philosophers sitting around a table and there are also 5 +forks placed on the table such that each fork is located between the left +hand of a philosopher and the right hand of another philosopher. Each +philosopher does the following routine repeatedly: thinking and dining. In +order to dine, a philosopher needs to first acquire two forks: one located +on his left-hand side and the other on his right-hand side. After +finishing dining, a philosopher puts the two acquired forks onto the table: +one on his left-hand side and the other on his right-hand side. + +

+A Variant of the Original Problem +

+ +The following twist is added to the original version: + +

+ +After a fork is used, it becomes a "dirty" fork and needs to be put in a +tray for dirty forks. There is a cleaner who cleans dirty forks and then +puts them back on the table. + +

+Channels for Communication +

+ +A channel is just a shared queue of fixed capacity. The following two +functions are for inserting an element into and taking an element out of a +given channel: + +
+#pats2xhtml_sats("\
+fun{a:vt0p} channel_insert (channel (a), a): void
+fun{a:vt0p} channel_takeout (chan: channel (a)): (a) 
+")
+ +If [channel_insert] is called on a channel that is full, then the caller is +blocked until an element is taken out of the channel. If [channel_takeout] +is called on a channel that is empty, then the caller is blocked until an +element is inserted into the channel. + +

+A Channel for Each Fork +

+ +Forks are resources given a linear type. Each fork is initially stored in a +channel, which can be obtained by calling the following function: + +
+#pats2xhtml_sats("\
+fun fork_changet (n: nphil): channel(fork)
+")
+ +where the type [nphil] is defined to be [natLt(5)] (for natural numbers +less than 5). The channels for storing forks are chosen to be of capacity +2. The reason that channels of capacity 2 are chosen to store at most one +element (in each of them) is to guarantee that these channels can never be +full (so that there is no attempt made to send signals to awake callers +supposedly being blocked due to channels being full). + + +

+A Channel for the Fork Tray +

+ +A tray for storing "dirty" forks is also a channel, which can be obtained +by calling the following function: + +
+#pats2xhtml_sats("\
+fun forktray_changet ((*void*)): channel(fork)
+")
+ +The capacity chosen for the channel is 6 (instead of 5) so that it can +never become full (as there are only 5 forks in total). + +

+Philosopher Loop +

+ +Each philosopher is implemented as a loop: + +
+#pats2xhtml_dats('\
+implement
+phil_loop (n) = let
+//
+val () = phil_think (n)
+//
+val nl = phil_left (n) // = n
+val nr = phil_right (n) // = (n+1) % 5
+//
+val ch_lfork = fork_changet (nl)
+val ch_rfork = fork_changet (nr)
+//
+val lf = channel_takeout (ch_lfork)
+val () = println! ("phil_loop(", n, ") picks left fork")
+//
+val () = randsleep (2) // sleep up to 2 seconds
+//
+val rf = channel_takeout (ch_rfork)
+val () = println! ("phil_loop(", n, ") picks right fork")
+//
+val () = phil_dine (n, lf, rf)
+//
+val ch_forktray = forktray_changet ()
+val () = channel_insert (ch_forktray, lf) // left fork to dirty tray
+val () = channel_insert (ch_forktray, rf) // right fork to dirty tray
+//
+in
+  phil_loop (n)
+end // end of [phil_loop]
+')
+ +It should be straighforward to follow the code for [phil_loop]. + +

+Fork Cleaner Loop +

+ +A cleaner is implemented as a loop: + +
+#pats2xhtml_dats('\
+implement
+cleaner_loop () = let
+//
+val ch = forktray_changet ()
+val f0 = channel_takeout (ch) // [f0] is dirty
+//
+val () = cleaner_wash (f0) // washes dirty [f0]
+val () = cleaner_return (f0) // puts back cleaned [f0]
+//
+in
+  cleaner_loop ()
+end // end of [cleaner_loop]
+')
+ +The function [cleaner_return] first finds out the number of a given fork +and then uses the number to locate the channel for storing the fork. Its +actual implementation is given as follows: + +
+#pats2xhtml_dats('\
+implement
+cleaner_return (f) =
+{
+  val n = fork_get_num (f)
+  val ch = fork_changet (n)
+  val () = channel_insert (ch, f)
+}
+')
+ +It should now be straighforward to follow the code for [cleaner_loop]. + +

+Testing +

+ +The entire code of this implementation is stored in the following files: + +
+DiningPhil2.sats
+DiningPhil2.dats
+DiningPhil2_fork.dats
+DiningPhil2_thread.dats
+
+ +There is also a Makefile available for compiling the ATS source code into +an excutable for testing. One should be able to encounter a deadlock after +running the simulation for a while. + +
+ +This article is written by Hongwei Xi. + + + + +%{ +implement main () = fprint_filsub (stdout_ref, "main_atxt.txt") +%} diff --git a/samples/C/dynarray.cats b/samples/C/dynarray.cats new file mode 100644 index 00000000..95ee54ba --- /dev/null +++ b/samples/C/dynarray.cats @@ -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 + +/* ****** ****** */ + +#define atslib_dynarray_memcpy memcpy +#define atslib_dynarray_memmove memmove + +/* ****** ****** */ + +#endif // ifndef ATSHOME_LIBATS_DYNARRAY_CATS + +/* ****** ****** */ + +/* end of [dynarray.cats] */ diff --git a/samples/C/readline.cats b/samples/C/readline.cats new file mode 100644 index 00000000..3fad326b --- /dev/null +++ b/samples/C/readline.cats @@ -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 + +/* ****** ****** */ +// +#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] */ diff --git a/samples/JSONLD/sample.jsonld b/samples/JSONLD/sample.jsonld new file mode 100644 index 00000000..dbae017a --- /dev/null +++ b/samples/JSONLD/sample.jsonld @@ -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" + } + ] + } +} diff --git a/samples/R/R-qgis-extension.rsx b/samples/R/R-qgis-extension.rsx new file mode 100644 index 00000000..adf59e67 --- /dev/null +++ b/samples/R/R-qgis-extension.rsx @@ -0,0 +1,5 @@ +##polyg=vector +##numpoints=number 10 +##output=output vector +##[Example scripts]=group +pts=spsample(polyg,numpoints,type="regular") diff --git a/samples/Scheme/basic.sld b/samples/Scheme/basic.sld new file mode 100644 index 00000000..85dc75c6 --- /dev/null +++ b/samples/Scheme/basic.sld @@ -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) + ))