diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -19,6 +19,9 @@ os: osx language: default + allow_failures: + - env: TARGET="x86_64-apple-darwin" + before_install: - mkdir -p ~/.local/bin - export PATH=$HOME/.local/bin:$PATH @@ -60,11 +63,16 @@ echo "skipping yaml verification..." fi - stack build --test --bench --no-run-tests --no-run-benchmarks - - find -name atsfmt -executable - | if [ `uname` = "Darwin" ] + find .stack-work -name atsfmt -perm 755 + else + echo 'nothing' + fi + - | + if [ `uname` = "Darwin" ] then - export BINPATH="$(find . -name atsfmt -perm 755 | tail -n1)" + export BINPATH="$(find .stack-work -name atsfmt -perm 755 | tail -n1)" else export BINPATH="$(find -name atsfmt -executable | tail -n1)" fi diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -1,3 +1,8 @@ +darcs: + @darcs optimize clean + @darcs optimize pristine + @darcs optimize cache + clean: sn c . rm -rf tags *.c diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,7 +7,8 @@ Currently it is only tested with ATS 0.3.8. If you find something that's not listed in `TODO.md` feel free to open -an issue. +an issue. The pretty-printer is a bit anemic, so you're welcome to submit code +samples where it produces bad output. The formatter is pleasantly fast, formatting a 1500 line file in <20ms. @@ -39,4 +40,4 @@ ## License -All code except `test/data/left-pad.dats` is license under the BSD3 license. +All code except `test/data/left-pad.dats` is licensed under the BSD3 license. diff --git a/ats-format.cabal b/ats-format.cabal --- a/ats-format.cabal +++ b/ats-format.cabal @@ -1,5 +1,5 @@ name: ats-format -version: 0.1.0.3 +version: 0.1.0.4 synopsis: A source-code formatter for ATS description: An opinionated source-code formatter for ATS (http://www.ats-lang.org/). homepage: https://hub.darcs.net/vmchale/ats-format#readme @@ -42,7 +42,7 @@ , Language.ATS.PrettyPrint , Language.ATS.Exec , Paths_ats_format - build-depends: base >= 4.9 && < 5 + build-depends: base >= 4.8 && < 5 , array , lens , deepseq @@ -87,6 +87,15 @@ build-depends: base , ats-format , hspec + , dirstream + , pipes + , system-filepath + , pipes-safe + , filepath + , mtl + , hspec-core + if flag(development) + ghc-options: -Werror if impl(ghc >= 8.0) ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall @@ -100,6 +109,8 @@ , ats-format , criterion ghc-options: -Wall + if flag(development) + ghc-options: -Werror if impl(ghc >= 8.0) ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat default-language: Haskell2010 diff --git a/man/atsfmt.1 b/man/atsfmt.1 --- a/man/atsfmt.1 +++ b/man/atsfmt.1 @@ -65,6 +65,19 @@ clang\-format\ =\ true \f[] .fi +.PP +You can also set ribbon width and line width in the file, viz. +.IP +.nf +\f[C] +ribbon\ =\ 0.6 +width\ =\ 120 +\f[] +.fi +.PP +Ribbon width is the width of a line excluding indentation. +In this example, the maximum column number will be 120 and the maximum +ribbon width will be 0.6 * 120 = 72 characters. .SH EDITOR INTEGRATION .PP Editor integration is available with the ATS vim plugin at: 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 @@ -32,9 +32,9 @@ $alpha = [a-zA-Z] $terminal = $printable # $white $esc_char = \27 -@escape_ch = \\ (n | t | \') -@escape_str = \\ (n | t | \") -@char = ($terminal # $special) | @escape_ch | $esc_char +@escape_ch = \\ [nt\'\\] +@escape_str = \\ [nt\"\\] +@char = ($terminal # [\\\']) | " " | @escape_ch | $esc_char @bool = (true | false) @char_lit = \' @char \' @@ -69,9 +69,9 @@ @ref_call = @identifier "<" ($alpha | $digit | "(" | ")" | _)+ ">" @not_close_c = \% [^\}] -@c_block = \%\{ ([^\%] | @not_close_c | \n)* \%\} +@c_block = \%\{ ([^\%] | @not_close_c | \n)* \%\} -- TODO include %{# and %{$ -@lambda = "=>" | "=" | "=" | "=>>" +@lambda = "=>" | "=" | "=" | "=>>" | "=" -- FIXME whatever the fuck this is: - @func_type = "-" | "-" | "-" | "-" | "-" | "-<>" | "-" -- FIXME allow spaces after comma? @@ -89,6 +89,7 @@ tokens :- $white+ ; + ^ @block_comment { tok (\p s -> CommentLex p s) } ^ "//".* { tok (\p s -> CommentLex p s) } "//".* ; @block_comment ; @@ -119,8 +120,8 @@ case"-" { tok (\p s -> Keyword p (KwCase Minus)) } case { tok (\p s -> Keyword p (KwCase None)) } castfn { tok (\p s -> Keyword p KwCastfn) } - val"+" { tok (\p s -> Keyword p (KwVal Plus)) } - val"-" { tok (\p s -> Keyword p (KwVal Minus)) } + val"+" { tok (\p s -> Keyword p (KwVal Plus)) } -- TODO also val@ ? + val"-" { tok (\p s -> Keyword p (KwVal Minus)) } val { tok (\p s -> Keyword p (KwVal None)) } var { tok (\p s -> Keyword p KwVar) } int { tok (\p s -> Keyword p KwInt) } @@ -165,7 +166,7 @@ @double_parens { tok (\p s -> DoubleParenTok p) } @double_braces { tok (\p s -> DoubleBracesTok p) } @double_brackets { tok (\p s -> DoubleBracketTok p) } - @char_lit { tok (\p s -> CharTok p (s !! 1)) } + @char_lit { tok (\p s -> CharTok p (toChar s)) } @lambda { tok (\p s -> Arrow p s) } @func_type { tok (\p s -> FuncType p s) } @bool { tok (\p s -> BoolTok p (read (over _head toUpper s)))} @@ -296,6 +297,12 @@ token_posn (DoubleParenTok p) = p token_posn (DoubleBracesTok p) = p token_posn (DoubleBracketTok p) = p + +toChar :: String -> Char +toChar "'\\n'" = '\n' +toChar "'\\t'" = '\t' +toChar "'\\\\'" = '\\' +toChar x = x !! 1 -- | This function turns a string into a stream of tokens for the parser. lexATS :: String -> [Token] 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 @@ -84,6 +84,7 @@ view { Keyword $$ KwView } raise { Keyword $$ KwRaise } tkindef { Keyword $$ KwTKind } + assume { Keyword $$ KwAssume } boolLit { BoolTok _ $$ } timeLit { TimeTok _ $$ } intLit { IntTok _ $$ } @@ -91,6 +92,7 @@ effmaskWrt { Identifier $$ "effmask_wrt" } effmaskAll { Identifier $$ "effmask_all" } extfcall { Identifier $$ "extfcall" } + ldelay { Identifier $$ "ldelay" } -- TODO token? raise { Identifier $$ "raise" } identifier { Identifier _ $$ } closeParen { Special $$ ")" } @@ -115,6 +117,7 @@ plainArrow { Arrow $$ "=>" } cloref1Arrow { Arrow $$ "=" } cloptr1Arrow { Arrow $$ "=" } + lincloptr1Arrow { Arrow $$ "=" } spear { Arrow $$ "=>>" } lsqbracket { Special $$ "[" } rsqbracket { Special $$ "]" } @@ -173,10 +176,10 @@ | t0pCo { T0p Plus } | vt0pPlain { Vt0p None } | vt0pCo { Vt0p Plus } - | stringType openParen Expression closeParen { DepString $3 } - | stringType Expression { DepString $2 } - | int openParen Expression closeParen { DependentInt $3 } - | bool openParen Expression closeParen { DependentBool $3 } + | stringType openParen PreExpression closeParen { DepString $3 } + | stringType PreExpression { DepString $2 } + | int openParen PreExpression closeParen { DependentInt $3 } + | bool openParen PreExpression closeParen { DependentBool $3 } | identifier { Named $1 } | int Expression { DependentInt $2 } | exclamation Type { Unconsumed $2 } @@ -193,7 +196,6 @@ | openParen Type vbar Type closeParen { ProofType $1 $2 $4 } | Name identifier { Dependent $1 [Named $2] } | openParen TypeIn closeParen { Tuple $1 $2 } - | absprop identifier openParen FullArgs closeParen { AbsProp $1 $2 [] } | openParen Type closeParen { $2 } FullArgs : Args { $1 } @@ -245,18 +247,18 @@ ExpressionIn : Expression { [$1] } | ExpressionIn comma Expression { $3 : $1 } -TupleExpression : PreExpression comma PreExpression { [$3, $1] } - | TupleExpression comma PreExpression { $3 : $1 } +Tuple : PreExpression comma PreExpression { [$3, $1] } + | Tuple comma PreExpression { $3 : $1 } LambdaArrow : plainArrow { Plain $1 } | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently. | cloptr1Arrow { Full $1 "cloptr1" } + | lincloptr1Arrow { Full $1 "lincloptr1" } | spear { Full $1 ">" } Expression : PreExpression { $1 } | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } | Name PreExpression { Call $1 [] [] Nothing [$2] } - | openParen TupleExpression closeParen { TupleEx $1 $2 } -- FIXME should these be types?? TypeArgs : lbrace Expression rbrace { [$2] } @@ -284,7 +286,7 @@ | let ATS in end { Let $1 $2 Nothing } | lambda Pattern LambdaArrow PreExpression { Lambda $1 $3 $2 $4 } | llambda Pattern LambdaArrow PreExpression { LinearLambda $1 $3 $2 $4 } - | begin PreExpression end { $2 } + | begin PreExpression end { Begin $1 $2 } | at lbrace RecordVal rbrace { RecordValue $1 $3 Nothing } | at lbrace RecordVal rbrace signature Type { RecordValue $1 $3 (Just $6) } | PreExpression semicolon PreExpression { Precede $1 $3 } @@ -295,6 +297,7 @@ | ref Type rbracket PreExpression { Ref $1 $2 $4 } | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 } | PreExpression signature Type { TypeSignature $1 $3 } + | openParen Tuple closeParen { TupleEx $1 $2 } | Name { NamedVal $1 } | lbrace ATS rbrace { Actions $2 } | underscore { UnderscoreLit $1 } @@ -334,6 +337,7 @@ | dollar identifier dot identifier { Qualified $1 $4 $2 } | dollar effmaskWrt { SpecialName $1 "effmask_wrt" } | dollar effmaskAll { SpecialName $1 "effmask_all" } -- FIXME there is probably a better/more efficient way of doing this + | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this RecordVal : identifier eq Expression { [($1, $3)] } | RecordVal comma identifier eq Expression { ($3, $5) : $1 } @@ -410,24 +414,29 @@ | overload BinOp with Name { OverloadOp $1 $2 $4 } | stadef identifier eq Name { Stadef $2 $4 } | sortdef identifier eq Type { SortDef $1 $2 $4 } - | typedef identifier eq at lbrace Records rbrace { RecordType $2 $6 } + | typedef identifier eq at lbrace Records rbrace { RecordType $2 [] $6 } + | vtypedef identifier eq at lbrace Records rbrace { RecordViewType $2 [] $6 } | typedef identifier eq Type { TypeDef $1 $2 [] $4 } - | vtypedef identifier eq Type { ViewTypeDef $1 $2 [] $4 } + | typedef identifier openParen FullArgs closeParen eq at lbrace Records rbrace { RecordType $2 $4 $9 } + | vtypedef identifier openParen FullArgs closeParen eq at lbrace Records rbrace { RecordViewType $2 $4 $9 } + | typedef identifier openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 } | vtypedef identifier openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 } - | datavtype identifier eq Leaves { SumViewType $2 $4 } + | vtypedef identifier eq Type { ViewTypeDef $1 $2 [] $4 } + | datavtype identifier eq Leaves { SumViewType $2 [] $4 } + | datavtype identifier openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 } | absvtype identifier openParen FullArgs closeParen eq Type { AbsViewType $1 $2 $4 $7 } | abstype identifier openParen FullArgs closeParen eq Type { AbsType $1 $2 $4 $7 } - | datatype identifier eq Leaves { SumType $2 $4 } + | datatype identifier eq Leaves { SumType $2 [] $4 } + | datatype identifier openParen Args closeParen eq Leaves { SumType $2 $4 $7 } | dataprop identifier openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 } + | assume Name openParen Args closeParen eq Expression { Assume $2 $4 $7 } | lineComment { Comment $1 } + | absprop identifier openParen FullArgs closeParen { AbsProp $1 $2 [] } | define { Define $1 } | cblock { CBlock $1 } | lambda {% Left $ Expected $1 "Declaration" "lam" } | llambda {% Left $ Expected $1 "Declaration" "llam" } | ref {% Left $ Expected $1 "Declaration" "ref" } - --- existentials --- { 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 @@ -1,5 +1,6 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} @@ -16,7 +17,9 @@ import Control.Arrow hiding ((<+>)) import Control.Composition import Control.DeepSeq (NFData) +#if __GLASGOW_HASKELL__ >= 801 import Data.Function (on) +#endif import Data.Functor.Foldable (cata) import GHC.Generics (Generic) import Language.ATS.Types @@ -103,6 +106,11 @@ pretty Minus = "-" pretty None = "" +startsParens :: Doc -> Bool +startsParens d = f (show d) where + f ('(':_) = True + f _ = False + instance Pretty Expression where pretty = cata a where a (IfF e e' (Just e'')) = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e'' @@ -118,24 +126,32 @@ a (LinearLambdaF _ lt p e) = "llam" <+> pretty p <+> pretty lt <+> e a (FloatLitF f) = pretty f a (StringLitF s) = string s + a (BinListF op es) + | splits op = encloseSep (head es) (" " <> pretty op <> " ") (last es) (init $ tail es) + | otherwise = "error state" a (BinaryF op e e') - | splits op = e pretty op <+> e' -- TODO if one operator splits, the rest should. + | splits op = e pretty op <+> e' | otherwise = e <+> pretty op <+> e' a (IndexF _ n e) = pretty n <> "[" <> e <> "]" a (UnaryF Negate e) = "~" <> e a (NamedValF name) = pretty name a (CallF name [] [] Nothing []) = pretty name <> "()" + a (CallF name [] [] Nothing [x]) + | startsParens x = pretty name <> pretty x a (CallF name [] [] Nothing xs) = pretty name <> prettyArgsG "(" ")" xs a (CallF name [] ys Nothing []) = pretty name <> prettyArgsG "<" ">" (fmap pretty ys)-- FIXME this should use { too? a (CallF name us [] Nothing []) = pretty name <> prettyArgsG "{" "}" us a (CallF name [] ys Nothing xs) = pretty name <> prettyArgsG "<" ">" (fmap pretty ys) <> prettyArgsG "(" ")" xs + a (CallF name us [] Nothing [x]) + | startsParens x = pretty name <> prettyArgsG "{" "}" us <> pretty x a (CallF name us [] Nothing xs) = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "(" ")" xs - a (CallF name us ys Nothing xs) = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "<" ">" (fmap pretty ys) <> prettyArgsG "(" ")" xs + a (CallF name us ys Nothing [x]) + | startsParens x = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "<" ">" (fmap pretty ys) <> pretty x + a (CallF name us ys Nothing xs) = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "<" ">" (fmap pretty ys) <+> prettyArgsG "(" ")" xs a (CaseF _ add e cs) = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs) a (VoidLiteralF _) = "()" a (RecordValueF _ es Nothing) = prettyRecord es a (RecordValueF _ es (Just x)) = prettyRecord es <+> ":" <+> pretty x - a (BeginF e) = "begin" <$> indent 2 (pretty e) <$> "end" a (PrecedeF e e') = parens (e <+> ";" e') a (FieldMutateF _ o f v) = pretty o <> "->" <> string f <+> ":=" <+> v a (MutateF e e') = e <+> ":=" <+> e' @@ -143,16 +159,22 @@ a (AccessF _ e n) | noParens e = e <> "." <> pretty n | otherwise = parens e <> "." <> pretty n + a (CharLitF '\\') = "'\\\\'" + a (CharLitF '\n') = "'\\n'" + a (CharLitF '\t') = "'\\t'" a (CharLitF c) = "'" <> char c <> "'" a (RefF _ t e) = "ref<" <> pretty t <> ">" <> parens e a (ProofExprF _ e e') = "(" <> e <+> "|" <+> e' <> ")" a (TypeSignatureF e t) = e <+> ":" <+> pretty t a (WhereExpF e d) = e <+> "where" <$> braces (" " <> pretty (ATS d) <> " ") - a (TupleExF _ es) = parens (mconcat $ punctuate ", " (reverse es)) + a (TupleExF _ es) = prettyArgs es -- parens (mconcat $ punctuate ", " (reverse es)) a (WhileF _ e e') = "while" <> parens e <> e' a (ActionsF as) = "{" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) as)) <$> "}" a UnderscoreLitF{} = "_" a (AtExprF e e') = e <> "@" <> parens e' + a (BeginF _ e) + | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end") + | otherwise = e a _ = "FIXME" prettyCases [] = mempty prettyCases [(s, t)] = "|" <+> pretty s <+> "=>" <+> t @@ -210,7 +232,6 @@ a (ConcreteTypeF e) = pretty e a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) a (RefTypeF t) = "&" <> t - a (AbsPropF _ n as) = "absprop" <+> string n <+> prettyArgs as a (ViewTypeF _ t) = "view@" <> parens t a (FunctionTypeF s t t') = t <+> string s <+> t' @@ -247,26 +268,23 @@ glue :: Declaration -> Declaration -> Bool glue Staload{} Staload{} = True glue Include{} Include{} = True +glue ViewTypeDef{} ViewTypeDef{} = True +glue Val{} Val{} = True +glue Val{} Var{} = True +glue Var{} Val{} = True +glue Var{} Var{} = True +glue Comment{} _ = True glue (Func _ Fnx{}) (Func _ And{}) = True glue _ _ = False -repulse :: Declaration -> Declaration -> Bool -repulse Impl{} Impl{} = True -repulse Extern{} Impl{} = True -repulse Include{} Extern{} = False -repulse _ Extern{} = True -repulse Extern{} _ = True -repulse _ _ = False - {-# INLINE glue #-} concatSame :: [Declaration] -> Doc concatSame [] = mempty concatSame [x] = pretty x concatSame (x:x':xs) - | glue x x' = pretty x <> concatSame (x':xs) - | repulse x x' = pretty x <> line <$> concatSame (x':xs) - | otherwise = pretty x <$> concatSame (x':xs) + | glue x x' = pretty x <$> concatSame (x':xs) + | otherwise = pretty x <> line <$> concatSame (x':xs) -- TODO - soft break ($$) :: Doc -> Doc -> Doc @@ -309,7 +327,7 @@ go x = x prettyArgs' :: (Pretty a) => Doc -> Doc -> [a] -> Doc -prettyArgs' = fmap pretty -.** prettyArgsG -- -.** fmap pretty +prettyArgs' = fmap pretty -.** prettyArgsG prettyArgs :: (Pretty a) => [a] -> Doc prettyArgs = prettyArgs' "(" ")" @@ -318,24 +336,29 @@ fancyU = foldMap pretty . reverse instance Pretty PreFunction where - pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i fancyU us prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus pretty i <> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus pretty i <+> ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line - pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> string si <+> pretty rt + pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i fancyU us prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus pretty i <> prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus pretty i <+> ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus pretty i fancyU us ".<" <> pretty t <> ">." prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> string si pretty rt <+> "=" <$> indent 2 (pretty e) + pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus pretty i fancyU us prettyArgs as <+> ":" <> string si pretty rt pretty _ = "FIXME" instance Pretty DataPropLeaf where pretty (DataPropLeaf us e) = "|" <+> foldMap pretty (reverse us) <+> pretty e instance Pretty Declaration where - pretty (RecordType s rs) = "typedef" <+> string s <+> "=" <+> prettyRecord rs <> line - pretty (SumViewType s ls) = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls <> linebreak - pretty (SumType s ls) = "datatype" <+> string s <+> "=" <$> prettyLeaf ls + pretty (RecordType s [] rs) = "typedef" <+> string s <+> "=" <+> prettyRecord rs + pretty (RecordType s as rs) = "typedef" <+> string s <> prettyArgs as <+> "=" <+> prettyRecord rs + pretty (RecordViewType s [] rs) = "vtypedef" <+> string s <+> "=" <+> prettyRecord rs + pretty (RecordViewType s as rs) = "vtypedef" <+> string s <> prettyArgs as <+> "=" <+> prettyRecord rs + pretty (SumViewType s [] ls) = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls + pretty (SumViewType s as ls) = "datavtype" <+> string s <> prettyArgs as <+> "=" <$> prettyLeaf ls + pretty (SumType s [] ls) = "datatype" <+> string s <+> "=" <$> prettyLeaf ls + pretty (SumType s as ls) = "datatype" <+> string s <> prettyArgs as <+> "=" <$> prettyLeaf ls pretty (Impl [] i) = pretty i pretty Impl{} = "FIXME" pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e @@ -343,12 +366,12 @@ pretty (Val a (Just t) p e) = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e pretty (Var Nothing p e) = "var" <+> pretty p <+> "=" <+> pretty e pretty (Var (Just t) p e) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e - pretty (Include s) = "#include" <+> pretty s <> line - pretty (Staload Nothing s) = "staload" <+> pretty s <> line - pretty (Staload (Just q) s) = "staload" <+> pretty q <+> "=" <+> pretty s <> line - pretty (CBlock s) = string s <> line + pretty (Include s) = "#include" <+> pretty s + pretty (Staload Nothing s) = "staload" <+> pretty s + pretty (Staload (Just q) s) = "staload" <+> pretty q <+> "=" <+> pretty s + pretty (CBlock s) = string s pretty (Comment s) = string s - pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n <> linebreak + pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n pretty (Func _ (Fun pref)) = "fun" pretty pref pretty (Func _ (Fnx pref)) = "fnx" pretty pref pretty (Func _ (And pref)) = "and" pretty pref @@ -356,5 +379,10 @@ pretty (Extern _ d) = "extern" <$> pretty d pretty (Define s) = string s pretty (DataProp _ s as ls) = "dataprop" <+> string s <> prettyArgs as <+> "=" <$> prettyDL ls - pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> string s <+> "=" <+> pretty t <> linebreak + pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> string s <+> "=" <+> pretty t + pretty (ViewTypeDef _ s as t) = "vtypedef" <+> string s <> prettyArgs as <+> "=" <+> pretty t + pretty (TypeDef _ s [] t) = "typedef" <+> string s <+> "=" <+> pretty t + pretty (TypeDef _ s as t) = "typedef" <+> string s <> prettyArgs as <+> "=" <+> pretty t + pretty (AbsProp _ n as) = "absprop" <+> string n <+> prettyArgs as + pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e pretty _ = mempty 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 @@ -3,6 +3,7 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} @@ -30,9 +31,12 @@ , Addendum (..) , DataPropLeaf (..) , PreFunction (..) + -- remove + , binList ) where import Control.DeepSeq (NFData) +import Control.Lens.Plated import Data.Functor.Foldable.TH (makeBaseFunctor) import GHC.Generics (Generic) import Language.ATS.Lexer (Addendum (..), AlexPosn) @@ -53,12 +57,12 @@ | Staload (Maybe String) String | Stadef String Name | CBlock String - | RecordType String [(String, Type)] - | RecordViewType String [(String, Type)] + | RecordType String [Arg] [(String, Type)] + | RecordViewType String [Arg] [(String, Type)] | TypeDef AlexPosn String [Arg] Type | ViewTypeDef AlexPosn String [Arg] Type - | SumType String [(String, Maybe Type)] - | SumViewType String [(String, Maybe Type)] + | SumType String [Arg] [(String, Maybe Type)] -- TODO [Arg] for here + | SumViewType String [Arg] [(String, Maybe Type)] | AbsType AlexPosn String [Arg] Type | AbsViewType AlexPosn String [Arg] Type | OverloadOp AlexPosn BinOp Name @@ -69,6 +73,8 @@ | SortDef AlexPosn String Type | AndD Declaration Declaration | Local AlexPosn [Declaration] [Declaration] + | AbsProp AlexPosn String [Arg] + | Assume Name [Arg] Expression deriving (Show, Eq, Generic, NFData) data DataPropLeaf = DataPropLeaf [Universal] Expression @@ -101,7 +107,6 @@ | ProofType AlexPosn Type Type -- Aka (prf | val) | ConcreteType Expression | RefType Type - | AbsProp AlexPosn String [Arg] | ViewType AlexPosn Type | FunctionType String Type Type deriving (Show, Eq, Generic, NFData) @@ -164,7 +169,6 @@ -- | A (possibly effectful) expression. data Expression = Let AlexPosn ATS (Maybe Expression) - | Begin ATS | VoidLiteral -- The '()' literal representing inaction. AlexPosn -- The first list is implicit arguments such as ``, the second is implicits such as `{list_vt(string)}`, the third is an optional proof, and the last is the actual arguments @@ -188,6 +192,7 @@ | CharLit Char | AtExpr Expression Expression | Binary BinOp Expression Expression + | BinList { _op :: BinOp, _exprs :: [Expression] } | Unary UnOp Expression | Case { posE :: AlexPosn , kind :: Addendum @@ -212,7 +217,18 @@ | Actions ATS | TKind AlexPosn Name String | ViewExpr AlexPosn Type -- TODO separate type for proof values? + | Begin AlexPosn Expression deriving (Show, Eq, Generic, NFData) + +instance Plated Expression where + plate f (Binary Add e e') = Binary Add <$> f e <*> f e' + plate _ x = pure x + +binList :: Expression -> Expression +binList = transform $ \case + (Binary Add e e'@Binary{}) -> BinList Add [e, e'] -- FIXME both have to be 'Add' + (Binary Add e@BinList{} e') -> BinList Add (e' : _exprs e) + a -> a -- | An 'implement' declaration data Implementation = Implement { pos :: AlexPosn diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -6,6 +6,7 @@ - ansi-wl-pprint-0.6.8.1 - htoml-megaparsec-1.0.1.11 - composition-prelude-0.1.1.1 + - dirstream-1.0.3 flags: ats-format: development: false diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,28 +1,41 @@ -{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +import Data.DirStream +import qualified Filesystem.Path.CurrentOS as F import Language.ATS +import Pipes +import qualified Pipes.Prelude as P +import Pipes.Safe +import System.FilePath import Test.Hspec +import Test.Hspec.Core.Spec +deriving instance MonadCatch (SpecM a) +deriving instance MonadThrow (SpecM a) +deriving instance MonadMask (SpecM a) +deriving instance MonadIO (SpecM a) + +isATS :: F.FilePath -> Bool +isATS x = (F.extension x `elem`) (pure <$> ["ats", "dats", "sats", "hats", "cats"]) + +testFile :: String -> SpecWith () +testFile f = it f $ do + sample <- readFile f + expected <- readFile (replaceExtension f ".out") + (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected + main :: IO () main = hspec $ - describe "pretty" $ do - parallel $ it "works on fib.dats" $ do - sample <- readFile "test/data/fib.dats" - expected <- readFile "test/data/fib.out" - (fmap printATS . parseATS . lexATS) sample `shouldBe` Right expected - parallel $ it "works on filecount.dats" $ do - sample <- readFile "test/data/filecount.dats" - expected <- readFile "test/data/filecount.out" - (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected - parallel $ it "works on filetype.sats" $ do - sample <- readFile "test/data/filetype.sats" - expected <- readFile "test/data/filetype.out" - (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected - parallel $ it "works on polyglot.dats" $ do - sample <- readFile "test/data/polyglot.dats" - expected <- readFile "test/data/polyglot.out" - (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected - parallel $ it "works on left-pad.dats" $ do - sample <- readFile "test/data/left-pad.dats" - expected <- readFile "test/data/left-pad.out" - (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected + describe "pretty-print" $ parallel $ + runSafeT $ runEffect $ atsPath >-> mapS testFile + +mapS :: (a -> SpecM () ()) -> Proxy () a y' y (SafeT (SpecM ())) r +mapS = P.mapM_ . (lift .) + +atsPath :: MonadSafe m => Producer String m () +atsPath = every (childOf p) >-> P.filter isATS >-> P.map F.encodeString + where p = F.decodeString "test/data"