summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorvmchale <>2018-01-13 00:47:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-01-13 00:47:00 (GMT)
commit8680c57fe75b4c2085453bb73f4c495ad8d2156f (patch)
tree95d21dde3ccabbed20e5bb55e9a26343ab564d68
parentbe1700ad9567da93ca8ef1825ad444e8cf663ccf (diff)
version 0.1.0.270.1.0.27
-rw-r--r--.travis.yml2
-rw-r--r--README.md4
-rw-r--r--ats-format.cabal5
-rw-r--r--src/Language/ATS/Exec.hs1
-rw-r--r--src/Language/ATS/Lexer.x24
-rw-r--r--src/Language/ATS/Parser.y39
-rw-r--r--src/Language/ATS/PrettyPrint.hs34
-rw-r--r--src/Language/ATS/Types.hs3
-rw-r--r--stack.yaml4
-rw-r--r--test/data/combinatorics.out4
-rw-r--r--test/data/left-pad.out2
-rw-r--r--test/data/number-theory.out4
-rw-r--r--test/data/polyglot.out26
-rw-r--r--test/data/toml-parse.out8
14 files changed, 84 insertions, 76 deletions
diff --git a/.travis.yml b/.travis.yml
index f4e4fa6..4e4d3a8 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -42,7 +42,7 @@ before_install:
fi
install:
- - stack --no-terminal --install-ghc test --only-dependencies
+ - stack --no-terminal --install-ghc build --test --bench --no-run-tests --no-run-benchmarks --only-dependencies
script:
- stack --no-terminal build --haddock --no-haddock-deps --test --bench --no-run-tests --no-run-benchmarks
diff --git a/README.md b/README.md
index a8fd8a4..9578d57 100644
--- a/README.md
+++ b/README.md
@@ -6,8 +6,8 @@
<img alt="Screenshot of sample results" src=https://github.com/vmchale/ats-format/raw/master/atsfmt2.png>
This is a code formatter for [ATS](http://www.ats-lang.org/). It is
-a work-in-progress, but it can handle a subset of the language already.
-Currently it is only tested with ATS 0.3.8.
+a work-in-progress, but it can handle a subset of the language already. The main
+remaining obstacle is formatting for comments.
If you find something that's not listed in `TODO.md` feel free to open
an issue. Code samples that were formatted into something ugly are also welcome.
diff --git a/ats-format.cabal b/ats-format.cabal
index 886d2f6..33fd7db 100644
--- a/ats-format.cabal
+++ b/ats-format.cabal
@@ -1,5 +1,5 @@
name: ats-format
-version: 0.1.0.26
+version: 0.1.0.27
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
@@ -54,8 +54,7 @@ library
, optparse-applicative
, ansi-terminal
, composition-prelude >= 0.1.1.2
- , htoml-megaparsec
- , megaparsec
+ , htoml-megaparsec >= 1.1.0.0
, unordered-containers
, text
, directory
diff --git a/src/Language/ATS/Exec.hs b/src/Language/ATS/Exec.hs
index 2fda5e0..c0ebb56 100644
--- a/src/Language/ATS/Exec.hs
+++ b/src/Language/ATS/Exec.hs
@@ -20,7 +20,6 @@ import Paths_ats_format
import System.Directory (doesFileExist)
import System.Exit (exitFailure)
import System.IO (hPutStr, stderr)
-import Text.Megaparsec (parseErrorPretty)
import Text.PrettyPrint.ANSI.Leijen (pretty)
import Text.Toml
import Text.Toml.Types hiding (Parser)
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
index 91d7e28..debf33d 100644
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -426,28 +426,28 @@ instance Pretty Keyword where
pretty (KwListLit s) = "list" <> string s
instance Pretty Token where
- pretty (Identifier _ s) = string s
- pretty (IdentifierSpace _ s) = string s
+ pretty (Identifier _ s) = text s
+ pretty (IdentifierSpace _ s) = text s
pretty (Keyword _ kw) = pretty kw
- pretty (BoolTok _ b) = string $ over _head toLower (show b)
+ pretty (BoolTok _ b) = text $ over _head toLower (show b)
pretty (IntTok _ i) = pretty i
pretty (FloatTok _ x) = pretty x
pretty (CharTok _ c) = squotes (pretty c)
- pretty (StringTok _ s) = dquotes (string s)
- pretty (Special _ s) = string s
+ pretty (StringTok _ s) = dquotes (text s)
+ pretty (Special _ s) = text s
pretty CBlockLex{} = "%{"
- pretty (Arrow _ s) = string s
- pretty (CommentLex _ s) = string $ take 2 s
- pretty (FuncType _ s) = string s
- pretty (TimeTok _ s) = string s
- pretty (SignatureTok _ s) = string s
- pretty (Operator _ s) = string s
+ pretty (Arrow _ s) = text s
+ pretty (CommentLex _ s) = text $ take 2 s
+ pretty (FuncType _ s) = text s
+ pretty (TimeTok _ s) = text s
+ pretty (SignatureTok _ s) = ":" <> text s
+ pretty (Operator _ s) = text s
pretty (MacroBlock _ s) = "#"
pretty DoubleParenTok{} = "()"
pretty DoubleBracesTok{} = "{}"
pretty DoubleBracketTok{} = "<>"
pretty SpecialBracket{} = "<"
- pretty (FixityTok _ s) = string s
+ pretty (FixityTok _ s) = text s
to_string (CommentLex _ s) = s
to_string (Identifier _ s) = s
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
index 5f3bf63..18c7231 100644
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -118,6 +118,7 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
identifierSpace { $$@IdentifierSpace{} }
closeParen { Special $$ ")" }
openParen { Special $$ "(" }
+ colon { SignatureTok $$ "" }
signature { SignatureTok _ $$ }
comma { Special $$ "," }
percent { Operator $$ "%" }
@@ -255,7 +256,7 @@ Args : Arg { [$1] }
| Arg vbar Arg { [ PrfArg $1 $3 ] }
Arg : identifier { Arg (First $ to_string $1) }
- | identifier signature Type { Arg (Both (to_string $1) $3) }
+ | identifier colon Type { Arg (Both (to_string $1) $3) }
| underscore { Arg (First "_") }
| Type { Arg (Second $1) }
| Expression { Arg (Second (ConcreteType $1)) }
@@ -328,7 +329,7 @@ Expression : PreExpression { $1 }
| Expression semicolon Expression { Precede $1 $3 }
| Expression semicolon { $1 }
| openParen Expression closeParen { $2 }
- | Expression signature Type { TypeSignature $1 $3 }
+ | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?
| openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }
| list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }
| list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 }
@@ -390,7 +391,7 @@ PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqua
| viewAt PreExpression { ViewAt $1 $2 }
| PreExpression at PreExpression { AtExpr $1 $3 }
| atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }
- | atbrace RecordVal rbrace signature Type { RecordValue $1 $2 (Just $5) }
+ | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }
| exclamation PreExpression { Deref $1 $2 }
| PreExpression mutateArrow identifierSpace mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }
| PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }
@@ -423,7 +424,7 @@ Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 Nothin
| lsqbracket Args rsqbracket { Existential $2 Nothing Nothing }
| openExistential Args rsqbracket { Existential $2 Nothing Nothing }
| openExistential Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) }
- | lsqbracket Args signature Type rsqbracket { Existential $2 (Just $4) Nothing } -- FIXME arguments should include more than just ':'
+ | lsqbracket Args colon Type rsqbracket { Existential $2 (Just $4) Nothing } -- FIXME arguments should include more than just ':'
| lsqbracket Expression rsqbracket { Existential [] Nothing (Just $2) }
-- | Parse a universal quantifier on a type
@@ -532,13 +533,16 @@ DataPropLeaves : DataPropLeaf { [$1] }
| prfTransform {% Left $ Expected $1 "Constructor" ">>" }
| maybeProof {% Left $ Expected $1 "Constructor" "?" }
+Signature : signature { $1 }
+ | colon { "" }
+
-- | Parse a type signature and optional function body
-PreFunction : FunName openParen FullArgs closeParen signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
- | FunName Universals OptTermetric signature Type OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
- | FunName Universals OptTermetric doubleParens signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
- | FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
- | Universals FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
- | Universals FunName Universals OptTermetric signature Type OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }
+PreFunction : FunName openParen FullArgs closeParen Signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
+ | FunName Universals OptTermetric Signature Type OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
+ | FunName Universals OptTermetric doubleParens Signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
+ | FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
+ | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
+ | 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" }
@@ -627,14 +631,14 @@ Declaration : include string { Include $2 }
| staload string { Staload Nothing $2 }
| staload IdentifierOr eq string { Staload (Just $2) $4 }
| 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 (get_addendum $1) (Just $4) $2 $6 }
+ | var Pattern colon Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general.
+ | var Pattern colon Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }
+ | val Pattern colon Type eq PreExpression { Val (get_addendum $1) (Just $4) $2 $6 }
| val Pattern eq Expression { Val (get_addendum $1) Nothing $2 $4 }
| var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }
- | var Pattern 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 }
- | var Pattern eq lambdaAt openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (PreF (Unnamed $4) $8 [] [] $6 $9 Nothing (Just $11))) Nothing }
+ | var Pattern colon 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 }
+ | var Pattern eq lambdaAt openParen Args closeParen Signature Type plainArrow Expression { Var Nothing $2 (Just $ LambdaAt (PreF (Unnamed $4) $8 [] [] $6 $9 Nothing (Just $11))) Nothing }
| prval Pattern eq PreExpression { PrVal $2 $4 }
| praxi PreFunction { Func $1 (Praxi $2) }
| primplmnt Implementation { ProofImpl $2 }
@@ -646,9 +650,10 @@ Declaration : include string { Include $2 }
| tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }
| TypeDecl { $1 }
| symintr Name { SymIntr $1 $2 }
- | stacst IdentifierOr signature Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
+ | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
| propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
| Fixity intLit Operators { FixityDecl $1 (Just $2) $3 }
+ | val lbrace Universals rbrace IdentifierOr colon Type { StaVal $3 $5 $7 }
| 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
index 8a96c87..352a6e6 100644
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -432,21 +432,25 @@ prettyArgs = prettyArgs' ", " "(" ")"
fancyU :: [Universal] -> Doc
fancyU = foldMap pretty . reverse
+(<#>) :: Doc -> Doc -> Doc
+(<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b)
+
+-- FIXME figure out a nicer algorithm for when/how to split lines.
instance Pretty PreFunction where
- pretty (PreF i si [] [] [NoArgs] rt Nothing (Just e)) = pretty i <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
- pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si [] us [NoArgs] rt Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si </> pretty rt <+> "=" <$> indent 2 (pretty e)
- pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si </> pretty rt
- pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si </> pretty rt
- pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si </> pretty rt
- pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si </> pretty rt
+ pretty (PreF i si [] [] [NoArgs] rt Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
+ pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si [] us [NoArgs] rt Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si pus us as rt (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si pus us as rt Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us <#> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+ pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt
+ pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
+ pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us <#> prettyArgs as <+> ":" <> text si <#> pretty rt
+ pretty (PreF i si pus us as rt Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
pretty _ = undefined
instance Pretty DataPropLeaf where
@@ -454,7 +458,7 @@ instance Pretty DataPropLeaf where
pretty (DataPropLeaf us e (Just e')) = "|" <+> foldMap pretty (reverse us) <+> pretty e <+> "of" <+> pretty e'
typeHelper :: [(String, Type)] -> Doc
-typeHelper rs = lineAlt ("=" <$> indent 2 (prettyRecord rs)) ("=" <+> prettyRecord rs)
+typeHelper = ("=" <#>) . prettyRecord
instance Pretty Declaration where
pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
index 00b71b0..b039daa 100644
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -69,7 +69,8 @@ data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constr
data Declaration = Func AlexPosn Function
| Impl [Arg] Implementation
| ProofImpl Implementation -- primplmnt -- TODO add args
- | Val Addendum (Maybe Type) Pattern Expression -- TODO expression should be optional?
+ | Val Addendum (Maybe Type) Pattern Expression
+ | StaVal [Universal] String Type
| PrVal Pattern Expression
| Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression) -- TODO AlexPosn
| AndDecl (Maybe Type) Pattern Expression
diff --git a/stack.yaml b/stack.yaml
index b51032d..0462526 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,10 +1,10 @@
---
-resolver: lts-10.2
+resolver: lts-10.3
packages:
- '.'
extra-deps:
- ansi-wl-pprint-0.6.8.1
- - htoml-megaparsec-1.0.1.12
+ - htoml-megaparsec-1.1.0.1
- composition-prelude-0.1.1.4
- dirstream-1.0.3
- hspec-dirstream-0.1.0.1
diff --git a/test/data/combinatorics.out b/test/data/combinatorics.out
index 7495e55..ba4d126 100644
--- a/test/data/combinatorics.out
+++ b/test/data/combinatorics.out
@@ -28,10 +28,10 @@ fn permutatsions {n : nat}{ k : nat | k <= n } ( n : int(n)
// 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 =
+ Intinf =
let
fun numerator_loop { m : nat | m > 1 } .<m>. (i : int(m)) :
- [ n : nat | n > 0 ] intinf(n) =
+ [ n : nat | n > 0 ] intinf(n) =
case+ i of
| 1 => int2intinf(n)
| 2 => $UN.cast(int2intinf(n - 1) * n)
diff --git a/test/data/left-pad.out b/test/data/left-pad.out
index 124d538..2635298 100644
--- a/test/data/left-pad.out
+++ b/test/data/left-pad.out
@@ -12,7 +12,7 @@ fun left_pad { p, l : nat | p > 0 && l > 0 } ( pad : ssize_t(p)
extern
fun {t : t@ype} fill_list {n : nat} (size : ssize_t(n), c : t) :
-list_vt(t, n)
+ list_vt(t, n)
implement {t} fill_list {n} (size, c) =
let
diff --git a/test/data/number-theory.out b/test/data/number-theory.out
index ae32696..b3f02af 100644
--- a/test/data/number-theory.out
+++ b/test/data/number-theory.out
@@ -74,7 +74,7 @@ dataprop FACT(int, int) =
+ 1, r1, r))
fun get_multiplicity { p : nat | p > 1 } (n : intGte(0), p : int(p)) :
-int =
+ int =
case+ n % p of
| 0 => 1 + get_multiplicity(witness(n / p), p)
| _ => 0
@@ -142,7 +142,7 @@ fn totient(n : intGte(1)) : int =
begin
let
fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>.
- (i : int(m), n : int(k)) : int =
+ (i : int(m), n : int(k)) : int =
if i >= n then
if is_prime(n) then
n - 1
diff --git a/test/data/polyglot.out b/test/data/polyglot.out
index 73d2928..d33f0a4 100644
--- a/test/data/polyglot.out
+++ b/test/data/polyglot.out
@@ -92,14 +92,14 @@ fun line_count(s : string, pre : Option(string)) : file =
// Pad a string of bounded length on the right by adding spaces.
fnx right_pad { k : int | k >= 0 }{ m : int | m <= k } .<k>.
-(s : string(m), n : int(k)) : string =
+ (s : string(m), n : int(k)) : string =
case+ length(s) < n of
| true when n > 0 => right_pad(s, n - 1) + " "
| _ => s
// Pad a string on the left by adding spaces.
fnx left_pad { k : int | k >= 0 } .<k>. (s : string, n : int(k)) :
-string =
+ string =
case+ length(s) < n of
| true when n > 0 => " " + left_pad(s, n - 1)
| _ => s
@@ -422,7 +422,7 @@ fun make_output(isc : source_contents) : string =
)
fun add_contents(x : source_contents, y : source_contents) :
-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
@@ -470,7 +470,7 @@ source_contents =
// This is the step function used when streaming directory contents.
fun adjust_contents(prev : source_contents, scf : pl_type) :
-source_contents =
+ source_contents =
let
val sc_r = ref<source_contents>(prev)
val _ = case+ scf of
@@ -1127,7 +1127,7 @@ fun process_excludes(s : string, acc : command_line) : command_line =
end
fun process(s : string, acc : command_line, is_first : bool) :
-command_line =
+ command_line =
let
val acc_r = ref<command_line>(acc)
val () = if is_flag(s) then
@@ -1164,12 +1164,12 @@ command_line =
end
fnx get_cli { n : int | n >= 1 }{ m : nat | m < n } .<n-m>.
-( argc : int(n)
-, argv : !argv(n)
-, current : int(m)
-, prev_is_exclude : bool
-, acc : command_line
-) : command_line =
+ ( argc : int(n)
+ , argv : !argv(n)
+ , current : int(m)
+ , prev_is_exclude : bool
+ , acc : command_line
+ ) : command_line =
let
var arg = argv[current]
in
@@ -1253,7 +1253,7 @@ int ncpu() {
#define NCPU 4
fun apportion(includes : List0(string)) :
-(List0(string), List0(string)) =
+ (List0(string), List0(string)) =
let
var n = length(includes) / 2
val (p, q) = list_split_at(includes, n)
@@ -1263,7 +1263,7 @@ fun apportion(includes : List0(string)) :
// TODO maybe make a parallel fold?
fun threads(includes : List0(string), excludes : List0(string)) :
-source_contents =
+ source_contents =
let
val chan = channel_make<source_contents>(2)
val chan2 = channel_ref(chan)
diff --git a/test/data/toml-parse.out b/test/data/toml-parse.out
index 12f27f8..f5de24c 100644
--- a/test/data/toml-parse.out
+++ b/test/data/toml-parse.out
@@ -28,7 +28,7 @@ fun stop_plain_string(c : char) : bool =
| _ => false
fun map {a : vtype}{b : vtype} (f : a -<lincloptr1> b, x : parser(a)) :
-parser(b) =
+ parser(b) =
let
val g = x.modify
in
@@ -53,7 +53,7 @@ fun pure {a : vtype} (x : a) : parser(a) =
@{ modify = llam c =<lincloptr1> (c, x) }
fun chain {a : vtype}{b : vtype} (x : parser(a), y : parser(b)) :
-parser(b) =
+ parser(b) =
@{ modify = llam c =<lincloptr1>
let
val f = x.modify
@@ -67,7 +67,7 @@ parser(b) =
end }
fun run_parser {a : vtype} (in_stream : cstream, parser : parser(a)) :
-a =
+ a =
let
val g = parser.modify
val (s, z) = g(in_stream)
@@ -203,7 +203,7 @@ fun consume_quoted() : parser(token) =
{ fun pre_consume_quoted() : parser(string) =
let
fun loop(input : cstream, is_escaped : bool, data : string) :
- (cstream, string) =
+ (cstream, string) =
case+ !input of
| ~stream_vt_cons ('\\', xs) => loop(xs, true, data)
| ~stream_vt_cons (x, xs) =>