ats-format 0.2.0.2 → 0.2.0.4

raw patch · 39 files changed

+30/−7633 lines, 39 filesdep +language-atsdep −ansi-terminaldep −arraydep −criteriondep ~ansi-wl-pprintdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: language-ats

Dependencies removed: ansi-terminal, array, criterion, deepseq, hspec, hspec-dirstream, lens, recursion-schemes, system-filepath

Dependency ranges changed: ansi-wl-pprint, base

API changes (from Hackage documentation)

Files

• app/Main.hs +1/−1
• ats-format.cabal +6/−48
• bench/Bench.hs +0/−20
• src/Language/ATS.hs +0/−57
• src/Language/ATS/Exec.hs +22/−4
• src/Language/ATS/Lexer.x +0/−491
• src/Language/ATS/Parser.y +0/−697
• src/Language/ATS/PrettyPrint.hs +0/−547
• src/Language/ATS/Types.hs +0/−361
• stack.yaml +1/−0
• test/Spec.hs +0/−14
• test/data/combinatorics.dats +0/−40
• test/data/combinatorics.out +0/−43
• test/data/concurrency.dats +0/−257
• test/data/concurrency.out +0/−287
• test/data/fact.dats +0/−32
• test/data/fact.out +0/−39
• test/data/factorial.dats +0/−4
• test/data/factorial.out +0/−4
• test/data/fast-combinatorics.dats +0/−93
• test/data/fast-combinatorics.out +0/−94
• test/data/fib.dats +0/−6
• test/data/fib.out +0/−6
• test/data/filecount.dats +0/−31
• test/data/filecount.out +0/−41
• test/data/filetype.out +0/−180
• test/data/filetype.sats +0/−180
• test/data/left-pad.dats +0/−98
• test/data/left-pad.out +0/−76
• test/data/number-theory.dats +0/−167
• test/data/number-theory.out +0/−186
• test/data/numerics.dats +0/−61
• test/data/numerics.out +0/−63
• test/data/polyglot.dats +0/−1235
• test/data/polyglot.out +0/−1619
• test/data/toml-parse.dats +0/−244
• test/data/toml-parse.out +0/−260
• test/data/types.out +0/−24
• test/data/types.sats +0/−23

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

