From 2770e4e111844936fdfa2f5f9861491cc000eaa6 Mon Sep 17 00:00:00 2001 From: Brandon Date: Sat, 25 Jan 2014 12:09:00 -0500 Subject: [PATCH] adding ATS and several sample files --- lib/linguist/languages.yml | 13 + samples/ATS/linset.hats | 187 ++++++++++++ samples/ATS/linset_listord.dats | 504 ++++++++++++++++++++++++++++++++ samples/ATS/linset_listord.sats | 51 ++++ samples/C/dynarray.cats | 56 ++++ 5 files changed, 811 insertions(+) create mode 100644 samples/ATS/linset.hats create mode 100644 samples/ATS/linset_listord.dats create mode 100644 samples/ATS/linset_listord.sats create mode 100644 samples/C/dynarray.cats diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 340c7682..4bef750b 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: + - .sats + - .hats + - .atxt + ActionScript: type: programming lexer: ActionScript 3 @@ -215,6 +227,7 @@ C: primary_extension: .c extensions: - .w + - .cats C#: type: programming 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/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] */