ats-format 0.1.3.1 → 0.1.3.3
raw patch · 12 files changed
+699/−146 lines, 12 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.ATS: RecordType :: String -> [Arg] -> [Universal] -> [(String, Type)] -> Declaration
- Language.ATS: RecordViewType :: String -> [Arg] -> [Universal] -> [(String, Type)] -> Declaration
+ Language.ATS: AnonymousRecord :: AlexPosn -> [(String, Type)] -> Type
+ Language.ATS: ExistentialPattern :: Existential -> Pattern -> Pattern
+ Language.ATS: UniversalPattern :: AlexPosn -> String -> [Universal] -> Pattern -> Pattern
+ Language.ATS: [isOpen] :: Existential -> Bool
- Language.ATS: ConcreteType :: Expression -> Type
+ Language.ATS: ConcreteType :: StaticExpression -> Type
- Language.ATS: Existential :: [Arg] -> Maybe Type -> Maybe Expression -> Existential
+ Language.ATS: Existential :: [Arg] -> Bool -> Maybe Type -> Maybe Expression -> Existential
- Language.ATS: Local :: AlexPosn -> [Declaration] -> [Declaration] -> Declaration
+ Language.ATS: Local :: AlexPosn -> ATS -> ATS -> Declaration
Files
- Justfile +4/−0
- ats-format.cabal +1/−1
- src/Language/ATS/Lexer.x +1/−1
- src/Language/ATS/Parser.y +26/−26
- src/Language/ATS/PrettyPrint.hs +105/−100
- src/Language/ATS/Types.hs +6/−5
- stack.yaml +1/−1
- test/data/concurrency.dats +257/−0
- test/data/concurrency.out +288/−0
- test/data/filecount.out +2/−1
- test/data/left-pad.out +2/−2
- test/data/polyglot.out +6/−9
Justfile view
@@ -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
ats-format.cabal view
@@ -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
src/Language/ATS/Lexer.x view
@@ -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) }
src/Language/ATS/Parser.y view
@@ -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) } {
src/Language/ATS/PrettyPrint.hs view
@@ -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
src/Language/ATS/Types.hs view
@@ -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 (@=>@, @=\<cloref1>@, 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
stack.yaml view
@@ -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
+ test/data/concurrency.dats view
@@ -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<a> (xs)+ end++implement {a} queue_insert(prf | xs, x) = + { + prval () = __assert(prf) where { extern praxi __assert {id:int} (p: ISFULL(id, false)) : [false] void }+ val () = deqarray_insert_atend<a>(xs, x)+ }++implement {a} queue_make(cap) = deqarray_make_cap(i2sz(cap))++implement {a} queue_free(que) = deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))++implement {a} channel_ref(chan) =+ let+ val@ CHANNEL(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = ch.refcount := ch.refcount + 1+ val () = spin_unlock (prf | spin)+ prval () = fold@(chan)+ in+ $UN.castvwtp1{channel(a)}(chan)+ end++implement {a} channel_unref(chan) = + let+ val@ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = spin_unlock(prf | spin)+ val refcount = ch.refcount // needed to make the theorem prover work+ in+ if refcount <= 1 then+ let+ val que = $UN.castvwtp0{queue(a)}(ch.queue)+ val () = spin_vt_destroy(ch.spin)+ val () = mutex_vt_destroy(ch.mutex)+ val () = condvar_vt_destroy(ch.CVisNil)+ val () = condvar_vt_destroy(ch.CVisFull)+ val () = free@{l0,l1,l2,l3}(chan)+ in+ Some_vt(que)+ end+ else+ let+ val () = ch.refcount := refcount - 1+ prval () = fold@chan+ prval () = $UN.cast2void(chan)+ in+ None_vt()+ end+ end++implement channel_refcount{a}(chan) =+ let+ val@ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val refcount = ch.refcount+ in+ fold@(chan) ; refcount+ end++implement {a} channel_make(cap) = + let+ extern praxi __assert() : [l:agz] void++ prval [l0:addr] () = __assert()+ prval [l1:addr] () = __assert()+ prval [l2:addr] () = __assert()+ prval [l3:addr] () = __assert()++ val chan = CHANNEL{l0,l1,l2,l3}(_)+ val+ CHANNEL(ch) = chan++ val () = ch.cap := cap+ val () = ch.refcount := 1+ + local + val x = spin_create_exn()+ in+ val () = ch.spin := unsafe_spin_t2vt(x)+ end++ local+ val x = mutex_create_exn()+ in+ val () = ch.mutex := unsafe_mutex_t2vt(x)+ end++ local+ val x = condvar_create_exn()+ in+ val () = ch.CVisNil := unsafe_condvar_t2vt(x)+ end++ local+ val x = condvar_create_exn()+ in+ val () = ch.CVisFull := unsafe_condvar_t2vt(x)+ end++ val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))++ in+ fold@(chan) ; chan+ end++implement {a} channel_insert(chan, x) = + let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val () = channel_insert_helper<a>(chan, xs, x)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ in+ end++implement {a} channel_remove(chan) = x where+ {+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val x = channel_remove_helper<a> (chan, xs)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ }++implement {a} channel_remove_helper(chan, xs) =+ let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val (prf | is_nil) = queue_is_nil(xs)+ in+ if is_nil then+ let+ prval (pfmut, fpf) = __assert() where { extern praxi __assert(): vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)+ val () = condvar_wait(pfmut | CVisNil, mutex)+ prval () = fpf(pfmut)+ in+ channel_remove_helper(chan, xs)+ end+ else+ let+ val is_full = queue_is_full(xs)+ val x_out = queue_remove(prf | xs)+ val () = if is_full.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))+ in+ x_out+ end+ end++implement {a} channel_insert_helper(chan, xs, x) = + let+ val+ CHANNEL{l0,l1,l2,l3}(ch) = chan+ val (prf | is_full) = queue_is_full(xs)+ in+ if is_full then+ let+ prval (pfmut, fpf) = __assert() where { extern praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)+ val () = condvar_wait(pfmut | CVisFull, mutex)+ prval () = fpf(pfmut)+ in+ channel_insert_helper(chan, xs, x)+ end+ else+ let+ val is_nil = queue_is_nil(xs)+ val () = queue_insert(prf | xs, x)+ val () = if is_nil.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))+ in+ end+ end
+ test/data/concurrency.out view
@@ -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<a>(xs)+ end++implement {a} queue_insert (prf | xs, x) =+ {+ prval () = __assert(prf) where+ { extern+ praxi __assert {id : int} (p : ISFULL(id, false)) : [ false ] void }+ val () = deqarray_insert_atend<a>(xs, x)+ }++implement {a} queue_make (cap) =+ deqarray_make_cap(i2sz(cap))++implement {a} queue_free (que) =+ deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))++implement {a} channel_ref (chan) =+ let+ val @CHANNEL (ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = ch.refcount := ch.refcount + 1+ val () = spin_unlock(prf | spin)+ prval () = fold@((chan))+ in+ $UN.castvwtp1{channel(a)}(chan)+ end++implement {a} channel_unref (chan) =+ let+ val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val spin = unsafe_spin_vt2t(ch.spin)+ val (prf | ()) = spin_lock(spin)+ val () = spin_unlock(prf | spin)+ val refcount = ch.refcount+ in+ if refcount <= 1 then+ let+ val que = $UN.castvwtp0{queue(a)}(ch.queue)+ val () = spin_vt_destroy(ch.spin)+ val () = mutex_vt_destroy(ch.mutex)+ val () = condvar_vt_destroy(ch.CVisNil)+ val () = condvar_vt_destroy(ch.CVisFull)+ val () = free@{l0,l1,l2,l3}(chan)+ in+ Some_vt(que)+ end+ else+ let+ val () = ch.refcount := refcount - 1+ prval () = fold@(chan)+ prval () = $UN.cast2void(chan)+ in+ None_vt()+ end+ end++implement channel_refcount {a} (chan) =+ let+ val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val refcount = ch.refcount+ in+ (fold@((chan)) ; refcount)+ end++implement {a} channel_make (cap) =+ let+ extern+ praxi __assert() : [ l : agz ] void+ + prval [ l0 : addr ]() = __assert()+ prval [ l1 : addr ]() = __assert()+ prval [ l2 : addr ]() = __assert()+ prval [ l3 : addr ]() = __assert()+ val chan = CHANNEL{l0,l1,l2,l3}(_)+ val+ CHANNEL (ch) = chan+ val () = ch.cap := cap+ val () = ch.refcount := 1+ + local+ val x = spin_create_exn()+ in+ val () = ch.spin := unsafe_spin_t2vt(x)+ end+ + local+ val x = mutex_create_exn()+ in+ val () = ch.mutex := unsafe_mutex_t2vt(x)+ end+ + local+ val x = condvar_create_exn()+ in+ val () = ch.CVisNil := unsafe_condvar_t2vt(x)+ end+ + local+ val x = condvar_create_exn()+ in+ val () = ch.CVisFull := unsafe_condvar_t2vt(x)+ end+ + val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))+ in+ (fold@((chan)) ; chan)+ end++implement {a} channel_insert (chan, x) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val () = channel_insert_helper<a>(chan, xs, x)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex)+ in end++implement {a} channel_remove (chan) =+ x where+ { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val (prf | ()) = mutex_lock(mutex)+ val xs = $UN.castvwtp0{queue(a)}((prf | ch.queue))+ val x = channel_remove_helper<a>(chan, xs)+ prval prf = $UN.castview0{locked_v(l1)}(xs)+ val () = mutex_unlock(prf | mutex) }++implement {a} channel_remove_helper (chan, xs) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val (prf | is_nil) = queue_is_nil(xs)+ in+ if is_nil then+ let+ prval (pfmut, fpf) = __assert() where+ { extern+ praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisNil = unsafe_condvar_vt2t(ch.CVisNil)+ val () = condvar_wait(pfmut | CVisNil, mutex)+ prval () = fpf(pfmut)+ in+ channel_remove_helper(chan, xs)+ end+ else+ let+ val is_full = queue_is_full(xs)+ val x_out = queue_remove(prf | xs)+ val () = if is_full.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisFull))+ in+ x_out+ end+ end++implement {a} channel_insert_helper (chan, xs, x) =+ let+ val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan+ val (prf | is_full) = queue_is_full(xs)+ in+ if is_full then+ let+ prval (pfmut, fpf) = __assert() where+ { extern+ praxi __assert() : vtakeout0(locked_v(l1)) }+ val mutex = unsafe_mutex_vt2t(ch.mutex)+ val CVisFull = unsafe_condvar_vt2t(ch.CVisFull)+ val () = condvar_wait(pfmut | CVisFull, mutex)+ prval () = fpf(pfmut)+ in+ channel_insert_helper(chan, xs, x)+ end+ else+ let+ val is_nil = queue_is_nil(xs)+ val () = queue_insert(prf | xs, x)+ val () = if is_nil.1 then+ condvar_broadcast(unsafe_condvar_vt2t(ch.CVisNil))+ in end+ end
test/data/filecount.out view
@@ -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
test/data/left-pad.out view
@@ -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 } .<i>. ( 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
test/data/polyglot.out view
@@ -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)