diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/ats-format.cabal b/ats-format.cabal --- a/ats-format.cabal +++ b/ats-format.cabal @@ -1,5 +1,5 @@ name: ats-format -version: 0.1.0.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 diff --git a/bench/Bench.hs b/bench/Bench.hs --- a/bench/Bench.hs +++ b/bench/Bench.hs @@ -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 diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs --- a/src/Language/ATS.hs +++ b/src/Language/ATS.hs @@ -24,6 +24,7 @@ , PreFunction (..) , StaticExpression (..) , Paired (..) + , Fixity (..) -- * Lexical types , Token (..) , AlexPosn (..) diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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' diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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" "-" } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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 diff --git a/test/data/combinatorics.dats b/test/data/combinatorics.dats new file mode 100644 --- /dev/null +++ b/test/data/combinatorics.dats @@ -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} .. (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} .. (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 } .. (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 diff --git a/test/data/combinatorics.out b/test/data/combinatorics.out new file mode 100644 --- /dev/null +++ b/test/data/combinatorics.out @@ -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} .. (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} .. (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 } .. (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 diff --git a/test/data/fact.dats b/test/data/fact.dats new file mode 100644 --- /dev/null +++ b/test/data/fact.dats @@ -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} .. *) +(* (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} .. +(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 diff --git a/test/data/fact.out b/test/data/fact.out new file mode 100644 --- /dev/null +++ b/test/data/fact.out @@ -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} .. *) +(* (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} .. ( 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 diff --git a/test/data/factorial.dats b/test/data/factorial.dats new file mode 100644 --- /dev/null +++ b/test/data/factorial.dats @@ -0,0 +1,4 @@ +fun factorial_recursion {n:nat} .. (n: int(n)) : int = +case+ n of +| 0 => 1 +| n =>> factorial_recursion(n-1) * n diff --git a/test/data/factorial.out b/test/data/factorial.out new file mode 100644 --- /dev/null +++ b/test/data/factorial.out @@ -0,0 +1,4 @@ +fun factorial_recursion {n : nat} .. (n : int(n)) : int = + case+ n of + | 0 => 1 + | n =>> factorial_recursion(n - 1) * n diff --git a/test/data/fast-combinatorics.dats b/test/data/fast-combinatorics.dats new file mode 100644 --- /dev/null +++ b/test/data/fast-combinatorics.dats @@ -0,0 +1,93 @@ +#define ATS_MAINATSFLAG 1 + +#include "share/atspre_staload.hats" + +staload "libats/libc/SATS/math.sats" + +fnx fact {n : nat} .. (k : int(n)) :<> int = + case+ k of + | 0 => 1 + | k =>> fact(k - 1) * k + +fnx dfact {n : nat} .. (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 } .. (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} .. (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) diff --git a/test/data/fast-combinatorics.out b/test/data/fast-combinatorics.out new file mode 100644 --- /dev/null +++ b/test/data/fast-combinatorics.out @@ -0,0 +1,95 @@ +#define ATS_MAINATSFLAG 1 + +#include "share/atspre_staload.hats" + +staload "libats/libc/SATS/math.sats" + +fnx fact {n : nat} .. (k : int(n)) :<> int = + case+ k of + | 0 => 1 + | k =>> fact(k - 1) * k + +fnx dfact {n : nat} .. (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 } .. (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} .. ( 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) diff --git a/test/data/fib.dats b/test/data/fib.dats new file mode 100644 --- /dev/null +++ b/test/data/fib.dats @@ -0,0 +1,6 @@ +#include "prelude/DATS/integer.dats" + +fnx fib { n : int | n >= 0 } .. (i : int(n)) : int = +case+ i of +| _ when i - 2 >= 0 => ( fib(i-1) + fib(i-2) ) +| _ => 1 diff --git a/test/data/fib.out b/test/data/fib.out new file mode 100644 --- /dev/null +++ b/test/data/fib.out @@ -0,0 +1,6 @@ +#include "prelude/DATS/integer.dats" + +fnx fib { n : int | n >= 0 } .. (i : int(n)) : int = + case+ i of + | _ when i - 2 >= 0 => (fib(i - 1) + fib(i - 2)) + | _ => 1 diff --git a/test/data/filecount.dats b/test/data/filecount.dats new file mode 100644 --- /dev/null +++ b/test/data/filecount.dats @@ -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(".") diff --git a/test/data/filecount.out b/test/data/filecount.out new file mode 100644 --- /dev/null +++ b/test/data/filecount.out @@ -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(".") diff --git a/test/data/filetype.out b/test/data/filetype.out new file mode 100644 --- /dev/null +++ b/test/data/filetype.out @@ -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 diff --git a/test/data/filetype.sats b/test/data/filetype.sats new file mode 100644 --- /dev/null +++ b/test/data/filetype.sats @@ -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 diff --git a/test/data/left-pad.dats b/test/data/left-pad.dats new file mode 100644 --- /dev/null +++ b/test/data/left-pad.dats @@ -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} + .. + ( + 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 \n" + end + ) + else print "Usage: left-pad \n" + in + list_vt_free(args) + end diff --git a/test/data/left-pad.out b/test/data/left-pad.out new file mode 100644 --- /dev/null +++ b/test/data/left-pad.out @@ -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 } .. ( 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 \n") + end) + else + print("Usage: left-pad \n") + in + list_vt_free(args) + end diff --git a/test/data/number-theory.dats b/test/data/number-theory.dats new file mode 100644 --- /dev/null +++ b/test/data/number-theory.dats @@ -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 } .. (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 } .. (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 } .. (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 } .. (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 } .. (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 } .. (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 } .. (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) diff --git a/test/data/number-theory.out b/test/data/number-theory.out new file mode 100644 --- /dev/null +++ b/test/data/number-theory.out @@ -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 } .. ( 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 } .. ( 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 } .. ( 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 } .. ( 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 } .. ( 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 } .. + (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 } .. ( 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) diff --git a/test/data/numerics.dats b/test/data/numerics.dats new file mode 100644 --- /dev/null +++ b/test/data/numerics.dats @@ -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} .. (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} .. (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 diff --git a/test/data/numerics.out b/test/data/numerics.out new file mode 100644 --- /dev/null +++ b/test/data/numerics.out @@ -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} .. (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} .. ( 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 diff --git a/test/data/polyglot.dats b/test/data/polyglot.dats new file mode 100644 --- /dev/null +++ b/test/data/polyglot.dats @@ -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) = 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 } .. (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 } .. (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(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) = 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(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(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 } .. ( 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(send) of + | ~None_vt() => () + | ~Some_vt (snd) => queue_free(snd) + } + +// Function returning the number of CPU cores. +extern +fun ncpu () : int + +%{^ +#include +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(2) + val chan2 = channel_ref(chan) + val chan3 = channel_ref(chan) + val send1 = channel_make(1) + val send2 = channel_make(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(chan) + val () = queue_free(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 diff --git a/test/data/polyglot.out b/test/data/polyglot.out new file mode 100644 --- /dev/null +++ b/test/data/polyglot.out @@ -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) = 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 } .. +(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 } .. (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(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) = 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(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(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 } .. +( 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(send) of + | ~None_vt() => () + | ~Some_vt (snd) => queue_free(snd) + } + +// Function returning the number of CPU cores. +extern +fun ncpu() : int + +%{^ +#include +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(2) + val chan2 = channel_ref(chan) + val chan3 = channel_ref(chan) + val send1 = channel_make(1) + val send2 = channel_make(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(chan) + val () = queue_free(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 diff --git a/test/data/toml-parse.dats b/test/data/toml-parse.dats new file mode 100644 --- /dev/null +++ b/test/data/toml-parse.dats @@ -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 - b, x : parser(a)) : parser(b) = + let + val g = x.modify + in + @{ modify = llam c = + 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 - parser(b)) : parser(b) + +fun pure {a : vtype} (x : a) : parser(a) = + @{ modify = llam c = (c, x) } + +fun chain {a : vtype}{b : vtype} (x : parser(a), y : parser(b)) : parser(b) = + @{ modify = llam c = 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) = 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) = 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 = 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) = data(input) } + end } + +fun consume_identifier() : parser(token) = + map(llam x = 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) = data(input) } + end } + +fun consume_quoted() : parser(token) = + map(llam x = 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) = 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 diff --git a/test/data/toml-parse.out b/test/data/toml-parse.out new file mode 100644 --- /dev/null +++ b/test/data/toml-parse.out @@ -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 - b, x : parser(a)) : +parser(b) = + let + val g = x.modify + in + @{ modify = llam c = + 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 - parser(b) + ) : parser(b) + +fun pure {a : vtype} (x : a) : parser(a) = + @{ modify = llam c = (c, x) } + +fun chain {a : vtype}{b : vtype} (x : parser(a), y : parser(b)) : +parser(b) = + @{ modify = llam c = 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) = 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) = 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 = 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) = data(input) } + end } + +fun consume_identifier() : parser(token) = + map( llam x = 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) = data(input) } + end } + +fun consume_quoted() : parser(token) = + map(llam x = 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) = 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 diff --git a/test/data/types.out b/test/data/types.out new file mode 100644 --- /dev/null +++ b/test/data/types.out @@ -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 - (cstream, a) } diff --git a/test/data/types.sats b/test/data/types.sats new file mode 100644 --- /dev/null +++ b/test/data/types.sats @@ -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 - (cstream, a) }