diff --git a/Justfile b/Justfile --- a/Justfile +++ b/Justfile @@ -59,6 +59,10 @@ @rm -rf rm .ghc.environment.* polyglot @git clone https://github.com/vmchale/polyglot cd polyglot && atsfmt src/polyglot.dats -i + cd polyglot && atsfmt src/cli.dats -i + cd polyglot && atsfmt src/concurrency.dats -i + cd polyglot && atsfmt src/shared.dats -i + cd polyglot && atsfmt src/filetype.sats -i cd polyglot && ./shake.hs @rm -rf polyglot 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.3.1 +version: 0.1.3.3 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 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 @@ -198,7 +198,7 @@ absview { tok (\p s -> Keyword p KwAbsview) } "$list" { tok (\p s -> Keyword p (KwListLit "")) } "$list_vt" { tok (\p s -> Keyword p (KwListLit "_vt")) } - "fold@" { tok (\p s -> Identifier p s) } + "fold@" { tok (\p s -> IdentifierSpace p s) } "free@" { tok (\p s -> Identifier p s) } @fixity_decl { tok (\p s -> FixityTok p s) } @double_parens { tok (\p s -> DoubleParenTok p) } 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 @@ -191,7 +191,7 @@ Declarations : { [] } | Declarations Declaration { $2 : $1 } | Declarations FunDecl { $2 ++ $1 } - | Declarations local Declarations in Declarations end { Local $2 $3 $5 : $1 } + | Declarations local ATS in ATS end { Local $2 $3 $5 : $1 } -- | Several comma-separated types TypeIn : Type { [$1] } @@ -199,9 +199,9 @@ -- | Several comma-separated types or static expressions TypeInExpr : TypeIn { $1 } - | Expression { [ConcreteType $1] } + | StaticExpression { [ConcreteType $1] } | TypeInExpr comma Type { $3 : $1 } - | TypeInExpr comma Expression { ConcreteType $3 : $1 } + | TypeInExpr comma StaticExpression { ConcreteType $3 : $1 } -- | Parse a type Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 } @@ -238,6 +238,7 @@ | Universal Type { ForA $1 $2 } | Type at Type { At $2 (Just $1) $3 } | at Type { At $1 Nothing $2 } + | atbrace Records rbrace { AnonymousRecord $1 $2 } | openParen Type vbar Type closeParen { ProofType $1 $2 $4 } | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] } | openParen TypeIn closeParen { Tuple $1 $2 } @@ -256,12 +257,13 @@ | Args comma Arg { $3 : $1 } | Arg vbar Arg { [ PrfArg $1 $3 ] } -Arg : identifier { Arg (First $ to_string $1) } - | identifier colon Type { Arg (Both (to_string $1) $3) } - | underscore { Arg (First "_") } - | Type { Arg (Second $1) } - | Expression { Arg (Second (ConcreteType $1)) } +TypeArg : identifier { Arg (First $ to_string $1) } + | IdentifierOr colon Type { Arg (Both $1 $3) } + | Type { Arg (Second $1) } +Arg : TypeArg { $1 } + | StaticExpression { Arg (Second (ConcreteType $1)) } + -- | Parse a literal Literal : boolLit { BoolLit $1 } | timeLit { TimeLit $1 } @@ -289,6 +291,9 @@ | Literal { PLiteral $1 } | Pattern when Expression { Guarded $2 $3 $1 } | at Pattern { AtPattern $1 $2 } + | identifier Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 } + | identifierSpace Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 } + | Existential Pattern { ExistentialPattern $1 $2 } | minus {% Left $ Expected $1 "Pattern" "-" } | plus {% Left $ Expected $1 "Pattern" "+" } @@ -335,6 +340,7 @@ | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 } | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 } | begin Expression extern {% Left $ Expected $3 "end" "extern" } + | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" } TypeArgs : lbrace Type rbrace { [$2] } | lbrace TypeIn rbrace { $2 } @@ -418,16 +424,16 @@ -- | Parse a termetric Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) } - | underscore {% Left $ Expected $1 "_" "Name" } - | dollar {% Left $ Expected $1 "$" "Name" } + | underscore {% Left $ Expected $1 "_" "Termination metric" } + | dollar {% Left $ Expected $1 "$" "Termination metric" } -- | Parse an existential quantier on a type -Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) } - | lsqbracket Args rsqbracket { Existential $2 Nothing Nothing } - | openExistential Args rsqbracket { Existential $2 Nothing Nothing } - | openExistential Args vbar Expression rsqbracket { Existential $2 Nothing (Just $4) } - | lsqbracket Args colon Type rsqbracket { Existential $2 (Just $4) Nothing } -- FIXME arguments should include more than just ':' - | lsqbracket Expression rsqbracket { Existential [] Nothing (Just $2) } +Existential : lsqbracket Args vbar Expression rsqbracket { Existential $2 False Nothing (Just $4) } + | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing } + | openExistential Args rsqbracket { Existential $2 True Nothing Nothing } + | openExistential Args vbar Expression rsqbracket { Existential $2 True Nothing (Just $4) } + | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':' + | lsqbracket Expression rsqbracket { Existential [] False Nothing (Just $2) } -- | Parse a universal quantifier on a type Universal : lbrace Args rbrace { Universal $2 Nothing Nothing } @@ -446,6 +452,7 @@ -- | Parse a general name Name : identifier { Unqualified (to_string $1) } + | underscore { Unqualified "_" } | listVT { Unqualified "list_vt" } | dollar identifier dot identifier { Qualified $1 (to_string $4) (to_string $2) } | dollar identifier dot identifierSpace { Qualified $1 (to_string $4) (to_string $2) } @@ -454,7 +461,6 @@ | dollar extype { SpecialName $1 "effmask_all" } | dollar listVT { SpecialName $1 "list_vt" } | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this - | underscore {% Left $ Expected $1 "Name" "_" } | dollar {% Left $ Expected $1 "Name" "$" } -- | Parse a list of values in a record @@ -585,13 +591,8 @@ | { Nothing } -- | Parse a declaration defining a type -TypeDecl : typedef IdentifierOr eq Universals atbrace Records rbrace { RecordType $2 [] $4 $6 } - | typedef IdentifierOr openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordType $2 $4 $7 $9 } - | typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 } +TypeDecl : typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 } | typedef IdentifierOr openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 } - | vtypedef IdentifierOr eq Universals atbrace Records rbrace { RecordViewType $2 [] $4 $6 } - | vtypedef IdentifierOr openParen FullArgs closeParen eq Universal atbrace Records rbrace { RecordViewType $2 $4 [$7] $9 } - | vtypedef IdentifierOr openParen FullArgs closeParen eq Universals atbrace Records rbrace { RecordViewType $2 $4 $7 $9 } | vtypedef IdentifierOr eq Type { ViewTypeDef $1 $2 [] $4 } | vtypedef IdentifierOr openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 } | datatype IdentifierOr eq Leaves { SumType $2 [] $4 } @@ -606,7 +607,7 @@ | abstype IdentifierOr openParen FullArgs closeParen MaybeType { AbsType $1 $2 $4 $6 } | absvtype IdentifierOr openParen FullArgs closeParen MaybeType { AbsViewType $1 $2 $4 $6 } | dataprop IdentifierOr openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 } - | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 [] } + | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 } | stadef IdentifierOr eq Name { Stadef $2 $4 [] } | stadef IdentifierOr eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 } | stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] } -- TODO identifierSpace @@ -644,7 +645,7 @@ | 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 } + | prval Pattern eq Expression { PrVal $2 $4 } | praxi PreFunction { Func $1 (Praxi $2) } | primplmnt Implementation { ProofImpl $2 } | implement Implementation { Impl [] $2 } @@ -667,7 +668,6 @@ | fromVT {% Left $ Expected $1 "Declaration" "?!" } | prfTransform {% Left $ Expected $1 "Declaration" ">>" } | maybeProof {% Left $ Expected $1 "Declaration" "?" } - | end {% Left $ Expected $1 "Declaration" "end" } | identifier {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) } { 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 @@ -141,7 +141,7 @@ -- FIXME we really need a monadic pretty printer lol. lengthAlt :: Doc -> Doc -> Doc lengthAlt d1 d2 - | length (showFast d2) >= 40 = d1 <$> indent 4 d2 + | length (showFast d2) >= 30 = d1 <$> indent 4 d2 | otherwise = d1 <+> d2 instance Pretty Expression where @@ -174,6 +174,7 @@ a (CallF nam [] [] (Just e) xs) = pretty nam <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|" a (CallF nam [] [] Nothing xs) = pretty nam <> prettyArgsG "(" ")" xs a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us + a (CallF nam [] us Nothing xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsG "(" ")" xs a (CallF nam is [] Nothing []) = pretty nam <> prettyArgsU "<" ">" is a (CallF nam is [] Nothing [x]) | startsParens x = pretty nam <> prettyArgsU "<" ">" is <> pretty x @@ -210,7 +211,10 @@ a (AddrAtF _ e) = "addr@" <> e a (ViewAtF _ e) = "view@" <> e a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es - a _ = undefined + a BinListF{} = undefined + a FixAtF{} = undefined + a LambdaAtF{} = undefined + a CallF{} = undefined prettyCases [] = mempty prettyCases [(s, l, t)] = "|" <+> pretty s <+> pretty l <+> t prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ... @@ -223,17 +227,19 @@ instance Pretty Pattern where pretty = cata a where - a (WildcardF _) = "_" - a (PSumF s x) = string s <+> x - a (PLiteralF e) = pretty e - a (PNameF s []) = string s - a (PNameF s [x]) = string s <> parens x - a (PNameF s ps) = string s <> parens (patternHelper ps) - a (FreeF p) = "~" <> p - a (GuardedF _ e p) = p <+> "when" <+> pretty e - a (ProofF _ p p') = parens (patternHelper p <+> "|" <+> patternHelper p') - a (TuplePatternF ps) = parens (patternHelper ps) - a (AtPatternF _ p) = "@" <> p + a (WildcardF _) = "_" + a (PSumF s x) = string s <+> x + a (PLiteralF e) = pretty e + a (PNameF s []) = string s + a (PNameF s [x]) = string s <> parens x + a (PNameF s ps) = string s <> parens (patternHelper ps) + a (FreeF p) = "~" <> p + a (GuardedF _ e p) = p <+> "when" <+> pretty e + a (ProofF _ p p') = parens (patternHelper p <+> "|" <+> patternHelper p') + a (TuplePatternF ps) = parens (patternHelper ps) + a (AtPatternF _ p) = "@" <> p + a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p + a (ExistentialPatternF e p) = pretty e <> p instance Pretty Arg where pretty (Arg (First s)) = pretty s @@ -264,49 +270,54 @@ instance Pretty Type where pretty = cata a where - a IntF = "int" - a StringF = "string" - a BoolF = "bool" - a VoidF = "void" - a NatF = "nat" - a AddrF = "addr" - a CharF = "char" - a (NamedF n) = pretty n - a (ExF e t) = pretty e <+> t - a (DependentIntF e) = "int(" <> pretty e <> ")" - a (DependentBoolF e) = "bool(" <> pretty e <> ")" - a (DepStringF e) = "string(" <> pretty e <> ")" - a (DependentF n ts) = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) - a DoubleF = "double" - a FloatF = "float" - a (ForAF u t) = pretty u <+> t - a (UnconsumedF t) = "!" <> t - a (AsProofF t (Just t')) = t <+> ">>" <+> t' - a (AsProofF t Nothing) = t <+> ">> _" - a (FromVTF t) = t <> "?!" - a (MaybeValF t) = t <> "?" - a (T0pF ad) = "t@ype" <> pretty ad - a (Vt0pF ad) = "vt@ype" <> pretty ad - a (AtF _ (Just t) t') = t <+> "@" <+> t' - a (AtF _ Nothing t) = "@" <> t - a (ProofTypeF _ t t') = parens (t <+> "|" <+> t') - a (ConcreteTypeF e) = pretty e - a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) - a (RefTypeF t) = "&" <> t - a (ViewTypeF _ t) = "view@" <> parens t - a (FunctionTypeF s t t') = t <+> string s <+> t' - a (ViewLiteralF c) = "view" <> pretty c - a NoneTypeF{} = "()" - a ImplicitTypeF{} = ".." + a IntF = "int" + a StringF = "string" + a BoolF = "bool" + a VoidF = "void" + a NatF = "nat" + a AddrF = "addr" + a CharF = "char" + a (NamedF n) = pretty n + a (ExF e t) = pretty e <+> t + a (DependentIntF e) = "int(" <> pretty e <> ")" + a (DependentBoolF e) = "bool(" <> pretty e <> ")" + a (DepStringF e) = "string(" <> pretty e <> ")" + a (DependentF n ts) = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) + a DoubleF = "double" + a FloatF = "float" + a (ForAF u t) = pretty u <+> t + a (UnconsumedF t) = "!" <> t + a (AsProofF t (Just t')) = t <+> ">>" <+> t' + a (AsProofF t Nothing) = t <+> ">> _" + a (FromVTF t) = t <> "?!" + a (MaybeValF t) = t <> "?" + a (T0pF ad) = "t@ype" <> pretty ad + a (Vt0pF ad) = "vt@ype" <> pretty ad + a (AtF _ (Just t) t') = t <+> "@" <+> t' + a (AtF _ Nothing t) = "@" <> t + a (ProofTypeF _ t t') = parens (t <+> "|" <+> t') + a (ConcreteTypeF e) = pretty e + a (TupleF _ ts) = parens (mconcat (punctuate ", " (fmap pretty (reverse ts)))) + a (RefTypeF t) = "&" <> t + a (ViewTypeF _ t) = "view@" <> parens t + a (FunctionTypeF s t t') = t <+> string s <+> t' + a (ViewLiteralF c) = "view" <> pretty c + a NoneTypeF{} = "()" + a ImplicitTypeF{} = ".." + a (AnonymousRecordF _ rs) = prettyRecord rs gan :: Maybe Type -> Doc gan (Just t) = " : " <> pretty t <> " " gan Nothing = "" +withHashtag :: Bool -> Doc +withHashtag True = "#[" +withHashtag _ = lbracket + instance Pretty Existential where - pretty (Existential [] Nothing (Just e)) = lbracket <+> pretty e <+> rbracket - pretty (Existential bs ty Nothing) = lbracket <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket - pretty (Existential bs ty (Just e)) = lbracket <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket + pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket + pretty (Existential bs b ty Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket + pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket where go (Arg (First s)) = pretty s go (Arg (Both s t)) = pretty s <+> colon <+> pretty t go (Arg (Second t)) = pretty t @@ -478,58 +489,52 @@ 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 = ("=" <#>) . prettyRecord - instance Pretty Declaration where - pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as - pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettyArgs as - pretty (RecordType s [] [] rs) = "typedef" <+> text s <+> "=" <+> prettyRecord rs - pretty (RecordType s as [] rs) = "typedef" <+> text s <> prettyArgs as <+> "=" <+> prettyRecord rs - pretty (RecordViewType s [] [] rs) = "vtypedef" <+> text s <+> "=" prettyRecord rs - pretty (RecordViewType s as [] rs) = "vtypedef" <+> text s <> prettyArgs as <+> typeHelper rs - pretty (RecordViewType s as us rs) = "vtypedef" <+> text s <> prettyArgs as <+> "=" fancyU us prettyRecord rs - pretty (SumViewType s [] ls) = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls - pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls - pretty (SumType s [] ls) = "datatype" <+> text s <+> "=" <$> prettyLeaf ls - pretty (SumType s as ls) = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls - pretty (Impl [] i) = pretty i - pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e - pretty (Val a Nothing p e) = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e - pretty (Val a (Just t) p e) = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e - pretty (Var (Just t) p Nothing e) = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e - pretty (Var Nothing p e Nothing) = "var" <+> pretty p <+> "=" <+> pretty e - pretty (Var (Just t) p e Nothing) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e - pretty (Include s) = "#include" <+> pretty s - pretty (Staload Nothing s) = "staload" <+> pretty s - pretty (Staload (Just q) s) = "staload" <+> pretty q <+> "=" <+> pretty s - pretty (CBlock s) = string s - pretty (Comment s) = string s - pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n - pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n + pretty (AbsType _ s as Nothing) = "abstype" <+> text s <> prettyArgs as + pretty (AbsViewType _ s as Nothing) = "absvtype" <+> text s <> prettyArgs as + pretty (AbsViewType _ s as (Just t)) = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t + pretty (SumViewType s [] ls) = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls + pretty (SumViewType s as ls) = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls + pretty (SumType s [] ls) = "datatype" <+> text s <+> "=" <$> prettyLeaf ls + pretty (SumType s as ls) = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls + pretty (Impl [] i) = pretty i + pretty (PrVal p e) = "prval" <+> pretty p <+> "=" <+> pretty e + pretty (Val a Nothing p e) = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e + pretty (Val a (Just t) p e) = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e + pretty (Var (Just t) p Nothing e) = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e + pretty (Var Nothing p e Nothing) = "var" <+> pretty p <+> "=" <+> pretty e + pretty (Var (Just t) p e Nothing) = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e + pretty (Include s) = "#include" <+> pretty s + pretty (Staload Nothing s) = "staload" <+> pretty s + pretty (Staload (Just q) s) = "staload" <+> pretty q <+> "=" <+> pretty s + pretty (CBlock s) = string s + pretty (Comment s) = string s + pretty (OverloadOp _ o n) = "overload" <+> pretty o <+> "with" <+> pretty n + pretty (OverloadIdent _ i n Nothing) = "overload" <+> text i <+> "with" <+> pretty n pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n' -- We use 'text' here, which means indentation might get fucked up for -- C preprocessor macros, but you absolutely deserve it if you indent your -- macros. - pretty (Define s) = text s - pretty (Func _ (Fn pref)) = "fn" pretty pref - pretty (Func _ (Fun pref)) = "fun" pretty pref - pretty (Func _ (CastFn pref)) = "castfn" pretty pref - pretty (Func _ (Fnx pref)) = "fnx" pretty pref - pretty (Func _ (And pref)) = "and" pretty pref - pretty (Func _ (Praxi pref)) = "praxi" pretty pref - pretty (Func _ (PrFun pref)) = "prfun" pretty pref - pretty (Func _ (PrFn pref)) = "prfn" pretty pref - pretty (Extern _ d) = "extern" <$> pretty d - pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls - pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> text s <+> "=" pretty t - pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettyArgs as <+> "=" pretty t - pretty (TypeDef _ s [] t) = "typedef" <+> text s <+> "=" <+> pretty t - pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t - pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as - pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e - pretty (SymIntr _ n) = "symintr" <+> pretty n - pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t - pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e - pretty (PropDef _ s as t) = "propdef" text s <+> prettyArgs as <+> "=" pretty t - pretty _ = undefined + pretty (Define s) = text s + pretty (Func _ (Fn pref)) = "fn" pretty pref + pretty (Func _ (Fun pref)) = "fun" pretty pref + pretty (Func _ (CastFn pref)) = "castfn" pretty pref + pretty (Func _ (Fnx pref)) = "fnx" pretty pref + pretty (Func _ (And pref)) = "and" pretty pref + pretty (Func _ (Praxi pref)) = "praxi" pretty pref + pretty (Func _ (PrFun pref)) = "prfun" pretty pref + pretty (Func _ (PrFn pref)) = "prfn" pretty pref + pretty (Extern _ d) = "extern" <$> pretty d + pretty (DataProp _ s as ls) = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls + pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> text s <+> "=" <#> pretty t + pretty (ViewTypeDef _ s as t) = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t + pretty (TypeDef _ s [] t) = "typedef" <+> text s <+> "=" <+> pretty t + pretty (TypeDef _ s as t) = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t + pretty (AbsProp _ n as) = "absprop" <+> text n <+> prettyArgs as + pretty (Assume n as e) = "assume" pretty n <> prettyArgs as <+> "=" pretty e + pretty (SymIntr _ n) = "symintr" <+> pretty n + pretty (Stacst _ n t Nothing) = "stacst" pretty n <+> ":" pretty t + pretty (Stacst _ n t (Just e)) = "stacst" pretty n <+> ":" pretty t <+> "=" pretty e + pretty (PropDef _ s as t) = "propdef" text s <+> prettyArgs as <+> "=" pretty t + pretty (Local _ d d') = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end" + pretty _ = undefined 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 @@ -78,8 +78,6 @@ | Staload (Maybe String) String | Stadef String Name [Type] | CBlock String - | RecordType String [Arg] [Universal] [(String, Type)] - | RecordViewType String [Arg] [Universal] [(String, Type)] | TypeDef AlexPosn String [Arg] Type | ViewTypeDef AlexPosn String [Arg] Type | SumType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] } @@ -98,7 +96,7 @@ | Define String | SortDef AlexPosn String Type | AndD Declaration Declaration - | Local AlexPosn [Declaration] [Declaration] + | Local AlexPosn ATS ATS | AbsProp AlexPosn String [Arg] | Assume Name [Arg] Expression | TKind AlexPosn Name String @@ -139,13 +137,14 @@ | Vt0p Addendum -- vt@ype | At AlexPosn (Maybe Type) Type | ProofType AlexPosn Type Type -- Aka (prf | val) - | ConcreteType Expression + | ConcreteType StaticExpression | RefType Type | ViewType AlexPosn Type | FunctionType String Type Type | NoneType AlexPosn | ImplicitType AlexPosn | ViewLiteral Addendum + | AnonymousRecord AlexPosn [(String, Type)] deriving (Show, Eq, Generic, NFData) -- | A type for the various lambda arrows (@=>@, @=\@, etc.) @@ -172,6 +171,8 @@ | Proof AlexPosn [Pattern] [Pattern] | TuplePattern [Pattern] | AtPattern AlexPosn Pattern + | UniversalPattern AlexPosn String [Universal] Pattern + | ExistentialPattern Existential Pattern deriving (Show, Eq, Generic, NFData) data Paired a b = Both a b @@ -190,7 +191,7 @@ deriving (Show, Eq, Generic, NFData) -- | Wrapper for existential quantifiers/types -data Existential = Existential { boundE :: [Arg], typeE :: Maybe Type, propE :: Maybe Expression } -- TODO #[id:int] existentials +data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe Expression } -- TODO #[id:int] existentials deriving (Show, Eq, Generic, NFData) -- | @~@ is used to negate numbers in ATS diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -8,7 +8,7 @@ - composition-prelude-1.1.0.0 - dirstream-1.0.3 - hspec-dirstream-0.3.0.0 - - cli-setup-0.1.0.2 + - cli-setup-0.1.0.3 flags: ats-format: development: false diff --git a/test/data/concurrency.dats b/test/data/concurrency.dats new file mode 100644 --- /dev/null +++ b/test/data/concurrency.dats @@ -0,0 +1,257 @@ +// This is mostly taken from the example in the book. + +#include "share/atspre_staload.hats" +#include "share/atspre_staload_libats_ML.hats" +#include "libats/DATS/athread_posix.dats" + +staload "libats/SATS/athread.sats" +staload "src/filetype.sats" +staload "libats/SATS/funarray.sats" +staload "libats/SATS/deqarray.sats" +staload _ = "libats/DATS/deqarray.dats" + +absvtype queue_vtype(a: vt@ype+, int) = ptr + +vtypedef queue(a: vt0p, id: int) = queue_vtype(a, id) +vtypedef queue(a: vt0p) = [id:int] queue(a, id) + +absprop ISNIL(id: int, b: bool) + +extern fun {a:vt0p} queue_is_nil {id:int} (!queue(a, id)) : [b:bool] (ISNIL(id, b) | bool(b)) + +absprop ISFULL(id: int, b: bool) + +extern fun {a:vt0p} queue_is_full {id:int} (!queue(a, id)) : [b:bool] (ISFULL(id, b) | bool(b)) + +extern fun {a:vt0p} queue_insert {id:int} (ISFULL(id, false) | xs: !queue(a, id) >> queue(a, id2), x: a) : #[id2:int] void + +extern fun {a:vt0p} queue_remove {id:int} (ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2)) : #[id2:int] a + +extern fun {a:vt0p} queue_make (cap: intGt(0)) : queue(a) + +extern fun {a:t@ype} queue_free(que: queue(a)) : void + +assume queue_vtype(a: vt0p, id: int) = deqarray(a) +assume ISNIL(id: int, b: bool) = unit_p +assume ISFULL(id: int, b: bool) = unit_p + +absvtype channel_vtype(a: vt@ype+) = ptr + +vtypedef channel(a: vt0p) = channel_vtype(a) + +extern fun {a:vt0p} channel_insert (!channel(a), a) : void + +extern fun {a:vt0p} channel_remove (chan: !channel(a)) : a + +extern fun {a:vt0p} channel_remove_helper (chan: !channel(a), !queue(a) >> _) : a + +extern fun {a:vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) : void + +datavtype channel_ = {l0,l1,l2,l3:agz} CHANNEL of + @{ cap = intGt(0) + , spin = spin_vt(l0) + , refcount = intGt(0) + , mutex = mutex_vt(l1) + , CVisNil = condvar_vt(l2) + , CVisFull = condvar_vt(l3) + , queue = ptr + } + +extern fun {a:vt0p} channel_make(cap: intGt(0)) : channel(a) + +extern fun {a:vt0p} channel_ref(ch: !channel(a)) : channel(a) + +extern fun {a:vt0p} channel_unref(ch: channel(a)) : Option_vt(queue(a)) + +extern fun channel_refcount{a:vt0p}(ch: !channel(a)) : intGt(0) + +assume channel_vtype(a:vt0p) = channel_ + +implement {a} queue_is_nil(xs) = (unit_p() | deqarray_is_nil(xs)) + +implement {a} queue_is_full(xs) = (unit_p() | deqarray_is_full(xs)) + +implement {a} queue_remove(prf | xs) = + let + prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISNIL(id, false)) : [false] void } + in + deqarray_takeout_atbeg (xs) + end + +implement {a} queue_insert(prf | xs, x) = + { + prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISFULL(id, false)) : [false] void } + val () = deqarray_insert_atend(xs, x) + } + +implement {a} queue_make(cap) = deqarray_make_cap(i2sz(cap)) + +implement {a} queue_free(que) = deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que)) + +implement {a} channel_ref(chan) = + let + val@ CHANNEL(ch) = chan + val spin = unsafe_spin_vt2t(ch.spin) + val (prf | ()) = spin_lock(spin) + val () = ch.refcount := ch.refcount + 1 + val () = spin_unlock (prf | spin) + prval () = fold@(chan) + in + $UN.castvwtp1{channel(a)}(chan) + end + +implement {a} channel_unref(chan) = + let + val@ CHANNEL{l0,l1,l2,l3}(ch) = chan + val spin = unsafe_spin_vt2t(ch.spin) + val (prf | ()) = spin_lock(spin) + val () = spin_unlock(prf | spin) + val refcount = ch.refcount // needed to make the theorem prover work + in + if refcount <= 1 then + let + val que = $UN.castvwtp0{queue(a)}(ch.queue) + val () = spin_vt_destroy(ch.spin) + val () = mutex_vt_destroy(ch.mutex) + val () = condvar_vt_destroy(ch.CVisNil) + val () = condvar_vt_destroy(ch.CVisFull) + val () = free@{l0,l1,l2,l3}(chan) + in + Some_vt(que) + end + else + let + val () = ch.refcount := refcount - 1 + prval () = fold@chan + prval () = $UN.cast2void(chan) + in + None_vt() + end + end + +implement channel_refcount{a}(chan) = + let + val@ CHANNEL{l0,l1,l2,l3}(ch) = chan + val refcount = ch.refcount + in + fold@(chan) ; refcount + end + +implement {a} channel_make(cap) = + let + extern praxi __assert() : [l:agz] void + + prval [l0:addr] () = __assert() + prval [l1:addr] () = __assert() + prval [l2:addr] () = __assert() + prval [l3:addr] () = __assert() + + val chan = CHANNEL{l0,l1,l2,l3}(_) + val+ CHANNEL(ch) = chan + + val () = ch.cap := cap + val () = ch.refcount := 1 + + local + val x = spin_create_exn() + in + val () = ch.spin := unsafe_spin_t2vt(x) + end + + local + val x = mutex_create_exn() + in + val () = ch.mutex := unsafe_mutex_t2vt(x) + end + + local + val x = condvar_create_exn() + in + val () = ch.CVisNil := unsafe_condvar_t2vt(x) + end + + local + val x = condvar_create_exn() + in + val () = ch.CVisFull := unsafe_condvar_t2vt(x) + end + + val () = ch.queue := $UN.castvwtp0{ptr}(queue_make(cap)) + + in + fold@(chan) ; chan + end + +implement {a} channel_insert(chan, x) = + let + val+ CHANNEL{l0,l1,l2,l3}(ch) = chan + val mutex = unsafe_mutex_vt2t(ch.mutex) + val (prf | ()) = mutex_lock(mutex) + val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue)) + val () = channel_insert_helper(chan, xs, x) + prval prf = $UN.castview0{locked_v(l1)}(xs) + val () = mutex_unlock(prf | mutex) + in + end + +implement {a} channel_remove(chan) = x where + { + val+ CHANNEL{l0,l1,l2,l3}(ch) = chan + val mutex = unsafe_mutex_vt2t(ch.mutex) + val (prf | ()) = mutex_lock(mutex) + val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue)) + val x = channel_remove_helper (chan, xs) + prval prf = $UN.castview0{locked_v(l1)}(xs) + val () = mutex_unlock(prf | mutex) + } + +implement {a} channel_remove_helper(chan, xs) = + let + val+ CHANNEL{l0,l1,l2,l3}(ch) = chan + val (prf | is_nil) = queue_is_nil(xs) + in + if is_nil then + let + prval (pfmut, fpf) = __assert() where { extern praxi __assert(): vtakeout0(locked_v(l1)) } + val mutex = unsafe_mutex_vt2t(ch.mutex) + val CVisNil = unsafe_condvar_vt2t(ch.CVisNil) + val () = condvar_wait(pfmut | CVisNil, mutex) + prval () = fpf(pfmut) + in + channel_remove_helper(chan, xs) + end + else + let + val is_full = queue_is_full(xs) + val x_out = queue_remove(prf | xs) + val () = if is_full.1 then + condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull)) + in + x_out + end + end + +implement {a} channel_insert_helper(chan, xs, x) = + let + val+ CHANNEL{l0,l1,l2,l3}(ch) = chan + val (prf | is_full) = queue_is_full(xs) + in + if is_full then + let + prval (pfmut, fpf) = __assert() where { extern praxi __assert() : vtakeout0(locked_v(l1)) } + val mutex = unsafe_mutex_vt2t(ch.mutex) + val CVisFull = unsafe_condvar_vt2t(ch.CVisFull) + val () = condvar_wait(pfmut | CVisFull, mutex) + prval () = fpf(pfmut) + in + channel_insert_helper(chan, xs, x) + end + else + let + val is_nil = queue_is_nil(xs) + val () = queue_insert(prf | xs, x) + val () = if is_nil.1 then + condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil)) + in + end + end diff --git a/test/data/concurrency.out b/test/data/concurrency.out new file mode 100644 --- /dev/null +++ b/test/data/concurrency.out @@ -0,0 +1,288 @@ +// This is mostly taken from the example in the book. +#include "share/atspre_staload.hats" +#include "share/atspre_staload_libats_ML.hats" +#include "libats/DATS/athread_posix.dats" + +staload "libats/SATS/athread.sats" +staload "src/filetype.sats" +staload "libats/SATS/funarray.sats" +staload "libats/SATS/deqarray.sats" +staload _ = "libats/DATS/deqarray.dats" + +absvtype queue_vtype(a : vt@ype+, int) = ptr + +vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id) +vtypedef queue(a : vt0p) = [ id : int ] queue(a, id) + +absprop ISNIL (id : int, b : bool) + +extern +fun {a : vt0p} queue_is_nil {id : int} (!queue(a, id)) : + [ b : bool ] (ISNIL(id, b) | bool(b)) + +absprop ISFULL (id : int, b : bool) + +extern +fun {a : vt0p} queue_is_full {id : int} (!queue(a, id)) : + [ b : bool ] (ISFULL(id, b) | bool(b)) + +extern +fun {a : vt0p} queue_insert {id : int} +(ISFULL(id,false) | xs : !queue(a, id) >> queue(a, id2), x : a) : + #[ id2 : int ] void + +extern +fun {a : vt0p} queue_remove {id : int} +(ISNIL(id,false) | xs : !queue(a, id) >> queue(a, id2)) : + #[ id2 : int ] a + +extern +fun {a : vt0p} queue_make (cap : intGt(0)) : queue(a) + +extern +fun {a : t@ype} queue_free (que : queue(a)) : void + +assume queue_vtype(a : vt0p, id : int) = deqarray(a) + +assume ISNIL(id : int, b : bool) = unit_p + +assume ISFULL(id : int, b : bool) = unit_p + +absvtype channel_vtype(a : vt@ype+) = ptr + +vtypedef channel(a : vt0p) = channel_vtype(a) + +extern +fun {a : vt0p} channel_insert (!channel(a), a) : void + +extern +fun {a : vt0p} channel_remove (chan : !channel(a)) : a + +extern +fun {a : vt0p} channel_remove_helper ( chan : !channel(a) + , !queue(a) >> _ + ) : a + +extern +fun {a : vt0p} channel_insert_helper (!channel(a), !queue(a) >> _, a) : + void + +datavtype channel_ = + | { l0, l1, l2, l3 : agz } CHANNEL of @{ cap = intGt(0) + , spin = spin_vt(l0) + , refcount = intGt(0) + , mutex = mutex_vt(l1) + , CVisNil = condvar_vt(l2) + , CVisFull = condvar_vt(l3) + , queue = ptr + } + +extern +fun {a : vt0p} channel_make (cap : intGt(0)) : channel(a) + +extern +fun {a : vt0p} channel_ref (ch : !channel(a)) : channel(a) + +extern +fun {a : vt0p} channel_unref (ch : channel(a)) : Option_vt(queue(a)) + +extern +fun channel_refcount {a : vt0p} (ch : !channel(a)) : intGt(0) + +assume channel_vtype(a : vt0p) = channel_ + +implement {a} queue_is_nil (xs) = + (unit_p() | deqarray_is_nil(xs)) + +implement {a} queue_is_full (xs) = + (unit_p() | deqarray_is_full(xs)) + +implement {a} queue_remove (prf | xs) = + let + prval () = __assert(prf) where + { extern + praxi __assert {id : int} (p : ISNIL(id, false)) : [ false ] void } + in + deqarray_takeout_atbeg(xs) + end + +implement {a} queue_insert (prf | xs, x) = + { + prval () = __assert(prf) where + { extern + praxi __assert {id : int} (p : ISFULL(id, false)) : [ false ] void } + val () = deqarray_insert_atend(xs, x) + } + +implement {a} queue_make (cap) = + deqarray_make_cap(i2sz(cap)) + +implement {a} queue_free (que) = + deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que)) + +implement {a} channel_ref (chan) = + let + val @CHANNEL (ch) = chan + val spin = unsafe_spin_vt2t(ch.spin) + val (prf | ()) = spin_lock(spin) + val () = ch.refcount := ch.refcount + 1 + val () = spin_unlock(prf | spin) + prval () = fold@((chan)) + in + $UN.castvwtp1{channel(a)}(chan) + end + +implement {a} channel_unref (chan) = + let + val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val spin = unsafe_spin_vt2t(ch.spin) + val (prf | ()) = spin_lock(spin) + val () = spin_unlock(prf | spin) + val refcount = ch.refcount + in + if refcount <= 1 then + let + val que = $UN.castvwtp0{queue(a)}(ch.queue) + val () = spin_vt_destroy(ch.spin) + val () = mutex_vt_destroy(ch.mutex) + val () = condvar_vt_destroy(ch.CVisNil) + val () = condvar_vt_destroy(ch.CVisFull) + val () = free@{l0,l1,l2,l3}(chan) + in + Some_vt(que) + end + else + let + val () = ch.refcount := refcount - 1 + prval () = fold@(chan) + prval () = $UN.cast2void(chan) + in + None_vt() + end + end + +implement channel_refcount {a} (chan) = + let + val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val refcount = ch.refcount + in + (fold@((chan)) ; refcount) + end + +implement {a} channel_make (cap) = + let + extern + praxi __assert() : [ l : agz ] void + + prval [ l0 : addr ]() = __assert() + prval [ l1 : addr ]() = __assert() + prval [ l2 : addr ]() = __assert() + prval [ l3 : addr ]() = __assert() + val chan = CHANNEL{l0,l1,l2,l3}(_) + val+ CHANNEL (ch) = chan + val () = ch.cap := cap + val () = ch.refcount := 1 + + local + val x = spin_create_exn() + in + val () = ch.spin := unsafe_spin_t2vt(x) + end + + local + val x = mutex_create_exn() + in + val () = ch.mutex := unsafe_mutex_t2vt(x) + end + + local + val x = condvar_create_exn() + in + val () = ch.CVisNil := unsafe_condvar_t2vt(x) + end + + local + val x = condvar_create_exn() + in + val () = ch.CVisFull := unsafe_condvar_t2vt(x) + end + + val () = ch.queue := $UN.castvwtp0{ptr}(queue_make(cap)) + in + (fold@((chan)) ; chan) + end + +implement {a} channel_insert (chan, x) = + let + val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val mutex = unsafe_mutex_vt2t(ch.mutex) + val (prf | ()) = mutex_lock(mutex) + val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue)) + val () = channel_insert_helper(chan, xs, x) + prval prf = $UN.castview0{locked_v(l1)}(xs) + val () = mutex_unlock(prf | mutex) + in end + +implement {a} channel_remove (chan) = + x where + { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val mutex = unsafe_mutex_vt2t(ch.mutex) + val (prf | ()) = mutex_lock(mutex) + val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue)) + val x = channel_remove_helper(chan, xs) + prval prf = $UN.castview0{locked_v(l1)}(xs) + val () = mutex_unlock(prf | mutex) } + +implement {a} channel_remove_helper (chan, xs) = + let + val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val (prf | is_nil) = queue_is_nil(xs) + in + if is_nil then + let + prval (pfmut, fpf) = __assert() where + { extern + praxi __assert() : vtakeout0(locked_v(l1)) } + val mutex = unsafe_mutex_vt2t(ch.mutex) + val CVisNil = unsafe_condvar_vt2t(ch.CVisNil) + val () = condvar_wait(pfmut | CVisNil, mutex) + prval () = fpf(pfmut) + in + channel_remove_helper(chan, xs) + end + else + let + val is_full = queue_is_full(xs) + val x_out = queue_remove(prf | xs) + val () = if is_full.1 then + condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull)) + in + x_out + end + end + +implement {a} channel_insert_helper (chan, xs, x) = + let + val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan + val (prf | is_full) = queue_is_full(xs) + in + if is_full then + let + prval (pfmut, fpf) = __assert() where + { extern + praxi __assert() : vtakeout0(locked_v(l1)) } + val mutex = unsafe_mutex_vt2t(ch.mutex) + val CVisFull = unsafe_condvar_vt2t(ch.CVisFull) + val () = condvar_wait(pfmut | CVisFull, mutex) + prval () = fpf(pfmut) + in + channel_insert_helper(chan, xs, x) + end + else + let + val is_nil = queue_is_nil(xs) + val () = queue_insert(prf | xs, x) + val () = if is_nil.1 then + condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil)) + in end + end diff --git a/test/data/filecount.out b/test/data/filecount.out --- a/test/data/filecount.out +++ b/test/data/filecount.out @@ -22,7 +22,8 @@ in stream_vt_foldleft_cloptr( ffiles , init - , lam (acc, next) => step_stream(acc, s + "/" + next) + , lam (acc, next) => + step_stream(acc, s + "/" + next) ) end diff --git a/test/data/left-pad.out b/test/data/left-pad.out --- a/test/data/left-pad.out +++ b/test/data/left-pad.out @@ -8,7 +8,7 @@ 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)) + ) : [ cushion : nat ] (PAD(p, l, cushion) | strnptr(cushion+l)) extern fun {t : t@ype} fill_list {n : nat} (size : ssize_t(n), c : t) : @@ -18,7 +18,7 @@ let fun loop { i : nat | i <= n } .. ( size : ssize_t(i) , c : t - , res : list_vt(t, n - i) + , res : list_vt(t, n-i) ) : list_vt(t, n) = if (size = i2ssz(0)) then res diff --git a/test/data/polyglot.out b/test/data/polyglot.out --- a/test/data/polyglot.out +++ b/test/data/polyglot.out @@ -1035,7 +1035,8 @@ var viewstream = $EXTRA.streamize_fileref_word(x) val result = stream_vt_foldleft_cloptr( viewstream , init - , lam (acc, next) => step_keyword(size, acc, next, ext) + , lam (acc, next) => + step_keyword(size, acc, next, ext) ) val _ = fileref_close(x) in @@ -1564,14 +1565,10 @@ 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 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)