packages feed

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 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.