ats-format (empty) → 0.1.0.0
raw patch · 19 files changed
+1842/−0 lines, 19 filesdep +ansi-terminaldep +ansi-wl-pprintdep +arraybuild-type:Customsetup-changed
Dependencies added: ansi-terminal, ansi-wl-pprint, array, ats-format, base, composition-prelude, criterion, deepseq, directory, file-embed, hspec, htoml-megaparsec, lens, megaparsec, optparse-applicative, process, recursion-schemes, text, unordered-containers
Files
- .atsfmt.toml +3/−0
- .travis.yml +82/−0
- Justfile +35/−0
- LICENSE +11/−0
- README.md +33/−0
- Setup.hs +49/−0
- app/Main.hs +6/−0
- appveyor.yml +35/−0
- ats-format.cabal +107/−0
- bench/Bench.hs +22/−0
- cabal.project.local +8/−0
- man/atsfmt.1 +72/−0
- src/Language/ATS/Exec.hs +118/−0
- src/Language/ATS/Lexer.x +267/−0
- src/Language/ATS/Parser.y +376/−0
- src/Language/ATS/PrettyPrint.hs +343/−0
- src/Language/ATS/Types.hs +233/−0
- stack.yaml +12/−0
- test/Spec.hs +30/−0
+ .atsfmt.toml view
@@ -0,0 +1,3 @@+ribbon = 0.6 # maximum ribbon fraction+width = 120 # maximum width+clang-format = false # call clang-format on inline code
+ .travis.yml view
@@ -0,0 +1,82 @@+---+sudo: false+cache:+ directories:+ - $HOME/.stack+addons:+ apt:+ packages:+ - libgmp3-dev+matrix:+ include:++ # Linux+ - env: TARGET=x86_64-unkown-linux-gnu+ language: python++ # OS X+ - env: TARGET=x86_64-apple-darwin+ os: osx+ language: default++before_install:+ - mkdir -p ~/.local/bin+ - export PATH=$HOME/.local/bin:$PATH+ - |+ if [ `uname` = "Darwin" ]+ then+ curl --insecure -L https://www.stackage.org/stack/osx-x86_64 | tar xz --strip-components=1 --include '*/stack' -C ~/.local/bin+ else+ curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'+ fi+ - chmod a+x ~/.local/bin/stack+ - |+ if [ `uname` = "Linux" ]+ then+ pip install yamllint+ else+ echo "skipping yaml verification..."+ fi++install:+ - stack --no-terminal --install-ghc test --only-dependencies++script:+ - stack --no-terminal build --haddock --no-haddock-deps+ - stack test --no-run-tests+ - |+ if [ `uname` = "Linux" ]+ then+ yamllint stack.yaml+ yamllint appveyor.yml+ yamllint .travis.yml+ else+ echo "skipping yaml verification..."+ fi+ - stack bench --no-bench+ - 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)"+ fi+ - echo $BINPATH+ - mv $BINPATH atsfmt-$TARGET+ - ls atsfmt-$TARGET++deploy:+ api_key:+ secure: "bdJVbM9pdNqkeQb9O4mUocyA+zLAHupCLUYMPyi5jZVXF5hDPQeB93C7bMb+G4DzfYdDhDvy/VACYSGWnV2JwbSDObtAi8//wiN4Ir/AjK6aELEF8oVuoPOr4geIOMpjcUbT5JZhqqTF4Ogtd0jW97eg6LnkOZj/Nmirk7NL9FV85r3iw1MEIWBsLdHbpHKgyItOo2YKh0dM3QTZ3tjaeEhEVgd4VQQlEB2SAtueOu/lJhbjT6Y7ztGLW+UXE6ITXuG623ewA8tXt8oyeDx0HES04RVnfkDN7QIDC7Crcx7Q7Kb+yCc1cRe9QQ/9/kaeloCYd0XAKf+Bd1kyH2MIm+/Pnriz5pkM+2z1xEUhTXqXM6Wm1cXHVXRUHJQWayii1TSDp8DhVVoz8N0L3GMEIIJi1rdkO4qA84JcZkQFnH4NhvVK9Bkd/a++h6vh2WOg/nvwnOUBooNLkKik78PrIgpgTapW8yFyXrOlVqtQ9sdCmhrpQGn7Ja1P2z3tNmZgSvIcyhx/SLgHegPae5EJ9roFWRNJ9A/tlgyqNbxBdr5hLWSo3zqyJXj51cqd68tp09lloXLlC9Q2HlAejenfWYQ4KEwT1A8u+cK9lJ7pN+hgmlbQFCz9aYzokD6CCzsdJo01yQMCW2LtlKEeWiUVuA3MrWZ3l+oFQ6/npGQoOQY="+ file: atsfmt-$TARGET+ on:+ tags: true+ provider: releases+ skip_cleanup: true++branches:+ only:+ - /\d+\.\d+\.\d+\.\d+.*$/+ - master
+ Justfile view
@@ -0,0 +1,35 @@+clean:+ sn c .+ rm -rf tags *.c++polyglot:+ @poly . -e data/++bench:+ bench "atsfmt test/data/polyglot.dats"++manpages:+ pandoc man/MANPAGE.md -s -t man -o man/atsfmt.1++install:+ @cabal new-build+ @cp $(fd 'atsfmt$' -IH dist-newstyle | tail -n1) ~/.local/bin+ @cp man/atsfmt.1 ~/.local/share/man/man1++ci:+ cabal new-build+ cabal new-test+ hlint src app bench test+ tomlcheck --file .atsfmt.toml+ stack build --test --bench --no-run-tests --no-run-benchmarks+ 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++size:+ @sn d $(fd 'atsfmt$' -IH dist-newstyle | tail -n1)
+ LICENSE view
@@ -0,0 +1,11 @@+Copyright Vanessa McHale (c) 2017++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,33 @@+# ats-formatter++[](https://travis-ci.org/vmchale/ats-format)++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.++If you find something that's not listed in `TODO.md` feel free to open+an issue.++## Configuration++`atsfmt` is configured with the `.atsfmt.toml` file. As an example:++```toml+ribbon = 0.6 # maximum ribbon fraction+width = 120 # maximum width+clang-format = false # call clang-format on inline code+```++## Installation++To install, first install [GHC](https://www.haskell.org/ghc/download.html), then+[cabal](https://www.haskell.org/cabal/download.html). Then++```bash+ $ cabal update+ $ cabal install ats-format+```++## License++All code except `test/data/left-pad.dats` is license under the BSD3 license.
+ Setup.hs view
@@ -0,0 +1,49 @@+import Control.Lens ((<&>))+import Control.Monad (unless, void)+import Data.Maybe+import Distribution.Simple+import System.Directory (createDirectoryIfMissing)+import System.Environment (lookupEnv)+import System.Process (readCreateProcessWithExitCode, shell)++manpage :: IO String+manpage = readFile "man/atsfmt.1"++main :: IO ()+main = setManpath >>+ writeManpages >>+ writeBashCompletions >>+ defaultMain++setManpath :: IO ()+setManpath = do+ home <- lookupEnv "HOME"+ case home of+ Just x -> do+ let bashRc = x ++ "/.bashrc"+ config <- readFile bashRc+ unless (or (["#manpath updated by atsfmt", "#manpath updated by madlang"] <&> (`elem` lines config)))+ (appendFile bashRc "\n#manpath updated by atsfmt\nexport MANPATH=~/.local/share:$MANPATH\n" >>+ void (readCreateProcessWithExitCode (shell $ "MANPATH=" ++ x ++ "/.local/share mandb") ""))+ Nothing -> pure ()++writeManpages :: IO ()+writeManpages = do+ home <- lookupEnv "HOME"+ case home of+ Just x -> do+ let manPath = x ++ "/.local/share/man/man1"+ createDirectoryIfMissing True manPath+ writeFile (manPath ++ "/atsfmt.1") =<< manpage+ Nothing -> pure ()++writeBashCompletions :: IO ()+writeBashCompletions = do+ home <- lookupEnv "HOME"+ case home of+ Just x -> do+ let bashRc = x ++ "/.bashrc"+ config <- readFile bashRc+ unless ("# Added by atsfmt" `elem` lines config)+ (appendFile bashRc "\n# Added by atsfmt\neval \"$(atsfmt --bash-completion-script atsfmt)\"\n")+ Nothing -> pure ()
+ app/Main.hs view
@@ -0,0 +1,6 @@+module Main where++import Language.ATS.Exec (exec)++main :: IO ()+main = exec
+ appveyor.yml view
@@ -0,0 +1,35 @@+---++build: off++before_test:+ - set PATH=C:\Program Files\Git\mingw64\bin;%PATH%++ - curl -sS -ostack.zip -L --insecure http://www.stackage.org/stack/windows-i386+ - 7z x stack.zip stack.exe++clone_folder: "c:\\stack"+environment:+ global:+ STACK_ROOT: "c:\\sr"++test_script:+ - stack setup > nul+ - echo "" | stack --no-terminal install+ - ps: Get-ChildItem . -name -recurse atsfmt.exe+ - ps: Copy-Item c:\\stack\\.stack-work\\install\\afd8a623\\bin\\atsfmt.exe atsfmt-x86_64-pc-windows.exe+ - ps: Push-AppveyorArtifact atsfmt-x86_64-pc-windows.exe++deploy:+ artifacts: atsfmt-x86_64-pc-windows.exe+ provider: GitHub+ on:+ appveyor_repo_tag: true+ auth_token:+ secure: 0qzMr6xmEwRoj/9TJOgDuW/LXWfGVM/4A7kvAXGe0BAwWCF13AWE2SARrYkyc3ji++branches:+ only:+ # Release tags+ - master+ - /\d+\.\d+\.\d+\.\d+.*$/
+ ats-format.cabal view
@@ -0,0 +1,107 @@+name: ats-format+version: 0.1.0.0+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+license: BSD3+license-file: LICENSE+author: Vanessa McHale+maintainer: vamchale@gmail.com+copyright: Copyright: (c) 2017 Vanessa McHale+category: Parser, Language+build-type: Custom+extra-doc-files: README.md+data-files: .travis.yml+ , appveyor.yml+ , Justfile+extra-source-files: stack.yaml+ , cabal.project.local+ , .atsfmt.toml+ , man/atsfmt.1+cabal-version: >=1.18++custom-setup+ setup-depends: base+ , Cabal+ , directory+ , lens+ , process >= 1.4.0.0++Flag development {+ Description: Enable `-Werror`+ manual: True+ default: False+}++library+ hs-source-dirs: src+ exposed-modules: Language.ATS.Types+ , Language.ATS.Lexer+ , Language.ATS.Parser+ , Language.ATS.PrettyPrint+ , Language.ATS.Exec+ other-modules: Paths_ats_format+ build-depends: base >= 4.8 && < 5+ , array+ , lens+ , deepseq+ , ansi-wl-pprint >= 0.6.8+ , recursion-schemes+ , optparse-applicative+ , ansi-terminal+ , composition-prelude >= 0.1.1.1+ , htoml-megaparsec+ , megaparsec+ , unordered-containers+ , text+ , directory+ , process+ , file-embed+ build-tools: happy+ , alex+ default-language: Haskell2010+ if flag(development)+ ghc-options: -Werror+ if impl(ghc >= 8.0)+ ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat+ ghc-options: -Wall++executable atsfmt+ hs-source-dirs: app+ main-is: Main.hs+ build-depends: base+ , ats-format+ default-language: Haskell2010+ if flag(development)+ ghc-options: -Werror+ if impl(ghc >= 8.0)+ ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat+ ghc-options: -Wall ++test-suite ats-format-test+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base+ , ats-format+ , hspec+ if impl(ghc >= 8.0)+ ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall + default-language: Haskell2010++benchmark ats-format-bench+ type: exitcode-stdio-1.0+ hs-source-dirs: bench+ main-is: Bench.hs+ build-depends: base+ , ats-format+ , criterion+ ghc-options: -Wall + if impl(ghc >= 8.0)+ ghc-options: -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/vmchale/ats-format
+ bench/Bench.hs view
@@ -0,0 +1,22 @@+module Main where++import Criterion.Main+import Language.ATS.Lexer+import Language.ATS.Parser+import Language.ATS.PrettyPrint++main :: IO ()+main =+ defaultMain [ env envFiles $ \ ~(l, m) ->+ bgroup "format"+ [ bench "lexATS (large)" $ nf lexATS l+ , bench "parseATS . lexATS (large)" $ nf (parseATS . lexATS) l+ , bench "printATS . parseATS . lexATS (large)" $ nf (fmap printATS . parseATS . lexATS) l+ , bench "lexATS (medium)" $ nf lexATS m+ , bench "parseATS . lexATS (medium)" $ nf (parseATS . lexATS) m+ , bench "printATS . parseATS . lexATS (medium)" $ nf (fmap printATS . parseATS . lexATS) m+ ]+ ]+ where large = readFile "test/data/polyglot.dats"+ medium = readFile "test/data/filetype.sats"+ envFiles = (,) <$> large <*> medium
+ cabal.project.local view
@@ -0,0 +1,8 @@+constraints: ats-format +development+optimization: 2+with-compiler: ghc-8.2.2+tests: True+benchmarks: True+documentation: True+haddock-hoogle: True+haddock-internal: True
+ man/atsfmt.1 view
@@ -0,0 +1,72 @@+.\" Automatically generated by Pandoc 2.0.5+.\"+.TH "atsfmt (1)" "" "" "" ""+.hy+.SH NAME+.PP+atsfmt \- a source code formatter for ATS+.SH SYNOPSIS+.PP+atsfmt <file>+.PP+atsfmt \-i <file>+.PP+atsfmt \-\-default\-config+.PP+ac file.dats | atsfmt+.SH DESCRIPTION+.PP+\f[B]atsfmt\f[] is an opinionated formatter for that ATS2 language.+.SH OPTIONS+.TP+.B \f[B]\-h\f[] \f[B]\-\-help\f[]+Display help+.RS+.RE+.TP+.B \f[B]\-V\f[] \f[B]\-\-version\f[]+Display version information+.RS+.RE+.TP+.B \f[B]\-o\f[] \f[B]\-\-no\-config\f[]+Ignore configuration files in scope+.RS+.RE+.TP+.B \f[B]\-i\f[]+Modify a file in\-place.+.RS+.RE+.SH CONFIGURATION+.PP+\f[B]atsfmt\f[] is configured using a TOML file, by default+\&.atsfmt.toml.+You can generate a default configuration with+.IP+.nf+\f[C]+atsfmt\ \-\-default\-config+\f[]+.fi+.PP+To make \f[B]atsfmt\f[] call clang\-format on embedded C code, add the+following to your .atsfmt.toml+.IP+.nf+\f[C]+clang\-format\ =\ true+\f[]+.fi+.SH EDITOR INTEGRATION+.PP+Editor integration is available with the ATS vim plugin at:+.PP+https://github.com/vmchale/ats\-vim+.SH COPYRIGHT+.PP+Copyright 2017.+Vanessa McHale.+All Rights Reserved.+.SH AUTHORS+Vanessa McHale<vamchale@gmail.com>.
+ src/Language/ATS/Exec.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-}++module Language.ATS.Exec ( exec+ , defaultConfig+ ) where++import Control.Monad (unless, (<=<))+import Data.FileEmbed (embedStringFile)+import qualified Data.HashMap.Lazy as HM+import Data.Maybe (fromMaybe)+import Data.Monoid ((<>))+import qualified Data.Text.IO as TIO+import Data.Version+import Language.ATS.Lexer (lexATS)+import Language.ATS.Parser (ATSError, parseATS)+import Language.ATS.PrettyPrint (printATS, printATSCustom, processClang)+import Language.ATS.Types (ATS)+import Options.Applicative+import Paths_ats_format+import System.Directory (doesFileExist)+import System.Exit (exitFailure)+import System.IO (hPutStr, stderr)+import Text.Megaparsec (parseErrorPretty)+import Text.PrettyPrint.ANSI.Leijen (pretty)+import Text.Toml+import Text.Toml.Types hiding (Parser)++data Program = Program { _path :: Maybe FilePath, _inplace :: Bool, _noConfig :: Bool }++file :: Parser Program+file = Program+ <$> optional (argument str+ (metavar "FILEPATH"+ <> completer (bashCompleter "file -X '!*.*ats' -o plusdirs")+ <> help "File path to ATS source."))+ <*> switch+ (short 'i'+ <> help "Modify file in-place")+ <*> switch+ (long "no-config"+ <> short 'o'+ <> help "Ignore configuration file")++versionInfo :: Parser (a -> a)+versionInfo = infoOption ("madlang version: " ++ showVersion version) (short 'V' <> long "version" <> help "Show version")++wrapper :: ParserInfo Program+wrapper = info (helper <*> versionInfo <*> file)+ (fullDesc+ <> progDesc "ATS source code formater. For more detailed help, see 'man atsfmt'"+ <> header "ats-format - a source code formatter written using happy/alex")++exec :: IO ()+exec = execParser wrapper >>= pick++printFail :: String -> IO a+printFail = const exitFailure <=< hPutStr stderr++defaultConfig :: FilePath -> IO ()+defaultConfig = flip writeFile $(embedStringFile ".atsfmt.toml")++asFloat :: Node -> Maybe Float+asFloat (VFloat d) = Just (realToFrac d)+asFloat _ = Nothing++asInt :: Node -> Maybe Int+asInt (VInteger i) = Just (fromIntegral i)+asInt _ = Nothing++asBool :: Node -> Maybe Bool+asBool (VBoolean True) = Just True+asBool (VBoolean False) = Just False+asBool _ = Nothing++parseToml :: String -> IO (Float, Int, Bool)+parseToml p = do+ f <- TIO.readFile p+ case parseTomlDoc p f of+ Right x -> pure . fromMaybe (0.6, 120, False) $ do+ r <- asFloat =<< HM.lookup "ribbon" x+ w <- asInt =<< HM.lookup "width" x+ cf <- asBool =<< HM.lookup "clang-format" x+ pure (r, w, cf)+ Left e -> printFail $ parseErrorPretty e++printCustom :: ATS -> IO String+printCustom ats = do+ let p = ".atsfmt.toml"+ config <- doesFileExist p+ if config then do+ (r, w, cf) <- parseToml p+ let t = printATSCustom r w ats+ if cf then+ processClang t+ else+ pure t+ else+ pure $ printATS ats++genErr :: Bool -> Either (ATSError String) ATS -> IO ()+genErr b = either (printFail . show . pretty) (putStrLn <=< go)+ where go = if not b then printCustom else pure . printATS++inplace :: FilePath -> (String -> IO String) -> IO ()+inplace p f = do+ contents <- readFile p+ newContents <- f contents+ unless (null newContents) $+ writeFile p newContents++fancyError :: Either (ATSError String) ATS -> IO ATS+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)
+ src/Language/ATS/Lexer.x view
@@ -0,0 +1,267 @@+{++ {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns #-}+ {-# LANGUAGE DeriveGeneric #-}+ {-# LANGUAGE DeriveAnyClass #-}+ {-# LANGUAGE StandaloneDeriving #-}++ -- | Module exporting the lexer itself as well as several data types for+ -- working with tokens.+ module Language.ATS.Lexer ( AlexPosn (..)+ , Token (..)+ , Keyword (..)+ , Addendum (..)+ , lexATS+ , token_posn+ ) where++import Data.Char (toUpper)+import Control.Lens (over, _head)+import Control.DeepSeq (NFData)+import GHC.Generics (Generic)++}++%wrapper "posn"++-- Digits+$digit = 0-9++-- Characters+$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\:\,\.\\\#]+$alpha = [a-zA-Z]+$terminal = $printable # $white+$esc_char = \27+@escape_ch = \\ (n | t | \')+@escape_str = \\ (n | t | \")+@char = ($terminal # $special) | @escape_ch | $esc_char+@bool = (true | false)++@char_lit = \' @char \'++@time_lit = $digit+ u++-- Integer+@integer = $digit+++-- Floats+@decimals = $digit++@float = @decimals \. @decimals++-- Strings+@string = \" ($printable # [\"] | @escape_str | $esc_char | \n)* \"++-- Identifiers -- FIXME this is buggy (can identifiers start with '!'?)+@identifier = $alpha ($alpha | $digit | _ | !)*++@block_comment = \(\* ([^\)] | \n)* \*\) | \/\* ([^\)] | \n)* \*\/ -- FIXME should be able to do (* ) *)++@ref = "ref<"++@ref_call = @identifier "<" ($alpha | $digit | "(" | ")" | _)+ ">"++@c_block = \%\{\^ (. # [\%] | \n)* \%\} -- FIXME only exclude the real bad parts++@lambda = "=>" | "=<cloref1>" | "=<cloptr1>"++@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,prf>" | "-<>" | "-<prf>" -- FIXME allow spaces after comma?++@operator = "+" | "-" | "*" | "/" | "!=" | ">=" | "()" | "<=" | "=" | "~" | "&&" | "||" | ">" | "<" | "->" | ":=" | ".<" | ">." | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |++-- TODO make stuff more specific = better errors + better speed.++tokens :-++ $white+ ;+ "//".* ;+ @block_comment ;+ "#define".* { tok (\p s -> DefineBlock p s) } + @c_block { tok (\p s -> CBlockLex p s) }+ fun { tok (\p s -> Keyword p KwFun) }+ fnx { tok (\p s -> Keyword p KwFnx) }+ and { tok (\p s -> Keyword p KwAnd) }+ prval { tok (\p s -> Keyword p KwPrval) }+ 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) }+ 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) }+ absprop { tok (\p s -> Keyword p KwAbsprop) }+ llam { tok (\p s -> Keyword p KwLinearLambda) }+ lam { tok (\p s -> Keyword p KwLambda) }+ staload { tok (\p s -> Keyword p KwStaload) }+ let { tok (\p s -> Keyword p KwLet) }+ in { tok (\p s -> Keyword p KwIn) }+ end { tok (\p s -> Keyword p KwEnd) }+ case"+" { tok (\p s -> Keyword p (KwCase Plus)) }+ case"-" { tok (\p s -> Keyword p (KwCase Minus)) }+ case { tok (\p s -> Keyword p (KwCase None)) }+ castfn { tok (\p s -> Keyword p KwCastfn) }+ val"+" { tok (\p s -> Keyword p (KwVal Plus)) }+ val"-" { tok (\p s -> Keyword p (KwVal Minus)) }+ val { tok (\p s -> Keyword p (KwVal None)) }+ var { tok (\p s -> Keyword p KwVar) }+ int { tok (\p s -> Keyword p KwInt) }+ if { tok (\p s -> Keyword p KwIf) }+ sif { tok (\p s -> Keyword p KwSif) }+ then { tok (\p s -> Keyword p KwThen) }+ else { tok (\p s -> Keyword p KwElse) }+ string { tok (\p s -> Keyword p KwString) }+ bool { tok (\p s -> Keyword p KwBool) }+ void { tok (\p s -> Keyword p KwVoid) }+ nat { tok (\p s -> Keyword p KwNat) }+ implement { tok (\p s -> Keyword p KwImplement) }+ 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)) }+ abstype { tok (\p s -> Keyword p KwAbstype) }+ absvtype { 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) }+ of { tok (\p s -> Keyword p KwOf) }+ stadef { tok (\p s -> Keyword p KwStadef) }+ local { tok (\p s -> Keyword p KwLocal) }+ praxi { tok (\p s -> Keyword p KwPraxi) }+ while { tok (\p s -> Keyword p KwWhile) }+ where { tok (\p s -> Keyword p KwWhere) }+ begin { tok (\p s -> Keyword p KwBegin) }+ overload { tok (\p s -> Keyword p KwOverload) }+ 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) }+ @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)))}+ @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) }+ $special { tok (\p s -> Special p s) }+ @identifier { tok (\p s -> Identifier p s) }+ @string { tok (\p s -> StringTok p s) }++{++deriving instance Generic AlexPosn+deriving instance NFData AlexPosn++tok f p s = f p s++data Addendum = None+ | Plus+ | Minus+ deriving (Eq, Show, Generic, NFData)++data Keyword = KwFun+ | KwFnx+ | KwAnd+ | KwDatatype+ | KwDatavtype+ | KwDataviewtype+ | KwAssume+ | KwTypedef+ | KwVtypedef+ | KwStaload+ | KwLet+ | KwIn+ | KwLocal+ | KwEnd+ | KwImplement+ | KwCase Addendum+ | KwIf+ | KwSif+ | KwThen+ | KwElse+ | KwString+ | KwBool+ | KwInt+ | KwVoid+ | KwNat+ | KwVal Addendum+ | KwVar+ | KwLambda+ | KwLinearLambda+ | KwInclude+ | KwWhen+ | KwOf+ | KwAbsprop+ | KwPrval+ | KwStadef+ | KwPraxi+ | KwWhile+ | KwWhere+ | KwBegin+ | KwOverload+ | KwWith+ | KwChar+ | KwDataview+ | KwDataprop+ | KwView+ | KwAbstype+ | KwType+ | KwAbst0p Addendum+ | KwT0p Addendum+ | KwVt0p Addendum+ | KwPrfun+ | KwPrfn+ | KwCastfn+ | KwExtern+ | KwAbsvtype+ | KwProofImplement+ deriving (Eq, Show, Generic, NFData)++data Token = Semicolon AlexPosn+ | Identifier AlexPosn String+ | Keyword AlexPosn Keyword+ | BoolTok AlexPosn Bool+ | IntTok AlexPosn Int+ | FloatTok AlexPosn Float+ | CharTok AlexPosn Char+ | StringTok AlexPosn String+ | Special AlexPosn String+ | CBlockLex AlexPosn String+ | Operator AlexPosn String+ | Arrow AlexPosn String+ | FuncType AlexPosn String+ | CommentLex AlexPosn String+ | RefTok AlexPosn+ | DefineBlock AlexPosn String+ | TimeTok AlexPosn String+ 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+token_posn (IntTok p _) = p+token_posn (FloatTok p _) = p+token_posn (StringTok p _) = p+token_posn (Special p _) = p+token_posn (CBlockLex p _) = p+token_posn (Operator p _) = p+token_posn (Arrow p _) = p+token_posn (FuncType p _) = p+token_posn (CharTok p _) = p+token_posn (CommentLex p _) = p+token_posn (RefTok p) = p+token_posn (DefineBlock p _) = p+token_posn (TimeTok p _) = p++-- | This function turns a string into a stream of tokens for the parser.+lexATS :: String -> [Token]+lexATS = alexScanTokens++}
+ src/Language/ATS/Parser.y view
@@ -0,0 +1,376 @@+{+ {-# LANGUAGE OverloadedStrings #-}+ {-# LANGUAGE DeriveGeneric #-}+ {-# LANGUAGE DeriveAnyClass #-}++ -- | This module contains the parser.+ module Language.ATS.Parser ( parseATS+ , ATSError (..)+ ) where++import Language.ATS.Types++import Language.ATS.Lexer ( Token (..)+ , AlexPosn (..)+ , Keyword (..)+ , Addendum (..)+ , token_posn+ )++import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))++import Prelude++import Control.DeepSeq (NFData)++import GHC.Generics (Generic)++}++%name parseATS+%tokentype { Token }+%error { parseError }+%monad { Either (ATSError String) } { (>>=) } { pure }++%token+ fun { Keyword $$ KwFun }+ fnx { Keyword $$ KwFnx }+ and { Keyword $$ KwAnd }+ lambda { Keyword $$ KwLambda }+ llambda { Keyword $$ KwLinearLambda }+ if { Keyword $$ KwIf }+ stadef { Keyword $$ KwStadef }+ val { Keyword _ (KwVal $$) }+ prval { Keyword $$ KwPrval }+ var { Keyword $$ KwVar }+ then { Keyword $$ KwThen }+ let { Keyword $$ KwLet }+ typedef { Keyword $$ KwTypedef }+ vtypedef { Keyword $$ KwVtypedef }+ absvtype { Keyword $$ KwAbsvtype }+ in { Keyword $$ KwIn }+ end { Keyword $$ KwEnd }+ stringType { Keyword $$ KwString }+ charType { Keyword $$ KwChar }+ voidType { Keyword $$ KwVoid }+ implement { Keyword $$ KwImplement }+ primplmnt { Keyword $$ KwProofImplement }+ else { Keyword $$ KwElse }+ bool { Keyword $$ KwBool }+ int { Keyword $$ KwInt }+ nat { Keyword $$ KwNat }+ when { Keyword $$ KwWhen }+ begin { Keyword $$ KwBegin }+ case { Keyword _ (KwCase $$) }+ datatype { Keyword $$ KwDatatype }+ datavtype { Keyword $$ KwDatavtype }+ while { Keyword $$ KwWhile }+ of { Keyword $$ KwOf }+ include { Keyword $$ KwInclude }+ staload { Keyword $$ KwStaload }+ overload { Keyword $$ KwOverload }+ with { Keyword $$ KwWith }+ dataprop { Keyword $$ KwDataprop }+ praxi { Keyword $$ KwPraxi }+ extern { Keyword $$ KwExtern }+ t0pPlain { Keyword $$ (KwT0p None) }+ vt0pCo { Keyword $$ (KwVt0p Plus) }+ where { Keyword $$ KwWhere }+ absprop { Keyword $$ KwAbsprop }+ boolLit { BoolTok _ $$ }+ timeLit { TimeTok _ $$ }+ intLit { IntTok _ $$ }+ floatLit { FloatTok _ $$ }+ identifier { Identifier _ $$ }+ closeParen { Special $$ ")" }+ openParen { Special $$ "(" }+ colon { Special $$ ":" }+ comma { Special $$ "," }+ geq { Operator $$ ">=" }+ leq { Operator $$ "<=" }+ neq { Operator $$ "!=" }+ openTermetric { Operator $$ ".<" }+ closeTermetric { Operator $$ ">." }+ mutateArrow { Operator $$ "->" }+ mutateEq { Operator $$ ":=" }+ lbracket { Operator $$ "<" }+ rbracket { Operator $$ ">" }+ eq { Operator $$ "=" }+ or { Operator $$ "||" }+ vbar { Special $$ "|" }+ lbrace { Special $$ "{" }+ rbrace { Special $$ "}" }+ plainArrow { Arrow $$ "=>" }+ cloref1Arrow { Arrow $$ "=<cloref1>" }+ cloptr1Arrow { Arrow $$ "=<cloptr1>" }+ lsqbracket { Special $$ "[" }+ rsqbracket { Special $$ "]" }+ string { StringTok _ $$ }+ charLit { CharTok _ $$ }+ underscore { Special $$ "_" }+ minus { Operator $$ "-" }+ plus { Operator $$ "+" }+ div { Operator $$ "/" }+ mult { Operator $$ "*" }+ exclamation { Special $$ "!" }+ dot { Special $$ "." }+ at { Special $$ "@" }+ tilde { Operator $$ "~" }+ dollar { Special $$ "$" }+ semicolon { Special $$ ";" }+ andOp { Operator $$ "&&" }+ doubleParens { Operator $$ "()" }+ prfTransform { Operator $$ ">>" } -- For types like &a >> a?!+ refType { Special $$ "&" } -- For types like &a+ maybeProof { Operator $$ "?" } -- For types like a?+ fromVT { Operator $$ "?!" } -- For types like a?!+ openExistential { Operator $$ "#[" } -- Same as `[` in ATS2+ cblock { CBlockLex _ $$ }+ ref { RefTok $$ }+ define { DefineBlock _ $$ }++%%++ATS : { ATS [] }+ | ATS Declaration { ATS ($2 : (\(ATS x) -> x) $1) }++TypeIn : Type { [$1] }+ | TypeIn comma Type { $3 : $1 }++TypeInExpr : TypeIn { $1 }+ | Expression { [ConcreteType $1] }+ | TypeInExpr comma PreExpression { ConcreteType $3 : $1 }++Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 }+ | bool { Bool }+ | int { Int }+ | nat { Nat }+ | stringType { String }+ | charType { Char }+ | voidType { Void }+ | t0pPlain { T0p None }+ | vt0pCo { Vt0p Plus }+ | stringType openParen Expression closeParen { DepString $3 }+ | stringType Expression { DepString $2 }+ | int openParen Expression closeParen { DependentInt $3 }+ | bool openParen Expression closeParen { DependentBool $3 }+ | identifier { Named $1 }+ | int Expression { DependentInt $2 }+ | exclamation Type { Unconsumed $2 }+ | 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 }+ | 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 [] }+ | 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.++Literal : boolLit { BoolLit $1 }+ | timeLit { TimeLit $1 }+ | intLit { IntLit $1 }+ | floatLit { FloatLit $1 }+ | string { StringLit (init . drop 1 $ $1) }+ | charLit { CharLit $1 }++PatternIn : Pattern { [$1] }+ | PatternIn comma Pattern { $3 : $1 }++Pattern : doubleParens { NullPattern $1 }+ | identifier { PName $1 [] }+ | underscore { Wildcard $1 }+ | identifier doubleParens { PName ($1 ++ "()") [] }+ | tilde Pattern { Free $2 }+ | identifier openParen PatternIn closeParen { PName $1 $3 }+ | identifier Pattern { PSum $1 $2 }+ | openParen Pattern vbar Pattern closeParen { Proof $1 $2 $4 }+ | openParen PatternIn closeParen { TuplePattern $2 }+ | Literal { PLiteral $1 }+ | Pattern when Expression { Guarded $2 $3 $1 }++Case : { [] }+ | Case vbar Pattern LambdaArrow Expression { ($3, $5) : $1 }++ExpressionIn : Expression { [$1] }+ | ExpressionIn comma Expression { $3 : $1 }++TupleExpression : PreExpression comma PreExpression { [$3, $1] }+ | TupleExpression comma PreExpression { $3 : $1 }++LambdaArrow : plainArrow { Plain $1 }+ | cloref1Arrow { Full $1 "cloref1" }+ | cloptr1Arrow { Full $1 "cloptr1" }++Expression : PreExpression { $1 }+ | Name PreExpression { Call $1 [] [] [$2] }+ | openParen TupleExpression closeParen { TupleEx $1 $2 }++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 [] [] }+ | 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 }+ | 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) }+ | PreExpression semicolon PreExpression { Precede $1 $3 }+ | PreExpression semicolon { $1 }+ | exclamation PreExpression { Deref $1 $2 }+ | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 $3 $5 }+ | ref Type rbracket PreExpression { Ref $1 $2 $4 }+ | PreExpression where lbrace Declaration rbrace { WhereExp $1 $4 }+ | PreExpression colon Type { TypeSignature $1 $3 }+ | Name { NamedVal $1 }+ | lbrace ATS rbrace { Actions $2 }+ | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }+ | include {% Left $ Expected $1 "Expression" "include" }+ | staload {% Left $ Expected $1 "Expression" "staload" }+ | overload {% Left $ Expected $1 "Expression" "overload" }+ | prval {% Left $ Expected $1 "Expression" "prval" }+ | var {% Left $ Expected $1 "Expression" "var" }+ | Termetric {% Left $ Expected (fst $1) "Expression" "termetric" }++Termetric : openTermetric Expression closeTermetric { ($1, $2) }++Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) }+ | lsqbracket Args rsqbracket { Existential $2 Nothing Nothing }+ | openExistential Args rsqbracket { Existential $2 Nothing Nothing }+ | openExistential Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) }+ | lsqbracket Args colon Type rsqbracket { Existential $2 (Just $4) Nothing }+ | 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 }++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 }++Name : identifier { Unqualified $1 }+ | dollar identifier dot identifier { Qualified $1 $4 $2 }++RecordVal : identifier eq Expression { [($1, $3)] }+ | RecordVal comma identifier eq Expression { ($3, $5) : $1 }++Records : identifier eq Type { [ ($1, $3) ] }+ | Records comma identifier eq Type { ($3, $5) : $1 }++SumLeaf : vbar identifier { ($2, Nothing) }+ | vbar identifier of Type { ($2, Just $4) }++Leaves : SumLeaf { [$1] }+ | Leaves SumLeaf { $2 : $1 }++Universals : { [] }+ | Universals Universal { $2 : $1 }++OptTermetric : { Nothing }+ | Termetric { Just (snd $1) }++UnOp : tilde { Negate }++BinOp : plus { Add }+ | minus { Sub }+ | div { Div }+ | mult { Mult }+ | geq { GreaterThanEq }+ | leq { LessThanEq }+ | lbracket { LessThan }+ | rbracket { GreaterThan }+ | eq { Equal }+ | neq { NotEqual }+ | andOp { LogicalAnd }+ | or { LogicalOr }++OptExpression : { Nothing }+ | eq Expression { Just $2 }++DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 }++DataPropLeaves : { [] }+ | 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 }++Declaration : include string { Include $2 }+ | staload underscore eq string { Staload (Just "_") $4 } -- FIXME+ | 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 }+ | 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 }+ | prval Pattern eq PreExpression { PrVal $2 $4 }+ | praxi PreFunction { Func $1 (Praxi $2) }+ | implement Implementation { Impl $2 }+ | primplmnt Implementation { ProofImpl $2 }+ | overload BinOp with Name { OverloadOp $1 $2 $4 }+ | stadef identifier eq Name { Stadef $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 }+ | datavtype identifier eq Leaves { SumViewType $2 $4 }+ | absvtype identifier openParen Args closeParen eq Type { AbsViewType $1 $2 $4 $7 }+ | datatype identifier eq Leaves { SumType $2 $4 }+ | dataprop identifier openParen Args closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }+ | define { Define $1 }+ | cblock { CBlock $1 }+ | lambda {% Left $ Expected $1 "Declaration" "lam" }+ | llambda {% Left $ Expected $1 "Declaration" "llam" }+ | ref {% Left $ Expected $1 "Declaration" "ref" }++{++data ATSError a = Expected AlexPosn a a+ | Unknown AlexPosn+ deriving (Eq, Show, Generic, NFData)++instance Pretty AlexPosn where+ 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 (Unknown p) = red "Error:" <+> "unknown" <+> pretty p <> linebreak++parseError :: [Token] -> Either (ATSError String) a+parseError = Left . Unknown . token_posn . head +}
+ src/Language/ATS/PrettyPrint.hs view
@@ -0,0 +1,343 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.ATS.PrettyPrint ( printATS+ , printATSCustom+ , processClang+ ) where++import Control.Arrow hiding ((<+>))+import Control.Composition+import Control.DeepSeq (NFData)+import Data.Function (on)+import Data.Functor.Foldable (cata)+import GHC.Generics (Generic)+import Language.ATS.Types+import Prelude hiding ((<$>))+import System.Console.ANSI.Types+import System.Process (readCreateProcess, shell)+import Text.PrettyPrint.ANSI.Leijen+import Text.PrettyPrint.ANSI.Leijen.Internal++deriving instance Generic Underlining+deriving instance NFData Underlining+deriving instance Generic ConsoleIntensity+deriving instance NFData ConsoleIntensity+deriving instance Generic Color+deriving instance NFData Color+deriving instance Generic ColorIntensity+deriving instance NFData ColorIntensity+deriving instance Generic ConsoleLayer+deriving instance NFData ConsoleLayer+deriving instance Generic Doc+deriving instance NFData Doc++instance Eq Doc where+ (==) = on (==) show++processClang :: String -> IO String+processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs)+ where+ takeBlock :: String -> (String, String)+ takeBlock ('%':'}':ys) = ("", ('%':) . ('}':) $ ys)+ takeBlock (y:ys) = first (y:) $ takeBlock ys+ takeBlock [] = ([], [])+processClang (x:xs) = fmap (x:) $ processClang xs+processClang [] = pure []++printClang :: String -> IO String+printClang = readCreateProcess (shell "clang-format")++printATS :: ATS -> String+printATS (ATS x) = g mempty+ where g = (displayS . renderPretty 0.6 120 . pretty) (ATS $ reverse x)++printATSCustom :: Float -> Int -> ATS -> String+printATSCustom r i (ATS x) = g mempty+ where g = (displayS . renderPretty r i . pretty) (ATS $ reverse x)+++instance Pretty Name where+ pretty (Unqualified n) = string n+ pretty (Qualified _ i n) = "$" <> string n <> "." <> string i++instance Pretty LambdaType where+ pretty Plain{} = "=>"+ pretty (Full _ v) = "=<" <> string v <> ">"++instance Pretty BinOp where+ pretty Mult = "*"+ pretty Add = "+"+ pretty Div = "/"+ pretty Sub = "-"+ pretty GreaterThan = ">"+ pretty LessThan = "<"+ pretty Equal = "="+ pretty NotEqual = "!="+ pretty LogicalAnd = "&&"+ pretty LogicalOr = "||"+ pretty LessThanEq = "<="+ pretty GreaterThanEq = ">="++splits :: BinOp -> Bool+splits Mult = True+splits Add = True+splits Div = True+splits Sub = True+splits LogicalAnd = True+splits LogicalOr = True+splits _ = False++instance Pretty Addendum where+ pretty Plus = "+"+ pretty Minus = "-"+ pretty None = ""++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 (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 (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 (WhileF _ e e') = "while" <> parens e <> e'+ a (ActionsF as) = "{" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) as)) <$> "}"+ prettyCases [] = mempty+ prettyCases [(s, t)] = "|" <+> pretty s <+> "=>" <+> t+ prettyCases ((s, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> "=>" <+> t++noParens :: Doc -> Bool+noParens = all (`notElem` ("()" :: String)) . show++instance Pretty Pattern where+ pretty = cata a where+ a (WildcardF _) = "_"+ a (PSumF s x) = string s <+> x+ a (PLiteralF e) = pretty e+ a (PNameF s []) = string s+ a (PNameF s [x]) = string s <> parens x+ a (PNameF s ps) = string s <> parens (mconcat (punctuate ", " (reverse ps)))+ a (FreeF p) = "~" <> p+ a (GuardedF _ e p) = p <+> "when" <+> pretty e+ a (ProofF _ p p') = parens (p <+> "|" <+> p')+ a NullPatternF{} = "()"+ a (TuplePatternF ps) = parens (mconcat (punctuate ", " (reverse ps)))++instance Pretty Arg where+ pretty (Arg s Nothing) = pretty s+ pretty (Arg "" (Just t)) = pretty t+ pretty (Arg s (Just t)) = pretty s <+> colon <+> pretty t++instance Pretty Type where+ pretty = cata a where+ a IntF = "int"+ a StringF = "string"+ a BoolF = "bool"+ a VoidF = "void"+ a NatF = "nat"+ a CharF = "char"+ a (NamedF n) = string n+ a (ExF e t) = pretty e <+> t+ a (DependentIntF e) = "int(" <> pretty e <> ")"+ a (DependentBoolF e) = "bool(" <> pretty e <> ")"+ a (DepStringF e) = "string(" <> pretty e <> ")"+ a (DependentF n ts) = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))+ a DoubleF = "double"+ a FloatF = "float"+ a (ForAF u t) = pretty u <+> t+ a (UnconsumedF t) = "!" <> t+ a (AsProofF t (Just t')) = t <+> ">>" <+> t'+ a (AsProofF t Nothing) = t <+> ">> _"+ a (FromVTF t) = t <> "?!"+ a (MaybeValF t) = t <> "?"+ a (T0pF ad) = "t@ype" <> pretty ad+ a (Vt0pF ad) = "vt@ype" <> pretty ad+ a (AtF _ t t') = t <> "@" <> t'+ a (ProofTypeF _ t t') = parens (t <+> "|" <+> t')+ a (ConcreteTypeF e) = pretty e+ a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))+ a (RefTypeF t) = "&" <> t+ a (AbsPropF _ n as) = "absprop" <+> string n <+> prettyArgs as++gan :: Maybe Type -> Doc+gan (Just t) = " : " <> pretty t <> " "+gan Nothing = ""++instance Pretty Existential where+ pretty (Existential [] Nothing (Just e)) = lbracket <+> pretty e <+> rbracket+ pretty (Existential bs ty Nothing) = lbracket <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket+ pretty (Existential bs ty (Just e)) = lbracket <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket+ where go (Arg s Nothing) = pretty s+ go (Arg s (Just t)) = pretty s <+> colon <+> pretty t++instance Pretty Universal where+ pretty (Universal [x] Nothing Nothing) = lbrace <> pretty x <> rbrace+ pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbrace+ pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace+ where go (Arg s Nothing) = pretty s+ go (Arg s (Just t)) = pretty s <+> colon <+> pretty t++instance Pretty ATS where+ pretty (ATS xs) = concatSame xs++instance Pretty Implementation where+ pretty (Implement _ [] [] n [] e) = "implement" <+> pretty n <+> "() =" <$> indent 2 (pretty e)+ pretty (Implement _ [] [] n ias e) = "implement" <+> pretty n <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)+ pretty (Implement _ [] us n ias e) = "implement" <+> pretty n <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)+ pretty (Implement _ ps [] n ias e) = "implement" <+> foldMap pretty ps </> pretty n <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)+ pretty (Implement _ ps us n ias e) = "implement" <+> foldMap pretty ps </> pretty n </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)++glue :: Declaration -> Declaration -> Bool+glue Staload{} Staload{} = True+glue Include{} Include{} = True+glue (Func _ Fnx{}) (Func _ And{}) = True+glue _ _ = False++repulse :: Declaration -> Declaration -> Bool+repulse Impl{} Impl{} = True+repulse Extern{} Impl{} = True+repulse _ Extern{} = True+repulse _ _ = False++{-# INLINE glue #-}++concatSame :: [Declaration] -> Doc+concatSame [] = mempty+concatSame [x] = pretty x+concatSame (x:x':xs)+ | glue x x' = pretty x <> concatSame (x':xs)+ | repulse x x' = pretty x <> line <$> concatSame (x':xs)+ | otherwise = pretty x <$> concatSame (x':xs)++-- TODO - soft break+($$) :: Doc -> Doc -> Doc+x $$ y = align (x <$> y)++prettyRecord :: (Pretty a) => [(String, a)] -> Doc+prettyRecord es = group (flatAlt (prettyRecordF True es) (prettyRecordS True es))++prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc+prettyRecordS _ [] = mempty+prettyRecordS True [(s, t)] = "@{" <+> string s <+> "=" <+> pretty t <+> "}"+prettyRecordS _ [(s, t)] = "@{" <+> string s <+> "=" <+> pretty t+prettyRecordS True ((s, t):xs) = prettyRecordS False xs <> ("," <+> string s <+> "=" <+> pretty t <+> "}")+prettyRecordS x ((s, t):xs) = prettyRecordS x xs <> ("," <+> string s <+> "=" <+> pretty t)++prettyRecordF :: (Pretty a) => Bool -> [(String, a)] -> Doc+prettyRecordF _ [] = mempty+prettyRecordF True [(s, t)] = "@{" <+> string s <+> "=" <+> pretty t <+> "}"+prettyRecordF _ [(s, t)] = "@{" <+> string s <+> "=" <+> pretty t+prettyRecordF True ((s, t):xs) = prettyRecordF False xs $$ indent 1 ("," <+> string s <+> "=" <+> pretty t <$> "}")+prettyRecordF x ((s, t):xs) = prettyRecordF x xs $$ indent 1 ("," <+> string s <+> "=" <+> pretty t)++prettyDL :: [DataPropLeaf] -> Doc+prettyDL [] = mempty+prettyDL [DataPropLeaf us e] = indent 2 ("|" <+> foldMap pretty us <+> pretty e)+prettyDL (DataPropLeaf us e:xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e)++prettyLeaf :: [(String, Maybe Type)] -> Doc+prettyLeaf [] = mempty+prettyLeaf [(s, Nothing)] = indent 2 ("|" <+> string s)+prettyLeaf [(s, Just e)] = indent 2 ("|" <+> string s <+> "of" <+> pretty e)+prettyLeaf ((s, Nothing):xs) = prettyLeaf xs $$ indent 2 ("|" <+> string s)+prettyLeaf ((s, Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> string s <+> "of" <+> pretty e)++prettyArgsG :: Doc -> Doc -> [Doc] -> Doc+prettyArgsG c1 c2 = (c1 <>) . align . indent (-1) . cat . (<> pure c2) . go . reverse -- TODO when it's only one arg, don't split ( off+ where go :: [Doc] -> [Doc]+ go [x] = [x]+ go (x:xs) = flatAlt (" " <> x) x : fmap (", " <>) xs+ go x = x++prettyArgs' :: (Pretty a) => Doc -> Doc -> [a] -> Doc+prettyArgs' = fmap pretty -.** prettyArgsG -- -.** fmap pretty++prettyArgs :: (Pretty a) => [a] -> Doc+prettyArgs = prettyArgs' "(" ")"++fancyU :: [Universal] -> Doc+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 _ = "FIXME"++instance Pretty DataPropLeaf where+ pretty (DataPropLeaf us e) = "|" <+> foldMap pretty (reverse us) <+> pretty e++instance Pretty Declaration where+ pretty (RecordType s rs) = "typedef" <+> string s <+> "=" <+> prettyRecord rs <> line+ pretty (SumViewType s ls) = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls+ pretty (SumType s ls) = "datatype" <+> string s <+> "=" <$> prettyLeaf ls+ pretty (Impl i) = pretty i+ 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+ pretty (Var Nothing p e) = "var" <+> pretty p <+> "=" <+> pretty e+ pretty (Var (Just t) p e) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e+ pretty (Include s) = "#include" <+> pretty s <> line+ pretty (Staload Nothing s) = "staload" <+> pretty s <> line+ pretty (Staload (Just q) s) = "staload" <+> pretty q <+> "=" <+> pretty s <> line+ pretty (CBlock s) = string s <> line+ pretty (Comment s) = string s+ pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n <> linebreak+ pretty (Func _ (Fun pref)) = "fun" </> pretty pref+ 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 (Define s) = string s+ pretty (DataProp _ s as ls) = "dataprop" <+> string s <> prettyArgs as <+> "=" <$> prettyDL ls+ pretty _ = mempty
+ src/Language/ATS/Types.hs view
@@ -0,0 +1,233 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}++-- | This is a module containing types to model the ATS syntax tree. As it is+-- collapsed by the pretty printer, you may see that in some places it is+-- focused on the lexical side of things.+module Language.ATS.Types+ ( ATS (..)+ , Declaration (..)+ , Type (..)+ , Name (..)+ , Pattern (..)+ , PatternF (..)+ , Arg (..)+ , Universal (..)+ , Function (..)+ , Expression (..)+ , ExpressionF (..)+ , Implementation (..)+ , BinOp (..)+ , UnOp (..)+ , TypeF (..)+ , Existential (..)+ , LambdaType (..)+ , Addendum (..)+ , DataPropLeaf (..)+ , PreFunction (..)+ ) where++import Control.DeepSeq (NFData)+import Data.Functor.Foldable.TH (makeBaseFunctor)+import GHC.Generics (Generic)+import Language.ATS.Lexer (Addendum (..), AlexPosn)++-- | Newtype wrapper containing a list of declarations+newtype ATS = ATS { unATS :: [Declaration] }+ deriving (Show, Eq, Generic, NFData)++-- | 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+ | PrVal Pattern Expression+ | Var (Maybe Type) Pattern Expression -- TODO can a `var` really appear anywhere in top-level declarations+ | AndDecl (Maybe Type) Pattern Expression+ | Include String+ | Staload (Maybe String) String+ | Stadef String Name+ | CBlock String+ | RecordType String [(String, Type)]+ | RecordViewType String Type+ | SumType String [(String, Maybe Type)]+ | SumViewType String [(String, Maybe Type)]+ | AbsViewType AlexPosn String [Arg] Type+ | OverloadOp AlexPosn BinOp Name+ | Comment String+ | DataProp AlexPosn String [Arg] [DataPropLeaf]+ | Extern AlexPosn Declaration+ | Define String+ deriving (Show, Eq, Generic, NFData)++data DataPropLeaf = DataPropLeaf [Universal] Expression+ deriving (Show, Eq, Generic, NFData)++-- | A type for parsed ATS types+data Type = Bool+ | Void+ | String+ | Char+ | Int+ | Nat+ | DependentInt Expression+ | DependentBool Expression+ | DepString Expression+ | Double+ | Float+ | Tuple AlexPosn [Type]+ | Named String+ | Ex Existential Type+ | ForA Universal Type+ | Dependent Name [Type]+ | Unconsumed Type -- !a+ | AsProof Type (Maybe Type) -- a >> b+ | FromVT Type -- For a viewtype VT, we can prove there exist a view V and type T such that `VT` is equivalent to `(V | T)` - that T is `VT?!`+ | MaybeVal Type -- This is just `a?` or the like+ | T0p Addendum -- t@ype+ | Vt0p Addendum -- vt@ype+ | At AlexPosn Type Type+ | ProofType AlexPosn Type Type -- Aka (prf | val)+ | ConcreteType Expression+ | RefType Type+ | AbsProp AlexPosn String [Arg]+ deriving (Show, Eq, Generic, NFData)++-- | A type for the various lambda arrows (`=>`, `=<cloref1>`, etc.)+data LambdaType = Plain AlexPosn+ | Full AlexPosn String+ deriving (Show, Eq, Generic, NFData)++-- | A name can be qualified (`$UN.unsafefn`) or not+data Name = Unqualified String+ | Qualified AlexPosn String String+ deriving (Show, Eq, Generic, NFData)++-- | A data type for patterns.+data Pattern = Wildcard AlexPosn+ | PName String [Pattern]+ | PSum String Pattern+ | PLiteral Expression+ | Guarded AlexPosn Expression Pattern+ | Free Pattern+ | Proof AlexPosn Pattern Pattern+ | NullPattern AlexPosn+ | TuplePattern [Pattern]+ deriving (Show, Eq, Generic, NFData)++-- | An argument to a function.+data Arg = Arg String (Maybe Type)+ deriving (Show, Eq, Generic, NFData)++-- | Wrapper for universal quantifiers (refinement types)+data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe Expression }+ deriving (Show, Eq, Generic, NFData)++-- | Wrapper for existential quantifiers/types+data Existential = Existential { boundE :: [Arg], typeE :: Maybe Type, propE :: Maybe Expression } -- TODO #[id:int] existentials+ deriving (Show, Eq, Generic, NFData)++-- | `~` is used to negate numbers in ATS+data UnOp = Negate+ deriving (Show, Eq, Generic, NFData)++-- | Binary operators on expressions+data BinOp = Add+ | Mult+ | Div+ | Sub+ | GreaterThan+ | GreaterThanEq+ | LessThan+ | LessThanEq+ | Equal+ | NotEqual+ | LogicalAnd+ | LogicalOr+ deriving (Show, Eq, Generic, NFData)++-- | A (possibly effectful) expression.+data Expression = Let AlexPosn ATS Expression+ | Begin ATS+ | Local ATS+ | VoidLiteral -- The '()' literal representing inaction.+ AlexPosn+ | Call Name [Expression] [Type] [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+ }+ | Sif { cond :: Expression, whenTrue :: Expression, elseExpr :: Expression }+ | BoolLit Bool+ | TimeLit String+ | FloatLit Float+ | IntLit Int+ | Lambda AlexPosn LambdaType Pattern Expression+ | LinearLambda AlexPosn LambdaType Pattern Expression+ | Index AlexPosn Name Expression+ | Access AlexPosn Expression Name+ | StringLit String+ | CharLit Char+ | Binary BinOp Expression Expression+ | Unary UnOp Expression+ | Case { posE :: AlexPosn+ , kind :: Addendum+ , val :: Expression+ , arms :: [(Pattern, Expression)] -- ^ Each `(Pattern, Expression)` pair corresponds to a branch of the 'case' statement+ }+ | RecordValue AlexPosn [(String, Expression)] (Maybe Type)+ | Precede Expression Expression+ | FieldMutate { posE :: AlexPosn+ , old :: Expression -- ^ Record to modify+ , field :: String -- ^ Field being modified+ , new :: Expression -- ^ New value of the field+ }+ | Deref AlexPosn Expression+ | Ref AlexPosn Type Expression+ | ProofExpr AlexPosn Expression Expression+ | TypeSignature Expression Type+ | WhereExp Expression Declaration+ | TupleEx AlexPosn [Expression]+ | While AlexPosn Expression Expression+ | Actions ATS+ deriving (Show, Eq, Generic, NFData)++-- | An 'implement' declaration+data Implementation = Implement { pos :: AlexPosn+ , preUniversalsI :: [Universal]+ , universalsI :: [Universal] -- ^ Universal quantifiers+ , nameI :: Name -- ^ Name of the template being implemented+ , iArgs :: [Arg] -- ^ Arguments+ , iExpression :: Expression -- ^ Expression holding the function body.+ }+ deriving (Show, Eq, Generic, NFData)++-- | A function declaration accounting for all three keywords (???) ATS uses to+-- define them.+data Function = Fun PreFunction+ | Fnx PreFunction+ | And PreFunction+ | PrFun PreFunction+ | PrFn PreFunction+ | Praxi PreFunction+ deriving (Show, Eq, Generic, NFData)++data PreFunction = PreF { fname :: String -- ^ Function name+ , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic+ , universals :: [Universal] -- ^ Universal quantifiers/refinement type+ , args :: [Arg] -- ^ Actual function arguments+ , returnType :: Type -- ^ Return type+ , termetric :: Maybe Expression -- ^ Optional termination metric+ , expression :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)+ }+ deriving (Show, Eq, Generic, NFData)++makeBaseFunctor ''Pattern+makeBaseFunctor ''Expression+makeBaseFunctor ''Type
+ stack.yaml view
@@ -0,0 +1,12 @@+---+resolver: nightly-2017-12-07+packages:+ - '.'+extra-deps:+ - ansi-wl-pprint-0.6.8.1+ - htoml-megaparsec-1.0.1.11+ - composition-prelude-0.1.1.1+flags:+ ats-format:+ development: false+extra-package-dbs: []
+ test/Spec.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE OverloadedStrings #-}++import Language.ATS.Lexer (lexATS)+import Language.ATS.Parser (parseATS)+import Language.ATS.PrettyPrint (printATS)+import Test.Hspec++main :: IO ()+main = hspec $+ describe "pretty" $ do+ parallel $ it "works on fib.dats" $ do+ sample <- readFile "test/data/fib.dats"+ expected <- readFile "test/data/fib.out"+ (fmap printATS . parseATS . lexATS) sample `shouldBe` Right expected+ parallel $ it "works on filecount.dats" $ do+ sample <- readFile "test/data/filecount.dats"+ expected <- readFile "test/data/filecount.out"+ (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected+ parallel $ it "works on filetype.sats" $ do+ sample <- readFile "test/data/filetype.sats"+ expected <- readFile "test/data/filetype.out"+ (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected+ parallel $ it "works on polyglot.dats" $ do+ sample <- readFile "test/data/polyglot.dats"+ expected <- readFile "test/data/polyglot.out"+ (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected+ parallel $ it "works on left-pad.dats" $ do+ sample <- readFile "test/data/left-pad.dats"+ expected <- readFile "test/data/left-pad.out"+ (fmap ((++ "\n") . printATS) . parseATS . lexATS) sample `shouldBe` Right expected