packages feed

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 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