diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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 diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 = "+" 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 @@ -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 } 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 @@ -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) 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 @@ -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 \ @@ -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