language-ats 1.2.0.2 → 1.2.0.3
raw patch · 6 files changed
+106/−60 lines, 6 filesdep +microlensdep +microlens-thdep −lensPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: microlens, microlens-th
Dependencies removed: lens
API changes (from Hackage documentation)
+ Language.ATS: ProofArrow :: a -> LambdaType a
+ Language.ATS: SCase :: Addendum -> (StaticExpression a) -> [(Pattern a, LambdaType a, StaticExpression a)] -> StaticExpression a
- Language.ATS: constructorUniversals :: forall a_aRT5. Lens' (Leaf a_aRT5) [Universal a_aRT5]
+ Language.ATS: constructorUniversals :: forall a_aNJZ. Lens' (Leaf a_aNJZ) [Universal a_aNJZ]
- Language.ATS: expression :: forall a_aRSI. Lens' (PreFunction a_aRSI) (Maybe (Expression a_aRSI))
+ Language.ATS: expression :: forall a_aNJC. Lens' (PreFunction a_aNJC) (Maybe (Expression a_aNJC))
- Language.ATS: fun :: forall a_aRT3. Traversal' (Declaration a_aRT3) (Function a_aRT3)
+ Language.ATS: fun :: forall a_aNJX. Traversal' (Declaration a_aNJX) (Function a_aNJX)
- Language.ATS: leaves :: forall a_aRT3. Traversal' (Declaration a_aRT3) [Leaf a_aRT3]
+ Language.ATS: leaves :: forall a_aNJX. Traversal' (Declaration a_aNJX) [Leaf a_aNJX]
- Language.ATS: preF :: forall a_aRSK a_a185n. Lens (Function a_aRSK) (Function a_a185n) (PreFunction a_aRSK) (PreFunction a_a185n)
+ Language.ATS: preF :: forall a_aNJE a_a13N0. Lens (Function a_aNJE) (Function a_a13N0) (PreFunction a_aNJE) (PreFunction a_a13N0)
- Language.ATS: typeCall :: forall a_aRT0. Traversal' (Type a_aRT0) (Name a_aRT0)
+ Language.ATS: typeCall :: forall a_aNJU. Traversal' (Type a_aNJU) (Name a_aNJU)
- Language.ATS: typeCallArgs :: forall a_aRT0. Traversal' (Type a_aRT0) [Type a_aRT0]
+ Language.ATS: typeCallArgs :: forall a_aNJU. Traversal' (Type a_aNJU) [Type a_aNJU]
Files
- language-ats.cabal +5/−3
- src/Language/ATS.hs +6/−3
- src/Language/ATS/Lexer.x +21/−8
- src/Language/ATS/Parser.y +58/−35
- src/Language/ATS/PrettyPrint.hs +11/−9
- src/Language/ATS/Types.hs +5/−2
language-ats.cabal view
@@ -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,
src/Language/ATS.hs view
@@ -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.
src/Language/ATS/Lexer.x view
@@ -113,6 +113,8 @@ tokens :- <0> $white+ ;++ -- (sort of) handle nested comments <one,two,three,one_c> "(*)" ; <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 @@ <three> [^\*\/]+ { tok (\p s -> alex $ CommentContents p s) } <three> @comment_in+ / [^\/] { tok (\p s -> alex $ CommentContents p s) } <three> @comment_general { tok (\p s -> alex $ CommentContents p s) }- <one_c> @c_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 }- <one_c> @c_comment_start { tok (\p _ -> alexError ("at " <> show (pretty p) <> ": Nested C comments of depth > 1 are not supported.")) }++ -- C-style nested comments+ <one_c> @c_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 }+ <one_c> @c_comment_start { tok (\p _ -> alexError ("at " <> show (pretty p) <> ": Nested C comments of depth > 1 are not supported.")) } <one_c> [^\*\/]+ { tok (\p s -> alex $ CommentContents p s) } <one_c> @comment_in+ / [^\/] { tok (\p s -> alex $ CommentContents p s) } <one_c> @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) } {
src/Language/ATS/Parser.y view
@@ -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 $$ "=<cloptr1>" } lincloptr1Arrow { Arrow $$ "=<lincloptr1>" } 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
src/Language/ATS/PrettyPrint.hs view
@@ -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
src/Language/ATS/Types.hs view
@@ -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 @=>@, @=\<cloref1>@, 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.