language-ats 1.7.0.5 → 1.7.0.6

raw patch · 6 files changed

+290/−41 lines, 6 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• LICENSE +1/−1
• language-ats.cabal +38/−38
• src/Language/ATS/Parser.y +3/−2
• test/data/levenshtein3.dats +120/−0
• test/data/levenshtein3.out +124/−0

@@ -1,5 +1,9 @@ # language-ats +## 1.7.0.6++  * Fix bug by introducing immorality+ ## 1.7.0.5    * Faster build times

@@ -1,4 +1,4 @@-Copyright Vanessa McHale (c) 2018+Copyright Vanessa McHale (c) 2018-2019  Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 

@@ -1,17 +1,17 @@-cabal-version:   1.18-name:            language-ats-version:         1.7.0.5-license:         BSD3-license-file:    LICENSE-copyright:       Copyright: (c) 2018 Vanessa McHale-maintainer:      vamchale@gmail.com-author:          Vanessa McHale-stability:       stable-synopsis:        Parser and pretty-printer for ATS.+cabal-version: 1.18+name: language-ats+version: 1.7.0.6+license: BSD3+license-file: LICENSE+copyright: Copyright: (c) 2018-2019 Vanessa McHale+maintainer: vamchale@gmail.com+author: Vanessa McHale+stability: stable+synopsis: Parser and pretty-printer for ATS. description:     Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.-category:        Language, Lexer, Parser, Pretty Printer, ATS-build-type:      Simple+category: Language, Lexer, Parser, Pretty Printer, ATS+build-type: Simple data-files:     test/data/*.dats     test/data/*.sats@@ -20,23 +20,24 @@     test/data/stdlib/*.out     test/data/stdlib/DATS/*.dats     test/data/stdlib/DATS/*.out-extra-doc-files:-    README.md-    CHANGELOG.md+extra-doc-files: README.md+                 CHANGELOG.md  source-repository head-    type:     darcs+    type: darcs     location: https://hub.darcs.net/vmchale/ats  flag development-    description: Enable `-Werror`-    default:     False-    manual:      True+    description:+        Enable `-Werror`+    default: False+    manual: True  library-    exposed-modules:  Language.ATS-    build-tools:      happy >=1.17.1, alex -any-    hs-source-dirs:   src+    exposed-modules:+        Language.ATS+    build-tools: happy >=1.17.1, alex -any+    hs-source-dirs: src     other-modules:         Language.ATS.Lexer         Language.ATS.Parser@@ -45,12 +46,11 @@         Language.ATS.Types.Lens         Language.ATS.Rewrite     default-language: Haskell2010-    other-extensions:-        OverloadedStrings DeriveGeneric DeriveAnyClass FlexibleContexts-        PatternSynonyms StandaloneDeriving GeneralizedNewtypeDeriving-        DerivingStrategies DuplicateRecordFields DeriveFunctor-        ScopedTypeVariables-    ghc-options:      -Wall -O2+    other-extensions: OverloadedStrings DeriveGeneric DeriveAnyClass+                      FlexibleContexts PatternSynonyms StandaloneDeriving+                      GeneralizedNewtypeDeriving DerivingStrategies DuplicateRecordFields+                      DeriveFunctor ScopedTypeVariables+    ghc-options: -Wall -O2     build-depends:         base >=4.9 && <5,         array -any,@@ -66,15 +66,15 @@         ghc-options: -Werror      if impl(ghc >=8.0)-        ghc-options:-            -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat+        ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates+                     -Wcompat  test-suite language-ats-test-    type:             exitcode-stdio-1.0-    main-is:          Spec.hs-    hs-source-dirs:   test+    type: exitcode-stdio-1.0+    main-is: Spec.hs+    hs-source-dirs: test     default-language: Haskell2010-    ghc-options:      -threaded -rtsopts -with-rtsopts=-N -Wall+    ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall     build-depends:         base -any,         language-ats -any,@@ -89,11 +89,11 @@         ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates  benchmark language-ats-bench-    type:             exitcode-stdio-1.0-    main-is:          Bench.hs-    hs-source-dirs:   bench+    type: exitcode-stdio-1.0+    main-is: Bench.hs+    hs-source-dirs: bench     default-language: Haskell2010-    ghc-options:      -Wall -O2+    ghc-options: -Wall -O2     build-depends:         base -any,         language-ats -any,

@@ -431,6 +431,7 @@ Expression :: { Expression AlexPosn }            : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }            | PreExpression { $1 }+           | openParen PreExpression comma PreExpression vbar PreExpression closeParen { ProofExpr $1 ($2 :| [$4]) $6 }            | openParen comma_sep(PreExpression) vbar PreExpression closeParen { ProofExpr $1 $2 $4 }            | Expression semicolon Expression { Precede $1 $3 }            | Expression semicolon { $1 }@@ -744,7 +745,7 @@               | lbrace {% left $ Expected $1 "Expression" "{" }  OptStaticExpression :: { Maybe (StaticExpression AlexPosn) }-OptStaticExpression : { Nothing }+                    : { Nothing }                     | eq StaticExpression { Just $2 }  -- | Parse a constructor for a 'dataprop'@@ -756,7 +757,7 @@  -- | Parse several constructors for a 'dataprop' DataPropLeaves :: { [DataPropLeaf AlexPosn] }-DataPropLeaves : DataPropLeaf { [$1] }+               : DataPropLeaf { [$1] }                | DataPropLeaves DataPropLeaf { $2 : $1 }                | lineComment { [] }                | DataPropLeaves lineComment { $1 }

@@ -0,0 +1,120 @@+staload UN = "prelude/SATS/unsafe.sats"+staload "./../SATS/edit-distance.sats"++implement {a} array_ptr_alloca {dummy}{n} (asz) =+  let+    val [l:addr](pf, fpf | p) = alloca(asz * sizeof<a>)+    prval pf = __assert(pf) where+    { extern+      praxi __assert(pf : b0ytes(n*sizeof(a)) @ l) : array_v(a?, l, n) }+    prval fpf = __assertfn(fpf) where+    { extern+      praxi __assertfn(fpf : b0ytes(n*sizeof(a)) @ l -> void @ dummy) : array_v(a?, l, n) -> void @ dummy }+  in+    (pf, fpf | p)+  end++// Ported over from+// https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+//+// With contributions from Hongwei Xi and Artyom Shalkhakov+implement levenshtein {m,n} (s1, s2) =+  let+    val s1_l+      : size_t(m) = length(s1)+    val s2_l: size_t(n) = length(s2)+    +    fn array_initialize() : arrayref(int, m+1) =+      let+        +#ifdef ALLOCA+        val (pf_arr, fpf | p_arr) = array_ptr_alloca<int>(succ(s1_l))+#else+        val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))+#endif+        var p1_arr = ptr1_succ<int>(p_arr)+        prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)+        val () = ptr_set<int>(pf1_at | p_arr, 0)+        var i: int = 0+        prval [l:addr]EQADDR () = eqaddr_make_ptr(p1_arr)+        var p = p1_arr+        prvar pf0 = array_v_nil{int}()+        prvar pf1 = pf_arr+        val () = while* { i : nat | i <= m } .<m-i>. ( i : int(i)+                                                     , p : ptr(l+i*sizeof(int))+                                                     , pf0 : array_v(int, l, i)+                                                     , pf1 : array_v(int?, l+i*sizeof(int), m-i)+                                                     ) : ( pf0 : array_v(int, l, m)+                                                         , pf1 : array_v(int?, l+i*sizeof(int), 0)+                                                         ) =>+            (i < sz2i(s1_l))+            {+              prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)+              prval () = pf1 := pf1_res+              var c = g0ofg1(i)+              val () = ptr_set<int>(pf_at | p, c)+              val () = p := ptr1_succ<int>(p)+              prval () = pf0 := array_v_extend{int}(pf0,pf_at)+              val () = i := i + 1+            }+        prval () = pf_arr := pf0+        prval () = array_v_unnil{int?}(pf1)+        prval pf_arr = array_v_cons{int}(pf1_at,pf_arr)+        +#ifdef ALLOCA+        var res = arrayptr_alloca_encode(pf_arr | p_arr)+#else+        var res = arrayptr_encode(pf_arr, pf_gc | p_arr)+#endif+      in+        arrayptr_refize(res)+      end+    +    val column = array_initialize()+    +    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) : void =+      if x <= sz2i(s2_l) then+        {+          val () = column[0] := x+          val () = let+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. (y : int(j), last_diag : int) : void =+              if y <= sz2i(s1_l) then+                let+                  fn min_3(x : int, y : int, z : int) : int =+                    min(x, (min(y, z)))+                  +                  fn bool2int(x : char, y : char) : int =+                    if x = y then+                      0+                    else+                      1+                  +                  var old_diag = column[y]+                  val () = column[y] := min_3( column[y] + 1+                                             , column[y - 1] + 1+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])+                                             )+                in+                  inner_loop(y + 1, old_diag)+                end+          in+            inner_loop(1, x - 1)+          end+          val () = loop2(x + 1)+        }+    +    val () = loop2(1)+  in+    column[s1_l]+  end++implement levenshtein_ (s1, s2) =+  let+    extern+    castfn witness(s : string) : [m:nat] string(m)+  in+    levenshtein(witness(s1), witness(s2))+  end++implement levenshtein_vt {m}{n} (s1, s2) =+  levenshtein{m,n}($UN.castvwtp1(s1), $UN.castvwtp1(s2))

@@ -0,0 +1,124 @@+staload UN = "prelude/SATS/unsafe.sats"+staload "./../SATS/edit-distance.sats"++implement {a} array_ptr_alloca {dummy}{n} (asz) =+  let+    val [l:addr](pf, fpf | p) = alloca(asz * sizeof<a>)+    prval pf = __assert(pf) where+    { extern+      praxi __assert(pf : b0ytes(n*sizeof(a)) @ l) : array_v(a?, l, n) }+    prval fpf = __assertfn(fpf) where+    { extern+      praxi __assertfn(fpf : b0ytes(n*sizeof(a)) @ l -> void @ dummy) :+        array_v(a?, l, n) -> void @ dummy }+  in+    (pf, fpf | p)+  end++// Ported over from+// https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C+//+// With contributions from Hongwei Xi and Artyom Shalkhakov+implement levenshtein {m,n} (s1, s2) =+  let+    val s1_l+      : size_t(m) = length(s1)+    val s2_l: size_t(n) = length(s2)+    +    fn array_initialize() : arrayref(int, m+1) =+      let+        +#ifdef ALLOCA+        val (pf_arr, fpf | p_arr) = array_ptr_alloca<int>(succ(s1_l))+#else+        val (pf_arr, pf_gc | p_arr) = array_ptr_alloc<int>(succ(s1_l))+#endif+        var p1_arr = ptr1_succ<int>(p_arr)+        prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr)+        val () = ptr_set<int>(pf1_at | p_arr, 0)+        var i: int = 0+        prval [l:addr]EQADDR () = eqaddr_make_ptr(p1_arr)+        var p = p1_arr+        prvar pf0 = array_v_nil{int}()+        prvar pf1 = pf_arr+        val () = while* { i : nat | i <= m } .<m-i>. ( i : int(i)+                                                     , p : ptr(l+i*sizeof(int))+                                                     , pf0 : array_v(int, l, i)+                                                     , pf1 : array_v(int?, l+i*sizeof(int), m-i)+                                                     ) : ( pf0 : array_v(int, l, m)+                                                         , pf1 : array_v(int?, l+i*sizeof(int), 0)+                                                         ) =>+            (i < sz2i(s1_l))+            {+              prval (pf_at, pf1_res) = array_v_uncons{int?}(pf1)+              prval () = pf1 := pf1_res+              var c = g0ofg1(i)+              val () = ptr_set<int>(pf_at | p, c)+              val () = p := ptr1_succ<int>(p)+              prval () = pf0 := array_v_extend{int}(pf0,pf_at)+              val () = i := i + 1+            }+        prval () = pf_arr := pf0+        prval () = array_v_unnil{int?}(pf1)+        prval pf_arr = array_v_cons{int}(pf1_at,pf_arr)+        +#ifdef ALLOCA+        var res = arrayptr_alloca_encode(pf_arr | p_arr)+#else+        var res = arrayptr_encode(pf_arr, pf_gc | p_arr)+#endif+      in+        arrayptr_refize(res)+      end+    +    val column = array_initialize()+    +    fun loop2 { i : nat | i > 0 && i <= n+1 } .<n-i+1>. (x : int(i)) :+      void =+      if x <= sz2i(s2_l) then+        {+          val () = column[0] := x+          val () = let+            fun inner_loop { j : nat | j > 0 && j <= m+1 } .<m-j+1>. ( y : int(j)+                                                                     , last_diag : int+                                                                     ) : void =+              if y <= sz2i(s1_l) then+                let+                  fn min_3(x : int, y : int, z : int) : int =+                    min(x, (min(y, z)))+                  +                  fn bool2int(x : char, y : char) : int =+                    if x = y then+                      0+                    else+                      1+                  +                  var old_diag = column[y]+                  val () = column[y] := min_3( column[y] + 1+                                             , column[y - 1] + 1+                                             , last_diag + bool2int(s1[y - 1], s2[x - 1])+                                             )+                in+                  inner_loop(y + 1, old_diag)+                end+          in+            inner_loop(1, x - 1)+          end+          val () = loop2(x + 1)+        }+    +    val () = loop2(1)+  in+    column[s1_l]+  end++implement levenshtein_ (s1, s2) =+  let+    extern+    castfn witness(s : string) : [m:nat] string(m)+  in+    levenshtein(witness(s1), witness(s2))+  end++implement levenshtein_vt {m}{n} (s1, s2) =+  levenshtein{m,n}($UN.castvwtp1(s1), $UN.castvwtp1(s2))