language-ats 0.3.0.7 → 1.0.0.0
raw patch · 7 files changed
+416/−418 lines, 7 files
Files
- README.md +2/−2
- language-ats.cabal +1/−1
- src/Language/ATS.hs +6/−5
- src/Language/ATS/Lexer.x +109/−100
- src/Language/ATS/Parser.y +9/−9
- src/Language/ATS/PrettyPrint.hs +49/−53
- src/Language/ATS/Types.hs +240/−248
README.md view
@@ -5,5 +5,5 @@ [haskell-src-exts](http://hackage.haskell.org/package/haskell-src-exts) that provides a parser and pretty-printer for [ATS](http://ats-lang.org/). -The parser is buggy but it can handle a good subset of the language; see-the `test/data` directory for some examples of what is currently working.+The parser is slightly buggy but it can handle most of the language; see+the `test/data` directory for examples of what it can handle.
language-ats.cabal view
@@ -1,5 +1,5 @@ name: language-ats-version: 0.3.0.7+version: 1.0.0.0 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
src/Language/ATS.hs view
@@ -63,18 +63,19 @@ import Language.ATS.Types import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) -rewriteATS' :: ATS -> ATS+rewriteATS' :: Eq a => ATS a -> ATS a rewriteATS' (ATS ds) = ATS (rewriteDecl <$> ds) -printErr :: MonadIO m => ATSError String -> m ()+-- | Print an error message to standard error.+printErr :: MonadIO m => ATSError -> m () printErr = liftIO . hPutDoc stderr . (<> "\n") . pretty -- | Parse a string containing ATS source.-parse :: String -> Either (ATSError String) ATS+parse :: String -> Either ATSError (ATS AlexPosn) parse = fmap rewriteATS' . (parseATS <=< (over _Left LexError . lexATS)) --- TODO use prepocessing?? here?-getDependencies :: ATS -> [FilePath]+-- | Extract a list of files that some code depends on.+getDependencies :: ATS a -> [FilePath] getDependencies (ATS ds) = join $ catMaybes (g <$> ds) where g (Staload _ _ s) = Just [s] g (Include s) = Just [s]
src/Language/ATS/Lexer.x view
@@ -1,6 +1,6 @@ { - {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns -fno-warn-unused-imports #-}+ {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns -fno-warn-unused-imports -fno-warn-orphans #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -48,7 +48,7 @@ -- Integer @integer = $digit+-@time_lit = $digit+ u+@unsigned_lit = $digit+ u -- Floats @decimals = $digit+@@ -109,114 +109,120 @@ tokens :- <0> $white+ ;- <0> @block_comment_start { tok (\p s -> alex $ CommentBegin p) `andBegin` one }- <one> @block_comment_end { tok (\p s -> alex $ CommentEnd p) `andBegin` 0 }+ <0> @block_comment_start { tok (\p _ -> alex $ CommentBegin p) `andBegin` one }+ <one> @block_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 } <one> @block_comment_start { tok (\p s -> alex $ CommentContents p s) `andBegin` two } <one> [^\*\(\)\/]+ { tok (\p s -> alex $ CommentContents p s) } <one> @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } <one> @comment_general { tok (\p s -> alex $ CommentContents p s) } <two> @block_comment_end { tok (\p s -> alex $ CommentContents p s) `andBegin` one }+ <two> @block_comment_start { tok (\p s -> alex $ CommentContents p s) `andBegin` three } <two> [^\*\(\)\/]+ { tok (\p s -> alex $ CommentContents p s) } <two> @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } <two> @comment_general { tok (\p s -> alex $ CommentContents p s) }+ <three> @block_comment_end { tok (\p s -> alex $ CommentContents p s) `andBegin` two }+ <three> @block_comment_start { tok (\_ _ -> alexError "Nested comments of depth >3 are not supported.") }+ <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) } <0> "//".* { tok (\p s -> alex $ CommentLex p s) } <0> "#define".* { tok (\p s -> alex $ MacroBlock p s) } <0> @if_block { tok (\p s -> alex $ MacroBlock p s) } <0> @c_block { tok (\p s -> alex $ CBlockLex p s) }- <0> fun { tok (\p s -> alex $ Keyword p KwFun) }- <0> fn { tok (\p s -> alex $ Keyword p KwFn) }- <0> fnx { tok (\p s -> alex $ Keyword p KwFnx) }- <0> and { tok (\p s -> alex $ Keyword p KwAnd) }- <0> prval { tok (\p s -> alex $ Keyword p KwPrval) }- <0> prfn { tok (\p s -> alex $ Keyword p KwPrfn) }- <0> prfun { tok (\p s -> alex $ Keyword p KwPrfun) }- <0> datatype { tok (\p s -> alex $ Keyword p KwDatatype) }- <0> data @view type { tok (\p s -> alex $ Keyword p KwDatavtype) }- <0> @view type { tok (\p s -> alex $ Keyword p (KwVtype None)) }- <0> @view type"+" { tok (\p s -> alex $ Keyword p (KwVtype Plus)) }- <0> @view type"-" { tok (\p s -> alex $ Keyword p (KwVtype Minus)) }- <0> dataview { tok (\p s -> alex $ Keyword p KwDataview) }- <0> dataprop { tok (\p s -> alex $ Keyword p KwDataprop) }- <0> assume { tok (\p s -> alex $ Keyword p KwAssume) }- <0> typedef { tok (\p s -> alex $ Keyword p KwTypedef) }- <0> @view typedef { tok (\p s -> alex $ Keyword p KwVtypedef) }- <0> absprop { tok (\p s -> alex $ Keyword p KwAbsprop) }- <0> llam { tok (\p s -> alex $ Keyword p KwLinearLambda) }- <0> lam { tok (\p s -> alex $ Keyword p KwLambda) }- <0> staload { tok (\p s -> alex $ Keyword p (KwStaload False)) }- <0> "#"staload { tok (\p s -> alex $ Keyword p (KwStaload True)) }- <0> let { tok (\p s -> alex $ Keyword p KwLet) }- <0> in { tok (\p s -> alex $ Keyword p KwIn) }- <0> end { tok (\p s -> alex $ Keyword p KwEnd) }- <0> case"+" { tok (\p s -> alex $ Keyword p (KwCase Plus)) }- <0> case"-" { tok (\p s -> alex $ Keyword p (KwCase Minus)) }- <0> case { tok (\p s -> alex $ Keyword p (KwCase None)) }- <0> castfn { tok (\p s -> alex $ Keyword p KwCastfn) }- <0> val"+" { tok (\p s -> alex $ Keyword p (KwVal Plus)) }- <0> val"-" { tok (\p s -> alex $ Keyword p (KwVal Minus)) }- <0> val { tok (\p s -> alex $ Keyword p (KwVal None)) }- <0> var { tok (\p s -> alex $ Keyword p KwVar) }- <0> if { tok (\p s -> alex $ Keyword p KwIf) }- <0> sif { tok (\p s -> alex $ Keyword p KwSif) }- <0> then { tok (\p s -> alex $ Keyword p KwThen) }- <0> else { tok (\p s -> alex $ Keyword p KwElse) }- <0> implement { tok (\p s -> alex $ Keyword p KwImplement) }- <0> implmnt { tok (\p s -> alex $ Keyword p KwImplement) }- <0> primplmnt { tok (\p s -> alex $ Keyword p KwProofImplement) }- <0> primplement { tok (\p s -> alex $ Keyword p KwProofImplement) }- <0> abst"@"ype { tok (\p s -> alex $ Keyword p (KwAbst0p None)) }- <0> abst"@ype+" { tok (\p s -> alex $ Keyword p (KwAbst0p Plus)) }- <0> abst"@type-" { tok (\p s -> alex $ Keyword p (KwAbst0p Minus)) }- <0> abs@view"t@ype" { tok (\p s -> alex $ Keyword p (KwAbsvt0p None)) }- <0> t"@"ype"+" { tok (\p s -> alex $ Keyword p (KwT0p Plus)) }- <0> t"@"ype"-" { tok (\p s -> alex $ Keyword p (KwT0p Minus)) }- <0> t"@"ype { tok (\p s -> alex $ Keyword p (KwT0p None)) }- <0> @view"t@ype+" { tok (\p s -> alex $ Keyword p (KwVt0p Plus)) }- <0> @view"t@ype-" { tok (\p s -> alex $ Keyword p (KwVt0p Minus)) }- <0> @view"t@ype" { tok (\p s -> alex $ Keyword p (KwVt0p None)) }- <0> abstype { tok (\p s -> alex $ Keyword p KwAbstype) }- <0> abs @view type { tok (\p s -> alex $ Keyword p KwAbsvtype) }- <0> absview { tok (\p s -> alex $ Keyword p KwAbsview) }- <0> view { tok (\p s -> alex $ Keyword p (KwView None)) }- <0> view"+" { tok (\p s -> alex $ Keyword p (KwView Plus)) }- <0> view"-" { tok (\p s -> alex $ Keyword p (KwView Minus)) }- <0> viewdef { tok (\p s -> alex $ Keyword p KwViewdef) }- <0> "#"include { tok (\p s -> alex $ Keyword p KwInclude) }- <0> when { tok (\p s -> alex $ Keyword p KwWhen) }- <0> of { tok (\p s -> alex $ Keyword p KwOf) }- <0> ifcase { tok (\p s -> alex $ Keyword p KwIfCase) }- <0> stadef { tok (\p s -> alex $ Keyword p KwStadef) }- <0> stacst { tok (\p s -> alex $ Keyword p KwStacst) }- <0> local { tok (\p s -> alex $ Keyword p KwLocal) }- <0> praxi { tok (\p s -> alex $ Keyword p KwPraxi) }- <0> while { tok (\p s -> alex $ Keyword p KwWhile) }- <0> where { tok (\p s -> alex $ Keyword p KwWhere) }- <0> begin { tok (\p s -> alex $ Keyword p KwBegin) }- <0> overload { tok (\p s -> alex $ Keyword p KwOverload) }- <0> with { tok (\p s -> alex $ Keyword p KwWith) }- <0> extern { tok (\p s -> alex $ Keyword p KwExtern) }- <0> extvar { tok (\p s -> alex $ Keyword p KwExtVar) }- <0> sortdef { tok (\p s -> alex $ Keyword p KwSortdef) }- <0> propdef { tok (\p s -> alex $ Keyword p KwPropdef) }- <0> tkindef { tok (\p s -> alex $ Keyword p KwTKind) }- <0> typekindef { tok (\p s -> alex $ Keyword p KwTKind) }- <0> "$raise" { tok (\p s -> alex $ Keyword p KwRaise) }- <0> macdef { tok (\p s -> alex $ Keyword p KwMacdef) }- <0> mod { tok (\p s -> alex $ Keyword p KwMod) }- <0> datasort { tok (\p s -> alex $ Keyword p KwDatasort) }+ <0> fun { tok (\p _ -> alex $ Keyword p KwFun) }+ <0> fn { tok (\p _ -> alex $ Keyword p KwFn) }+ <0> fnx { tok (\p _ -> alex $ Keyword p KwFnx) }+ <0> and { tok (\p _ -> alex $ Keyword p KwAnd) }+ <0> prval { tok (\p _ -> alex $ Keyword p KwPrval) }+ <0> prfn { tok (\p _ -> alex $ Keyword p KwPrfn) }+ <0> prfun { tok (\p _ -> alex $ Keyword p KwPrfun) }+ <0> datatype { tok (\p _ -> alex $ Keyword p KwDatatype) }+ <0> data @view type { tok (\p _ -> alex $ Keyword p KwDatavtype) }+ <0> @view type { tok (\p _ -> alex $ Keyword p (KwVtype None)) }+ <0> @view type"+" { tok (\p _ -> alex $ Keyword p (KwVtype Plus)) }+ <0> @view type"-" { tok (\p _ -> alex $ Keyword p (KwVtype Minus)) }+ <0> dataview { tok (\p _ -> alex $ Keyword p KwDataview) }+ <0> dataprop { tok (\p _ -> alex $ Keyword p KwDataprop) }+ <0> assume { tok (\p _ -> alex $ Keyword p KwAssume) }+ <0> typedef { tok (\p _ -> alex $ Keyword p KwTypedef) }+ <0> @view typedef { tok (\p _ -> alex $ Keyword p KwVtypedef) }+ <0> absprop { tok (\p _ -> alex $ Keyword p KwAbsprop) }+ <0> llam { tok (\p _ -> alex $ Keyword p KwLinearLambda) }+ <0> lam { tok (\p _ -> alex $ Keyword p KwLambda) }+ <0> staload { tok (\p _ -> alex $ Keyword p (KwStaload False)) }+ <0> "#"staload { tok (\p _ -> alex $ Keyword p (KwStaload True)) }+ <0> let { tok (\p _ -> alex $ Keyword p KwLet) }+ <0> in { tok (\p _ -> alex $ Keyword p KwIn) }+ <0> end { tok (\p _ -> alex $ Keyword p KwEnd) }+ <0> case"+" { tok (\p _ -> alex $ Keyword p (KwCase Plus)) }+ <0> case"-" { tok (\p _ -> alex $ Keyword p (KwCase Minus)) }+ <0> case { tok (\p _ -> alex $ Keyword p (KwCase None)) }+ <0> castfn { tok (\p _ -> alex $ Keyword p KwCastfn) }+ <0> val"+" { tok (\p _ -> alex $ Keyword p (KwVal Plus)) }+ <0> val"-" { tok (\p _ -> alex $ Keyword p (KwVal Minus)) }+ <0> val { tok (\p _ -> alex $ Keyword p (KwVal None)) }+ <0> var { tok (\p _ -> alex $ Keyword p KwVar) }+ <0> if { tok (\p _ -> alex $ Keyword p KwIf) }+ <0> sif { tok (\p _ -> alex $ Keyword p KwSif) }+ <0> then { tok (\p _ -> alex $ Keyword p KwThen) }+ <0> else { tok (\p _ -> alex $ Keyword p KwElse) }+ <0> implement { tok (\p _ -> alex $ Keyword p KwImplement) }+ <0> implmnt { tok (\p _ -> alex $ Keyword p KwImplement) }+ <0> primplmnt { tok (\p _ -> alex $ Keyword p KwProofImplement) }+ <0> primplement { tok (\p _ -> alex $ Keyword p KwProofImplement) }+ <0> abst"@"ype { tok (\p _ -> alex $ Keyword p (KwAbst0p None)) }+ <0> abst"@ype+" { tok (\p _ -> alex $ Keyword p (KwAbst0p Plus)) }+ <0> abst"@type-" { tok (\p _ -> alex $ Keyword p (KwAbst0p Minus)) }+ <0> abs@view"t@ype" { tok (\p _ -> alex $ Keyword p (KwAbsvt0p None)) }+ <0> t"@"ype"+" { tok (\p _ -> alex $ Keyword p (KwT0p Plus)) }+ <0> t"@"ype"-" { tok (\p _ -> alex $ Keyword p (KwT0p Minus)) }+ <0> t"@"ype { tok (\p _ -> alex $ Keyword p (KwT0p None)) }+ <0> @view"t@ype+" { tok (\p _ -> alex $ Keyword p (KwVt0p Plus)) }+ <0> @view"t@ype-" { tok (\p _ -> alex $ Keyword p (KwVt0p Minus)) }+ <0> @view"t@ype" { tok (\p _ -> alex $ Keyword p (KwVt0p None)) }+ <0> abstype { tok (\p _ -> alex $ Keyword p KwAbstype) }+ <0> abs @view type { tok (\p _ -> alex $ Keyword p KwAbsvtype) }+ <0> absview { tok (\p _ -> alex $ Keyword p KwAbsview) }+ <0> view { tok (\p _ -> alex $ Keyword p (KwView None)) }+ <0> view"+" { tok (\p _ -> alex $ Keyword p (KwView Plus)) }+ <0> view"-" { tok (\p _ -> alex $ Keyword p (KwView Minus)) }+ <0> viewdef { tok (\p _ -> alex $ Keyword p KwViewdef) }+ <0> "#"include { tok (\p _ -> alex $ Keyword p KwInclude) }+ <0> when { tok (\p _ -> alex $ Keyword p KwWhen) }+ <0> of { tok (\p _ -> alex $ Keyword p KwOf) }+ <0> ifcase { tok (\p _ -> alex $ Keyword p KwIfCase) }+ <0> stadef { tok (\p _ -> alex $ Keyword p KwStadef) }+ <0> stacst { tok (\p _ -> alex $ Keyword p KwStacst) }+ <0> local { tok (\p _ -> alex $ Keyword p KwLocal) }+ <0> praxi { tok (\p _ -> alex $ Keyword p KwPraxi) }+ <0> while { tok (\p _ -> alex $ Keyword p KwWhile) }+ <0> where { tok (\p _ -> alex $ Keyword p KwWhere) }+ <0> begin { tok (\p _ -> alex $ Keyword p KwBegin) }+ <0> overload { tok (\p _ -> alex $ Keyword p KwOverload) }+ <0> with { tok (\p _ -> alex $ Keyword p KwWith) }+ <0> extern { tok (\p _ -> alex $ Keyword p KwExtern) }+ <0> extvar { tok (\p _ -> alex $ Keyword p KwExtVar) }+ <0> sortdef { tok (\p _ -> alex $ Keyword p KwSortdef) }+ <0> propdef { tok (\p _ -> alex $ Keyword p KwPropdef) }+ <0> tkindef { tok (\p _ -> alex $ Keyword p KwTKind) }+ <0> typekindef { tok (\p _ -> alex $ Keyword p KwTKind) }+ <0> "$raise" { tok (\p _ -> alex $ Keyword p KwRaise) }+ <0> macdef { tok (\p _ -> alex $ Keyword p KwMacdef) }+ <0> mod { tok (\p _ -> alex $ Keyword p KwMod) }+ <0> datasort { tok (\p _ -> alex $ Keyword p KwDatasort) } <0> "println!" { tok (\p s -> alex $ Identifier p s) } <0> "prerrln!" { tok (\p s -> alex $ Identifier p s) }- <0> "fix@" { tok (\p s -> alex $ Keyword p KwFixAt) }- <0> "lam@" { tok (\p s -> alex $ Keyword p KwLambdaAt) }- <0> "addr" { tok (\p s -> alex $ Keyword p KwAddr) }- <0> "addr@" { tok (\p s -> alex $ Keyword p KwAddrAt) }- <0> "view@" { tok (\p s -> alex $ Keyword p KwViewAt) }- <0> sta { tok (\p s -> alex $ Keyword p KwSta) }- <0> symintr { tok (\p s -> alex $ Keyword p KwSymintr) }- <0> absview { tok (\p s -> alex $ Keyword p KwAbsview) }- <0> exception { tok (\p s -> alex $ Keyword p KwException) }- <0> "$list" { tok (\p s -> alex $ Keyword p (KwListLit "")) }- <0> "$list_vt" { tok (\p s -> alex $ Keyword p (KwListLit "_vt")) }+ <0> "fix@" { tok (\p _ -> alex $ Keyword p KwFixAt) }+ <0> "lam@" { tok (\p _ -> alex $ Keyword p KwLambdaAt) }+ <0> "addr" { tok (\p _ -> alex $ Keyword p KwAddr) }+ <0> "addr@" { tok (\p _ -> alex $ Keyword p KwAddrAt) }+ <0> "view@" { tok (\p _ -> alex $ Keyword p KwViewAt) }+ <0> sta { tok (\p _ -> alex $ Keyword p KwSta) }+ <0> symintr { tok (\p _ -> alex $ Keyword p KwSymintr) }+ <0> absview { tok (\p _ -> alex $ Keyword p KwAbsview) }+ <0> exception { tok (\p _ -> alex $ Keyword p KwException) }+ <0> "$list" { tok (\p _ -> alex $ Keyword p (KwListLit "")) }+ <0> "$list_vt" { tok (\p _ -> alex $ Keyword p (KwListLit "_vt")) } <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) }@@ -226,7 +232,7 @@ <0> @char_lit { tok (\p s -> alex $ CharTok p (toChar s)) } <0> @lambda { tok (\p s -> alex $ Arrow p s) } <0> @func_type { tok (\p s -> alex $ FuncType p s) }- <0> @time_lit { tok (\p s -> alex $ TimeTok 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> @at_brace { tok (\p s -> alex $ Operator p "@{") } -- FIXME this is kinda sloppy@@ -361,7 +367,7 @@ | CommentEnd AlexPosn | CommentContents AlexPosn String | MacroBlock AlexPosn String- | TimeTok AlexPosn String+ | UintTok AlexPosn Word | SignatureTok AlexPosn String | DoubleParenTok AlexPosn | DoubleBracesTok AlexPosn@@ -454,6 +460,9 @@ pretty (KwListLit s) = "list" <> string s pretty KwMacdef = "macdef" +instance Pretty Word where+ pretty = text . show+ instance Pretty Token where pretty (SpecialIdentifier _ s) = text ('$' : s) pretty (Identifier _ s) = text s@@ -471,7 +480,7 @@ pretty CommentEnd{} = "*)" pretty (CommentContents _ s) = text s pretty (FuncType _ s) = text s- pretty (TimeTok _ s) = text s+ pretty (UintTok _ u) = pretty u pretty (SignatureTok _ s) = ":" <> text s pretty (Operator _ s) = text s pretty (MacroBlock _ s) = "#"@@ -505,7 +514,7 @@ token_posn (CharTok p _) = p token_posn (CommentLex p _) = p token_posn (MacroBlock p _) = p-token_posn (TimeTok p _) = p+token_posn (UintTok p _) = p token_posn (SignatureTok p _) = p token_posn (DoubleParenTok p) = p token_posn (DoubleBracesTok p) = p
src/Language/ATS/Parser.y view
@@ -32,7 +32,7 @@ %name parseATS %tokentype { Token } %error { parseError }-%monad { Either (ATSError String) } { (>>=) } { pure }+%monad { Either ATSError } { (>>=) } { pure } %token fun { Keyword $$ KwFun }@@ -107,7 +107,7 @@ list { Keyword $$ (KwListLit "") } list_vt { Keyword $$ (KwListLit "_vt") } datasort { Keyword $$ KwDatasort }- timeLit { TimeTok _ $$ }+ uintLit { UintTok _ $$ } intLit { IntTok _ $$ } floatLit { FloatTok _ $$ } specialIdentifier { $$@SpecialIdentifier{} }@@ -259,7 +259,7 @@ | StaticExpression { Arg (Second (ConcreteType $1)) } -- | Parse a literal-Literal : timeLit { TimeLit $1 }+Literal : uintLit { UintLit $1 } | intLit { IntLit $1 } | floatLit { FloatLit $1 } | string { StringLit $1 }@@ -806,21 +806,21 @@ { -data ATSError a = Expected AlexPosn a a- | Unknown Token- | LexError String- deriving (Eq, Show, Generic, NFData)+data ATSError = Expected AlexPosn String String+ | Unknown Token+ | LexError String+ deriving (Eq, Show, Generic, NFData) instance Pretty AlexPosn where pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col -instance Pretty (ATSError String) where+instance Pretty ATSError where 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 pretty (LexError s) = red "Lexical error:" <+> text s -parseError :: [Token] -> Either (ATSError String) a+parseError :: [Token] -> Either ATSError a parseError = Left . Unknown . head }
src/Language/ATS/PrettyPrint.hs view
@@ -43,38 +43,38 @@ instance Eq Doc where (==) = on (==) show -pattern NoA :: [Arg]+pattern NoA :: [Arg a] pattern NoA = [NoArgs] -- | Pretty-print with sensible defaults.-printATS :: ATS -> String+printATS :: Eq a => ATS a -> String printATS = (<> "\n") . printATSCustom 0.6 120 -printATSCustom :: Float -- ^ Ribbon fraction+printATSCustom :: Eq a+ => Float -- ^ Ribbon fraction -> Int -- ^ Ribbon width- -> ATS -> String+ -> ATS a -> String printATSCustom r i x = g mempty where g = (displayS . renderSmart r i . pretty) x -- | Slightly faster pretty-printer without indendation (for code generation).-printATSFast :: ATS -> String+printATSFast :: Eq a => ATS a -> String printATSFast x = g mempty where g = (displayS . renderCompact . (<> "\n") . pretty) x -instance Pretty Name where+instance Pretty (Name a) where pretty (Unqualified n) = text n pretty (Qualified _ i n) = "$" <> text n <> "." <> text i pretty (SpecialName _ s) = "$" <> text s pretty (Functorial s s') = text s <> "$" <> text s' pretty (FieldName _ n n') = text n <> "." <> text n'- pretty Unnamed{} = mempty -instance Pretty LambdaType where+instance Pretty (LambdaType a) where pretty Plain{} = "=>" pretty Spear{} = "=>>" pretty (Full _ v) = "=<" <> text v <> ">" -instance Pretty BinOp where+instance Pretty (BinOp a) where pretty Mult = "*" pretty Add = "+" pretty Div = "/"@@ -95,7 +95,7 @@ pretty At = "@" pretty (SpecialInfix _ s) = text s -splits :: BinOp -> Bool+splits :: BinOp a -> Bool splits Mult = True splits Add = True splits Div = True@@ -131,21 +131,19 @@ prettyArgsProof (Just e) = prettyArgsG ("(" <> prettyArgsG mempty mempty (fmap pretty e) <+> "| ") ")" prettyArgsProof Nothing = prettyArgs -instance Pretty UnOp where+instance Pretty (UnOp a) where pretty Negate = "~" pretty Deref = "!" pretty (SpecialOp s) = text s -instance Pretty Expression where+instance Eq a => Pretty (Expression a) where 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 e') = flatAlt ("let" <$> indent 2 (pretty e) <$> endLet e') ("let" <+> pretty e <$> endLet e')- a (BoolLitF True) = "true"- a (BoolLitF False) = "false"- a (TimeLitF s) = text s+ a (UintLitF u) = pretty u <> "u" a (IntLitF i) = pretty i a (LambdaF _ lt p e) = let pre = "lam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e) a (LinearLambdaF _ lt p e) = let pre = "llam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)@@ -192,11 +190,11 @@ a (BeginF _ e) | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end") | otherwise = e- a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)+ a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e) a (LambdaAtF (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)- a (AddrAtF _ e) = "addr@" <> e- a (ViewAtF _ e) = "view@" <> e- a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es+ a (AddrAtF _ e) = "addr@" <> e+ a (ViewAtF _ e) = "view@" <> e+ a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es a (CommentExprF c e) = text c <$> e a (MacroVarF _ s) = ",(" <> text s <> ")" a BinListF{} = undefined -- Shouldn't happen@@ -214,7 +212,7 @@ patternHelper :: [Doc] -> Doc patternHelper ps = mconcat (punctuate ", " (reverse ps)) -instance Pretty Pattern where+instance Eq a => Pretty (Pattern a) where pretty = cata a where a (WildcardF _) = "_" a (PSumF s x) = string s <+> x@@ -230,21 +228,21 @@ a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p a (ExistentialPatternF e p) = pretty e <> p -argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc+argHelper :: Eq a => (Doc -> Doc -> Doc) -> Arg a -> Doc argHelper _ (Arg (First s)) = pretty s argHelper _ (Arg (Second t)) = pretty t argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t argHelper op (PrfArg a a') = pretty a `op` "|" `op` pretty a' argHelper _ NoArgs = undefined -- in theory we handle this elsewhere. -instance Pretty SortArg where+instance Eq a => Pretty (SortArg a) where pretty (SortArg n st) = text n <> ":" <+> pretty st pretty (Anonymous s) = pretty s -instance Pretty Arg where+instance Eq a => Pretty (Arg a) where pretty = argHelper (<+>) -squish :: BinOp -> Bool+squish :: BinOp a -> Bool squish Add = True squish Sub = True squish Mult = True@@ -254,7 +252,7 @@ endLet Nothing = "in end" endLet (Just d) = "in" <$> indent 2 d <$> "end" -instance Pretty StaticExpression where+instance Eq a => Pretty (StaticExpression a) where pretty = cata a where a (StaticValF n) = pretty n a (StaticBinaryF op se se')@@ -263,16 +261,14 @@ a (StaticIntF i) = pretty i a StaticVoidF{} = "()" a (SifF e e' e'') = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''- a (StaticBoolF True) = "true"- 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 op e) = pretty op <> e- a (SLetF _ e e') = flatAlt+ a (SUnaryF op e) = pretty op <> e+ a (SLetF _ e e') = flatAlt ("let" <$> indent 2 (pretty e) <$> endLet e') ("let" <+> pretty e <$> endLet e') -instance Pretty Sort where+instance Eq a => Pretty (Sort a) where pretty (T0p ad) = "t@ype" <> pretty ad pretty (Vt0p ad) = "vt@ype" <> pretty ad pretty (NamedSort s) = text s@@ -280,7 +276,7 @@ pretty (View _ t) = "view" <> pretty t pretty (VType _ a) = "vtype" <> pretty a -instance Pretty Type where+instance Eq a => Pretty (Type a) where pretty = cata a where a (NamedF n) = pretty n a (ViewTypeF _ t) = "view@" <> parens t@@ -307,7 +303,7 @@ a (AnonymousRecordF _ rs) = prettyRecord rs a (ParenTypeF _ t) = parens t -gan :: Maybe Sort -> Doc+gan :: Eq a => Maybe (Sort a) -> Doc gan (Just t) = " : " <> pretty t <> " " gan Nothing = "" @@ -315,32 +311,32 @@ withHashtag True = "#[" withHashtag _ = lbracket -instance Pretty Existential where+instance Eq a => Pretty (Existential a) where pretty (Existential [] b (Just st) (Just e')) = withHashtag b <> pretty st <> pretty e' <> rbracket pretty (Existential [] b Nothing (Just e')) = withHashtag b <> pretty e' <> rbracket pretty (Existential [e] b (Just st) Nothing) = withHashtag b <> text e <> ":" <> pretty st <> rbracket pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <+> rbracket pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <> "|" <+> pretty e <+> rbracket -instance Pretty Universal where+instance Eq a => Pretty (Universal a) where pretty (Universal [x] Nothing []) = lbrace <> text x <> rbrace pretty (Universal [x] (Just st) []) = lbrace <> text x <> ":" <> pretty st <> rbrace pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace -instance Pretty ATS where- pretty (ATS xs) = concatSame (fmap rewriteDecl (reverse xs))+instance Eq a => Pretty (ATS a) where+ pretty (ATS xs) = concatSame (reverse xs) -prettyOr :: (Pretty a) => [[a]] -> Doc+prettyOr :: (Pretty a, Eq a) => [[a]] -> Doc prettyOr [] = mempty prettyOr is = mconcat (fmap (prettyArgsU "<" ">") is) -prettyImplExpr :: Either StaticExpression Expression -> Doc+prettyImplExpr :: Eq a => Either (StaticExpression a) (Expression a) -> Doc prettyImplExpr (Left se) = pretty se prettyImplExpr (Right e) = pretty e -instance Pretty Implementation where+instance Eq a => Pretty (Implementation a) where pretty (Implement _ [] is [] n [] e) = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e) pretty (Implement _ [] is [] n NoA 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)@@ -348,13 +344,13 @@ pretty (Implement _ ps is [] n ias e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e) pretty (Implement _ ps is us n ias e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e) -isVal :: Declaration -> Bool+isVal :: Declaration a -> Bool isVal Val{} = True isVal Var{} = True isVal PrVal{} = True isVal _ = False -glue :: Declaration -> Declaration -> Bool+glue :: Declaration a -> Declaration a -> Bool glue x y | isVal x && isVal y = True glue Staload{} Staload{} = True@@ -373,7 +369,7 @@ {-# INLINE glue #-} -concatSame :: [Declaration] -> Doc+concatSame :: Eq a => [Declaration a] -> Doc concatSame [] = mempty concatSame [x] = pretty x concatSame (x:x':xs)@@ -409,7 +405,7 @@ prettyRecordF True ((s, t):xs) = prettyRecordF False xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t) <$> "}") prettyRecordF x ((s, t):xs) = prettyRecordF x xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t)) -prettyUsNil :: [Universal] -> Doc+prettyUsNil :: Eq a => [Universal a] -> Doc prettyUsNil [] = space prettyUsNil us = space <> foldMap pretty (reverse us) <> space @@ -417,20 +413,20 @@ prettyOf Nothing = mempty prettyOf (Just x) = space <> "of" <+> pretty x -prettyDL :: [DataPropLeaf] -> Doc+prettyDL :: Eq a => [DataPropLeaf a] -> Doc prettyDL [] = mempty prettyDL [DataPropLeaf us e e'] = indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e') prettyDL (DataPropLeaf us e e':xs) = prettyDL xs $$ indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e') -universalHelper :: [Universal] -> Doc+universalHelper :: Eq a => [Universal a] -> Doc universalHelper = mconcat . fmap pretty . reverse -prettyDSL :: [DataSortLeaf] -> Doc+prettyDSL :: Eq a => [DataSortLeaf a] -> Doc prettyDSL [] = mempty prettyDSL [DataSortLeaf us sr sr'] = indent 2 ("|" <> prettyUsNil us <> pretty sr <> prettyOf sr') prettyDSL (DataSortLeaf us sr sr':xs) = prettyDSL xs $$ indent 2 ("|" <> prettyUsNil us <> pretty sr <> prettyOf sr') -prettyLeaf :: [Leaf] -> Doc+prettyLeaf :: Eq a => [Leaf a] -> Doc prettyLeaf [] = mempty prettyLeaf [Leaf [] s [] Nothing] = indent 2 ("|" <+> text s) prettyLeaf [Leaf [] s [] (Just e)] = indent 2 ("|" <+> text s <+> "of" <+> pretty e)@@ -479,11 +475,11 @@ prettyArgs :: (Pretty a) => [a] -> Doc prettyArgs = prettyArgs' ", " "(" ")" -prettyArgsNil :: [Arg] -> Doc+prettyArgsNil :: Eq a => [Arg a] -> Doc prettyArgsNil NoA = mempty prettyArgsNil as = prettyArgs' ", " "(" ")" as -fancyU :: [Universal] -> Doc+fancyU :: Eq a => [Universal a] -> Doc fancyU = foldMap pretty . reverse (<#>) :: Doc -> Doc -> Doc@@ -501,7 +497,7 @@ prettyTermetric Nothing = mempty -- FIXME figure out a nicer algorithm for when/how to split lines.-instance Pretty PreFunction where+instance Eq a => Pretty (PreFunction a) where pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e) pretty (PreF i si [] us as rt t (Just e)) = pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e) pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)@@ -512,11 +508,11 @@ pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <+> ":" <> text si <#> pretty rt pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt -instance Pretty DataPropLeaf where+instance Eq a => Pretty (DataPropLeaf a) where pretty (DataPropLeaf us e Nothing) = "|" <+> foldMap pretty (reverse us) <+> pretty e pretty (DataPropLeaf us e (Just e')) = "|" <+> foldMap pretty (reverse us) <+> pretty e <+> "of" <+> pretty e' -instance Pretty Fixity where+instance Eq a => Pretty (Fixity a) where pretty (Infix _ i) = "infix" <+> pretty i pretty (RightFix _ i) = "infixr" <+> pretty i pretty (LeftFix _ i) = "infixl" <+> pretty i@@ -534,7 +530,7 @@ prettySortArgs Nothing = mempty prettySortArgs (Just as) = prettyArgs' ", " "(" ")" as -instance Pretty Declaration where+instance Eq a => Pretty (Declaration a) where pretty (Exception s t) = "exception" <+> text s <+> "of" <+> pretty t pretty (AbsType _ s as t) = "abstype" <+> text s <> prettySortArgs as <> prettyMaybeType t pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettySortArgs as
src/Language/ATS/Types.hs view
@@ -67,130 +67,126 @@ import Data.Maybe (isJust) import Data.Semigroup (Semigroup) import GHC.Generics (Generic)-import Language.ATS.Lexer (Addendum (..), AlexPosn)+import Language.ATS.Lexer (Addendum (..)) --- uses an 'Int' because you fully deserve what you get if your--- fixity declarations overflow.-data Fixity = RightFix { pos :: AlexPosn, ifix :: Int }- | LeftFix { pos :: AlexPosn, ifix :: Int }- | Pre { pos :: AlexPosn, ifix :: Int }- | Post { pos :: AlexPosn, ifix :: Int }- | Infix { pos :: AlexPosn, ifix :: Int }- deriving (Show, Eq, Generic, NFData)+data Fixity a = RightFix { pos :: a, ifix :: Int }+ | LeftFix { pos :: a, ifix :: Int }+ | Pre { pos :: a, ifix :: Int }+ | Post { pos :: a, ifix :: Int }+ | Infix { pos :: a, ifix :: Int }+ deriving (Show, Eq, Generic, NFData) -- | Newtype wrapper containing a list of declarations-newtype ATS = ATS { unATS :: [Declaration] }+newtype ATS a = ATS { unATS :: [Declaration a] } deriving (Show, Eq, Generic) deriving newtype (NFData, Semigroup, Monoid) -data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [StaticExpression], maybeType :: Maybe Type }+data Leaf a = Leaf { _constructorUniversals :: [Universal a], name :: String, constructorArgs :: [StaticExpression a], maybeType :: Maybe (Type a) } deriving (Show, Eq, Generic, NFData) -type SortArgs = Maybe [SortArg]+type SortArgs a = Maybe [SortArg a] -- | Declare something in a scope (a function, value, action, etc.)-data Declaration = Func { pos :: AlexPosn, _fun :: Function }- | Impl [Arg] Implementation -- TODO do something better for implicit universals- | ProofImpl [Arg] Implementation- | Val Addendum (Maybe Type) Pattern Expression- | StaVal [Universal] String Type- | PrVal Pattern Expression- | Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression) -- TODO AlexPosn- | AndDecl (Maybe Type) Pattern Expression- | Include String- | Staload Bool (Maybe String) String- | Stadef String SortArgs Type -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n]- | CBlock String- | TypeDef AlexPosn String SortArgs Type- | ViewTypeDef AlexPosn String SortArgs Type- | SumType { typeName :: String, typeArgs :: SortArgs, _leaves :: [Leaf] }- | SumViewType { typeName :: String, typeArgs :: SortArgs, _leaves :: [Leaf] }- | AbsType AlexPosn String SortArgs (Maybe Type)- | AbsViewType AlexPosn String SortArgs (Maybe Type)- | AbsView AlexPosn String SortArgs (Maybe Type)- | AbsVT0p AlexPosn String SortArgs (Maybe Type)- | AbsT0p AlexPosn String SortArgs (Maybe Type)- | ViewDef AlexPosn String SortArgs Type- | OverloadOp AlexPosn BinOp Name (Maybe Int)- | OverloadIdent AlexPosn String Name (Maybe Int)- | Comment { _comment :: String }- | DataProp AlexPosn String SortArgs [DataPropLeaf]- | DataView AlexPosn String SortArgs [Leaf]- | Extern AlexPosn Declaration- | Define String- | SortDef AlexPosn String (Either Sort Universal)- | AndD Declaration Declaration- | Local AlexPosn ATS ATS- | AbsProp AlexPosn String [Arg]- | Assume Name [Arg] Type- | TKind AlexPosn Name String- | SymIntr AlexPosn Name- | Stacst AlexPosn Name Type (Maybe Expression)- | PropDef AlexPosn String [Arg] Type- | FixityDecl Fixity [String]- | MacDecl AlexPosn String [String] Expression- | DataSort AlexPosn String [DataSortLeaf]- | Exception String Type- | ExtVar AlexPosn String Expression- deriving (Show, Eq, Generic, NFData)+data Declaration a = Func { pos :: a, _fun :: Function a }+ | Impl [Arg a] (Implementation a) -- TODO do something better for implicit universals+ | ProofImpl [Arg a] (Implementation a)+ | Val Addendum (Maybe (Type a)) (Pattern a) (Expression a)+ | StaVal [Universal a] String (Type a)+ | PrVal (Pattern a) (Expression a)+ | Var (Maybe (Type a)) (Pattern a) (Maybe (Expression a)) (Maybe (Expression a)) -- TODO a+ | AndDecl (Maybe (Type a)) (Pattern a) (Expression a)+ | Include String+ | Staload Bool (Maybe String) String+ | Stadef String (SortArgs a) (Type a) -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n]+ | CBlock String+ | TypeDef a String (SortArgs a) (Type a)+ | ViewTypeDef a String (SortArgs a) (Type a)+ | SumType { typeName :: String, typeArgs :: SortArgs a, _leaves :: [Leaf a] }+ | SumViewType { typeName :: String, typeArgs :: SortArgs a, _leaves :: [Leaf a] }+ | AbsType a String (SortArgs a) (Maybe (Type a))+ | AbsViewType a String (SortArgs a) (Maybe (Type a))+ | AbsView a String (SortArgs a) (Maybe (Type a))+ | AbsVT0p a String (SortArgs a) (Maybe (Type a))+ | AbsT0p a String (SortArgs a) (Maybe (Type a))+ | ViewDef a String (SortArgs a) (Type a)+ | OverloadOp a (BinOp a) (Name a) (Maybe Int)+ | OverloadIdent a String (Name a) (Maybe Int)+ | Comment { _comment :: String }+ | DataProp a String (SortArgs a) [DataPropLeaf a]+ | DataView a String (SortArgs a) [Leaf a]+ | Extern a (Declaration a)+ | Define String+ | SortDef a String (Either (Sort a) (Universal a))+ | AndD (Declaration a) (Declaration a)+ | Local a (ATS a) (ATS a)+ | AbsProp a String [Arg a]+ | Assume (Name a) [Arg a] (Type a)+ | TKind a (Name a) String+ | SymIntr a (Name a)+ | Stacst a (Name a) (Type a) (Maybe (Expression a))+ | PropDef a String [Arg a] (Type a)+ | FixityDecl (Fixity a) [String]+ | MacDecl a String [String] (Expression a)+ | DataSort a String [DataSortLeaf a]+ | Exception String (Type a)+ | ExtVar a String (Expression a)+ deriving (Show, Eq, Generic, NFData) -data DataSortLeaf = DataSortLeaf [Universal] Sort (Maybe Sort)- deriving (Show, Eq, Generic, NFData)+data DataSortLeaf a = DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a))+ deriving (Show, Eq, Generic, NFData) -data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)- deriving (Show, Eq, Generic, NFData)+data DataPropLeaf a = DataPropLeaf [Universal a] (Expression a) (Maybe (Expression a))+ deriving (Show, Eq, Generic, NFData) -- | A type for parsed ATS types-data Type = Tuple AlexPosn [Type]- | Named Name- | Ex Existential (Maybe Type)- | ForA Universal Type- | Dependent { _typeCall :: Name, _typeCallArgs :: [Type] }- | Unconsumed Type -- @!a@- | AsProof Type (Maybe Type) -- @a >> b@- | FromVT Type -- | @a?!@- | MaybeVal Type -- | @a?@- | AtExpr AlexPosn Type StaticExpression- | AtType AlexPosn Type- | ProofType AlexPosn [Type] Type -- Aka (prf | val)- | ConcreteType StaticExpression- | RefType Type- | ViewType AlexPosn Type- | FunctionType String Type Type- | NoneType AlexPosn- | ImplicitType AlexPosn- | ViewLiteral Addendum- | AnonymousRecord AlexPosn [(String, Type)]- | ParenType AlexPosn Type- deriving (Show, Eq, Generic, NFData)---- | A type for the various lambda arrows (@=>@, @=\<cloref1>@, etc.)-data LambdaType = Plain AlexPosn- | Full AlexPosn String- | Spear AlexPosn- deriving (Show, Eq, Generic, NFData)+data Type a = Tuple a [Type a]+ | Named (Name a)+ | Ex (Existential a) (Maybe (Type a))+ | ForA (Universal a) (Type a)+ | Dependent { _typeCall :: Name a, _typeCallArgs :: [Type a] }+ | Unconsumed (Type a) -- @!a@+ | AsProof (Type a) (Maybe (Type a)) -- @a >> b@+ | FromVT (Type a) -- | @a?!@+ | MaybeVal (Type a) -- | @a?@+ | AtExpr a (Type a) (StaticExpression a)+ | AtType a (Type a)+ | ProofType a [Type a] (Type a) -- Aka (prf | val)+ | ConcreteType (StaticExpression a)+ | RefType (Type a)+ | ViewType a (Type a)+ | FunctionType String (Type a) (Type a)+ | NoneType a+ | ImplicitType a+ | ViewLiteral Addendum+ | AnonymousRecord a [(String, Type a)]+ | ParenType a (Type a)+ deriving (Show, Eq, Generic, NFData) +-- | A type for @=>@, @=\<cloref1>@, etc.+data LambdaType a = Plain a+ | Full a String+ | Spear a+ deriving (Show, Eq, Generic, NFData) -data Name = Unqualified String- | Qualified AlexPosn String String -- ^ A name can be qualified (@$UN.unsafefn@)- | SpecialName AlexPosn String -- ^ A name for builtin functions such as @$showtype@.- | Functorial String String- | FieldName AlexPosn String String- | Unnamed AlexPosn- deriving (Show, 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) -- | A data type for patterns.-data Pattern = Wildcard AlexPosn- | PName Name [Pattern]- | PSum String Pattern- | PLiteral Expression- | Guarded AlexPosn Expression Pattern- | Free Pattern- | Proof AlexPosn [Pattern] [Pattern]- | TuplePattern [Pattern]- | AtPattern AlexPosn Pattern- | UniversalPattern AlexPosn String [Universal] Pattern- | ExistentialPattern Existential Pattern+data Pattern a = Wildcard a+ | PName (Name a) [Pattern a]+ | PSum String (Pattern a)+ | PLiteral (Expression a)+ | Guarded a (Expression a) (Pattern a)+ | Free (Pattern a)+ | Proof a [Pattern a] [Pattern a]+ | TuplePattern [Pattern a]+ | AtPattern a (Pattern a)+ | UniversalPattern a String [Universal a] (Pattern a)+ | ExistentialPattern (Existential a) (Pattern a) deriving (Show, Eq, Generic, NFData) data Paired a b = Both a b@@ -198,168 +194,164 @@ | Second b deriving (Show, Eq, Generic, NFData) -data SortArg = SortArg String Sort- | Anonymous Sort+data SortArg a = SortArg String (Sort a)+ | Anonymous (Sort a) deriving (Show, Eq, Generic, NFData) -- | An argument to a function.-data Arg = Arg (Paired String Type)- | PrfArg Arg Arg- | NoArgs- deriving (Show, Eq, Generic, NFData)+data Arg a = Arg (Paired String (Type a))+ | PrfArg (Arg a) (Arg a)+ | NoArgs+ deriving (Show, Eq, Generic, NFData) -- | A datatype for sorts.-data Sort = NamedSort { _sortName :: String }- | T0p Addendum -- ^ t@ype- | Vt0p Addendum -- ^ vt@ype- | Addr- | VType AlexPosn Addendum -- ^ viewtype or vtype- | View AlexPosn Addendum -- ^ view- deriving (Show, Eq, Generic, NFData)+data Sort a = NamedSort { _sortName :: String }+ | T0p Addendum -- ^ t@ype+ | Vt0p Addendum -- ^ vt@ype+ | Addr+ | VType a Addendum -- ^ viewtype or vtype+ | View a Addendum -- ^ view+ deriving (Show, Eq, Generic, NFData) -- FIXME a type for sorts? -- | Wrapper for universal quantifiers (refinement types)-data Universal = Universal { bound :: [String], typeU :: Maybe Sort, prop :: [StaticExpression] }+data Universal a = Universal { bound :: [String], typeU :: Maybe (Sort a), prop :: [StaticExpression a] } deriving (Show, Eq, Generic, NFData) -- | Wrapper for existential quantifiers/types-data Existential = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe Sort, propE :: Maybe StaticExpression }+data Existential a = Existential { boundE :: [String], isOpen :: Bool, typeE :: Maybe (Sort a), propE :: Maybe (StaticExpression a) } deriving (Show, Eq, Generic, NFData) -- | @~@ is used to negate numbers in ATS-data UnOp = Negate- | Deref- | SpecialOp String+data UnOp a = Negate+ | Deref+ | SpecialOp String deriving (Show, Eq, Generic, NFData) -- | Binary operators on expressions-data BinOp = Add- | Mult- | Div- | Sub- | GreaterThan- | GreaterThanEq- | LessThan- | LessThanEq- | Equal- | NotEqual- | LogicalAnd- | LogicalOr- | StaticEq- | Mod- | NotEq- | Mutate -- ^ @:=@- | At- | SpearOp -- ^ @->@- | SpecialInfix AlexPosn String- deriving (Show, Eq, Generic, NFData)+data BinOp a = Add+ | Mult+ | Div+ | Sub+ | GreaterThan+ | GreaterThanEq+ | LessThan+ | LessThanEq+ | Equal+ | NotEqual+ | LogicalAnd+ | LogicalOr+ | StaticEq+ | Mod+ | NotEq+ | Mutate -- ^ @:=@+ | At+ | SpearOp -- ^ @->@+ | SpecialInfix a String+ deriving (Show, Eq, Generic, NFData) --- FIXME add position information?-data StaticExpression = StaticVal Name- | StaticBinary BinOp StaticExpression StaticExpression- | StaticInt Int- | SPrecede StaticExpression StaticExpression- | StaticBool Bool- | 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)+data StaticExpression a = StaticVal (Name a)+ | StaticBinary (BinOp a) (StaticExpression a) (StaticExpression a)+ | StaticInt Int+ | SPrecede (StaticExpression a) (StaticExpression a)+ | StaticVoid a+ | Sif { scond :: StaticExpression a, wwhenTrue :: StaticExpression a, selseExpr :: StaticExpression a } -- Static if (for proofs)+ | SCall (Name a) [StaticExpression a]+ | SUnary (UnOp a) (StaticExpression a)+ | SLet a [Declaration a] (Maybe (StaticExpression a))+ deriving (Show, Eq, Generic, NFData) -- | A (possibly effectful) expression.-data Expression = Let AlexPosn ATS (Maybe Expression)- | VoidLiteral -- The '()' literal representing inaction.- AlexPosn- -- function call: <a>, then {n}- | Call Name [[Type]] [Type] (Maybe [Expression]) [Expression]- | NamedVal Name- | ListLiteral AlexPosn String Type [Expression]- | If { cond :: Expression -- ^ Expression evaluating to a boolean value- , whenTrue :: Expression -- ^ Expression to be returned when true- , elseExpr :: Maybe Expression -- ^ Expression to be returned when false- }- | BoolLit Bool- | TimeLit String- | FloatLit Float- | IntLit Int- | UnderscoreLit AlexPosn- | Lambda AlexPosn LambdaType Pattern Expression- | LinearLambda AlexPosn LambdaType Pattern Expression- | Index AlexPosn Name Expression- | Access AlexPosn Expression Name- | StringLit String- | CharLit Char- | AddrAt AlexPosn Expression- | ViewAt AlexPosn Expression- | Binary BinOp Expression Expression- | Unary UnOp Expression- | IfCase { posE :: AlexPosn- , ifArms :: [(Expression, LambdaType, Expression)]- }- | Case { posE :: AlexPosn- , kind :: Addendum- , val :: Expression- , arms :: [(Pattern, LambdaType, Expression)] -- ^ Each @(Pattern, Expression)@ pair corresponds to a branch of the 'case' statement+data Expression a = Let a (ATS a) (Maybe (Expression a))+ | VoidLiteral -- ^ The '()' literal representing inaction.+ a+ | Call (Name a) [[Type a]] [Type a] (Maybe [Expression a]) [Expression a]+ | NamedVal (Name a)+ | ListLiteral a String (Type a) [Expression a]+ | If { cond :: Expression a -- ^ Expression evaluating to a boolean value+ , whenTrue :: Expression a -- ^ Expression to be returned when true+ , elseExpr :: Maybe (Expression a) -- ^ Expression to be returned when false }- | RecordValue AlexPosn [(String, Expression)] (Maybe Type)- | Precede Expression Expression- | ProofExpr AlexPosn Expression Expression- | TypeSignature Expression Type- | WhereExp Expression ATS- | TupleEx AlexPosn [Expression] -- TODO support boxed tuples- | While AlexPosn Expression Expression- | Actions ATS- | Begin AlexPosn Expression- | BinList { _op :: BinOp, _exprs :: [Expression] }- | PrecedeList { _exprs :: [Expression] }- | FixAt String StackFunction- | LambdaAt StackFunction- | ParenExpr AlexPosn Expression- | CommentExpr String Expression- | MacroVar AlexPosn String- deriving (Show, Eq, Generic, NFData)+ | UintLit Word -- ^ @1000u@+ | FloatLit Float+ | IntLit Int+ | UnderscoreLit a+ | Lambda a (LambdaType a) (Pattern a) (Expression a)+ | LinearLambda a (LambdaType a) (Pattern a) (Expression a)+ | Index a (Name a) (Expression a)+ | Access a (Expression a) (Name a)+ | StringLit String+ | CharLit Char+ | AddrAt a (Expression a)+ | ViewAt a (Expression a)+ | Binary (BinOp a) (Expression a) (Expression a)+ | Unary (UnOp a) (Expression a)+ | IfCase { posE :: a+ , ifArms :: [(Expression a, LambdaType a, Expression a)]+ }+ | Case { posE :: a+ , kind :: Addendum+ , val :: Expression a+ , arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each @((Pattern a), (Expression a))@ pair corresponds to a branch of the 'case' statement+ }+ | RecordValue a [(String, Expression a)] (Maybe (Type a))+ | Precede (Expression a) (Expression a)+ | ProofExpr a (Expression a) (Expression a)+ | TypeSignature (Expression a) (Type a)+ | WhereExp (Expression a) (ATS a)+ | TupleEx a [Expression a] -- TODO support boxed tuples+ | While a (Expression a) (Expression a)+ | Actions (ATS a)+ | Begin a (Expression a)+ | BinList { _op :: BinOp a, _exprs :: [Expression a] }+ | PrecedeList { _exprs :: [Expression a] }+ | FixAt String (StackFunction a)+ | LambdaAt (StackFunction a)+ | ParenExpr a (Expression a)+ | CommentExpr String (Expression a)+ | MacroVar a String+ deriving (Show, Eq, Generic, NFData) -- | An 'implement' or 'primplmnt' declaration-data Implementation = Implement { pos :: AlexPosn- , preUniversalsI :: [Universal]- , implicits :: [[Type]] -- ^ Implicit arguments- , universalsI :: [Universal] -- ^ Universal quantifiers- , nameI :: Name -- ^ Name of the template being implemented- , iArgs :: [Arg] -- ^ Arguments- , iExpression :: Either StaticExpression Expression -- ^ Expression (or static expression) holding the function body.- }+data Implementation a = Implement { pos :: a+ , preUniversalsI :: [Universal a]+ , implicits :: [[Type a]] -- ^ Implicit arguments+ , universalsI :: [Universal a] -- ^ Universal quantifiers+ , nameI :: Name a -- ^ (Name a) of the template being implemented+ , iArgs :: [Arg a] -- ^ Arguments+ , iExpression :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.+ } deriving (Show, Eq, Generic, NFData) -- | A function declaration accounting for all keywords ATS uses to -- define them.-data Function = Fun { _preF :: PreFunction }- | Fn { _preF :: PreFunction }- | Fnx { _preF :: PreFunction }- | And { _preF :: PreFunction }- | PrFun { _preF :: PreFunction }- | PrFn { _preF :: PreFunction }- | Praxi { _preF :: PreFunction }- | CastFn { _preF :: PreFunction }- deriving (Show, Eq, Generic, NFData)+data Function a = Fun { _preF :: PreFunction a }+ | Fn { _preF :: PreFunction a }+ | Fnx { _preF :: PreFunction a }+ | And { _preF :: PreFunction a }+ | PrFun { _preF :: PreFunction a }+ | PrFn { _preF :: PreFunction a }+ | Praxi { _preF :: PreFunction a }+ | CastFn { _preF :: PreFunction a }+ deriving (Show, Eq, Generic, NFData) -data StackFunction = StackF { stSig :: String- , stArgs :: [Arg]- , stReturnType :: Type- , stExpression :: Expression- }- deriving (Show, Eq, Generic, NFData)+data StackFunction a = StackF { stSig :: String+ , stArgs :: [Arg a]+ , stReturnType :: Type a+ , stExpression :: Expression a+ }+ deriving (Show, Eq, Generic, NFData) -data PreFunction = PreF { fname :: Name -- ^ Function name- , sig :: String -- ^ e.g. <> or \<!wrt>- , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic- , universals :: [Universal] -- ^ Universal quantifiers/refinement type- , args :: [Arg] -- ^ Actual function arguments- , returnType :: Maybe Type -- ^ Return type- , termetric :: Maybe StaticExpression -- ^ Optional termination metric- , _expression :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)- }- deriving (Show, Eq, Generic, NFData)+data PreFunction a = PreF { fname :: Name a -- ^ Function name+ , sig :: String -- ^ e.g. <> or \<!wrt>+ , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic+ , universals :: [Universal a] -- ^ (Universal a) quantifiers/refinement type+ , args :: [Arg a] -- ^ Actual function arguments+ , returnType :: Maybe (Type a) -- ^ Return type+ , termetric :: Maybe (StaticExpression a) -- ^ Optional termination metric+ , _expression :: Maybe (Expression a) -- ^ Expression holding the actual function body (not present in static templates)+ }+ deriving (Show, Eq, Generic, NFData) makeBaseFunctor ''Pattern makeBaseFunctor ''Expression@@ -371,10 +363,10 @@ makeLenses ''Function makeLenses ''Type -rewriteDecl :: Declaration -> Declaration+rewriteDecl :: Eq a => Declaration a -> Declaration a rewriteDecl x@SumViewType{} = g x where g = over (leaves.mapped.constructorUniversals) h- h :: [Universal] -> [Universal]+ h :: Eq a => [Universal a] -> [Universal a] h = ana c where c (y:y':ys) | typeU y == typeU y' && isJust (typeU y) =@@ -383,20 +375,20 @@ rewriteDecl x = x -- FIXME left vs. right shouldn't be treated the same-instance Ord Fixity where+instance (Eq a) => Ord (Fixity a) where compare = on compare ifix -leftFix :: Int -> Fixity+leftFix :: Int -> Fixity a leftFix = LeftFix undefined -rightFix :: Int -> Fixity+rightFix :: Int -> Fixity a rightFix = RightFix undefined -infix_ :: Int -> Fixity+infix_ :: Int -> Fixity a infix_ = Infix undefined -- | Default fixities from @fixity.ats@-getFixity :: BinOp -> Fixity+getFixity :: BinOp a -> Fixity a getFixity Add = leftFix 50 getFixity Sub = leftFix 50 getFixity Mutate = infix_ 0@@ -415,10 +407,10 @@ getFixity Mod = leftFix 60 getFixity _ = leftFix 100 -instance Ord BinOp where+instance (Eq a) => Ord (BinOp a) where compare = on compare getFixity -rewriteATS :: Expression -> Expression+rewriteATS :: Eq a => Expression a -> Expression a rewriteATS = cata a where a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e] a (CallF n ts ts' me [ParenExpr _ e@Call{}]) = Call n ts ts' me [e]