language-ats 0.1.1.15 → 0.1.1.17
raw patch · 6 files changed
+224/−9 lines, 6 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.ATS: Call :: Name -> [[Type]] -> [Type] -> (Maybe Expression) -> [Expression] -> Expression
+ Language.ATS: Call :: Name -> [[Type]] -> [Type] -> (Maybe [Expression]) -> [Expression] -> Expression
- Language.ATS: ProofType :: AlexPosn -> Type -> Type -> Type
+ Language.ATS: ProofType :: AlexPosn -> [Type] -> Type -> Type
Files
- language-ats.cabal +1/−1
- src/Language/ATS/Parser.y +4/−3
- src/Language/ATS/PrettyPrint.hs +3/−3
- src/Language/ATS/Types.hs +2/−2
- test/data/fastcount.dats +99/−0
- test/data/fastcount.out +115/−0
language-ats.cabal view
@@ -1,5 +1,5 @@ name: language-ats-version: 0.1.1.15+version: 0.1.1.17 synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license: BSD3
src/Language/ATS/Parser.y view
@@ -114,9 +114,9 @@ effmaskWrt { Identifier $$ "effmask_wrt" } effmaskAll { Identifier $$ "effmask_all" } effmaskRef { Identifier $$ "effmask_ref" }+ extfcall { Identifier $$ "extfcall" } tempenver { Identifier $$ "tempenver" } extype { Identifier $$ "extype" }- extfcall { Identifier $$ "extfcall" } ldelay { Identifier $$ "ldelay" } listVT { Identifier $$ "list_vt" } foldAt { Identifier $$ "fold@" }@@ -247,7 +247,7 @@ | Type at Type { At $2 (Just $1) $3 } | at Type { At $1 Nothing $2 } | atbrace Records rbrace { AnonymousRecord $1 $2 }- | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }+ | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 } -- FIXME can have multiple first parts | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] } | openParen TypeIn closeParen { Tuple $1 $2 } | openParen Type closeParen { ParenType $1 $2 }@@ -316,7 +316,7 @@ | IfCase vbar Expression CaseArrow Expression { ($3, $4, $5) : $1 } ExpressionPrf : ExpressionIn { (Nothing, $1) }- | Expression vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?+ | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof? -- | A list of comma-separated expressions ExpressionIn : Expression { [$1] }@@ -507,6 +507,7 @@ | dollar effmaskWrt { SpecialName $1 "effmask_wrt" } | dollar effmaskAll { SpecialName $1 "effmask_all" } | dollar effmaskRef { SpecialName $1 "effmask_ref" }+ | dollar extfcall { SpecialName $1 "extfcall" } | dollar tempenver { SpecialName $1 "tempenver" } | dollar extype { SpecialName $1 "effmask_all" } | dollar listVT { SpecialName $1 "list_vt" }
src/Language/ATS/PrettyPrint.hs view
@@ -123,8 +123,8 @@ | length (showFast d2) >= 30 = d1 <$> indent 4 d2 | otherwise = d1 <+> d2 -prettyArgsProof :: (Pretty a) => Maybe a -> [Doc] -> Doc-prettyArgsProof (Just e) = prettyArgsG ("(" <> pretty e <+> "| ") ")"+prettyArgsProof :: (Pretty a) => Maybe [a] -> [Doc] -> Doc+prettyArgsProof (Just e) = prettyArgsG ("(" <> prettyArgsG mempty mempty (fmap pretty e) <+> "| ") ")" prettyArgsProof Nothing = prettyArgs instance Pretty Expression where@@ -293,7 +293,7 @@ a (Vt0pF ad) = "vt@ype" <> pretty ad a (AtF _ (Just t) t') = t <+> "@" <+> t' a (AtF _ Nothing t) = "@" <> t- a (ProofTypeF _ t t') = parens (t <+> "|" <+> t')+ a (ProofTypeF _ t t') = parens (prettyArgsU "" "" t <+> "|" <+> t') a (ConcreteTypeF e) = pretty e a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) a (RefTypeF t) = "&" <> t
src/Language/ATS/Types.hs view
@@ -144,7 +144,7 @@ | T0p Addendum -- t@ype | Vt0p Addendum -- vt@ype | At AlexPosn (Maybe Type) Type- | ProofType AlexPosn Type Type -- Aka (prf | val)+ | ProofType AlexPosn [Type] Type -- Aka (prf | val) | ConcreteType StaticExpression | RefType Type | ViewType AlexPosn Type@@ -244,7 +244,7 @@ | VoidLiteral -- The '()' literal representing inaction. AlexPosn -- function call: <a>, then {n}- | Call Name [[Type]] [Type] (Maybe Expression) [Expression]+ | Call Name [[Type]] [Type] (Maybe [Expression]) [Expression] | NamedVal Name | ListLiteral AlexPosn String Type [Expression] | If { cond :: Expression -- ^ Expression evaluating to a boolean value
+ test/data/fastcount.dats view
@@ -0,0 +1,99 @@+(*+**+** A fast approach to counting newlines+**+** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)+** Time: April 17, 2013+**+*)+#include "share/atspre_staload.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "libats/libc/SATS/stdio.sats"++%{^+extern void *rawmemchr(const void *s, int c);+#define atslib_rawmemchr rawmemchr+%}++extern+fun rawmemchr {l:addr}{m:int}(pf : bytes_v(l, m) | p : ptr(l), c : int) :+ [ l2 : addr | l+m > l2 ] (bytes_v(l, l2-l),bytes_v(l2, l+m-l2) | ptr(l2)) =+ "mac#atslib_rawmemchr"++(* ****** ****** *)+#define BUFSZ (16*1024)++(* ****** ****** *)+extern+fun freadc {l:addr} (pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : char) : size_t++implement freadc (pf | inp, p, c) =+ let+ var n = $extfcall(size_t, "fread", p, sizeof<char>, BUFSZ - 1, inp)+ val () = $UN.ptr0_set<char>(ptr_add<char>(p, n), c)+ in+ n+ end++(* ****** ****** *)+extern+fun wclbuf {l:addr}{n:int} (pf : !bytes_v(l, n) | p : ptr(l), pz : ptr, c : int, res : int) :+ int++implement wclbuf (pf | p, pz, c, res) =+ let+ val (pf1, pf2 | p2) = rawmemchr(pf | p, c)+ in+ if p2 < pz then+ let+ prval (pf21, pf22) = array_v_uncons(pf2)+ var res = wclbuf(pf22 | ptr_succ<byte>(p2), pz, c, res + 1)+ prval () = pf2 := array_v_cons(pf21, pf22)+ prval () = pf := bytes_v_unsplit(pf1, pf2)+ in+ res+ end+ else+ let+ prval () = pf := bytes_v_unsplit(pf1, pf2)+ in+ res+ end+ end++(* ****** ****** *)+extern+fun wclfil {l:addr} (pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : int) : int++implement wclfil {l} (pf | inp, p, c) =+ let+ fun loop(pf : !bytes_v(l, BUFSZ) | inp : FILEref, p : ptr(l), c : int, res : int) : int =+ let+ val n = freadc(pf | inp, p, $UN.cast{char}(c))+ in+ if n > 0 then+ let+ var pz = ptr_add<char>(p, n)+ var res = wclbuf(pf | p, pz, c, res)+ in+ loop(pf | inp, p, c, res)+ end+ else+ res+ end+ in+ loop(pf | inp, p, c, 0)+ end++(* ****** ****** *)+fun line_count(s : string) : int =+ let+ var inp: FILEref = fopen_ref_exn(s, file_mode_r)+ val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))+ prval () = pfat := b0ytes2bytes_v(pfat)+ var res = wclfil(pfat | inp, p, $UN.cast2int('\n'))+ val () = mfree_gc(pfat, pfgc | p)+ in+ res+ end
+ test/data/fastcount.out view
@@ -0,0 +1,115 @@+(*+**+** A fast approach to counting newlines+**+** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)+** Time: April 17, 2013+**+*)+#include "share/atspre_staload.hats"++staload UN = "prelude/SATS/unsafe.sats"+staload "libats/libc/SATS/stdio.sats"++%{^+extern void *rawmemchr(const void *s, int c);+#define atslib_rawmemchr rawmemchr+%}++extern+fun rawmemchr {l:addr}{m:int}( pf : bytes_v(l, m) | p : ptr(l)+ , c : int+ ) : [ l2 : addr | l+m > l2 ] ( bytes_v(l, l2-l)+ ,bytes_v(l2, l+m-l2)+ | ptr(l2)) =+ "mac#atslib_rawmemchr"++(* ****** ****** *)+#define BUFSZ (16*1024)++(* ****** ****** *)+extern+fun freadc {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref+ , p : ptr(l)+ , c : char+ ) : size_t++implement freadc (pf | inp, p, c) =+ let+ var n = $extfcall(size_t, "fread", p, sizeof<char>, BUFSZ - 1, inp)+ val () = $UN.ptr0_set<char>(ptr_add<char>(p, n), c)+ in+ n+ end++(* ****** ****** *)+extern+fun wclbuf {l:addr}{n:int} ( pf : !bytes_v(l, n) | p : ptr(l)+ , pz : ptr+ , c : int+ , res : int+ ) : int++implement wclbuf (pf | p, pz, c, res) =+ let+ val (pf1, pf2 | p2) = rawmemchr(pf | p, c)+ in+ if p2 < pz then+ let+ prval (pf21, pf22) = array_v_uncons(pf2)+ var res = wclbuf(pf22 | ptr_succ<byte>(p2), pz, c, res + 1)+ prval () = pf2 := array_v_cons(pf21, pf22)+ prval () = pf := bytes_v_unsplit(pf1, pf2)+ in+ res+ end+ else+ let+ prval () = pf := bytes_v_unsplit(pf1, pf2)+ in+ res+ end+ end++(* ****** ****** *)+extern+fun wclfil {l:addr} ( pf : !bytes_v(l, BUFSZ) | inp : FILEref+ , p : ptr(l)+ , c : int+ ) : int++implement wclfil {l} (pf | inp, p, c) =+ let+ fun loop( pf : !bytes_v(l, BUFSZ) | inp : FILEref+ , p : ptr(l)+ , c : int+ , res : int+ ) : int =+ let+ val n = freadc(pf | inp, p, $UN.cast{char}(c))+ in+ if n > 0 then+ let+ var pz = ptr_add<char>(p, n)+ var res = wclbuf(pf | p, pz, c, res)+ in+ loop(pf | inp, p, c, res)+ end+ else+ res+ end+ in+ loop(pf | inp, p, c, 0)+ end++(* ****** ****** *)+fun line_count(s : string) : int =+ let+ var inp: FILEref = fopen_ref_exn(s, file_mode_r)+ val (pfat, pfgc | p) = malloc_gc(g1i2u(BUFSZ))+ prval () = pfat := b0ytes2bytes_v(pfat)+ var res = wclfil(pfat | inp, p, $UN.cast2int('\n'))+ val () = mfree_gc(pfat, pfgc | p)+ in+ res+ end