@@ -1,5 +1,5 @@ name:                ats-format-version:             0.2.0.2+version:             0.2.0.4 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@@ -14,9 +14,6 @@ data-files:          .travis.yml                    , appveyor.yml                    , Justfile-                   , test/data/*.dats-                   , test/data/*.sats-                   , test/data/*.out extra-source-files:  stack.yaml                    , cabal.project.local                    , .atsfmt.toml@@ -41,26 +38,17 @@  library   hs-source-dirs:      src-  exposed-modules:     Language.ATS-  other-modules:       Language.ATS.Types-                     , Language.ATS.Lexer-                     , Language.ATS.Parser-                     , Language.ATS.PrettyPrint-                     , Language.ATS.Exec-                     , Paths_ats_format+  exposed-modules:     Language.ATS.Exec+  other-modules:       Paths_ats_format   build-depends:       base >= 4.10 && < 5-                     , array-                     , lens-                     , deepseq-                     , ansi-wl-pprint >= 0.6.8-                     , recursion-schemes+                     , language-ats                      , optparse-applicative-                     , ansi-terminal                      , composition-prelude >= 0.1.1.2                      , htoml-megaparsec >= 1.1.0.0-                     , unordered-containers                      , text+                     , ansi-wl-pprint                      , directory+                     , unordered-containers                      , process                      , file-embed   build-tools:         happy@@ -85,36 +73,6 @@   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-                     , hspec-dirstream-                     , system-filepath-  if flag(development)-    ghc-options:       -Werror-  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 flag(development)-    ghc-options:       -Werror-  if impl(ghc >= 8.0)-    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat-  default-language:    Haskell2010  source-repository head   type:     git

@@ -1,20 +0,0 @@-module Main where--import           Criterion.Main-import           Language.ATS--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/toml-parse.dats"-          envFiles = (,) <$> large <*> medium

@@ -1,57 +0,0 @@--- | Main module for the library-module Language.ATS ( -- * Functions for working with syntax-                      lexATS-                    , parseATS-                    , printATS-                    , printATSCustom-                    , printATSFast-                    -- * Library functions-                    , getDependencies-                    -- * Syntax Tree-                    , ATS (..)-                    , Declaration (..)-                    , Expression (..)-                    , Type (..)-                    , Function (..)-                    , Implementation (..)-                    , Pattern (..)-                    , Name (..)-                    , UnOp (..)-                    , BinOp (..)-                    , DataPropLeaf (..)-                    , Leaf (..)-                    , Arg (..)-                    , Addendum (..)-                    , LambdaType (..)-                    , Universal (..)-                    , Existential (..)-                    , PreFunction (..)-                    , StaticExpression (..)-                    , Paired (..)-                    , Fixity (..)-                    -- * Lexical types-                    , Token (..)-                    , AlexPosn (..)-                    , Keyword (..)-                    -- * Error types-                    , ATSError-                    -- * Lenses-                    , leaves-                    , constructorUniversals-                    -- * Library functions-                    -- * Executable-                    , exec-                    ) where--import           Data.Maybe               (catMaybes)-import           Language.ATS.Exec-import           Language.ATS.Lexer-import           Language.ATS.Parser-import           Language.ATS.PrettyPrint-import           Language.ATS.Types--getDependencies :: ATS -> [FilePath]-getDependencies (ATS ds) = catMaybes (g <$> ds)-    where g (Staload _ s) = Just s-          g (Include s)   = Just s-          g _             = Nothing

@@ -4,6 +4,7 @@ module Language.ATS.Exec ( exec                          ) where +import Control.Arrow hiding ((<+>)) import           Control.Monad                (unless, (<=<)) import           Data.FileEmbed               (embedStringFile) import qualified Data.HashMap.Lazy            as HM@@ -11,10 +12,7 @@ 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           Language.ATS import           Options.Applicative import           Paths_ats_format import           System.Directory             (doesFileExist)@@ -23,8 +21,28 @@ import           Text.PrettyPrint.ANSI.Leijen (pretty) import           Text.Toml import           Text.Toml.Types              hiding (Parser)+import           System.Process                        (readCreateProcess, shell)  data Program = Program { _path :: Maybe FilePath, _inplace :: Bool, _noConfig :: Bool, _defaultConfig :: Bool }++takeBlock :: String -> (String, String)+takeBlock ('%':'}':ys) = ("", ('%':) . ('}':) $ ys)+takeBlock (y:ys)       = first (y:) $ takeBlock ys+takeBlock []           = ([], [])++rest :: String -> IO String+rest xs = fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs)++printClang :: String -> IO String+printClang = readCreateProcess (shell "clang-format")++processClang :: String -> IO String+processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ rest xs+processClang ('%':'{':'#':xs) = fmap (('%':) . ('{':) . ('#':)) $ rest xs+processClang ('%':'{':'$':xs) = fmap (('%':) . ('{':) . ('$':)) $ rest xs+processClang ('%':'{':xs)     = fmap (('%':) . ('{':)) $ rest xs+processClang (x:xs)           = fmap (x:) $ processClang xs+processClang []               = pure []  file :: Parser Program file = Program

@@ -1,491 +0,0 @@-{--    {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns #-}-    {-# LANGUAGE DeriveGeneric #-}-    {-# LANGUAGE DeriveAnyClass #-}-    {-# LANGUAGE DeriveDataTypeable #-}-    {-# LANGUAGE StandaloneDeriving #-}-    {-# LANGUAGE OverloadedStrings #-}--    -- | Module exporting the lexer itself as well as several data types for-    -- working with tokens.-    module Language.ATS.Lexer ( AlexPosn (..)-                              , Token (..)-                              , Keyword (..)-                              , Addendum (..)-                              , lexATS-                              , token_posn-                              , to_string-                              , get_addendum-                              ) where--import Data.Data (Typeable, Data)-import Data.Char (toUpper, toLower)-import Control.Lens (over, _head)-import Control.DeepSeq (NFData)-import GHC.Generics (Generic)-import Text.PrettyPrint.ANSI.Leijen hiding (line, column, (<$>))--}--%wrapper "posn"---- Digits-$digit = 0-9-$octal = 0-7---- Characters-$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#]-$alpha = [a-zA-Z]-$terminal = $printable # $white-$esc_char = \27-@escape_ch = \\ ([nt\'\\] | $octal+)-@escape_str = \\ ([nt\"\\] | $octal+)-@char = ($terminal # [\\\']) | " " | @escape_ch | $esc_char-@char_lit = \' @char \'--$br = [\<\>]---- Boolean literals-@bool = (true | false)---- Integer-@integer = $digit+-@time_lit = $digit+ u---- Floats-@decimals = $digit+-@float = @decimals \. @decimals---- Strings-@string = \" ($printable # [\"\\] | @escape_str | $esc_char | \n)* \"---- Identifiers-@identifier = ($alpha | _) ($alpha | $digit | _ | ! | ' | \$)*---- 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--@if_block = "#if" ([^\#] | "#then" | "#print" | \n)+ "#endif" .*---- FIXME this is a disaster lol-@ref_call = ($alpha | $digit | "(" | ")" | _ | (","))+ ">"--@not_close_c = \% [^\}]-@c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\}--@inner_signature = ("!wrt" | "!exn" | "!exnwrt" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment)-@inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | ""--@lambda = "=>" | "=>>" | "=<" @inner_signature_mult ">"-@signature = ":<" @inner_signature_mult ">" | ":"-@func_type = "->" | "-<" @inner_signature_mult ">"--@at_brace = \@ ($white | @block_comment)* \{--@operator = "**" | "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "%" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow--@double_parens = "(" @block_comment ")" | "()"-@double_braces = "{" @block_comment "}" | "{}"-@double_brackets = "<" @block_comment ">" | "<>"--@view = v | view--@fixity_decl = "infixr" | "infixl" | "prefix" | "postfix"--tokens :---    $white+                  ;-    ^ @block_comment         { tok (\p s -> CommentLex p s) }-    ^ "//".*                 { tok (\p s -> CommentLex p s) }-    "//".*                   ;-    @block_comment           ;-    "#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) }-    fn                       { tok (\p s -> Keyword p KwFn) }-    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) }-    data @view type          { tok (\p s -> Keyword p KwDatavtype) }-    dataview                 { tok (\p s -> Keyword p KwDataview) }-    dataprop                 { tok (\p s -> Keyword p KwDataprop) }-    assume                   { tok (\p s -> Keyword p KwAssume) }-    typedef                  { tok (\p s -> Keyword p KwTypedef) }-    @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) }-    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)) } -- TODO also val@ ?-    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) }-    implmnt                  { tok (\p s -> Keyword p KwImplement) }-    primplmnt                { tok (\p s -> Keyword p KwProofImplement) }-    primplement              { tok (\p s -> Keyword p KwProofImplement) }-    abst"@"ype               { tok (\p s -> Keyword p (KwAbst0p None)) }-    abst"@ype+"              { tok (\p s -> Keyword p (KwAbst0p Plus)) }-    abst"@type-"             { tok (\p s -> Keyword p (KwAbst0p Minus)) }-    abs@view"t@ype"          { tok (\p s -> Keyword p (KwAbsvt0p 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)) }-    @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) }-    abs @view type           { tok (\p s -> Keyword p KwAbsvtype) }-    absview                  { tok (\p s -> Keyword p KwAbsview) }-    view                     { tok (\p s -> Keyword p (KwView None)) }-    view"+"                  { tok (\p s -> Keyword p (KwView Plus)) }-    view"-"                  { tok (\p s -> Keyword p (KwView Minus)) }-    viewdef                  { tok (\p s -> Keyword p KwViewdef) }-    "#"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) }-    stacst                   { tok (\p s -> Keyword p KwStacst) }-    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) }-    sortdef                  { tok (\p s -> Keyword p KwSortdef) }-    propdef                  { tok (\p s -> Keyword p KwPropdef) }-    tkindef                  { tok (\p s -> Keyword p KwTKind) }-    typekindef               { tok (\p s -> Keyword p KwTKind) }-    "$raise"                 { tok (\p s -> Keyword p KwRaise) }-    mod                      { tok (\p s -> Keyword p KwMod) }-    "println!"               { tok (\p s -> Identifier p s) }-    "prerrln!"               { tok (\p s -> Identifier p s) }-    "fix@"                   { tok (\p s -> Keyword p KwFixAt) }-    "lam@"                   { tok (\p s -> Keyword p KwLambdaAt) }-    "addr"                   { tok (\p s -> Keyword p KwAddr) }-    "addr@"                  { tok (\p s -> Keyword p KwAddrAt) }-    "view@"                  { tok (\p s -> Keyword p KwViewAt) }-    sta                      { tok (\p s -> Keyword p KwSta) }-    symintr                  { tok (\p s -> Keyword p KwSymintr) }-    absview                  { tok (\p s -> Keyword p KwAbsview) }-    "$list"                  { tok (\p s -> Keyword p (KwListLit "")) }-    "$list_vt"               { tok (\p s -> Keyword p (KwListLit "_vt")) }-    "fold@"                  { tok (\p s -> IdentifierSpace p s) }-    "free@"                  { tok (\p s -> Identifier p s) }-    @fixity_decl             { tok (\p s -> FixityTok p s) }-    @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 (toChar s)) }-    @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)) } -- FIXME shouldn't fail silenty on overflow-    @float                   { tok (\p s -> FloatTok p (read s)) }-    $br / @ref_call          { tok (\p s -> SpecialBracket p) }-    @at_brace                { tok (\p s -> Operator p "@{") } -- FIXME this is kinda sloppy-    @operator                { tok (\p s -> Operator p s) }-    @signature               { tok (\p s -> SignatureTok p (tail s)) }-    $special                 { tok (\p s -> Special p s) }-    "effmask_all"            { tok (\p s -> Identifier p s) }-    "effmask_wrt"            { tok (\p s -> Identifier p s) }-    "extype"                 { tok (\p s -> Identifier p s) }-    @identifier / " "        { tok (\p s -> IdentifierSpace p s) }-    @identifier              { tok (\p s -> Identifier p s) }-    @string                  { tok (\p s -> StringTok p s) }--{--deriving instance Generic AlexPosn-deriving instance NFData AlexPosn-deriving instance Data AlexPosn-deriving instance Typeable AlexPosn--tok f p s = f p s---- | Determines the default behavior for incomplete pattern matches-data Addendum = None-              | Plus-              | Minus-              deriving (Eq, Show, Generic, NFData, Data, Typeable)--get_addendum (Keyword _ (KwVal a)) = a-get_addendum _ = None--data Keyword = KwFun-             | KwFnx-             | KwAnd-             | KwDatatype-             | KwDatavtype-             | 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 Addendum-             | KwAbstype-             | KwType-             | KwAbst0p Addendum-             | KwAbsvt0p Addendum-             | KwT0p Addendum-             | KwVt0p Addendum-             | KwPrfun-             | KwPrfn-             | KwCastfn-             | KwExtern-             | KwAbsvtype-             | KwProofImplement-             | KwSortdef-             | KwPropdef-             | KwRaise-             | KwTKind-             | KwMod-             | KwFixAt-             | KwLambdaAt-             | KwAddrAt-             | KwAddr-             | KwSta-             | KwViewAt-             | KwViewdef-             | KwSymintr-             | KwAbsview-             | KwFn-             | KwInfix-             | KwInfixr-             | KwInfixl-             | KwStacst-             | KwListLit String-             deriving (Eq, Show, Generic, NFData)--data Token = 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-           | IdentifierSpace AlexPosn String-           | Operator AlexPosn String-           | Arrow AlexPosn String-           | FuncType AlexPosn String-           | CommentLex AlexPosn String-           | MacroBlock AlexPosn String-           | TimeTok AlexPosn String-           | SignatureTok AlexPosn String-           | DoubleParenTok AlexPosn-           | DoubleBracesTok AlexPosn-           | DoubleBracketTok AlexPosn-           | SpecialBracket AlexPosn-           | FixityTok AlexPosn String-           deriving (Eq, Show, Generic, NFData)--instance Pretty Addendum where-    pretty Plus = "+"-    pretty Minus = "-"-    pretty None = ""--instance Pretty Keyword where-    pretty KwFun = "fun"-    pretty KwAnd = "and"-    pretty KwDatatype = "datatype"-    pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype-    pretty KwFnx = "fnx"-    pretty KwAssume = "assume"-    pretty KwTypedef = "typedef"-    pretty KwVtypedef = "vtypedef"-    pretty KwStaload = "stload"-    pretty KwLet = "let"-    pretty KwWhere = "where"-    pretty KwLocal = "local"-    pretty KwEnd = "end"-    pretty KwBegin = "begin"-    pretty KwIn = "in"-    pretty KwImplement = "implement"-    pretty (KwCase c) = "case" <> pretty c-    pretty KwIf = "if"-    pretty KwSif = "sif"-    pretty KwThen = "then"-    pretty KwElse = "else"-    pretty KwString = "string"-    pretty KwBool = "bool"-    pretty KwInt = "int"-    pretty KwVoid = "void"-    pretty KwNat = "nat"-    pretty (KwVal c) = "val" <> pretty c-    pretty KwVar = "var"-    pretty KwLambda = "lam"-    pretty KwLinearLambda = "llam"-    pretty KwInclude = "include"-    pretty KwWhen = "when"-    pretty KwOf = "of"-    pretty KwAbsprop = "absprop"-    pretty KwPrval = "prval"-    pretty KwStadef = "stadef"-    pretty KwPraxi = "praxi"-    pretty KwWhile = "while"-    pretty KwOverload = "overload"-    pretty KwWith = "with"-    pretty KwChar = "char"-    pretty KwDataview = "dataview"-    pretty KwDataprop = "dataprop"-    pretty (KwView c) = "view" <> pretty c-    pretty KwAbstype = "abstype"-    pretty KwAbsvtype = "absvtype"-    pretty KwType = "type"-    pretty (KwAbst0p c) = "abst@ype" <> pretty c-    pretty (KwAbsvt0p c) = "absvt@ype" <> pretty c-    pretty (KwT0p c) = "t@ype" <> pretty c-    pretty (KwVt0p c) = "vt@ype" <> pretty c-    pretty KwPrfun = "prfun"-    pretty KwPrfn = "prfn"-    pretty KwCastfn = "castfn"-    pretty KwExtern = "extern"-    pretty KwRaise = "$raise"-    pretty KwProofImplement = "primplmnt"-    pretty KwSortdef = "sortdef"-    pretty KwPropdef = "propdef"-    pretty KwTKind = "tkind"-    pretty KwMod = "mod"-    pretty KwFixAt = "fix@"-    pretty KwLambdaAt = "lam@"-    pretty KwAddrAt = "addr@"-    pretty KwAddr = "addr"-    pretty KwSta = "sta"-    pretty KwStacst = "stacst"-    pretty KwViewAt = "view@"-    pretty KwViewdef = "viewdef"-    pretty KwSymintr = "symintr"-    pretty KwAbsview = "absview"-    pretty KwFn = "fn"-    pretty KwInfix = "infix"-    pretty KwInfixr = "infixr"-    pretty KwInfixl = "infixl"-    pretty (KwListLit s) = "list" <> string s--instance Pretty Token where-    pretty (Identifier _ s) = text s-    pretty (IdentifierSpace _ s) = text s-    pretty (Keyword _ kw) = pretty kw-    pretty (BoolTok _ b) = text $ over _head toLower (show b)-    pretty (IntTok _ i) = pretty i-    pretty (FloatTok _ x) = pretty x-    pretty (CharTok _ c) = squotes (pretty c)-    pretty (StringTok _ s) = dquotes (text s)-    pretty (Special _ s) = text s-    pretty CBlockLex{} = "%{"-    pretty (Arrow _ s) = text s-    pretty (CommentLex _ s) = text $ take 2 s-    pretty (FuncType _ s) = text s-    pretty (TimeTok _ s) = text s-    pretty (SignatureTok _ s) = ":" <> text s-    pretty (Operator _ s) = text s-    pretty (MacroBlock _ s) = "#"-    pretty DoubleParenTok{} = "()"-    pretty DoubleBracesTok{} = "{}"-    pretty DoubleBracketTok{} = "<>"-    pretty SpecialBracket{} = "<"-    pretty (FixityTok _ s) = text s--to_string (CommentLex _ s) = s-to_string (Identifier _ s) = s-to_string (IdentifierSpace _ s) = s-to_string _ = mempty--token_posn (Identifier p _) = p-token_posn (IdentifierSpace 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 (MacroBlock p _) = p-token_posn (TimeTok p _) = p-token_posn (SignatureTok p _) = p-token_posn (DoubleParenTok p) = p-token_posn (DoubleBracesTok p) = p-token_posn (DoubleBracketTok p) = p-token_posn (SpecialBracket p) = p-token_posn (FixityTok p _) = p--toChar :: String -> Char-toChar "'\\n'" = '\n'-toChar "'\\t'" = '\t'-toChar "'\\\\'" = '\\'-toChar x = x !! 1---- | This function turns a string into a stream of tokens for the parser.-lexATS :: String -> [Token]-lexATS = alexScanTokens--}

@@ -1,697 +0,0 @@-{-    {-# LANGUAGE OverloadedStrings #-}-    {-# LANGUAGE DeriveGeneric     #-}-    {-# LANGUAGE DeriveAnyClass    #-}-    {-# LANGUAGE FlexibleContexts  #-}--    -- | 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-                          , to_string-                          , get_addendum-                          )--import Data.Char (toLower)-import Control.DeepSeq (NFData)-import Control.Lens (over, _head)-import GHC.Generics (Generic)-import Prelude-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))--}--%name parseATS-%tokentype { Token }-%error { parseError }-%monad { Either (ATSError String) } { (>>=) } { pure }--%token-    fun { Keyword $$ KwFun }-    fn { Keyword $$ KwFn }-    castfn { Keyword $$ KwCastfn }-    prfun { Keyword $$ KwPrfun }-    prfn { Keyword $$ KwPrfn }-    fnx { Keyword $$ KwFnx }-    and { Keyword $$ KwAnd }-    lambda { Keyword $$ KwLambda }-    llambda { Keyword $$ KwLinearLambda }-    if { Keyword $$ KwIf }-    sif { Keyword $$ KwSif }-    stadef { Keyword $$ KwStadef }-    val { $$@(Keyword _ (KwVal _)) }-    prval { Keyword $$ KwPrval }-    var { Keyword $$ KwVar }-    then { Keyword $$ KwThen }-    let { Keyword $$ KwLet }-    typedef { Keyword $$ KwTypedef }-    vtypedef { Keyword $$ KwVtypedef }-    absview { Keyword $$ KwAbsview }-    absvtype { Keyword $$ KwAbsvtype }-    abstype { Keyword $$ KwAbstype }-    abst0p { Keyword $$ (KwAbst0p None) }-    absvt0p { Keyword $$ (KwAbsvt0p None) }-    viewdef { Keyword $$ KwViewdef }-    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 }-    addr { Keyword $$ KwAddr }-    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) }-    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 None) }-    viewPlusMinus { Keyword _ (KwView $$) }-    raise { Keyword $$ KwRaise }-    tkindef { Keyword $$ KwTKind }-    assume { Keyword $$ KwAssume }-    addrAt { Keyword $$ KwAddrAt }-    viewAt { Keyword $$ KwViewAt }-    symintr { Keyword $$ KwSymintr }-    stacst { Keyword $$ KwStacst }-    propdef { Keyword $$ KwPropdef }-    list { Keyword $$ (KwListLit "") }-    list_vt { Keyword $$ (KwListLit "_vt") }-    boolLit { BoolTok _ $$ }-    timeLit { TimeTok _ $$ }-    intLit { IntTok _ $$ }-    floatLit { FloatTok _ $$ }-    effmaskWrt { Identifier $$ "effmask_wrt" }-    effmaskAll { Identifier $$ "effmask_all" }-    extype { Identifier $$ "extype" }-    extfcall { Identifier $$ "extfcall" }-    ldelay { Identifier $$ "ldelay" }-    listVT { Identifier $$ "list_vt" }-    foldAt { Identifier $$ "fold@" }-    identifier { $$@Identifier{} }-    identifierSpace { $$@IdentifierSpace{} }-    closeParen { Special $$ ")" }-    openParen { Special $$ "(" }-    colon { SignatureTok $$ "" }-    signature { SignatureTok _ $$ }-    comma { Special $$ "," }-    percent { Operator $$ "%" }-    geq { Operator $$ ">=" }-    leq { Operator $$ "<=" }-    neq { Operator $$ "!=" }-    openTermetric { Operator $$ ".<" }-    closeTermetric { Operator $$ ">." }-    mutateArrow { FuncType $$ "->" }-    mutateEq { Operator $$ ":=" }-    lbracket { Operator $$ "<" }-    rbracket { Operator $$ ">" }-    eq { Operator $$ "=" }-    or { Operator $$ "||" }-    vbar { Special $$ "|" }-    lbrace { Special $$ "{" }-    rbrace { Special $$ "}" }-    funcArrow { FuncType _ $$ }-    plainArrow { Arrow $$ "=>" }-    cloref1Arrow { Arrow $$ "=<cloref1>" }-    cloptr1Arrow { Arrow $$ "=<cloptr1>" }-    lincloptr1Arrow { Arrow $$ "=<lincloptr1>" }-    spear { Arrow $$ "=>>" }-    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 $$ "&&" }-    doubleEq { Operator $$ "==" }-    doubleDot { Operator $$ ".." }-    doubleParens { DoubleParenTok $$ }-    doubleBraces { DoubleBracesTok $$ }-    doubleBrackets { DoubleBracketTok $$ }-    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 _ $$ }-    define { MacroBlock _ $$ }-    lineComment { $$@CommentLex{} }-    lspecial { SpecialBracket $$ }-    atbrace { Operator $$ "@{" }-    exp { Operator $$ "**" }-    mod { Keyword $$ KwMod }-    fixAt { Keyword $$ KwFixAt }-    lamAt { Keyword $$ KwLambdaAt }-    infixr { FixityTok $$ "infixr" }-    infixl { FixityTok $$ "infixr" }-    prefix { FixityTok $$ "prefix" }-    postfix { FixityTok $$ "postfix" }--%%--ATS : Declarations { ATS $1 }---- | Parse declarations in a list-Declarations : { [] } -             | Declarations Declaration { $2 : $1 }-             | Declarations FunDecl { $2 ++ $1 }-             | Declarations local ATS in ATS end { Local $2 $3 $5 : $1 }---- | Several comma-separated types-TypeIn : Type { [$1] }-       | TypeIn comma Type { $3 : $1 }---- | Several comma-separated types or static expressions-TypeInExpr : TypeIn { $1 }-           | StaticExpression { [ConcreteType $1] }-           | TypeInExpr comma Type { $3 : $1 }-           | TypeInExpr comma StaticExpression { ConcreteType $3 : $1 }---- | Parse a type-Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 }-     | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 }-     | bool { Bool }-     | int { Int }-     | nat { Nat }-     | addr { Addr }-     | stringType { String }-     | charType { Char }-     | voidType { Void }-     | t0pPlain { T0p None }-     | t0pCo { T0p Plus }-     | vt0pPlain { Vt0p None }-     | vt0pCo { Vt0p Plus }-     | stringType openParen StaticExpression closeParen { DepString $3 }-     | stringType StaticExpression { DepString $2 }-     | int openParen StaticExpression closeParen { DependentInt $3 }-     | bool openParen StaticExpression closeParen { DependentBool $3 }-     | identifierSpace { Named (Unqualified $ to_string $1) }-     | Name { Named $1 }-     | exclamation Type { Unconsumed $2 }-     | Type mutateArrow Type { FunctionType "->" $1 $3 }-     | 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 }-     | viewPlusMinus { ViewLiteral $1 }-     | view { ViewLiteral None }-     | Existential Type { Ex $1 $2 }-     | Universal Type { ForA $1 $2 }-     | Type at Type { At $2 (Just $1) $3 }-     | at Type { At $1 Nothing $2 }-     | atbrace Records rbrace { AnonymousRecord $1 $2 }-     | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }-     | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }-     | openParen TypeIn closeParen { Tuple $1 $2 }-     | openParen Type closeParen { $2 }-     | int StaticExpression { DependentInt $2 }-     | doubleParens { NoneType $1 }-     | minus {% Left $ Expected $1 "Type" "-" }-     | dollar {% Left $ Expected $1 "Type" "$" }-     | int identifier openParen {% Left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }--FullArgs : Args { $1 }---- | A comma-separated list of arguments-Args : Arg { [$1] }-     | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 }-     | Args comma Arg { $3 : $1 }-     | Arg vbar Arg { [ PrfArg $1 $3 ] }--TypeArg : identifier { Arg (First $ to_string $1) }-        | IdentifierOr colon Type { Arg (Both $1 $3) }-        | Type { Arg (Second $1) }--Arg : TypeArg { $1 }-    | StaticExpression { Arg (Second (ConcreteType $1)) }---- | Parse a literal-Literal : boolLit { BoolLit $1 }-        | timeLit { TimeLit $1 }-        | intLit { IntLit $1 }-        | floatLit { FloatLit $1 }-        | string { StringLit $1 }-        | charLit { CharLit $1 }-        | doubleParens { VoidLiteral $1 }---- | Parse a list of comma-separated patterns-PatternIn : Pattern { [$1] }-          | PatternIn comma Pattern { $3 : $1 }---- | Parse a pattern match-Pattern : identifier { PName (to_string $1) [] }-        | identifierSpace { PName (to_string $1) [] }-        | underscore { Wildcard $1 }-        | identifier doubleParens { PName (to_string $1 ++ "()") [] }-        | tilde Pattern { Free $2 }-        | identifier openParen PatternIn closeParen { PName (to_string $1) $3 }-        | identifier Pattern { PSum (to_string $1) $2 }-        | identifierSpace Pattern { PSum (to_string $1) $2 }-        | openParen PatternIn vbar PatternIn closeParen { Proof $1 $2 $4 }-        | openParen PatternIn closeParen { TuplePattern $2 }-        | Literal { PLiteral $1 }-        | Pattern when Expression { Guarded $2 $3 $1 }-        | at Pattern { AtPattern $1 $2 }-        | identifier Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }-        | identifierSpace Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }-        | Existential Pattern { ExistentialPattern $1 $2 }-        | minus {% Left $ Expected $1 "Pattern" "-" }-        | plus {% Left $ Expected $1 "Pattern" "+" }---- | Parse a case expression-Case : vbar Pattern CaseArrow Expression { [($2, $3, $4)] }-     | Pattern CaseArrow Expression { [($1, $2, $3)] }-     | Case vbar Pattern CaseArrow Expression { ($3, $4, $5) : $1 }--ExpressionPrf : ExpressionIn { (Nothing, $1) }-              | Expression vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?---- | A list of comma-separated expressions-ExpressionIn : Expression { [$1] }-             | ExpressionIn comma Expression { $3 : $1 }--Tuple : PreExpression comma PreExpression { [$3, $1] }-      | Tuple comma PreExpression { $3 : $1 }---- | Parse an arrow in a case statement-CaseArrow : plainArrow { Plain $1 }-          | spear { Spear $1 }-          | minus {% Left $ Expected $1 "Arrow" "-" }-          | eq {% Left $ Expected $1 "Arrow" "=" }-          | minus {% Left $ Expected $1 "Arrow" "-" }--LambdaArrow : plainArrow { Plain $1 }-            | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently.-            | cloptr1Arrow { Full $1 "cloptr1" }-            | lincloptr1Arrow { Full $1 "lincloptr1" }-            | minus {% Left $ Expected $1 "Arrow" "-" }-            | openParen {% Left $ Expected $1 "Arrow" "(" }-            | closeParen {% Left $ Expected $1 "Arrow" ")" }---- | Expression or named call to an expression-Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }-           | PreExpression { $1 }-           | openParen Tuple closeParen { TupleEx $1 $2 }-           | Expression semicolon Expression { Precede $1 $3 }-           | Expression semicolon { $1 }-           | openParen Expression closeParen { $2 }-           | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?-           | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }-           | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }-           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 }-           | begin Expression extern {% Left $ Expected $3 "end" "extern" }-           | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" }--TypeArgs : lbrace Type rbrace { [$2] }-         | lbrace TypeIn rbrace { $2 }-         | TypeArgs lbrace Type rbrace { $3 : $1 }-         | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls-         | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 }--BracketedArgs : lbracket Type rbracket { [$2] }-              | lbracket TypeIn rbrace { $2 }--Call : Name doubleParens { Call $1 [] [] Nothing [] }-     | identifierSpace openParen ExpressionPrf closeParen { Call (Unqualified $ to_string $1) [] [] (fst $3) (snd $3) }-     | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }-     | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) }-     | Name TypeArgs { Call $1 [] $2 Nothing [] }-     | Name lspecial TypeIn rbracket doubleParens { Call $1 $3 [] Nothing [VoidLiteral $5] }-     | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) }-     | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }-     | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument-     | Name openParen ExpressionPrf end {% Left $ Expected $4 ")" "end"}-     | Name openParen ExpressionPrf else {% Left $ Expected $4 ")" "else"}--StaticArgs : StaticExpression { [$1] }-           | StaticArgs comma StaticExpression { $3 : $1 }--StaticExpression : Name { StaticVal $1 }-                 | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }-                 | intLit { StaticInt $1 }-                 | doubleParens { StaticVoid $1 }-                 | boolLit { StaticBool $1 }-                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions-                 | identifierSpace { StaticVal (Unqualified $ to_string $1) }-                 | Name openParen StaticArgs closeParen { SCall $1 $3 }-                 | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }-                 | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }-    --- | Parse an expression that can be called without parentheses-PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }-              | Literal { $1 }-              | Call { $1 }-              | case Expression of Case { Case $3 $1 $2 $4 }-              | openParen Expression closeParen { ParenExpr $1 $2 }-              | PreExpression BinOp PreExpression { Binary $2 $1 $3 }-              | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time-              | PreExpression dot Name { Access $2 $1 $3 }-              | PreExpression dot intLit { Access $2 $1 (Unqualified $ show $3) }-              | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $ to_string $3) }-              | if Expression then Expression { If $2 $4 Nothing}-              | if Expression then Expression else Expression { If $2 $4 (Just $6) }-              | let ATS in end { Let $1 $2 Nothing }-              | let ATS in Expression end { Let $1 $2 (Just $4) }-              | let ATS in Expression vbar {% Left $ Expected $5 "end" "|" }-              | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 }-              | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 }-              | addrAt PreExpression { AddrAt $1 $2 }-              | viewAt PreExpression { ViewAt $1 $2 }-              | PreExpression at PreExpression { AtExpr $1 $3 }-              | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }-              | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }-              | exclamation PreExpression { Deref $1 $2 }-              | PreExpression mutateArrow identifierSpace mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }-              | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }-              | PreExpression mutateEq PreExpression { Mutate $1 $3 }-              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }-              | identifierSpace { NamedVal (Unqualified $ to_string $1) }-              | begin Expression end { Begin $1 $2 }-              | 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" }-              | var {% Left $ Expected $1 "Expression" "var" }-              | Termetric {% Left $ Expected (fst $1) "Expression" "termetric" }-              | fromVT {% Left $ Expected $1 "Expression" "?!" }-              | prfTransform {% Left $ Expected $1 "Expression" ">>" }-              | maybeProof {% Left $ Expected $1 "Expression" "?" }-              | let openParen {% Left $ Expected $1 "Expression" "let (" }-              | let ATS in Expression lineComment {% Left $ Expected (token_posn $5) "end" (take 2 $ to_string $5) }-              | let ATS in Expression extern {% Left $ Expected $5 "end" "extern" }-              | let ATS in Expression fun {% Left $ Expected $5 "end" "fun" }-              | let ATS in Expression vtypedef {% Left $ Expected $5 "end" "vtypedef" }-              | if Expression then Expression else else {% Left $ Expected $6 "Expression" "else" }---- | Parse a termetric-Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) }-          | underscore {% Left $ Expected $1 "_" "Termination metric" }-          | dollar {% Left $ Expected $1 "$" "Termination metric" }---- | Parse an existential quantier on a type-Existential : lsqbracket Args vbar StaticExpression rsqbracket { Existential $2 False Nothing (Just $4) }-            | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing }-            | openExistential Args rsqbracket { Existential $2 True Nothing Nothing }-            | openExistential Args vbar StaticExpression rsqbracket { Existential $2 True Nothing (Just $4) }-            | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':'-            | lsqbracket StaticExpression rsqbracket { Existential [] False Nothing (Just $2) }-            --- | Parse a universal quantifier on a type-Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }-          | lbrace Args vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }---- | Parse the details of an implementation-Implementation : FunName doubleParens eq Expression { Implement $2 [] [] $1 [] $4 }-               | FunName openParen FullArgs closeParen eq Expression { Implement $2 [] [] $1 $3 $6 }-               | FunName Universals openParen FullArgs closeParen eq Expression { Implement $3 [] $2 $1 $4 $7 }-               | Universals FunName openParen FullArgs closeParen eq Expression { Implement $3 $1 [] $2 $4 $7 }-               | Universals FunName Universals openParen FullArgs closeParen eq Expression { Implement $4 $1 $3 $2 $5 $8 }---- | Parse a function name-FunName : IdentifierOr { Unqualified $1 }-        | identifier dollar identifier { Functorial (to_string $1) (to_string $3) }---- | Parse a general name-Name : identifier { Unqualified (to_string $1) }-     | underscore { Unqualified "_" }-     | listVT { Unqualified "list_vt" }-     | foldAt { Unqualified "fold@" }-     | dollar identifier dot identifier { Qualified $1 (to_string $4) (to_string $2) }-     | dollar identifier dot identifierSpace { Qualified $1 (to_string $4) (to_string $2) }-     | dollar effmaskWrt { SpecialName $1 "effmask_wrt" }-     | dollar effmaskAll { SpecialName $1 "effmask_all" }-     | dollar extype { SpecialName $1 "effmask_all" }-     | dollar listVT { SpecialName $1 "list_vt" }-     | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this-     | dollar {% Left $ Expected $1 "Name" "$" }---- | Parse a list of values in a record-RecordVal : IdentifierOr eq Expression { [($1, $3)] }-          | RecordVal comma IdentifierOr eq Expression { ($3, $5) : $1 }---- | Parse a list of types in a record-Records : IdentifierOr eq Type { [($1, $3)] }-        | Records comma IdentifierOr eq Type { ($3, $5) : $1 }--IdentifiersIn : IdentifierOr { [$1] }-              | IdentifiersIn comma IdentifierOr { $3 : $1 }--OfType : { Nothing }-       | of Type { Just $2 }---- | Parse a constructor for a sum type-SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }-        | vbar Universals identifierSpace of Type { Leaf $2 (to_string $3) [] (Just $5) }-        | vbar Universals IdentifierOr openParen IdentifiersIn closeParen OfType { Leaf $2 $3 $5 $7 }---- | Parse all constructors of a sum type-Leaves : SumLeaf { [$1] }-       | Leaves SumLeaf { $2 : $1 }-       | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }-       | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }-       | Universals identifier openParen IdentifiersIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.-       | dollar {% Left $ Expected $1 "|" "$" }--Universals : { [] }-           | doubleBraces { [] }-           | Universals Universal { $2 : $1 }---- | Optionally parse a termetric-OptTermetric : { Nothing }-             | Termetric { Just (snd $1) }---- | Parse a unary operator-UnOp : tilde { Negate }---- | Parse a binary operator-BinOp : plus { Add }-      | minus { Sub }-      | div { Div }-      | mult { Mult }-      | geq { GreaterThanEq }-      | leq { LessThanEq }-      | lbracket { LessThan }-      | rbracket { GreaterThan }-      | neq { NotEqual }-      | andOp { LogicalAnd }-      | or { LogicalOr }-      | doubleEq { StaticEq }-      | eq { Equal }-      | mod { Mod }-      | percent { Mod }---- | Optionally parse a function body-OptExpression : { Nothing }-              | eq Expression { Just $2 } -- FIXME only let this happen for external declarations---- | Parse a constructor for a 'dataprop'-DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing }-             | Universals Expression { DataPropLeaf $1 $2 Nothing }-             | vbar Universals Expression of Expression { DataPropLeaf $2 $3 (Just $5) }-             | Universals Expression of Expression { DataPropLeaf $1 $2 (Just $4) }---- | Parse several constructors for a 'dataprop'-DataPropLeaves : DataPropLeaf { [$1] }-               | DataPropLeaves DataPropLeaf { $2 : $1 }-               | prval {% Left $ Expected $1 "Constructor" "prval" }-               | var {% Left $ Expected $1 "Constructor" "var" }-               | val {% Left $ Expected (token_posn $1) "Constructor" "val" }-               | lambda {% Left $ Expected $1 "Constructor" "lam" }-               | llambda {% Left $ Expected $1 "Constructor" "llam" }-               | minus {% Left $ Expected $1 "Constructor" "-" }-               | dollar {% Left $ Expected $1 "Constructor" "$" }-               | fromVT {% Left $ Expected $1 "Constructor" "?!" }-               | prfTransform {% Left $ Expected $1 "Constructor" ">>" }-               | maybeProof {% Left $ Expected $1 "Constructor" "?" }--Signature : signature { $1 }-          | colon { "" }--OptType : Type { Just $1 }-        | { Nothing }---- | Parse a type signature and optional function body-PreFunction : FunName openParen FullArgs closeParen Signature OptType OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }-            | FunName Universals OptTermetric Signature OptType OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }-            | FunName Universals OptTermetric doubleParens Signature OptType OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }-            | FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }-            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }-            | Universals FunName Universals OptTermetric Signature OptType OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }-            | prval {% Left $ Expected $1 "Function signature" "prval" }-            | var {% Left $ Expected $1 "Function signature" "var" }-            | val {% Left $ Expected (token_posn $1) "Function signature" "val" }-            | lambda {% Left $ Expected $1 "Function signature" "lam" }-            | llambda {% Left $ Expected $1 "Function signature" "llam" }-            | lsqbracket {% Left $ Expected $1 "Function signature" "[" }---- | Parse affiliated `sortdef`s-AndSort : AndSort and IdentifierOr eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way-        | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 }---- | Function declaration-FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }-        | prfun PreFunction { [ Func $1 (PrFun $2) ] }-        | prfn PreFunction { [ Func $1 (PrFn $2) ] }-        | fnx PreFunction { [ Func $1 (Fnx $2) ] }-        | castfn PreFunction { [ Func $1 (CastFn $2) ] }-        | fn PreFunction identifier {% Left $ Expected (token_posn $3) "=" (to_string $3) }-        | fn PreFunction { [ Func $1 (Fn $2) ] }-        | FunDecl and PreFunction { Func $2 (And $3) : $1 }-        | extern FunDecl { over _head (Extern $1) $2 }-        | extern fun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }-        | extern fnx PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }-        | extern praxi PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }-        | extern prfun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }-        | extern prfn PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }-        | lambda {% Left $ Expected $1 "Function declaration" "lam" }-        | llambda {% Left $ Expected $1 "Function declaration" "llam" }-        | fun fn {% Left $ Expected $2 "Function name" "fn" }-        | fn fun {% Left $ Expected $2 "Function name" "fun" }-        | extern FunDecl identifier openParen {% Left $ Expected (token_posn $3) "Static integer expression" (to_string $3) }--IdentifierOr : identifier { to_string $1 }-             | identifierSpace { to_string $1 }--MaybeType : eq Type { Just $2 }-          | { Nothing }---- | Parse a declaration defining a type-TypeDecl : typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 }-         | typedef IdentifierOr openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 }-         | vtypedef IdentifierOr eq Type { ViewTypeDef $1 $2 [] $4 }-         | vtypedef IdentifierOr openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 }-         | datatype IdentifierOr eq Leaves { SumType $2 [] $4 }-         | datatype IdentifierOr openParen Args closeParen eq Leaves { SumType $2 $4 $7 }-         | datavtype IdentifierOr eq Leaves { SumViewType $2 [] $4 }-         | datavtype IdentifierOr openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 }-         | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 }-         | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 }-         | absvt0p IdentifierOr openParen FullArgs closeParen MaybeType { AbsVT0p $1 $2 $4 $6 }-         | absvt0p IdentifierOr eq Type { AbsVT0p $1 $2 [] (Just $4) }-         | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 }-         | abstype IdentifierOr openParen FullArgs closeParen MaybeType { AbsType $1 $2 $4 $6 }-         | absvtype IdentifierOr openParen FullArgs closeParen MaybeType { AbsViewType $1 $2 $4 $6 }-         | dataprop IdentifierOr openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }-         | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 }-         | stadef IdentifierOr eq Name { Stadef $2 $4 [] }-         | stadef IdentifierOr eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 }-         | stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] } -- TODO identifierSpace-         | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 }-         | AndSort { $1 }--Fixity : infixr { RightFix $1 }-       | infixl { LeftFix $1 }-       | prefix { Pre $1 }-       | postfix { Post $1 }--Operator : identifierSpace { to_string $1 }-         | exp { "**" }--Operators : Operator { [$1] }-          | Operators Operator { $2 : $1 }-          | Operators identifier { to_string $2 : $1 }--StackFunction : openParen Args closeParen Signature Type plainArrow Expression { StackF $4 $2 $5 $7 }---- | Parse a declaration-Declaration : include string { Include $2 }-            | define { Define $1 }-            | define identifierSpace string { Define ($1 ++ " " ++ to_string $2 ++ $3) } -- FIXME better approach?-            | define identifierSpace intLit { Define ($1 ++ " " ++ to_string $2 ++ " " ++ show $3) }-            | cblock { CBlock $1 }-            | lineComment { Comment (to_string $1) }-            | staload underscore eq string { Staload (Just "_") $4 }-            | staload string { Staload Nothing $2 }-            | staload IdentifierOr eq string { Staload (Just $2) $4 }-            | extern Declaration { Extern $1 $2 }-            | var Pattern colon Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general.-            | var Pattern colon Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }-            | val Pattern colon Type eq PreExpression { Val (get_addendum $1) (Just $4) $2 $6 }-            | val Pattern eq Expression { Val (get_addendum $1) Nothing $2 $4 }-            | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }-            | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }-            | var Pattern eq fixAt IdentifierOr StackFunction { Var Nothing $2 (Just $ FixAt $5 $6) Nothing }-            | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing }-            | prval Pattern eq Expression { PrVal $2 $4 }-            | praxi PreFunction { Func $1 (Praxi $2) }-            | primplmnt Implementation { ProofImpl $2 }-            | implement Implementation { Impl [] $2 }-            | implement openParen Args closeParen Implementation { Impl $3 $5 }-            | overload BinOp with Name { OverloadOp $1 $2 $4 }-            | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }-            | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) } -- FIXME figure out a general solution.-            | assume Name openParen Args closeParen eq Expression { Assume $2 $4 $7 }-            | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }-            | TypeDecl { $1 }-            | symintr Name { SymIntr $1 $2 }-            | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }-            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }-            | Fixity intLit Operators { FixityDecl $1 (Just $2) $3 }-            | val Universals IdentifierOr colon Type { StaVal $2 $3 $5 }-            | lambda {% Left $ Expected $1 "Declaration" "lam" }-            | llambda {% Left $ Expected $1 "Declaration" "llam" }-            | minus {% Left $ Expected $1 "Declaration" "-" }-            | dollar {% Left $ Expected $1 "Declaration" "$" }-            | fromVT {% Left $ Expected $1 "Declaration" "?!" }-            | prfTransform {% Left $ Expected $1 "Declaration" ">>" }-            | maybeProof {% Left $ Expected $1 "Declaration" "?" }-            | identifier {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }--{--data ATSError a = Expected AlexPosn a a-                | Unknown Token -- FIXME error type for expression when a static expression was expected (?)-                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 s2) <> ", expected:" <+> squotes (string s1)) <> linebreak-    pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak--parseError :: [Token] -> Either (ATSError String) a-parseError = Left . Unknown . head -}

@@ -1,547 +0,0 @@-{-# OPTIONS_GHC -fno-warn-orphans #-}--{-# LANGUAGE CPP                  #-}-{-# LANGUAGE DeriveAnyClass       #-}-{-# LANGUAGE DeriveGeneric        #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE OverloadedStrings    #-}-{-# LANGUAGE PatternSynonyms      #-}-{-# LANGUAGE StandaloneDeriving   #-}-{-# LANGUAGE TypeSynonymInstances #-}--module Language.ATS.PrettyPrint ( printATS-                                , printATSCustom-                                , printATSFast-                                , processClang-                                ) where--import           Control.Arrow                         hiding ((<+>))-import           Control.Composition                   hiding ((&))-import           Control.DeepSeq                       (NFData)-import           Control.Lens                          hiding (op, pre)-#if __GLASGOW_HASKELL__ >= 801-import           Data.Function                         (on)-#endif-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--infixr 5 $$--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--takeBlock :: String -> (String, String)-takeBlock ('%':'}':ys) = ("", ('%':) . ('}':) $ ys)-takeBlock (y:ys)       = first (y:) $ takeBlock ys-takeBlock []           = ([], [])--rest :: String -> IO String-rest xs = fmap (<> (snd $ takeBlock xs)) $ printClang (fst $ takeBlock xs)--processClang :: String -> IO String-processClang ('%':'{':'^':xs) = fmap (('%':) . ('{':) . ('^':)) $ rest xs-processClang ('%':'{':'#':xs) = fmap (('%':) . ('{':) . ('#':)) $ rest xs-processClang ('%':'{':'$':xs) = fmap (('%':) . ('{':) . ('$':)) $ rest xs-processClang ('%':'{':xs)     = fmap (('%':) . ('{':)) $ rest xs-processClang (x:xs)           = fmap (x:) $ processClang xs-processClang []               = pure []--printClang :: String -> IO String-printClang = readCreateProcess (shell "clang-format")---- | Pretty-print with sensible defaults.-printATS :: ATS -> String-printATS = (<> "\n") . printATSCustom 0.6 120--printATSCustom :: Float -- ^ Ribbon fraction-               -> Int -- ^ Ribbon width-               -> ATS -> String-printATSCustom r i (ATS x) = g mempty-    where g = (displayS . renderSmart r i . pretty) (ATS $ reverse x)---- | Fast pretty-printer without indendation. Useful for generating code.-printATSFast :: ATS -> String-printATSFast (ATS x) = g mempty-    where g = (displayS . renderCompact . (<> "\n") . pretty) (ATS $ reverse x)--instance Pretty Name where-    pretty (Unqualified n)   = text n-    pretty (Qualified _ i n) = "$" <> text n <> "." <> text i-    pretty (SpecialName _ s) = "$" <> text s-    pretty (Functorial s s') = text s <> "$" <> text s'-    pretty Unnamed{}         = mempty--instance Pretty LambdaType where-    pretty Plain{}    = "=>"-    pretty Spear{}    = "=>>"-    pretty (Full _ v) = "=<" <> text 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 = ">="-    pretty StaticEq      = "=="-    pretty Mod           = "%"--splits :: BinOp -> Bool-splits Mult       = True-splits Add        = True-splits Div        = True-splits Sub        = True-splits LogicalAnd = True-splits LogicalOr  = True-splits _          = False--startsParens :: Doc -> Bool-startsParens d = f (show d) where-    f ('(':_) = True-    f _       = False--prettySmall :: Doc -> [Doc] -> Doc-prettySmall op es = mconcat (punctuate (" " <> op <> " ") es)--prettyBinary :: Doc -> [Doc] -> Doc-prettyBinary op es-    | length (showFast $ mconcat es) < 80 = prettySmall op es-    | otherwise = prettyLarge op es--prettyLarge :: Doc -> [Doc] -> Doc-prettyLarge _ []      = mempty-prettyLarge op (e:es) = e <$> vsep (fmap (op <+>) es)---- FIXME we really need a monadic pretty printer lol.-lengthAlt :: Doc -> Doc -> Doc-lengthAlt d1 d2-    | length (showFast d2) >= 30 = d1 <$> indent 4 d2-    | otherwise = d1 <+> d2--instance Pretty Expression where-    pretty = cata a . rewriteATS where-        a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (IfF e e' Nothing)            = "if" <+> e <+> "then" <$> indent 2 e'-        a (LetF _ e (Just e'))          = flatAlt-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end")-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in" <+> e' <$> "end")-        a (LetF _ e Nothing)            = flatAlt-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end")-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in end")-        a (BoolLitF True)               = "true"-        a (BoolLitF False)              = "false"-        a (TimeLitF s)                  = text s-        a (IntLitF i)                   = pretty i-        a (LambdaF _ lt p e)            = let pre = "lam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)-        a (LinearLambdaF _ lt p e)      = let pre = "llam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)-        a (FloatLitF f)                 = pretty f-        a (StringLitF s)                = text s -- FIXME escape indentation in multi-line strings.-        a (ParenExprF _ e)              = parens e-        a (BinListF op@Add es)          = prettyBinary (pretty op) es-        a (BinaryF op e e')-            | splits op = e </> pretty op <+> e'-            | otherwise = e <+> pretty op <+> e'-        a (IndexF _ n e)                = pretty n <> "[" <> e <> "]"-        a (UnaryF Negate e)             = "~" <> e-        a (NamedValF nam)              = pretty nam-        a (CallF nam [] [] Nothing []) = pretty nam <> "()"-        a (CallF nam [] [] (Just e) xs) = pretty nam <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|"-        a (CallF nam [] [] Nothing xs) = pretty nam <> prettyArgs xs-        a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us-        a (CallF nam [] us Nothing xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsG "(" ")" xs-        a (CallF nam is [] Nothing []) = pretty nam <> prettyArgsU "<" ">" is-        a (CallF nam is [] Nothing [x])-            | startsParens x = pretty nam <> prettyArgsU "<" ">" is <> pretty x-        a (CallF nam is [] Nothing xs) = pretty nam <> prettyArgsU "<" ">" is <> prettyArgs xs-        a (CaseF _ add e cs)            = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs)-        a (VoidLiteralF _)              = "()"-        a (RecordValueF _ es Nothing)   = prettyRecord es-        a (RecordValueF _ es (Just x))  = prettyRecord es <+> ":" <+> pretty x-        a (PrecedeF e e')               = parens (e <+> ";" </> e')-        a (PrecedeListF es)             = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")-        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 '\\')              = "'\\\\'"-        a (CharLitF '\n')              = "'\\n'"-        a (CharLitF '\t')              = "'\\t'"-        a (CharLitF c)                 = "'" <> char c <> "'"-        a (ProofExprF _ e e')          = "(" <> e <+> "|" <+> e' <> ")"-        a (TypeSignatureF e t)         = e <+> ":" <+> pretty t-        a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> nest 2 (pretty (ATS $ reverse 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 <> "@" <> e'-        a (BeginF _ e)-            | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")-            | otherwise = e-        a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)-        a (LambdaAtF (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)-        a (AddrAtF _ e)                = "addr@" <> e-        a (ViewAtF _ e)                = "view@" <> e-        a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es-        a BinListF{} = undefined-        a CallF{} = undefined-        prettyCases []              = mempty-        prettyCases [(s, l, t)]     = "|" <+> pretty s <+> pretty l <+> t-        prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ...--noParens :: Doc -> Bool-noParens = all (`notElem` ("()" :: String)) . show--patternHelper :: [Doc] -> Doc-patternHelper ps = mconcat (punctuate ", " (reverse ps))--instance Pretty Pattern where-    pretty = cata a where-        a (WildcardF _)                = "_"-        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 (patternHelper ps)-        a (FreeF p)                    = "~" <> p-        a (GuardedF _ e p)             = p <+> "when" <+> pretty e-        a (ProofF _ p p')              = parens (patternHelper p <+> "|" <+> patternHelper p')-        a (TuplePatternF ps)           = parens (patternHelper ps)-        a (AtPatternF _ p)             = "@" <> p-        a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p-        a (ExistentialPatternF e p)    = pretty e <> p--singleArg :: Arg -> Doc-singleArg x@Arg{} = argHelper (<>) x-singleArg x       = pretty x--argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc-argHelper _ (Arg (First s))   = pretty s-argHelper _ (Arg (Second t))  = pretty t-argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t-argHelper op (PrfArg a a')    = pretty a `op` "|" `op` pretty a'-argHelper _ NoArgs            = undefined -- in theory we handle this elsewhere.--instance Pretty Arg where-    pretty = argHelper (<+>)--squish :: BinOp -> Bool-squish Add  = True-squish Sub  = True-squish Mult = True-squish _    = False--instance Pretty StaticExpression where-    pretty = cata a where-        a (StaticValF n)            = pretty n-        a (StaticBinaryF op se se')-            | squish op = se <> pretty op <> se'-            | otherwise = se <+> pretty op <+> se'-        a (StaticIntF i)            = pretty i-        a StaticVoidF{}             = "()"-        a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''-        a (StaticBoolF True)        = "true"-        a (StaticBoolF False)       = "false"-        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))-        a (SPrecedeF e e')          = e <> ";" <+> e'--instance Pretty Type where-    pretty = cata a where-        a IntF                    = "int"-        a StringF                 = "string"-        a BoolF                   = "bool"-        a VoidF                   = "void"-        a NatF                    = "nat"-        a AddrF                   = "addr"-        a CharF                   = "char"-        a (NamedF n)              = pretty 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 _ (Just t) t')     = t <+> "@" <+> t'-        a (AtF _ Nothing 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 (ViewTypeF _ t)         = "view@" <> parens t-        a (FunctionTypeF s t t')  = t <+> string s <+> t'-        a (ViewLiteralF c)        = "view" <> pretty c-        a NoneTypeF{}             = "()"-        a ImplicitTypeF{}         = ".."-        a (AnonymousRecordF _ rs) = prettyRecord rs--gan :: Maybe Type -> Doc-gan (Just t) = " : " <> pretty t <> " "-gan Nothing  = ""--withHashtag :: Bool -> Doc-withHashtag True = "#["-withHashtag _    = lbracket--instance Pretty Existential where-    pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket-    pretty (Existential [x@Arg{}] b Nothing Nothing) = withHashtag b <> singleArg x <> rbracket-    pretty (Existential bs b ty Nothing)  = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket-    pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket-        where go (Arg (First s))  = pretty s-              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t-              go (Arg (Second t)) = pretty t-              go _                = undefined--instance Pretty Universal where-    pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments-    pretty (Universal [x] Nothing Nothing) = lbrace <> singleArg x <> rbrace -- FIXME universals can now be length-one arguments-    pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbrace-    pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace-        where go (Arg (First s))  = pretty s-              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t-              go (Arg (Second t)) = pretty t-              go _                = undefined--instance Pretty ATS where-    pretty (ATS xs) = concatSame (fmap rewriteDecl 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)--isVal :: Declaration -> Bool-isVal Val{}   = True-isVal Var{}   = True-isVal PrVal{} = True-isVal _       = False--glue :: Declaration -> Declaration -> Bool-glue x y-    | isVal x && isVal y = True-glue Staload{} Staload{}           = True-glue Include{} Include{}           = True-glue ViewTypeDef{} ViewTypeDef{}   = True-glue TypeDef{} TypeDef{}           = True-glue Comment{} _                   = True-glue (Func _ Fnx{}) (Func _ And{}) = True-glue _ _                           = False--{-# INLINE glue #-}--concatSame :: [Declaration] -> Doc-concatSame []  = mempty-concatSame [x] = pretty x-concatSame (x:x':xs)-    | glue x x' = pretty x <$> concatSame (x':xs)-    | otherwise = pretty x <> line <$> concatSame (x':xs)---- TODO - soft break-($$) :: Doc -> Doc -> Doc-x $$ y = align (x <$> y)--lineAlt :: Doc -> Doc -> Doc-lineAlt = group .* flatAlt--showFast :: Doc -> String-showFast d = displayS (renderCompact d) mempty--prettyRecord :: (Pretty a) => [(String, a)] -> Doc-prettyRecord es-    | any ((>40) . length . showFast . pretty) es = prettyRecordF True es-    | otherwise = lineAlt (prettyRecordF True es) (prettyRecordS True es)--prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc-prettyRecordS _ []             = mempty-prettyRecordS True [(s, t)]    = "@{" <+> text s <+> "=" <+> pretty t <+> "}"-prettyRecordS _ [(s, t)]       = "@{" <+> text s <+> "=" <+> pretty t-prettyRecordS True ((s, t):xs) = prettyRecordS False xs <> "," <+> text s <+> ("=" <+> pretty t) <+> "}"-prettyRecordS x ((s, t):xs)    = prettyRecordS x xs <> "," <+> text s <+> ("=" <+> pretty t)--prettyRecordF :: (Pretty a) => Bool -> [(String, a)] -> Doc-prettyRecordF _ []             = mempty-prettyRecordF True [(s, t)]    = "@{" <+> text s <+> align ("=" <+> pretty t) <+> "}"-prettyRecordF _ [(s, t)]       = "@{" <+> text s <+> align ("=" <+> pretty t)-prettyRecordF True ((s, t):xs) = prettyRecordF False xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t) <$> "}")-prettyRecordF x ((s, t):xs)    = prettyRecordF x xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t))--prettyDL :: [DataPropLeaf] -> Doc-prettyDL []                               = mempty-prettyDL [DataPropLeaf [] e Nothing]      = indent 2 ("|" <+> pretty e)-prettyDL [DataPropLeaf [] e (Just e')]    = indent 2 ("|" <+> pretty e <+> "of" <+> pretty e')-prettyDL (DataPropLeaf [] e Nothing:xs)   = prettyDL xs $$ indent 2 ("|" <+> pretty e)-prettyDL (DataPropLeaf [] e (Just e'):xs) = prettyDL xs $$ indent 2 ("|" <+> pretty e <+> "of" <+> pretty e')-prettyDL [DataPropLeaf us e Nothing]      = indent 2 ("|" <+> foldMap pretty us <+> pretty e)-prettyDL [DataPropLeaf us e (Just e')]    = indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e')-prettyDL (DataPropLeaf us e Nothing:xs)   = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e)-prettyDL (DataPropLeaf us e (Just e'):xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e')--universalHelper :: [Universal] -> Doc-universalHelper = mconcat . fmap pretty . reverse--prettyLeaf :: [Leaf] -> Doc-prettyLeaf []                         = mempty-prettyLeaf [Leaf [] s [] Nothing]     = indent 2 ("|" <+> text s)-prettyLeaf [Leaf [] s [] (Just e)]    = indent 2 ("|" <+> text s <+> "of" <+> pretty e)-prettyLeaf (Leaf [] s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s)-prettyLeaf (Leaf [] s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <+> "of" <+> pretty e)-prettyLeaf [Leaf [] s as Nothing]     = indent 2 ("|" <+> text s <> prettyArgs as)-prettyLeaf [Leaf [] s as (Just e)]    = indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)-prettyLeaf (Leaf [] s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as)-prettyLeaf (Leaf [] s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)-prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s)-prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)-prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s)-prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)-prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)-prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)-prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)-prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)--prettyHelper :: Doc -> [Doc] -> [Doc]-prettyHelper _ [x]    = [x]-prettyHelper c (x:xs) = flatAlt (" " <> x) x : fmap (c <>) xs-prettyHelper _ x      = x--prettyBody :: Doc -> Doc -> [Doc] -> Doc-prettyBody c1 c2 [d] = c1 <> d <> c2-prettyBody c1 c2 ds  = (c1 <>) . align . indent (-1) . cat . (<> pure c2) $ ds--prettyArgsG' :: Doc -> Doc -> Doc -> [Doc] -> Doc-prettyArgsG' c3 c1 c2 = prettyBody c1 c2 . prettyHelper c3 . reverse--prettyArgsList :: Doc -> Doc -> Doc -> [Doc] -> Doc-prettyArgsList c3 c1 c2 = prettyBody c1 c2 . va . prettyHelper c3--va :: [Doc] -> [Doc]-va = (& _tail.traverse %~ group)--prettyArgsG :: Doc -> Doc -> [Doc] -> Doc-prettyArgsG = prettyArgsG' ", "--prettyArgsU :: (Pretty a) => Doc -> Doc -> [a] -> Doc-prettyArgsU = prettyArgs' ","--prettyArgs' :: (Pretty a) => Doc -> Doc -> Doc -> [a] -> Doc-prettyArgs' = fmap pretty -.*** prettyArgsG'--prettyArgs :: (Pretty a) => [a] -> Doc-prettyArgs = prettyArgs' ", " "(" ")"--fancyU :: [Universal] -> Doc-fancyU = foldMap pretty . reverse--(<#>) :: Doc -> Doc -> Doc-(<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b)---- FIXME figure out a nicer algorithm for when/how to split lines.--- aka don't use '</>' in places.-instance Pretty PreFunction where-    pretty (PreF i si [] [] [NoArgs] (Just rt) Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack-    pretty (PreF i si [] [] as (Just rt) Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] [] as (Just rt) (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] us as (Just rt) (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] us [NoArgs] (Just rt) Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] us as (Just rt) Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus [] as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus [] as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus us as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si pus us as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)-    pretty (PreF i si [] [] as (Just rt) Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt-    pretty (PreF i si [] us [] (Just rt) Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt-    pretty (PreF i si [] us as (Just rt) Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt-    pretty (PreF i si pus us as (Just rt) Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt-    pretty _ = undefined--instance Pretty DataPropLeaf where-    pretty (DataPropLeaf us e Nothing)   = "|" <+> foldMap pretty (reverse us) <+> pretty e-    pretty (DataPropLeaf us e (Just e')) = "|" <+> foldMap pretty (reverse us) <+> pretty e <+> "of" <+> pretty e'--instance Pretty Declaration where-    pretty (AbsType _ s as Nothing)        = "abstype" <+> text s <> prettyArgs as-    pretty (AbsViewType _ s as Nothing)    = "absvtype" <+> text s <> prettyArgs as-    pretty (AbsViewType _ s as (Just t))   = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t-    pretty (SumViewType s [] ls)           = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls-    pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls-    pretty (SumType s [] ls)               = "datatype" <+> text s <+> "=" <$> prettyLeaf ls-    pretty (SumType s as ls)               = "datatype" <+> text s <> prettyArgs as <+> "=" <$> 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 (Just t) p Nothing e)      = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e-    pretty (Var Nothing p e Nothing)       = "var" <+> pretty p <+> "=" <+> pretty e-    pretty (Var (Just t) p e Nothing)      = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e-    pretty (Include s)                     = "#include" <+> pretty s-    pretty (Staload Nothing s)             = "staload" <+> pretty s-    pretty (Staload (Just q) s)            = "staload" <+> pretty q <+> "=" <+> pretty s-    pretty (CBlock s)                      = string s-    pretty (Comment s)                     = string s-    pretty (OverloadOp _ o n)              = "overload" <+> pretty o <+> "with" <+> pretty n-    pretty (OverloadIdent _ i n Nothing)   = "overload" <+> text i <+> "with" <+> pretty n-    pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n'-    -- We use 'text' here, which means indentation might get fucked up for-    -- C preprocessor macros, but you absolutely deserve it if you indent your-    -- macros.-    pretty (Define s)                      = text s-    pretty (Func _ (Fn pref))              = "fn" </> pretty pref-    pretty (Func _ (Fun pref))             = "fun" </> pretty pref-    pretty (Func _ (CastFn pref))          = "castfn" </> pretty pref-    pretty (Func _ (Fnx pref))             = "fnx" </> pretty pref-    pretty (Func _ (And pref))             = "and" </> pretty pref-    pretty (Func _ (Praxi pref))           = "praxi" </> pretty pref-    pretty (Func _ (PrFun pref))           = "prfun" </> pretty pref-    pretty (Func _ (PrFn pref))            = "prfn" </> pretty pref-    pretty (Extern _ d)                    = "extern" <$> pretty d-    pretty (DataProp _ s as ls)            = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls-    pretty (ViewTypeDef _ s [] t)          = "vtypedef" <+> text s <+> "=" <#> pretty t-    pretty (ViewTypeDef _ s as t)          = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t-    pretty (TypeDef _ s [] t)              = "typedef" <+> text s <+> "=" <+> pretty t-    pretty (TypeDef _ s as t)              = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t-    pretty (AbsProp _ n as)                = "absprop" <+> text n <+> prettyArgs as-    pretty (Assume n as e)                 = "assume" </> pretty n <> prettyArgs as <+> "=" </> pretty e-    pretty (SymIntr _ n)                   = "symintr" <+> pretty n-    pretty (Stacst _ n t Nothing)          = "stacst" </> pretty n <+> ":" </> pretty t-    pretty (Stacst _ n t (Just e))         = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e-    pretty (PropDef _ s as t)              = "propdef" </> text s <+> prettyArgs as <+> "=" </> pretty t-    pretty (Local _ d d')                  = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"-    pretty _                               = undefined

@@ -1,361 +0,0 @@-{-# LANGUAGE DeriveAnyClass             #-}-{-# LANGUAGE DeriveDataTypeable         #-}-{-# LANGUAGE DeriveFoldable             #-}-{-# LANGUAGE DeriveFunctor              #-}-{-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE DeriveTraversable          #-}-{-# LANGUAGE DerivingStrategies         #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE LambdaCase                 #-}-{-# LANGUAGE TemplateHaskell            #-}-{-# LANGUAGE TypeFamilies               #-}---- | This is a module containing types to model the ATS syntax tree. As it is--- collapsed by the pretty printer, you may see that in some places it is--- 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 (..)-    , Paired (..)-    , Leaf (..)-    , StaticExpression (..)-    , StaticExpressionF (..)-    , Fixity (..)-    , StackFunction (..)-    , rewriteATS-    , rewriteDecl-    -- * Lenses-    , leaves-    , constructorUniversals-    ) where--import           Control.DeepSeq          (NFData)-import           Control.Lens-import           Data.Functor.Foldable    (ListF (Cons), ana, cata, embed, project)-import           Data.Functor.Foldable.TH (makeBaseFunctor)-import           Data.Maybe               (isJust)-import           Data.Semigroup           (Semigroup)-import           GHC.Generics             (Generic)-import           Language.ATS.Lexer       (Addendum (..), AlexPosn)--data Fixity = RightFix AlexPosn-            | LeftFix AlexPosn-            | Pre AlexPosn-            | Post AlexPosn-            deriving (Show, Eq, Generic, NFData)---- | Newtype wrapper containing a list of declarations-newtype ATS = ATS { unATS :: [Declaration] }-    deriving (Show, Eq, Generic)-    deriving newtype (NFData, Semigroup, Monoid)--data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [String], maybeType :: Maybe Type }-    deriving (Show, Eq, Generic, NFData)---- | Declare something in a scope (a function, value, action, etc.)-data Declaration = Func AlexPosn Function-                 | Impl [Arg] Implementation-                 | ProofImpl Implementation -- primplmnt -- TODO add args-                 | Val Addendum (Maybe Type) Pattern Expression-                 | StaVal [Universal] String Type-                 | PrVal Pattern Expression-                 | Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression) -- TODO AlexPosn-                 | AndDecl (Maybe Type) Pattern Expression-                 | Include String-                 | Staload (Maybe String) String-                 | Stadef String Name [Type]-                 | CBlock String-                 | TypeDef AlexPosn String [Arg] Type-                 | ViewTypeDef AlexPosn String [Arg] Type-                 | SumType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }-                 | SumViewType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }-                 | AbsType AlexPosn String [Arg] (Maybe Type)-                 | AbsViewType AlexPosn String [Arg] (Maybe Type)-                 | AbsView AlexPosn String [Arg] (Maybe Type)-                 | AbsVT0p AlexPosn String [Arg] (Maybe Type)-                 | AbsT0p AlexPosn String Type-                 | ViewDef AlexPosn String [Arg] Type-                 | OverloadOp AlexPosn BinOp Name-                 | OverloadIdent AlexPosn String Name (Maybe Int)-                 | Comment String-                 | DataProp AlexPosn String [Arg] [DataPropLeaf]-                 | Extern AlexPosn Declaration-                 | Define String-                 | SortDef AlexPosn String Type-                 | AndD Declaration Declaration-                 | Local AlexPosn ATS ATS-                 | AbsProp AlexPosn String [Arg]-                 | Assume Name [Arg] Expression-                 | TKind AlexPosn Name String-                 | SymIntr AlexPosn Name-                 | Stacst AlexPosn Name Type (Maybe Expression)-                 | PropDef AlexPosn String [Arg] Type-                 -- uses an 'Int' because you fully deserve what you get if your-                 -- fixity declarations overflow.-                 | FixityDecl Fixity (Maybe Int) [String]-                 deriving (Show, Eq, Generic, NFData)--data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)-                  deriving (Show, Eq, Generic, NFData)---- | A type for parsed ATS types-data Type = Bool-          | Void-          | String-          | Char-          | Int-          | Nat-          | Addr-          | DependentInt StaticExpression-          | DependentBool StaticExpression-          | DepString StaticExpression-          | Double-          | Float-          | Tuple AlexPosn [Type]-          | Named Name-          | 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 (Maybe Type) Type-          | ProofType AlexPosn Type Type -- Aka (prf | val)-          | ConcreteType StaticExpression-          | RefType Type-          | ViewType AlexPosn Type-          | FunctionType String Type Type-          | NoneType AlexPosn-          | ImplicitType AlexPosn-          | ViewLiteral Addendum-          | AnonymousRecord AlexPosn [(String, Type)]-          deriving (Show, Eq, Generic, NFData)---- | A type for the various lambda arrows (@=>@, @=\<cloref1>@, etc.)-data LambdaType = Plain AlexPosn-                | Full AlexPosn String-                | Spear AlexPosn-                deriving (Show, Eq, Generic, NFData)---- | A name can be qualified (@$UN.unsafefn@) or not-data Name = Unqualified String-          | Qualified AlexPosn String String-          | SpecialName AlexPosn String-          | Functorial String String-          | Unnamed AlexPosn-          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]-             | TuplePattern [Pattern]-             | AtPattern AlexPosn Pattern-             | UniversalPattern AlexPosn String [Universal] Pattern-             | ExistentialPattern Existential Pattern-             deriving (Show, Eq, Generic, NFData)--data Paired a b = Both a b-                | First a-                | Second b-                deriving (Show, Eq, Generic, NFData)---- | An argument to a function.-data Arg = Arg (Paired String Type)-         | PrfArg Arg Arg-         | NoArgs-    deriving (Show, Eq, Generic, NFData)---- | Wrapper for universal quantifiers (refinement types)-data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe StaticExpression } -- TODO NonEmpty type?-    deriving (Show, Eq, Generic, NFData)---- | Wrapper for existential quantifiers/types-data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }-    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-           | StaticEq-           | Mod-           deriving (Show, Eq, Generic, NFData)---- FIXME add position information?-data StaticExpression = StaticVal Name-                      | StaticBinary BinOp StaticExpression StaticExpression-                      | StaticInt Int-                      | SPrecede StaticExpression StaticExpression-                      | StaticBool Bool-                      | StaticVoid AlexPosn-                      | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)-                      | SCall Name [StaticExpression]-                      deriving (Show, Eq, Generic, NFData)---- | A (possibly effectful) expression.-data Expression = Let AlexPosn ATS (Maybe Expression)-                | VoidLiteral -- The '()' literal representing inaction.-                    AlexPosn-                -- function call: <a>, then {n}-                | Call Name [Type] [Type] (Maybe Expression) [Expression]-                | NamedVal Name-                | ListLiteral AlexPosn String Type [Expression]-                | If { cond     :: Expression -- ^ Expression evaluating to a boolean value-                     , whenTrue :: Expression -- ^ Expression to be returned when true-                     , elseExpr :: Maybe Expression -- ^ Expression to be returned when false-                     }-                | 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-                | AddrAt AlexPosn Expression-                | ViewAt AlexPosn Expression-                | Binary BinOp Expression Expression-                | Unary UnOp Expression-                | Case { posE :: AlexPosn-                       , kind :: Addendum-                       , val  :: Expression-                       , arms :: [(Pattern, LambdaType, 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-                              }-                | Mutate Expression Expression-                | Deref AlexPosn Expression-                | ProofExpr AlexPosn Expression Expression-                | TypeSignature Expression Type-                | WhereExp Expression [Declaration]-                | TupleEx AlexPosn [Expression]-                | While AlexPosn Expression Expression-                | Actions ATS-                | Begin AlexPosn Expression-                | BinList { _op :: BinOp, _exprs :: [Expression] }-                | PrecedeList { _exprs :: [Expression] }-                | FixAt String StackFunction-                | LambdaAt StackFunction-                | ParenExpr AlexPosn Expression-                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-              | Fn PreFunction-              | Fnx PreFunction-              | And PreFunction-              | PrFun PreFunction-              | PrFn PreFunction-              | Praxi PreFunction-              | CastFn PreFunction-              deriving (Show, Eq, Generic, NFData)--data StackFunction = StackF { stSig        :: String-                            , stArgs       :: [Arg]-                            , stReturnType :: Type-                            , stExpression :: Expression-                            }-                            deriving (Show, Eq, Generic, NFData)--data PreFunction = PreF { fname         :: Name -- ^ Function name-                        , sig           :: String -- ^ e.g. <> or \<!wrt>-                        , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic-                        , universals    :: [Universal] -- ^ Universal quantifiers/refinement type-                        , args          :: [Arg] -- ^ Actual function arguments-                        , returnType    :: Maybe Type -- ^ Return type-                        , termetric     :: Maybe StaticExpression -- ^ 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 ''StaticExpression-makeBaseFunctor ''Type-makeLenses ''Leaf-makeLenses ''Declaration--rewriteDecl :: Declaration -> Declaration-rewriteDecl x@SumViewType{} = g x-    where g = over (leaves.mapped.constructorUniversals) h-          h :: [Universal] -> [Universal]-          h = ana c where-            c (y:y':ys)-                | typeU y == typeU y' && isJust (typeU y) =-                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys-            c y = project y-rewriteDecl x = x---- precedence: rewrite n + 2 * x to n + (2 * x)--- TODO: rewrite multiple universals when it's the right context?-rewriteATS :: Expression -> Expression-rewriteATS = cata a where-    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]-    a (CallF n ts ts' me [ParenExpr _ e@Call{}])     = Call n ts ts' me [e]-    a (PrecedeF e e'@PrecedeList{})                  = PrecedeList (e : _exprs e')-    a (PrecedeF e e')                                = PrecedeList [e, e']-    a (BinaryF Mult (Binary Add e e') e'')           = Binary Add e (Binary Mult e' e'')-    a (BinaryF Add e (BinList Add es))               = BinList Add (e : es)-    a (BinaryF Add e e')                             = BinList Add [e, e']-    a (ParenExprF _ e@Precede{})                     = e-    a (ParenExprF _ e@PrecedeList{})                 = e-    a x                                              = embed x

@@ -9,6 +9,7 @@   - dirstream-1.0.3   - hspec-dirstream-0.3.0.0   - cli-setup-0.1.0.3+  - language-ats-0.1.0.0 flags:   ats-format:     development: false

@@ -1,14 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--import qualified Filesystem.Path.CurrentOS as F-import           Language.ATS-import           Test.Hspec-import           Test.Hspec.Dirstream--isATS :: F.FilePath -> Bool-isATS x = (extension x `elem`) (pure <$> ["ats", "dats", "sats", "hats", "cats"])--main :: IO ()-main = hspec $-    describe "pretty-print" $ parallel $-        testFiles "test/data" isATS (fmap printATS . parseATS . lexATS)

@@ -1,40 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "contrib/atscntrb-hx-intinf/SATS/intinf_t.sats"-staload "libats/libc/SATS/math.sats"-staload "contrib/atscntrb-hx-intinf/SATS/intinf.sats"-staload UN = "prelude/SATS/unsafe.sats"--fnx fact {n : nat} .<n>. (k : int(n)) : [ n : nat | n > 0 ] intinf(n) =-  case+ k of-    | 0 => int2intinf(1)-    | 1 => int2intinf(1)-    | k =>> $UN.cast(fact(k - 1) * k)--// double factorial http://mathworld.wolfram.com/DoubleFactorial.html-fnx dfact {n : nat} .<n>. (k : int(n)) : Intinf =-  case+ k of-    | 0 => int2intinf(1)-    | 1 => int2intinf(1)-    | k =>> k * dfact(k - 2)--// Number of permutations on n objects using k at a time.-fn permutatsions {n : nat}{ k : nat | k <= n } (n : int(n), k : int(k)) : Intinf =-  ndiv(fact(n), fact(n - k))--// Number of permutations on n objects using k at a time.-fn choose {n : nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : Intinf =-  let-    fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : [ n : nat | n > 0 ] intinf(n) =-      case+ i of-        | 1 => int2intinf(n)-        | 2 => $UN.cast(int2intinf(n - 1) * n)-        | i =>> $UN.cast((n + 1 - i) * numerator_loop(i - 1))-  in-    case+ k of-      | 0 => int2intinf(1)-      | 1 => int2intinf(n)-      | k =>> ndiv(numerator_loop(k), fact(k))-  end

@@ -1,43 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "contrib/atscntrb-hx-intinf/SATS/intinf_t.sats"-staload "libats/libc/SATS/math.sats"-staload "contrib/atscntrb-hx-intinf/SATS/intinf.sats"-staload UN = "prelude/SATS/unsafe.sats"--fnx fact {n:nat} .<n>. (k : int(n)) : [ n : nat | n > 0 ] intinf(n) =-  case+ k of-    | 0 => int2intinf(1)-    | 1 => int2intinf(1)-    | k =>> $UN.cast(fact(k - 1) * k)--// double factorial http://mathworld.wolfram.com/DoubleFactorial.html-fnx dfact {n:nat} .<n>. (k : int(n)) : Intinf =-  case+ k of-    | 0 => int2intinf(1)-    | 1 => int2intinf(1)-    | k =>> k * dfact(k - 2)--// Number of permutations on n objects using k at a time.-fn permutatsions {n:nat}{ k : nat | k <= n } (n : int(n), k : int(k)) :-  Intinf =-  ndiv(fact(n), fact(n - k))--// Number of permutations on n objects using k at a time.-fn choose {n:nat}{ m : nat | m <= n } (n : int(n), k : int(m)) :-  Intinf =-  let-    fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) :-      [ n : nat | n > 0 ] intinf(n) =-      case+ i of-        | 1 => int2intinf(n)-        | 2 => $UN.cast(int2intinf(n - 1) * n)-        | i =>> $UN.cast((n + 1 - i) * numerator_loop(i - 1))-  in-    case+ k of-      | 0 => int2intinf(1)-      | 1 => int2intinf(n)-      | k =>> ndiv(numerator_loop(k), fact(k))-  end

@@ -1,257 +0,0 @@-// This is mostly taken from the example in the book.--#include "share/atspre_staload.hats"-#include "share/atspre_staload_libats_ML.hats"-#include "libats/DATS/athread_posix.dats"--staload "libats/SATS/athread.sats"-staload "src/filetype.sats"-staload "libats/SATS/funarray.sats"-staload "libats/SATS/deqarray.sats"-staload _ = "libats/DATS/deqarray.dats"--absvtype queue_vtype(a: vt@ype+, int) = ptr--vtypedef queue(a: vt0p, id: int) = queue_vtype(a, id)-vtypedef queue(a: vt0p) = [id:int] queue(a, id)--absprop ISNIL(id: int, b: bool)--extern fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) : [b:bool] (ISNIL(id, b) | bool(b))--absprop ISFULL(id: int, b: bool)--extern fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) : [b:bool] (ISFULL(id, b) | bool(b))--extern fun {a:vt0p} queue_insert {id:int} (ISFULL(id, false) | xs: !queue(a, id) >> queue(a, id2), x: a) : #[id2:int] void--extern fun {a:vt0p} queue_remove {id:int} (ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2)) : #[id2:int] a--extern fun {a:vt0p} queue_make (cap: intGt(0)) : queue(a)--extern fun {a:t@ype} queue_free(que: queue(a)) : void--assume queue_vtype(a: vt0p, id: int) = deqarray(a)-assume ISNIL(id: int, b: bool) = unit_p-assume ISFULL(id: int, b: bool) = unit_p--absvtype channel_vtype(a: vt@ype+) = ptr--vtypedef channel(a: vt0p) = channel_vtype(a)--extern fun {a:vt0p} channel_insert (!channel(a), a) : void--extern fun {a:vt0p} channel_remove (chan: !channel(a)) : a--extern fun {a:vt0p} channel_remove_helper (chan: !channel(a), !queue(a) >> _) : a--extern fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) : void--datavtype channel_ = {l0,l1,l2,l3:agz} CHANNEL of-                                       @{ cap = intGt(0)-                                        , spin = spin_vt(l0)-                                        , refcount = intGt(0)-                                        , mutex = mutex_vt(l1)-                                        , CVisNil = condvar_vt(l2)-                                        , CVisFull = condvar_vt(l3)-                                        , queue = ptr-                                        }--extern fun {a:vt0p} channel_make(cap: intGt(0)) : channel(a)--extern fun {a:vt0p} channel_ref(ch: !channel(a)) : channel(a)--extern fun {a:vt0p} channel_unref(ch: channel(a)) : Option_vt(queue(a))--extern fun channel_refcount{a:vt0p}(ch: !channel(a)) : intGt(0)--assume channel_vtype(a:vt0p) = channel_--implement {a} queue_is_nil(xs) = (unit_p() | deqarray_is_nil(xs))--implement {a} queue_is_full(xs) = (unit_p() | deqarray_is_full(xs))--implement {a} queue_remove(prf | xs) = -  let-    prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISNIL(id, false)) : [false] void }-  in-    deqarray_takeout_atbeg<a> (xs)-  end--implement {a} queue_insert(prf | xs, x) = -  { -    prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISFULL(id, false)) : [false] void }-    val () = deqarray_insert_atend<a>(xs, x)-  }--implement {a} queue_make(cap) = deqarray_make_cap(i2sz(cap))--implement {a} queue_free(que) = deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))--implement {a} channel_ref(chan) =-  let-    val@ CHANNEL(ch) = chan-    val spin = unsafe_spin_vt2t(ch.spin)-    val (prf | ()) = spin_lock(spin)-    val () = ch.refcount := ch.refcount + 1-    val () = spin_unlock (prf | spin)-    prval () = fold@(chan)-  in-    $UN.castvwtp1{channel(a)}(chan)-  end--implement {a} channel_unref(chan) = -  let-    val@ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val spin = unsafe_spin_vt2t(ch.spin)-    val (prf | ()) = spin_lock(spin)-    val () = spin_unlock(prf | spin)-    val refcount = ch.refcount // needed to make the theorem prover work-  in-    if refcount <= 1 then-      let-        val que = $UN.castvwtp0{queue(a)}(ch.queue)-        val () = spin_vt_destroy(ch.spin)-        val () = mutex_vt_destroy(ch.mutex)-        val () = condvar_vt_destroy(ch.CVisNil)-        val () = condvar_vt_destroy(ch.CVisFull)-        val () = free@{l0,l1,l2,l3}(chan)-      in-        Some_vt(que)-      end-    else-      let-        val () = ch.refcount := refcount - 1-        prval () = fold@chan-        prval () = $UN.cast2void(chan)-      in-        None_vt()-      end-  end--implement channel_refcount{a}(chan) =-  let-    val@ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val refcount = ch.refcount-  in-    fold@(chan) ; refcount-  end--implement {a} channel_make(cap) = -  let-    extern praxi __assert() : [l:agz] void--    prval [l0:addr] () = __assert()-    prval [l1:addr] () = __assert()-    prval [l2:addr] () = __assert()-    prval [l3:addr] () = __assert()--    val chan = CHANNEL{l0,l1,l2,l3}(_)-    val+ CHANNEL(ch) = chan--    val () = ch.cap := cap-    val () = ch.refcount := 1-    -    local -      val x = spin_create_exn()-    in-      val () = ch.spin := unsafe_spin_t2vt(x)-    end--    local-      val x = mutex_create_exn()-    in-      val () = ch.mutex := unsafe_mutex_t2vt(x)-    end--    local-      val x = condvar_create_exn()-    in-      val () = ch.CVisNil := unsafe_condvar_t2vt(x)-    end--    local-      val x = condvar_create_exn()-    in-      val () = ch.CVisFull := unsafe_condvar_t2vt(x)-    end--    val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))--    in-      fold@(chan) ; chan-    end--implement {a} channel_insert(chan, x) = -  let-    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val mutex = unsafe_mutex_vt2t(ch.mutex)-    val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))-    val () = channel_insert_helper<a>(chan, xs, x)-    prval prf = $UN.castview0{locked_v(l1)}(xs)-    val () = mutex_unlock(prf | mutex)-  in-  end--implement {a} channel_remove(chan) = x where-  {-    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val mutex = unsafe_mutex_vt2t(ch.mutex)-    val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))-    val x = channel_remove_helper<a> (chan, xs)-    prval prf = $UN.castview0{locked_v(l1)}(xs)-    val () = mutex_unlock(prf | mutex)-  }--implement {a} channel_remove_helper(chan, xs) =-  let-    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val (prf | is_nil) = queue_is_nil(xs)-  in-    if is_nil then-      let-        prval (pfmut, fpf) = __assert() where { extern praxi __assert(): vtakeout0(locked_v(l1)) }-        val mutex = unsafe_mutex_vt2t(ch.mutex)-        val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)-        val () = condvar_wait(pfmut | CVisNil, mutex)-        prval () = fpf(pfmut)-      in-        channel_remove_helper(chan, xs)-      end-    else-      let-        val is_full = queue_is_full(xs)-        val x_out = queue_remove(prf | xs)-        val () = if is_full.1 then-          condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))-      in-        x_out-      end-  end--implement {a} channel_insert_helper(chan, xs, x) = -  let-    val+ CHANNEL{l0,l1,l2,l3}(ch) = chan-    val (prf | is_full) = queue_is_full(xs)-  in-    if is_full then-      let-        prval (pfmut, fpf) = __assert() where { extern praxi __assert() : vtakeout0(locked_v(l1)) }-        val mutex = unsafe_mutex_vt2t(ch.mutex)-        val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)-        val () = condvar_wait(pfmut | CVisFull, mutex)-        prval () = fpf(pfmut)-      in-        channel_insert_helper(chan, xs, x)-      end-    else-      let-        val is_nil = queue_is_nil(xs)-        val () = queue_insert(prf | xs, x)-        val () = if is_nil.1 then-          condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))-      in-      end-  end  

@@ -1,287 +0,0 @@-// This is mostly taken from the example in the book.-#include "share/atspre_staload.hats"-#include "share/atspre_staload_libats_ML.hats"-#include "libats/DATS/athread_posix.dats"--staload "libats/SATS/athread.sats"-staload "src/filetype.sats"-staload "libats/SATS/funarray.sats"-staload "libats/SATS/deqarray.sats"-staload _ = "libats/DATS/deqarray.dats"--absvtype queue_vtype(a : vt@ype+, int) = ptr--vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id)-vtypedef queue(a : vt0p) = [id:int] queue(a, id)--absprop ISNIL (id : int, b : bool)--extern-fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) :-  [b:bool] (ISNIL(id, b) | bool(b))--absprop ISFULL (id : int, b : bool)--extern-fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) :-  [b:bool] (ISFULL(id, b) | bool(b))--extern-fun {a:vt0p} queue_insert {id:int}-(ISFULL(id,false) | xs : !queue(a, id) >> queue(a, id2), x : a) :-  #[id2:int] void--extern-fun {a:vt0p} queue_remove {id:int}-(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : #[id2:int] a--extern-fun {a:vt0p} queue_make  (cap : intGt(0)) : queue(a)--extern-fun {a:t@ype} queue_free  (que : queue(a)) : void--assume queue_vtype(a : vt0p, id : int) = deqarray(a)--assume ISNIL(id : int, b : bool) = unit_p--assume ISFULL(id : int, b : bool) = unit_p--absvtype channel_vtype(a : vt@ype+) = ptr--vtypedef channel(a : vt0p) = channel_vtype(a)--extern-fun {a:vt0p} channel_insert  (!channel(a), a) : void--extern-fun {a:vt0p} channel_remove  (chan : !channel(a)) : a--extern-fun {a:vt0p} channel_remove_helper  ( chan : !channel(a)-                                    , !queue(a) >> _-                                    ) : a--extern-fun {a:vt0p} channel_insert_helper  (!channel(a), !queue(a) >> _, a) :-  void--datavtype channel_ =-  | { l0, l1, l2, l3 : agz } CHANNEL of @{ cap = intGt(0)-                                         , spin = spin_vt(l0)-                                         , refcount = intGt(0)-                                         , mutex = mutex_vt(l1)-                                         , CVisNil = condvar_vt(l2)-                                         , CVisFull = condvar_vt(l3)-                                         , queue = ptr-                                         }--extern-fun {a:vt0p} channel_make  (cap : intGt(0)) : channel(a)--extern-fun {a:vt0p} channel_ref  (ch : !channel(a)) : channel(a)--extern-fun {a:vt0p} channel_unref  (ch : channel(a)) : Option_vt(queue(a))--extern-fun channel_refcount {a:vt0p} (ch : !channel(a)) : intGt(0)--assume channel_vtype(a : vt0p) = channel_--implement {a} queue_is_nil (xs) =-  (unit_p() | deqarray_is_nil(xs))--implement {a} queue_is_full (xs) =-  (unit_p() | deqarray_is_full(xs))--implement {a} queue_remove (prf | xs) =-  let-    prval () = __assert(prf) where-    { extern-      praxi __assert {id:int} (p : ISNIL(id, false)) : [ false ] void }-  in-    deqarray_takeout_atbeg<a>(xs)-  end--implement {a} queue_insert (prf | xs, x) =-  {-    prval () = __assert(prf) where-    { extern-      praxi __assert {id:int} (p : ISFULL(id, false)) : [ false ] void }-    val () = deqarray_insert_atend<a>(xs, x)-  }--implement {a} queue_make (cap) =-  deqarray_make_cap(i2sz(cap))--implement {a} queue_free (que) =-  deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))--implement {a} channel_ref (chan) =-  let-    val @CHANNEL (ch) = chan-    val spin = unsafe_spin_vt2t(ch.spin)-    val (prf | ()) = spin_lock(spin)-    val () = ch.refcount := ch.refcount + 1-    val () = spin_unlock(prf | spin)-    prval () = fold@(chan)-  in-    $UN.castvwtp1{channel(a)}(chan)-  end--implement {a} channel_unref (chan) =-  let-    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val spin = unsafe_spin_vt2t(ch.spin)-    val (prf | ()) = spin_lock(spin)-    val () = spin_unlock(prf | spin)-    val refcount = ch.refcount-  in-    if refcount <= 1 then-      let-        val que = $UN.castvwtp0{queue(a)}(ch.queue)-        val () = spin_vt_destroy(ch.spin)-        val () = mutex_vt_destroy(ch.mutex)-        val () = condvar_vt_destroy(ch.CVisNil)-        val () = condvar_vt_destroy(ch.CVisFull)-        val () = free@{l0,l1,l2,l3}(chan)-      in-        Some_vt(que)-      end-    else-      let-        val () = ch.refcount := refcount - 1-        prval () = fold@(chan)-        prval () = $UN.cast2void(chan)-      in-        None_vt()-      end-  end--implement channel_refcount {a} (chan) =-  let-    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val refcount = ch.refcount-  in-    (fold@(chan) ; refcount)-  end--implement {a} channel_make (cap) =-  let-    extern-    praxi __assert() : [l:agz] void-    -    prval [l0:addr]() = __assert()-    prval [l1:addr]() = __assert()-    prval [l2:addr]() = __assert()-    prval [l3:addr]() = __assert()-    val chan = CHANNEL{l0,l1,l2,l3}(_)-    val+ CHANNEL (ch) = chan-    val () = ch.cap := cap-    val () = ch.refcount := 1-    -    local-      val x = spin_create_exn()-    in-      val () = ch.spin := unsafe_spin_t2vt(x)-    end-    -    local-      val x = mutex_create_exn()-    in-      val () = ch.mutex := unsafe_mutex_t2vt(x)-    end-    -    local-      val x = condvar_create_exn()-    in-      val () = ch.CVisNil := unsafe_condvar_t2vt(x)-    end-    -    local-      val x = condvar_create_exn()-    in-      val () = ch.CVisFull := unsafe_condvar_t2vt(x)-    end-    -    val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))-  in-    (fold@(chan) ; chan)-  end--implement {a} channel_insert (chan, x) =-  let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val mutex = unsafe_mutex_vt2t(ch.mutex)-    val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))-    val () = channel_insert_helper<a>(chan, xs, x)-    prval prf = $UN.castview0{locked_v(l1)}(xs)-    val () = mutex_unlock(prf | mutex)-  in end--implement {a} channel_remove (chan) =-  x where-  { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val mutex = unsafe_mutex_vt2t(ch.mutex)-    val (prf | ()) = mutex_lock(mutex)-    val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))-    val x = channel_remove_helper<a>(chan, xs)-    prval prf = $UN.castview0{locked_v(l1)}(xs)-    val () = mutex_unlock(prf | mutex) }--implement {a} channel_remove_helper (chan, xs) =-  let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val (prf | is_nil) = queue_is_nil(xs)-  in-    if is_nil then-      let-        prval (pfmut, fpf) = __assert() where-        { extern-          praxi __assert() : vtakeout0(locked_v(l1)) }-        val mutex = unsafe_mutex_vt2t(ch.mutex)-        val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)-        val () = condvar_wait(pfmut | CVisNil, mutex)-        prval () = fpf(pfmut)-      in-        channel_remove_helper(chan, xs)-      end-    else-      let-        val is_full = queue_is_full(xs)-        val x_out = queue_remove(prf | xs)-        val () = if is_full.1 then-          condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))-      in-        x_out-      end-  end--implement {a} channel_insert_helper (chan, xs, x) =-  let-    val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan-    val (prf | is_full) = queue_is_full(xs)-  in-    if is_full then-      let-        prval (pfmut, fpf) = __assert() where-        { extern-          praxi __assert() : vtakeout0(locked_v(l1)) }-        val mutex = unsafe_mutex_vt2t(ch.mutex)-        val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)-        val () = condvar_wait(pfmut | CVisFull, mutex)-        prval () = fpf(pfmut)-      in-        channel_insert_helper(chan, xs, x)-      end-    else-      let-        val is_nil = queue_is_nil(xs)-        val () = queue_insert(prf | xs, x)-        val () = if is_nil.1 then-          condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))-      in end-  end

@@ -1,32 +0,0 @@-#include "share/atspre_staload.hats"-#include "share/HATS/atslib_staload_libats_libc.hats"--fnx fact_boring(n: int) : int =-  case+ n of-    | 0 => 1-    | n => n * fact_boring(n-1)--(* fnx collatz{n:nat} *)-(* (n: int(n)) : int = let *)-(* fun loop{n:nat}{l:addr} .<n>. *)-(* (pf: !int @ l | n: int n, res: ptr l) : void = *)-(* if n > 1  *)--// TODO rewrite this for collatz?-fnx fact{n:nat}-(n: int (n)): int = let-fun loop{n:nat}{l:addr} .<n>.-(pf: !int @ l | n: int n, res: ptr l): void =-if n > 0 then let-val () = !res := n * !res in loop (pf | n-1, res)-end // end of [if]-// end of [loop]-var res: int with pf = 1-val () = loop (pf | n, addr@res) // addr@res: the pointer to res-in-res-end // end of [fact]--implement main0 () =-  let val x = fact(30) in-  println!(tostring_int(x)) end

@@ -1,39 +0,0 @@-#include "share/atspre_staload.hats"-#include "share/HATS/atslib_staload_libats_libc.hats"--fnx fact_boring(n : int) : int =-  case+ n of-    | 0 => 1-    | n => n * fact_boring(n - 1)--(* fnx collatz{n:nat} *)-(* (n: int(n)) : int = let *)-(* fun loop{n:nat}{l:addr} .<n>. *)-(* (pf: !int @ l | n: int n, res: ptr l) : void = *)-(* if n > 1  *)-// TODO rewrite this for collatz?-fnx fact {n:nat} (n : int(n)) : int =-  let-    fun loop {n:nat}{l:addr} .<n>. ( pf : !int @ l | n : int(n)-                                   , res : ptr(l)-                                   ) : void =-      if n > 0 then-        let-          val () = !res := n * !res-        in-          loop(pf | n - 1, res)-        end-    -    // end of [loop]-    var res: int with pf = 1-    val () = loop(pf | n, addr@res)-  in-    res-  end--implement main0 () =-  let-    val x = fact(30)-  in-    println!(tostring_int(x))-  end

@@ -1,4 +0,0 @@-fun factorial_recursion {n:nat} .<n>. (n: int(n)) : int =-case+ n of-| 0 => 1-| n =>> factorial_recursion(n-1) * n

@@ -1,4 +0,0 @@-fun factorial_recursion {n:nat} .<n>. (n : int(n)) : int =-  case+ n of-    | 0 => 1-    | n =>> factorial_recursion(n - 1) * n

@@ -1,93 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "libats/libc/SATS/math.sats"--fnx fact {n : nat} .<n>. (k : int(n)) :<> int =-  case+ k of-    | 0 => 1-    | k =>> fact(k - 1) * k--fnx dfact {n : nat} .<n>. (k : int(n)) :<> int =-  case+ k of-    | 0 => 1-    | 1 => 1-    | k =>> k * dfact(k - 2)--// TODO make this more versatile?-fn choose {n : nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : int =-  let-    fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : int =-      case+ i of-        | 1 => n-        | 2 => (n - 1) * n-        | i =>> (n + 1 - i) * numerator_loop(i - 1)-  in-    case+ k of-      | 0 => 1-      | 1 => n-      | k =>> numerator_loop(k) / fact(k)-  end--// FIXME-fun bad(n : int) : [ m : nat ] int(m) =-  case+ n of-    | 0 => 0-    | n => 1 + bad(n - 1)--fun is_prime(k : intGt(0)) : bool =-  case+ k of-    | 1 => false-    | k => -      begin-        let-          var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))-          var bound: [ m : nat ] int(m) = bad(pre_bound)-          -          fun loop {n : nat}{m : nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<> bool =-            if i < bound then-              if k mod i = 0 then-                false-              else-                true && loop(i + 1, bound)-            else-              if i = bound then-                if k mod i = 0 then-                  false-                else-                  true-              else-                true-        in-          loop(2, bound)-        end-      end--extern-fun choose_ats {n : nat}{ m : nat | m <= n } : (int(n), int(m)) -> int =-  "mac#"--extern-fun double_factorial {n : nat} : int(n) -> int =-  "mac#"--extern-fun factorial_ats {n : nat} : int(n) -> int =-  "mac#"--extern-fun is_prime_ats { n : nat | n > 0 } : int(n) -> bool =-  "mac#"--implement choose_ats (n, k) =-  choose(n, k)--implement double_factorial (m) =-  dfact(m)--implement is_prime_ats (n) =-  is_prime(n)--implement factorial_ats (m) =-  fact(m)

@@ -1,94 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "libats/libc/SATS/math.sats"--fnx fact {n:nat} .<n>. (k : int(n)) :<> int =-  case+ k of-    | 0 => 1-    | k =>> fact(k - 1) * k--fnx dfact {n:nat} .<n>. (k : int(n)) :<> int =-  case+ k of-    | 0 => 1-    | 1 => 1-    | k =>> k * dfact(k - 2)--// TODO make this more versatile?-fn choose {n:nat}{ m : nat | m <= n } (n : int(n), k : int(m)) : int =-  let-    fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) : int =-      case+ i of-        | 1 => n-        | 2 => (n - 1) * n-        | i =>> (n + 1 - i) * numerator_loop(i - 1)-  in-    case+ k of-      | 0 => 1-      | 1 => n-      | k =>> numerator_loop(k) / fact(k)-  end--// FIXME-fun bad(n : int) : [m:nat] int(m) =-  case+ n of-    | 0 => 0-    | n => 1 + bad(n - 1)--fun is_prime(k : intGt(0)) : bool =-  case+ k of-    | 1 => false-    | k => -      begin-        let-          var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))-          var bound: [m:nat] int(m) = bad(pre_bound)-          -          fun loop {n:nat}{m:nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<>-            bool =-            if i < bound then-              if k % i = 0 then-                false-              else-                true && loop(i + 1, bound)-            else-              if i = bound then-                if k % i = 0 then-                  false-                else-                  true-              else-                true-        in-          loop(2, bound)-        end-      end--extern-fun choose_ats {n:nat}{ m : nat | m <= n } : (int(n), int(m)) -> int =-  "mac#"--extern-fun double_factorial {n:nat} : int(n) -> int =-  "mac#"--extern-fun factorial_ats {n:nat} : int(n) -> int =-  "mac#"--extern-fun is_prime_ats { n : nat | n > 0 } : int(n) -> bool =-  "mac#"--implement choose_ats (n, k) =-  choose(n, k)--implement double_factorial (m) =-  dfact(m)--implement is_prime_ats (n) =-  is_prime(n)--implement factorial_ats (m) =-  fact(m)

@@ -1,6 +0,0 @@-#include "prelude/DATS/integer.dats"--fnx fib { n : int | n >= 0 } .<n>. (i : int(n)) : int =-case+ i of-| _ when i - 2 >= 0 => ( fib(i-1) + fib(i-2) )-| _ => 1

@@ -1,6 +0,0 @@-#include "prelude/DATS/integer.dats"--fnx fib { n : int | n >= 0 } .<n>. (i : int(n)) : int =-  case+ i of-    | _ when i - 2 >= 0 => (fib(i - 1) + fib(i - 2))-    | _ => 1

@@ -1,31 +0,0 @@-#include "share/atspre_staload.hats"-#include "libats/ML/DATS/filebas_dirent.dats"-#include "libats/libc/DATS/dirent.dats"--staload "libats/ML/DATS/string.dats"--fun good_dir(next: string) : bool = case next of | "." => false | ".." => false | _ => true-fnx step_stream(acc: int, s: string) : int =-if test_file_isdir(s) != 0 then-flow_stream(s, acc + 1)-else-acc + 1-and flow_stream(s: string, init: int) : int =-let-var files = streamize_dirname_fname(s)-var ffiles = stream_vt_filter_cloptr(files, lam x => good_dir(x))-in-stream_vt_foldleft_cloptr(ffiles, init, lam (acc, next) => step_stream(acc, s + "/" + next))-end-fun count_files(s: string) : void =-let-var n: int = step_stream(0, g1ofg0(s))-in-println!(tostring_int(n))-end--implement main0 (argc, argv) =-if argc > 1 then-count_files(argv[1])-else-count_files(".")

@@ -1,41 +0,0 @@-#include "share/atspre_staload.hats"-#include "libats/ML/DATS/filebas_dirent.dats"-#include "libats/libc/DATS/dirent.dats"--staload "libats/ML/DATS/string.dats"--fun good_dir(next : string) : bool =-  case next of-    | "." => false-    | ".." => false-    | _ => true--fnx step_stream(acc : int, s : string) : int =-  if test_file_isdir(s) != 0 then-    flow_stream(s, acc + 1)-  else-    acc + 1-and flow_stream(s : string, init : int) : int =-  let-    var files = streamize_dirname_fname(s)-    var ffiles = stream_vt_filter_cloptr(files, lam x => good_dir(x))-  in-    stream_vt_foldleft_cloptr( ffiles-                             , init-                             , lam (acc, next) =>-                                 step_stream(acc, s + "/" + next)-                             )-  end--fun count_files(s : string) : void =-  let-    var n: int = step_stream(0, g1ofg0(s))-  in-    println!(tostring_int(n))-  end--implement main0 (argc, argv) =-  if argc > 1 then-    count_files(argv[1])-  else-    count_files(".")

@@ -1,180 +0,0 @@-// Type for a collection of files (monoidal)-typedef file = @{ lines = int, files = int }--// Type for the parsed command-line arguments. -typedef command_line = @{ version = bool-                        , help = bool-                        , table = bool-                        , excludes = [m:nat] list(string, m)-                        , includes = [m:nat] list(string, m)-                        }--// Program state, tracking *all* supported file types in an unboxed structure.-typedef source_contents = @{ rust = file-                           , haskell = file-                           , ats = file-                           , python = file-                           , vimscript = file-                           , elm = file-                           , idris = file-                           , madlang = file-                           , tex = file-                           , markdown = file-                           , yaml = file-                           , toml = file-                           , cabal = file-                           , happy = file-                           , alex = file-                           , go = file-                           , html = file-                           , css = file-                           , verilog = file-                           , vhdl = file-                           , c = file-                           , purescript = file-                           , futhark = file-                           , brainfuck = file-                           , ruby = file-                           , julia = file-                           , perl = file-                           , ocaml = file-                           , agda = file-                           , cobol = file-                           , tcl = file-                           , r = file-                           , lua = file-                           , cpp = file-                           , lalrpop = file-                           , header = file-                           , sixten = file-                           , dhall = file-                           , ipkg = file-                           , makefile = file-                           , justfile = file-                           , ion = file-                           , bash = file-                           , hamlet = file-                           , cassius = file-                           , lucius = file-                           , julius = file-                           , mercury = file-                           , yacc = file-                           , lex = file-                           , coq = file-                           , jupyter = file-                           , java = file-                           , scala = file-                           , erlang = file-                           , elixir = file-                           , pony = file-                           , clojure = file-                           , cabal_project = file-                           , assembly = file-                           , nix = file-                           , php = file-                           , javascript = file-                           , kotlin = file-                           , fsharp = file-                           , fortran = file-                           , swift = file-                           , csharp = file-                           , nim = file-                           , cpp_header = file-                           , elisp = file-                           , plaintext = file-                           , rakefile = file-                           , llvm = file-                           , autoconf = file-                           , batch = file-                           , powershell = file-                           , m4 = file-                           , objective_c = file-                           , automake = file-                           }--// Reference to source_contents; used to update the structure.-vtypedef source_contents_r = ref(source_contents)--// Sum type representing all supported data types.-datavtype pl_type =-  | unknown-  | rust of int-  | haskell of int-  | perl of int-  | verilog of int-  | vhdl of int-  | agda of int-  | futhark of int-  | ats of int-  | idris of int-  | python of int-  | elm of int-  | purescript of int-  | vimscript of int-  | ocaml of int-  | madlang of int-  | tex of int-  | markdown of int-  | yaml of int-  | toml of int-  | cabal of int-  | happy of int-  | alex of int-  | go of int-  | html of int-  | css of int-  | c of int-  | brainfuck of int-  | ruby of int-  | julia of int-  | cobol of int-  | tcl of int-  | r of int-  | lua of int-  | cpp of int-  | lalrpop of int-  | header of int-  | sixten of int-  | dhall of int-  | ipkg of int-  | makefile of int-  | justfile of int-  | ion of int-  | bash of int-  | hamlet of int-  | cassius of int-  | lucius of int-  | julius of int-  | mercury of int-  | yacc of int-  | lex of int-  | coq of int-  | jupyter of int-  | java of int-  | scala of int-  | erlang of int-  | elixir of int-  | pony of int-  | clojure of int-  | cabal_project of int-  | assembly of int-  | nix of int-  | php of int-  | javascript of int-  | kotlin of int-  | fsharp of int-  | fortran of int-  | swift of int-  | csharp of int-  | nim of int-  | cpp_header of int-  | elisp of int-  | rakefile of int-  | plaintext of int-  | llvm of int-  | autoconf of int-  | batch of int-  | powershell of int-  | m4 of int-  | objective_c of int-  | automake of int

@@ -1,180 +0,0 @@-// Type for a collection of files (monoidal)-typedef file = @{ lines = int, files = int }--// Type for the parsed command-line arguments. -typedef command_line = @{ version = bool-, help = bool-, table = bool-, excludes = [ m : nat ] list(string, m)-, includes = [ m : nat ] list(string, m)-}--// Program state, tracking *all* supported file types in an unboxed structure.-typedef source_contents = @{ rust = file-, haskell = file-, ats = file-, python = file-, vimscript = file-, elm = file-, idris = file-, madlang = file-, tex = file-, markdown = file-, yaml = file-, toml = file-, cabal = file-, happy = file-, alex = file-, go = file-, html = file-, css = file-, verilog = file-, vhdl = file-, c = file-, purescript = file-, futhark = file-, brainfuck = file-, ruby = file-, julia = file-, perl = file-, ocaml = file-, agda = file-, cobol = file-, tcl = file-, r = file-, lua = file-, cpp = file-, lalrpop = file-, header = file-, sixten = file-, dhall = file-, ipkg = file-, makefile = file-, justfile = file-, ion = file-, bash = file-, hamlet = file-, cassius = file-, lucius = file-, julius = file-, mercury = file-, yacc = file-, lex = file-, coq = file-, jupyter = file-, java = file-, scala = file-, erlang = file-, elixir = file-, pony = file-, clojure = file-, cabal_project = file-, assembly = file-, nix = file-, php = file-, javascript = file-, kotlin = file-, fsharp = file-, fortran = file-, swift = file-, csharp = file-, nim = file-, cpp_header = file-, elisp = file-, plaintext = file-, rakefile = file-, llvm = file-, autoconf = file-, batch = file-, powershell = file-, m4 = file-, objective_c = file-, automake = file-}--// Reference to source_contents; used to update the structure.-vtypedef source_contents_r = ref(source_contents)--// Sum type representing all supported data types.-datavtype pl_type =-| unknown-| rust of int-| haskell of int-| perl of int-| verilog of int-| vhdl of int-| agda of int-| futhark of int-| ats of int-| idris of int-| python of int-| elm of int-| purescript of int-| vimscript of int-| ocaml of int-| madlang of int-| tex of int-| markdown of int-| yaml of int-| toml of int-| cabal of int-| happy of int-| alex of int-| go of int-| html of int-| css of int-| c of int-| brainfuck of int-| ruby of int-| julia of int-| cobol of int-| tcl of int-| r of int-| lua of int-| cpp of int-| lalrpop of int-| header of int-| sixten of int-| dhall of int-| ipkg of int-| makefile of int-| justfile of int-| ion of int-| bash of int-| hamlet of int-| cassius of int-| lucius of int-| julius of int-| mercury of int-| yacc of int-| lex of int-| coq of int-| jupyter of int-| java of int-| scala of int-| erlang of int-| elixir of int-| pony of int-| clojure of int-| cabal_project of int-| assembly of int-| nix of int-| php of int-| javascript of int-| kotlin of int-| fsharp of int-| fortran of int-| swift of int-| csharp of int-| nim of int-| cpp_header of int-| elisp of int-| rakefile of int-| plaintext of int-| llvm of int-| autoconf of int-| batch of int-| powershell of int-| m4 of int-| objective_c of int-| automake of int

@@ -1,98 +0,0 @@-#include "share/atspre_staload.hats"--dataprop PAD(int,int,int) =-  | {p,l:nat} Yep(p,l,p-l)-  | {p,l:nat} Nope(p,l,0)--extern fun left_pad-  {p,l:nat | p>0 && l>0}-  (-    pad: ssize_t p,-    c: charNZ,-    s: strnptr l-  ): [cushion:nat] (PAD(p,l,cushion) | strnptr (cushion+l))--extern fun {t:t@ype} fill_list-  {n:nat}-  (-    size:ssize_t n,-    c: t-  ): list_vt(t,n)--implement {t}fill_list{n}(size,c) =-  let-    fun loop-      {i:nat | i <= n}-      .<i>.-      (-        size : ssize_t i,-        c: t,-        res: list_vt(t, n-i)-      ): list_vt(t,n) =-      if (size = i2ssz(0))-      then res-      else loop(pred size, c, list_vt_cons(c,res))-  in-    loop(size,c,list_vt_nil())-  end--implement left_pad{p,l}(pad,c,s) =-  let-    val size = strnptr_length(s)-  in-    if (pad > size)-    then-      let-        val padding = pad-size-        val char_list = fill_list(padding,c)-        val pad_string = string_make_list_vt(char_list)-        val res = strnptr_append(pad_string, s)-      in-        begin-          strnptr_free(pad_string);-          strnptr_free(s);-          (Yep{p,l} | res)-        end-      end-    else-      (Nope{p,l} | s)-  end--implement main0(argc, argv) =-  let-    val args = listize_argc_argv(argc,argv)-    val _ =-      if list_vt_length(args) = 3-      then (-        let-          val c = '0'-          val s = g1ofg0(args[1]) : [n:nat] string n-          val pad = g1ofg0(g0string2int(args[2]))-        in-          if length(s) > 0 && pad > 0-          then (-            let-              prval _ = lemma_not_empty(s) where {-                extern praxi-                  lemma_not_empty{n:int}(x:string(n)):[n > 0] void-              }-              prval _ = lemma_not_zero(pad) where {-                extern praxi-                  lemma_not_zero{n:int}(x:int(n)):[n > 0] void-              }-              val (pf | res) = left_pad(i2ssz(pad),c, string1_copy(s))-            in-              begin-                println! ("padding: ", res);-                strnptr_free(res);-              end-           end-          )-          else-            print "Usage: left-pad <string-to-pad> <pad-length>\n"-        end-      )-      else print "Usage: left-pad <string-to-pad> <pad-length>\n"-  in-    list_vt_free(args)-  end

@@ -1,76 +0,0 @@-#include "share/atspre_staload.hats"--dataprop PAD(int, int, int) =-  | { p, l : nat } Yep(p, l, p - l)-  | { p, l : nat } Nope(p, l, 0)--extern-fun left_pad { p, l : nat | p > 0 && l > 0 } ( pad : ssize_t(p)-                                             , c : charNZ-                                             , s : strnptr(l)-                                             ) : [cushion:nat] (PAD(p, l, cushion) | strnptr(cushion+l))--extern-fun {t:t@ype} fill_list {n:nat} (size : ssize_t(n), c : t) :-  list_vt(t, n)--implement {t} fill_list {n} (size, c) =-  let-    fun loop { i : nat | i <= n } .<i>. ( size : ssize_t(i)-                                        , c : t-                                        , res : list_vt(t, n-i)-                                        ) : list_vt(t, n) =-      if (size = i2ssz(0)) then-        res-      else-        loop(pred(size), c, list_vt_cons(c, res))-  in-    loop(size, c, list_vt_nil())-  end--implement left_pad { p, l } (pad, c, s) =-  let-    val size = strnptr_length(s)-  in-    if (pad > size) then-      let-        val padding = pad - size-        val char_list = fill_list(padding, c)-        val pad_string = string_make_list_vt(char_list)-        val res = strnptr_append(pad_string, s)-      in-        (strnptr_free(pad_string) ; strnptr_free(s) ; (Yep{p,l} | res))-      end-    else-      (Nope{p,l} | s)-  end--implement main0 (argc, argv) =-  let-    val args = listize_argc_argv(argc, argv)-    val _ = if list_vt_length(args) = 3 then-      (let-        val c = '0'-        val s = g1ofg0(args[1]) : [n:nat] string(n)-        val pad = g1ofg0(g0string2int(args[2]))-      in-        if length(s) > 0 && pad > 0 then-          (let-            prval _ = lemma_not_empty(s) where-            { extern-              praxi lemma_not_empty {n:int} (x : string(n)) : [ n > 0 ] void }-            prval _ = lemma_not_zero(pad) where-            { extern-              praxi lemma_not_zero {n:int} (x : int(n)) : [ n > 0 ] void }-            val (pf | res) = left_pad(i2ssz(pad), c, string1_copy(s))-          in-            (println!("padding: ", res) ; strnptr_free(res))-          end)-        else-          print("Usage: left-pad <string-to-pad> <pad-length>\n")-      end)-    else-      print("Usage: left-pad <string-to-pad> <pad-length>\n")-  in-    list_vt_free(args)-  end

@@ -1,167 +0,0 @@-#include "share/atspre_staload.hats"-#include "ats-src/numerics.dats"-#include "contrib/atscntrb-hx-intinf/mylibies.hats"--staload UN = "prelude/SATS/unsafe.sats"-staload "contrib/atscntrb-hx-intinf/SATS/intinf_vt.sats"--#define ATS_MAINATSFLAG 1--// Existential types for even and odd numbers. These are only usable with the-// ATS library.-typedef Even = [ n : nat ] int(2 * n)--typedef Odd = [ n : nat ] int(2 * n+1)--// TODO jacobi symbol-// fn legendre(a: int, p: int) : int =-//  a ^ (p - 1 / 2) % p-// m | n-fn divides(m : int, n : int) :<> bool =-  n % m = 0--fnx gcd {k : nat}{l : nat} (m : int(l), n : int(k)) : int =-  if n > 0 then-    gcd(n, witness(m % n))-  else-    m--fn lcm {k : nat}{l : nat} (m : int(l), n : int(k)) : int =-  (m / gcd(m, n)) * n--// stream all divisors of an integer.-fn divisors(n : intGte(1)) :<> stream_vt(int) =-  let-    fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> stream_vt(int) =-      if acc >= n then-        $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))-      else-        if n % acc = 0 then-          $ldelay(stream_vt_cons(n, loop(n, acc + 1)))-        else-          $ldelay(stream_vt_nil)-  in-    loop(n, 1)-  end--// stream all prime divisors of an integer (without multiplicity)-fn prime_divisors(n : intGte(1)) :<> stream_vt(int) =-  let-    fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> stream_vt(int) =-      if acc >= n then-        $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))-      else-        if n % acc = 0 && is_prime(n) then-          $ldelay(stream_vt_cons(n, loop(n, acc + 1)))-        else-          $ldelay(stream_vt_nil)-  in-    loop(n, 1)-  end--fn witness(n : int) : intGte(0) =-  $UN.cast(n)--propdef PRIME (p : int) = { x, y : nat | x <= y } MUL(x, y, p) -<> [ x == 1 ] void--dataprop FACT(int, int) =-  | FACTbas(0, 1)-  | {n : nat}{ r, r1 : int } FACTind(n + 1, r) of (FACT(n, r1), MUL(n + 1, r1, r))--fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) : int =-  case+ n % p of-    | 0 => 1 + get_multiplicity(witness(n / p), p)-    | _ => 0--fn count_divisors(n : intGte(1)) :<> int =-  let-    fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =-      if acc >= n then-        1-      else-        if n % acc = 0 then-          1 + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--fn sum_divisors(n : intGte(1)) :<> int =-  let-    fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =-      if acc >= n then-        0-      else-        if n % acc = 0 then-          acc + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--fn is_perfect(n : intGte(1)) :<> bool =-  sum_divisors(n) = n--// distinct prime divisors-fn little_omega(n : intGte(1)) :<> int =-  let-    fun loop {k : nat}{ m : nat | m > 0 && k >= m } .<k-m>. (n : int(k), acc : int(m)) :<> int =-      if acc >= n then-        if is_prime(n) then-          1-        else-          0-      else-        if n % acc = 0 && is_prime(acc) then-          1 + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--// Euler's totient function.-fn totient(n : intGte(1)) : int =-  case+ n of-    | 1 => 1-    | n =>> -      begin-        let-          fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>. (i : int(m), n : int(k)) : int =-            if i >= n then-              if is_prime(n) then-                n - 1-              else-                n-            else-              if n % i = 0 && is_prime(i) && i != n then-                (loop(i + 1, n) / i) * (i - 1)-              else-                loop(i + 1, n)-        in-          loop(1, n)-        end-      end--// TODO modular exponentiation-// The sum of all φ(m) for m between 1 and n -fun totient_sum(n : intGte(1)) : Intinf =-  let-    fnx loop { n : nat | n >= 1 }{ m : nat | m >= n } .<m-n>. (i : int(n), bound : int(m)) : Intinf =-      if i < bound then-        let-          val x = loop(i + 1, bound)-          val y = add_intinf0_int(x, witness(totient(i)))-        in-          y-        end-      else-        int2intinf(witness(totient(i)))-  in-    loop(1, n)-  end--extern-fun chinese_remainder {n : nat} (residues : list_vt(int, n), moduli : list_vt(int, n)) : Option_vt(int)

@@ -1,186 +0,0 @@-#include "share/atspre_staload.hats"-#include "ats-src/numerics.dats"-#include "contrib/atscntrb-hx-intinf/mylibies.hats"--staload UN = "prelude/SATS/unsafe.sats"-staload "contrib/atscntrb-hx-intinf/SATS/intinf_vt.sats"--#define ATS_MAINATSFLAG 1--// Existential types for even and odd numbers. These are only usable with the-// ATS library.-typedef Even = [n:nat] int(2*n)-typedef Odd = [n:nat] int(2*n+1)--// TODO jacobi symbol-// fn legendre(a: int, p: int) : int =-//  a ^ (p - 1 / 2) % p-// m | n-fn divides(m : int, n : int) :<> bool =-  n % m = 0--fnx gcd {k:nat}{l:nat} (m : int(l), n : int(k)) : int =-  if n > 0 then-    gcd(n, witness(m % n))-  else-    m--fn lcm {k:nat}{l:nat} (m : int(l), n : int(k)) : int =-  (m / gcd(m, n)) * n--// stream all divisors of an integer.-fn divisors(n : intGte(1)) :<> stream_vt(int) =-  let-    fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)-                                                          , acc : int(m)-                                                          ) :<> stream_vt(int) =-      if acc >= n then-        $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))-      else-        if n % acc = 0 then-          $ldelay(stream_vt_cons(n, loop(n, acc + 1)))-        else-          $ldelay(stream_vt_nil)-  in-    loop(n, 1)-  end--// stream all prime divisors of an integer (without multiplicity)-fn prime_divisors(n : intGte(1)) :<> stream_vt(int) =-  let-    fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)-                                                          , acc : int(m)-                                                          ) :<> stream_vt(int) =-      if acc >= n then-        $ldelay(stream_vt_cons(acc, $ldelay(stream_vt_nil)))-      else-        if n % acc = 0 && is_prime(n) then-          $ldelay(stream_vt_cons(n, loop(n, acc + 1)))-        else-          $ldelay(stream_vt_nil)-  in-    loop(n, 1)-  end--fn witness(n : int) : intGte(0) =-  $UN.cast(n)--propdef PRIME (p : int) =-{ x, y : nat | x <= y } MUL(x, y, p) -<> [ x == 1 ] void--dataprop FACT(int, int) =-  | FACTbas(0, 1)-  | { r, r1 : int }{n:nat} FACTind(n + 1, r) of (FACT(n, r1), MUL( n + 1-                                                                 , r1-                                                                 , r-                                                                 ))--fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) :-  int =-  case+ n % p of-    | 0 => 1 + get_multiplicity(witness(n / p), p)-    | _ => 0--fn count_divisors(n : intGte(1)) :<> int =-  let-    fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)-                                                          , acc : int(m)-                                                          ) :<> int =-      if acc >= n then-        1-      else-        if n % acc = 0 then-          1 + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--fn sum_divisors(n : intGte(1)) :<> int =-  let-    fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)-                                                          , acc : int(m)-                                                          ) :<> int =-      if acc >= n then-        0-      else-        if n % acc = 0 then-          acc + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--fn is_perfect(n : intGte(1)) :<> bool =-  sum_divisors(n) = n--// distinct prime divisors-fn little_omega(n : intGte(1)) :<> int =-  let-    fun loop {k:nat}{ m : nat | m > 0 && k >= m } .<k-m>. ( n : int(k)-                                                          , acc : int(m)-                                                          ) :<> int =-      if acc >= n then-        if is_prime(n) then-          1-        else-          0-      else-        if n % acc = 0 && is_prime(acc) then-          1 + loop(n, acc + 1)-        else-          loop(n, acc + 1)-  in-    loop(n, 1)-  end--// Euler's totient function.-fn totient(n : intGte(1)) : int =-  case+ n of-    | 1 => 1-    | n =>> -      begin-        let-          fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>.-          (i : int(m), n : int(k)) : int =-            if i >= n then-              if is_prime(n) then-                n - 1-              else-                n-            else-              if n % i = 0 && is_prime(i) && i != n then-                (loop(i + 1, n) / i) * (i - 1)-              else-                loop(i + 1, n)-        in-          loop(1, n)-        end-      end--// TODO modular exponentiation-// The sum of all φ(m) for m between 1 and n -fun totient_sum(n : intGte(1)) : Intinf =-  let-    fnx loop { n : nat | n >= 1 }{ m : nat | m >= n } .<m-n>. ( i : int(n)-                                                              , bound : int(m)-                                                              ) : Intinf =-      if i < bound then-        let-          val x = loop(i + 1, bound)-          val y = add_intinf0_int(x, witness(totient(i)))-        in-          y-        end-      else-        int2intinf(witness(totient(i)))-  in-    loop(1, n)-  end--extern-fun chinese_remainder {n:nat} ( residues : list_vt(int, n)-                              , moduli : list_vt(int, n)-                              ) : Option_vt(int)

@@ -1,61 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "libats/libc/SATS/math.sats"-staload UN = "prelude/SATS/unsafe.sats"--fun exp {n : nat} .<n>. (x : int, n : int(n)) :<> int =-  case+ x of-    | 0 => 0-    | x => -      begin-        if n > 0 then-          let-            val n2 = half(n)-            val i2 = n % 2-          in-            if i2 = 0 then-              exp(x * x, n2)-            else-              x * exp(x * x, n2)-          end-        else-          1-      end--castfn lemma_bounded(i: int) : [n:nat] int(n)-  = $UN.cast(i)--fun sqrt_bad(k : intGt(0)) : [ m : nat ] int(m) =-  let-    var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))-    var bound: [m:nat] int(m) = lemma_bounded(pre_bound)-  in-    bound-  end--fn is_prime(k : intGt(0)) : bool =-  case+ k of-    | 1 => false-    | k => -      begin-        let-          fun loop {n : nat}{m : nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<> bool =-            if i < bound then-              if k % i = 0 then-                false-              else-                loop(i + 1, bound)-            else-              if i = bound then-                if k % i = 0 then-                  false-                else-                  true-              else-                true-        in-          loop(2, sqrt_bad(k))-        end-      end

@@ -1,63 +0,0 @@-#define ATS_MAINATSFLAG 1--#include "share/atspre_staload.hats"--staload "libats/libc/SATS/math.sats"-staload UN = "prelude/SATS/unsafe.sats"--fun exp {n:nat} .<n>. (x : int, n : int(n)) :<> int =-  case+ x of-    | 0 => 0-    | x => -      begin-        if n > 0 then-          let-            val n2 = half(n)-            val i2 = n % 2-          in-            if i2 = 0 then-              exp(x * x, n2)-            else-              x * exp(x * x, n2)-          end-        else-          1-      end--castfn lemma_bounded(i : int) : [n:nat] int(n) =-  $UN.cast(i)--fun sqrt_bad(k : intGt(0)) : [m:nat] int(m) =-  let-    var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k)))-    var bound: [m:nat] int(m) = lemma_bounded(pre_bound)-  in-    bound-  end--fn is_prime(k : intGt(0)) : bool =-  case+ k of-    | 1 => false-    | k => -      begin-        let-          fun loop {n:nat}{m:nat} .<max(0,m-n)>. ( i : int(n)-                                                 , bound : int(m)-                                                 ) :<> bool =-            if i < bound then-              if k % i = 0 then-                false-              else-                loop(i + 1, bound)-            else-              if i = bound then-                if k % i = 0 then-                  false-                else-                  true-              else-                true-        in-          loop(2, sqrt_bad(k))-        end-      end

@@ -1,1235 +0,0 @@-#include "share/atspre_staload.hats"-#include "share/HATS/atslib_staload_libats_libc.hats"-#include "prelude/DATS/filebas.dats"-#include "libats/ML/DATS/filebas_dirent.dats"-#include "libats/libc/DATS/dirent.dats"-#include "src/concurrency.dats"-#include "libats/DATS/athread_posix.dats"-#include "prelude/DATS/stream_vt.dats"--%{^-#include "libats/libc/CATS/string.cats"-#include "prelude/CATS/filebas.cats"-%}--staload "prelude/SATS/stream_vt.sats"-staload "libats/ML/DATS/list0.dats"-staload "libats/SATS/athread.sats"-staload "libats/ML/DATS/string.dats"-staload "libats/libc/SATS/stdio.sats"-staload "prelude/SATS/filebas.sats"-staload "src/filetype.sats"-staload "libats/ML/DATS/filebas.dats"-staload EXTRA = "libats/ML/SATS/filebas.sats"-staload "libats/libc/SATS/unistd.sats"-staload "libats/DATS/athread.dats"--fun to_file(s : string, pre : Option(string)) : file =-  let-    val is_comment = case+ pre of-      | Some (x) => string_is_prefix(x, s)-      | None => false-  in-    if s = "" then-      @{ lines = 1, blanks = 1, comments = 0, files = 0 }-    else-      if is_comment then-        @{ lines = 1, blanks = 0, comments = 1, files = 0 }-      else-        @{ lines = 1, blanks = 0, comments = 0, files = 0 }-  end--fun empty_file() : file =-  let-    var f = @{ files = 0, blanks = 0, comments = 0, lines = 0 } : file-  in-    f-  end--fun acc_file() : file =-  let-    var f = @{ files = 1, blanks = 0, comments = 0, lines = ~1 } : file-  in-    f-  end--// monoidal addition for 'file' type-fun add_results(x : file, y : file) : file =-  let-    var next = @{ lines = x.lines + y.lines, blanks = x.blanks + y.blanks, comments = x.comments-    + y.comments, files = x.files + y.files }-  in-    next-  end--overload + with add_results--// Given a string representing a filepath, return an integer.-fun line_count(s : string, pre : Option(string)) : file =-  let-    var ref = fileref_open_opt(s, file_mode_r)-  in-    case ref of-      | ~Some_vt (x) => -        begin-          let-            var viewstream: stream_vt(string) = $EXTRA.streamize_fileref_line(x)-            val n: file = stream_vt_foldleft_cloptr( viewstream-                                                   , acc_file()-                                                   , lam (acc, f) =<cloptr1> acc + to_file(f, pre)-                                                   )-            val _ = fileref_close(x)-          in-            n-          end-        end-      | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; to_file( s-                                                                                              , None-                                                                                              ))-  end--// Pad a string of bounded length on the right by adding spaces.-fnx right_pad { k : int | k >= 0 }{ m : int | m <= k } .<k>. (s : string(m), n : int(k)) :-string =-  case+ length(s) < n of-    | true when n > 0 => right_pad(s, n - 1) + " "-    | _ => s--// Pad a string on the left by adding spaces.-fnx left_pad { k : int | k >= 0 } .<k>. (s : string, n : int(k)) : string =-  case+ length(s) < n of-    | true when n > 0 => " " + left_pad(s, n - 1)-    | _ => s--// helper function for make_output-fun maybe_string(s : string, n : int) : string =-  if n > 0 then-    s + ": " + tostring_int(n) + "\n"-  else-    ""--// helper function for make_table-fun maybe_table { k : int | k >= 0 && k < 20 } (s : string(k), f : file) : string =-  let-    var code = f.lines - f.comments - f.blanks-  in-    if f.files > 0 then-      " " + right_pad(s, 21) + left_pad(tostring_int(f.files), 5) + left_pad(tostring_int(f.lines-                                                                                         ), 12)-      + left_pad(tostring_int(code), 13) + left_pad(tostring_int(f.comments), 13)-      + left_pad(tostring_int(f.blanks), 13) + "\n"-    else-      ""-  end--// helper function for make_output-fun with_nonempty(s1 : string, s2 : string) : string =-  if s2 != "" then-    s1 + s2-  else-    ""--// helper function to make totals for tabular output.-fun sum_fields(sc : source_contents) : file =-  let-    var f = @{ lines = sc.rust.lines + sc.haskell.lines + sc.ats.lines + sc.python.lines-    + sc.vimscript.lines + sc.elm.lines + sc.idris.lines + sc.madlang.lines + sc.tex.lines-    + sc.markdown.lines + sc.yaml.lines + sc.toml.lines + sc.cabal.lines + sc.happy.lines-    + sc.alex.lines + sc.go.lines + sc.html.lines + sc.css.lines + sc.verilog.lines + sc.vhdl.lines-    + sc.c.lines + sc.purescript.lines + sc.futhark.lines + sc.brainfuck.lines + sc.ruby.lines-    + sc.julia.lines + sc.perl.lines + sc.ocaml.lines + sc.agda.lines + sc.cobol.lines-    + sc.tcl.lines + sc.r.lines + sc.lua.lines + sc.cpp.lines + sc.lalrpop.lines + sc.header.lines-    + sc.sixten.lines + sc.dhall.lines + sc.ipkg.lines + sc.makefile.lines + sc.justfile.lines-    + sc.ion.lines + sc.bash.lines + sc.hamlet.lines + sc.cassius.lines + sc.lucius.lines-    + sc.julius.lines + sc.mercury.lines + sc.yacc.lines + sc.lex.lines + sc.coq.lines-    + sc.jupyter.lines + sc.java.lines + sc.scala.lines + sc.erlang.lines + sc.elixir.lines-    + sc.pony.lines + sc.clojure.lines + sc.cabal_project.lines + sc.assembly.lines + sc.nix.lines-    + sc.php.lines + sc.javascript.lines + sc.kotlin.lines + sc.fsharp.lines + sc.fortran.lines-    + sc.swift.lines + sc.csharp.lines + sc.nim.lines + sc.cpp_header.lines + sc.elisp.lines-    + sc.plaintext.lines + sc.rakefile.lines + sc.llvm.lines + sc.autoconf.lines + sc.batch.lines-    + sc.powershell.lines + sc.m4.lines + sc.objective_c.lines-    + sc.automake.lines, blanks = sc.rust.blanks + sc.haskell.blanks + sc.ats.blanks-    + sc.python.blanks + sc.vimscript.blanks + sc.elm.blanks + sc.idris.blanks + sc.madlang.blanks-    + sc.tex.blanks + sc.markdown.blanks + sc.yaml.blanks + sc.toml.blanks + sc.cabal.blanks-    + sc.happy.blanks + sc.alex.blanks + sc.go.blanks + sc.html.blanks + sc.css.blanks-    + sc.verilog.blanks + sc.vhdl.blanks + sc.c.blanks + sc.purescript.blanks + sc.futhark.blanks-    + sc.brainfuck.blanks + sc.ruby.blanks + sc.julia.blanks + sc.perl.blanks + sc.ocaml.blanks-    + sc.agda.blanks + sc.cobol.blanks + sc.tcl.blanks + sc.r.blanks + sc.lua.blanks + sc.cpp.blanks-    + sc.lalrpop.blanks + sc.header.blanks + sc.sixten.blanks + sc.dhall.blanks + sc.ipkg.blanks-    + sc.makefile.blanks + sc.justfile.blanks + sc.ion.blanks + sc.bash.blanks + sc.hamlet.blanks-    + sc.cassius.blanks + sc.lucius.blanks + sc.julius.blanks + sc.mercury.blanks + sc.yacc.blanks-    + sc.lex.blanks + sc.coq.blanks + sc.jupyter.blanks + sc.java.blanks + sc.scala.blanks-    + sc.erlang.blanks + sc.elixir.blanks + sc.pony.blanks + sc.clojure.blanks-    + sc.cabal_project.blanks + sc.assembly.blanks + sc.nix.blanks + sc.php.blanks-    + sc.javascript.blanks + sc.kotlin.blanks + sc.fsharp.blanks + sc.fortran.blanks-    + sc.swift.blanks + sc.csharp.blanks + sc.nim.blanks + sc.cpp_header.blanks + sc.elisp.blanks-    + sc.plaintext.blanks + sc.rakefile.blanks + sc.llvm.blanks + sc.autoconf.blanks-    + sc.batch.blanks + sc.powershell.blanks + sc.m4.blanks + sc.objective_c.blanks-    + sc.automake.blanks, comments = sc.rust.comments + sc.haskell.comments + sc.ats.comments-    + sc.python.comments + sc.vimscript.comments + sc.elm.comments + sc.idris.comments-    + sc.madlang.comments + sc.tex.comments + sc.markdown.comments + sc.yaml.comments-    + sc.toml.comments + sc.cabal.comments + sc.happy.comments + sc.alex.comments + sc.go.comments-    + sc.html.comments + sc.css.comments + sc.verilog.comments + sc.vhdl.comments + sc.c.comments-    + sc.purescript.comments + sc.futhark.comments + sc.brainfuck.comments + sc.ruby.comments-    + sc.julia.comments + sc.perl.comments + sc.ocaml.comments + sc.agda.comments-    + sc.cobol.comments + sc.tcl.comments + sc.r.comments + sc.lua.comments + sc.cpp.comments-    + sc.lalrpop.comments + sc.header.comments + sc.sixten.comments + sc.dhall.comments-    + sc.ipkg.comments + sc.makefile.comments + sc.justfile.comments + sc.ion.comments-    + sc.bash.comments + sc.hamlet.comments + sc.cassius.comments + sc.lucius.comments-    + sc.julius.comments + sc.mercury.comments + sc.yacc.comments + sc.lex.comments-    + sc.coq.comments + sc.jupyter.comments + sc.java.comments + sc.scala.comments-    + sc.erlang.comments + sc.elixir.comments + sc.pony.comments + sc.clojure.comments-    + sc.cabal_project.comments + sc.assembly.comments + sc.nix.comments + sc.php.comments-    + sc.javascript.comments + sc.kotlin.comments + sc.fsharp.comments + sc.fortran.comments-    + sc.swift.comments + sc.csharp.comments + sc.nim.comments + sc.cpp_header.comments-    + sc.elisp.comments + sc.plaintext.comments + sc.rakefile.comments + sc.llvm.comments-    + sc.autoconf.comments + sc.batch.comments + sc.powershell.comments + sc.m4.comments-    + sc.objective_c.comments + sc.automake.comments, files = sc.rust.files + sc.haskell.files-    + sc.ats.files + sc.python.files + sc.vimscript.files + sc.elm.files + sc.idris.files-    + sc.madlang.files + sc.tex.files + sc.markdown.files + sc.yaml.files + sc.toml.files-    + sc.cabal.files + sc.happy.files + sc.alex.files + sc.go.files + sc.html.files + sc.css.files-    + sc.verilog.files + sc.vhdl.files + sc.c.files + sc.purescript.files + sc.futhark.files-    + sc.brainfuck.files + sc.ruby.files + sc.julia.files + sc.perl.files + sc.ocaml.files-    + sc.agda.files + sc.cobol.files + sc.tcl.files + sc.r.files + sc.lua.files + sc.cpp.files-    + sc.lalrpop.files + sc.header.files + sc.sixten.files + sc.dhall.files + sc.ipkg.files-    + sc.makefile.files + sc.justfile.files + sc.ion.files + sc.bash.files + sc.hamlet.files-    + sc.cassius.files + sc.lucius.files + sc.julius.files + sc.mercury.files + sc.yacc.files-    + sc.lex.files + sc.coq.files + sc.jupyter.files + sc.java.files + sc.scala.files-    + sc.erlang.files + sc.elixir.files + sc.pony.files + sc.clojure.files + sc.cabal_project.files-    + sc.assembly.files + sc.nix.files + sc.php.files + sc.javascript.files + sc.kotlin.files-    + sc.fsharp.files + sc.fortran.files + sc.swift.files + sc.csharp.files + sc.nim.files-    + sc.cpp_header.files + sc.elisp.files + sc.plaintext.files + sc.rakefile.files + sc.llvm.files-    + sc.autoconf.files + sc.batch.files + sc.powershell.files + sc.m4.files + sc.objective_c.files-    + sc.automake.files }-  in-    f-  end--// function to print tabular output at the end-fun make_table(isc : source_contents) : string =-  "-------------------------------------------------------------------------------\n \33[35mLanguage\33[0m            \33[35mFiles\33[0m        \33[35mLines\33[0m         \33[35mCode\33[0m     \33[35mComments\33[0m       \33[35mBlanks\33[0m\n-------------------------------------------------------------------------------\n"-  + maybe_table("Alex", isc.alex) + maybe_table("Agda", isc.agda) + maybe_table( "Assembly"-                                                                               , isc.assembly-                                                                               ) + maybe_table("ATS", isc.ats)-  + maybe_table("Autoconf", isc.autoconf) + maybe_table("Automake", isc.automake)-  + maybe_table("Bash", isc.bash) + maybe_table("Batch", isc.batch) + maybe_table( "Brainfuck"-                                                                                 , isc.brainfuck-                                                                                 ) + maybe_table("C", isc.c)-  + maybe_table("C Header", isc.header) + maybe_table("C++ cpp_header", isc.cpp_header)-  + maybe_table("C++", isc.cpp) + maybe_table("C#", isc.csharp) + maybe_table("Cabal", isc.cabal)-  + maybe_table("Cabal Project", isc.cabal_project) + maybe_table("Cassius", isc.cassius)-  + maybe_table("COBOL", isc.cobol) + maybe_table("Coq", isc.coq) + maybe_table("CSS", isc.css)-  + maybe_table("Dhall", isc.dhall) + maybe_table("Elixir", isc.elixir) + maybe_table( "Elm"-                                                                                     , isc.elm-                                                                                     ) + maybe_table( "Emacs Lisp"-                                                                                                    , isc.elisp-                                                                                                    )-  + maybe_table("Erlang", isc.erlang) + maybe_table("F#", isc.fsharp) + maybe_table( "Fortran"-                                                                                   , isc.fortran-                                                                                   ) + maybe_table("Go", isc.go)-  + maybe_table("Hamlet", isc.hamlet) + maybe_table("Happy", isc.happy) + maybe_table( "Haskell"-                                                                                     , isc.haskell-                                                                                     ) + maybe_table("HTML", isc.html)-  + maybe_table("Idris", isc.idris) + maybe_table("iPKG", isc.ipkg) + maybe_table("Ion", isc.ion)-  + maybe_table("Java", isc.java) + maybe_table("JavaScript", isc.javascript)-  + maybe_table("Julius", isc.julius) + maybe_table("Julia", isc.julia) + maybe_table( "Jupyter"-                                                                                     , isc.jupyter-                                                                                     ) + maybe_table( "Justfile"-                                                                                                    , isc.justfile-                                                                                                    )-  + maybe_table("Kotlin", isc.kotlin) + maybe_table("LALRPOP", isc.lalrpop) + maybe_table( "Lex"-                                                                                         , isc.lex-                                                                                         ) + maybe_table( "LLVM"-                                                                                                        , isc.llvm-                                                                                                        )-  + maybe_table("Lua", isc.lua) + maybe_table("Lucius", isc.lucius) + maybe_table("M4", isc.m4)-  + maybe_table("Madlang", isc.madlang) + maybe_table("Makefile", isc.makefile)-  + maybe_table("Margaret", isc.margaret) + maybe_table("Markdown", isc.markdown)-  + maybe_table("Mercury", isc.mercury) + maybe_table("Nim", isc.nim) + maybe_table( "Nix"-                                                                                   , isc.nix-                                                                                   ) + maybe_table( "Objective C"-                                                                                                  , isc.objective_c-                                                                                                  )-  + maybe_table("OCaml", isc.ocaml) + maybe_table("Perl", isc.perl) + maybe_table("PHP", isc.php)-  + maybe_table("Plaintext", isc.plaintext) + maybe_table("PowerShell", isc.powershell)-  + maybe_table("Pony", isc.pony) + maybe_table("Python", isc.python) + maybe_table( "PureScript"-                                                                                   , isc.purescript-                                                                                   ) + maybe_table("R", isc.r)-  + maybe_table("Rakefile", isc.rakefile) + maybe_table("Ruby", isc.ruby) + maybe_table( "Rust"-                                                                                       , isc.rust-                                                                                       ) + maybe_table( "Scala"-                                                                                                      , isc.scala-                                                                                                      )-  + maybe_table("Sixten", isc.sixten) + maybe_table("Swift", isc.swift) + maybe_table( "TCL"-                                                                                     , isc.tcl-                                                                                     ) + maybe_table("TeX", isc.tex)-  + maybe_table("TOML", isc.toml) + maybe_table("Verilog", isc.verilog) + maybe_table( "VHDL"-                                                                                     , isc.vhdl-                                                                                     ) + maybe_table( "Vimscript"-                                                                                                    , isc.vimscript-                                                                                                    )-  + maybe_table("Yacc", isc.yacc) + maybe_table("YAML", isc.yaml)-  + "-------------------------------------------------------------------------------\n"-  + maybe_table("Total", sum_fields(isc))-  + "-------------------------------------------------------------------------------\n"--// Function to print output sorted by type of language.-fun make_output(isc : source_contents) : string =-  with_nonempty( "\33[33mProgramming Languages:\33[0m\n"-               , maybe_string("Agda", isc.agda.lines) + maybe_string("Assembly", isc.assembly.lines)-               + maybe_string("ATS", isc.ats.lines) + maybe_string("Brainfuck", isc.brainfuck.lines)-               + maybe_string("C", isc.c.lines) + maybe_string("C Header", isc.header.lines)-               + maybe_string("C++", isc.cpp.lines) + maybe_string("C++ Header", isc.cpp_header.lines)-               + maybe_string("C#", isc.csharp.lines) + maybe_string("COBOL", isc.cobol.lines)-               + maybe_string("Coq", isc.coq.lines) + maybe_string("Elixir", isc.elixir.lines)-               + maybe_string("Elm", isc.elm.lines) + maybe_string("Erlang", isc.erlang.lines)-               + maybe_string("F#", isc.fsharp.lines) + maybe_string("Fortran", isc.fortran.lines)-               + maybe_string("Go", isc.go.lines) + maybe_string("Haskell", isc.haskell.lines)-               + maybe_string("Idris", isc.idris.lines) + maybe_string("Kotline", isc.kotlin.lines)-               + maybe_string("Java", isc.java.lines) + maybe_string("Julia", isc.julia.lines)-               + maybe_string("Lua", isc.lua.lines) + maybe_string("Margaret", isc.margaret.lines)-               + maybe_string("Mercury", isc.mercury.lines) + maybe_string("Nim", isc.nim.lines)-               + maybe_string("Objective C", isc.objective_c.lines) + maybe_string("OCaml", isc.ocaml.lines)-               + maybe_string("Perl", isc.perl.lines) + maybe_string("Pony", isc.pony.lines)-               + maybe_string("PureScript", isc.purescript.lines) + maybe_string("Python", isc.python.lines)-               + maybe_string("R", isc.r.lines) + maybe_string("Ruby", isc.ruby.lines) + maybe_string( "Rust"-                                                                                                     , isc.rust.lines-                                                                                                     )-               + maybe_string("Scala", isc.scala.lines) + maybe_string("Sixten", isc.sixten.lines)-               + maybe_string("Swift", isc.swift.lines) + maybe_string("TCL", isc.tcl.lines)-               ) + with_nonempty( "\n\33[33mEditor Plugins:\33[0m\n"-                                , maybe_string("Emacs Lisp", isc.elisp.lines) + maybe_string( "Vimscript"-                                                                                            , isc.vimscript.lines-                                                                                            )-                                ) + with_nonempty( "\n\33[33mDocumentation:\33[0m\n"-                                                 , maybe_string("Markdown", isc.markdown.lines)-                                                 + maybe_string("Plaintext", isc.plaintext.lines) + maybe_string( "TeX"-                                                                                                                , isc.tex.lines-                                                                                                                )-                                                 ) + with_nonempty( "\n\33[33mConfiguration:\33[0m\n"-                                                                  , maybe_string("Cabal", isc.cabal.lines)-                                                                  + maybe_string( "Cabal Project"-                                                                                , isc.cabal_project.lines-                                                                                ) + maybe_string( "Dhall"-                                                                                                , isc.dhall.lines-                                                                                                ) + maybe_string( "iPKG"-                                                                                                                , isc.ipkg.lines-                                                                                                                )-                                                                  + maybe_string("TOML", isc.toml.lines)-                                                                  + maybe_string("YAML", isc.yaml.lines)-                                                                  ) + with_nonempty( "\n\33[33mShell:\33[0m\n"-                                                                                   , maybe_string( "Bash"-                                                                                                 , isc.bash.lines-                                                                                                 )-                                                                                   + maybe_string( "Batch"-                                                                                                 , isc.batch.lines-                                                                                                 ) + maybe_string( "Ion"-                                                                                                                 , isc.ion.lines-                                                                                                                 )-                                                                                   + maybe_string( "PowerShell"-                                                                                                 , isc.powershell.lines-                                                                                                 )-                                                                                   )-  + with_nonempty( "\n\33[33mParser Generators:\33[0m\n"-                 , maybe_string("Alex", isc.alex.lines) + maybe_string("Happy", isc.happy.lines)-                 + maybe_string("LALRPOP", isc.lalrpop.lines) + maybe_string("Lex", isc.lex.lines)-                 + maybe_string("Yacc", isc.yacc.lines)-                 ) + with_nonempty( "\n\33[33mWeb:\33[0m\n"-                                  , maybe_string("Cassius", isc.cassius.lines) + maybe_string("CSS", isc.css.lines)-                                  + maybe_string("Hamlet", isc.hamlet.lines) + maybe_string("HTML", isc.html.lines)-                                  + maybe_string("JavaScript", isc.javascript.lines) + maybe_string( "Julius"-                                                                                                   , isc.julius.lines-                                                                                                   )-                                  + maybe_string("Lucius", isc.lucius.lines)-                                  ) + with_nonempty( "\n\33[33mHardware:\33[0m\n"-                                                   , maybe_string("Verilog", isc.verilog.lines) + maybe_string( "VHDL"-                                                                                                              , isc.vhdl.lines-                                                                                                              )-                                                   ) + with_nonempty( "\n\33[33mNotebooks:\33[0m\n"-                                                                    , maybe_string("Jupyter", isc.jupyter.lines)-                                                                    ) + with_nonempty( "\n\33[33mOther:\33[0m\n"-                                                                                     , maybe_string( "Autoconf"-                                                                                                   , isc.autoconf.lines-                                                                                                   )-                                                                                     + maybe_string( "Automake"-                                                                                                   , isc.automake.lines-                                                                                                   )-                                                                                     + maybe_string( "Justfile"-                                                                                                   , isc.justfile.lines-                                                                                                   )-                                                                                     + maybe_string( "LLVM"-                                                                                                   , isc.llvm.lines-                                                                                                   )-                                                                                     + maybe_string("M4", isc.m4.lines)-                                                                                     + maybe_string( "Madlang"-                                                                                                   , isc.madlang.lines-                                                                                                   )-                                                                                     + maybe_string( "Makefile"-                                                                                                   , isc.makefile.lines-                                                                                                   )-                                                                                     + maybe_string( "Rakefile"-                                                                                                   , isc.rakefile.lines-                                                                                                   )-                                                                                     )--fun add_contents(x : source_contents, y : source_contents) : source_contents =-  let-    var next = @{ rust = x.rust + y.rust, haskell = x.haskell + y.haskell, ats = x.ats-    + y.ats, python = x.python + y.python, vimscript = x.vimscript + y.vimscript, elm = x.elm-    + y.elm, idris = x.idris + y.idris, madlang = x.madlang + y.madlang, tex = x.tex-    + y.tex, markdown = x.markdown + y.markdown, yaml = x.yaml + y.yaml, toml = x.toml-    + y.toml, cabal = x.cabal + y.cabal, happy = x.happy + y.happy, alex = x.alex-    + y.alex, go = x.go + y.go, html = x.html + y.html, css = x.css + y.css, verilog = x.verilog-    + y.verilog, vhdl = x.vhdl + y.vhdl, c = x.c + y.c, purescript = x.purescript-    + y.purescript, futhark = x.futhark + y.futhark, brainfuck = x.brainfuck-    + y.brainfuck, ruby = x.ruby + y.ruby, julia = x.julia + y.julia, perl = x.perl-    + y.perl, ocaml = x.ocaml + y.ocaml, agda = x.agda + y.agda, cobol = x.cobol-    + y.cobol, tcl = x.tcl + y.tcl, r = x.r + y.r, lua = x.lua + y.lua, cpp = x.cpp-    + y.cpp, lalrpop = x.lalrpop + y.lalrpop, header = x.header + y.header, sixten = x.sixten-    + y.sixten, dhall = x.dhall + y.dhall, ipkg = x.ipkg + y.ipkg, makefile = x.makefile-    + y.makefile, justfile = x.justfile + y.justfile, ion = x.ion + y.ion, bash = x.bash-    + y.bash, hamlet = x.hamlet + y.hamlet, cassius = x.cassius + y.cassius, lucius = x.lucius-    + y.lucius, julius = x.julius + y.julius, mercury = x.mercury + y.mercury, yacc = x.yacc-    + y.yacc, lex = x.lex + y.lex, coq = x.coq + y.coq, jupyter = x.jupyter-    + y.jupyter, java = x.java + y.java, scala = x.scala + y.scala, erlang = x.erlang-    + y.erlang, elixir = x.elixir + y.elixir, pony = x.pony + y.pony, clojure = x.clojure-    + y.clojure, cabal_project = x.cabal_project + y.cabal_project, assembly = x.assembly-    + y.assembly, nix = x.nix + y.nix, php = x.php + y.php, javascript = x.javascript-    + y.javascript, kotlin = x.kotlin + y.kotlin, fsharp = x.fsharp + y.fsharp, fortran = x.fortran-    + y.fortran, swift = x.swift + y.swift, csharp = x.csharp + y.csharp, nim = x.nim-    + y.nim, cpp_header = x.cpp_header + y.cpp_header, elisp = x.elisp-    + y.elisp, plaintext = x.plaintext + y.plaintext, rakefile = x.rakefile-    + y.rakefile, llvm = x.llvm + y.llvm, autoconf = x.autoconf + y.autoconf, batch = x.batch-    + y.batch, powershell = x.powershell + y.powershell, m4 = x.m4-    + y.m4, objective_c = x.objective_c + y.objective_c, automake = x.automake-    + y.automake, margaret = x.margaret + y.margaret } : source_contents-  in-    next-  end--// This is the step function used when streaming directory contents. -fun adjust_contents(prev : source_contents, scf : pl_type) : source_contents =-  let-    val sc_r = ref<source_contents>(prev)-    val _ = case+ scf of-      | ~haskell n => sc_r->haskell := prev.haskell + n-      | ~ats n => sc_r->ats := prev.ats + n-      | ~rust n => sc_r->rust := prev.rust + n-      | ~markdown n => sc_r->markdown := prev.markdown + n-      | ~python n => sc_r->python := prev.python + n-      | ~vimscript n => sc_r->vimscript := prev.vimscript + n-      | ~yaml n => sc_r->yaml := prev.yaml + n-      | ~toml n => sc_r->toml := prev.toml + n-      | ~happy n => sc_r->happy := prev.happy + n-      | ~alex n => sc_r->alex := prev.alex + n-      | ~idris n => sc_r->idris := prev.idris + n-      | ~madlang n => sc_r->madlang := prev.madlang + n-      | ~elm n => sc_r->elm := prev.elm + n-      | ~c n => sc_r->c := prev.c + n-      | ~go n => sc_r->go := prev.go + n-      | ~cabal n => sc_r->cabal := prev.cabal + n-      | ~verilog n => sc_r->verilog := prev.verilog + n-      | ~vhdl n => sc_r->vhdl := prev.vhdl + n-      | ~html n => sc_r->html := prev.html + n-      | ~css n => sc_r->css := prev.css + n-      | ~purescript n => sc_r->purescript := prev.purescript + n-      | ~futhark n => sc_r->futhark := prev.futhark + n-      | ~brainfuck n => sc_r->brainfuck := prev.brainfuck + n-      | ~ruby n => sc_r->ruby := prev.ruby + n-      | ~julia n => sc_r->julia := prev.julia + n-      | ~tex n => sc_r->tex := prev.tex + n-      | ~perl n => sc_r->perl := prev.perl + n-      | ~ocaml n => sc_r->ocaml := prev.ocaml + n-      | ~agda n => sc_r->agda := prev.agda + n-      | ~cobol n => sc_r->cobol := prev.cobol + n-      | ~tcl n => sc_r->tcl := prev.tcl + n-      | ~r n => sc_r->r := prev.r + n-      | ~lua n => sc_r->lua := prev.lua + n-      | ~cpp n => sc_r->cpp := prev.cpp + n-      | ~lalrpop n => sc_r->lalrpop := prev.lalrpop + n-      | ~header n => sc_r->header := prev.header + n-      | ~sixten n => sc_r->sixten := prev.sixten + n-      | ~dhall n => sc_r->dhall := prev.dhall + n-      | ~ipkg n => sc_r->ipkg := prev.ipkg + n-      | ~justfile n => sc_r->justfile := prev.justfile + n-      | ~makefile n => sc_r->makefile := prev.makefile + n-      | ~ion n => sc_r->ion := prev.ion + n-      | ~bash n => sc_r->bash := prev.bash + n-      | ~hamlet n => sc_r->hamlet := prev.hamlet + n-      | ~cassius n => sc_r->cassius := prev.cassius + n-      | ~lucius n => sc_r->lucius := prev.lucius + n-      | ~julius n => sc_r->julius := prev.julius + n-      | ~mercury n => sc_r->mercury := prev.mercury + n-      | ~yacc n => sc_r->yacc := prev.yacc + n-      | ~lex n => sc_r->lex := prev.lex + n-      | ~coq n => sc_r->coq := prev.coq + n-      | ~jupyter n => sc_r->jupyter := prev.jupyter + n-      | ~java n => sc_r->java := prev.java + n-      | ~scala n => sc_r->scala := prev.scala + n-      | ~erlang n => sc_r->erlang := prev.erlang + n-      | ~elixir n => sc_r->elixir := prev.elixir + n-      | ~pony n => sc_r->pony := prev.pony + n-      | ~clojure n => sc_r->clojure := prev.clojure + n-      | ~cabal_project n => sc_r->cabal_project := prev.cabal_project + n-      | ~assembly n => sc_r->assembly := prev.assembly + n-      | ~nix n => sc_r->nix := prev.nix + n-      | ~php n => sc_r->php := prev.php + n-      | ~javascript n => sc_r->javascript := prev.javascript + n-      | ~kotlin n => sc_r->kotlin := prev.kotlin + n-      | ~fsharp n => sc_r->fsharp := prev.fsharp + n-      | ~fortran n => sc_r->fortran := prev.fortran + n-      | ~swift n => sc_r->swift := prev.swift + n-      | ~csharp n => sc_r->csharp := prev.csharp + n-      | ~nim n => sc_r->nim := prev.nim + n-      | ~cpp_header n => sc_r->cpp_header := prev.cpp_header + n-      | ~elisp n => sc_r->elisp := prev.elisp + n-      | ~plaintext n => sc_r->plaintext := prev.plaintext + n-      | ~rakefile n => sc_r->rakefile := prev.rakefile + n-      | ~llvm n => sc_r->llvm := prev.llvm + n-      | ~autoconf n => sc_r->autoconf := prev.autoconf + n-      | ~batch n => sc_r->batch := prev.batch + n-      | ~powershell n => sc_r->powershell := prev.powershell + n-      | ~m4 n => sc_r->m4 := prev.m4 + n-      | ~objective_c n => sc_r->objective_c := prev.objective_c + n-      | ~automake n => sc_r->automake := prev.automake + n-      | ~margaret n => sc_r->margaret := prev.margaret + n-      | ~unknown _ => ()-  in-    !sc_r-  end--fun free_pl(pl : pl_type) : void =-  case+ pl of-    | ~unknown _ => ()-    | ~rust _ => ()-    | ~haskell _ => ()-    | ~perl _ => ()-    | ~lucius _ => ()-    | ~cassius _ => ()-    | ~hamlet _ => ()-    | ~julius _ => ()-    | ~bash _ => ()-    | ~coq _ => ()-    | ~justfile _ => ()-    | ~makefile _ => ()-    | ~yaml _ => ()-    | ~toml _ => ()-    | ~dhall _ => ()-    | ~ipkg _ => ()-    | ~ion _ => ()-    | ~mercury _ => ()-    | ~yacc _ => ()-    | ~lex _ => ()-    | ~r _ => ()-    | ~c _ => ()-    | ~cpp _ => ()-    | ~lua _ => ()-    | ~lalrpop _ => ()-    | ~header _ => ()-    | ~sixten _ => ()-    | ~java _ => ()-    | ~scala _ => ()-    | ~elixir _ => ()-    | ~erlang _ => ()-    | ~happy _ => ()-    | ~alex _ => ()-    | ~go _ => ()-    | ~html _ => ()-    | ~css _ => ()-    | ~brainfuck _ => ()-    | ~ruby _ => ()-    | ~julia _ => ()-    | ~elm _ => ()-    | ~purescript _ => ()-    | ~vimscript _ => ()-    | ~ocaml _ => ()-    | ~madlang _ => ()-    | ~agda _ => ()-    | ~idris _ => ()-    | ~futhark _ => ()-    | ~ats _ => ()-    | ~tex _ => ()-    | ~cabal _ => ()-    | ~cobol _ => ()-    | ~tcl _ => ()-    | ~verilog _ => ()-    | ~vhdl _ => ()-    | ~markdown _ => ()-    | ~python _ => ()-    | ~pony _ => ()-    | ~jupyter _ => ()-    | ~clojure _ => ()-    | ~cabal_project _ => ()-    | ~assembly _ => ()-    | ~nix _ => ()-    | ~php _ => ()-    | ~javascript _ => ()-    | ~kotlin _ => ()-    | ~fsharp _ => ()-    | ~fortran _ => ()-    | ~swift _ => ()-    | ~csharp _ => ()-    | ~nim _ => ()-    | ~cpp_header _ => ()-    | ~elisp _ => ()-    | ~plaintext _ => ()-    | ~rakefile _ => ()-    | ~llvm _ => ()-    | ~autoconf _ => ()-    | ~batch _ => ()-    | ~powershell _ => ()-    | ~m4 _ => ()-    | ~objective_c _ => ()-    | ~automake _ => ()-    | ~margaret _ => ()--// match a particular word against a list of keywords-fun match_keywords { m : nat | m <= 10 } (keys : list(string, m), word : string) : bool =-  list_foldright_cloref( keys-                       , lam (next, acc) =<cloref1> acc || eq_string_string(next, word)-                       , false-                       )--// TODO use list_vt{int}(0, 1, 2, 3, 4) instead?-// helper function for check_keywords-fun step_keyword(size : file, pre : pl_type, word : string, ext : string) : pl_type =-  case+ pre of-    | unknown _ => let-      -    in-      case+ ext of-        | "y" => let-          val _ = free_pl(pre)-          var happy_keywords = list_cons("module", list_nil())-        in-          if match_keywords(happy_keywords, word) then-            happy(size)-          else-            if let-              var yacc_keywords = list_cons("struct", list_cons("char", list_cons("int", list_nil())))-            in-              match_keywords(yacc_keywords, word)-            end then-              yacc(size)-            else-              unknown-        end-        | "v" => let-          var _ = free_pl(pre)-          var verilog_keywords = list_cons( "endmodule"-                                          , list_cons( "posedge"-                                                     , list_cons( "edge"-                                                                , list_cons("always", list_cons("wire", list_nil()))-                                                                )-                                                     )-                                          )-        in-          if match_keywords(verilog_keywords, word) then-            verilog(size)-          else-            if let-              var coq_keywords = list_cons( "Qed"-                                          , list_cons( "Require"-                                                     , list_cons( "Hypothesis"-                                                                , list_cons( "Inductive"-                                                                           , list_cons( "Remark"-                                                                                      , list_cons( "Lemma"-                                                                                                 , list_cons( "Proof"-                                                                                                            , list_cons( "Definition"-                                                                                                                       , list_cons( "Theorem"-                                                                                                                                  , list_nil()-                                                                                                                                  )-                                                                                                                       )-                                                                                                            )-                                                                                                 )-                                                                                      )-                                                                           )-                                                                )-                                                     )-                                          )-            in-              match_keywords(coq_keywords, word)-            end then-              coq(size)-            else-              unknown-        end-        | "m" => let-          val _ = free_pl(pre)-          var mercury_keywords = list_cons("module", list_cons("pred", list_cons("mode", list_nil())))-        in-          if match_keywords(mercury_keywords, word) then-            mercury(size)-          else-            if let-              var objective_c_keywords = list_cons( "nil"-                                                  , list_cons("nullable", list_cons("nonnull", list_nil()))-                                                  )-            in-              match_keywords(objective_c_keywords, word)-            end then-              objective_c(size)-            else-              unknown-        end-        | _ => pre-    end-    | _ => pre--// Function to disambiguate extensions such as .v (Coq and Verilog) and .m-// (Mercury and Objective C). This should only be called when extensions are in-// conflict, as it reads the whole file.-fun check_keywords(s : string, size : file, ext : string) : pl_type =-  let-    var ref = fileref_open_opt(s, file_mode_r)-  in-    case+ ref of-      | ~Some_vt (x) => let-        var init: pl_type = unknown-        var viewstream = $EXTRA.streamize_fileref_word(x)-        val result = stream_vt_foldleft_cloptr( viewstream-                                              , init-                                              , lam (acc, next) => step_keyword(size, acc, next, ext)-                                              )-        val _ = fileref_close(x)-      in-        result-      end-      | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; unknown)-  end--// Check shebang on scripts.-//-// TODO flexible parser that drops spaces as appropriate-// TODO check magic number so as to avoid checking shebang of binary file-fun check_shebang(s : string) : pl_type =-  let-    val ref = fileref_open_opt(s, file_mode_r)-    val str: string = case+ ref of-      | ~Some_vt (x) => let-        val s = strptr2string(fileref_get_line_string(x))-        val _ = fileref_close(x)-      in-        s-      end-      | ~None_vt() => (println!("\33[33mWarning:\33[0m could not open file at " + s) ; "")-  in-    case+ str of-      | "#!/usr/bin/env ion" => ion(line_count(s, Some("#")))-      | "#!/usr/bin/env bash" => bash(line_count(s, Some("#")))-      | "#!/bin/bash" => bash(line_count(s, Some("#")))-      | "#!python" => python(line_count(s, Some("#")))-      | "#!python2" => python(line_count(s, Some("#")))-      | "#!python3" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python2" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python3" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env perl" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/env perl6" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/perl" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/env stack" => haskell(line_count(s, Some("--")))-      | "#!/usr/bin/env runhaskell" => haskell(line_count(s, Some("--")))-      | "#!/usr/bin/env node" => javascript(line_count(s, None))-      | _ => unknown-  end--// Match based on filename (for makefiles, etc.)-fun match_filename(s : string) : pl_type =-  let-    val (prf | str) = filename_get_base(s)-    val match = $UN.strptr2string(str)-    -    prval () = prf(str)-  in-    case+ match of-      | "Makefile" => makefile(line_count(s, Some("#")))-      | "Makefile.tc" => makefile(line_count(s, Some("#")))-      | "makefile" => makefile(line_count(s, Some("#")))-      | "GNUmakefile" => makefile(line_count(s, Some("#")))-      | "Justfile" => justfile(line_count(s, Some("#")))-      | "justfile" => justfile(line_count(s, Some("#")))-      | "Rakefile" => rakefile(line_count(s, None))-      | "cabal.project.local" => cabal_project(line_count(s, Some("--")))-      | _ => check_shebang(s)-  end--// Match based on file extension (assuming the file name is passed in as an-// argument).-fun prune_extension(s : string, file_proper : string) : pl_type =-  let-    val (prf | str) = filename_get_ext(file_proper)-    val match: string = if strptr2ptr(str) > 0 then-      $UN.strptr2string(str)-    else-      ""-    -    prval () = prf(str)-  in-    case+ match of-      | "hs" => haskell(line_count(s, Some("--")))-      | "hs-boot" => haskell(line_count(s, Some("--")))-      | "hsig" => haskell(line_count(s, Some("--")))-      | "rs" => rust(line_count(s, Some("//")))-      | "tex" => tex(line_count(s, Some("%")))-      | "md" => markdown(line_count(s, None))-      | "markdown" => markdown(line_count(s, None))-      | "dats" => ats(line_count(s, Some("//")))-      | "hats" => ats(line_count(s, Some("//")))-      | "cats" => ats(line_count(s, Some("//")))-      | "sats" => ats(line_count(s, Some("//")))-      | "py" => python(line_count(s, None))-      | "fut" => futhark(line_count(s, Some("--")))-      | "pl" => perl(line_count(s, None))-      | "agda" => agda(line_count(s, Some("--")))-      | "idr" => idris(line_count(s, Some("--")))-      | "v" => check_keywords(s, line_count(s, Some("--")), match)-      | "m" => check_keywords(s, line_count(s, None), match)-      | "vhdl" => vhdl(line_count(s, None))-      | "vhd" => vhdl(line_count(s, None))-      | "go" => go(line_count(s, Some("//")))-      | "vim" => vimscript(line_count(s, None))-      | "ml" => ocaml(line_count(s, None))-      | "purs" => purescript(line_count(s, None))-      | "elm" => elm(line_count(s, Some("--")))-      | "mad" => madlang(line_count(s, Some("#")))-      | "toml" => toml(line_count(s, Some("#")))-      | "cabal" => cabal(line_count(s, Some("--")))-      | "yml" => yaml(line_count(s, Some("#")))-      | "yaml" => yaml(line_count(s, Some("#")))-      | "y" => check_keywords(s, line_count(s, None), match)-      | "ypp" => yacc(line_count(s, Some("//")))-      | "x" => alex(line_count(s, Some("--")))-      | "l" => lex(line_count(s, None))-      | "lpp" => lex(line_count(s, None))-      | "html" => html(line_count(s, None))-      | "htm" => html(line_count(s, None))-      | "css" => css(line_count(s, None))-      | "vhdl" => vhdl(line_count(s, None))-      | "vhd" => vhdl(line_count(s, None))-      | "c" => c(line_count(s, Some("//")))-      | "b" => brainfuck(line_count(s, None))-      | "bf" => brainfuck(line_count(s, None))-      | "rb" => ruby(line_count(s, None))-      | "cob" => cobol(line_count(s, None))-      | "cbl" => cobol(line_count(s, None))-      | "cpy" => cobol(line_count(s, None))-      | "ml" => ocaml(line_count(s, None))-      | "tcl" => tcl(line_count(s, None))-      | "r" => r(line_count(s, None))-      | "R" => r(line_count(s, None))-      | "lua" => lua(line_count(s, None))-      | "cpp" => cpp(line_count(s, Some("//")))-      | "cc" => cpp(line_count(s, Some("//")))-      | "lalrpop" => lalrpop(line_count(s, Some("//")))-      | "h" => header(line_count(s, None))-      | "vix" => sixten(line_count(s, Some("--")))-      | "dhall" => dhall(line_count(s, None))-      | "ipkg" => ipkg(line_count(s, Some("--")))-      | "mk" => makefile(line_count(s, Some("#")))-      | "hamlet" => hamlet(line_count(s, None))-      | "cassius" => cassius(line_count(s, None))-      | "lucius" => cassius(line_count(s, None))-      | "julius" => julius(line_count(s, None))-      | "jl" => julia(line_count(s, None))-      | "ion" => ion(line_count(s, Some("#")))-      | "bash" => bash(line_count(s, Some("#")))-      | "ipynb" => jupyter(line_count(s, None))-      | "java" => java(line_count(s, None))-      | "scala" => scala(line_count(s, None))-      | "erl" => erlang(line_count(s, None))-      | "hrl" => erlang(line_count(s, None))-      | "ex" => elixir(line_count(s, None))-      | "exs" => elixir(line_count(s, None))-      | "pony" => pony(line_count(s, None))-      | "clj" => clojure(line_count(s, None))-      | "s" => assembly(line_count(s, Some(";")))-      | "S" => assembly(line_count(s, Some(";")))-      | "asm" => assembly(line_count(s, Some(";")))-      | "nix" => nix(line_count(s, None))-      | "php" => php(line_count(s, None))-      | "local" => match_filename(s)-      | "project" => cabal_project(line_count(s, Some("--")))-      | "js" => javascript(line_count(s, None))-      | "jsexe" => javascript(line_count(s, None))-      | "kt" => kotlin(line_count(s, None))-      | "kts" => kotlin(line_count(s, None))-      | "fs" => fsharp(line_count(s, None))-      | "f" => fortran(line_count(s, None))-      | "for" => fortran(line_count(s, None))-      | "f90" => fortran(line_count(s, None))-      | "f95" => fortran(line_count(s, None))-      | "swift" => swift(line_count(s, None))-      | "csharp" => csharp(line_count(s, None))-      | "nim" => nim(line_count(s, None))-      | "el" => elisp(line_count(s, None))-      | "txt" => plaintext(line_count(s, None))-      | "ll" => llvm(line_count(s, None))-      | "in" => autoconf(line_count(s, Some("#")))-      | "bat" => batch(line_count(s, None))-      | "ps1" => powershell(line_count(s, None))-      | "ac" => m4(line_count(s, None))-      | "mm" => objective_c(line_count(s, Some("//")))-      | "am" => automake(line_count(s, Some("#")))-      | "mgt" => margaret(line_count(s, Some("--")))-      | "" => match_filename(s)-      | "sh" => match_filename(s)-      | "yamllint" => match_filename(s)-      | _ => unknown-  end--// filter out directories containing artifacts-fun bad_dir(s : string, excludes : List0(string)) : bool =-  case+ s of-    | "." => true-    | ".." => true-    | ".pijul" => true-    | "_darcs" => true-    | ".hg" => true-    | ".git" => true-    | "target" => true-    | ".egg-info" => true-    | "nimcache" => true-    | ".shake" => true-    | "dist-newstyle" => true-    | "dist" => true-    | ".psc-package" => true-    | ".pulp-cache" => true-    | "output" => true-    | "bower_components" => true-    | "elm-stuff" => true-    | ".stack-work" => true-    | ".reco" => true-    | ".reco-work" => true-    | ".cabal-sandbox" => true-    | "node_modules" => true-    | ".lein-plugins" => true-    | ".sass-cache" => true-    | _ => list_exists_cloref(excludes, lam x => x = s || x = s + "/")--fnx step_stream( acc : source_contents-               , full_name : string-               , file_proper : string-               , excludes : List0(string)-               ) : source_contents =-  if test_file_isdir(full_name) != 0 then-    flow_stream(full_name, acc, excludes)-  else-    adjust_contents(acc, prune_extension(full_name, file_proper))-and flow_stream(s : string, init : source_contents, excludes : List0(string)) :-source_contents =-  let-    var files = streamize_dirname_fname(s)-    var ffiles = stream_vt_filter_cloptr(files, lam x => not(bad_dir(x, excludes)))-  in-    stream_vt_foldleft_cloptr( ffiles-                             , init-                             , lam (acc, next) => step_stream(acc, s + "/" + next, next, excludes)-                             )-  end--fun empty_contents() : source_contents =-  let-    var isc = @{ rust = empty_file()-               , haskell = empty_file()-               , ats = empty_file()-               , python = empty_file()-               , vimscript = empty_file()-               , elm = empty_file()-               , idris = empty_file()-               , madlang = empty_file()-               , tex = empty_file()-               , markdown = empty_file()-               , yaml = empty_file()-               , toml = empty_file()-               , cabal = empty_file()-               , happy = empty_file()-               , alex = empty_file()-               , go = empty_file()-               , html = empty_file()-               , css = empty_file()-               , verilog = empty_file()-               , vhdl = empty_file()-               , c = empty_file()-               , purescript = empty_file()-               , futhark = empty_file()-               , brainfuck = empty_file()-               , ruby = empty_file()-               , julia = empty_file()-               , perl = empty_file()-               , ocaml = empty_file()-               , agda = empty_file()-               , cobol = empty_file()-               , tcl = empty_file()-               , r = empty_file()-               , lua = empty_file()-               , cpp = empty_file()-               , lalrpop = empty_file()-               , header = empty_file()-               , sixten = empty_file()-               , dhall = empty_file()-               , ipkg = empty_file()-               , makefile = empty_file()-               , justfile = empty_file()-               , ion = empty_file()-               , bash = empty_file()-               , hamlet = empty_file()-               , cassius = empty_file()-               , lucius = empty_file()-               , julius = empty_file()-               , mercury = empty_file()-               , yacc = empty_file()-               , lex = empty_file()-               , coq = empty_file()-               , jupyter = empty_file()-               , java = empty_file()-               , scala = empty_file()-               , erlang = empty_file()-               , elixir = empty_file()-               , pony = empty_file()-               , clojure = empty_file()-               , cabal_project = empty_file()-               , assembly = empty_file()-               , nix = empty_file()-               , php = empty_file()-               , javascript = empty_file()-               , kotlin = empty_file()-               , fsharp = empty_file()-               , fortran = empty_file()-               , swift = empty_file()-               , csharp = empty_file()-               , nim = empty_file()-               , cpp_header = empty_file()-               , elisp = empty_file()-               , plaintext = empty_file()-               , rakefile = empty_file()-               , llvm = empty_file()-               , autoconf = empty_file()-               , batch = empty_file()-               , powershell = empty_file()-               , m4 = empty_file()-               , objective_c = empty_file()-               , automake = empty_file()-               , margaret = empty_file()-               } : source_contents-  in-    isc-  end--fun map_stream(acc : source_contents, includes : List0(string), excludes : List0(string)) :-source_contents =-  list_foldleft_cloref( includes-                      , acc-                      , lam (acc, next) => if test_file_exists(next) || next = "" then-                        step_stream(acc, next, next, excludes)-                      else-                        (prerr("\33[31mError:\33[0m directory '" + next + "' does not exist\n") ; (exit(1) ; acc))-                      )--fun is_flag(s : string) : bool =-  string_is_prefix("-", s)--fun process_excludes(s : string, acc : command_line) : command_line =-  let-    val acc_r = ref<command_line>(acc)-    val () = if is_flag(s) then-      (println!("Error: flag " + s + " found where a directory name was expected") ; (exit(0) ; ()))-    else-      acc_r->excludes := list_cons(s, acc.excludes)-  in-    !acc_r-  end--fun process(s : string, acc : command_line, is_first : bool) : command_line =-  let-    val acc_r = ref<command_line>(acc)-    val () = if is_flag(s) then-      case+ s of-        | "--help" => acc_r->help := true-        | "-h" => acc_r->help := true-        | "--no-table" => if not(acc.no_table) then-          acc_r->no_table := true-        else-          (println!("\33[31mError:\33[0m flag " + s + " cannot appear twice") ; (exit(0) ; ()))-        | "-t" => if not(acc.no_table) then-          acc_r->no_table := true-        else-          (println!("\33[31mError:\33[0m flag " + s + " cannot appear twice") ; (exit(0) ; ()))-        | "--parallel" => acc_r->parallel := true-        | "-p" => acc_r->parallel := true-        | "--version" => acc_r->version := true-        | "-V" => acc_r->version := true-        | "-e" => (println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument") ;-        (exit(0) ; ()))-        | "--exclude" => (println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument"-                                  ) ; (exit(0) ; ()))-        | _ => (println!("\33[31mError:\33[0m flag '" + s + "' not recognized") ; (exit(0) ; ()))-    else-      if not(is_first) then-        acc_r->includes := list_cons(s, acc.includes)-      else-        ()-  in-    !acc_r-  end--fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n - m>. ( argc : int(n)-                                                              , argv : !(argv(n))-                                                              , current : int(m)-                                                              , prev_is_exclude : bool-                                                              , acc : command_line-                                                              ) : command_line =-  let-    var arg = argv[current]-  in-    if current < argc - 1 then-      if arg != "--exclude" && arg != "-e" then-        let-          val c = get_cli(argc, argv, current + 1, false, acc)-        in-          if prev_is_exclude && current != 0 then-            process_excludes(arg, c)-          else-            if current != 0 then-              process(arg, c, current = 0)-            else-              c-        end-      else-        let-          val c = get_cli(argc, argv, current + 1, true, acc)-        in-          c-        end-    else-      if prev_is_exclude then-        process_excludes(arg, acc)-      else-        process(arg, acc, current = 0)-  end--fun version() : void =-  println!("polygot version 0.3.11\nCopyright (c) 2017 Vanessa McHale")--fun help() : void =-  print("polyglot - Count lines of code quickly.--\33[36mUSAGE:\33[0m poly [DIRECTORY] ... [OPTION] ...--\33[36mFLAGS:\33[0m-    -V, --version            show version information-    -h, --help               display this help and exit-    -e, --exclude            exclude a directory-    -p, --parallel           execute in parallel-    -t, --no-table           display results in alternate format--When no directory is provided poly will execute in the-current directory.--Bug reports and updates: nest.pijul.com/vamchale/polyglot\n"-       )--fun head(xs : List0(string)) : string =-  case+ xs of-    | list_cons (x, xs) => x + ", " + head(xs)-    | list_nil() => ""--// TODO channel to draw work? e.g. take a channel of strings, return a channel of source_contents-fun work( excludes : List0(string)-        , send : channel(List0(string))-        , chan : channel(source_contents)-        ) : void =-  {-    val- (n) = channel_remove(send)-    var x = map_stream(empty_contents(), n, excludes)-    val () = channel_insert(chan, x)-    val- ~None_vt() = channel_unref(chan)-    val- () = case channel_unref<List0(string)>(send) of-      | ~None_vt() => ()-      | ~Some_vt (snd) => queue_free<List0(string)>(snd)-  }--// Function returning the number of CPU cores.-extern-fun  ncpu  () : int--%{^-#include <unistd.h>-int ncpu() {-  return sysconf(_SC_NPROCESSORS_ONLN);-}-%}--#define NCPU 4--fun apportion(includes : List0(string)) : (List0(string), List0(string)) =-  let-    var n = length(includes) / 2-    val (p, q) = list_split_at(includes, n)-  in-    (list_vt2t(p), q)-  end--// TODO maybe make a parallel fold?-fun threads(includes : List0(string), excludes : List0(string)) : source_contents =-  let-    val chan = channel_make<source_contents>(2)-    val chan2 = channel_ref(chan)-    val chan3 = channel_ref(chan)-    val send1 = channel_make<List0(string)>(1)-    val send2 = channel_make<List0(string)>(1)-    val send_r1 = channel_ref(send1)-    val send_r2 = channel_ref(send2)-    var new_includes = if length(includes) > 0 then-      includes-    else-      list_cons(".", list_nil())-    val (fst, snd) = apportion(new_includes)-    val _ = channel_insert(send1, fst)-    val _ = channel_insert(send2, snd)-    val t2 = athread_create_cloptr_exn(llam () => work(excludes, send_r1, chan2))-    val t3 = athread_create_cloptr_exn(llam () => work(excludes, send_r2, chan3))-    val- ~None_vt() = channel_unref(send1)-    val- ~None_vt() = channel_unref(send2)-    val- (n) = channel_remove(chan)-    val- (m) = channel_remove(chan)-    val () = ignoret(usleep(1u))-    val () = while(channel_refcount(chan) >= 2)()-    val r = add_contents(n, m)-    val- ~Some_vt (que) = channel_unref<source_contents>(chan)-    val () = queue_free<source_contents>(que)-  in-    r-  end--implement main0 (argc, argv) =-  let-    val cli = @{ version = false-               , help = false-               , no_table = false-               , parallel = false-               , excludes = list_nil()-               , includes = list_nil()-               } : command_line-    val parsed = get_cli(argc, argv, 0, false, cli)-  in-    if parsed.help then-      (help() ; exit(0))-    else-      if parsed.version then-        (version() ; exit(0))-      else-        let-          val result = if parsed.parallel then-            threads(parsed.includes, parsed.excludes)-          else-            if length(parsed.includes) > 0 then-              map_stream(empty_contents(), parsed.includes, parsed.excludes)-            else-              map_stream(empty_contents(), list_cons(".", list_nil()), parsed.excludes)-        in-          if parsed.no_table then-            print(make_output(result))-          else-            print(make_table(result))-        end-  end

@@ -1,1619 +0,0 @@-#include "share/atspre_staload.hats"-#include "share/HATS/atslib_staload_libats_libc.hats"-#include "prelude/DATS/filebas.dats"-#include "libats/ML/DATS/filebas_dirent.dats"-#include "libats/libc/DATS/dirent.dats"-#include "src/concurrency.dats"-#include "libats/DATS/athread_posix.dats"-#include "prelude/DATS/stream_vt.dats"--%{^-#include "libats/libc/CATS/string.cats"-#include "prelude/CATS/filebas.cats"-%}--staload "prelude/SATS/stream_vt.sats"-staload "libats/ML/DATS/list0.dats"-staload "libats/SATS/athread.sats"-staload "libats/ML/DATS/string.dats"-staload "libats/libc/SATS/stdio.sats"-staload "prelude/SATS/filebas.sats"-staload "src/filetype.sats"-staload "libats/ML/DATS/filebas.dats"-staload EXTRA = "libats/ML/SATS/filebas.sats"-staload "libats/libc/SATS/unistd.sats"-staload "libats/DATS/athread.dats"--fun to_file(s : string, pre : Option(string)) : file =-  let-    val is_comment = case+ pre of-      | Some (x) => string_is_prefix(x, s)-      | None => false-  in-    if s = "" then-      @{ lines = 1, blanks = 1, comments = 0, files = 0 }-    else-      if is_comment then-        @{ lines = 1, blanks = 0, comments = 1, files = 0 }-      else-        @{ lines = 1, blanks = 0, comments = 0, files = 0 }-  end--fun empty_file() : file =-  let-    var f = @{ files = 0, blanks = 0, comments = 0, lines = 0 } : file-  in-    f-  end--fun acc_file() : file =-  let-    var f = @{ files = 1, blanks = 0, comments = 0, lines = ~1 } : file-  in-    f-  end--// monoidal addition for 'file' type-fun add_results(x : file, y : file) : file =-  let-    var next = @{ lines = x.lines + y.lines-                , blanks = x.blanks + y.blanks-                , comments = x.comments + y.comments-                , files = x.files + y.files-                }-  in-    next-  end--overload + with add_results--// Given a string representing a filepath, return an integer.-fun line_count(s : string, pre : Option(string)) : file =-  let-    var ref = fileref_open_opt(s, file_mode_r)-  in-    case ref of-      | ~Some_vt (x) => -        begin-          let-            var viewstream: stream_vt(string) = $EXTRA.streamize_fileref_line(x)-            val n: file = stream_vt_foldleft_cloptr( viewstream-                                                   , acc_file()-                                                   , lam (acc, f) =<cloptr1> acc + to_file(f, pre)-                                                   )-            val _ = fileref_close(x)-          in-            n-          end-        end-      | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)-                      ; to_file(s, None)-                      )-  end--// Pad a string of bounded length on the right by adding spaces.-fnx right_pad { k : int | k >= 0 }{ m : int | m <= k } .<k>.-(s : string(m), n : int(k)) : string =-  case+ length(s) < n of-    | true when n > 0 => right_pad(s, n - 1) + " "-    | _ => s--// Pad a string on the left by adding spaces.-fnx left_pad { k : int | k >= 0 } .<k>. (s : string, n : int(k)) :-  string =-  case+ length(s) < n of-    | true when n > 0 => " " + left_pad(s, n - 1)-    | _ => s--// helper function for make_output-fun maybe_string(s : string, n : int) : string =-  if n > 0 then-    s + ": " + tostring_int(n) + "\n"-  else-    ""--// helper function for make_table-fun maybe_table { k : int | k >= 0 && k < 20 } ( s : string(k)-                                               , f : file-                                               ) : string =-  let-    var code = f.lines - f.comments - f.blanks-  in-    if f.files > 0 then-      " "-      + right_pad(s, 21)-      + left_pad(tostring_int(f.files), 5)-      + left_pad(tostring_int(f.lines), 12)-      + left_pad(tostring_int(code), 13)-      + left_pad(tostring_int(f.comments), 13)-      + left_pad(tostring_int(f.blanks), 13)-      + "\n"-    else-      ""-  end--// helper function for make_output-fun with_nonempty(s1 : string, s2 : string) : string =-  if s2 != "" then-    s1 + s2-  else-    ""--// helper function to make totals for tabular output.-fun sum_fields(sc : source_contents) : file =-  let-    var f = @{ lines = sc.rust.lines-                     + sc.haskell.lines-                     + sc.ats.lines-                     + sc.python.lines-                     + sc.vimscript.lines-                     + sc.elm.lines-                     + sc.idris.lines-                     + sc.madlang.lines-                     + sc.tex.lines-                     + sc.markdown.lines-                     + sc.yaml.lines-                     + sc.toml.lines-                     + sc.cabal.lines-                     + sc.happy.lines-                     + sc.alex.lines-                     + sc.go.lines-                     + sc.html.lines-                     + sc.css.lines-                     + sc.verilog.lines-                     + sc.vhdl.lines-                     + sc.c.lines-                     + sc.purescript.lines-                     + sc.futhark.lines-                     + sc.brainfuck.lines-                     + sc.ruby.lines-                     + sc.julia.lines-                     + sc.perl.lines-                     + sc.ocaml.lines-                     + sc.agda.lines-                     + sc.cobol.lines-                     + sc.tcl.lines-                     + sc.r.lines-                     + sc.lua.lines-                     + sc.cpp.lines-                     + sc.lalrpop.lines-                     + sc.header.lines-                     + sc.sixten.lines-                     + sc.dhall.lines-                     + sc.ipkg.lines-                     + sc.makefile.lines-                     + sc.justfile.lines-                     + sc.ion.lines-                     + sc.bash.lines-                     + sc.hamlet.lines-                     + sc.cassius.lines-                     + sc.lucius.lines-                     + sc.julius.lines-                     + sc.mercury.lines-                     + sc.yacc.lines-                     + sc.lex.lines-                     + sc.coq.lines-                     + sc.jupyter.lines-                     + sc.java.lines-                     + sc.scala.lines-                     + sc.erlang.lines-                     + sc.elixir.lines-                     + sc.pony.lines-                     + sc.clojure.lines-                     + sc.cabal_project.lines-                     + sc.assembly.lines-                     + sc.nix.lines-                     + sc.php.lines-                     + sc.javascript.lines-                     + sc.kotlin.lines-                     + sc.fsharp.lines-                     + sc.fortran.lines-                     + sc.swift.lines-                     + sc.csharp.lines-                     + sc.nim.lines-                     + sc.cpp_header.lines-                     + sc.elisp.lines-                     + sc.plaintext.lines-                     + sc.rakefile.lines-                     + sc.llvm.lines-                     + sc.autoconf.lines-                     + sc.batch.lines-                     + sc.powershell.lines-                     + sc.m4.lines-                     + sc.objective_c.lines-                     + sc.automake.lines-             , blanks = sc.rust.blanks-                      + sc.haskell.blanks-                      + sc.ats.blanks-                      + sc.python.blanks-                      + sc.vimscript.blanks-                      + sc.elm.blanks-                      + sc.idris.blanks-                      + sc.madlang.blanks-                      + sc.tex.blanks-                      + sc.markdown.blanks-                      + sc.yaml.blanks-                      + sc.toml.blanks-                      + sc.cabal.blanks-                      + sc.happy.blanks-                      + sc.alex.blanks-                      + sc.go.blanks-                      + sc.html.blanks-                      + sc.css.blanks-                      + sc.verilog.blanks-                      + sc.vhdl.blanks-                      + sc.c.blanks-                      + sc.purescript.blanks-                      + sc.futhark.blanks-                      + sc.brainfuck.blanks-                      + sc.ruby.blanks-                      + sc.julia.blanks-                      + sc.perl.blanks-                      + sc.ocaml.blanks-                      + sc.agda.blanks-                      + sc.cobol.blanks-                      + sc.tcl.blanks-                      + sc.r.blanks-                      + sc.lua.blanks-                      + sc.cpp.blanks-                      + sc.lalrpop.blanks-                      + sc.header.blanks-                      + sc.sixten.blanks-                      + sc.dhall.blanks-                      + sc.ipkg.blanks-                      + sc.makefile.blanks-                      + sc.justfile.blanks-                      + sc.ion.blanks-                      + sc.bash.blanks-                      + sc.hamlet.blanks-                      + sc.cassius.blanks-                      + sc.lucius.blanks-                      + sc.julius.blanks-                      + sc.mercury.blanks-                      + sc.yacc.blanks-                      + sc.lex.blanks-                      + sc.coq.blanks-                      + sc.jupyter.blanks-                      + sc.java.blanks-                      + sc.scala.blanks-                      + sc.erlang.blanks-                      + sc.elixir.blanks-                      + sc.pony.blanks-                      + sc.clojure.blanks-                      + sc.cabal_project.blanks-                      + sc.assembly.blanks-                      + sc.nix.blanks-                      + sc.php.blanks-                      + sc.javascript.blanks-                      + sc.kotlin.blanks-                      + sc.fsharp.blanks-                      + sc.fortran.blanks-                      + sc.swift.blanks-                      + sc.csharp.blanks-                      + sc.nim.blanks-                      + sc.cpp_header.blanks-                      + sc.elisp.blanks-                      + sc.plaintext.blanks-                      + sc.rakefile.blanks-                      + sc.llvm.blanks-                      + sc.autoconf.blanks-                      + sc.batch.blanks-                      + sc.powershell.blanks-                      + sc.m4.blanks-                      + sc.objective_c.blanks-                      + sc.automake.blanks-             , comments = sc.rust.comments-                        + sc.haskell.comments-                        + sc.ats.comments-                        + sc.python.comments-                        + sc.vimscript.comments-                        + sc.elm.comments-                        + sc.idris.comments-                        + sc.madlang.comments-                        + sc.tex.comments-                        + sc.markdown.comments-                        + sc.yaml.comments-                        + sc.toml.comments-                        + sc.cabal.comments-                        + sc.happy.comments-                        + sc.alex.comments-                        + sc.go.comments-                        + sc.html.comments-                        + sc.css.comments-                        + sc.verilog.comments-                        + sc.vhdl.comments-                        + sc.c.comments-                        + sc.purescript.comments-                        + sc.futhark.comments-                        + sc.brainfuck.comments-                        + sc.ruby.comments-                        + sc.julia.comments-                        + sc.perl.comments-                        + sc.ocaml.comments-                        + sc.agda.comments-                        + sc.cobol.comments-                        + sc.tcl.comments-                        + sc.r.comments-                        + sc.lua.comments-                        + sc.cpp.comments-                        + sc.lalrpop.comments-                        + sc.header.comments-                        + sc.sixten.comments-                        + sc.dhall.comments-                        + sc.ipkg.comments-                        + sc.makefile.comments-                        + sc.justfile.comments-                        + sc.ion.comments-                        + sc.bash.comments-                        + sc.hamlet.comments-                        + sc.cassius.comments-                        + sc.lucius.comments-                        + sc.julius.comments-                        + sc.mercury.comments-                        + sc.yacc.comments-                        + sc.lex.comments-                        + sc.coq.comments-                        + sc.jupyter.comments-                        + sc.java.comments-                        + sc.scala.comments-                        + sc.erlang.comments-                        + sc.elixir.comments-                        + sc.pony.comments-                        + sc.clojure.comments-                        + sc.cabal_project.comments-                        + sc.assembly.comments-                        + sc.nix.comments-                        + sc.php.comments-                        + sc.javascript.comments-                        + sc.kotlin.comments-                        + sc.fsharp.comments-                        + sc.fortran.comments-                        + sc.swift.comments-                        + sc.csharp.comments-                        + sc.nim.comments-                        + sc.cpp_header.comments-                        + sc.elisp.comments-                        + sc.plaintext.comments-                        + sc.rakefile.comments-                        + sc.llvm.comments-                        + sc.autoconf.comments-                        + sc.batch.comments-                        + sc.powershell.comments-                        + sc.m4.comments-                        + sc.objective_c.comments-                        + sc.automake.comments-             , files = sc.rust.files-                     + sc.haskell.files-                     + sc.ats.files-                     + sc.python.files-                     + sc.vimscript.files-                     + sc.elm.files-                     + sc.idris.files-                     + sc.madlang.files-                     + sc.tex.files-                     + sc.markdown.files-                     + sc.yaml.files-                     + sc.toml.files-                     + sc.cabal.files-                     + sc.happy.files-                     + sc.alex.files-                     + sc.go.files-                     + sc.html.files-                     + sc.css.files-                     + sc.verilog.files-                     + sc.vhdl.files-                     + sc.c.files-                     + sc.purescript.files-                     + sc.futhark.files-                     + sc.brainfuck.files-                     + sc.ruby.files-                     + sc.julia.files-                     + sc.perl.files-                     + sc.ocaml.files-                     + sc.agda.files-                     + sc.cobol.files-                     + sc.tcl.files-                     + sc.r.files-                     + sc.lua.files-                     + sc.cpp.files-                     + sc.lalrpop.files-                     + sc.header.files-                     + sc.sixten.files-                     + sc.dhall.files-                     + sc.ipkg.files-                     + sc.makefile.files-                     + sc.justfile.files-                     + sc.ion.files-                     + sc.bash.files-                     + sc.hamlet.files-                     + sc.cassius.files-                     + sc.lucius.files-                     + sc.julius.files-                     + sc.mercury.files-                     + sc.yacc.files-                     + sc.lex.files-                     + sc.coq.files-                     + sc.jupyter.files-                     + sc.java.files-                     + sc.scala.files-                     + sc.erlang.files-                     + sc.elixir.files-                     + sc.pony.files-                     + sc.clojure.files-                     + sc.cabal_project.files-                     + sc.assembly.files-                     + sc.nix.files-                     + sc.php.files-                     + sc.javascript.files-                     + sc.kotlin.files-                     + sc.fsharp.files-                     + sc.fortran.files-                     + sc.swift.files-                     + sc.csharp.files-                     + sc.nim.files-                     + sc.cpp_header.files-                     + sc.elisp.files-                     + sc.plaintext.files-                     + sc.rakefile.files-                     + sc.llvm.files-                     + sc.autoconf.files-                     + sc.batch.files-                     + sc.powershell.files-                     + sc.m4.files-                     + sc.objective_c.files-                     + sc.automake.files-             }-  in-    f-  end--// function to print tabular output at the end-fun make_table(isc : source_contents) : string =-  "-------------------------------------------------------------------------------\n \33[35mLanguage\33[0m            \33[35mFiles\33[0m        \33[35mLines\33[0m         \33[35mCode\33[0m     \33[35mComments\33[0m       \33[35mBlanks\33[0m\n-------------------------------------------------------------------------------\n"-  + maybe_table("Alex", isc.alex)-  + maybe_table("Agda", isc.agda)-  + maybe_table("Assembly", isc.assembly)-  + maybe_table("ATS", isc.ats)-  + maybe_table("Autoconf", isc.autoconf)-  + maybe_table("Automake", isc.automake)-  + maybe_table("Bash", isc.bash)-  + maybe_table("Batch", isc.batch)-  + maybe_table("Brainfuck", isc.brainfuck)-  + maybe_table("C", isc.c)-  + maybe_table("C Header", isc.header)-  + maybe_table("C++ cpp_header", isc.cpp_header)-  + maybe_table("C++", isc.cpp)-  + maybe_table("C#", isc.csharp)-  + maybe_table("Cabal", isc.cabal)-  + maybe_table("Cabal Project", isc.cabal_project)-  + maybe_table("Cassius", isc.cassius)-  + maybe_table("COBOL", isc.cobol)-  + maybe_table("Coq", isc.coq)-  + maybe_table("CSS", isc.css)-  + maybe_table("Dhall", isc.dhall)-  + maybe_table("Elixir", isc.elixir)-  + maybe_table("Elm", isc.elm)-  + maybe_table("Emacs Lisp", isc.elisp)-  + maybe_table("Erlang", isc.erlang)-  + maybe_table("F#", isc.fsharp)-  + maybe_table("Fortran", isc.fortran)-  + maybe_table("Go", isc.go)-  + maybe_table("Hamlet", isc.hamlet)-  + maybe_table("Happy", isc.happy)-  + maybe_table("Haskell", isc.haskell)-  + maybe_table("HTML", isc.html)-  + maybe_table("Idris", isc.idris)-  + maybe_table("iPKG", isc.ipkg)-  + maybe_table("Ion", isc.ion)-  + maybe_table("Java", isc.java)-  + maybe_table("JavaScript", isc.javascript)-  + maybe_table("Julius", isc.julius)-  + maybe_table("Julia", isc.julia)-  + maybe_table("Jupyter", isc.jupyter)-  + maybe_table("Justfile", isc.justfile)-  + maybe_table("Kotlin", isc.kotlin)-  + maybe_table("LALRPOP", isc.lalrpop)-  + maybe_table("Lex", isc.lex)-  + maybe_table("LLVM", isc.llvm)-  + maybe_table("Lua", isc.lua)-  + maybe_table("Lucius", isc.lucius)-  + maybe_table("M4", isc.m4)-  + maybe_table("Madlang", isc.madlang)-  + maybe_table("Makefile", isc.makefile)-  + maybe_table("Margaret", isc.margaret)-  + maybe_table("Markdown", isc.markdown)-  + maybe_table("Mercury", isc.mercury)-  + maybe_table("Nim", isc.nim)-  + maybe_table("Nix", isc.nix)-  + maybe_table("Objective C", isc.objective_c)-  + maybe_table("OCaml", isc.ocaml)-  + maybe_table("Perl", isc.perl)-  + maybe_table("PHP", isc.php)-  + maybe_table("Plaintext", isc.plaintext)-  + maybe_table("PowerShell", isc.powershell)-  + maybe_table("Pony", isc.pony)-  + maybe_table("Python", isc.python)-  + maybe_table("PureScript", isc.purescript)-  + maybe_table("R", isc.r)-  + maybe_table("Rakefile", isc.rakefile)-  + maybe_table("Ruby", isc.ruby)-  + maybe_table("Rust", isc.rust)-  + maybe_table("Scala", isc.scala)-  + maybe_table("Sixten", isc.sixten)-  + maybe_table("Swift", isc.swift)-  + maybe_table("TCL", isc.tcl)-  + maybe_table("TeX", isc.tex)-  + maybe_table("TOML", isc.toml)-  + maybe_table("Verilog", isc.verilog)-  + maybe_table("VHDL", isc.vhdl)-  + maybe_table("Vimscript", isc.vimscript)-  + maybe_table("Yacc", isc.yacc)-  + maybe_table("YAML", isc.yaml)-  + "-------------------------------------------------------------------------------\n"-  + maybe_table("Total", sum_fields(isc))-  + "-------------------------------------------------------------------------------\n"--// Function to print output sorted by type of language.-fun make_output(isc : source_contents) : string =-  with_nonempty( "\33[33mProgramming Languages:\33[0m\n"-               , maybe_string("Agda", isc.agda.lines)-               + maybe_string("Assembly", isc.assembly.lines)-               + maybe_string("ATS", isc.ats.lines)-               + maybe_string("Brainfuck", isc.brainfuck.lines)-               + maybe_string("C", isc.c.lines)-               + maybe_string("C Header", isc.header.lines)-               + maybe_string("C++", isc.cpp.lines)-               + maybe_string("C++ Header", isc.cpp_header.lines)-               + maybe_string("C#", isc.csharp.lines)-               + maybe_string("COBOL", isc.cobol.lines)-               + maybe_string("Coq", isc.coq.lines)-               + maybe_string("Elixir", isc.elixir.lines)-               + maybe_string("Elm", isc.elm.lines)-               + maybe_string("Erlang", isc.erlang.lines)-               + maybe_string("F#", isc.fsharp.lines)-               + maybe_string("Fortran", isc.fortran.lines)-               + maybe_string("Go", isc.go.lines)-               + maybe_string("Haskell", isc.haskell.lines)-               + maybe_string("Idris", isc.idris.lines)-               + maybe_string("Kotline", isc.kotlin.lines)-               + maybe_string("Java", isc.java.lines)-               + maybe_string("Julia", isc.julia.lines)-               + maybe_string("Lua", isc.lua.lines)-               + maybe_string("Margaret", isc.margaret.lines)-               + maybe_string("Mercury", isc.mercury.lines)-               + maybe_string("Nim", isc.nim.lines)-               + maybe_string("Objective C", isc.objective_c.lines)-               + maybe_string("OCaml", isc.ocaml.lines)-               + maybe_string("Perl", isc.perl.lines)-               + maybe_string("Pony", isc.pony.lines)-               + maybe_string("PureScript", isc.purescript.lines)-               + maybe_string("Python", isc.python.lines)-               + maybe_string("R", isc.r.lines)-               + maybe_string("Ruby", isc.ruby.lines)-               + maybe_string("Rust", isc.rust.lines)-               + maybe_string("Scala", isc.scala.lines)-               + maybe_string("Sixten", isc.sixten.lines)-               + maybe_string("Swift", isc.swift.lines)-               + maybe_string("TCL", isc.tcl.lines)-               )-  + with_nonempty( "\n\33[33mEditor Plugins:\33[0m\n"-                 , maybe_string("Emacs Lisp", isc.elisp.lines)-                 + maybe_string("Vimscript", isc.vimscript.lines)-                 )-  + with_nonempty( "\n\33[33mDocumentation:\33[0m\n"-                 , maybe_string("Markdown", isc.markdown.lines)-                 + maybe_string("Plaintext", isc.plaintext.lines)-                 + maybe_string("TeX", isc.tex.lines)-                 )-  + with_nonempty( "\n\33[33mConfiguration:\33[0m\n"-                 , maybe_string("Cabal", isc.cabal.lines)-                 + maybe_string("Cabal Project", isc.cabal_project.lines)-                 + maybe_string("Dhall", isc.dhall.lines)-                 + maybe_string("iPKG", isc.ipkg.lines)-                 + maybe_string("TOML", isc.toml.lines)-                 + maybe_string("YAML", isc.yaml.lines)-                 )-  + with_nonempty( "\n\33[33mShell:\33[0m\n"-                 , maybe_string("Bash", isc.bash.lines)-                 + maybe_string("Batch", isc.batch.lines)-                 + maybe_string("Ion", isc.ion.lines)-                 + maybe_string("PowerShell", isc.powershell.lines)-                 )-  + with_nonempty( "\n\33[33mParser Generators:\33[0m\n"-                 , maybe_string("Alex", isc.alex.lines)-                 + maybe_string("Happy", isc.happy.lines)-                 + maybe_string("LALRPOP", isc.lalrpop.lines)-                 + maybe_string("Lex", isc.lex.lines)-                 + maybe_string("Yacc", isc.yacc.lines)-                 )-  + with_nonempty( "\n\33[33mWeb:\33[0m\n"-                 , maybe_string("Cassius", isc.cassius.lines)-                 + maybe_string("CSS", isc.css.lines)-                 + maybe_string("Hamlet", isc.hamlet.lines)-                 + maybe_string("HTML", isc.html.lines)-                 + maybe_string("JavaScript", isc.javascript.lines)-                 + maybe_string("Julius", isc.julius.lines)-                 + maybe_string("Lucius", isc.lucius.lines)-                 )-  + with_nonempty( "\n\33[33mHardware:\33[0m\n"-                 , maybe_string("Verilog", isc.verilog.lines)-                 + maybe_string("VHDL", isc.vhdl.lines)-                 )-  + with_nonempty( "\n\33[33mNotebooks:\33[0m\n"-                 , maybe_string("Jupyter", isc.jupyter.lines)-                 )-  + with_nonempty( "\n\33[33mOther:\33[0m\n"-                 , maybe_string("Autoconf", isc.autoconf.lines)-                 + maybe_string("Automake", isc.automake.lines)-                 + maybe_string("Justfile", isc.justfile.lines)-                 + maybe_string("LLVM", isc.llvm.lines)-                 + maybe_string("M4", isc.m4.lines)-                 + maybe_string("Madlang", isc.madlang.lines)-                 + maybe_string("Makefile", isc.makefile.lines)-                 + maybe_string("Rakefile", isc.rakefile.lines)-                 )--fun add_contents(x : source_contents, y : source_contents) :-  source_contents =-  let-    var next = @{ rust = x.rust + y.rust-                , haskell = x.haskell + y.haskell-                , ats = x.ats + y.ats-                , python = x.python + y.python-                , vimscript = x.vimscript + y.vimscript-                , elm = x.elm + y.elm-                , idris = x.idris + y.idris-                , madlang = x.madlang + y.madlang-                , tex = x.tex + y.tex-                , markdown = x.markdown + y.markdown-                , yaml = x.yaml + y.yaml-                , toml = x.toml + y.toml-                , cabal = x.cabal + y.cabal-                , happy = x.happy + y.happy-                , alex = x.alex + y.alex-                , go = x.go + y.go-                , html = x.html + y.html-                , css = x.css + y.css-                , verilog = x.verilog + y.verilog-                , vhdl = x.vhdl + y.vhdl-                , c = x.c + y.c-                , purescript = x.purescript + y.purescript-                , futhark = x.futhark + y.futhark-                , brainfuck = x.brainfuck + y.brainfuck-                , ruby = x.ruby + y.ruby-                , julia = x.julia + y.julia-                , perl = x.perl + y.perl-                , ocaml = x.ocaml + y.ocaml-                , agda = x.agda + y.agda-                , cobol = x.cobol + y.cobol-                , tcl = x.tcl + y.tcl-                , r = x.r + y.r-                , lua = x.lua + y.lua-                , cpp = x.cpp + y.cpp-                , lalrpop = x.lalrpop + y.lalrpop-                , header = x.header + y.header-                , sixten = x.sixten + y.sixten-                , dhall = x.dhall + y.dhall-                , ipkg = x.ipkg + y.ipkg-                , makefile = x.makefile + y.makefile-                , justfile = x.justfile + y.justfile-                , ion = x.ion + y.ion-                , bash = x.bash + y.bash-                , hamlet = x.hamlet + y.hamlet-                , cassius = x.cassius + y.cassius-                , lucius = x.lucius + y.lucius-                , julius = x.julius + y.julius-                , mercury = x.mercury + y.mercury-                , yacc = x.yacc + y.yacc-                , lex = x.lex + y.lex-                , coq = x.coq + y.coq-                , jupyter = x.jupyter + y.jupyter-                , java = x.java + y.java-                , scala = x.scala + y.scala-                , erlang = x.erlang + y.erlang-                , elixir = x.elixir + y.elixir-                , pony = x.pony + y.pony-                , clojure = x.clojure + y.clojure-                , cabal_project = x.cabal_project + y.cabal_project-                , assembly = x.assembly + y.assembly-                , nix = x.nix + y.nix-                , php = x.php + y.php-                , javascript = x.javascript + y.javascript-                , kotlin = x.kotlin + y.kotlin-                , fsharp = x.fsharp + y.fsharp-                , fortran = x.fortran + y.fortran-                , swift = x.swift + y.swift-                , csharp = x.csharp + y.csharp-                , nim = x.nim + y.nim-                , cpp_header = x.cpp_header + y.cpp_header-                , elisp = x.elisp + y.elisp-                , plaintext = x.plaintext + y.plaintext-                , rakefile = x.rakefile + y.rakefile-                , llvm = x.llvm + y.llvm-                , autoconf = x.autoconf + y.autoconf-                , batch = x.batch + y.batch-                , powershell = x.powershell + y.powershell-                , m4 = x.m4 + y.m4-                , objective_c = x.objective_c + y.objective_c-                , automake = x.automake + y.automake-                , margaret = x.margaret + y.margaret-                } : source_contents-  in-    next-  end--// This is the step function used when streaming directory contents. -fun adjust_contents(prev : source_contents, scf : pl_type) :-  source_contents =-  let-    val sc_r = ref<source_contents>(prev)-    val _ = case+ scf of-      | ~haskell n => sc_r->haskell := prev.haskell + n-      | ~ats n => sc_r->ats := prev.ats + n-      | ~rust n => sc_r->rust := prev.rust + n-      | ~markdown n => sc_r->markdown := prev.markdown + n-      | ~python n => sc_r->python := prev.python + n-      | ~vimscript n => sc_r->vimscript := prev.vimscript + n-      | ~yaml n => sc_r->yaml := prev.yaml + n-      | ~toml n => sc_r->toml := prev.toml + n-      | ~happy n => sc_r->happy := prev.happy + n-      | ~alex n => sc_r->alex := prev.alex + n-      | ~idris n => sc_r->idris := prev.idris + n-      | ~madlang n => sc_r->madlang := prev.madlang + n-      | ~elm n => sc_r->elm := prev.elm + n-      | ~c n => sc_r->c := prev.c + n-      | ~go n => sc_r->go := prev.go + n-      | ~cabal n => sc_r->cabal := prev.cabal + n-      | ~verilog n => sc_r->verilog := prev.verilog + n-      | ~vhdl n => sc_r->vhdl := prev.vhdl + n-      | ~html n => sc_r->html := prev.html + n-      | ~css n => sc_r->css := prev.css + n-      | ~purescript n => sc_r->purescript := prev.purescript + n-      | ~futhark n => sc_r->futhark := prev.futhark + n-      | ~brainfuck n => sc_r->brainfuck := prev.brainfuck + n-      | ~ruby n => sc_r->ruby := prev.ruby + n-      | ~julia n => sc_r->julia := prev.julia + n-      | ~tex n => sc_r->tex := prev.tex + n-      | ~perl n => sc_r->perl := prev.perl + n-      | ~ocaml n => sc_r->ocaml := prev.ocaml + n-      | ~agda n => sc_r->agda := prev.agda + n-      | ~cobol n => sc_r->cobol := prev.cobol + n-      | ~tcl n => sc_r->tcl := prev.tcl + n-      | ~r n => sc_r->r := prev.r + n-      | ~lua n => sc_r->lua := prev.lua + n-      | ~cpp n => sc_r->cpp := prev.cpp + n-      | ~lalrpop n => sc_r->lalrpop := prev.lalrpop + n-      | ~header n => sc_r->header := prev.header + n-      | ~sixten n => sc_r->sixten := prev.sixten + n-      | ~dhall n => sc_r->dhall := prev.dhall + n-      | ~ipkg n => sc_r->ipkg := prev.ipkg + n-      | ~justfile n => sc_r->justfile := prev.justfile + n-      | ~makefile n => sc_r->makefile := prev.makefile + n-      | ~ion n => sc_r->ion := prev.ion + n-      | ~bash n => sc_r->bash := prev.bash + n-      | ~hamlet n => sc_r->hamlet := prev.hamlet + n-      | ~cassius n => sc_r->cassius := prev.cassius + n-      | ~lucius n => sc_r->lucius := prev.lucius + n-      | ~julius n => sc_r->julius := prev.julius + n-      | ~mercury n => sc_r->mercury := prev.mercury + n-      | ~yacc n => sc_r->yacc := prev.yacc + n-      | ~lex n => sc_r->lex := prev.lex + n-      | ~coq n => sc_r->coq := prev.coq + n-      | ~jupyter n => sc_r->jupyter := prev.jupyter + n-      | ~java n => sc_r->java := prev.java + n-      | ~scala n => sc_r->scala := prev.scala + n-      | ~erlang n => sc_r->erlang := prev.erlang + n-      | ~elixir n => sc_r->elixir := prev.elixir + n-      | ~pony n => sc_r->pony := prev.pony + n-      | ~clojure n => sc_r->clojure := prev.clojure + n-      | ~cabal_project n => sc_r->cabal_project := prev.cabal_project + n-      | ~assembly n => sc_r->assembly := prev.assembly + n-      | ~nix n => sc_r->nix := prev.nix + n-      | ~php n => sc_r->php := prev.php + n-      | ~javascript n => sc_r->javascript := prev.javascript + n-      | ~kotlin n => sc_r->kotlin := prev.kotlin + n-      | ~fsharp n => sc_r->fsharp := prev.fsharp + n-      | ~fortran n => sc_r->fortran := prev.fortran + n-      | ~swift n => sc_r->swift := prev.swift + n-      | ~csharp n => sc_r->csharp := prev.csharp + n-      | ~nim n => sc_r->nim := prev.nim + n-      | ~cpp_header n => sc_r->cpp_header := prev.cpp_header + n-      | ~elisp n => sc_r->elisp := prev.elisp + n-      | ~plaintext n => sc_r->plaintext := prev.plaintext + n-      | ~rakefile n => sc_r->rakefile := prev.rakefile + n-      | ~llvm n => sc_r->llvm := prev.llvm + n-      | ~autoconf n => sc_r->autoconf := prev.autoconf + n-      | ~batch n => sc_r->batch := prev.batch + n-      | ~powershell n => sc_r->powershell := prev.powershell + n-      | ~m4 n => sc_r->m4 := prev.m4 + n-      | ~objective_c n => sc_r->objective_c := prev.objective_c + n-      | ~automake n => sc_r->automake := prev.automake + n-      | ~margaret n => sc_r->margaret := prev.margaret + n-      | ~unknown _ => ()-  in-    !sc_r-  end--fun free_pl(pl : pl_type) : void =-  case+ pl of-    | ~unknown _ => ()-    | ~rust _ => ()-    | ~haskell _ => ()-    | ~perl _ => ()-    | ~lucius _ => ()-    | ~cassius _ => ()-    | ~hamlet _ => ()-    | ~julius _ => ()-    | ~bash _ => ()-    | ~coq _ => ()-    | ~justfile _ => ()-    | ~makefile _ => ()-    | ~yaml _ => ()-    | ~toml _ => ()-    | ~dhall _ => ()-    | ~ipkg _ => ()-    | ~ion _ => ()-    | ~mercury _ => ()-    | ~yacc _ => ()-    | ~lex _ => ()-    | ~r _ => ()-    | ~c _ => ()-    | ~cpp _ => ()-    | ~lua _ => ()-    | ~lalrpop _ => ()-    | ~header _ => ()-    | ~sixten _ => ()-    | ~java _ => ()-    | ~scala _ => ()-    | ~elixir _ => ()-    | ~erlang _ => ()-    | ~happy _ => ()-    | ~alex _ => ()-    | ~go _ => ()-    | ~html _ => ()-    | ~css _ => ()-    | ~brainfuck _ => ()-    | ~ruby _ => ()-    | ~julia _ => ()-    | ~elm _ => ()-    | ~purescript _ => ()-    | ~vimscript _ => ()-    | ~ocaml _ => ()-    | ~madlang _ => ()-    | ~agda _ => ()-    | ~idris _ => ()-    | ~futhark _ => ()-    | ~ats _ => ()-    | ~tex _ => ()-    | ~cabal _ => ()-    | ~cobol _ => ()-    | ~tcl _ => ()-    | ~verilog _ => ()-    | ~vhdl _ => ()-    | ~markdown _ => ()-    | ~python _ => ()-    | ~pony _ => ()-    | ~jupyter _ => ()-    | ~clojure _ => ()-    | ~cabal_project _ => ()-    | ~assembly _ => ()-    | ~nix _ => ()-    | ~php _ => ()-    | ~javascript _ => ()-    | ~kotlin _ => ()-    | ~fsharp _ => ()-    | ~fortran _ => ()-    | ~swift _ => ()-    | ~csharp _ => ()-    | ~nim _ => ()-    | ~cpp_header _ => ()-    | ~elisp _ => ()-    | ~plaintext _ => ()-    | ~rakefile _ => ()-    | ~llvm _ => ()-    | ~autoconf _ => ()-    | ~batch _ => ()-    | ~powershell _ => ()-    | ~m4 _ => ()-    | ~objective_c _ => ()-    | ~automake _ => ()-    | ~margaret _ => ()--// match a particular word against a list of keywords-fun match_keywords { m : nat | m <= 10 } ( keys : list(string, m)-                                         , word : string-                                         ) : bool =-  list_foldright_cloref(keys, lam (next, acc) =<cloref1> acc-                       || eq_string_string(next, word), false)--// TODO use list_vt{int}(0, 1, 2, 3, 4) instead?-// helper function for check_keywords-fun step_keyword( size : file-                , pre : pl_type-                , word : string-                , ext : string-                ) : pl_type =-  case+ pre of-    | unknown _ => let-      -    in-      case+ ext of-        | "y" => let-          val _ = free_pl(pre)-          var happy_keywords = list_cons("module", list_nil())-        in-          if match_keywords(happy_keywords, word) then-            happy(size)-          else-            if let-              var yacc_keywords = list_cons( "struct"-                                           , list_cons("char", list_cons("int", list_nil()))-                                           )-            in-              match_keywords(yacc_keywords, word)-            end then-              yacc(size)-            else-              unknown-        end-        | "v" => let-          var _ = free_pl(pre)-          var verilog_keywords = list_cons( "endmodule"-                                          , list_cons( "posedge"-                                                     , list_cons( "edge"-                                                                , list_cons("always", list_cons("wire", list_nil()))-                                                                )-                                                     )-                                          )-        in-          if match_keywords( verilog_keywords-                           , word-                           ) then-            verilog(size)-          else-            if let-              var coq_keywords = list_cons( "Qed"-                                          , list_cons( "Require"-                                                     , list_cons( "Hypothesis"-                                                                , list_cons( "Inductive"-                                                                           , list_cons( "Remark"-                                                                                      , list_cons( "Lemma"-                                                                                                 , list_cons( "Proof"-                                                                                                            , list_cons( "Definition"-                                                                                                                       , list_cons( "Theorem"-                                                                                                                                  , list_nil()-                                                                                                                                  )-                                                                                                                       )-                                                                                                            )-                                                                                                 )-                                                                                      )-                                                                           )-                                                                )-                                                     )-                                          )-            in-              match_keywords(coq_keywords, word)-            end then-              coq(size)-            else-              unknown-        end-        | "m" => let-          val _ = free_pl(pre)-          var mercury_keywords = list_cons( "module"-                                          , list_cons("pred", list_cons("mode", list_nil()))-                                          )-        in-          if match_keywords(mercury_keywords, word) then-            mercury(size)-          else-            if let-              var objective_c_keywords = list_cons( "nil"-                                                  , list_cons("nullable", list_cons("nonnull", list_nil()))-                                                  )-            in-              match_keywords(objective_c_keywords, word)-            end then-              objective_c(size)-            else-              unknown-        end-        | _ => pre-    end-    | _ => pre--// Function to disambiguate extensions such as .v (Coq and Verilog) and .m-// (Mercury and Objective C). This should only be called when extensions are in-// conflict, as it reads the whole file.-fun check_keywords(s : string, size : file, ext : string) : pl_type =-  let-    var ref = fileref_open_opt(s, file_mode_r)-  in-    case+ ref of-      | ~Some_vt (x) => let-        var init: pl_type = unknown-        var viewstream = $EXTRA.streamize_fileref_word(x)-        val result = stream_vt_foldleft_cloptr( viewstream-                                              , init-                                              , lam (acc, next) =>-                                                  step_keyword(size, acc, next, ext)-                                              )-        val _ = fileref_close(x)-      in-        result-      end-      | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)-                      ; unknown-                      )-  end--// Check shebang on scripts.-//-// TODO flexible parser that drops spaces as appropriate-// TODO check magic number so as to avoid checking shebang of binary file-fun check_shebang(s : string) : pl_type =-  let-    val ref = fileref_open_opt(s, file_mode_r)-    val str: string = case+ ref of-      | ~Some_vt (x) => let-        val s = strptr2string(fileref_get_line_string(x))-        val _ = fileref_close(x)-      in-        s-      end-      | ~None_vt() => ( println!("\33[33mWarning:\33[0m could not open file at " + s)-                      ; ""-                      )-  in-    case+ str of-      | "#!/usr/bin/env ion" => ion(line_count(s, Some("#")))-      | "#!/usr/bin/env bash" => bash(line_count(s, Some("#")))-      | "#!/bin/bash" => bash(line_count(s, Some("#")))-      | "#!python" => python(line_count(s, Some("#")))-      | "#!python2" => python(line_count(s, Some("#")))-      | "#!python3" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python2" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env python3" => python(line_count(s, Some("#")))-      | "#!/usr/bin/env perl" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/env perl6" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/perl" => perl(line_count(s, Some("#")))-      | "#!/usr/bin/env stack" => haskell(line_count(s, Some("--")))-      | "#!/usr/bin/env runhaskell" => haskell(line_count(s, Some("--")))-      | "#!/usr/bin/env node" => javascript(line_count(s, None))-      | _ => unknown-  end--// Match based on filename (for makefiles, etc.)-fun match_filename(s : string) : pl_type =-  let-    val (prf | str) = filename_get_base(s)-    val match = $UN.strptr2string(str)-    prval () = prf(str)-  in-    case+ match of-      | "Makefile" => makefile(line_count(s, Some("#")))-      | "Makefile.tc" => makefile(line_count(s, Some("#")))-      | "makefile" => makefile(line_count(s, Some("#")))-      | "GNUmakefile" => makefile(line_count(s, Some("#")))-      | "Justfile" => justfile(line_count(s, Some("#")))-      | "justfile" => justfile(line_count(s, Some("#")))-      | "Rakefile" => rakefile(line_count(s, None))-      | "cabal.project.local" => cabal_project(line_count(s, Some("--")))-      | _ => check_shebang(s)-  end--// Match based on file extension (assuming the file name is passed in as an-// argument).-fun prune_extension(s : string, file_proper : string) : pl_type =-  let-    val (prf | str) = filename_get_ext(file_proper)-    val match: string = if strptr2ptr(str) > 0 then-      $UN.strptr2string(str)-    else-      ""-    prval () = prf(str)-  in-    case+ match of-      | "hs" => haskell(line_count(s, Some("--")))-      | "hs-boot" => haskell(line_count(s, Some("--")))-      | "hsig" => haskell(line_count(s, Some("--")))-      | "rs" => rust(line_count(s, Some("//")))-      | "tex" => tex(line_count(s, Some("%")))-      | "md" => markdown(line_count(s, None))-      | "markdown" => markdown(line_count(s, None))-      | "dats" => ats(line_count(s, Some("//")))-      | "hats" => ats(line_count(s, Some("//")))-      | "cats" => ats(line_count(s, Some("//")))-      | "sats" => ats(line_count(s, Some("//")))-      | "py" => python(line_count(s, None))-      | "fut" => futhark(line_count(s, Some("--")))-      | "pl" => perl(line_count(s, None))-      | "agda" => agda(line_count(s, Some("--")))-      | "idr" => idris(line_count(s, Some("--")))-      | "v" => check_keywords(s, line_count(s, Some("--")), match)-      | "m" => check_keywords(s, line_count(s, None), match)-      | "vhdl" => vhdl(line_count(s, None))-      | "vhd" => vhdl(line_count(s, None))-      | "go" => go(line_count(s, Some("//")))-      | "vim" => vimscript(line_count(s, None))-      | "ml" => ocaml(line_count(s, None))-      | "purs" => purescript(line_count(s, None))-      | "elm" => elm(line_count(s, Some("--")))-      | "mad" => madlang(line_count(s, Some("#")))-      | "toml" => toml(line_count(s, Some("#")))-      | "cabal" => cabal(line_count(s, Some("--")))-      | "yml" => yaml(line_count(s, Some("#")))-      | "yaml" => yaml(line_count(s, Some("#")))-      | "y" => check_keywords(s, line_count(s, None), match)-      | "ypp" => yacc(line_count(s, Some("//")))-      | "x" => alex(line_count(s, Some("--")))-      | "l" => lex(line_count(s, None))-      | "lpp" => lex(line_count(s, None))-      | "html" => html(line_count(s, None))-      | "htm" => html(line_count(s, None))-      | "css" => css(line_count(s, None))-      | "vhdl" => vhdl(line_count(s, None))-      | "vhd" => vhdl(line_count(s, None))-      | "c" => c(line_count(s, Some("//")))-      | "b" => brainfuck(line_count(s, None))-      | "bf" => brainfuck(line_count(s, None))-      | "rb" => ruby(line_count(s, None))-      | "cob" => cobol(line_count(s, None))-      | "cbl" => cobol(line_count(s, None))-      | "cpy" => cobol(line_count(s, None))-      | "ml" => ocaml(line_count(s, None))-      | "tcl" => tcl(line_count(s, None))-      | "r" => r(line_count(s, None))-      | "R" => r(line_count(s, None))-      | "lua" => lua(line_count(s, None))-      | "cpp" => cpp(line_count(s, Some("//")))-      | "cc" => cpp(line_count(s, Some("//")))-      | "lalrpop" => lalrpop(line_count(s, Some("//")))-      | "h" => header(line_count(s, None))-      | "vix" => sixten(line_count(s, Some("--")))-      | "dhall" => dhall(line_count(s, None))-      | "ipkg" => ipkg(line_count(s, Some("--")))-      | "mk" => makefile(line_count(s, Some("#")))-      | "hamlet" => hamlet(line_count(s, None))-      | "cassius" => cassius(line_count(s, None))-      | "lucius" => cassius(line_count(s, None))-      | "julius" => julius(line_count(s, None))-      | "jl" => julia(line_count(s, None))-      | "ion" => ion(line_count(s, Some("#")))-      | "bash" => bash(line_count(s, Some("#")))-      | "ipynb" => jupyter(line_count(s, None))-      | "java" => java(line_count(s, None))-      | "scala" => scala(line_count(s, None))-      | "erl" => erlang(line_count(s, None))-      | "hrl" => erlang(line_count(s, None))-      | "ex" => elixir(line_count(s, None))-      | "exs" => elixir(line_count(s, None))-      | "pony" => pony(line_count(s, None))-      | "clj" => clojure(line_count(s, None))-      | "s" => assembly(line_count(s, Some(";")))-      | "S" => assembly(line_count(s, Some(";")))-      | "asm" => assembly(line_count(s, Some(";")))-      | "nix" => nix(line_count(s, None))-      | "php" => php(line_count(s, None))-      | "local" => match_filename(s)-      | "project" => cabal_project(line_count(s, Some("--")))-      | "js" => javascript(line_count(s, None))-      | "jsexe" => javascript(line_count(s, None))-      | "kt" => kotlin(line_count(s, None))-      | "kts" => kotlin(line_count(s, None))-      | "fs" => fsharp(line_count(s, None))-      | "f" => fortran(line_count(s, None))-      | "for" => fortran(line_count(s, None))-      | "f90" => fortran(line_count(s, None))-      | "f95" => fortran(line_count(s, None))-      | "swift" => swift(line_count(s, None))-      | "csharp" => csharp(line_count(s, None))-      | "nim" => nim(line_count(s, None))-      | "el" => elisp(line_count(s, None))-      | "txt" => plaintext(line_count(s, None))-      | "ll" => llvm(line_count(s, None))-      | "in" => autoconf(line_count(s, Some("#")))-      | "bat" => batch(line_count(s, None))-      | "ps1" => powershell(line_count(s, None))-      | "ac" => m4(line_count(s, None))-      | "mm" => objective_c(line_count(s, Some("//")))-      | "am" => automake(line_count(s, Some("#")))-      | "mgt" => margaret(line_count(s, Some("--")))-      | "" => match_filename(s)-      | "sh" => match_filename(s)-      | "yamllint" => match_filename(s)-      | _ => unknown-  end--// filter out directories containing artifacts-fun bad_dir(s : string, excludes : List0(string)) : bool =-  case+ s of-    | "." => true-    | ".." => true-    | ".pijul" => true-    | "_darcs" => true-    | ".hg" => true-    | ".git" => true-    | "target" => true-    | ".egg-info" => true-    | "nimcache" => true-    | ".shake" => true-    | "dist-newstyle" => true-    | "dist" => true-    | ".psc-package" => true-    | ".pulp-cache" => true-    | "output" => true-    | "bower_components" => true-    | "elm-stuff" => true-    | ".stack-work" => true-    | ".reco" => true-    | ".reco-work" => true-    | ".cabal-sandbox" => true-    | "node_modules" => true-    | ".lein-plugins" => true-    | ".sass-cache" => true-    | _ => list_exists_cloref(excludes, lam x => x = s || x = s + "/")--fnx step_stream( acc : source_contents-               , full_name : string-               , file_proper : string-               , excludes : List0(string)-               ) : source_contents =-  if test_file_isdir(full_name) != 0 then-    flow_stream(full_name, acc, excludes)-  else-    adjust_contents(acc, prune_extension(full_name, file_proper))-and flow_stream( s : string-               , init : source_contents-               , excludes : List0(string)-               ) : source_contents =-  let-    var files = streamize_dirname_fname(s)-    var ffiles = stream_vt_filter_cloptr(files, lam x => not(bad_dir( x-                                                                    , excludes-                                                                    )))-  in-    stream_vt_foldleft_cloptr( ffiles-                             , init-                             , lam (acc, next) =>-                                 step_stream(acc, s + "/" + next, next, excludes)-                             )-  end--fun empty_contents() : source_contents =-  let-    var isc = @{ rust = empty_file()-               , haskell = empty_file()-               , ats = empty_file()-               , python = empty_file()-               , vimscript = empty_file()-               , elm = empty_file()-               , idris = empty_file()-               , madlang = empty_file()-               , tex = empty_file()-               , markdown = empty_file()-               , yaml = empty_file()-               , toml = empty_file()-               , cabal = empty_file()-               , happy = empty_file()-               , alex = empty_file()-               , go = empty_file()-               , html = empty_file()-               , css = empty_file()-               , verilog = empty_file()-               , vhdl = empty_file()-               , c = empty_file()-               , purescript = empty_file()-               , futhark = empty_file()-               , brainfuck = empty_file()-               , ruby = empty_file()-               , julia = empty_file()-               , perl = empty_file()-               , ocaml = empty_file()-               , agda = empty_file()-               , cobol = empty_file()-               , tcl = empty_file()-               , r = empty_file()-               , lua = empty_file()-               , cpp = empty_file()-               , lalrpop = empty_file()-               , header = empty_file()-               , sixten = empty_file()-               , dhall = empty_file()-               , ipkg = empty_file()-               , makefile = empty_file()-               , justfile = empty_file()-               , ion = empty_file()-               , bash = empty_file()-               , hamlet = empty_file()-               , cassius = empty_file()-               , lucius = empty_file()-               , julius = empty_file()-               , mercury = empty_file()-               , yacc = empty_file()-               , lex = empty_file()-               , coq = empty_file()-               , jupyter = empty_file()-               , java = empty_file()-               , scala = empty_file()-               , erlang = empty_file()-               , elixir = empty_file()-               , pony = empty_file()-               , clojure = empty_file()-               , cabal_project = empty_file()-               , assembly = empty_file()-               , nix = empty_file()-               , php = empty_file()-               , javascript = empty_file()-               , kotlin = empty_file()-               , fsharp = empty_file()-               , fortran = empty_file()-               , swift = empty_file()-               , csharp = empty_file()-               , nim = empty_file()-               , cpp_header = empty_file()-               , elisp = empty_file()-               , plaintext = empty_file()-               , rakefile = empty_file()-               , llvm = empty_file()-               , autoconf = empty_file()-               , batch = empty_file()-               , powershell = empty_file()-               , m4 = empty_file()-               , objective_c = empty_file()-               , automake = empty_file()-               , margaret = empty_file()-               } : source_contents-  in-    isc-  end--fun map_stream( acc : source_contents-              , includes : List0(string)-              , excludes : List0(string)-              ) : source_contents =-  list_foldleft_cloref( includes-                      , acc-                      , lam (acc, next) =>-                          if test_file_exists(next) || next = "" then-                            step_stream(acc, next, next, excludes)-                          else-                            ( prerr("\33[31mError:\33[0m directory '" + next + "' does not exist\n")-                            ; exit(1)-                            ; acc-                            )-                      )--fun is_flag(s : string) : bool =-  string_is_prefix("-", s)--fun process_excludes(s : string, acc : command_line) : command_line =-  let-    val acc_r = ref<command_line>(acc)-    val () = if is_flag(s) then-      ( println!("Error: flag " + s + " found where a directory name was expected")-      ; exit(0)-      ; ()-      )-    else-      acc_r->excludes := list_cons(s, acc.excludes)-  in-    !acc_r-  end--fun process(s : string, acc : command_line, is_first : bool) :-  command_line =-  let-    val acc_r = ref<command_line>(acc)-    val () = if is_flag(s) then-      case+ s of-        | "--help" => acc_r->help := true-        | "-h" => acc_r->help := true-        | "--no-table" => if not(acc.no_table) then-          acc_r->no_table := true-        else-          ( println!("\33[31mError:\33[0m flag " + s + " cannot appear twice")-          ; exit(0)-          ; ()-          )-        | "-t" => if not(acc.no_table) then-          acc_r->no_table := true-        else-          ( println!("\33[31mError:\33[0m flag " + s + " cannot appear twice")-          ; exit(0)-          ; ()-          )-        | "--parallel" => acc_r->parallel := true-        | "-p" => acc_r->parallel := true-        | "--version" => acc_r->version := true-        | "-V" => acc_r->version := true-        | "-e" => ( println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument")-                  ; exit(0)-                  ; ()-                  )-        | "--exclude" => ( println!("\33[31mError:\33[0m flag " + s + " must be followed by an argument")-                         ; exit(0)-                         ; ()-                         )-        | _ => ( println!("\33[31mError:\33[0m flag '" + s + "' not recognized")-               ; exit(0)-               ; ()-               )-    else-      if not(is_first) then-        acc_r->includes := list_cons(s, acc.includes)-      else-        ()-  in-    !acc_r-  end--fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n-m>.-( argc : int(n)-, argv : !argv(n)-, current : int(m)-, prev_is_exclude : bool-, acc : command_line-) : command_line =-  let-    var arg = argv[current]-  in-    if current < argc - 1 then-      if arg != "--exclude" && arg != "-e" then-        let-          val c = get_cli(argc, argv, current + 1, false, acc)-        in-          if prev_is_exclude && current != 0 then-            process_excludes(arg, c)-          else-            if current != 0 then-              process(arg, c, current = 0)-            else-              c-        end-      else-        let-          val c = get_cli(argc, argv, current + 1, true, acc)-        in-          c-        end-    else-      if prev_is_exclude then-        process_excludes(arg, acc)-      else-        process(arg, acc, current = 0)-  end--fun version() : void =-  println!("polygot version 0.3.11\nCopyright (c) 2017 Vanessa McHale")--fun help() : void =-  print("polyglot - Count lines of code quickly.--\33[36mUSAGE:\33[0m poly [DIRECTORY] ... [OPTION] ...--\33[36mFLAGS:\33[0m-    -V, --version            show version information-    -h, --help               display this help and exit-    -e, --exclude            exclude a directory-    -p, --parallel           execute in parallel-    -t, --no-table           display results in alternate format--When no directory is provided poly will execute in the-current directory.--Bug reports and updates: nest.pijul.com/vamchale/polyglot\n")--fun head(xs : List0(string)) : string =-  case+ xs of-    | list_cons (x, xs) => x + ", " + head(xs)-    | list_nil() => ""--// TODO channel to draw work? e.g. take a channel of strings, return a channel of source_contents-fun work( excludes : List0(string)-        , send : channel(List0(string))-        , chan : channel(source_contents)-        ) : void =-  {-    val- (n) = channel_remove(send)-    var x = map_stream(empty_contents(), n, excludes)-    val () = channel_insert(chan, x)-    val- ~None_vt() = channel_unref(chan)-    val- () = case channel_unref<List0(string)>(send) of-      | ~None_vt() => ()-      | ~Some_vt (snd) => queue_free<List0(string)>(snd)-  }--// Function returning the number of CPU cores.-extern-fun ncpu() : int--%{^-#include <unistd.h>-int ncpu() {-  return sysconf(_SC_NPROCESSORS_ONLN);-}-%}--#define NCPU 4--fun apportion(includes : List0(string)) :-  (List0(string), List0(string)) =-  let-    var n = length(includes) / 2-    val (p, q) = list_split_at(includes, n)-  in-    (list_vt2t(p), q)-  end--// TODO maybe make a parallel fold?-fun threads(includes : List0(string), excludes : List0(string)) :-  source_contents =-  let-    val chan = channel_make<source_contents>(2)-    val chan2 = channel_ref(chan)-    val chan3 = channel_ref(chan)-    val send1 = channel_make<List0(string)>(1)-    val send2 = channel_make<List0(string)>(1)-    val send_r1 = channel_ref(send1)-    val send_r2 = channel_ref(send2)-    var new_includes = if length(includes) > 0 then-      includes-    else-      list_cons(".", list_nil())-    val (fst, snd) = apportion(new_includes)-    val _ = channel_insert(send1, fst)-    val _ = channel_insert(send2, snd)-    val t2 = athread_create_cloptr_exn(llam () =>-        work(excludes, send_r1, chan2))-    val t3 = athread_create_cloptr_exn(llam () =>-        work(excludes, send_r2, chan3))-    val- ~None_vt() = channel_unref(send1)-    val- ~None_vt() = channel_unref(send2)-    val- (n) = channel_remove(chan)-    val- (m) = channel_remove(chan)-    val () = ignoret(usleep(1u))-    val () = while(channel_refcount(chan) >= 2)()-    val r = add_contents(n, m)-    val- ~Some_vt (que) = channel_unref<source_contents>(chan)-    val () = queue_free<source_contents>(que)-  in-    r-  end--implement main0 (argc, argv) =-  let-    val cli = @{ version = false-               , help = false-               , no_table = false-               , parallel = false-               , excludes = list_nil()-               , includes = list_nil()-               } : command_line-    val parsed = get_cli(argc, argv, 0, false, cli)-  in-    if parsed.help then-      (help() ; exit(0))-    else-      if parsed.version then-        (version() ; exit(0))-      else-        let-          val result = if parsed.parallel then-            threads(parsed.includes, parsed.excludes)-          else-            if length(parsed.includes) > 0 then-              map_stream(empty_contents(), parsed.includes, parsed.excludes)-            else-              map_stream( empty_contents()-                        , list_cons(".", list_nil())-                        , parsed.excludes-                        )-        in-          if parsed.no_table then-            print(make_output(result))-          else-            print(make_table(result))-        end-  end

@@ -1,244 +0,0 @@-#include "share/atspre_staload.hats"-#include "share/HATS/atslib_staload_libats_libc.hats"--staload UN = "prelude/SATS/unsafe.sats"-staload "src/types.sats"-staload "prelude/basics_sta.sats"-staload "libats/libc/SATS/stdio.sats"-staload "prelude/SATS/string.sats"--fun snoc(s : string, c : char) : string =-  let-    val sc = char2string(c)-    val x = string0_append(s, sc)-  in-    strptr2string(x)-  end--fun next {m : nat} (x : string(m)) : Option_vt(char) =-  if length(x) > 0 then-    Some_vt(string_head(x))-  else-    None_vt--fun stop_plain_string(c : char) : bool =-  case+ c of-    | '\n' => true-    | '#' => true-    | _ => false--fun map {a : vtype}{b : vtype} (f : a -<lincloptr1> b, x : parser(a)) : parser(b) =-  let-    val g = x.modify-  in-    @{ modify = llam c =<lincloptr1> -      begin-        let-          val (y, z): (cstream, a) = g(c)-          val w: b = f(z)-        in-          (cloptr_free($UN.castvwtp0(f)) ; cloptr_free($UN.castvwtp0(g)) ; (y, w))-        end-      end }-  end--extern-fun bind {a : vtype}{b : vtype} (x : parser(a), f : a -<lincloptr1> parser(b)) : parser(b)--fun pure {a : vtype} (x : a) : parser(a) =-  @{ modify = llam c =<lincloptr1> (c, x) }--fun chain {a : vtype}{b : vtype} (x : parser(a), y : parser(b)) : parser(b) =-  @{ modify = llam c =<lincloptr1> let-    val f = x.modify-    val g = y.modify-    val (pre_res, _) = f(c)-    val (res, y) = g(pre_res)-    val _ = cloptr_free($UN.castvwtp0(f))-    val _ = cloptr_free($UN.castvwtp0(g))-  in-    (res, y)-  end }--fun run_parser {a : vtype} (in_stream : cstream, parser : parser(a)) : a =-  let-    val g = parser.modify-    val (s, z) = g(in_stream)-    val _ = stream_vt_free(s)-    val _ = cloptr_free($UN.castvwtp0(g))-  in-    z-  end--fun consume_space() : parser(null) =-  pre_consume_space() where-  { fun pre_consume_space() : parser(null) =-      let-        fnx loop(input : cstream) : (cstream, null) =-          case+ !input of-            | ~stream_vt_cons (' ', xs) => loop(xs)-            | ~stream_vt_cons (_, xs) => (xs, null)-            | ~stream_vt_nil() => ($ldelay(stream_vt_nil), null)-      in-        @{ modify = llam (input) =<lincloptr1> loop(input) }-      end }--fun consume_int() : parser(token) =-  pre_consume_int() where-  { fun pre_consume_int() : parser(token) =-      let-        fun loop(input : cstream, data : int) : (cstream, int) =-          case+ !input of-            | ~stream_vt_cons ('0', xs) => loop(xs, 10 * data)-            | ~stream_vt_cons ('1', xs) => loop(xs, 10 * data + 1)-            | ~stream_vt_cons ('2', xs) => loop(xs, 10 * data + 2)-            | ~stream_vt_cons ('3', xs) => loop(xs, 10 * data + 3)-            | ~stream_vt_cons ('4', xs) => loop(xs, 10 * data + 4)-            | ~stream_vt_cons ('5', xs) => loop(xs, 10 * data + 5)-            | ~stream_vt_cons ('6', xs) => loop(xs, 10 * data + 6)-            | ~stream_vt_cons ('7', xs) => loop(xs, 10 * data + 7)-            | ~stream_vt_cons ('8', xs) => loop(xs, 10 * data + 8)-            | ~stream_vt_cons ('9', xs) => loop(xs, 10 * data + 9)-            | ~stream_vt_cons (_, xs) => (xs, data)-            | ~stream_vt_nil() => ($ldelay(stream_vt_nil), data)-        -        fun data(input : cstream) : (cstream, token) =-          let-            val (x, y) = loop(input, 0)-          in-            (x, int_tok(y))-          end-      in-        @{ modify = llam (input) =<lincloptr1> data(input) }-      end }--fun is_letter(c : char) : bool =-  case+ c of-    | 'a' => true-    | 'b' => true-    | 'c' => true-    | 'd' => true-    | 'e' => true-    | 'f' => true-    | 'g' => true-    | 'h' => true-    | 'i' => true-    | 'j' => true-    | 'k' => true-    | 'l' => true-    | 'm' => true-    | 'n' => true-    | 'o' => true-    | 'p' => true-    | 'q' => true-    | 'r' => true-    | 's' => true-    | 't' => true-    | 'u' => true-    | 'v' => true-    | 'w' => true-    | 'x' => true-    | 'y' => true-    | 'z' => true-    | '-' => true-    | _ => false--fun free_tok(t : token) : void =-  case+ t of-    | ~string_tok (_) => ()-    | ~int_tok (_) => ()-    | ~eq_tok() => ()-    | ~pound_tok() => ()-    | ~float_tok (_) => ()-    | ~bool_tok (_) => ()--fun mk_eq(s : string) : token =-  eq_tok()--// TODO consider list_vt(char)? what would that accomplish/help-// FIXME this is stupid as hell.-fun consume_eq() : parser(token) =-  map(llam x =<lincloptr1> mk_eq(x), pre_consume_identifier()) where-  { fun pre_consume_identifier() : parser(string) =-      let-        fun loop(input : cstream, data : string) : (cstream, string) =-          case+ !input of-            | ~stream_vt_cons ('=', xs) => loop(xs, snoc(data, '='))-            | ~stream_vt_cons (_, xs) => (xs, data)-            | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")-        -        fun data(input : cstream) : (cstream, string) =-          loop(input, "")-      in-        @{ modify = llam (input) =<lincloptr1> data(input) }-      end }--fun consume_identifier() : parser(token) =-  map(llam x =<lincloptr1> string_tok(x), pre_consume_identifier()) where-  { fun pre_consume_identifier() : parser(string) =-      let-        fun loop(input : cstream, data : string) : (cstream, string) =-          case+ !input of-            | ~stream_vt_cons (c, xs) when is_letter(c) => loop(xs, snoc(data, c))-            | ~stream_vt_cons (_, xs) => (xs, data)-            | ~stream_vt_nil() => ($ldelay(stream_vt_nil), "")-        -        fun data(input : cstream) : (cstream, string) =-          loop(input, "")-      in-        @{ modify = llam (input) =<lincloptr1> data(input) }-      end }--fun consume_quoted() : parser(token) =-  map(llam x =<lincloptr1> string_tok(x), pre_consume_quoted()) where-  { fun pre_consume_quoted() : parser(string) =-      let-        fun loop(input : cstream, is_escaped : bool, data : string) : (cstream, string) =-          case+ !input of-            | ~stream_vt_cons ('\\', xs) => loop(xs, true, data)-            | ~stream_vt_cons (x, xs) => -              begin-                if not(is_escaped) then-                  if x = '"' then-                    (xs, data)-                  else-                    loop(xs, false, snoc(data, x))-                else-                  loop(xs, false, snoc(data, x))-              end-            | ~stream_vt_nil() => (prerr!("Error: missing \"") ; exit(1) ; ($ldelay(stream_vt_nil), ""))-        -        fun data(input : cstream) : (cstream, string) =-          loop(input, false, "")-      in-        @{ modify = llam (input) =<lincloptr1> data(input) }-      end }--fun tokenize(input : cstream) : tstream =-  case+ !input of-    | ~stream_vt_cons (x, xs) => (stream_vt_free(xs) ; $ldelay(stream_vt_nil()))-    | ~stream_vt_nil() => $ldelay(stream_vt_nil())--fun display_token(t : token) : void =-  case+ t of-    | ~string_tok (s) => println!(s)-    | ~int_tok (i) => println!(tostring_int(i))-    | ~eq_tok() => println!("=")-    | ~pound_tok() => println!("#")-    | ~float_tok (x) => ()-    | ~bool_tok (b) => ()--implement main0 () =-  let-    var fr = fileref_open_exn("junk1", file_mode_r)-    var stream = streamize_fileref_char(fr)-    val t1: token = run_parser(stream, consume_quoted())-    var fr = fileref_open_exn("junk2", file_mode_r)-    var stream = streamize_fileref_char(fr)-    val t2: token = run_parser(stream, consume_int())-    var fr = fileref_open_exn("junk3", file_mode_r)-    var stream = streamize_fileref_char(fr)-    val t3: token = run_parser(stream, chain(consume_identifier(), chain(consume_eq(), consume_int())))-  in-    (display_token(t1) ; display_token(t2) ; display_token(t3))-  end