diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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 diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -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] diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 } - @block_comment_end { tok (\p s -> alex $ CommentEnd p) `andBegin` 0 } + <0> @block_comment_start { tok (\p _ -> alex $ CommentBegin p) `andBegin` one } + @block_comment_end { tok (\p _ -> alex $ CommentEnd p) `andBegin` 0 } @block_comment_start { tok (\p s -> alex $ CommentContents p s) `andBegin` two } [^\*\(\)\/]+ { tok (\p s -> alex $ CommentContents p s) } @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } @comment_general { tok (\p s -> alex $ CommentContents p s) } @block_comment_end { tok (\p s -> alex $ CommentContents p s) `andBegin` one } + @block_comment_start { tok (\p s -> alex $ CommentContents p s) `andBegin` three } [^\*\(\)\/]+ { tok (\p s -> alex $ CommentContents p s) } @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } @comment_general { tok (\p s -> alex $ CommentContents p s) } + @block_comment_end { tok (\p s -> alex $ CommentContents p s) `andBegin` two } + @block_comment_start { tok (\_ _ -> alexError "Nested comments of depth >3 are not supported.") } + [^\*\(\)\/]+ { tok (\p s -> alex $ CommentContents p s) } + @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) } + @comment_general { tok (\p s -> alex $ CommentContents p s) } <0> "//".* { tok (\p s -> alex $ CommentLex p s) } <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 diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 (@=>@, @=\@, 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 @=>@, @=\@, 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: , 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 \ - , 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 \ + , 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]