language-ats 1.7.4.1 → 1.7.5.0

raw patch · 8 files changed

+320/−25 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• language-ats.cabal +1/−1
• src/Language/ATS/Parser.y +12/−11
• src/Language/ATS/PrettyPrint.hs +20/−10
• src/Language/ATS/Rewrite.hs +1/−1
• src/Language/ATS/Types.hs +2/−2
• test/data/wc.dats +132/−0
• test/data/wc.out +148/−0

@@ -1,5 +1,9 @@ # language-ats +## 1.7.5.0++  * Fix `StaticExpression` to allow calls with dynamic components+ ## 1.7.4.1    * Improve pretty-printer

@@ -1,6 +1,6 @@ cabal-version:   1.18 name:            language-ats-version:         1.7.4.1+version:         1.7.5.0 license:         BSD3 license-file:    LICENSE copyright:       Copyright: (c) 2018-2019 Vanessa McHale

@@ -465,8 +465,9 @@      | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"}      | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"} -StaticArgs :: { [StaticExpression AlexPosn] }-           : comma_sep(StaticExpression) { reverse (toList $1) }+StaticArgs :: { ([StaticExpression AlexPosn], Maybe [Expression AlexPosn]) }+           : comma_sep(StaticExpression) { (reverse (toList $1), Nothing) }+           | comma_sep(StaticExpression) vbar comma_sep(Expression) { (reverse (toList $1), Just $ reverse (toList $3)) }  StaticDecls :: { [Declaration AlexPosn] }             : StaticDeclaration { [$1] }@@ -483,15 +484,15 @@                  | doubleParens { StaticVoid $1 } -- TODO: static tuple?                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }-                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [] [$2] }-                 | Name parens(StaticArgs) { SCall $1 [] [] $2 }-                 | Name Implicits parens(StaticArgs) { SCall $1 $2 [] $3 }-                 | Name TypeArgs parens(StaticArgs) { SCall $1 [] $2 $3 }-                 | Name TypeArgs doubleParens { SCall $1 [] $2 [] }-                 | Name doubleParens { SCall $1 [] [] [] }-                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 $3 }-                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] [] $2 }-                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] [] } -- TODO: this causes an ambiguity because we might have SCall void instead!+                 | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [] [] [$2] Nothing }+                 | Name parens(StaticArgs) { SCall $1 [] [] (fst $2) (snd $2) }+                 | Name Implicits parens(StaticArgs) { SCall $1 $2 [] (fst $3) (snd $3) }+                 | Name TypeArgs parens(StaticArgs) { SCall $1 [] $2 (fst $3) (snd $3) }+                 | Name TypeArgs doubleParens { SCall $1 [] $2 [] Nothing }+                 | Name doubleParens { SCall $1 [] [] [] Nothing }+                 | identifierSpace TypeArgs parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] $2 (fst $3) (snd $3) }+                 | identifierSpace parens(StaticArgs) { SCall (Unqualified $ to_string $1) [] [] (fst $2) (snd $2) }+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] [] [] Nothing } -- TODO: this causes an ambiguity because we might have SCall void instead!                  | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }                  | UnOp StaticExpression { SUnary $1 $2 }                  | let StaticDecls comment_after(in) end { SLet $1 (reverse $2) Nothing }

