language-ats 1.7.1.2 → 1.7.2.0

raw patch · 8 files changed

+130/−72 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 +44/−41
• src/Language/ATS.hs +2/−1
• src/Language/ATS/Parser.y +14/−8
• src/Language/ATS/PrettyPrint.hs +25/−21
• src/Language/ATS/Types.hs +1/−1
• test/data/ifact2.dats +19/−0
• test/data/ifact2.out +21/−0

@@ -1,5 +1,9 @@ # language-ats +## 1.7.2.0++  * Update `termetric` field type to allow empty termetrics+ ## 1.7.1.2    * Add `cross` flag to cabal file

@@ -1,17 +1,18 @@-cabal-version: 1.18-name: language-ats-version: 1.7.1.2-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.+cabal-version:   1.18+name:            language-ats+version:         1.7.2.0+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,29 +21,28 @@     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 cross-    description:-        Set this flag if cross-compiling-    default: False-    manual: True+    description: Set this flag if cross-compiling+    default:     False+    manual:      True  flag development-    description:-        Enable `-Werror`-    default: False-    manual: True+    description: Enable `-Werror`+    default:     False+    manual:      True  library-    exposed-modules:-        Language.ATS-    hs-source-dirs: src+    exposed-modules:  Language.ATS+    hs-source-dirs:   src     other-modules:         Language.ATS.Lexer         Language.ATS.Parser@@ -50,12 +50,15 @@         Language.ATS.Types         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,@@ -74,15 +77,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,@@ -97,11 +100,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,

@@ -61,6 +61,7 @@                     , typeCallArgs                     ) where +import           Control.Composition          ((-$)) import           Control.Monad import           Control.Monad.IO.Class import           Control.Monad.Trans.State@@ -108,7 +109,7 @@ -- | Parse with some fixity declarations already in scope. parseWithCtx :: FixityState AlexPosn -> ([Token] -> [Token]) -> String -> Either ATSError (ATS AlexPosn) parseWithCtx st p = stateParse <=< lex'-    where withSt = flip runStateT st+    where withSt = runStateT -$ st           lex' = lexErr . fmap p . lexATS           stateParse = fmap rewriteATS' . withSt . parseATS 

@@ -15,6 +15,7 @@ import qualified Data.Map as M import Control.Monad.Trans.Class import Control.Monad.Trans.State+import Data.Bifunctor (second) import Data.Char (toLower) import Data.List.NonEmpty (NonEmpty (..)) import Data.Foldable (toList)@@ -167,6 +168,7 @@     neq { Operator $$ "!=" }     openTermetric { Operator $$ ".<" }     closeTermetric { Operator $$ ">." }+    emptyTermetric { Operator $$ ".<>." }     mutateArrow { FuncType $$ "->" }     mutateEq { Operator $$ ":=" }     lbracket { Special $$ "<" }@@ -536,9 +538,9 @@               | braces(ATS) { Actions $1 }               | while parens(PreExpression) PreExpression { While $1 $2 $3 }               | for parens(PreExpression) PreExpression { For $1 $2 $3 }-              | whileStar Universals Termetric parens(Args) plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $6 $7 Nothing }-              | whileStar Universals Termetric parens(Args) colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $10 $11 (Just $7) }-              | forStar Universals Termetric parens(Args) plainArrow Expression Expression { ForStar $1 $2 (snd $3) $4 $6 $7 }+              | whileStar Universals PreTermetric parens(Args) plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $6 $7 Nothing }+              | whileStar Universals PreTermetric parens(Args) colon openParen Args closeParen plainArrow Expression Expression { WhileStar $1 $2 (snd $3) $4 $10 $11 (Just $7) }+              | forStar Universals PreTermetric parens(Args) plainArrow Expression Expression { ForStar $1 $2 (snd $3) $4 $6 $7 }               | lineComment PreExpression { CommentExpr (to_string $1) $2 }               | comma parens(identifier) { MacroVar $1 (to_string $2) }               | PreExpression where braces(ATS) { WhereExp $1 $3 }@@ -563,11 +565,15 @@               | begin Expression implement {% left $ Expected $3 "end" "implement" }  -- | Parse a termetric-Termetric :: { (AlexPosn, StaticExpression AlexPosn) }-          : openTermetric StaticExpression closeTermetric { ($1, $2) }-          | underscore {% left $ Expected $1 "_" "Termination metric" }-          | dollar {% left $ Expected $1 "$" "Termination metric" }+PreTermetric :: { (AlexPosn, (StaticExpression AlexPosn)) }+             : openTermetric StaticExpression closeTermetric { ($1, $2) }+             | underscore {% left $ Expected $1 "_" "Termination metric" }+             | dollar {% left $ Expected $1 "$" "Termination metric" } +Termetric :: { (AlexPosn, Maybe (StaticExpression AlexPosn)) }+          : PreTermetric { second Just $1 }+          | emptyTermetric { ($1, Nothing) }+ Sort :: { Sort AlexPosn }      : t0pPlain { T0p None }      | t0pCo { T0p Plus }@@ -699,7 +705,7 @@            : PreUniversals { reverse $1 }  -- | Optionally parse a termetric-OptTermetric :: { Maybe (StaticExpression AlexPosn) }+OptTermetric :: { Maybe (Maybe (StaticExpression AlexPosn)) }              : { Nothing }              | Termetric { Just (snd $1) } 

