diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -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 diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -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) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -1,6 +1,6 @@ module Main where -import Language.ATS.Exec (exec) +import Language.ATS (exec) main :: IO () main = exec diff --git a/ats-format.cabal b/ats-format.cabal --- a/ats-format.cabal +++ b/ats-format.cabal @@ -1,5 +1,5 @@ name: ats-format -version: 0.1.0.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 diff --git a/bench/Bench.hs b/bench/Bench.hs --- a/bench/Bench.hs +++ b/bench/Bench.hs @@ -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 = diff --git a/cabal.project.local b/cabal.project.local --- a/cabal.project.local +++ b/cabal.project.local @@ -6,3 +6,7 @@ documentation: True haddock-hoogle: True haddock-internal: True + +program-options + happy-options: -gcsa + alex-options: -g diff --git a/man/atsfmt.1 b/man/atsfmt.1 --- a/man/atsfmt.1 +++ b/man/atsfmt.1 @@ -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 diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs new file mode 100644 --- /dev/null +++ b/src/Language/ATS.hs @@ -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 diff --git a/src/Language/ATS/Exec.hs b/src/Language/ATS/Exec.hs --- a/src/Language/ATS/Exec.hs +++ b/src/Language/ATS/Exec.hs @@ -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) diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 = "=>" | "=" | "=" +@lambda = "=>" | "=" | "=" | "=>>" -@func_type = "-" | "-" | "-" | "-" | "-<>" | "-" -- FIXME allow spaces after comma? +-- FIXME whatever the fuck this is: - +@func_type = "-" | "-" | "-" | "-" | "-" | "-<>" | "-" -- 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 = ":<>" | ":" | ":" | ":" | ":" | ":" + 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] diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 $$ "=" } cloptr1Arrow { Arrow $$ "=" } + 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 diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 (`=>`, `=`, 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 ``, 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 , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic , universals :: [Universal] -- ^ Universal quantifiers/refinement type , args :: [Arg] -- ^ Actual function arguments diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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 ()