diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -65,12 +65,6 @@ - stack build --test --bench --no-run-tests --no-run-benchmarks - | if [ `uname` = "Darwin" ] - find .stack-work -name atsfmt -perm 755 - else - echo 'nothing' - fi - - | - if [ `uname` = "Darwin" ] then export BINPATH="$(find .stack-work -name atsfmt -perm 755 | tail -n1)" else diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -1,3 +1,9 @@ +approve FILE: + @atsfmt test/data/{{ FILE }} -o > test/data/$(echo {{ FILE }} | sed 's/\(dats\|sats\)/out/') + +diff FILE: + @diff <(atsfmt test/data/{{ FILE }} -o) test/data/$(echo {{ FILE }} | sed 's/\(dats\|sats\)/out/') | ac -s + darcs: @darcs optimize clean @darcs optimize pristine @@ -11,7 +17,7 @@ @poly . -e data/ bench: - bench "atsfmt test/data/polyglot.dats" "atsfmt test/data/left-pad.dats" + bench "atsfmt test/data/polyglot.dats" "atsfmt test/data/left-pad.dats" "atsfmt ~/programming/ats/toml-parse/src/toml-parse.dats" manpages: pandoc man/MANPAGE.md -s -t man -o man/atsfmt.1 @@ -28,6 +34,7 @@ ci: test cabal new-build + cabal new-haddock cabal new-test hlint src app bench test tomlcheck --file .atsfmt.toml diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,15 +2,15 @@ [![Build Status](https://travis-ci.org/vmchale/ats-format.svg?branch=master)](https://travis-ci.org/vmchale/ats-format) +Screenshot of sample results +Screenshot of sample results + This is a code formatter for [ATS](http://www.ats-lang.org/). It is a work-in-progress, but it can handle a subset of the language already. 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. 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. +an issue. Code samples that were formatted into something ugly are also welcome. ## Configuration 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.4 +version: 0.1.0.5 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 @@ -50,7 +50,7 @@ , recursion-schemes , optparse-applicative , ansi-terminal - , composition-prelude >= 0.1.1.1 + , composition-prelude >= 0.1.1.2 , htoml-megaparsec , megaparsec , unordered-containers diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -3,11 +3,30 @@ lexATS , parseATS , printATS - -- * Types + -- * Syntax Tree , ATS (..) , Declaration (..) , Expression (..) , Type (..) + , Function (..) + , Implementation (..) + , Pattern (..) + , Name (..) + , UnOp (..) + , BinOp (..) + , DataPropLeaf (..) + , Arg (..) + , Addendum (..) + , LambdaType (..) + , Universal (..) + , Existential (..) + , PreFunction (..) + -- * Lexical types + , Token (..) + , AlexPosn (..) + , Keyword (..) + -- * Error types + , ATSError -- * Executable , exec ) where 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 @@ -3,7 +3,9 @@ {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} + {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} + {-# LANGUAGE OverloadedStrings #-} -- | Module exporting the lexer itself as well as several data types for -- working with tokens. @@ -15,10 +17,12 @@ , token_posn ) where -import Data.Char (toUpper) +import Data.Data (Typeable, Data) +import Data.Char (toUpper, toLower) import Control.Lens (over, _head) import Control.DeepSeq (NFData) import GHC.Generics (Generic) +import Text.PrettyPrint.ANSI.Leijen hiding (line, column, (<$>)) } @@ -35,14 +39,16 @@ @escape_ch = \\ [nt\'\\] @escape_str = \\ [nt\"\\] @char = ($terminal # [\\\']) | " " | @escape_ch | $esc_char -@bool = (true | false) - @char_lit = \' @char \' -@time_lit = $digit+ u +$br = [\<\>] +-- Boolean literals +@bool = (true | false) + -- Integer @integer = $digit+ +@time_lit = $digit+ u -- Floats @decimals = $digit+ @@ -61,26 +67,24 @@ @slash_comment = \/\* ([^\/\*] | @not_close_slash | \n)* \*\/ @block_comment = @paren_comment | @slash_comment -@ref = "ref<" - @if_block = "#if" ([^\#] | "#then" | "#print" | \n)+ "#endif" .* -- FIXME this is a disaster lol -@ref_call = @identifier "<" ($alpha | $digit | "(" | ")" | _)+ ">" +@ref_call = ($alpha | $digit | "(" | ")" | _ | ($white* "," $white*))+ ">" @not_close_c = \% [^\}] -@c_block = \%\{ ([^\%] | @not_close_c | \n)* \%\} -- TODO include %{# and %{$ +@c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\} -- TODO include %{# and %{$ @lambda = "=>" | "=" | "=" | "=>>" | "=" -- FIXME whatever the fuck this is: - -@func_type = "-" | "-" | "-" | "-" | "-" | "-<>" | "-" -- FIXME allow spaces after comma? +@func_type = "-" | "-" | "-" | "-" | "-" | "-" | "-<>" | "-" -- FIXME allow spaces after comma? -@operator = "+" | "-" | "*" | "/" | "!=" | ">=" | "<=" | "=" | "~" | "&&" | "||" | ">" | "<" | "->" | ":=" | ".<" | ">." | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow | +@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "&&" | "||" | "->" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow | -@double_parens = "(" (@block_comment | "") ")" -@double_braces = "{" (@block_comment | "") "}" -@double_brackets = "<" (@block_comment | "") ">" +@double_parens = "(" @block_comment ")" | "()" +@double_braces = "{" @block_comment "}" | "{}" +@double_brackets = "<" @block_comment ">" | "<>" @view = v | view @@ -173,8 +177,7 @@ @time_lit { tok (\p s -> TimeTok p s) } @integer { tok (\p s -> IntTok p (read s)) } @float { tok (\p s -> FloatTok p (read s)) } - @ref { tok (\p s -> RefTok p) } - @ref_call { tok (\p s -> Identifier p s) } + $br / @ref_call { tok (\p s -> SpecialBracket p) } @operator { tok (\p s -> Operator p s) } @signature { tok (\p s -> SignatureTok p (tail s)) } $special { tok (\p s -> Special p s) } @@ -185,20 +188,22 @@ deriving instance Generic AlexPosn deriving instance NFData AlexPosn +deriving instance Data AlexPosn +deriving instance Typeable AlexPosn tok f p s = f p s +-- | Determines the default behavior for incomplete pattern matches data Addendum = None | Plus | Minus - deriving (Eq, Show, Generic, NFData) + deriving (Eq, Show, Generic, NFData, Data, Typeable) data Keyword = KwFun | KwFnx | KwAnd | KwDatatype | KwDatavtype - | KwDataviewtype | KwAssume | KwTypedef | KwVtypedef @@ -268,15 +273,103 @@ | Arrow AlexPosn String | FuncType AlexPosn String | CommentLex AlexPosn String - | RefTok AlexPosn | MacroBlock AlexPosn String | TimeTok AlexPosn String | SignatureTok AlexPosn String | DoubleParenTok AlexPosn | DoubleBracesTok AlexPosn | DoubleBracketTok AlexPosn + | SpecialBracket AlexPosn deriving (Eq, Show, Generic, NFData) +instance Pretty Addendum where + pretty Plus = "+" + pretty Minus = "-" + pretty None = "" + +instance Pretty Keyword where + pretty KwFun = "fun" + pretty KwAnd = "and" + pretty KwDatatype = "datatype" + pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype + pretty KwFnx = "fnx" + pretty KwAssume = "assume" + pretty KwTypedef = "typedef" + pretty KwVtypedef = "vtypedef" + pretty KwStaload = "stload" + pretty KwLet = "let" + pretty KwWhere = "where" + pretty KwLocal = "local" + pretty KwEnd = "end" + pretty KwBegin = "begin" + pretty KwIn = "in" + pretty KwImplement = "implement" + pretty (KwCase c) = "case" <> pretty c + pretty KwIf = "if" + pretty KwSif = "sif" + pretty KwThen = "then" + pretty KwElse = "else" + pretty KwString = "string" + pretty KwBool = "bool" + pretty KwInt = "int" + pretty KwVoid = "void" + pretty KwNat = "nat" + pretty (KwVal c) = "val" <> pretty c + pretty KwVar = "var" + pretty KwLambda = "lam" + pretty KwLinearLambda = "llam" + pretty KwInclude = "include" + pretty KwWhen = "when" + pretty KwOf = "of" + pretty KwAbsprop = "absprop" + pretty KwPrval = "prval" + pretty KwStadef = "stadef" + pretty KwPraxi = "praxi" + pretty KwWhile = "while" + pretty KwOverload = "overload" + pretty KwWith = "with" + pretty KwChar = "char" + pretty KwDataview = "dataview" + pretty KwDataprop = "dataprop" + pretty KwView = "view" + pretty KwAbstype = "abstype" + pretty KwAbsvtype = "absvtype" + pretty KwType = "type" + pretty (KwAbst0p c) = "abst@ype" <> pretty c + pretty (KwT0p c) = "t@ype" <> pretty c + pretty (KwVt0p c) = "vt@ype" <> pretty c + pretty KwPrfun = "prfun" + pretty KwPrfn = "prfn" + pretty KwCastfn = "castfn" + pretty KwExtern = "extern" + pretty KwRaise = "$raise" + pretty KwProofImplement = "primplmnt" + pretty KwSortdef = "sortdef" + pretty KwPropdef = "propdef" + pretty KwTKind = "tkind" + +instance Pretty Token where + pretty (Identifier _ s) = string s + pretty (Keyword _ kw) = pretty kw + pretty (BoolTok _ b) = string $ over _head toLower (show b) + pretty (IntTok _ i) = pretty i + pretty (FloatTok _ x) = pretty x + pretty (CharTok _ c) = squotes (pretty c) + pretty (StringTok _ s) = dquotes (string s) + pretty (Special _ s) = string s + pretty CBlockLex{} = "%{" + pretty (Arrow _ s) = string s + pretty (CommentLex _ s) = string $ take 2 s + pretty (FuncType _ s) = string s + pretty (TimeTok _ s) = string s + pretty (SignatureTok _ s) = string s + pretty (Operator _ s) = string s + pretty (MacroBlock _ s) = "#" + pretty DoubleParenTok{} = "()" + pretty DoubleBracesTok{} = "{}" + pretty DoubleBracketTok{} = "<>" + pretty SpecialBracket{} = "{" + token_posn (Identifier p _) = p token_posn (Keyword p _) = p token_posn (BoolTok p _) = p @@ -290,13 +383,13 @@ token_posn (FuncType p _) = p token_posn (CharTok p _) = p token_posn (CommentLex p _) = p -token_posn (RefTok p) = p token_posn (MacroBlock p _) = p token_posn (TimeTok p _) = p token_posn (SignatureTok p _) = p token_posn (DoubleParenTok p) = p token_posn (DoubleBracesTok p) = p token_posn (DoubleBracketTok p) = p +token_posn (SpecialBracket p) = p toChar :: String -> Char toChar "'\\n'" = '\n' 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,6 +32,7 @@ %token fun { Keyword $$ KwFun } + prfun { Keyword $$ KwPrfun } fnx { Keyword $$ KwFnx } and { Keyword $$ KwAnd } lambda { Keyword $$ KwLambda } @@ -93,6 +94,7 @@ effmaskAll { Identifier $$ "effmask_all" } extfcall { Identifier $$ "extfcall" } ldelay { Identifier $$ "ldelay" } + listVT { Identifier $$ "list_vt" } -- TODO token? raise { Identifier $$ "raise" } identifier { Identifier _ $$ } closeParen { Special $$ ")" } @@ -135,6 +137,8 @@ dollar { Special $$ "$" } semicolon { Special $$ ";" } andOp { Operator $$ "&&" } + doubleEq { Operator $$ "==" } + doubleDot { Operator $$ ".." } doubleParens { DoubleParenTok $$ } doubleBraces { DoubleBracesTok $$ } prfTransform { Operator $$ ">>" } -- For types like &a >> a?! @@ -143,28 +147,30 @@ fromVT { Operator $$ "?!" } -- For types like a?! openExistential { Operator $$ "#[" } -- Same as `[` in ATS2 cblock { CBlockLex _ $$ } - ref { RefTok $$ } define { MacroBlock _ $$ } lineComment { CommentLex _ $$ } + lspecial { SpecialBracket $$ } %% ATS : Declarations { ATS $1 } +-- | Parse declarations in a list Declarations : { [] } | Declarations Declaration { $2 : $1 } | Declarations FunDecl { $2 ++ $1 } | Declarations local Declarations in Declarations end { Local $2 $3 $5 : $1 } - | fromVT {% Left $ Expected $1 "Declaration" "?!" } - | prfTransform {% Left $ Expected $1 "Declaration" ">>" } +-- | Several comma-separated types TypeIn : Type { [$1] } | TypeIn comma Type { $3 : $1 } +-- | Several comma-separated types or static expressions TypeInExpr : TypeIn { $1 } | Expression { [ConcreteType $1] } - | TypeInExpr comma PreExpression { ConcreteType $3 : $1 } + | TypeInExpr comma Expression { ConcreteType $3 : $1 } +-- | Parse a type Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 } | bool { Bool } | int { Int } @@ -197,120 +203,148 @@ | Name identifier { Dependent $1 [Named $2] } | openParen TypeIn closeParen { Tuple $1 $2 } | openParen Type closeParen { $2 } + | doubleParens { NoneType $1 } + | minus {% Left $ Expected $1 "Type" "-" } + | dollar {% Left $ Expected $1 "Type" "$" } FullArgs : Args { $1 } - | Arg vbar Args { [ PrfArg $1 $3 ] } - | Arg vbar { [ PrfArg $1 [] ] } --- TODO {i:nat;j:int} - +-- | A comma-separated list of arguments Args : Arg { [$1] } | Args comma Arg { $3 : $1 } + | Arg vbar Arg { [ PrfArg $1 $3 ] } + | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 } -Arg : identifier { Arg $1 Nothing } - | identifier signature Type { Arg $1 (Just $3) } - | underscore { Arg "_" Nothing } - | Type { Arg "" (Just $1) } -- FIXME take a maybe here +Arg : identifier { Arg (First $1) } + | identifier signature Type { Arg (Both $1 $3) } + | underscore { Arg (First "_") } + | Type { Arg (Second $1) } + | Expression { Arg (Second (ConcreteType $1)) } +-- | Parse a literal Literal : boolLit { BoolLit $1 } | timeLit { TimeLit $1 } | intLit { IntLit $1 } | floatLit { FloatLit $1 } | string { StringLit $1 } | charLit { CharLit $1 } + | doubleParens { VoidLiteral $1 } +-- | Parse a list of comma-separated patterns PatternIn : Pattern { [$1] } | PatternIn comma Pattern { $3 : $1 } -Pattern : doubleParens { NullPattern $1 } - | identifier { PName $1 [] } +-- | Parse a pattern match +Pattern : identifier { PName $1 [] } | underscore { Wildcard $1 } | identifier doubleParens { PName ($1 ++ "()") [] } | tilde Pattern { Free $2 } | identifier openParen PatternIn closeParen { PName $1 $3 } | identifier Pattern { PSum $1 $2 } - | openParen Pattern vbar Pattern closeParen { Proof $1 $2 $4 } + | openParen PatternIn vbar PatternIn closeParen { Proof $1 $2 $4 } | openParen PatternIn closeParen { TuplePattern $2 } | Literal { PLiteral $1 } | Pattern when Expression { Guarded $2 $3 $1 } + | minus {% Left $ Expected $1 "Pattern" "-" } + | plus {% Left $ Expected $1 "Pattern" "+" } -Case : vbar Pattern LambdaArrow Expression { [($2, $4)] } - | Pattern LambdaArrow Expression { [($1, $3)] } - | Case vbar Pattern LambdaArrow Expression { ($3, $5) : $1 } +-- | Parse a case expression +Case : vbar Pattern CaseArrow Expression { [($2, $4)] } + | Pattern CaseArrow Expression { [($1, $3)] } + | Case vbar Pattern CaseArrow Expression { ($3, $5) : $1 } ExpressionPrf : ExpressionIn { (Nothing, $1) } - | Expression vbar ExpressionIn { (Just $1, $3) } - | PrfExpr vbar ExpressionIn { (Just $1, $3) } - -PrfExpr : view at Type { ViewExpr $1 $3 } + | Expression vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof? +-- | A list of comma-separated expressions ExpressionIn : Expression { [$1] } | ExpressionIn comma Expression { $3 : $1 } Tuple : PreExpression comma PreExpression { [$3, $1] } | Tuple comma PreExpression { $3 : $1 } +-- | Parse an arrow in a case statement +CaseArrow : plainArrow { Plain $1 } + | spear { Spear $1 } + | minus {% Left $ Expected $1 "Arrow" "-" } + | eq {% Left $ Expected $1 "Arrow" "=" } + LambdaArrow : plainArrow { Plain $1 } | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently. | cloptr1Arrow { Full $1 "cloptr1" } | lincloptr1Arrow { Full $1 "lincloptr1" } - | spear { Full $1 ">" } + | minus {% Left $ Expected $1 "Arrow" "-" } + | openParen {% Left $ Expected $1 "Arrow" "(" } + | closeParen {% Left $ Expected $1 "Arrow" ")" } +-- | Expression or named call to an expression Expression : PreExpression { $1 } - | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } + | openParen Tuple closeParen { TupleEx $1 $2 } | Name PreExpression { Call $1 [] [] Nothing [$2] } + | begin Expression end { Begin $1 $2 } + | Expression semicolon Expression { Precede $1 $3 } + | Expression semicolon { $1 } + | openParen Expression closeParen { $2 } + | Expression signature Type { TypeSignature $1 $3 } --- FIXME should these be types?? -TypeArgs : lbrace Expression rbrace { [$2] } - | lbrace ExpressionIn rbrace { $2 } -- TODO how much of this should be preserved? - | TypeArgs lbrace Expression rbrace { $3 : $1 } - | TypeArgs lbrace ExpressionIn rbrace { $3 ++ $1 } +TypeArgs : lbrace Type rbrace { [$2] } + | lbrace TypeIn rbrace { $2 } + | TypeArgs lbrace Type rbrace { $3 : $1 } + | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls + | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 } +BracketedArgs : lbracket Type rbracket { [$2] } + | lbracket TypeIn rbrace { $2 } + +Call : Name doubleParens { Call $1 [] [] Nothing [] } + | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) } + | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) } + | Name TypeArgs { Call $1 [] $2 Nothing [] } + | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) } + | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] } + | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- we do this because a $raise can have at most one argument + +-- | Parse an expression that can be called without parentheses PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $1) $3 } | Literal { $1 } - | doubleParens { VoidLiteral $1 } - | Name doubleParens { Call $1 [] [] Nothing [] } - | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) } - | Name TypeArgs { Call $1 $2 [] Nothing [] } - | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) } + | Call { $1 } | openParen PreExpression vbar PreExpression closeParen { ProofExpr $1 $2 $4 } | case PreExpression of Case { Case $3 $1 $2 $4 } | PreExpression BinOp PreExpression { Binary $2 $1 $3 } - | UnOp PreExpression { Unary $1 $2 } + | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time | PreExpression dot Name { Access $2 $1 $3 } - | openParen PreExpression closeParen { $2 } - | sif PreExpression then Expression else Expression { Sif $2 $4 $6 } - | if PreExpression then Expression { If $2 $4 Nothing} - | if PreExpression then Expression else Expression { If $2 $4 (Just $6) } - | let ATS in Expression end { Let $1 $2 (Just $4) } + | if Expression then Expression { If $2 $4 Nothing} + | if Expression then Expression else Expression { If $2 $4 (Just $6) } | let ATS in end { Let $1 $2 Nothing } - | lambda Pattern LambdaArrow PreExpression { Lambda $1 $3 $2 $4 } - | llambda Pattern LambdaArrow PreExpression { LinearLambda $1 $3 $2 $4 } - | begin PreExpression end { Begin $1 $2 } + | let ATS in Expression end { Let $1 $2 (Just $4) } + | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 } + | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 } | 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 } - | PreExpression semicolon { $1 } | exclamation PreExpression { Deref $1 $2 } | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 $3 $5 } | PreExpression mutateEq PreExpression { Mutate $1 $3 } - | 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 } | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 } + | sif PreExpression then Expression else Expression { Sif $2 $4 $6 } -- TODO separate type for static expressions | include {% Left $ Expected $1 "Expression" "include" } | staload {% Left $ Expected $1 "Expression" "staload" } | overload {% Left $ Expected $1 "Expression" "overload" } | prval {% Left $ Expected $1 "Expression" "prval" } | var {% Left $ Expected $1 "Expression" "var" } | Termetric {% Left $ Expected (fst $1) "Expression" "termetric" } + | fromVT {% Left $ Expected $1 "Expression" "?!" } + | prfTransform {% Left $ Expected $1 "Expression" ">>" } + | maybeProof {% Left $ Expected $1 "Expression" "?" } +-- | Parse a termetric Termetric : openTermetric Expression closeTermetric { ($1, $2) } + | underscore {% Left $ Expected $1 "_" "Name" } + | dollar {% Left $ Expected $1 "$" "Name" } +-- | Parse an existential quantier on a type Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) } | lsqbracket Args rsqbracket { Existential $2 Nothing Nothing } | openExistential Args rsqbracket { Existential $2 Nothing Nothing } @@ -318,48 +352,65 @@ | lsqbracket Args signature Type rsqbracket { Existential $2 (Just $4) Nothing } -- FIXME arguments should include more than just ':' | lsqbracket Expression rsqbracket { Existential [] Nothing (Just $2) } - +-- | Parse a universal quantifier on a type Universal : lbrace Args vbar PreExpression rbrace { Universal $2 Nothing (Just $4) } | lbrace Args rbrace { Universal $2 Nothing Nothing } | lbrace Args signature Type vbar Expression rbrace { Universal $2 (Just $4) (Just $6) } | lbrace Args signature Type { Universal $2 (Just $4) Nothing } +-- | Parse the details of an implementation Implementation : FunName doubleParens eq Expression { Implement $2 [] [] $1 [] $4 } | FunName openParen FullArgs closeParen eq Expression { Implement $2 [] [] $1 $3 $6 } | FunName Universals openParen FullArgs closeParen eq Expression { Implement $3 [] $2 $1 $4 $7 } | Universals FunName openParen FullArgs closeParen eq Expression { Implement $3 $1 [] $2 $4 $7 } | Universals FunName Universals openParen FullArgs closeParen eq Expression { Implement $4 $1 $3 $2 $5 $8 } +-- | Parse a function name FunName : identifier { Unqualified $1 } | identifier dollar identifier { Functorial $1 $3 } -Name : FunName { $1 } +-- | Parse a general name +Name : identifier { Unqualified $1 } + | listVT { Unqualified "list_vt" } | 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 effmaskAll { SpecialName $1 "effmask_all" } + | dollar listVT { SpecialName $1 "list_vt" } | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this + | underscore {% Left $ Expected $1 "_" "Name" } + | dollar {% Left $ Expected $1 "$" "Name" } +-- | Parse a list of values in a record RecordVal : identifier eq Expression { [($1, $3)] } | RecordVal comma identifier eq Expression { ($3, $5) : $1 } +-- | Parse a list of types in a record Records : identifier eq Type { [($1, $3)] } | Records comma identifier eq Type { ($3, $5) : $1 } +-- | Parse a constructor for a sum type SumLeaf : vbar identifier { ($2, Nothing) } | vbar identifier of Type { ($2, Just $4) } +-- | Parse all constructors of a sum type Leaves : SumLeaf { [$1] } | Leaves SumLeaf { $2 : $1 } + | identifier of Type { [($1, Just $3)] } + | identifier { [($1, Nothing)] } + | dollar {% Left $ Expected $1 "$" "|" } Universals : { [] } - | doubleBraces { [] } -- TODO this gets rid of information + | doubleBraces { [] } | Universals Universal { $2 : $1 } +-- | Optionally parse a termetric OptTermetric : { Nothing } | Termetric { Just (snd $1) } +-- | Parse a unary operator UnOp : tilde { Negate } +-- | Parse a binary operator BinOp : plus { Add } | minus { Sub } | div { Div } @@ -368,81 +419,113 @@ | leq { LessThanEq } | lbracket { LessThan } | rbracket { GreaterThan } - | eq { Equal } | neq { NotEqual } | andOp { LogicalAnd } | or { LogicalOr } + | doubleEq { StaticEq } + | eq { Equal } +-- | Optionally parse a function body OptExpression : { Nothing } - | eq Expression { Just $2 } + | eq Expression { Just $2 } -- FIXME only let this happen for external declarations +-- | Parse a constructor for a 'dataprop' DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 } +-- | Parse several constructors for a 'dataprop' DataPropLeaves : DataPropLeaf { [$1] } | DataPropLeaves DataPropLeaf { $2 : $1 } + | prval {% Left $ Expected $1 "Constructor" "prval" } + | var {% Left $ Expected $1 "Constructor" "var" } + | lambda {% Left $ Expected $1 "Constructor" "lam" } + | llambda {% Left $ Expected $1 "Constructor" "llam" } + | minus {% Left $ Expected $1 "Constructor" "-" } + | dollar {% Left $ Expected $1 "Constructor" "$" } + | fromVT {% Left $ Expected $1 "Constructor" "?!" } + | prfTransform {% Left $ Expected $1 "Constructor" ">>" } + | maybeProof {% Left $ Expected $1 "Constructor" "?" } +-- | Parse a type signature and optional function body PreFunction : FunName openParen FullArgs closeParen signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) } | FunName Universals OptTermetric signature Type OptExpression { PreF $1 $4 [] $2 [] $5 $3 $6 } | FunName Universals OptTermetric doubleParens signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 } | FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 } | Universals FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 } + | prval {% Left $ Expected $1 "Function signature" "prval" } + | var {% Left $ Expected $1 "Function signature" "var" } + | lambda {% Left $ Expected $1 "Function signature" "lam" } + | llambda {% Left $ Expected $1 "Function signature" "llam" } +-- | Parse affiliated `sortdef`s AndSort : AndSort and identifier eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way | sortdef identifier eq Type { SortDef $1 $2 $4 } +-- | Function declaration FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] } + | prfun PreFunction { [ Func $1 (PrFun $2) ] } | fnx PreFunction { [ Func $1 (Fnx $2) ] } - | FunDecl and PreFunction { Func $2 (And $3) : $1 } | extern FunDecl { over _head (Extern $1) $2 } + | FunDecl and PreFunction { Func $2 (And $3) : $1 } + | lambda {% Left $ Expected $1 "Function declaration" "lam" } + | llambda {% Left $ Expected $1 "Function declaration" "llam" } +-- | Parse a declaration defining a type +TypeDecl : typedef identifier eq at lbrace Records rbrace { RecordType $2 [] $6 } + | typedef identifier eq Type { TypeDef $1 $2 [] $4 } + | typedef identifier openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 } + | typedef identifier openParen FullArgs closeParen eq at lbrace Records rbrace { RecordType $2 $4 $9 } + | vtypedef identifier eq at lbrace Records rbrace { RecordViewType $2 [] $6 } + | vtypedef identifier eq Type { ViewTypeDef $1 $2 [] $4 } + | vtypedef identifier openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 } + | vtypedef identifier openParen FullArgs closeParen eq at lbrace Records rbrace { RecordViewType $2 $4 $9 } + | datatype identifier eq Leaves { SumType $2 [] $4 } + | datatype identifier openParen Args closeParen eq Leaves { SumType $2 $4 $7 } + | datavtype identifier eq Leaves { SumViewType $2 [] $4 } + | datavtype identifier openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 } + | abstype identifier openParen FullArgs closeParen eq Type { AbsType $1 $2 $4 $7 } + | absvtype identifier openParen FullArgs closeParen eq Type { AbsViewType $1 $2 $4 $7 } + | dataprop identifier openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 } + | absprop identifier openParen FullArgs closeParen { AbsProp $1 $2 [] } + | stadef identifier eq Name { Stadef $2 $4 [] } + | stadef identifier eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 } + | sortdef identifier eq Type { SortDef $1 $2 $4 } + | AndSort { $1 } + +-- | Parse a declaration Declaration : include string { Include $2 } - | staload underscore eq string { Staload (Just "_") $4 } -- FIXME wildcard name should have its own type? + | define { Define $1 } + | cblock { CBlock $1 } + | lineComment { Comment $1 } + | staload underscore eq string { Staload (Just "_") $4 } | staload string { Staload Nothing $2 } | staload identifier eq string { Staload (Just $2) $4 } | extern Declaration { Extern $1 $2 } - | AndSort { $1 } | var Pattern signature Type eq PreExpression { Var (Just $4) $2 (Just $6) } | val Pattern signature Type eq PreExpression { Val $1 (Just $4) $2 $6 } - | val Pattern eq PreExpression { Val $1 Nothing $2 $4 } + | val Pattern eq Expression { Val $1 Nothing $2 $4 } | var Pattern eq PreExpression { Var Nothing $2 (Just $4) } | var Pattern signature Type { Var (Just $4) $2 Nothing } | prval Pattern eq PreExpression { PrVal $2 $4 } | praxi PreFunction { Func $1 (Praxi $2) } + | primplmnt Implementation { ProofImpl $2 } | implement Implementation { Impl [] $2 } | implement openParen Args closeParen Implementation { Impl $3 $5 } - | primplmnt Implementation { ProofImpl $2 } | 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 } - | vtypedef identifier eq at lbrace Records rbrace { RecordViewType $2 [] $6 } - | typedef identifier eq Type { TypeDef $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 } - | 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 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 } + | tkindef Name eq string { TKind $1 $2 $4 } + | TypeDecl { $1 } | lambda {% Left $ Expected $1 "Declaration" "lam" } | llambda {% Left $ Expected $1 "Declaration" "llam" } - | ref {% Left $ Expected $1 "Declaration" "ref" } + | minus {% Left $ Expected $1 "Declaration" "-" } + | dollar {% Left $ Expected $1 "Declaration" "$" } + | fromVT {% Left $ Expected $1 "Declaration" "?!" } + | prfTransform {% Left $ Expected $1 "Declaration" ">>" } + | maybeProof {% Left $ Expected $1 "Declaration" "?" } { data ATSError a = Expected AlexPosn a a - | On AlexPosn a - | Unknown AlexPosn + | Unknown Token deriving (Eq, Show, Generic, NFData) instance Pretty AlexPosn where @@ -450,8 +533,8 @@ instance Pretty (ATSError String) where pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s2) <> ", expected:" <+> squotes (string s1)) <> linebreak - pretty (Unknown p) = red "Error:" <+> "unknown" <+> pretty p <> linebreak + pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak parseError :: [Token] -> Either (ATSError String) a -parseError = Left . Unknown . token_posn . head +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 @@ -17,6 +17,7 @@ import Control.Arrow hiding ((<+>)) import Control.Composition import Control.DeepSeq (NFData) +import Control.Lens hiding (op) #if __GLASGOW_HASKELL__ >= 801 import Data.Function (on) #endif @@ -45,16 +46,21 @@ instance Eq Doc where (==) = on (==) show --- FIXME account for %{, %{$, and %{# +takeBlock :: String -> (String, String) +takeBlock ('%':'}':ys) = ("", ('%':) . ('}':) $ ys) +takeBlock (y:ys) = first (y:) $ takeBlock ys +takeBlock [] = ([], []) + +rest :: String -> IO String +rest xs = fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs) + processClang :: String -> IO String -processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs) - where - takeBlock :: String -> (String, String) - takeBlock ('%':'}':ys) = ("", ('%':) . ('}':) $ ys) - takeBlock (y:ys) = first (y:) $ takeBlock ys - takeBlock [] = ([], []) -processClang (x:xs) = fmap (x:) $ processClang xs -processClang [] = pure [] +processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ rest xs +processClang ('%':'{':'#':xs) = fmap (('%':) . ('{':) . ('#':)) $ rest xs +processClang ('%':'{':'$':xs) = fmap (('%':) . ('{':) . ('$':)) $ rest xs +processClang ('%':'{':xs) = fmap (('%':) . ('{':)) $ rest xs +processClang (x:xs) = fmap (x:) $ processClang xs +processClang [] = pure [] printClang :: String -> IO String printClang = readCreateProcess (shell "clang-format") @@ -76,6 +82,7 @@ instance Pretty LambdaType where pretty Plain{} = "=>" + pretty Spear{} = "=>>" pretty (Full _ v) = "=<" <> string v <> ">" instance Pretty BinOp where @@ -91,6 +98,7 @@ pretty LogicalOr = "||" pretty LessThanEq = "<=" pretty GreaterThanEq = ">=" + pretty StaticEq = "==" splits :: BinOp -> Bool splits Mult = True @@ -101,18 +109,19 @@ splits LogicalOr = True splits _ = False -instance Pretty Addendum where - pretty Plus = "+" - pretty Minus = "-" - pretty None = "" - startsParens :: Doc -> Bool startsParens d = f (show d) where f ('(':_) = True f _ = False +prettyBinary :: Doc -> [Doc] -> Doc +prettyBinary _ [] = mempty +prettyBinary _ [e] = e +prettyBinary op [e, e'] = e <+> op <+> e' +prettyBinary _ _ = "FIXME" + instance Pretty Expression where - pretty = cata 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 (SifF e e' e'') = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e'' @@ -126,9 +135,7 @@ 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 (BinListF op@Add es) = prettyBinary (pretty op) es a (BinaryF op e e') | splits op = e pretty op <+> e' | otherwise = e <+> pretty op <+> e' @@ -139,20 +146,17 @@ 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 [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 (CallF name [] us Nothing []) = pretty name <> prettyArgsU "{" "}" us + a (CallF name is [] Nothing []) = pretty name <> prettyArgsU "<" ">" is + a (CallF name is [] Nothing [x]) + | startsParens x = pretty name <> prettyArgsU "<" ">" is <> pretty x + a (CallF name is [] Nothing xs) = pretty name <> prettyArgsU "<" ">" is <> 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 (PrecedeF e e') = parens (e <+> ";" e') + a (PrecedeF e e') = parens (e <+> ";" e') -- TODO use plated + write this like arguments with commas + a (PrecedeListF es) = prettyArgsList " ; " "(" ")" es a (FieldMutateF _ o f v) = pretty o <> "->" <> string f <+> ":=" <+> v a (MutateF e e') = e <+> ":=" <+> e' a (DerefF _ e) = "!" <> e @@ -163,7 +167,6 @@ 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) <> " ") @@ -183,6 +186,9 @@ noParens :: Doc -> Bool noParens = all (`notElem` ("()" :: String)) . show +patternHelper :: [Doc] -> Doc +patternHelper ps = mconcat (punctuate ", " (reverse ps)) + instance Pretty Pattern where pretty = cata a where a (WildcardF _) = "_" @@ -190,18 +196,17 @@ a (PLiteralF e) = pretty e a (PNameF s []) = string s a (PNameF s [x]) = string s <> parens x - a (PNameF s ps) = string s <> parens (mconcat (punctuate ", " (reverse ps))) + a (PNameF s ps) = string s <> parens (patternHelper ps) a (FreeF p) = "~" <> p a (GuardedF _ e p) = p <+> "when" <+> pretty e - a (ProofF _ p p') = parens (p <+> "|" <+> p') - a NullPatternF{} = "()" - a (TuplePatternF ps) = parens (mconcat (punctuate ", " (reverse ps))) + a (ProofF _ p p') = parens (patternHelper p <+> "|" <+> patternHelper p') + a (TuplePatternF ps) = parens (patternHelper ps) instance Pretty Arg where - pretty (Arg s Nothing) = pretty s - pretty (Arg "" (Just t)) = pretty t - pretty (Arg s (Just t)) = pretty s <+> colon <+> pretty t - pretty (PrfArg a as) = "(" <> pretty a <+> "|" <+> prettyArgs as <> ")" + pretty (Arg (First s)) = pretty s + pretty (Arg (Second t)) = pretty t + pretty (Arg (Both s t)) = pretty s <+> colon <+> pretty t + pretty (PrfArg a a') = pretty a <+> "|" <+> pretty a' instance Pretty Type where pretty = cata a where @@ -234,6 +239,8 @@ a (RefTypeF t) = "&" <> t a (ViewTypeF _ t) = "view@" <> parens t a (FunctionTypeF s t t') = t <+> string s <+> t' + a NoneTypeF{} = "()" + a ImplicitTypeF{} = ".." gan :: Maybe Type -> Doc gan (Just t) = " : " <> pretty t <> " " @@ -243,16 +250,18 @@ pretty (Existential [] Nothing (Just e)) = lbracket <+> pretty e <+> rbracket pretty (Existential bs ty Nothing) = lbracket <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket pretty (Existential bs ty (Just e)) = lbracket <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket - where go (Arg s Nothing) = pretty s - go (Arg s (Just t)) = pretty s <+> colon <+> pretty t + where go (Arg (First s)) = pretty s + go (Arg (Both s t)) = pretty s <+> colon <+> pretty t go _ = "FIXME" -- maybe use a new type? I don't think this should ever happen. instance Pretty Universal where - pretty (Universal [x] Nothing Nothing) = lbrace <> pretty x <> rbrace + pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments + pretty (Universal [x] Nothing Nothing) = lbrace <> pretty x <> rbrace -- FIXME universals can now be length-one arguments pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbrace pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace - where go (Arg s Nothing) = pretty s - go (Arg s (Just t)) = pretty s <+> colon <+> pretty t + where go (Arg (First s)) = pretty s + go (Arg (Both s t)) = pretty s <+> colon <+> pretty t + go (Arg (Second t)) = pretty t go _ = "FIXME" instance Pretty ATS where @@ -319,18 +328,34 @@ prettyLeaf ((s, Nothing):xs) = prettyLeaf xs $$ indent 2 ("|" <+> string s) prettyLeaf ((s, Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> string s <+> "of" <+> pretty e) +prettyHelper :: Doc -> [Doc] -> [Doc] +prettyHelper _ [x] = [x] +prettyHelper c (x:xs) = flatAlt (" " <> x) x : fmap (c <>) xs +prettyHelper _ x = x + +prettyBody :: Doc -> Doc -> [Doc] -> Doc +prettyBody c1 c2 = (c1 <>) . align . indent (-1) . cat . (<> pure c2) + +prettyArgsG' :: Doc -> Doc -> Doc -> [Doc] -> Doc +prettyArgsG' c3 c1 c2 = prettyBody c1 c2 . prettyHelper c3 . reverse + +prettyArgsList :: Doc -> Doc -> Doc -> [Doc] -> Doc +prettyArgsList c3 c1 c2 = prettyBody c1 c2 . va . prettyHelper c3 + +va :: [Doc] -> [Doc] +va = (& _tail.traverse %~ group) + prettyArgsG :: Doc -> Doc -> [Doc] -> Doc -prettyArgsG c1 c2 = (c1 <>) . align . indent (-1) . cat . (<> pure c2) . go . reverse -- TODO when it's only one arg, don't split ( off - where go :: [Doc] -> [Doc] - go [x] = [x] - go (x:xs) = flatAlt (" " <> x) x : fmap (", " <>) xs - go x = x +prettyArgsG = prettyArgsG' ", " -prettyArgs' :: (Pretty a) => Doc -> Doc -> [a] -> Doc -prettyArgs' = fmap pretty -.** prettyArgsG +prettyArgsU :: (Pretty a) => Doc -> Doc -> [a] -> Doc +prettyArgsU = prettyArgs' "," +prettyArgs' :: (Pretty a) => Doc -> Doc -> Doc -> [a] -> Doc +prettyArgs' = fmap pretty -.*** prettyArgsG' + prettyArgs :: (Pretty a) => [a] -> Doc -prettyArgs = prettyArgs' "(" ")" +prettyArgs = prettyArgs' ", " "(" ")" fancyU :: [Universal] -> Doc fancyU = foldMap pretty . reverse @@ -385,4 +410,4 @@ 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 + pretty _ = "FIXME" 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 @@ -1,11 +1,12 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} -- | This is a module containing types to model the ATS syntax tree. As it is -- collapsed by the pretty printer, you may see that in some places it is @@ -31,12 +32,12 @@ , Addendum (..) , DataPropLeaf (..) , PreFunction (..) - -- remove - , binList + , Paired (..) + , rewriteATS ) where import Control.DeepSeq (NFData) -import Control.Lens.Plated +import Data.Functor.Foldable (cata, embed) import Data.Functor.Foldable.TH (makeBaseFunctor) import GHC.Generics (Generic) import Language.ATS.Lexer (Addendum (..), AlexPosn) @@ -55,7 +56,7 @@ | AndDecl (Maybe Type) Pattern Expression | Include String | Staload (Maybe String) String - | Stadef String Name + | Stadef String Name [Type] | CBlock String | RecordType String [Arg] [(String, Type)] | RecordViewType String [Arg] [(String, Type)] @@ -75,6 +76,7 @@ | Local AlexPosn [Declaration] [Declaration] | AbsProp AlexPosn String [Arg] | Assume Name [Arg] Expression + | TKind AlexPosn Name String deriving (Show, Eq, Generic, NFData) data DataPropLeaf = DataPropLeaf [Universal] Expression @@ -109,11 +111,14 @@ | RefType Type | ViewType AlexPosn Type | FunctionType String Type Type + | NoneType AlexPosn + | ImplicitType AlexPosn 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) -- | A name can be qualified (`$UN.unsafefn`) or not @@ -130,14 +135,18 @@ | PLiteral Expression | Guarded AlexPosn Expression Pattern | Free Pattern - | Proof AlexPosn Pattern Pattern - | NullPattern AlexPosn + | Proof AlexPosn [Pattern] [Pattern] | TuplePattern [Pattern] deriving (Show, Eq, Generic, NFData) +data Paired a b = Both a b + | First a + | Second b + deriving (Show, Eq, Generic, NFData) + -- | An argument to a function. -data Arg = Arg String (Maybe Type) - | PrfArg Arg [Arg] +data Arg = Arg (Paired String Type) + | PrfArg Arg Arg deriving (Show, Eq, Generic, NFData) -- | Wrapper for universal quantifiers (refinement types) @@ -165,14 +174,15 @@ | NotEqual | LogicalAnd | LogicalOr + | StaticEq deriving (Show, Eq, Generic, NFData) -- | A (possibly effectful) expression. data Expression = Let AlexPosn ATS (Maybe Expression) | 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 - | Call Name [Expression] [Type] (Maybe Expression) [Expression] + -- function call: , then {n} + | Call Name [Type] [Type] (Maybe Expression) [Expression] | NamedVal Name | If { cond :: Expression -- ^ Expression evaluating to a boolean value , whenTrue :: Expression -- ^ Expression to be returned when true @@ -192,7 +202,6 @@ | CharLit Char | AtExpr Expression Expression | Binary BinOp Expression Expression - | BinList { _op :: BinOp, _exprs :: [Expression] } | Unary UnOp Expression | Case { posE :: AlexPosn , kind :: Addendum @@ -208,28 +217,17 @@ } | Mutate Expression Expression | Deref AlexPosn Expression - | Ref AlexPosn Type Expression | ProofExpr AlexPosn Expression Expression | TypeSignature Expression Type | WhereExp Expression [Declaration] | TupleEx AlexPosn [Expression] | While AlexPosn Expression Expression | Actions ATS - | TKind AlexPosn Name String - | ViewExpr AlexPosn Type -- TODO separate type for proof values? | Begin AlexPosn Expression + | BinList { _op :: BinOp, _exprs :: [Expression] } + | PrecedeList { _exprs :: [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 , preUniversalsI :: [Universal] @@ -264,3 +262,11 @@ makeBaseFunctor ''Pattern makeBaseFunctor ''Expression makeBaseFunctor ''Type + +rewriteATS :: Expression -> Expression +rewriteATS = cata a where + a (PrecedeF e e'@PrecedeList{}) = PrecedeList (e : _exprs e') + a (PrecedeF e e') = PrecedeList [e, e'] + a x = embed x + {- a (BinaryF Add e e'@BinList{}) = BinList Add (e : _exprs e') -} + {- a (BinaryF Add e e') = BinList Add [e, e'] -} diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -5,7 +5,7 @@ extra-deps: - ansi-wl-pprint-0.6.8.1 - htoml-megaparsec-1.0.1.11 - - composition-prelude-0.1.1.1 + - composition-prelude-0.1.1.2 - dirstream-1.0.3 flags: ats-format: diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -31,7 +31,7 @@ main :: IO () main = hspec $ describe "pretty-print" $ parallel $ - runSafeT $ runEffect $ atsPath >-> mapS testFile + runSafeT $ runEffect $ atsPath >-> mapS testFile mapS :: (a -> SpecM () ()) -> Proxy () a y' y (SafeT (SpecM ())) r mapS = P.mapM_ . (lift .)