language-ats 0.1.1.14 → 0.1.1.15

raw patch · 5 files changed

+61/−25 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• language-ats.cabal +1/−1
• src/Language/ATS.hs +6/−0
• src/Language/ATS/Parser.y +29/−10
• src/Language/ATS/PrettyPrint.hs +21/−12
• src/Language/ATS/Types.hs +4/−2

@@ -1,5 +1,5 @@ name:                language-ats-version:             0.1.1.14+version:             0.1.1.15 synopsis:            Parser and pretty-printer for ATS. description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license:             BSD3

@@ -2,6 +2,7 @@ module Language.ATS ( -- * Functions for working with syntax                       lexATS                     , parseATS+                    , parseATS'                     , printATS                     , printATSCustom                     , printATSFast@@ -27,6 +28,7 @@                     , Existential (..)                     , PreFunction (..)                     , StaticExpression (..)+                    , StackFunction (..)                     , Paired (..)                     , Fixity (..)                     -- * Lexical types@@ -47,6 +49,10 @@ import           Language.ATS.Parser import           Language.ATS.PrettyPrint import           Language.ATS.Types++-- | Parse a string containing ATS source.+parseATS' :: String -> Either (ATSError String) ATS+parseATS' = parseATS . lexATS  getDependencies :: ATS -> [FilePath] getDependencies (ATS ds) = catMaybes (g <$> ds)

@@ -351,7 +351,7 @@            | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?            | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }            | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }-           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 }+           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 } -- TODO is this legal??            | begin Expression extern {% Left $ Expected $3 "end" "extern" }            | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" } @@ -378,6 +378,11 @@ StaticArgs : StaticExpression { [$1] }            | StaticArgs comma StaticExpression { $3 : $1 } +StaticDecls : StaticDeclaration { [$1] }+            | StaticDecls StaticDeclaration { $2 : $1 }+            | StaticDecls FunDecl { $2 ++ $1 }+            | FunDecl StaticDecls { $1 ++ $2 }+ StaticExpression : Name { StaticVal $1 }                  | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }                  | intLit { StaticInt $1 }@@ -388,6 +393,10 @@                  | Name openParen StaticArgs closeParen { SCall $1 $3 }                  | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }                  | 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 in StaticExpression end { SLet $1 $2 (Just $4) }      -- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }@@ -468,11 +477,16 @@ MaybeImplicit : Implicits { $1 }               | { [] } --- TODO also allow static expressions!+ImplExpression : StaticExpression { Left $1 }+               | Expression { Right $1 }+ -- | Parse the details of an implementation-Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 $9 }-               | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] $7 }+Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 (Right $9) }+               | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] (Right $7) } +StaticImplementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq StaticExpression { Implement $5 $1 $3 $4 $2 $6 (Left $9) }+                     | Universals FunName MaybeImplicit Universals doubleParens eq StaticExpression { Implement $5 $1 $3 $4 $2 [] (Left $7) }+ -- | Parse a function name FunName : IdentifierOr { Unqualified $1 }         | identifier dollar identifier { Functorial (to_string $1) (to_string $3) }@@ -611,15 +625,17 @@           | AndStadef and stadef boolLit eq identifierSpace { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) }           | AndStadef and stadef boolLit eq identifier { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) } +StafunDecl : prfun PreFunction { Func $1 (PrFun $2) }+           | prfn PreFunction { Func $1 (PrFn $2) }+ -- | Function declaration FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }-        | prfun PreFunction { [ Func $1 (PrFun $2) ] }-        | prfn PreFunction { [ Func $1 (PrFn $2) ] }         | fnx PreFunction { [ Func $1 (Fnx $2) ] }         | castfn PreFunction { [ Func $1 (CastFn $2) ] }         | fn PreFunction identifier {% Left $ Expected (token_posn $3) "=" (to_string $3) }         | fn PreFunction { [ Func $1 (Fn $2) ] }         | FunDecl and PreFunction { Func $2 (And $3) : $1 }+        | StafunDecl { [$1] }         | extern FunDecl { over _head (Extern $1) $2 }         | extern fun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }         | extern fnx PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }@@ -684,6 +700,11 @@         | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }         | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 } +StaticDeclaration : prval Pattern eq Expression { PrVal $2 $4 }+                  | praxi PreFunction { Func $1 (Praxi $2) }+                  | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 }+                  | StafunDecl { $1 }+ -- | Parse a declaration Declaration : include string { Include $2 }             | define { Define $1 }@@ -705,10 +726,8 @@             | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }             | var Pattern eq fixAt IdentifierOr StackFunction { Var Nothing $2 (Just $ FixAt $5 $6) Nothing }             | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing }-            | prval Pattern eq Expression { PrVal $2 $4 }-            | praxi PreFunction { Func $1 (Praxi $2) }-            | primplmnt FunArgs Implementation { ProofImpl $2 $3 }             | implement FunArgs Implementation { Impl $2 $3 }+            | StaticDeclaration { $1 }             | overload BinOp with Name { OverloadOp $1 $2 $4 }             | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }             | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) }@@ -744,7 +763,7 @@     pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col  instance Pretty (ATSError String) where-    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s2) <> ", expected:" <+> squotes (string s1)) <> linebreak+    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak     pretty (Unknown (Special l ")")) = red "Error:" <+> "unmatched ')' at" <+> pretty l <> linebreak      pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak 

