ats-format 0.1.0.1 → 0.1.0.2

raw patch · 15 files changed

+359/−178 lines, 15 filesdep +bytestringPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: bytestring

API changes (from Hackage documentation)

Files

• .travis.yml +6/−4
• Justfile +12/−7
• README.md +7/−5
• app/Main.hs +1/−1
• ats-format.cabal +6/−4
• bench/Bench.hs +1/−3
• cabal.project.local +4/−0
• man/atsfmt.1 +7/−0
• src/Language/ATS.hs +19/−0
• src/Language/ATS/Exec.hs +8/−5
• src/Language/ATS/Lexer.x +58/−22
• src/Language/ATS/Parser.y +134/−63
• src/Language/ATS/PrettyPrint.hs +66/−49
• src/Language/ATS/Types.hs +29/−12
• test/Spec.hs +1/−3

@@ -44,27 +44,29 @@ script:   - stack --no-terminal build --haddock --no-haddock-deps   - stack test --no-run-tests-  - curl -sL https://raw.githubusercontent.com/vmchale/tomlcheck/master/sh/check | sh -s .atsconfig.toml+  - curl -sL https://raw.githubusercontent.com/vmchale/tomlcheck/master/sh/check | sh -s .atsfmt.toml   - |     if [ `uname` = "Linux" ]     then       yamllint stack.yaml       yamllint appveyor.yml+      yamllint .yamllint       yamllint .travis.yml       yamllint .hlint.yaml       yamllint .stylish-haskell.yaml+      # curl -sL https://raw.github.com/ndmitchell/hlint/master/misc/travis.sh | sh -s src app test bench+      # curl -sL https://raw.github.com/ndmitchell/weeder/master/misc/travis.sh | sh -s src app test bench     else       echo "skipping yaml verification..."     fi   - stack build --test --bench --no-run-tests --no-run-benchmarks-  - curl -sL https://raw.github.com/ndmitchell/hlint/master/misc/travis.sh | sh -s .-  - curl -sL https://raw.github.com/ndmitchell/weeder/master/misc/travis.sh | sh -s .   - |     if [ `uname` = "Darwin" ]     then       export BINPATH="$(find . -name atsfmt -perm 755 | tail -n1)"     else-      export BINPATH="$(find -name atsfmt -executable | tail -n2 | head -n1)"+      rm -rf .stack-work+      export BINPATH="$(find -name atsfmt -executable | tail -n1 | head -n1)"     fi   - echo $BINPATH   - mv $BINPATH atsfmt-$TARGET

@@ -6,17 +6,22 @@     @poly . -e data/  bench:-    bench "atsfmt test/data/polyglot.dats"+    bench "atsfmt test/data/polyglot.dats" "atsfmt test/data/left-pad.dats"  manpages:     pandoc man/MANPAGE.md -s -t man -o man/atsfmt.1 +profile:+    @cabal new-build -p+    @cp $(fd 'atsfmt$' -IH dist-newstyle | tail -n1) ~/.local/bin+    @cp man/atsfmt.1 ~/.local/share/man/man1+ install:     @cabal new-build     @cp $(fd 'atsfmt$' -IH dist-newstyle | tail -n1) ~/.local/bin     @cp man/atsfmt.1 ~/.local/share/man/man1 -ci:+ci: test     cabal new-build     cabal new-test     hlint src app bench test@@ -29,11 +34,11 @@     weeder  test:-    @patscc -DATS_MEMALLOC_LIBC test/data/polyglot.dats -cleanaft -o pre &> /dev/null-    atsfmt test/data/polyglot.dats > tmp.dats-    @patscc -DATS_MEMALLOC_LIBC tmp.dats -cleanaft -o post &> /dev/null-    diff <(./pre) <(./post)-    @rm -f pre post *.c tmp.dats+    @rm -rf rm .ghc.environment.* polyglot+    @git clone https://github.com/vmchale/polyglot+    cd polyglot && atsfmt src/polyglot.dats -i+    cd polyglot && ./shake.hs+    @rm -rf polyglot  size:     @sn d $(fd 'atsfmt$' -IH dist-newstyle | tail -n1)

@@ -4,18 +4,20 @@  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 formatter is pleasantly fast, formatting a 1500 line file in <20ms.+ ## Configuration -`atsfmt` is configured with the `.atsfmt.toml` file. As an example:+`atsfmt` is configured with the `.atsfmt.toml` file. You can generate a default+configuration with -```toml-ribbon = 0.6 # maximum ribbon fraction-width = 120 # maximum width-clang-format = false # call clang-format on inline code+```bash+ $ atsfmt --default-config ```  ## Installation

@@ -1,6 +1,6 @@ module Main where -import           Language.ATS.Exec (exec)+import           Language.ATS (exec)  main :: IO () main = exec

@@ -1,5 +1,5 @@ name:                ats-format-version:             0.1.0.1+version:             0.1.0.2 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@@ -35,12 +35,13 @@  library   hs-source-dirs:      src-  exposed-modules:     Language.ATS.Types+  exposed-modules:     Language.ATS+  other-modules:       Language.ATS.Types                      , Language.ATS.Lexer                      , Language.ATS.Parser                      , Language.ATS.PrettyPrint                      , Language.ATS.Exec-  other-modules:       Paths_ats_format+                     , Paths_ats_format   build-depends:       base >= 4.9 && < 5                      , array                      , lens@@ -57,6 +58,7 @@                      , directory                      , process                      , file-embed+                     , bytestring   build-tools:         happy                      , alex   default-language:    Haskell2010@@ -73,7 +75,7 @@                      , ats-format   default-language:    Haskell2010   if flag(development)-    ghc-options: -Werror+    ghc-options:       -Werror   if impl(ghc >= 8.0)     ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat   ghc-options:         -Wall 

@@ -1,9 +1,7 @@ module Main where  import           Criterion.Main-import           Language.ATS.Lexer-import           Language.ATS.Parser-import           Language.ATS.PrettyPrint+import           Language.ATS  main :: IO () main =

