ats-format 0.1.0.4 → 0.1.0.5

raw patch · 11 files changed

+431/−204 lines, 11 filesdep ~composition-preludePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: composition-prelude

API changes (from Hackage documentation)

Files

• .travis.yml +0/−6
• Justfile +8/−1
• README.md +4/−4
• ats-format.cabal +2/−2
• src/Language/ATS.hs +20/−1
• src/Language/ATS/Lexer.x +112/−19
• src/Language/ATS/Parser.y +169/−86
• src/Language/ATS/PrettyPrint.hs +76/−51
• src/Language/ATS/Types.hs +38/−32
• stack.yaml +1/−1
• test/Spec.hs +1/−1

@@ -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

@@ -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

@@ -2,15 +2,15 @@  [![Build Status](https://travis-ci.org/vmchale/ats-format.svg?branch=master)](https://travis-ci.org/vmchale/ats-format) +<img alt="Screenshot of sample results" src=https://github.com/vmchale/ats-format/raw/master/atsfmt.png>+<img alt="Screenshot of sample results" src=https://github.com/vmchale/ats-format/raw/master/atsfmt2.png>+ 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 

@@ -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

@@ -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

@@ -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 = "=>" | "=<cloref1>" | "=<cloptr1>" | "=>>" | "=<lincloptr1>"  -- FIXME whatever the fuck this is: -<cloptr,fe>-@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,cloptr1>" | "-<lin,prf>" | "-<>" | "-<prf>" -- FIXME allow spaces after comma?+@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,cloptr1>" | "-<fun0>" | "-<lin,prf>" | "-<>" | "-<prf>" -- 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'

@@ -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  }

@@ -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"

@@ -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 (`=>`, `=<cloref1>`, 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 `<a>`, 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: <a>, 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'] -}

@@ -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:

@@ -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 .)