@@ -278,14 +278,18 @@         a (StaticHexF h)               = text h         a StaticVoidF{}                = "()"         a (SifF e e' e'')              = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (SCallF n [] [] ["()"])      = pretty n <> "()"-        a (SCallF n [] us ["()"])      = pretty n <> prettyTypes us <> "()"-        a (SCallF n [] [] cs)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))-        a (SCallF n [] us cs)          = pretty n <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))-        a (SCallF n is [] ["()"])      = pretty n <> prettyImplicits is <> "()"-        a (SCallF n is us ["()"])      = pretty n <> prettyImplicits is <> prettyTypes us <> "()"-        a (SCallF n is [] cs)          = pretty n <> prettyImplicits is <> parens (mconcat (punctuate "," . fmap pretty $ cs))-        a (SCallF n is us cs)          = pretty n <> prettyImplicits is <> prettyTypes us <> parens (mconcat (punctuate "," . fmap pretty $ cs))+        a (SCallF n [] [] ["()"] Nothing)      = pretty n <> "()"+        a (SCallF n [] us ["()"] Nothing)      = pretty n <> prettyTypes us <> "()"+        a (SCallF n [] [] cs Nothing)          = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))+        a (SCallF n [] us cs Nothing)          = pretty n <> prettyTypes us <> parens (commaTight cs)+        a (SCallF n is [] ["()"] Nothing)      = pretty n <> prettyImplicits is <> "()"+        a (SCallF n is us ["()"] Nothing)      = pretty n <> prettyImplicits is <> prettyTypes us <> "()"+        a (SCallF n is [] cs Nothing)          = pretty n <> prettyImplicits is <> parens (commaTight cs)+        a (SCallF n is us cs Nothing)          = pretty n <> prettyImplicits is <> prettyTypes us <> parens (commaTight cs)+        a (SCallF n [] [] cs (Just ds))        = pretty n <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)+        a (SCallF n [] us cs (Just ds))        = pretty n <> prettyTypes us <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)+        a (SCallF n is [] cs (Just ds))        = pretty n <> prettyImplicits is <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)+        a (SCallF n is us cs (Just ds))        = pretty n <> prettyImplicits is <> prettyTypes us <> parens (commaTight cs <+> "|" <+> commaTightDyn ds)         a (SPrecedeF e e')             = e <> ";" <+> e'         a (SPrecedeListF es)           = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")         a (SParensF e)                 = parens e@@ -300,6 +304,12 @@         a (ProofLinearLambdaF _ lt p e) = prettyLam "llam" p lt e         a (WhereStaExpF e ds) = prettyWhere e ds +        commaTight :: [Doc] -> Doc+        commaTight = mconcat . punctuate ","++        commaTightDyn :: Pretty b => [b] -> Doc+        commaTightDyn = commaTight . fmap pretty+ instance Eq a => Pretty (Sort a) where     pretty = cata a where         a (T0pF ad)           = "t@ype" <> pretty ad@@ -396,9 +406,9 @@ isVal _         = False  isOverload :: Declaration a -> Bool-isOverload OverloadOp{} = True+isOverload OverloadOp{}    = True isOverload OverloadIdent{} = True-isOverload _ = False+isOverload _               = False  -- isTypeDef :: Declaration a -> Bool -- isTypeDef ViewTypeDef{} = True

@@ -86,7 +86,7 @@  rewriteStaATS :: Eq a => FixityState a -> StaticExpression a -> StaticExpression a rewriteStaATS st = cata a where-    a (SCallF n is ts [StaticVoid{}]) = SCall n is ts []+    a (SCallF n is ts [StaticVoid{}] dyn) = SCall n is ts [] dyn     a (StaticBinaryF op (StaticBinary op' e e') e'')         | compareFixity st op op'  = StaticBinary op e (StaticBinary op' e' e'')     a (WhereStaExpF se (ATS ds))   = WhereStaExp se (ATS (rewriteDecl st <$> ds))

@@ -314,7 +314,7 @@                         | SPrecedeList { _sExprs :: [StaticExpression a] }                         | StaticVoid a                         | Sif { scond :: StaticExpression a, whenTrue :: StaticExpression a, selseExpr :: StaticExpression a } -- Static if (for proofs)-                        | SCall (Name a) [[Type a]] [[Type a]] [StaticExpression a]+                        | SCall (Name a) [[Type a]] [[Type a]] [StaticExpression a] (Maybe [Expression a])                         | SUnary (UnOp a) (StaticExpression a)                         | SLet a [Declaration a] (Maybe (StaticExpression a))                         | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)]@@ -334,7 +334,7 @@                            | SPrecedeListF [x]                            | StaticVoidF a                            | SifF x x x-                           | SCallF (Name a) [[Type a]] [[Type a]] [x]+                           | SCallF (Name a) [[Type a]] [[Type a]] [x] (Maybe [Expression a])                            | SUnaryF (UnOp a) x                            | SLetF a [Declaration a] (Maybe x)                            | SCaseF Addendum x [(Pattern a, LambdaType a, x)]

