diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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, diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -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 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 @@ -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) } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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) diff --git a/test/data/ifact2.dats b/test/data/ifact2.dats new file mode 100644 --- /dev/null +++ b/test/data/ifact2.dats @@ -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} .. + ( + 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] diff --git a/test/data/ifact2.out b/test/data/ifact2.out new file mode 100644 --- /dev/null +++ b/test/data/ifact2.out @@ -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} .. (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]