ats-format 0.1.0.23 → 0.1.0.24
raw patch · 35 files changed
+4662/−35 lines, 35 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ Language.ATS: FixityDecl :: Fixity -> (Maybe Int) -> [String] -> Declaration
+ Language.ATS: FixityTok :: AlexPosn -> String -> Token
+ Language.ATS: LeftFix :: AlexPosn -> Fixity
+ Language.ATS: Post :: AlexPosn -> Fixity
+ Language.ATS: Pre :: AlexPosn -> Fixity
+ Language.ATS: RightFix :: AlexPosn -> Fixity
+ Language.ATS: data Fixity
- Language.ATS: At :: AlexPosn -> Type -> Type -> Type
+ Language.ATS: At :: AlexPosn -> (Maybe Type) -> Type -> Type
Files
- Justfile +2/−0
- README.md +1/−1
- ats-format.cabal +4/−1
- bench/Bench.hs +1/−1
- src/Language/ATS.hs +1/−0
- src/Language/ATS/Lexer.x +16/−4
- src/Language/ATS/Parser.y +30/−9
- src/Language/ATS/PrettyPrint.hs +24/−14
- src/Language/ATS/Types.hs +10/−5
- test/data/combinatorics.dats +40/−0
- test/data/combinatorics.out +44/−0
- test/data/fact.dats +32/−0
- test/data/fact.out +39/−0
- test/data/factorial.dats +4/−0
- test/data/factorial.out +4/−0
- test/data/fast-combinatorics.dats +93/−0
- test/data/fast-combinatorics.out +95/−0
- test/data/fib.dats +6/−0
- test/data/fib.out +6/−0
- test/data/filecount.dats +31/−0
- test/data/filecount.out +40/−0
- test/data/filetype.out +180/−0
- test/data/filetype.sats +180/−0
- test/data/left-pad.dats +98/−0
- test/data/left-pad.out +76/−0
- test/data/number-theory.dats +167/−0
- test/data/number-theory.out +185/−0
- test/data/numerics.dats +61/−0
- test/data/numerics.out +63/−0
- test/data/polyglot.dats +1235/−0
- test/data/polyglot.out +1344/−0
- test/data/toml-parse.dats +244/−0
- test/data/toml-parse.out +259/−0
- test/data/types.out +24/−0
- test/data/types.sats +23/−0
Justfile view
@@ -41,6 +41,8 @@ ci: test cabal new-build+ cabal new-build -w ghc-8.0.2+ cabal new-build -w ghc-7.10.3 cabal new-haddock cabal new-test hlint src app bench test
README.md view
@@ -40,7 +40,7 @@ ```bash $ cabal update- $ cabal install ats-format+ $ cabal new-install ats-format --happy-options='-gcsa' --alex-options='-g' --symlink-bindir ~/.cabal/bin ``` ## License
ats-format.cabal view
@@ -1,5 +1,5 @@ name: ats-format-version: 0.1.0.23+version: 0.1.0.24 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,6 +14,9 @@ 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
bench/Bench.hs view
@@ -16,5 +16,5 @@ ] ] where large = readFile "test/data/polyglot.dats"- medium = readFile "test/data/filetype.sats"+ medium = readFile "test/data/toml-parse.dats" envFiles = (,) <$> large <*> medium
src/Language/ATS.hs view
@@ -24,6 +24,7 @@ , PreFunction (..) , StaticExpression (..) , Paired (..)+ , Fixity (..) -- * Lexical types , Token (..) , AlexPosn (..)
src/Language/ATS/Lexer.x view
@@ -16,6 +16,7 @@ , lexATS , token_posn , to_string+ , get_addendum ) where import Data.Data (Typeable, Data)@@ -60,7 +61,7 @@ @string = \" ($printable # [\"\\] | @escape_str | $esc_char | \n)* \" -- Identifiers-@identifier = $alpha ($alpha | $digit | _ | ! | ')*+@identifier = ($alpha | _) ($alpha | $digit | _ | ! | ' | \$)* -- Multi-line comments @not_close_paren = (\*+ [^\)] | [^\*] \))@@ -86,7 +87,7 @@ @at_brace = \@ ($white | @block_comment)* \{ -@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "%" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |+@operator = "**" | "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "%" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow @double_parens = "(" @block_comment ")" | "()" @double_braces = "{" @block_comment "}" | "{}"@@ -94,6 +95,8 @@ @view = v | view +@fixity_decl = "infixr" | "infixl" | "prefix" | "postfix"+ tokens :- $white+ ;@@ -197,6 +200,7 @@ "$list_vt" { tok (\p s -> Keyword p (KwListLit "_vt")) } "fold@" { tok (\p s -> Identifier 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) }@@ -205,13 +209,15 @@ @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)) }+ @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) } @identifier / " " { tok (\p s -> IdentifierSpace p s) } @identifier { tok (\p s -> Identifier p s) } @string { tok (\p s -> StringTok p s) }@@ -231,6 +237,9 @@ | Minus deriving (Eq, Show, Generic, NFData, Data, Typeable) +get_addendum (Keyword _ (KwVal a)) = a+get_addendum _ = None+ data Keyword = KwFun | KwFnx | KwAnd@@ -330,6 +339,7 @@ | DoubleBracesTok AlexPosn | DoubleBracketTok AlexPosn | SpecialBracket AlexPosn+ | FixityTok AlexPosn String deriving (Eq, Show, Generic, NFData) instance Pretty Addendum where@@ -436,7 +446,8 @@ pretty DoubleParenTok{} = "()" pretty DoubleBracesTok{} = "{}" pretty DoubleBracketTok{} = "<>"- pretty SpecialBracket{} = "{"+ pretty SpecialBracket{} = "<"+ pretty (FixityTok _ s) = string s to_string (CommentLex _ s) = s to_string _ = mempty@@ -462,6 +473,7 @@ 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'
src/Language/ATS/Parser.y view
@@ -16,6 +16,7 @@ , Addendum (..) , token_posn , to_string+ , get_addendum ) import Data.Char (toLower)@@ -45,7 +46,7 @@ if { Keyword $$ KwIf } sif { Keyword $$ KwSif } stadef { Keyword $$ KwStadef }- val { Keyword _ (KwVal $$) }+ val { $$@(Keyword _ (KwVal _)) } prval { Keyword $$ KwPrval } var { Keyword $$ KwVar } then { Keyword $$ KwThen }@@ -160,6 +161,7 @@ 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?@@ -170,9 +172,14 @@ lineComment { $$@CommentLex{} } lspecial { SpecialBracket $$ } atbrace { Operator $$ "@{" }+ exp { Operator $$ "**" } mod { Keyword $$ KwMod } fixAt { Keyword $$ KwFixAt } lambdaAt { Keyword $$ KwLambdaAt }+ infixr { FixityTok $$ "infixr" }+ infixl { FixityTok $$ "infixr" }+ prefix { FixityTok $$ "prefix" }+ postfix { FixityTok $$ "postfix" } %% @@ -227,7 +234,8 @@ | view { ViewLiteral None } | Existential Type { Ex $1 $2 } | Universal Type { ForA $1 $2 }- | Type at Type { At $2 $1 $3 }+ | Type at Type { At $2 (Just $1) $3 }+ | at Type { At $1 Nothing $2 } | openParen Type vbar Type closeParen { ProofType $1 $2 $4 } | identifierSpace identifier { Dependent (Unqualified $1) [Named (Unqualified $2)] } | openParen TypeIn closeParen { Tuple $1 $2 }@@ -239,10 +247,6 @@ FullArgs : Args { $1 } -FunArgs : Arg { Comma $1 Nil }- | FunArgs comma Arg { Comma $3 $1 }- | FunArgs vbar Arg { Bar $3 $1 }- -- | A comma-separated list of arguments Args : Arg { [$1] } | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 }@@ -518,6 +522,7 @@ | 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" "-" }@@ -535,6 +540,7 @@ | Universals FunName Universals OptTermetric signature Type 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" "[" }@@ -559,6 +565,8 @@ | 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" } IdentifierOr : identifier { $1 } | identifierSpace { $1 }@@ -594,11 +602,23 @@ | 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 { $1 }+ | exp { "**" }++Operators : Operator { [$1] }+ | Operators Operator { $2 : $1 }+ | Operators identifier { $2 : $1 }+ -- | Parse a declaration Declaration : include string { Include $2 } | define { Define $1 } | define identifierSpace string { Define ($1 ++ $2 ++ $3) } -- FIXME better approach?- | define identifierSpace int { Define ($1 ++ $2 ++ " " ++ show $3) }+ | define identifierSpace intLit { Define ($1 ++ $2 ++ " " ++ show $3) } | cblock { CBlock $1 } | lineComment { Comment (to_string $1) } | staload underscore eq string { Staload (Just "_") $4 }@@ -607,8 +627,8 @@ | extern Declaration { Extern $1 $2 } | var Pattern signature Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general. | var Pattern signature Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }- | val Pattern signature Type eq PreExpression { Val $1 (Just $4) $2 $6 }- | val Pattern eq Expression { Val $1 Nothing $2 $4 }+ | val Pattern signature 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 signature Type { Var (Just $4) $2 Nothing Nothing } | var Pattern eq fixAt IdentifierOr openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing }@@ -626,6 +646,7 @@ | symintr Name { SymIntr $1 $2 } | stacst IdentifierOr signature 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 } | lambda {% Left $ Expected $1 "Declaration" "lam" } | llambda {% Left $ Expected $1 "Declaration" "llam" } | minus {% Left $ Expected $1 "Declaration" "-" }
src/Language/ATS/PrettyPrint.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -120,7 +121,7 @@ prettyBinary _ [] = mempty prettyBinary _ [e] = e prettyBinary op [e, e'] = e <+> op <+> e'-prettyBinary _ _ = "FIXME"+prettyBinary _ _ = undefined instance Pretty Expression where pretty = cata a . rewriteATS where@@ -160,8 +161,8 @@ a (VoidLiteralF _) = "()" a (RecordValueF _ es Nothing) = prettyRecord es a (RecordValueF _ es (Just x)) = prettyRecord es <+> ":" <+> pretty x- a (PrecedeF e e') = parens (e <+> ";" </> e') -- TODO use plated + write this like arguments with commas- a (PrecedeListF es) = prettyArgsList " ; " "(" ")" es+ 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@@ -175,7 +176,7 @@ 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) = prettyArgs es -- parens (mconcat $ punctuate ", " (reverse es))+ 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{} = "_"@@ -188,7 +189,7 @@ a (AddrAtF _ e) = "addr@" <> e a (ViewAtF _ e) = "view@" <> e a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es- a _ = "FIXME"+ a _ = 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 ...@@ -218,7 +219,7 @@ pretty (Arg (Second t)) = pretty t pretty (Arg (Both s t)) = pretty s <+> colon <+> pretty t pretty (PrfArg a a') = pretty a <+> "|" <+> pretty a'- pretty NoArgs = "FIXME"+ pretty NoArgs = undefined squish :: BinOp -> Bool squish Add = True@@ -264,7 +265,8 @@ a (MaybeValF t) = t <> "?" a (T0pF ad) = "t@ype" <> pretty ad a (Vt0pF ad) = "vt@ype" <> pretty ad- a (AtF _ t t') = t <+> "@" <+> t'+ a (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))))@@ -286,7 +288,7 @@ where go (Arg (First s)) = pretty s go (Arg (Both s t)) = pretty s <+> colon <+> pretty t go (Arg (Second t)) = pretty t- go _ = "FIXME"+ go _ = undefined instance Pretty Universal where pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments@@ -296,7 +298,7 @@ where go (Arg (First s)) = pretty s go (Arg (Both s t)) = pretty s <+> colon <+> pretty t go (Arg (Second t)) = pretty t- go _ = "FIXME"+ go _ = undefined instance Pretty ATS where pretty (ATS xs) = concatSame (fmap rewriteDecl xs)@@ -337,8 +339,11 @@ ($$) :: Doc -> Doc -> Doc x $$ y = align (x <$> y) +lineAlt :: Doc -> Doc -> Doc+lineAlt = group .* flatAlt+ prettyRecord :: (Pretty a) => [(String, a)] -> Doc-prettyRecord es = group (flatAlt (prettyRecordF True es) (prettyRecordS True es))+prettyRecord es = lineAlt (prettyRecordF True es) (prettyRecordS True es) prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc prettyRecordS _ [] = mempty@@ -356,6 +361,10 @@ 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)@@ -389,7 +398,8 @@ prettyHelper _ x = x prettyBody :: Doc -> Doc -> [Doc] -> Doc-prettyBody c1 c2 = (c1 <>) . align . indent (-1) . cat . (<> pure c2)+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@@ -430,14 +440,14 @@ pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> string si </> pretty rt pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si </> pretty rt pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si </> pretty rt- pretty _ = "FIXME"+ 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' typeHelper :: [(String, Type)] -> Doc-typeHelper rs = group (flatAlt ("=" <$> indent 2 (prettyRecord rs)) ("=" <+> prettyRecord rs))+typeHelper rs = lineAlt ("=" <$> indent 2 (prettyRecord rs)) ("=" <+> prettyRecord rs) instance Pretty Declaration where pretty (AbsType _ s as Nothing) = "abstype" <+> string s <> prettyArgs as@@ -486,4 +496,4 @@ 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" </> string s <+> prettyArgs as <+> "=" </> pretty t- pretty _ = "FIXME"+ pretty _ = undefined
src/Language/ATS/Types.hs view
@@ -33,10 +33,10 @@ , DataPropLeaf (..) , PreFunction (..) , Paired (..)- , Bifurcated (..) , Leaf (..) , StaticExpression (..) , StaticExpressionF (..)+ , Fixity (..) , rewriteATS , rewriteDecl -- * Lenses@@ -52,9 +52,11 @@ import GHC.Generics (Generic) import Language.ATS.Lexer (Addendum (..), AlexPosn) -data Bifurcated a = Nil- | Comma a (Bifurcated a)- | Bar a (Bifurcated a)+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] }@@ -102,6 +104,9 @@ | 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)@@ -131,7 +136,7 @@ | MaybeVal Type -- This is just `a?` or the like | T0p Addendum -- t@ype | Vt0p Addendum -- vt@ype- | At AlexPosn Type Type+ | At AlexPosn (Maybe Type) Type | ProofType AlexPosn Type Type -- Aka (prf | val) | ConcreteType Expression | RefType Type
+ test/data/combinatorics.dats view
@@ -0,0 +1,40 @@+#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
+ test/data/combinatorics.out view
@@ -0,0 +1,44 @@+#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
+ test/data/fact.dats view
@@ -0,0 +1,32 @@+#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
+ test/data/fact.out view
@@ -0,0 +1,39 @@+#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
+ test/data/factorial.dats view
@@ -0,0 +1,4 @@+fun factorial_recursion {n:nat} .<n>. (n: int(n)) : int =+case+ n of+| 0 => 1+| n =>> factorial_recursion(n-1) * n
+ test/data/factorial.out view
@@ -0,0 +1,4 @@+fun factorial_recursion {n : nat} .<n>. (n : int(n)) : int =+ case+ n of+ | 0 => 1+ | n =>> factorial_recursion(n - 1) * n
+ test/data/fast-combinatorics.dats view
@@ -0,0 +1,93 @@+#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)
+ test/data/fast-combinatorics.out view
@@ -0,0 +1,95 @@+#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)
+ test/data/fib.dats view
@@ -0,0 +1,6 @@+#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
+ test/data/fib.out view
@@ -0,0 +1,6 @@+#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
+ test/data/filecount.dats view
@@ -0,0 +1,31 @@+#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(".")
+ test/data/filecount.out view
@@ -0,0 +1,40 @@+#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(".")
+ test/data/filetype.out view
@@ -0,0 +1,180 @@+// 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
+ test/data/filetype.sats view
@@ -0,0 +1,180 @@+// 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
+ test/data/left-pad.dats view
@@ -0,0 +1,98 @@+#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
+ test/data/left-pad.out view
@@ -0,0 +1,76 @@+#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
+ test/data/number-theory.dats view
@@ -0,0 +1,167 @@+#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)
+ test/data/number-theory.out view
@@ -0,0 +1,185 @@+#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)
+ test/data/numerics.dats view
@@ -0,0 +1,61 @@+#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
+ test/data/numerics.out view
@@ -0,0 +1,63 @@+#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
+ test/data/polyglot.dats view
@@ -0,0 +1,1235 @@+#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
+ test/data/polyglot.out view
@@ -0,0 +1,1344 @@+#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
+ test/data/toml-parse.dats view
@@ -0,0 +1,244 @@+#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
+ test/data/toml-parse.out view
@@ -0,0 +1,259 @@+#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
+ test/data/types.out view
@@ -0,0 +1,24 @@+datavtype null =+ | null++datavtype token =+ | string_tok of string+ | int_tok of int+ | eq_tok+ | pound_tok+ | float_tok of float+ | bool_tok of bool++datavtype error_state =+ | okay+ | error_state of string++vtypedef cstream = stream_vt(char)+vtypedef tstream = stream_vt(token)++datavtype either(a : t@ype, b : t@ype+) =+ | left of a+ | right of b++vtypedef parser(a : vt@ype+) =+ @{ modify = cstream -<lincloptr1> (cstream, a) }
+ test/data/types.sats view
@@ -0,0 +1,23 @@+datavtype null =+ | null++datavtype token =+ | string_tok of string+ | int_tok of int+ | eq_tok+ | pound_tok+ | float_tok of float+ | bool_tok of bool++datavtype error_state =+ | okay+ | error_state of string++vtypedef cstream = stream_vt(char)+vtypedef tstream = stream_vt(token)++datavtype either(a : t@ype, b : t@ype+) =+ | left of a+ | right of b++vtypedef parser(a : vt@ype+) = @{ modify = cstream -<lincloptr1> (cstream, a) }