diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -1,11 +1,12 @@ cabal-version: 1.18 name: language-ats -version: 1.2.0.2 +version: 1.2.0.3 license: BSD3 license-file: LICENSE copyright: Copyright: (c) 2018 Vanessa McHale maintainer: vamchale@gmail.com author: Vanessa McHale +stability: experimental synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. @@ -30,7 +31,7 @@ library exposed-modules: Language.ATS - build-tools: happy -any, alex -any + build-tools: happy >=1.17.1, alex -any hs-source-dirs: src other-modules: Language.ATS.Lexer @@ -42,7 +43,8 @@ build-depends: base >=4.10 && <5, array -any, - lens -any, + microlens -any, + microlens-th -any, deepseq -any, ansi-wl-pprint >=0.6.8, recursion-schemes >=5.0.1, diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -59,7 +59,6 @@ , typeCallArgs ) where -import Control.Lens import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans.State @@ -68,6 +67,7 @@ import Language.ATS.Parser import Language.ATS.PrettyPrint import Language.ATS.Types +import Lens.Micro import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) rewriteATS' :: Eq a => (ATS a, FixityState a) -> ATS a @@ -89,6 +89,9 @@ parse :: String -> Either ATSError (ATS AlexPosn) parse = parseWithCtx defaultFixityState id +lexErr :: Either String a -> Either ATSError a +lexErr = over _Left LexError + stripComments :: [Token] -> [Token] stripComments = filter nc where nc CommentLex{} = False @@ -99,9 +102,9 @@ -- | Parse with some fixity declarations already in scope. parseWithCtx :: FixityState AlexPosn -> ([Token] -> [Token]) -> String -> Either ATSError (ATS AlexPosn) -parseWithCtx st p = stateParse <=< lexErr +parseWithCtx st p = stateParse <=< lex' where withSt = flip runStateT st - lexErr = over _Left LexError . fmap p . lexATS + lex' = lexErr . fmap p . lexATS stateParse = fmap rewriteATS' . withSt . parseATS -- | Extract a list of files that some code depends on. 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 @@ -113,6 +113,8 @@ tokens :- <0> $white+ ; + + -- (sort of) handle nested comments "(*)" ; <0> @block_comment_start { tok (\p _ -> alex $ CommentBegin p) `andBegin` one } <0> @c_comment_start { tok (\p _ -> alex $ CommentBegin p) `andBegin` one_c } @@ -131,16 +133,21 @@ [^\*\/]+ { tok (\p s -> alex $ CommentContents p s) } @comment_in+ / [^\/] { tok (\p s -> alex $ CommentContents p s) } @comment_general { tok (\p s -> alex $ CommentContents p s) } - @c_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 } - @c_comment_start { tok (\p _ -> alexError ("at " <> show (pretty p) <> ": Nested C comments of depth > 1 are not supported.")) } + + -- C-style nested comments + @c_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 } + @c_comment_start { tok (\p _ -> alexError ("at " <> show (pretty p) <> ": Nested C comments of depth > 1 are not supported.")) } [^\*\/]+ { tok (\p s -> alex $ CommentContents p s) } @comment_in+ / [^\/] { tok (\p s -> alex $ CommentContents p s) } @comment_general { tok (\p s -> alex $ CommentContents p s) } - <0> "//".* { tok (\p s -> alex $ CommentLex p s) } + + -- comments and macros <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) } + + -- keywords <0> fun { tok (\p _ -> alex $ Keyword p KwFun) } <0> fn { tok (\p _ -> alex $ Keyword p KwFn) } <0> fnx { tok (\p _ -> alex $ Keyword p KwFnx) } @@ -239,15 +246,13 @@ <0> "fold@" { tok (\p s -> alex $ IdentifierSpace p s) } <0> "free@" { tok (\p s -> alex $ Identifier p s) } <0> @fixity_decl { tok (\p s -> alex $ FixityTok p s) } + + -- special symbols, literals <0> @double_parens { tok (\p s -> alex $ DoubleParenTok p) } <0> @double_braces { tok (\p s -> alex $ DoubleBracesTok p) } <0> @double_brackets { tok (\p s -> alex $ DoubleBracketTok p) } <0> @lambda { tok (\p s -> alex $ Arrow p s) } <0> @func_type { tok (\p s -> alex $ FuncType p s) } - <0> @unsigned_lit { tok (\p s -> alex $ UintTok p (read $ init s)) } - <0> @integer { tok (\p s -> alex $ IntTok p (read s)) } -- FIXME shouldn't fail silenty on overflow - <0> @float { tok (\p s -> alex $ FloatTok p (read s)) } - <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } <0> @at_brace { tok (\p s -> alex $ Special p "@{") } <0> @at_tuple { tok (\p s -> alex $ Special p "@(") } <0> @box_tuple { tok (\p s -> alex $ Special p "'(") } @@ -257,9 +262,17 @@ <0> @operator { tok (\p s -> alex $ Operator p s) } <0> @builtin { tok (\p s -> alex $ SpecialIdentifier p (tail s)) } <0> $special { tok (\p s -> alex $ Special p s) } + + -- literals + <0> @unsigned_lit { tok (\p s -> alex $ UintTok p (read $ init s)) } + <0> @integer { tok (\p s -> alex $ IntTok p (read s)) } -- FIXME shouldn't fail silenty on overflow + <0> @float { tok (\p s -> alex $ FloatTok p (read s)) } + <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } + <0> @string { tok (\p s -> alex $ StringTok p s) } + + -- identifiers <0> @identifier / " " { tok (\p s -> alex $ IdentifierSpace p s) } -- FIXME get rid of this for performance reasons <0> @identifier { tok (\p s -> alex $ Identifier p s) } - <0> @string { tok (\p s -> alex $ StringTok p s) } { 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 @@ -23,7 +23,7 @@ import Control.Composition import Control.DeepSeq (NFData) -import Control.Lens (over, _head) +import Lens.Micro (over, _head) import qualified Data.Map as M import Control.Monad.Trans.Class import Control.Monad.Trans.State @@ -170,6 +170,7 @@ cloptr1Arrow { Arrow $$ "=" } lincloptr1Arrow { Arrow $$ "=" } spear { Arrow $$ "=>>" } + proofArrow { Arrow $$ "=/=>" } lsqbracket { Special $$ "[" } rsqbracket { Special $$ "]" } string { StringTok _ $$ } @@ -217,6 +218,27 @@ %% +some(p) + : some(p) p { $2 : $1 } + | p { [$1] } + +many(p) + : some(p) p { $2 : $1 } + | { [] } + +sep_by(p,sep) : p { [$1] } + | sep_by(p,sep) sep p { $3 : $1 } + +comma_sep(p) + : sep_by(p, comma) { $1 } + +between(p1,p,p2) : p1 p p2 { $2 } + +parens(p) : between(openParen, p, closeParen) { $1 } + +alt(p,q) : p { $1 } + | q { $1 } + ATS : Declarations { ATS $1 } -- | Parse declarations in a list @@ -226,18 +248,14 @@ | Declarations ValDecl { $2 ++ $1 } | Declarations local ATS in ATS end { Local $2 $3 $5 : $1 } --- | Several comma-separated types -TypeIn : Type { [$1] } - | TypeIn comma Type { $3 : $1 } +TypeIn : comma_sep(Type) { $1 } --- | Several comma-separated types or static expressions -TypeInExpr : Type { [$1] } - | StaticExpression { [ConcreteType $1] } - | TypeInExpr comma Type { $3 : $1 } - | TypeInExpr comma StaticExpression { ConcreteType $3 : $1 } +ExprType : StaticExpression { ConcreteType $1 } +TypeInExpr : comma_sep(alt(Type,ExprType)) { $1 } + -- | Parse a type -Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 } +Type : Name parens(TypeInExpr) { Dependent $1 $2 } | Name doubleParens { Dependent $1 [] } | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 } | identifierSpace { Named (Unqualified $ to_string $1) } @@ -264,8 +282,8 @@ | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] } | openParen TypeIn closeParen { Tuple $1 $2 } | openParen TypeIn closeParen lineComment { Tuple $1 $2 } - | openParen TypeIn rbrace {% left $ Expected $3 ")" "}" } | openParen Type closeParen { ParenType $1 $2 } + | openParen TypeIn rbrace {% left $ Expected $3 ")" "}" } | doubleParens { NoneType $1 } | Type where IdentifierOr SortArgs eq Type { WhereType $2 $1 $3 $4 $6 } | dollar {% left $ Expected $1 "Type" "$" } @@ -298,8 +316,7 @@ | doubleParens { VoidLiteral $1 } -- | Parse a list of comma-separated patterns -PatternIn : Pattern { [$1] } - | PatternIn comma Pattern { $3 : $1 } +PatternIn : comma_sep(Pattern) { $1 } -- | Parse a pattern match Pattern : Name { PName $1 [] } @@ -311,7 +328,7 @@ | identifier Pattern { PSum (to_string $1) $2 } | identifierSpace Pattern { PSum (to_string $1) $2 } | openParen PatternIn vbar PatternIn closeParen { Proof $1 $2 $4 } - | openParen PatternIn closeParen { TuplePattern $2 } + | parens(PatternIn) { TuplePattern $1 } | Literal { PLiteral $1 } | Pattern when Expression { Guarded $2 $3 $1 } | at Pattern { AtPattern $1 $2 } @@ -321,21 +338,24 @@ | minus {% left $ Expected $1 "Pattern" "-" } | plus {% left $ Expected $1 "Pattern" "+" } --- | Parse a case expression -Case : vbar Pattern CaseArrow Expression { [($2, $3, $4)] } - | Pattern CaseArrow Expression { [($1, $2, $3)] } - | Case vbar Pattern CaseArrow Expression { ($3, $4, $5) : $1 } +-- | Common parser for @case@ expressions, @ifcase@ expressions, and @case@ +-- static expressions. +case_pattern(pat,expr) + : vbar pat CaseArrow expr { [($2, $3, $4)] } + | pat CaseArrow expr { [($1, $2, $3)] } + | case_pattern(pat, expr) vbar pat CaseArrow expr { ($3, $4, $5) : $1 } -IfCase : vbar Expression CaseArrow Expression { [($2, $3, $4)] } - | Expression CaseArrow Expression { [($1, $2, $3)] } - | IfCase vbar Expression CaseArrow Expression { ($3, $4, $5) : $1 } +Case : case_pattern(Pattern, Expression) { $1 } +StaticCase : case_pattern(Pattern, StaticExpression) { $1 } + +IfCase : case_pattern(Expression, Expression) { $1 } + ExpressionPrf : ExpressionIn { (Nothing, $1) } | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof? -- | A list of comma-separated expressions -ExpressionIn : Expression { [$1] } - | ExpressionIn comma Expression { $3 : $1 } +ExpressionIn : comma_sep(Expression) { $1 } Tuple : PreExpression comma PreExpression { [$3, $1] } | Tuple comma PreExpression { $3 : $1 } @@ -343,6 +363,7 @@ -- | Parse an arrow in a case statement CaseArrow : plainArrow { Plain $1 } | spear { Spear $1 } + | proofArrow { ProofArrow $1 } | minus {% left $ Expected $1 "Arrow" "-" } | eq {% left $ Expected $1 "Arrow" "=" } | minus {% left $ Expected $1 "Arrow" "-" } @@ -389,8 +410,7 @@ | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"} | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"} -StaticArgs : StaticExpression { [$1] } - | StaticArgs comma StaticExpression { $3 : $1 } +StaticArgs : comma_sep(StaticExpression) { $1 } StaticDecls : StaticDeclaration { [$1] } | StaticDecls StaticDeclaration { $2 : $1 } @@ -409,9 +429,10 @@ | StaticExpression semicolon StaticExpression { SPrecede $1 $3 } | UnOp StaticExpression { SUnary $1 $2 } | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] } - | let StaticDecls in end { SLet $1 $2 Nothing } + | let StaticDecls comment_after(in) end { SLet $1 $2 Nothing } | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) } | openParen StaticExpression closeParen { $2 } + | case StaticExpression of StaticCase { SCase $1 $2 $4 } -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 } @@ -428,7 +449,7 @@ | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $ to_string $3) } | if Expression then Expression { If $2 $4 Nothing} | if Expression then Expression else Expression { If $2 $4 (Just $6) } - | let ATS in end { Let $1 $2 Nothing } + | let ATS comment_after(in) end { Let $1 $2 Nothing } | let ATS in Expression end { Let $1 $2 (Just $4) } | let ATS in Expression vbar {% left $ Expected $5 "end" "|" } | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 } @@ -484,8 +505,7 @@ | IdentifierOr { NamedSort $1 } | IdentifierOr plus { NamedSort ($1 <> "+") } -QuantifierArgs : IdentifierOr { [$1] } - | QuantifierArgs comma IdentifierOr { $3 : $1 } +QuantifierArgs : comma_sep(IdentifierOr) { $1 } | { [] } Existential : lsqbracket QuantifierArgs colon Sort vbar StaticExpression rsqbracket { Existential $2 False (Just $4) (Just $6) } @@ -517,8 +537,12 @@ ImplExpression : StaticExpression { Left $1 } | Expression { Right $1 } +comment_after(p) : p { $1 } + | p Comment { $1 } + | p lineComment { $1 } + -- | Parse the details of an implementation -Implementation : Universals FunName MaybeImplicit Universals FunArgs eq Expression { Implement $6 $1 $3 $4 $2 $5 (Right $7) } +Implementation : comment_after(Universals) FunName MaybeImplicit Universals FunArgs eq Expression { Implement $6 $1 $3 $4 $2 $5 (Right $7) } StaticImplementation : Universals FunName MaybeImplicit Universals FunArgs eq StaticExpression { Implement $6 $1 $3 $4 $2 $5 (Left $7) } @@ -551,14 +575,12 @@ Records : IdentifierOr eq Type { [($1, $3)] } | Records comma IdentifierOr eq Type { ($3, $5) : $1 } -IdentifiersIn : IdentifierOr { [$1] } - | IdentifiersIn comma IdentifierOr { $3 : $1 } +IdentifiersIn : comma_sep(IdentifierOr) { $1 } OfType : { Nothing } | of Type { Just $2 } -StaticExpressionsIn : StaticExpression { [$1] } - | StaticExpressionsIn comma StaticExpression { $3 : $1 } +StaticExpressionsIn : comma_sep(StaticExpression) { $1 } -- | Parse a constructor for a sum type SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing } @@ -792,7 +814,7 @@ | Operators Operator { $2 : $1 } | Operators identifier { to_string $2 : $1 } -StackFunction : openParen Args closeParen Signature Type plainArrow Expression { StackF $4 $2 $5 $7 } +StackFunction : parens(Args) Signature Type plainArrow Expression { StackF $2 $1 $3 $5 } ValDecl : val Pattern colon Type eq PreExpression { [ Val (get_addendum $1) (Just $4) $2 $6 ] } | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] } @@ -907,6 +929,7 @@ unmatched :: AlexPosn -> String -> Doc unmatched l chr = "unmatched" <+> squotes (text chr) <+> "at" <+> pretty l <> linebreak +-- ors = bear bear :: Bool -> [Doc] -> Doc bear _ [] = mempty bear False [x, y] = x <+> "or" <+> y 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 @@ -15,9 +15,9 @@ ) where import Control.Composition hiding ((&)) -import Control.Lens hiding (op, pre) import Data.Functor.Foldable (cata) import Language.ATS.Types +import Lens.Micro import Prelude hiding ((<$>)) import Text.PrettyPrint.ANSI.Leijen hiding (bool) @@ -50,9 +50,10 @@ pretty (FieldName _ n n') = text n <> "." <> text n' instance Pretty (LambdaType a) where - pretty Plain{} = "=>" - pretty Spear{} = "=>>" - pretty (Full _ v) = "=<" <> text v <> ">" + pretty Plain{} = "=>" + pretty Spear{} = "=>>" + pretty ProofArrow{} = "=/=>" + pretty (Full _ v) = "=<" <> text v <> ">" instance Pretty (BinOp a) where pretty Mult = "*" @@ -182,10 +183,12 @@ prettyIfCase [] = mempty prettyIfCase [(s, l, t)] = "|" <+> s <+> pretty l <+> t prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t - prettyCases [] = mempty - prettyCases [(s, l, t)] = "|" <+> pretty s <+> pretty l <+> t - prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ... +prettyCases :: (Pretty a, Pretty b) => [(a, b, Doc)] -> Doc +prettyCases [] = mempty +prettyCases [(s, l, t)] = "|" <+> pretty s <+> pretty l <+> t +prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ... + noParens :: Doc -> Bool noParens = all (`notElem` ("()" :: String)) . show @@ -247,6 +250,7 @@ a (SLetF _ e e') = flatAlt ("let" <$> indent 2 (pretty e) <$> endLet e') ("let" <+> pretty e <$> endLet e') + a (SCaseF ad e sls) = "case" <> pretty ad <+> e <+> "of" <$> indent 2 (prettyCases sls) instance Eq a => Pretty (Sort a) where pretty (T0p ad) = "t@ype" <> pretty ad @@ -351,8 +355,6 @@ glue (Func _ Fnx{}) (Func _ And{}) = True glue Assume{} Assume{} = True glue _ _ = False - -{-# INLINE glue #-} concatSame :: Eq a => [Declaration a] -> Doc concatSame [] = mempty 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 @@ -64,7 +64,6 @@ import Control.Composition import Control.DeepSeq (NFData) -import Control.Lens import Data.Function (on) import Data.Functor.Foldable (ListF (Cons), ana, cata, embed, project) import Data.Functor.Foldable.TH (makeBaseFunctor) @@ -73,6 +72,8 @@ import Data.Semigroup (Semigroup) import GHC.Generics (Generic) import Language.ATS.Lexer (Addendum (..)) +import Lens.Micro +import Lens.Micro.TH type Fix = Either Int String @@ -173,7 +174,8 @@ -- | A type for @=>@, @=\@, etc. data LambdaType a = Plain a | Full a String - | Spear a + | Spear a -- @=>>@ + | ProofArrow a -- @=/=>@ deriving (Show, Eq, Generic, NFData) data Name a = Unqualified String @@ -267,6 +269,7 @@ | SCall (Name a) [StaticExpression a] | SUnary (UnOp a) (StaticExpression a) | SLet a [Declaration a] (Maybe (StaticExpression a)) + | SCase Addendum (StaticExpression a) [(Pattern a, LambdaType a, StaticExpression a)] deriving (Show, Eq, Generic, NFData) -- | A (possibly effectful) expression.