@@ -0,0 +1,132 @@+staload "SATS/wc.sats"+staload UN = "prelude/SATS/unsafe.sats"++%{+size_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {+  return ((char *)p1 - (char *)p2);+}+%}++extern+fn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }(p1 : ptr(l0), p2 : ptr(l1)) :<> size_t(l0-l1) =+  "ext#"++// bad (?) idea: use rawmemchr + append lol+extern+fn memchr { l : addr | l != null }{m:nat}{ n : nat | n <= m }(bytes_v(l,m) | ptr(l), int, size_t(n)) :+  [ l0 : addr | l0 == null || l0 >= l && l0-l <= m ] (bytes_v(l, l0-l), bytes_v(l0, l+m-l0)| ptr(l0)) =+  "mac#"++extern+fn memchr2 { l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m) | ptr(l), char, char, size_t(n)) :+  Option_vt([ k : nat | k <= n ] size_t(k)) =+  "ext#"++extern+fn memchr3 { l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m) | ptr(l), char, char, char, size_t(n)) :+  Option_vt([ k : nat | k <= n ] size_t(k)) =+  "ext#"++fn freadc_ {l:addr}{ sz : nat | sz > 0 }{ n : nat | n <= sz }(pf : !bytes_v(l, sz)+                                                             | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) :+  size_t(n) =+  let+    extern+    castfn as_fileref(x : !FILEptr1) :<> FILEref+    +    var n = $extfcall(size_t(n), "fread", p, sizeof<byte>, bufsize - 1, as_fileref(inp))+  in+    n+  end++extern+fn count_char { l : addr | l != null }{m:nat}(!bytes_v(l, m) | ptr(l), c : char, bufsz : size_t(m)) :+  [ n : nat | n <= m ] int(n) =+  "ext#"++fn count_lines { l : addr | l != null }{m:nat}(pf : !bytes_v(l, m) | p : ptr(l), bufsz : size_t(m)) :+  [ n : nat | n <= m ] int(n) =+  count_char(pf | p, '\n', bufsz)++implement empty_file =+  @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file++implement free_st (st) =+  case+ st of+    | ~in_string (_) => ()+    | ~in_block_comment (_) => ()+    | ~line_comment() => ()+    | ~regular() => ()++(* fun charptr1_add_guint{l:addr}{i:int}(p:ptr(l), offsz: size_t(i)) :<> ptr(l+i) = *)++implement count_buf (pf | ptr, bufsz, st) =+  case+ st of+    | ~in_string (n) => let+      // 34 -> "+      val (pf0, pf1 | p2) = memchr(pf | ptr, 34, bufsz)+    in+      if ptr_is_null(p2) then+        let+          prval () = pf := bytes_v_unsplit(pf0,pf1)+          var strlines = count_lines(pf | ptr, bufsz)+          val () = st := in_string(n + strlines)+        in+          empty_file+        end+      else+        let+          //TODO: check that p2's predecessor is not a backslash+          var pred_is_slash = if p2 > ptr then+            let+              val () = print(p2)+            in+              // 92 -> \+              ptr1_pred<byte>(p2) = $UN.cast(92)+            end+          else+            false+          var bytes_taken = sub_ptr1_ptr1_size(p2, ptr)+          var strlines = count_lines(pf0 | ptr, bytes_taken)+          var in_str = strlines + n+          var bytes_remaining = bufsz - bytes_taken+          val () = st := regular()+          var ret_file: file+          val () = ret_file := count_buf(pf1 | p2, bytes_remaining, st)+          val () = ret_file.lines := ret_file.lines + strlines+          prval () = pf := bytes_v_unsplit(pf0,pf1)+        in+          ret_file+        end+    end+    | in_block_comment (_) => empty_file+    | line_comment () => empty_file+    | regular() => let+      val next_char_offset = memchr3(pf | ptr, '\n', '"', '/', bufsz)+      val ret = case+ next_char_offset of+        | ~Some_vt (char_ptr_off) => let+          var char_ptr = add_ptr_bsz(ptr, char_ptr_off)+          var char_val = $UN.ptr0_get<char>(char_ptr)+          +          extern+          praxi ptr_eq { l0, l1 : addr }{m:nat} (pf : !bytes_v(l0, m) | ptr(l1)) : [l0 == l1 && l0 != null] void+          +          var ret_file = case- char_val of+            | '\n' => let+              prval (pf0, pf1) = bytes_v_split_at(pf | char_ptr_off)+              prval () = ptr_eq(pf1 | char_ptr)+              var bytes_remaining = bufsz - char_ptr_off+              var ret_file: file+              val () = ret_file := count_buf(pf1 | char_ptr, bytes_remaining, st)+              prval () = pf := bytes_v_unsplit(pf0,pf1)+            in+              ret_file+            end+            | _ => empty_file+        in+          ret_file+        end+        | ~None_vt() => empty_file+    in+      ret+    end