@@ -6,3 +6,7 @@ documentation: True haddock-hoogle: True haddock-internal: True++program-options+  happy-options: -gcsa+  alex-options: -g

@@ -14,6 +14,8 @@ atsfmt \-\-default\-config .PP ac file.dats | atsfmt+.PP+atsfmt \[en]default\-config .SH DESCRIPTION .PP \f[B]atsfmt\f[] is an opinionated formatter for that ATS2 language.@@ -36,6 +38,11 @@ .TP .B \f[B]\-i\f[] Modify a file in\-place.+.RS+.RE+.TP+.B \f[B]\-\-default\-config\f[]+Generate a default configuration file in the current directory .RS .RE .SH CONFIGURATION

@@ -0,0 +1,19 @@+-- | Main module for the library+module Language.ATS ( -- * Functions+                      lexATS+                    , parseATS+                    , printATS+                    -- * Types+                    , ATS (..)+                    , Declaration (..)+                    , Expression (..)+                    , Type (..)+                    -- * Executable+                    , exec+                    ) where++import           Language.ATS.Exec+import           Language.ATS.Lexer+import           Language.ATS.Parser+import           Language.ATS.PrettyPrint+import           Language.ATS.Types

@@ -2,7 +2,6 @@ {-# LANGUAGE TemplateHaskell   #-}  module Language.ATS.Exec ( exec-                         , defaultConfig                          ) where  import           Control.Monad                (unless, (<=<))@@ -26,7 +25,7 @@ import           Text.Toml import           Text.Toml.Types              hiding (Parser) -data Program = Program { _path :: Maybe FilePath, _inplace :: Bool, _noConfig :: Bool }+data Program = Program { _path :: Maybe FilePath, _inplace :: Bool, _noConfig :: Bool, _defaultConfig :: Bool }  file :: Parser Program file = Program@@ -41,6 +40,9 @@         (long "no-config"         <> short 'o'         <> help "Ignore configuration file")+    <*> switch+        (long "default-config"+        <> help "Ignore configuration file")  versionInfo :: Parser (a -> a) versionInfo = infoOption ("madlang version: " ++ showVersion version) (short 'V' <> long "version" <> help "Show version")@@ -113,6 +115,7 @@ fancyError = either (printFail . show . pretty) pure  pick :: Program -> IO ()-pick (Program (Just p) False nc) = (genErr nc . parseATS . lexATS) =<< readFile p-pick (Program Nothing _ nc)      = (genErr nc . parseATS . lexATS) =<< getContents-pick (Program (Just p) True _)   = inplace p (fmap printATS . fancyError . parseATS . lexATS)+pick (Program (Just p) False nc _) = (genErr nc . parseATS . lexATS) =<< readFile p+pick (Program Nothing _ nc False)  = (genErr nc . parseATS . lexATS) =<< getContents+pick (Program Nothing _ _ True)    = defaultConfig ".atsfmt.toml"+pick (Program (Just p) True _ _)   = inplace p (fmap printATS . fancyError . parseATS . lexATS)

@@ -28,7 +28,7 @@ $digit = 0-9  -- Characters-$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\:\,\.\\\#]+$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#] $alpha = [a-zA-Z] $terminal = $printable # $white $esc_char = \27@@ -51,31 +51,48 @@ -- Strings @string = \" ($printable # [\"] | @escape_str | $esc_char | \n)* \" --- Identifiers -- FIXME this is buggy (can identifiers start with '!'?)+-- Identifiers @identifier = $alpha ($alpha | $digit | _ | !)* -@block_comment = \(\* ([^\)] | \n)* \*\) | \/\* ([^\)] | \n)* \*\/ -- FIXME should be able to do (* ) *)+-- Multi-line comments+@not_close_paren = (\*+ [^\)] | [^\*] \))+@paren_comment = \(\* ([^\)\*] | @not_close_paren | \n)* \*\)+@not_close_slash = (\*+ [^\/] | [^\*] \/)+@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 | "(" | ")" | _)+ ">" -@c_block = \%\{\^ (. # [\%] | \n)* \%\} -- FIXME only exclude the real bad parts+@not_close_c = \% [^\}]+@c_block = \%\{ ([^\%] | @not_close_c | \n)* \%\} -@lambda = "=>" | "=<cloref1>" | "=<cloptr1>"+@lambda = "=>" | "=<cloref1>" | "=<cloptr1>" | "=>>" -@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,prf>" | "-<>" | "-<prf>" -- FIXME allow spaces after comma?+-- FIXME whatever the fuck this is: -<cloptr,fe>+@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,cloptr1>" | "-<lin,prf>" | "-<>" | "-<prf>" -- FIXME allow spaces after comma? -@operator = "+" | "-" | "*" | "/" | "!=" | ">=" | "()" | "<=" | "=" | "~" | "&&" | "||" | ">" | "<" | "->" | ":=" | ".<" | ">." | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |+@operator = "+" | "-" | "*" | "/" | "!=" | ">=" | "<=" | "=" | "~" | "&&" | "||" | ">" | "<" | "->" | ":=" | ".<" | ">." | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow | --- TODO make stuff more specific = better errors + better speed.+@double_parens = "(" (@block_comment | "") ")"+@double_braces = "{" (@block_comment | "") "}"+@double_brackets = "<" (@block_comment | "") ">" +@view = v | view++@signature = ":<>" | ":<!wrt>" | ":<!exnwrt>" | ":<!laz>" | ":<!all>" | ":"+ tokens :-      $white+                  ;     "//".*                   ;     @block_comment           ;-    "#define".*              { tok (\p s -> DefineBlock p s) }      +    "#define".*              { tok (\p s -> MacroBlock p s) }      +    @if_block                { tok (\p s -> MacroBlock p s) }           @c_block                 { tok (\p s -> CBlockLex p s) }     fun                      { tok (\p s -> Keyword p KwFun) }     fnx                      { tok (\p s -> Keyword p KwFnx) }@@ -84,13 +101,12 @@     prfn                     { tok (\p s -> Keyword p KwPrfn) }     prfun                    { tok (\p s -> Keyword p KwPrfun) }     datatype                 { tok (\p s -> Keyword p KwDatatype) }-    datavtype                { tok (\p s -> Keyword p KwDatavtype) }+    data @view type          { tok (\p s -> Keyword p KwDatavtype) }     dataview                 { tok (\p s -> Keyword p KwDataview) }-    dataviewtype             { tok (\p s -> Keyword p KwDataviewtype) }     dataprop                 { tok (\p s -> Keyword p KwDataprop) }     assume                   { tok (\p s -> Keyword p KwAssume) }     typedef                  { tok (\p s -> Keyword p KwTypedef) }-    vtypedef                 { tok (\p s -> Keyword p KwVtypedef) }+    @view typedef            { tok (\p s -> Keyword p KwVtypedef) }     absprop                  { tok (\p s -> Keyword p KwAbsprop) }     llam                     { tok (\p s -> Keyword p KwLinearLambda) }     lam                      { tok (\p s -> Keyword p KwLambda) }@@ -116,15 +132,17 @@     void                     { tok (\p s -> Keyword p KwVoid) }     nat                      { tok (\p s -> Keyword p KwNat) }     implement                { tok (\p s -> Keyword p KwImplement) }+    primplmnt                { tok (\p s -> Keyword p KwProofImplement) }+    primplement              { tok (\p s -> Keyword p KwProofImplement) } -- TODO does this squash too much?     abst"@"ype               { tok (\p s -> Keyword p (KwAbst0p None)) }     t"@"ype"+"               { tok (\p s -> Keyword p (KwT0p Plus)) }     t"@"ype"-"               { tok (\p s -> Keyword p (KwT0p Minus)) }     t"@"ype                  { tok (\p s -> Keyword p (KwT0p None)) }-    vt"@"ype"+"              { tok (\p s -> Keyword p (KwVt0p Plus)) }-    vt"@"ype"-"              { tok (\p s -> Keyword p (KwVt0p Minus)) }-    vt"@"ype                 { tok (\p s -> Keyword p (KwVt0p None)) }+    @view"t@ype+"            { tok (\p s -> Keyword p (KwVt0p Plus)) }+    @view"t@ype-"            { tok (\p s -> Keyword p (KwVt0p Minus)) }+    @view"t@ype"             { tok (\p s -> Keyword p (KwVt0p None)) }     abstype                  { tok (\p s -> Keyword p KwAbstype) }-    absvtype                 { tok (\p s -> Keyword p KwAbsvtype) }+    abs @view type           { tok (\p s -> Keyword p KwAbsvtype) }     view                     { tok (\p s -> Keyword p KwView) }     "#"include               { tok (\p s -> Keyword p KwInclude) }     when                     { tok (\p s -> Keyword p KwWhen) }@@ -139,16 +157,24 @@     with                     { tok (\p s -> Keyword p KwWith) }     char                     { tok (\p s -> Keyword p KwChar) }     extern                   { tok (\p s -> Keyword p KwExtern) }-    @time_lit                { tok (\p s -> TimeTok p s) }+    sortdef                  { tok (\p s -> Keyword p KwSortdef) }+    propdef                  { tok (\p s -> Keyword p KwPropdef) }+    tkindef                  { tok (\p s -> Keyword p KwTKind) }+    "$raise"                 { tok (\p s -> Keyword p KwRaise) }+    @double_parens           { tok (\p s -> DoubleParenTok p) }+    @double_braces           { tok (\p s -> DoubleBracesTok p) }+    @double_brackets         { tok (\p s -> DoubleBracketTok p) }     @char_lit                { tok (\p s -> CharTok p (s !! 1)) }     @lambda                  { tok (\p s -> Arrow p s) }     @func_type               { tok (\p s -> FuncType p s) }     @bool                    { tok (\p s -> BoolTok p (read (over _head toUpper s)))}+    @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) }     @operator                { tok (\p s -> Operator p s) }+    @signature               { tok (\p s -> SignatureTok p (tail s)) }     $special                 { tok (\p s -> Special p s) }     @identifier              { tok (\p s -> Identifier p s) }     @string                  { tok (\p s -> StringTok p s) }@@ -221,10 +247,13 @@              | KwExtern              | KwAbsvtype              | KwProofImplement+             | KwSortdef+             | KwPropdef+             | KwRaise+             | KwTKind              deriving (Eq, Show, Generic, NFData) -data Token = Semicolon AlexPosn-           | Identifier AlexPosn String+data Token = Identifier AlexPosn String            | Keyword AlexPosn Keyword            | BoolTok AlexPosn Bool            | IntTok AlexPosn Int@@ -238,11 +267,14 @@            | FuncType AlexPosn String            | CommentLex AlexPosn String            | RefTok AlexPosn-           | DefineBlock AlexPosn String+           | MacroBlock AlexPosn String            | TimeTok AlexPosn String+           | SignatureTok AlexPosn String+           | DoubleParenTok AlexPosn+           | DoubleBracesTok AlexPosn+           | DoubleBracketTok AlexPosn            deriving (Eq, Show, Generic, NFData) -token_posn (Semicolon p) = p token_posn (Identifier p _) = p token_posn (Keyword p _) = p token_posn (BoolTok p _) = p@@ -257,8 +289,12 @@ token_posn (CharTok p _) = p token_posn (CommentLex p _) = p token_posn (RefTok p) = p-token_posn (DefineBlock 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  -- | This function turns a string into a stream of tokens for the parser. lexATS :: String -> [Token]

@@ -2,14 +2,14 @@     {-# LANGUAGE OverloadedStrings #-}     {-# LANGUAGE DeriveGeneric     #-}     {-# LANGUAGE DeriveAnyClass    #-}+    {-# LANGUAGE FlexibleContexts  #-}      -- | This module contains the parser.     module Language.ATS.Parser ( parseATS-                               , ATSError (..)+                               , ATSError                                ) where  import Language.ATS.Types- import Language.ATS.Lexer ( Token (..)                           , AlexPosn (..)                           , Keyword (..)@@ -17,13 +17,11 @@                           , token_posn                           ) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))--import Prelude- import Control.DeepSeq (NFData)-+import Control.Lens (over, _head) import GHC.Generics (Generic)+import Prelude+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))  } @@ -39,6 +37,7 @@     lambda { Keyword $$ KwLambda }     llambda { Keyword $$ KwLinearLambda }     if { Keyword $$ KwIf }+    sif { Keyword $$ KwSif }     stadef { Keyword $$ KwStadef }     val { Keyword _ (KwVal $$) }     prval { Keyword $$ KwPrval }@@ -48,6 +47,7 @@     typedef { Keyword $$ KwTypedef }     vtypedef { Keyword $$ KwVtypedef }     absvtype { Keyword $$ KwAbsvtype }+    abstype { Keyword $$ KwAbstype }     in { Keyword $$ KwIn }     end { Keyword $$ KwEnd }     stringType { Keyword $$ KwString }@@ -74,17 +74,28 @@     praxi { Keyword $$ KwPraxi }     extern { Keyword $$ KwExtern }     t0pPlain { Keyword $$ (KwT0p None) }+    t0pCo { Keyword $$ (KwT0p Plus) }     vt0pCo { Keyword $$ (KwVt0p Plus) }+    vt0pPlain { Keyword $$ (KwVt0p None) }     where { Keyword $$ KwWhere }     absprop { Keyword $$ KwAbsprop }+    sortdef { Keyword $$ KwSortdef }+    local { Keyword $$ KwLocal }+    view { Keyword $$ KwView }+    raise { Keyword $$ KwRaise }+    tkindef { Keyword $$ KwTKind }     boolLit { BoolTok _ $$ }     timeLit { TimeTok _ $$ }     intLit { IntTok _ $$ }     floatLit { FloatTok _ $$ }+    effmaskWrt { Identifier $$ "effmask_wrt" }+    effmaskAll { Identifier $$ "effmask_all" }+    extfcall { Identifier $$ "extfcall" }+    -- TODO token? raise { Identifier $$ "raise" }     identifier { Identifier _ $$ }     closeParen { Special $$ ")" }     openParen { Special $$ "(" }-    colon { Special $$ ":" }+    signature { SignatureTok _ $$ }     comma { Special $$ "," }     geq { Operator $$ ">=" }     leq { Operator $$ "<=" }@@ -100,9 +111,11 @@     vbar { Special $$ "|" }     lbrace { Special $$ "{" }     rbrace { Special $$ "}" }+    funcArrow { FuncType _ $$ }     plainArrow { Arrow $$ "=>" }     cloref1Arrow { Arrow $$ "=<cloref1>" }     cloptr1Arrow { Arrow $$ "=<cloptr1>" }+    spear { Arrow $$ "=>>" }     lsqbracket { Special $$ "[" }     rsqbracket { Special $$ "]" }     string { StringTok _ $$ }@@ -119,7 +132,8 @@     dollar { Special $$ "$" }     semicolon { Special $$ ";" }     andOp { Operator $$ "&&" }-    doubleParens { Operator $$ "()" }+    doubleParens { DoubleParenTok $$ }+    doubleBraces { DoubleBracesTok $$ }     prfTransform { Operator $$ ">>" } -- For types like &a >> a?!     refType { Special $$ "&" } -- For types like &a     maybeProof { Operator $$ "?" } -- For types like a?@@ -127,13 +141,19 @@     openExistential { Operator $$ "#[" } -- Same as `[` in ATS2     cblock { CBlockLex _ $$ }     ref { RefTok $$ }-    define { DefineBlock _ $$ }+    define { MacroBlock _ $$ }  %% -ATS : { ATS [] }-    | ATS Declaration { ATS ($2 : (\(ATS x) -> x) $1) }+ATS : Declarations { ATS $1 } +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" ">>" }+ TypeIn : Type { [$1] }        | TypeIn comma Type { $3 : $1 } @@ -149,6 +169,8 @@      | charType { Char }      | voidType { Void }      | t0pPlain { T0p None }+     | t0pCo { T0p Plus }+     | vt0pPlain { Vt0p None }      | vt0pCo { Vt0p Plus }      | stringType openParen Expression closeParen { DepString $3 }      | stringType Expression { DepString $2 }@@ -157,34 +179,41 @@      | identifier { Named $1 }      | int Expression { DependentInt $2 }      | exclamation Type { Unconsumed $2 }+     | Type funcArrow Type { FunctionType $2 $1 $3 }      | refType Type { RefType $2 }      | Type maybeProof { MaybeVal $1 }       | Type fromVT { FromVT $1 }      | Type prfTransform Type { AsProof $1 (Just $3) }      | Type prfTransform underscore { AsProof $1 Nothing }+     | view at Type { ViewType $1 $3 }      | Existential Type { Ex $1 $2 }      | Universal Type { ForA $1 $2 }      | Type at Type { At $2 $1 $3 }      | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }      | Name identifier { Dependent $1 [Named $2] }      | openParen TypeIn closeParen { Tuple $1 $2 }-     | absprop identifier openParen Args closeParen { AbsProp $1 $2 [] }+     | absprop identifier openParen FullArgs closeParen { AbsProp $1 $2 [] }      | openParen Type closeParen { $2 } -Args : { [] }-     | identifier { [Arg $1 Nothing] }-     | identifier colon Type { [Arg $1 (Just $3)] }-     | Type { [Arg "" (Just $1)] }-     | Args comma Type { Arg "" (Just $3) : $1 }-     | Args comma identifier colon Type { Arg $3 (Just $5) : $1 }-     | Args comma identifier { Arg $3 Nothing : $1 }-     | Type vbar Args { $3 } -- FIXME very very bad.+FullArgs : Args { $1 }+         | Arg vbar Args { [ PrfArg $1 $3 ] }+         | Arg vbar { [ PrfArg $1 [] ] } +-- TODO {i:nat;j:int}++Args : Arg { [$1] }+     | Args comma Arg { $3 : $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+ Literal : boolLit { BoolLit $1 }         | timeLit { TimeLit $1 }         | intLit { IntLit $1 }         | floatLit { FloatLit $1 }-        | string { StringLit (init . drop 1 $ $1) }+        | string { StringLit $1 }         | charLit { CharLit $1 }  PatternIn : Pattern { [$1] }@@ -202,9 +231,16 @@         | Literal { PLiteral $1 }         | Pattern when Expression { Guarded $2 $3 $1 } -Case : { [] }+Case : vbar Pattern LambdaArrow Expression { [($2, $4)] }+     | Pattern LambdaArrow Expression { [($1, $3)] }      | Case vbar Pattern LambdaArrow 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 }+ ExpressionIn : Expression { [$1] }              | ExpressionIn comma Expression { $3 : $1 } @@ -212,41 +248,55 @@                 | TupleExpression comma PreExpression { $3 : $1 }  LambdaArrow : plainArrow { Plain $1 }-            | cloref1Arrow { Full $1 "cloref1" }+            | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently.             | cloptr1Arrow { Full $1 "cloptr1" }+            | spear { Full $1 ">" }  Expression : PreExpression { $1 }-           | Name PreExpression { Call $1 [] [] [$2] }+           | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] }+           | Name PreExpression { Call $1 [] [] Nothing [$2] }            | openParen TupleExpression closeParen { TupleEx $1 $2 } +-- FIXME should these be types??+TypeArgs : lbrace Expression rbrace { [$2] }+         | lbrace ExpressionIn rbrace { $2 } -- TODO how much of this should be preserved?+         | TypeArgs lbrace Expression rbrace { $3 : $1 }+         | TypeArgs lbrace ExpressionIn rbrace { $3 ++ $1 }+ PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $1) $3 }               | Literal { $1 }               | doubleParens { VoidLiteral $1 }-              | Name doubleParens { Call $1 [] [] [] }-              | Name openParen ExpressionIn closeParen { Call $1 [] [] $3 }-              | Name lbrace ExpressionIn rbrace { Call $1 $3 [] [] }+              | 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) }               | 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 }               | PreExpression dot Name { Access $2 $1 $3 }               | openParen PreExpression closeParen { $2 }-              | if PreExpression then Expression else Expression { If $2 $4 $6 }-              | let ATS in Expression end { Let $1 $2 $4 }+              | 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) }+              | let ATS in end { Let $1 $2 Nothing }               | lambda Pattern LambdaArrow PreExpression { Lambda $1 $3 $2 $4 }               | llambda Pattern LambdaArrow PreExpression { LinearLambda $1 $3 $2 $4 }               | begin PreExpression end { $2 }               | at lbrace RecordVal rbrace { RecordValue $1 $3 Nothing }-              | at lbrace RecordVal rbrace colon Type { RecordValue $1 $3 (Just $6) }+              | 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 Declaration rbrace { WhereExp $1 $4 }-              | PreExpression colon Type { TypeSignature $1 $3 }+              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }+              | PreExpression signature Type { TypeSignature $1 $3 }               | Name { NamedVal $1 }               | lbrace ATS rbrace { Actions $2 }+              | underscore { UnderscoreLit $1 }               | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }               | include {% Left $ Expected $1 "Expression" "include" }               | staload {% Left $ Expected $1 "Expression" "staload" }@@ -261,28 +311,33 @@             | lsqbracket Args rsqbracket { Existential $2 Nothing Nothing }             | openExistential Args rsqbracket { Existential $2 Nothing Nothing }             | openExistential Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) }-            | lsqbracket Args colon Type rsqbracket { Existential $2 (Just $4) Nothing }+            | lsqbracket Args signature Type rsqbracket { Existential $2 (Just $4) Nothing } -- FIXME arguments should include more than just ':'             | lsqbracket Expression rsqbracket { Existential [] Nothing (Just $2) }               Universal : lbrace Args vbar PreExpression rbrace { Universal $2 Nothing (Just $4) }           | lbrace Args rbrace { Universal $2 Nothing Nothing }-          | lbrace Args colon Type vbar Expression rbrace { Universal $2 (Just $4) (Just $6) }-          | lbrace Args colon Type { Universal $2 (Just $4) Nothing }+          | lbrace Args signature Type vbar Expression rbrace { Universal $2 (Just $4) (Just $6) }+          | lbrace Args signature Type { Universal $2 (Just $4) Nothing } -Implementation : identifier doubleParens eq Expression { Implement $2 [] [] (Unqualified $1) [] $4 }-               | identifier openParen Args closeParen eq Expression { Implement $2 [] [] (Unqualified $1) $3 $6 }-               | identifier Universals openParen Args closeParen eq Expression { Implement $3 [] $2 (Unqualified $1) $4 $7 }-               | Universals identifier openParen Args closeParen eq Expression { Implement $3 $1 [] (Unqualified $2) $4 $7 }-               | Universals identifier Universals openParen Args closeParen eq Expression { Implement $4 $1 $3 (Unqualified $2) $5 $8 }+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 } -Name : identifier { Unqualified $1 }+FunName : identifier { Unqualified $1 }+        | identifier dollar identifier { Functorial $1 $3 }++Name : FunName { $1 }      | 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  RecordVal : identifier eq Expression { [($1, $3)] }           | RecordVal comma identifier eq Expression { ($3, $5) : $1 } -Records : identifier eq Type { [ ($1, $3) ] }+Records : identifier eq Type { [($1, $3)] }         | Records comma identifier eq Type { ($3, $5) : $1 }  SumLeaf : vbar identifier { ($2, Nothing) }@@ -292,6 +347,7 @@        | Leaves SumLeaf { $2 : $1 }  Universals : { [] }+           | doubleBraces { [] } -- TODO this gets rid of information            | Universals Universal { $2 : $1 }  OptTermetric : { Nothing }@@ -317,50 +373,65 @@  DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 } -DataPropLeaves : { [] }+DataPropLeaves : DataPropLeaf { [$1] }                | DataPropLeaves DataPropLeaf { $2 : $1 } -PreFunction : identifier openParen Args closeParen colon Type OptExpression { (PreF $1 [] [] $3 $6 Nothing $7) }-            | identifier Universals OptTermetric colon Type OptExpression { PreF $1 [] $2 [] $5 $3 $6 }-            | identifier Universals OptTermetric doubleParens colon Type OptExpression { PreF $1 [] $2 [] $6 $3 $7 }-            | identifier Universals OptTermetric openParen Args closeParen colon Type OptExpression { PreF $1 [] $2 $5 $8 $3 $9 }-            | Universals identifier Universals OptTermetric openParen Args closeParen colon Type OptExpression { PreF $2 $1 $3 $6 $9 $4 $10 }+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 } +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 }++FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }+        | fnx PreFunction { [ Func $1 (Fnx $2) ] }+        | FunDecl and PreFunction { Func $2 (And $3) : $1 }+        | extern FunDecl { over _head (Extern $1) $2 }+ Declaration : include string { Include $2 }-            | staload underscore eq string { Staload (Just "_") $4 } -- FIXME+            | staload underscore eq string { Staload (Just "_") $4 } -- FIXME wildcard name should have its own type?             | staload string { Staload Nothing $2 }             | staload identifier eq string { Staload (Just $2) $4 }             | extern Declaration { Extern $1 $2 }-            | var Pattern colon Type eq PreExpression { Var (Just $4) $2 $6 }-            | val Pattern colon Type eq PreExpression { Val $1 (Just $4) $2 $6 }-            | and Pattern colon Type eq PreExpression { AndDecl (Just $4) $2 $6 }+            | 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 }-            | and Pattern eq PreExpression { AndDecl Nothing $2 $4 }-            | var Pattern eq PreExpression { Var 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) }-            | implement Implementation { Impl $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 }-            | and PreFunction { Func $1 (And $2) }-            | fun PreFunction { Func $1 (Fun $2) }-            | fnx PreFunction { Func $1 (Fnx $2) }-            | vtypedef identifier eq Type { RecordViewType $2 $4 }+            | typedef identifier eq Type { TypeDef $1 $2 [] $4 }+            | vtypedef identifier eq Type { ViewTypeDef $1 $2 [] $4 }+            | vtypedef identifier openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 }             | datavtype identifier eq Leaves { SumViewType $2 $4 }-            | absvtype identifier openParen Args closeParen eq Type { AbsViewType $1 $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 }-            | dataprop identifier openParen Args closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }+            | dataprop identifier openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }+            -- | tkindef FunName eq string { TKind $1 $2 $4 }             | define { Define $1 }             | cblock { CBlock $1 }             | lambda {% Left $ Expected $1 "Declaration" "lam" }             | llambda {% Left $ Expected $1 "Declaration" "llam" }             | ref {% Left $ Expected $1 "Declaration" "ref" } +-- existentials+-- + {  data ATSError a = Expected AlexPosn a a+                | On AlexPosn a                 | Unknown AlexPosn                 deriving (Eq, Show, Generic, NFData) @@ -368,7 +439,7 @@     pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col  instance Pretty (ATSError String) where-    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s1) <> ", expected:" <+> squotes (string s2)) <> linebreak+    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  parseError :: [Token] -> Either (ATSError String) a

@@ -42,6 +42,7 @@ instance Eq Doc where     (==) = on (==) show +-- FIXME account for %{, %{$, and %{# processClang :: String -> IO String processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs)     where@@ -67,6 +68,8 @@ instance Pretty Name where     pretty (Unqualified n)   = string n     pretty (Qualified _ i n) = "$" <> string n <> "." <> string i+    pretty (SpecialName _ s) = "$" <> string s+    pretty (Functorial s s') = string s <> "$" <> string s'  instance Pretty LambdaType where     pretty Plain{}    = "=>"@@ -102,50 +105,55 @@  instance Pretty Expression where     pretty = cata a where-        a (IfF e e' e'')               = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (SifF e e' e'')              = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (LetF _ e e')                = "let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end" -- TODO soft linebreak?-        a (BoolLitF True)              = "true"-        a (BoolLitF False)             = "false"-        a (TimeLitF s)                 = string s-        a (IntLitF i)                  = pretty i-        a (LambdaF _ lt p e)          = "lam" <+> pretty p <+> pretty lt <+> e-        a (LinearLambdaF _ lt p e)    = "llam" <+> pretty p <+> pretty lt <+> e-        a (FloatLitF f)                = pretty f-        a (StringLitF s)               = dquotes (string s)+        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''+        a (LetF _ e (Just e'))          = "let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end" -- TODO soft linebreak?+        a (LetF _ e Nothing)            = "let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end"+        a (BoolLitF True)               = "true"+        a (BoolLitF False)              = "false"+        a (TimeLitF s)                  = string s+        a (IntLitF i)                   = pretty i+        a (LambdaF _ lt p e)            = "lam" <+> pretty p <+> pretty lt <+> e+        a (LinearLambdaF _ lt p e)      = "llam" <+> pretty p <+> pretty lt <+> e+        a (FloatLitF f)                 = pretty f+        a (StringLitF s)                = string s         a (BinaryF op e e')             | splits op = e </> pretty op <+> e' -- TODO if one operator splits, the rest should.             | otherwise = e <+> pretty op <+> e'-        a (IndexF _ n e)               = pretty n <> "[" <> e <> "]"-        a (UnaryF Negate e)            = "~" <> e-        a (NamedValF name)             = pretty name-        a (CallF name [] [] [])        = pretty name <> "()"-        a (CallF name [] [] xs)        = pretty name <> prettyArgsG "(" ")" xs-        a (CallF name [] ys [])        = pretty name <> prettyArgsG "<" ">" (fmap pretty ys)-- FIXME this should use { too?-        a (CallF name us [] [])        = pretty name <> prettyArgsG "{" "}" us-        a (CallF name [] ys xs)        = pretty name <> prettyArgsG "<" ">" (fmap pretty ys) <> prettyArgsG "(" ")" xs-        a (CallF name us [] xs)        = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "(" ")" xs-        a (CallF name us ys xs)        = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "<" ">" (fmap pretty ys) <> prettyArgsG "(" ")" xs-        a (CaseF _ add e cs)           = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs)-        a (VoidLiteralF _)             = "()"-        a (RecordValueF _ es Nothing)  = prettyRecord es-        a (RecordValueF _ es (Just x)) = prettyRecord es <+> ":" <+> pretty x-        a (BeginF e)                   = "begin" <$> indent 2 (pretty e) <$> "end"-        a (PrecedeF e e')              = parens (e <+> ";" </> e')-        a (FieldMutateF _ o f v)       = pretty o <> "->" <> string f <+> ":=" <+> v-        a (DerefF _ e)                 = "!" <> e+        a (IndexF _ n e)                = pretty n <> "[" <> e <> "]"+        a (UnaryF Negate e)             = "~" <> e+        a (NamedValF name)              = pretty name+        a (CallF name [] [] Nothing []) = pretty name <> "()"+        a (CallF name [] [] Nothing 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 xs) = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "(" ")" xs+        a (CallF name us ys Nothing xs) = pretty name <> prettyArgsG "{" "}" us <> prettyArgsG "<" ">" (fmap pretty ys) <> prettyArgsG "(" ")" xs+        a (CaseF _ add e cs)            = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs)+        a (VoidLiteralF _)              = "()"+        a (RecordValueF _ es Nothing)   = prettyRecord es+        a (RecordValueF _ es (Just x))  = prettyRecord es <+> ":" <+> pretty x+        a (BeginF e)                    = "begin" <$> indent 2 (pretty e) <$> "end"+        a (PrecedeF e e')               = parens (e <+> ";" </> e')+        a (FieldMutateF _ o f v)        = pretty o <> "->" <> string f <+> ":=" <+> v+        a (MutateF e e')                = e <+> ":=" <+> e'+        a (DerefF _ e)                  = "!" <> e         a (AccessF _ e n)             | noParens e = e <> "." <> pretty n             | otherwise = parens e <> "." <> pretty n         a (CharLitF c)                 = "'" <> char c <> "'"         a (RefF _ t e)                 = "ref<" <> pretty t <> ">" <> parens e-        a LocalF{}                     = "FIXME"         a (ProofExprF _ e e')          = "(" <> e <+> "|" <+> e' <> ")"         a (TypeSignatureF e t)         = e <+> ":" <+> pretty t-        a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> pretty d <> " ")-        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " es)+        a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> pretty (ATS d) <> " ")+        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (reverse es))         a (WhileF _ e e')              = "while" <> parens e <> e'         a (ActionsF as)                = "{" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) as)) <$> "}"+        a UnderscoreLitF{}             = "_"+        a (AtExprF e e')               = e <> "@" <> parens e'+        a _ = "FIXME"         prettyCases []           = mempty         prettyCases [(s, t)]     = "|" <+> pretty s <+> "=>" <+> t         prettyCases ((s, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> "=>" <+> t@@ -171,6 +179,7 @@     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 <> ")"  instance Pretty Type where     pretty = cata a where@@ -189,7 +198,7 @@         a DoubleF             = "double"         a FloatF              = "float"         a (ForAF u t)         = pretty u <+> t-        a (UnconsumedF t)     = "!" <> t+        a (UnconsumedF t)     = "!" <> parens t         a (AsProofF t (Just t')) = t <+> ">>" <+> t'         a (AsProofF t Nothing) = t <+> ">> _"         a (FromVTF t)         = t <> "?!"@@ -202,6 +211,8 @@         a (TupleF _ ts)       = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))         a (RefTypeF t)        = "&" <> t         a (AbsPropF _ n as)   = "absprop" <+> string n <+> prettyArgs as+        a (ViewTypeF _ t)     = "view@" <> parens t+        a (FunctionTypeF s t t') = t <+> string s <+> t'  gan :: Maybe Type -> Doc gan (Just t) = " : " <> pretty t <> " "@@ -213,6 +224,7 @@     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+              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@@ -220,6 +232,7 @@     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+              go _                = "FIXME"  instance Pretty ATS where     pretty (ATS xs) = concatSame xs@@ -238,10 +251,12 @@ glue _ _                           = False  repulse :: Declaration -> Declaration -> Bool-repulse Impl{} Impl{}   = True-repulse Extern{} Impl{} = True-repulse _ Extern{}      = True-repulse _ _             = False+repulse Impl{} Impl{}      = True+repulse Extern{} Impl{}    = True+repulse Include{} Extern{} = False+repulse _ Extern{}         = True+repulse Extern{} _         = True+repulse _ _                = False  {-# INLINE glue #-} @@ -303,15 +318,15 @@ fancyU = foldMap pretty . reverse  instance Pretty PreFunction where-    pretty (PreF i [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i pus us as rt (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i pus us as rt Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line-    pretty (PreF i pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <+> pretty rt+    pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si <+> pretty rt <+> "=" <$> indent 2 (pretty e) <> line+    pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si <+> pretty rt     pretty _ = "FIXME"  instance Pretty DataPropLeaf where@@ -319,9 +334,10 @@  instance Pretty Declaration where     pretty (RecordType s rs)     = "typedef" <+> string s <+> "=" <+> prettyRecord rs <> line-    pretty (SumViewType s ls)    = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls+    pretty (SumViewType s ls)    = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls <> linebreak     pretty (SumType s ls)        = "datatype" <+> string s <+> "=" <$> prettyLeaf ls-    pretty (Impl i)              = pretty i+    pretty (Impl [] i)           = pretty i+    pretty Impl{}                = "FIXME"     pretty (PrVal p e)           = "prval" <+> pretty p <+> "=" <+> pretty e     pretty (Val a Nothing p e)   = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e     pretty (Val a (Just t) p e)  = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e@@ -337,7 +353,8 @@     pretty (Func _ (Fnx pref))   = "fnx" </> pretty pref     pretty (Func _ (And pref))   = "and" </> pretty pref     pretty (Func _ (Praxi pref)) = "praxi" </> pretty pref-    pretty (Extern _ d)          = "extern" </> pretty d+    pretty (Extern _ d)          = "extern" <$> pretty d     pretty (Define s)            = string s     pretty (DataProp _ s as ls)  = "dataprop" <+> string s <> prettyArgs as <+> "=" <$> prettyDL ls+    pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> string s <+> "=" <+> pretty t <> linebreak     pretty _                     = mempty

@@ -43,26 +43,32 @@  -- | Declare something in a scope (a function, value, action, etc.) data Declaration = Func AlexPosn Function-                 | Impl Implementation-                 | ProofImpl Implementation -- primplmnt-                 | Val Addendum (Maybe Type) Pattern Expression+                 | Impl [Arg] Implementation+                 | ProofImpl Implementation -- primplmnt -- TODO add args+                 | Val Addendum (Maybe Type) Pattern Expression -- TODO expression should be optional?                  | PrVal Pattern Expression-                 | Var (Maybe Type) Pattern Expression -- TODO can a `var` really appear anywhere in top-level declarations+                 | Var (Maybe Type) Pattern (Maybe Expression) -- TODO AlexPosn                  | AndDecl (Maybe Type) Pattern Expression                  | Include String                  | Staload (Maybe String) String                  | Stadef String Name                  | CBlock String                  | RecordType String [(String, Type)]-                 | RecordViewType String Type+                 | RecordViewType String [(String, Type)]+                 | TypeDef AlexPosn String [Arg] Type+                 | ViewTypeDef AlexPosn String [Arg] Type                  | SumType String [(String, Maybe Type)]                  | SumViewType String [(String, Maybe Type)]+                 | AbsType AlexPosn String [Arg] Type                  | AbsViewType AlexPosn String [Arg] Type                  | OverloadOp AlexPosn BinOp Name                  | Comment String                  | DataProp AlexPosn String [Arg] [DataPropLeaf]                  | Extern AlexPosn Declaration                  | Define String+                 | SortDef AlexPosn String Type+                 | AndD Declaration Declaration+                 | Local AlexPosn [Declaration] [Declaration]                  deriving (Show, Eq, Generic, NFData)  data DataPropLeaf = DataPropLeaf [Universal] Expression@@ -96,6 +102,8 @@           | ConcreteType Expression           | RefType Type           | AbsProp AlexPosn String [Arg]+          | ViewType AlexPosn Type+          | FunctionType String Type Type           deriving (Show, Eq, Generic, NFData)  -- | A type for the various lambda arrows (`=>`, `=<cloref1>`, etc.)@@ -106,6 +114,8 @@ -- | A name can be qualified (`$UN.unsafefn`) or not data Name = Unqualified String           | Qualified AlexPosn String String+          | SpecialName AlexPosn String+          | Functorial String String           deriving (Show, Eq, Generic, NFData)  -- | A data type for patterns.@@ -122,6 +132,7 @@  -- | An argument to a function. data Arg = Arg String (Maybe Type)+         | PrfArg Arg [Arg]     deriving (Show, Eq, Generic, NFData)  -- | Wrapper for universal quantifiers (refinement types)@@ -152,28 +163,30 @@            deriving (Show, Eq, Generic, NFData)  -- | A (possibly effectful) expression.-data Expression = Let AlexPosn ATS Expression+data Expression = Let AlexPosn ATS (Maybe Expression)                 | Begin ATS-                | Local ATS                 | VoidLiteral -- The '()' literal representing inaction.                     AlexPosn-                | Call Name [Expression] [Type] [Expression]+                -- 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]                 | NamedVal Name                 | If { cond     :: Expression -- ^ Expression evaluating to a boolean value                      , whenTrue :: Expression -- ^ Expression to be returned when true-                     , elseExpr :: Expression -- ^ Expression to be returned when false+                     , elseExpr :: Maybe Expression -- ^ Expression to be returned when false                      }-                | Sif { cond :: Expression, whenTrue :: Expression, elseExpr :: Expression }+                | Sif { cond :: Expression, whenTrue :: Expression, selseExpr :: Expression } -- Static if (for proofs)                 | BoolLit Bool                 | TimeLit String                 | FloatLit Float                 | IntLit Int+                | UnderscoreLit AlexPosn                 | Lambda AlexPosn LambdaType Pattern Expression                 | LinearLambda AlexPosn LambdaType Pattern Expression                 | Index AlexPosn Name Expression                 | Access AlexPosn Expression Name                 | StringLit String                 | CharLit Char+                | AtExpr Expression Expression                 | Binary BinOp Expression Expression                 | Unary UnOp Expression                 | Case { posE :: AlexPosn@@ -188,14 +201,17 @@                               , field :: String -- ^ Field being modified                               , new   :: Expression -- ^ New value of the field                               }+                | Mutate Expression Expression                 | Deref AlexPosn Expression                 | Ref AlexPosn Type Expression                 | ProofExpr AlexPosn Expression Expression                 | TypeSignature Expression Type-                | WhereExp Expression Declaration+                | 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?                 deriving (Show, Eq, Generic, NFData)  -- | An 'implement' declaration@@ -218,7 +234,8 @@               | Praxi PreFunction               deriving (Show, Eq, Generic, NFData) -data PreFunction = PreF { fname         :: String -- ^ Function name+data PreFunction = PreF { fname         :: Name -- ^ Function name+                        , sig           :: String -- ^ e.g. <> or <!wrt>                         , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic                         , universals    :: [Universal] -- ^ Universal quantifiers/refinement type                         , args          :: [Arg] -- ^ Actual function arguments

@@ -1,8 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} -import           Language.ATS.Lexer       (lexATS)-import           Language.ATS.Parser      (parseATS)-import           Language.ATS.PrettyPrint (printATS)+import           Language.ATS import           Test.Hspec  main :: IO ()