@@ -56,7 +56,7 @@ printATSCustom r i (ATS x) = g mempty     where g = (displayS . renderSmart r i . pretty) (ATS $ reverse x) --- | Fast pretty-printer without indendation. Useful for generating code.+-- | Slightly faster pretty-printer without indendation (for code generation). printATSFast :: ATS -> String printATSFast (ATS x) = g mempty     where g = (displayS . renderCompact . (<> "\n") . pretty) (ATS $ reverse x)@@ -131,12 +131,9 @@     pretty = cata a . rewriteATS where         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''         a (IfF e e' Nothing)            = "if" <+> e <+> "then" <$> indent 2 e'-        a (LetF _ e (Just e'))          = flatAlt-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end")-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in" <+> e' <$> "end")-        a (LetF _ e Nothing)            = flatAlt-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end")-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in end")+        a (LetF _ e e')          = flatAlt+            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> endLet e')+            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> endLet e')         a (BoolLitF True)               = "true"         a (BoolLitF False)              = "false"         a (TimeLitF s)                  = text s@@ -247,6 +244,10 @@ squish Mult = True squish _    = False +endLet :: Maybe Doc -> Doc+endLet Nothing  = "in end"+endLet (Just d) = "in" <$> indent 2 d <$> "end"+ instance Pretty StaticExpression where     pretty = cata a where         a (StaticValF n)            = pretty n@@ -260,6 +261,10 @@         a (StaticBoolF False)       = "false"         a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))         a (SPrecedeF e e')          = e <> ";" <+> e'+        a (SUnaryF Negate e)        = "~" <> e+        a (SLetF _ e e')          = flatAlt+            ("let" <$> indent 2 (pretty ((ATS . reverse) e)) <$> endLet e')+            ("let" <+> pretty ((ATS . reverse) e) <$> endLet e')  instance Pretty Type where     pretty = cata a where@@ -335,12 +340,16 @@ prettyOr [] = mempty prettyOr is = mconcat (fmap (prettyArgsU "<" ">") is) +prettyImplExpr :: Either StaticExpression Expression -> Doc+prettyImplExpr (Left se) = pretty se+prettyImplExpr (Right e) = pretty e+ instance Pretty Implementation where-    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (pretty e)-    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)-    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)-    pretty (Implement _ ps is [] n ias e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)-    pretty (Implement _ ps is us n ias e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)+    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is [] n ias e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)+    pretty (Implement _ ps is us n ias e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)  isVal :: Declaration -> Bool isVal Val{}   = True

@@ -235,6 +235,8 @@                       | StaticVoid AlexPosn                       | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)                       | SCall Name [StaticExpression]+                      | SUnary UnOp StaticExpression+                      | SLet AlexPosn [Declaration] (Maybe StaticExpression)                       deriving (Show, Eq, Generic, NFData)  -- | A (possibly effectful) expression.@@ -306,11 +308,11 @@                                 , universalsI    :: [Universal] -- ^ Universal quantifiers                                 , nameI          :: Name -- ^ Name of the template being implemented                                 , iArgs          :: [Arg] -- ^ Arguments-                                , iExpression    :: Expression -- ^ Expression holding the function body.+                                , iExpression    :: Either StaticExpression Expression -- ^ Expression (or static expression) holding the function body.                                 }     deriving (Show, Eq, Generic, NFData) --- | A function declaration accounting for all three keywords (???) ATS uses to+-- | A function declaration accounting for all keywords ATS uses to -- define them. data Function = Fun PreFunction               | Fn PreFunction