diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # language-ats +## 1.7.0.6 + + * Fix bug by introducing immorality + ## 1.7.0.5 * Faster build times diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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: diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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, diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 } diff --git a/test/data/levenshtein3.dats b/test/data/levenshtein3.dats new file mode 100644 --- /dev/null +++ b/test/data/levenshtein3.dats @@ -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) + 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(succ(s1_l)) +#else + val (pf_arr, pf_gc | p_arr) = array_ptr_alloc(succ(s1_l)) +#endif + var p1_arr = ptr1_succ(p_arr) + prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr) + val () = ptr_set(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 } .. ( 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(pf_at | p, c) + val () = p := ptr1_succ(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 } .. (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 } .. (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)) diff --git a/test/data/levenshtein3.out b/test/data/levenshtein3.out new file mode 100644 --- /dev/null +++ b/test/data/levenshtein3.out @@ -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) + 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(succ(s1_l)) +#else + val (pf_arr, pf_gc | p_arr) = array_ptr_alloc(succ(s1_l)) +#endif + var p1_arr = ptr1_succ(p_arr) + prval (pf1_at, pf_arr) = array_v_uncons{int?}(pf_arr) + val () = ptr_set(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 } .. ( 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(pf_at | p, c) + val () = p := ptr1_succ(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 } .. (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 } .. ( 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))