language-ats 1.7.0.3 → 1.7.0.4
raw patch · 6 files changed
+71/−50 lines, 6 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +12/−6
- language-ats.cabal +2/−2
- src/Language/ATS/Lexer.x +4/−4
- src/Language/ATS/Parser.y +22/−14
- src/Language/ATS/PrettyPrint.hs +7/−0
- src/Language/ATS/Types.hs +24/−24
CHANGELOG.md view
@@ -1,5 +1,11 @@-# language-ats +# language-ats +## 1.7.0.4++ * Allow `datatype`, `datavtype`, and `dataview` to work with `and`.+ * Remove spurious dependency on `cpphs`+ * Prettier errors when parsing records+ ## 1.7.0.3 * Bump `recursion` version bounds@@ -7,22 +13,22 @@ ## 1.7.0.2 Bug fixes:- + * Support `llam@` keyword Enhancements:- - * Use `recursion` library to incur fewer dependencies + * Use `recursion` library to incur fewer dependencies+ ## 1.7.0.0 Bug Fixes:- + * Now accepts proof-level lambdas. * Include all test data Breaking Changes:- + * `PrVar` and `PrVal` now take a `StaticExpression` * `PrFun`, `PrFn`, and `Praxi` now take a `StaticExpression` * Add a rewrite phase for `StaticExpression`s
language-ats.cabal view
@@ -1,6 +1,6 @@ cabal-version: 1.18 name: language-ats-version: 1.7.0.3+version: 1.7.0.4 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale@@ -36,7 +36,7 @@ library exposed-modules: Language.ATS- build-tools: happy >=1.17.1, alex -any, cpphs -any+ build-tools: happy >=1.17.1, alex -any hs-source-dirs: src other-modules: Language.ATS.Lexer
src/Language/ATS/Lexer.x view
@@ -147,7 +147,7 @@ <0> "//".* { tok (\p s -> alex $ CommentLex p s) } <0> @c_block { tok (\p s -> alex $ CBlockLex p s) } <0> "#define".* { tok (\p s -> alex $ MacroBlock p s) }- <0> @if_block { tok (\p s -> alex $ MacroBlock p s) } + <0> @if_block { tok (\p s -> alex $ MacroBlock p s) } -- keywords <0> fun { tok (\p _ -> alex $ Keyword p KwFun) }@@ -329,7 +329,7 @@ data Addendum = None | Plus | Minus- deriving (Eq, Show, Generic, NFData)+ deriving (Show, Eq, Generic, NFData) -- TODO ideally we'd handle this as an internal error later in the parser. get_staload (Keyword _ (KwStaload b)) = b@@ -423,7 +423,7 @@ | KwMacdef | KwDatasort | KwException- deriving (Eq, Show, Generic, NFData)+ deriving (Show, Eq, Generic, NFData) data Token = Identifier AlexPosn String | SpecialIdentifier AlexPosn String@@ -452,7 +452,7 @@ | SpecialBracket AlexPosn | FixityTok AlexPosn String | End- deriving (Eq, Show, Generic, NFData)+ deriving (Show, Eq, Generic, NFData) instance Pretty Addendum where pretty Plus = "+"
src/Language/ATS/Parser.y view
@@ -265,7 +265,7 @@ ATS : Declarations { ATS (reverse $1) } -- | Parse declarations in a list-Declarations : { [] } +Declarations : { [] } | Declarations Declaration { $2 : $1 } | Declarations FunDecl { $2 ++ $1 } | Declarations ValDecl { $2 ++ $1 }@@ -495,7 +495,7 @@ | let ATS in Expression end { Let $1 $2 (Just $4) } | let ATS in Expression vbar {% left $ Expected $5 "end" "|" } | let ATS fun {% left $ Expected $3 "in" "fun" }- | let ATS plainArrow {% left $ Expected $3 "in" "=>" } + | let ATS plainArrow {% left $ Expected $3 "in" "=>" } | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 } | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 } | addrAt PreExpression { AddrAt $1 $2 }@@ -580,7 +580,7 @@ | Implicits doubleBrackets { [] : $1 } | lbracket TypeIn rbracket { [toList $2] } | Implicits lspecial TypeIn rbracket { toList $3 : $1 }- + MaybeImplicit : Implicits { $1 } | { [] } @@ -617,6 +617,7 @@ RecordVal : IdentifierOr eq Expression { ($1, $3) :| [] } | RecordVal comma IdentifierOr eq Expression { ($3, $5) :| toList $1 } | IdentifierOr eq comma {% left $ Expected $3 "Expression" "," }+ | identifierSpace {% left $ Expected (token_posn $1) "Record field assignment" (to_string $1) } -- | Parse a list of types in a record Records : IdentifierOr eq Type { ($1, $3) :| [] }@@ -807,15 +808,20 @@ | doubleParens { Just [] } | { Nothing } -SumDecl : datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 }+AndViewtype : datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }+ | datavtype IdentifierOr SortArgs eq lineComment Leaves { SumViewType $2 $3 $6 }+ | datavtype lineComment IdentifierOr SortArgs eq Leaves { SumViewType $3 $4 $6 }+ | datavtype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumViewType $3 $4 $7 }+ | AndViewtype and IdentifierOr SortArgs eq Leaves { AndD $1 (SumViewType $3 $4 $6) }++AndView : dataview IdentifierOr SortArgs eq Leaves { DataView $1 $2 $3 $5 }+ | dataview IdentifierOr SortArgs eq lineComment Leaves { DataView $1 $2 $3 $6 }+ | AndView and IdentifierOr SortArgs eq Leaves { AndD $1 (DataView $2 $3 $4 $6) }++AndType : datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 } | datatype lineComment IdentifierOr SortArgs eq Leaves { SumType $3 $4 $6 } | datatype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumType $3 $4 $7 }- | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }- | datavtype IdentifierOr SortArgs eq lineComment Leaves { SumViewType $2 $3 $6 }- | datavtype lineComment IdentifierOr SortArgs eq Leaves { SumViewType $3 $4 $6 }- | datavtype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumViewType $3 $4 $7 }- | dataview IdentifierOr SortArgs eq Leaves { DataView $1 $2 $3 $5 }- | dataview IdentifierOr SortArgs eq lineComment Leaves { DataView $1 $2 $3 $6 }+ | AndType and IdentifierOr SortArgs eq Leaves { AndD $1 (SumType $3 $4 $6) } -- | Parse a declaration defining a type TypeDecl : typedef IdentifierOr SortArgs eq Type MaybeAnnot { TypeDef $1 $2 $3 $5 $6 }@@ -831,7 +837,9 @@ | absprop IdentifierOr parens(Args) { AbsProp $1 $2 $3 } | AndSort { $1 } | AndStadef { $1 }- | SumDecl { $1 }+ | AndViewtype { $1 }+ | AndView { $1 }+ | AndType { $1 } | extern typedef {% left $ Expected $2 "external declaration" "typedef" } | vtypedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Viewtype" "|" } | typedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Type" "|" }@@ -1000,7 +1008,7 @@ deriving (Eq, Show, Generic, NFData) unmatched :: AlexPosn -> String -> Doc-unmatched l chr = "unmatched" <+> squotes (text chr) <+> "at" <+> pretty l <> linebreak +unmatched l chr = "unmatched" <+> squotes (text chr) <+> "at" <+> pretty l <> linebreak -- ors = bear bear :: Bool -> [Doc] -> Doc@@ -1014,7 +1022,7 @@ preErr (OneOf p ss s) = pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s) <> ", expected one of" <+> bear False (fmap (squotes . text) ss)) <> linebreak preErr (Expected p s1 s2) = pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak-preErr (Unknown (Special l ")")) = unmatched l ")" +preErr (Unknown (Special l ")")) = unmatched l ")" preErr (Unknown (Special l "}")) = unmatched l "}" preErr (Unknown (Special l ">")) = unmatched l ">" preErr (Unknown t) = "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak@@ -1025,7 +1033,7 @@ left = lift . Left parseError :: [Token] -> ParseSt a-parseError [] = left Exhausted +parseError [] = left Exhausted parseError x = left . Unknown . head $ x }
src/Language/ATS/PrettyPrint.hs view
@@ -394,6 +394,10 @@ isVal AndDecl{} = True isVal _ = False +-- isTypeDef :: Declaration a -> Bool+-- isTypeDef ViewTypeDef{} = True+-- isTypeDef TypeDef{} = True+ notDefine :: String -> Bool notDefine = not . ("#define" `isPrefixOf`) @@ -592,6 +596,9 @@ pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettySortArgs as pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettySortArgs as <+> "=" <+> pretty t pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls)+ pretty (AndD d (SumViewType s as ls)) = pretty d <$> "and" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls)+ pretty (AndD d (SumType s as ls)) = pretty d <$> "and" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls)+ pretty (AndD d (DataView _ s as ls)) = pretty d <$> "and" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls) pretty (DataView _ s as ls) = "dataview" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls) pretty (SumType s as ls) = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf (toList ls) pretty (DataSort _ s ls) = "datasort" <+> text s <+> "=" <$> prettyDSL (toList ls)
src/Language/ATS/Types.hs view
@@ -66,15 +66,15 @@ | Pre { pos :: a, ifix :: Fix } | Post { pos :: a, ifix :: Fix } | Infix { pos :: a, ifix :: Fix }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | An ATS file, containing a list of declarations newtype ATS a = ATS { unATS :: [Declaration a] }- deriving (Show, Eq, Generic)+ deriving (Eq, Generic) deriving newtype (NFData, Semigroup, Monoid) data Leaf a = Leaf { _constructorUniversals :: [Universal a], name :: String, constructorArgs :: [StaticExpression a], maybeType :: Maybe (Type a) }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) type SortArgs a = Maybe [SortArg a] type Args a = Maybe [Arg a]@@ -125,13 +125,13 @@ | Exception String (Type a) | ExtVar a String (Expression a) | AbsImpl a (Name a) (SortArgs a) (Type a)- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data DataSortLeaf a = DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a))- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data DataPropLeaf a = DataPropLeaf { propU :: [Universal a], _propExpr1 :: Expression a, _propExpr2 :: Maybe (Expression a) }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | A type for parsed ATS types data Type a = Tuple a [Type a]@@ -156,7 +156,7 @@ | AnonymousRecord a (NonEmpty (String, Type a)) | WhereType a (Type a) String (SortArgs a) (Type a) | AddrType a -- ^ @addr@- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data TypeF a x = TupleF a [x] | BoxTupleF a (NonEmpty x)@@ -214,14 +214,14 @@ | ProofArrow a -- | @=/=>@ | ProofSpear a -- | @=/=>>@ | Full a String- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data Name a = Unqualified String | Qualified a String String -- ^ A name can be qualified e.g. @$UN.unsafefn@ | SpecialName a String -- ^ A name for builtin functions such as @$showtype@. | Functorial String String | FieldName a String String- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | A data type for patterns. data Pattern a = PName (Name a) [Pattern a]@@ -237,7 +237,7 @@ | ExistentialPattern (Existential a) (Pattern a) | As a (Pattern a) (Pattern a) | BinPattern a (BinOp a) (Pattern a) (Pattern a) -- ^ For use with e.g. @::@.- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data PatternF a x = PNameF (Name a) [x] | PSumF String x@@ -274,16 +274,16 @@ data Paired a b = Both a b | First a | Second b- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data SortArg a = SortArg String (Sort a) | Anonymous (Sort a)- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | An argument to a function. data Arg a = Arg (Paired String (Type a)) | PrfArg [Arg a] (Arg a)- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | A datatype for sorts. data Sort a = NamedSort { _sortName :: String }@@ -294,7 +294,7 @@ | View a Addendum -- ^ @view@ | TupleSort a (Sort a) (Sort a) | ArrowSort a (Sort a) (Sort a)- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data SortF a x = NamedSortF String | T0pF Addendum@@ -320,17 +320,17 @@ -- | Wrapper for universal quantifiers (refinement types) data Universal a = Universal { bound :: [String], typeU :: Maybe (Sort a), prop :: [StaticExpression a] }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | Wrapper for existential quantifiers/types data Existential a = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe (Sort a), propE :: Maybe (StaticExpression a) }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | Unary operators data UnOp a = Negate -- | @~@ | Deref -- | @!@ | SpecialOp a String- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | Binary operators on expressions data BinOp a = Add@@ -351,7 +351,7 @@ | At | SpearOp -- ^ @->@ | SpecialInfix a String- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) pattern Con :: a -> BinOp a pattern Con l = SpecialInfix l "::"@@ -374,7 +374,7 @@ | ProofLinearLambda a (LambdaType a) (Pattern a) (StaticExpression a) | WhereStaExp (StaticExpression a) (ATS a) | SParens (StaticExpression a)- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data StaticExpressionF a x = StaticValF (Name a) | StaticBinaryF (BinOp a) x x@@ -498,7 +498,7 @@ | ParenExpr a (Expression a) | CommentExpr String (Expression a) | MacroVar a String- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data ExpressionF a x = LetF a (ATS a) (Maybe x) | VoidLiteralF a@@ -652,7 +652,7 @@ , iArgs :: Args a -- ^ Arguments , _iExpression :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body. }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | A function declaration accounting for all keywords ATS uses to -- define them.@@ -664,7 +664,7 @@ | PrFn { _preStaF :: PreFunction StaticExpression a } | Praxi { _preStaF :: PreFunction StaticExpression a } | CastFn { _preF :: PreFunction Expression a }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- | A type for stack-allocated functions. See -- [here](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html)@@ -674,7 +674,7 @@ , stReturnType :: Type a , stExpression :: Expression a }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) data PreFunction ek a = PreF { fname :: Name a -- ^ Function name , sig :: Maybe String -- ^ e.g. <> or \<!wrt>@@ -685,7 +685,7 @@ , termetric :: Maybe (StaticExpression a) -- ^ Optional termination metric , _expression :: Maybe (ek a) -- ^ Expression holding the actual function body (not present in static templates) }- deriving (Show, Eq, Generic, NFData)+ deriving (Eq, Generic, NFData) -- FIXME left vs. right shouldn't be treated the same instance (Eq a) => Ord (Fixity a) where