@@ -0,0 +1,148 @@+staload "SATS/wc.sats"+staload UN = "prelude/SATS/unsafe.sats"++%{+size_t sub_ptr1_ptr1_size(atstype_ptr p1, atstype_ptr p2) {+  return ((char *)p1 - (char *)p2);+}+%}++extern+fn sub_ptr1_ptr1_size { l0, l1 : addr | l0 >= l1 }( p1 : ptr(l0)+                                                  , p2 : ptr(l1)+                                                  ) :<> size_t(l0-l1) =+  "ext#"++// bad (?) idea: use rawmemchr + append lol+extern+fn memchr+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(bytes_v(l,m)+                                                   | ptr(l), int, size_t(n)) :+  [ l0 : addr | l0 == null || l0 >= l && l0-l <= m ] ( bytes_v(l, l0-l)+                                                     , bytes_v(l0, l+m-l0)+                                                     | ptr(l0)) =+  "mac#"++extern+fn memchr2+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m)+                                                   | ptr(l), char, char, size_t(n)) :+  Option_vt([ k : nat | k <= n ] size_t(k)) =+  "ext#"++extern+fn memchr3+{ l : addr | l != null }{m:nat}{ n : nat | n <= m }(!bytes_v(l, m)+                                                   | ptr(l), char, char, char, size_t(n)) :+  Option_vt([ k : nat | k <= n ] size_t(k)) =+  "ext#"++fn freadc_+{l:addr}{ sz : nat | sz > 0 }{ n : nat | n <= sz }(pf : !bytes_v(l, sz)+                                                  | inp : !FILEptr1, bufsize : size_t(sz), p : ptr(l)) : size_t(n) =+  let+    extern+    castfn as_fileref(x : !FILEptr1) :<> FILEref+    +    var n = $extfcall( size_t(n)+                     , "fread"+                     , p+                     , sizeof<byte>+                     , bufsize - 1+                     , as_fileref(inp)+                     )+  in+    n+  end++extern+fn count_char { l : addr | l != null }{m:nat}(!bytes_v(l, m)+                                             | ptr(l), c : char, bufsz : size_t(m)) : [ n : nat | n <= m ] int(n) =+  "ext#"++fn count_lines { l : addr | l != null }{m:nat}(pf : !bytes_v(l, m)+                                              | p : ptr(l), bufsz : size_t(m)) : [ n : nat | n <= m ] int(n) =+  count_char(pf | p, '\n', bufsz)++implement empty_file =+  @{ lines = 0, blanks = 0, comments = 0, doc_comments = 0 } : file++implement free_st (st) =+  case+ st of+    | ~in_string (_) => ()+    | ~in_block_comment (_) => ()+    | ~line_comment() => ()+    | ~regular() => ()++(* fun charptr1_add_guint{l:addr}{i:int}(p:ptr(l), offsz: size_t(i)) :<> ptr(l+i) = *)+implement count_buf (pf | ptr, bufsz, st) =+  case+ st of+    | ~in_string (n) => let+      // 34 -> "+      val (pf0, pf1 | p2) = memchr(pf | ptr, 34, bufsz)+    in+      if ptr_is_null(p2) then+        let+          prval () = pf := bytes_v_unsplit(pf0,pf1)+          var strlines = count_lines(pf | ptr, bufsz)+          val () = st := in_string(n + strlines)+        in+          empty_file+        end+      else+        let+          //TODO: check that p2's predecessor is not a backslash+          var pred_is_slash = if p2 > ptr then+            let+              val () = print(p2)+            in+              // 92 -> \+              ptr1_pred<byte>(p2) = $UN.cast(92)+            end+          else+            false+          var bytes_taken = sub_ptr1_ptr1_size(p2, ptr)+          var strlines = count_lines(pf0 | ptr, bytes_taken)+          var in_str = strlines + n+          var bytes_remaining = bufsz - bytes_taken+          val () = st := regular()+          var ret_file: file+          val () = ret_file := count_buf(pf1 | p2, bytes_remaining, st)+          val () = ret_file.lines := ret_file.lines + strlines+          prval () = pf := bytes_v_unsplit(pf0,pf1)+        in+          ret_file+        end+    end+    | in_block_comment (_) => empty_file+    | line_comment () => empty_file+    | regular() => let+      val next_char_offset = memchr3(pf | ptr, '\n', '"', '/', bufsz)+      val ret = case+ next_char_offset of+        | ~Some_vt (char_ptr_off) => let+          var char_ptr = add_ptr_bsz(ptr, char_ptr_off)+          var char_val = $UN.ptr0_get<char>(char_ptr)+          +          extern+          praxi ptr_eq { l0, l1 : addr }{m:nat} (pf : !bytes_v(l0, m) | ptr(l1)) :+            [l0 == l1 && l0 != null] void+          +          var ret_file = case- char_val of+            | '\n' => let+              prval (pf0, pf1) = bytes_v_split_at(pf | char_ptr_off)+              prval () = ptr_eq(pf1 | char_ptr)+              var bytes_remaining = bufsz - char_ptr_off+              var ret_file: file+              val () = ret_file := count_buf(pf1 | char_ptr, bytes_remaining, st)+              prval () = pf := bytes_v_unsplit(pf0,pf1)+            in+              ret_file+            end+            | _ => empty_file+        in+          ret_file+        end+        | ~None_vt() => empty_file+    in+      ret+    end