@@ -216,22 +216,22 @@  instance Eq a => Pretty (Pattern a) where     pretty = cata a where-        a (PSumF s x)                  = string s <+> x-        a (PLiteralF e)                = pretty e-        a (PNameF s [])                = pretty s-        a (PNameF s [x])               = pretty s <> parens x-        a (PNameF s ps)                = pretty s <> parens (patternHelper ps)-        a (FreeF p)                    = "~" <> p-        a (GuardedF _ e p)             = p <+> "when" <+> pretty e-        a (ProofF _ p p')              = parens (patternHelper p <+> "|" <+> patternHelper p')-        a (TuplePatternF ps)           = parens (patternHelper ps)-        a (BoxTuplePatternF _ ps)      = "'(" <> patternHelper ps <> ")"-        a (AtPatternF _ p)             = "@" <> p+        a (PSumF s x)                         = string s <+> x+        a (PLiteralF e)                       = pretty e+        a (PNameF s [])                       = pretty s+        a (PNameF s [x])                      = pretty s <> parens x+        a (PNameF s ps)                       = pretty s <> parens (patternHelper ps)+        a (FreeF p)                           = "~" <> p+        a (GuardedF _ e p)                    = p <+> "when" <+> pretty e+        a (ProofF _ p p')                     = parens (patternHelper p <+> "|" <+> patternHelper p')+        a (TuplePatternF ps)                  = parens (patternHelper ps)+        a (BoxTuplePatternF _ ps)             = "'(" <> patternHelper ps <> ")"+        a (AtPatternF _ p)                    = "@" <> p         a (UniversalPatternF _ n us (Just p)) = text n <> prettyArgsU "" "" us <> p-        a (UniversalPatternF _ n us Nothing) = text n <> prettyArgsU "" "" us-        a (ExistentialPatternF e p)    = pretty e <> p-        a (AsF _ p p')                 = p <+> "as" <+> p'-        a (BinPatternF _ op p p')      = p <+> pretty op <+> p'+        a (UniversalPatternF _ n us Nothing)  = text n <> prettyArgsU "" "" us+        a (ExistentialPatternF e p)           = pretty e <> p+        a (AsF _ p p')                        = p <+> "as" <+> p'+        a (BinPatternF _ op p p')             = p <+> pretty op <+> p'  argHelper :: Eq a => (Doc -> Doc -> Doc) -> Arg a -> Doc argHelper _ (Arg (First s))   = pretty s@@ -353,10 +353,10 @@  instance Eq a => Pretty (Existential a) where     pretty (Existential [] b (Just st) (Just e')) = withHashtag b <> pretty st <> pretty e' <> rbracket-    pretty (Existential [] b Nothing (Just e')) = withHashtag b <> pretty e' <> rbracket-    pretty (Existential [e] b (Just st) Nothing) = withHashtag b <> text e <> ":" <> pretty st <> rbracket-    pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <+> rbracket-    pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <> "|" <+> pretty e <+> rbracket+    pretty (Existential [] b Nothing (Just e'))   = withHashtag b <> pretty e' <> rbracket+    pretty (Existential [e] b (Just st) Nothing)  = withHashtag b <> text e <> ":" <> pretty st <> rbracket+    pretty (Existential bs b st Nothing)          = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <+> rbracket+    pretty (Existential bs b st (Just e))         = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <> "|" <+> pretty e <+> rbracket  instance Eq a => Pretty (Universal a) where     pretty (Universal [x] Nothing []) = lbrace <> text x <> rbrace@@ -551,8 +551,12 @@ prettyTermetric :: Pretty a => a -> Doc prettyTermetric t = softline <> ".<" <> pretty t <> ">." <> softline -prettyMTermetric :: Pretty a => Maybe a -> Doc-prettyMTermetric = maybe mempty prettyTermetric+prettyETermetric :: Pretty a => Maybe a -> Doc+prettyETermetric Nothing  = softline <> ".<>." <> softline+prettyETermetric (Just t) = softline <> ".<" <> pretty t <> ">." <> softline++prettyMTermetric :: Pretty a => Maybe (Maybe a) -> Doc+prettyMTermetric = maybe mempty prettyETermetric  -- FIXME figure out a nicer algorithm for when/how to split lines. instance (Eq a, Pretty (ek a)) => Pretty (PreFunction ek a) where

@@ -499,7 +499,7 @@                              , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type                              , args          :: Args a -- ^ Actual function arguments                              , returnType    :: Maybe (Type a) -- ^ Return type-                             , termetric     :: Maybe (StaticExpression a) -- ^ Optional termination metric+                             , termetric     :: Maybe (Maybe (StaticExpression a)) -- ^ Optional termination metric, which may be empty                              , _expression   :: Maybe (ek a) -- ^ Expression holding the actual function body (not present in static templates)                              }                              deriving (Show, Eq, Generic, NFData)

@@ -0,0 +1,19 @@+fun+ifact2+{n:nat} .<>.+(+  n: int (n)+) :<> [r:int] (FACT(n, r) | int r) = let+  fun loop+    {i:nat|i <= n}{r:int} .<n-i>.+  (+    pf: FACT(i, r)+  | n: int n, i: int i, r: int r+  ) :<> [r:int] (FACT(n, r) | int r) =+    if n - i > 0 then let+      val (pfmul | r1) = imul2 (i+1, r) in loop (FACTind(pf, pfmul) | n, i+1, r1)+    end else (pf | r) // end of [if]+  // end of [loop]+in+  loop (FACTbas() | n, 0, 1)+end // end of [ifact2]

@@ -0,0 +1,21 @@+fun ifact2 {n:nat} .<>. (n : int(n)) :<> [r:int] (FACT(n, r) | int(r)) =+  let+    fun loop { i : nat | i <= n }{r:int} .<n-i>. (pf : FACT(i, r)+                                                 | n : int(n), i : int(i), r : int(r)) :<>+      [r:int] (FACT(n, r) | int(r)) =+      if n - i > 0 then+        let+          val (pfmul | r1) = imul2((i + 1, r))+        in+          loop(FACTind(pf, pfmul) | n, i + 1, r1)+        end+      else+        (pf | r)+    +    // end of [if]+    // end of [loop]+  in+    loop(FACTbas() | n, 0, 1)+  end++// end of [ifact2]