language-ats 0.1.1.4 → 0.1.1.5
raw patch · 19 files changed
+25/−3354 lines, 19 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.ATS: Call :: Name -> [Type] -> [Type] -> (Maybe Expression) -> [Expression] -> Expression
+ Language.ATS: Call :: Name -> [[Type]] -> [Type] -> (Maybe Expression) -> [Expression] -> Expression
Files
- language-ats.cabal +1/−1
- src/Language/ATS/Lexer.x +1/−1
- src/Language/ATS/Parser.y +7/−9
- src/Language/ATS/PrettyPrint.hs +14/−9
- src/Language/ATS/Types.hs +2/−1
- test/data/DivideConquerPar.dats +0/−325
- test/data/DivideConquerPar.out +0/−205
- test/data/chanlst_t.dats +0/−290
- test/data/chanlst_t.out +0/−144
- test/data/channel_vt.dats +0/−650
- test/data/channel_vt.out +0/−362
- test/data/concurrency.out +0/−2
- test/data/fworkshop.dats +0/−467
- test/data/fworkshop.out +0/−270
- test/data/fworkshop_channel.dats +0/−174
- test/data/fworkshop_channel.out +0/−114
- test/data/mylibies.out +0/−1
- test/data/nwaiter.dats +0/−197
- test/data/nwaiter.out +0/−132
language-ats.cabal view
@@ -1,5 +1,5 @@ name: language-ats-version: 0.1.1.4+version: 0.1.1.5 synopsis: Parser and pretty-printer for ATS. description: Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex. license: BSD3
src/Language/ATS/Lexer.x view
@@ -63,7 +63,7 @@ @string = \" ($printable # [\"\\] | @escape_str | $esc_char | \\ \n | \n)* \" -- Identifiers-@identifier = ($alpha | _) ($alpha | $digit | _ | ! | ' | "<>")*+@identifier = ($alpha | _) ($alpha | $digit | _ | ! | ')* -- Multi-line comments @not_close_paren = (\*+ [^\)] | [^\*] \))
src/Language/ATS/Parser.y view
@@ -356,12 +356,10 @@ TypeArgs : lbrace Type rbrace { [$2] } | lbrace TypeIn rbrace { $2 }- -- | lbrace StaticExpression rbrace { [ ConcreteType $2 ] } | TypeArgs lbrace Type rbrace { $3 : $1 } | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 } | TypeArgs lbrace StaticExpression rbrace { (ConcreteType $3) : $1 }- | Implicits { [] } -- FIXME this is stupid Call : Name doubleParens { Call $1 [] [] Nothing [] } | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }@@ -369,11 +367,9 @@ | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) } | Name TypeArgs doubleParens { Call $1 [] $2 Nothing [VoidLiteral $3] } | Name TypeArgs { Call $1 [] $2 Nothing [] }- | Name lspecial TypeIn rbracket doubleParens { Call $1 $3 [] Nothing [VoidLiteral $5] }- | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) }- | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }- | Name doubleBrackets doubleParens { Call $1 [] [Named (Unqualified "")] Nothing [VoidLiteral $3] } -- FIXME prints wrong- | Name doubleBrackets openParen ExpressionPrf closeParen { Call $1 [] [Named (Unqualified "")] (fst $4) (snd $4) } -- FIXME prints wrong+ | Name Implicits doubleParens { Call $1 $2 [] Nothing [VoidLiteral $3] }+ | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }+ | Name Implicits { Call $1 $2 [] Nothing [] } | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument | Name openParen ExpressionPrf end {% Left $ Expected $4 ")" "end"} | Name openParen ExpressionPrf else {% Left $ Expected $4 ")" "else"}@@ -422,8 +418,8 @@ | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 } | PreExpression mutateEq PreExpression { Mutate $1 $3 } | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }- | identifierSpace { NamedVal (Unqualified $ to_string $1) } | begin Expression end { Begin $1 $2 }+ | identifierSpace { NamedVal (Unqualified $ to_string $1) } | Name { NamedVal $1 } | lbrace ATS rbrace { Actions $2 } | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }@@ -462,6 +458,8 @@ Implicits : lspecial TypeIn rbracket { [$2] } | Implicits lspecial TypeIn rbracket { $3 : $1 }+ | doubleBrackets { [[Named (Unqualified "")]] }+ | Implicits doubleBrackets { [Named (Unqualified "")] : $1 } MaybeImplicit : Implicits { $1 } | { [] }@@ -707,7 +705,7 @@ | overload BinOp with Name { OverloadOp $1 $2 $4 } | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing } | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) } -- FIXME figure out a general solution.- | assume identifierSpace eq Type { Assume (Unqualified (to_string $2)) [] $4 }+ | assume identifierSpace eq Type { Assume (Unqualified (to_string $2)) [NoArgs] $4 } | assume Name eq Type { Assume $2 [NoArgs] $4 } | assume Name doubleParens eq Type { Assume $2 [] $5 } | assume Name openParen Args closeParen eq Type { Assume $2 $4 $7 }
src/Language/ATS/PrettyPrint.hs view
@@ -43,6 +43,9 @@ instance Eq Doc where (==) = on (==) show +pattern NoA :: [Arg]+pattern NoA = [NoArgs]+ -- | Pretty-print with sensible defaults. printATS :: ATS -> String printATS = (<> "\n") . printATSCustom 0.6 120@@ -150,11 +153,11 @@ a (CallF nam [] [] Nothing xs) = pretty nam <> prettyArgs 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 []) = pretty nam <> prettyImplicits is a (CallF nam is [] Nothing [x])- | startsParens x = pretty nam <> prettyArgsU "<" ">" is <> pretty x- a (CallF nam is [] Nothing xs) = pretty nam <> prettyArgsU "<" ">" is <> prettyArgs xs- a (CallF nam is [] (Just e) xs) = pretty nam <> prettyArgsU "<" ">" is <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs+ | startsParens x = pretty nam <> prettyImplicits is <> pretty x+ a (CallF nam is [] Nothing xs) = pretty nam <> prettyImplicits is <> prettyArgs xs+ a (CallF nam is [] (Just e) xs) = pretty nam <> prettyImplicits is <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs a (CaseF _ add e cs) = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs) a (IfCaseF _ cs) = "ifcase" <$> indent 2 (prettyIfCase cs) a (VoidLiteralF _) = "()"@@ -191,8 +194,9 @@ a (ListLiteralF _ s t es) = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es a BinListF{} = undefined a CallF{} = undefined- prettyIfCase [] = mempty- prettyIfCase [(s, l, t)] = "|" <+> s <+> pretty l <+> t+ prettyImplicits = mconcat . fmap (prettyArgsU "<" ">")+ prettyIfCase [] = mempty+ prettyIfCase [(s, l, t)] = "|" <+> s <+> pretty l <+> t prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t prettyCases [] = mempty prettyCases [(s, l, t)] = "|" <+> pretty s <+> pretty l <+> t@@ -345,6 +349,7 @@ glue TypeDef{} TypeDef{} = True glue Comment{} _ = True glue (Func _ Fnx{}) (Func _ And{}) = True+glue Assume{} Assume{} = True glue _ _ = False {-# INLINE glue #-}@@ -457,11 +462,11 @@ -- FIXME figure out a nicer algorithm for when/how to split lines. -- aka don't use '</>' in places. instance Pretty PreFunction where- pretty (PreF i si [] [] [NoArgs] (Just rt) Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack+ pretty (PreF i si [] [] NoA (Just 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 (Just rt) Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) pretty (PreF i si [] [] as (Just 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 (Just 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] (Just rt) Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)+ pretty (PreF i si [] us NoA (Just rt) Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) pretty (PreF i si [] us as (Just rt) Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) pretty (PreF i si pus [] as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) pretty (PreF i si pus [] as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)@@ -520,7 +525,7 @@ 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 [NoArgs] e) = "assume" </> pretty n <+> "=" </> pretty e+ pretty (Assume n NoA e) = "assume" </> pretty n <+> "=" </> pretty e 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
src/Language/ATS/Types.hs view
@@ -7,6 +7,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} @@ -238,7 +239,7 @@ | VoidLiteral -- The '()' literal representing inaction. AlexPosn -- function call: <a>, then {n}- | Call Name [Type] [Type] (Maybe Expression) [Expression]+ | Call Name [[Type]] [Type] (Maybe Expression) [Expression] | NamedVal Name | ListLiteral AlexPosn String Type [Expression] | If { cond :: Expression -- ^ Expression evaluating to a boolean value
− test/data/DivideConquerPar.dats
@@ -1,325 +0,0 @@-(***********************************************************************)-(* *)-(* Applied Type System *)-(* *)-(***********************************************************************)--(*-** ATS/Postiats - Unleashing the Potential of Types!-** Copyright (C) 2011-2017 Hongwei Xi, ATS Trustful Software, Inc.-** All rights reserved-**-** ATS is free software; you can redistribute it and/or modify it under-** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the-** Free Software Foundation; either version 3, or (at your option) any-** later version.-** -** ATS is distributed in the hope that it will be useful, but WITHOUT ANY-** WARRANTY; without even the implied warranty of MERCHANTABILITY or-** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License-** for more details.-** -** You should have received a copy of the GNU General Public License-** along with ATS; see the file COPYING. If not, please write to the-** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA-** 02110-1301, USA.-*)--(* ****** ****** *)--(* Author: Hongwei Xi *)-(* Start time: February, 2017 *)-(* Authoremail: hwxiATcsDOTbuDOTedu *)--(* ****** ****** *)-//-#define-ATS_PACKNAME-"ATSLIB.libats\-.BUCS320.DivideConquerPar"-//-(* ****** ****** *)-//-#staload-UN =-"prelude/SATS/unsafe.sats"-//-(* ****** ****** *)-//-#staload-"libats/ML/SATS/basis.sats"-#staload-"libats/ML/SATS/list0.sats"-//-#staload-"prelude/DATS/list_vt.dats"-#staload-"libats/ML/SATS/atspre.sats"-//-(* ****** ****** *)-//-#include "./../mydepies.hats"-//-(* ****** ****** *)-//-typedef-input = $DivideConquer.input-typedef-output = $DivideConquer.output-//-(* ****** ****** *)-//-vtypedef-fwork = () -<lincloptr1> void-vtypedef fworklst = List0_vt_(fwork)-//-typedef-spinref = $SPINREF.spinref(int)-//-(* ****** ****** *)-//-extern-fun{}-DivideConquerPar$submit- (fwork): void-extern-fun{}-DivideConquerPar$submit2- (x0: input, fwork): void-//-(* ****** ****** *)-//-datatype-fworkshop =-| FWORKSHOP_chanlst of- $FWORKSHOP_chanlst.fworkshop-| FWORKSHOP_channel of- $FWORKSHOP_channel.fworkshop-//-extern-fun{}-DivideConquerPar$fworkshop(): fworkshop-//-(* ****** ****** *)--implement-{}(*tmp*)-DivideConquerPar$submit- (fwork) = let-//-val-fworkshop =-DivideConquerPar$fworkshop<>- ((*void*))-//-in-//-case+-fworkshop-of (*case+*)-| FWORKSHOP_chanlst(fws) =>- {- val () =- $FWORKSHOP_chanlst.fworkshop_insert_lincloptr- ( fws- , llam() => 0 where- {- val () = fwork()- val () = // fwork needs to be freed- cloptr_free($UN.castvwtp0{cloptr(void)}(fwork))- } // end of [fworkshop_insert_lincloptr]- )- } (* FWORKSHOP_chanlst *)-| FWORKSHOP_channel(fws) =>- {- val () =- $FWORKSHOP_channel.fworkshop_insert_lincloptr- ( fws- , llam() => 0 where- {- val () = fwork()- val () = // fwork needs to be freed- cloptr_free($UN.castvwtp0{cloptr(void)}(fwork))- } // end of [fworkshop_insert_lincloptr]- )- } (* FWORKSHOP_channel *)-//-end // end of [DivideConquerPar$submit]--(* ****** ****** *)-//-implement-{}(*tmp*)-DivideConquerPar$submit2- (x0, fwork) =-(- DivideConquerPar$submit<>(fwork)-)-//-(* ****** ****** *)-//-#staload-DC = $DivideConquer-#staload-DC_cont = $DivideConquer_cont-//-(* ****** ****** *)--implement-{}(*tmp*)-$DC.DivideConquer$solve- (x0) = let-//-#staload $NWAITER-//-val NW =- nwaiter_create_exn()-val NWT =- nwaiter_initiate(NW)-val NWT =- $UN.castvwtp0{ptr}(NWT)-//-var res: output-//-val ((*void*)) =-$DC_cont.DivideConquer_cont$solve<>-( x0-, lam(r0) =>- nwaiter_ticket_put(NWT) where- {- val () =- $UN.ptr0_set<output>(addr@res, r0)- val NWT =- $UN.castvwtp0{nwaiter_ticket}(NWT)- } (* end of [lam] *)-) (* end of [val] *)-//-val () = nwaiter_waitfor(NW)-val () = nwaiter_destroy(NW)-//-in- $UN.ptr0_get<output>(addr@res)-end // end of [DivideConquer$solve]--(* ****** ****** *)--implement-{}(*tmp*)-$DC_cont.DivideConquer_cont$conquer- (_, xs, k0) = let-//-#staload-$SPINREF // opening it-//-fun-spinref_decget- (spnr: spinref) : int = let-//-var env: int = 0-typedef tenv = int-//-implement-spinref_process$fwork<int><tenv>- (x, env) =- let val () = (x := x - 1) in env := x end-//-in-//-let val () =- spinref_process_env<int><tenv>(spnr, env) in env-end // end of [let]-//-end // end of [spinref_decget]-//-fun-loop2-{n:nat}-(- x0: input-, xs: list(input, n)-, rs: !list_vt(output, n+1)-, spnr: spinref, res: list0(output)-) : void = let- val+- @list_vt_cons- (r0, rs1) = rs- // list_vt_cons- val addr_r0 = addr@(r0)- val () =- DivideConquerPar$submit2<>- ( x0- , llam() =>- (- $DC_cont.DivideConquer_cont$solve- ( x0- , lam(r0) => let- val () =- $UN.ptr0_set<output>- (addr_r0, r0)- // end of [$UN.ptr0_set]- val c0 = spinref_decget(spnr)- in- if (c0 > 0)- then (- // unfinished- ) (* end of [then] *)- else k0(res) where- {- val () =- $SPINVAR.spinvar_destroy($UN.castvwtp0(spnr))- } (* end of [else] *)- end // end of [let] // end of [lam]- )- ) (* llam *)- ) (* end of [val] *)-//-in-//-case+ xs of-| list_nil() => () where- {- prval ((*folded*)) = fold@(rs)- }-| list_cons(x1, xs) => () where- {- val () =- loop2(x1, xs, rs1, spnr, res)- prval ((*folded*)) = fold@(rs)- }-end (* end of [loop2] *)-//-val xs = g1ofg0(xs); val n0 = length(xs)-//-in (* in-of-let *)-//-ifcase-| n0 = 0 =>- k0(list0_nil())-| n0 = 1 => let- val+list_sing(x0) = xs- in- $DC_cont.DivideConquer_cont$solve(x0, lam(r0) => k0(list0_sing(r0)))- end // end of [n0 = 1]-| _(* n0 >= 2 *) => let-//- val rs =- list_map_cloref<input><output>- (- xs, lam _ => _- ) (* end of [val] *)- val res =- $UN.castvwtp1{list0(output)}(rs)-//- val+list_cons(x, xs) = xs- val ((*void*)) = loop2(x, xs, rs, spinref_create_exn<int>(n0), res)- prval ((*void*)) = $UN.cast2void(rs)-//- in- // nothing- end // end of [n0 >= 2]-//-end // end of [DivideConquer_cont$conquer]--(* ****** ****** *)--(* end of [DivideConquerPar.dats] *)
− test/data/DivideConquerPar.out
@@ -1,205 +0,0 @@-(***********************************************************************)-(* *)-(* Applied Type System *)-(* *)-(***********************************************************************)-(*-** ATS/Postiats - Unleashing the Potential of Types!-** Copyright (C) 2011-2017 Hongwei Xi, ATS Trustful Software, Inc.-** All rights reserved-**-** ATS is free software; you can redistribute it and/or modify it under-** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the-** Free Software Foundation; either version 3, or (at your option) any-** later version.-** -** ATS is distributed in the hope that it will be useful, but WITHOUT ANY-** WARRANTY; without even the implied warranty of MERCHANTABILITY or-** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License-** for more details.-** -** You should have received a copy of the GNU General Public License-** along with ATS; see the file COPYING. If not, please write to the-** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA-** 02110-1301, USA.-*)-(* ****** ****** *)-(* Author: Hongwei Xi *)-(* Start time: February, 2017 *)-(* Authoremail: hwxiATcsDOTbuDOTedu *)-(* ****** ****** *)-#define ATS_PACKNAME"ATSLIB.libats\-.BUCS320.DivideConquerPar"--(* ****** ****** *)-#staload UN = "prelude/SATS/unsafe.sats"--(* ****** ****** *)-#staload "libats/ML/SATS/basis.sats"-#staload "libats/ML/SATS/list0.sats"-#staload "prelude/DATS/list_vt.dats"-#staload "libats/ML/SATS/atspre.sats"--(* ****** ****** *)-#include "./../mydepies.hats"--(* ****** ****** *)-typedef input = $DivideConquer.input-typedef output = $DivideConquer.output--(* ****** ****** *)-vtypedef fwork = () -<lincloptr1> void-vtypedef fworklst = List0_vt_(fwork)--typedef spinref = $SPINREF.spinref(int)--(* ****** ****** *)-extern-fun DivideConquerPar$submit(fwork) : void--extern-fun DivideConquerPar$submit2(x0 : input, fwork) : void--(* ****** ****** *)-datatype fworkshop =- | FWORKSHOP_chanlst of $FWORKSHOP_chanlst.fworkshop- | FWORKSHOP_channel of $FWORKSHOP_channel.fworkshop--extern-fun DivideConquerPar$fworkshop() : fworkshop--(* ****** ****** *)-implement DivideConquerPar$submit (fwork) =- let- val fworkshop = DivideConquerPar$fworkshop{}(())- in- case+ fworkshop of- | FWORKSHOP_chanlst (fws) => {- val () = $FWORKSHOP_chanlst.fworkshop_insert_lincloptr( fws- , llam () =>- 0 where- { val () = fwork()- val () = cloptr_free($UN.castvwtp0{cloptr(void)}(fwork)) }- )- }- | FWORKSHOP_channel (fws) => {- val () = $FWORKSHOP_channel.fworkshop_insert_lincloptr( fws- , llam () =>- 0 where- { val () = fwork()- val () = cloptr_free($UN.castvwtp0{cloptr(void)}(fwork)) }- )- }- end--(* ****** ****** *)-implement DivideConquerPar$submit2 (x0, fwork) =- (DivideConquerPar$submit{}(fwork))--(* ****** ****** *)-#staload DC = $DivideConquer-#staload DC_cont = $DivideConquer_cont--(* ****** ****** *)-implement $DivideConquer$solve.DC (x0) =- let- #staload $NWAITER- - val NW = nwaiter_create_exn()- val NWT = nwaiter_initiate(NW)- val NWT = $UN.castvwtp0{ptr}(NWT)- var res: output with - val () = $DC_cont.DivideConquer_cont$solve{}( x0- , lam (r0) =>- nwaiter_ticket_put(NWT) where- { val () = $UN.ptr0_set<output>(addr@res, r0)- val NWT = $UN.castvwtp0{nwaiter_ticket}(NWT) }- )- val () = nwaiter_waitfor(NW)- val () = nwaiter_destroy(NW)- in- $UN.ptr0_get<output>(addr@res)- end--(* ****** ****** *)-implement $DivideConquer_cont$conquer.DC_cont (_, xs, k0) =- let- #staload $SPINREF- - fun spinref_decget(spnr : spinref) : int =- let- var env: int = 0- - typedef tenv = int- - implement spinref_process$fwork (x, env) =- let- val () = (x := x - 1)- in- env := x- end- in- let- val () = spinref_process_env(spnr, env)- in- env- end- end- - fun loop2 {n:nat} ( x0 : input- , xs : list(input, n)- , rs : !list_vt(output, n+1)- , spnr : spinref- , res : list0(output)- ) : void =- let- val+ @list_vt_cons (r0, rs1) = rs- val addr_r0 = addr@(r0)- val () = DivideConquerPar$submit2{}( x0- , llam () =>- ($DC_cont.DivideConquer_cont$solve( x0- , lam (r0) =>- let- val () = $UN.ptr0_set<output>( addr_r0- , r0- )- val c0 = spinref_decget(spnr)- in- if (c0 > 0) then- ()- else- k0(res) where- { val () = $SPINVAR.spinvar_destroy($UN.castvwtp0(spnr)) }- end- ))- )- in- case+ xs of- | list_nil() => () where- { prval () = fold@(rs) }- | list_cons (x1, xs) => () where- { val () = loop2(x1, xs, rs1, spnr, res)- prval () = fold@(rs) }- end- - val xs = g1ofg0(xs)- val n0 = length(xs)- in- ifcase- | n0 = 0 => k0(list0_nil())- | n0 = 1 => let- val+ list_sing (x0) = xs- in- $DC_cont.DivideConquer_cont$solve(x0, lam (r0) => k0(list0_sing(r0)))- end- | _ => let- val rs = list_map_cloref(xs, lam _ => _)- val res = $UN.castvwtp1{list0(output)}(rs)- val+ list_cons (x, xs) = xs- val () = loop2(x, xs, rs, spinref_create_exn<int>(n0), res)- prval () = $UN.cast2void(rs)- in end- end--(* ****** ****** *)-(* end of [DivideConquerPar.dats] *)
− test/data/chanlst_t.dats
@@ -1,290 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)--(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)--(* ****** ****** *)-//-// HX-2013-11:-// A list-based channel-//-(* ****** ****** *)-//-staload-UN =-"prelude/SATS/unsafe.sats"-//-(* ****** ****** *)-//-staload-"libats/SATS/athread.sats"-//-(* ****** ****** *)-//-staload "./../SATS/chanlst_t.sats"-//-(* ****** ****** *)-//-datatype-chanlst =-{-l1,l2:agz-} CHANLST of-(- ptr // List0_vt(a)-, mutex(l1), condvar(l2)-) (* end of [chanlst] *)-datavtype-chanlst_vt =-{-l1,l2:agz-} CHANLST_vt of-(- ptr // List0_vt(a)-, mutex(l1), condvar(l2)-) (* end of [chanlst_vt] *)-//-(* ****** ****** *)-//-assume-chanlst_type(a:vt0p) = chanlst-//-(* ****** ****** *)--implement-{a}(*tmp*)-chanlst_create_exn- ((*void*)) = let-//-val mut = mutex_create_exn()-//-val CVisnil = condvar_create_exn()-//-val xs0 = list_vt_nil{a}()-val xs0 = $UN.castvwtp0{ptr}(xs0)-//-in- CHANLST(xs0, mut, CVisnil)-end // end of [chanlst_create_exn]--(* ****** ****** *)--implement-{a}(*tmp*)-chanlst_insert- (chan, x0) = let-//-val-chan2 =-$UN.castvwtp0{chanlst_vt}(chan)-val+-@CHANLST_vt-{l1,l2}(buf, mut, CVisnil) = chan2-//-val-(pfmut | ()) = mutex_lock(mut)-//-val xs0 =-$UN.castvwtp0{List0_vt(a)}((pfmut|buf))-//-val-isnil = list_vt_is_nil(xs0)-//-val xs0 =- list_vt_cons{a}( x0, xs0 )-val ((*void*)) =- (buf := $UN.castvwtp0{ptr}(xs0))-//-val ((*void*)) =- if isnil then condvar_broadcast(CVisnil)-// end of [val]-//-prval-pfmut = $UN.castview0{locked_v(l1)}(buf)-//-val ((*void*)) = mutex_unlock(pfmut | mut)-//-prval ((*void*)) = fold@(chan2)-prval ((*void*)) = $UN.cast2void(chan2)-//-in- // nothing-end // end of [chanlst_insert]-//-(* ****** ****** *)--implement-{a}(*tmp*)-chanlst_insert_opt-(- chan, x0-) = None_vt((*void*)) where-{- val () = chanlst_insert(chan, x0) // non-blocking-} (* end of [chanlst_insert_opt] *)--(* ****** ****** *)-//-extern-fun{a:vt0p}-chanlst_takeout_buf- (chan: chanlst(a), buf_p: !aPtr1(List0_vt(a))): (a)-//-(* ****** ****** *)--implement-{a}(*tmp*)-chanlst_takeout- (chan) = x0_out where-{-//-val-chan2 =-$UN.castvwtp0{chanlst_vt}(chan)-val+-@CHANLST_vt-{l1,l2}(buf, mut, CVisnil) = chan2-//-val (pfmut | ()) = mutex_lock(mut)-//-val-buf_p =-$UN.castvwtp0-{aPtr1(List0_vt(a))}((pfmut|addr@buf))-//-val-x0_out =- chanlst_takeout_buf<a>(chan, buf_p)-//-prval-pfmut = $UN.castview0{locked_v(l1)}(buf_p)-//-val ((*void*)) = mutex_unlock(pfmut | mut)-//-prval ((*void*)) = fold@(chan2)-prval ((*void*)) = $UN.cast2void(chan2)-//-} (* end of [chanlst_takeout] *)--(* ****** ****** *)-//-implement-{a}(*tmp*)-chanlst_takeout_opt- (chan) = opt where-{-//-val-chan2 =-$UN.castvwtp0{chanlst_vt}(chan)-val+-@CHANLST_vt-{l1,l2}(buf, mut, CVisnil) = chan2-//-val-(pfmut | ()) = mutex_lock(mut)-//-val xs0 =-$UN.castvwtp0{List0_vt(a)}((pfmut|buf))-//-val opt =-(-case+ xs0 of-| ~list_vt_nil- () => None_vt()-| ~list_vt_cons- (x0, xs0) =>- Some_vt(x0) where- {- val () =- (buf := $UN.castvwtp0{ptr}(xs0))- }-) : Option_vt(a)-//-prval-pfmut = $UN.castview0{locked_v(l1)}(buf)-//-val ((*void*)) = mutex_unlock(pfmut | mut)-//-prval ((*void*)) = fold@(chan2)-prval ((*void*)) = $UN.cast2void(chan2)-//-} (* end of [chanlst_takeout_opt] *)-//-(* ****** ****** *)--implement-{a}(*tmp*)-chanlst_takeout_buf- (chan, buf_p) = let-//-val-chan2 =-$UN.castvwtp0{chanlst_vt}(chan)-val+-@CHANLST_vt-{l1,l2}(buf, mut, CVisnil) = chan2-//-val mut = mut and CVisnil = CVisnil-//-prval ((*void*)) = fold@(chan2)-prval ((*void*)) = $UN.cast2void(chan2)-//-val xs0 =- $UN.ptr1_get<List0_vt(a)>(aptr2ptr(buf_p))-//-in (* in-of-let *)-//-case+ xs0 of-| ~list_vt_nil() => let- prval- (pfmut, fpf) =- __assert((*void*)) where- {- extern- praxi- __assert- (- // argless- ) : vtakeout0(locked_v(l1))- }- val ((*void*)) =- condvar_wait(pfmut | CVisnil, mut)- prval ((*returned*)) = fpf( pfmut )- in- chanlst_takeout_buf<a>(chan, buf_p)- end // end of [list_vt_nil]-| ~list_vt_cons(x0_out, xs0) => x0_out where- {- val () =- $UN.ptr1_set<List0_vt(a)>(aptr2ptr(buf_p), xs0)- }-//-end // end of [chanlst_takeout_buf]--(* ****** ****** *)--(* end of [chanlst_t.dats] *)
− test/data/chanlst_t.out
@@ -1,144 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)-(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)-(* ****** ****** *)-// HX-2013-11:-// A list-based channel-(* ****** ****** *)-staload UN = "prelude/SATS/unsafe.sats"--(* ****** ****** *)-staload "libats/SATS/athread.sats"--(* ****** ****** *)-staload "./../SATS/chanlst_t.sats"--(* ****** ****** *)-datatype chanlst =- | { l1, l2 : agz } CHANLST of (ptr, mutex(l1), condvar(l2))--datavtype chanlst_vt =- | { l1, l2 : agz } CHANLST_vt of (ptr, mutex(l1), condvar(l2))--(* ****** ****** *)-assume chanlst_type(a : vt0p) = chanlst--(* ****** ****** *)-implement {a} chanlst_create_exn () =- let- val mut = mutex_create_exn()- val CVisnil = condvar_create_exn()- val xs0 = list_vt_nil{a}(())- val xs0 = $UN.castvwtp0{ptr}(xs0)- in- CHANLST(xs0, mut, CVisnil)- end--(* ****** ****** *)-implement {a} chanlst_insert (chan, x0) =- let- val chan2 = $UN.castvwtp0{chanlst_vt}(chan)- val+ @CHANLST_vt{ l1, l2 }(buf, mut, CVisnil) = chan2- val (pfmut | ()) = mutex_lock(mut)- val xs0 = $UN.castvwtp0{List0_vt(a)}((pfmut | buf))- val isnil = list_vt_is_nil(xs0)- val xs0 = list_vt_cons{a}(x0, xs0)- val () = (buf := $UN.castvwtp0{ptr}(xs0))- val () = if isnil then- condvar_broadcast(CVisnil)- prval pfmut = $UN.castview0{locked_v(l1)}(buf)- val () = mutex_unlock(pfmut | mut)- prval () = fold@(chan2)- prval () = $UN.cast2void(chan2)- in end--(* ****** ****** *)-implement {a} chanlst_insert_opt (chan, x0) =- None_vt() where- { val () = chanlst_insert(chan, x0) }--(* ****** ****** *)-extern-fun {a:vt0p} chanlst_takeout_buf ( chan : chanlst(a)- , buf_p : !aPtr1(List0_vt(a))- ) : a--(* ****** ****** *)-implement {a} chanlst_takeout (chan) =- x0_out where- { val chan2 = $UN.castvwtp0{chanlst_vt}(chan)- val+ @CHANLST_vt{ l1, l2 }(buf, mut, CVisnil) = chan2- val (pfmut | ()) = mutex_lock(mut)- val buf_p = $UN.castvwtp0{aPtr1(List0_vt(a))}((pfmut | addr@buf))- val x0_out = chanlst_takeout_buf<a>(chan, buf_p)- prval pfmut = $UN.castview0{locked_v(l1)}(buf_p)- val () = mutex_unlock(pfmut | mut)- prval () = fold@(chan2)- prval () = $UN.cast2void(chan2) }--(* ****** ****** *)-implement {a} chanlst_takeout_opt (chan) =- opt where- { val chan2 = $UN.castvwtp0{chanlst_vt}(chan)- val+ @CHANLST_vt{ l1, l2 }(buf, mut, CVisnil) = chan2- val (pfmut | ()) = mutex_lock(mut)- val xs0 = $UN.castvwtp0{List0_vt(a)}((pfmut | buf))- val opt = (case+ xs0 of- | ~list_vt_nil() => None_vt()- | ~list_vt_cons (x0, xs0) => Some_vt(x0) where- { val () = (buf := $UN.castvwtp0{ptr}(xs0)) }) : Option_vt(a)- prval pfmut = $UN.castview0{locked_v(l1)}(buf)- val () = mutex_unlock(pfmut | mut)- prval () = fold@(chan2)- prval () = $UN.cast2void(chan2) }--(* ****** ****** *)-implement {a} chanlst_takeout_buf (chan, buf_p) =- let- val chan2 = $UN.castvwtp0{chanlst_vt}(chan)- val+ @CHANLST_vt{ l1, l2 }(buf, mut, CVisnil) = chan2- val mut = mut- val CVisnil = CVisnil- prval () = fold@(chan2)- prval () = $UN.cast2void(chan2)- val xs0 = $UN.ptr1_get<List0_vt(a)>(aptr2ptr(buf_p))- in- case+ xs0 of- | ~list_vt_nil() => let- prval (pfmut, fpf) = __assert() where- { extern- praxi __assert() : vtakeout0(locked_v(l1)) }- val () = condvar_wait(pfmut | CVisnil, mut)- prval () = fpf(pfmut)- in- chanlst_takeout_buf<a>(chan, buf_p)- end- | ~list_vt_cons (x0_out, xs0) => x0_out where- { val () = $UN.ptr1_set<List0_vt(a)>(aptr2ptr(buf_p), xs0) }- end--(* ****** ****** *)-(* end of [chanlst_t.dats] *)
− test/data/channel_vt.dats
@@ -1,650 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)--(*-** Copyright (C) 2015-2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)--(* ****** ****** *)-//-// HX-2015-01:-// An array-based linear channel-//-(* ****** ****** *)-//-staload-UN =-"prelude/SATS/unsafe.sats"-//-(* ****** ****** *)-//-staload-"libats/SATS/athread.sats"-//-staload-"libats/SATS/deqarray.sats"-//-(* ****** ****** *)-//-staload "./../SATS/channel_vt.sats"-//-(* ****** ****** *)-//-absvtype-queue_vtype- (a:vt@ype+, int(*id*)) = ptr-//-vtypedef-queue(a:vt0p, id:int) = queue_vtype(a, id)-//-vtypedef queue(a:vt0p) = [id:int] queue(a, id)-//-(* ****** ****** *)-//-extern-fun-{a:vt0p}-queue_make(cap: sizeGt(0)): queue(a)-//-extern-fun-{a:t@ype}-queue_free_type(que: queue(a)): void-//-(* ****** ****** *)-//-absprop-ISNIL(id:int, b:bool)-absprop-ISFUL(id:int, b:bool)-//-(* ****** ****** *)-//-extern-fun-{a:vt0p}-queue_isnil- {id:int}-(- que: !queue(a, id)-) : [b:bool] (ISNIL(id, b) | bool(b))-extern-fun-{a:vt0p}-queue_isful- {id:int}-(- que: !queue(a, id)-) : [b:bool] (ISFUL(id, b) | bool(b))-//-(* ****** ****** *)-//-extern-fun-{a:vt0p}-queue_insert- {id:int}-(- pf: ISFUL(id, false)-| xs: !queue(a, id) >> queue(a, id2), x0: a-) : #[id2:int] void-//-extern-fun-{a:vt0p}-queue_takeout- {id:int}-(- pf: ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2)-) : #[id2:int] (a) // end of [queue_takeout]-//-(* ****** ****** *)--local-//-staload-"libats/SATS/deqarray.sats"-//-assume-queue_vtype- (a:vt0p, id:int) = deqarray(a)-//-assume ISNIL(id:int, b:bool) = unit_p-assume ISFUL(id:int, b:bool) = unit_p-//-in (* in-of-local *)--implement-{a}(*tmp*)-queue_make(cap) = deqarray_make_cap(cap)--implement-{a}(*tmp*)-queue_free_type(q0) =-deqarray_free_nil{a}-(- $UN.castvwtp0{deqarray(a,1,0)}(q0)-) // end of [queue_free_type]--implement-{a}(*tmp*)-queue_isnil(xs) =- (unit_p() | deqarray_is_nil{a}(xs))--implement-{a}(*tmp*)-queue_isful(xs) =- (unit_p() | deqarray_is_full<a>(xs))--implement-{a}(*tmp*)-queue_insert- (pf | xs, x0) =-{-//-prval () =-__assert(pf) where-{- extern- praxi- __assert- {id:int}- (- pf: ISFUL(id, false)- ) : [false] void-} (* end of [prval] *)-//-val () =- deqarray_insert_atend<a>(xs, x0)-//-} (* end of [queue_insert] *)--(* ****** ****** *)--implement-{a}(*tmp*)-queue_takeout- (pf | xs) = let-//-prval () =-__assert(pf) where-{- extern- praxi- __assert- {id:int}- (- pf: ISNIL(id, false)- ) : [false] void-} (* end of [prval] *)-//-in- deqarray_takeout_atbeg<a>(xs)-end (* end of [queue_takeout] *)--end // end of [local]--(* ****** ****** *)-//-datavtype-channel_ =-{-l0,l1,l2,l3:agz-} CHANNEL of-@{- cap=sizeGt(0)-, spin=spin_vt(l0)-, rfcnt=intGt(0)-, mutex=mutex_vt(l1)-, CVisnil=condvar_vt(l2)-, CVisful=condvar_vt(l3)-, queue=ptr // deqarray-} (* end of [channel] *)-//-(* ****** ****** *)-//-assume-channel_vtype(a:vt0p) = channel_-//-(* ****** ****** *)--implement-{a}(*tmp*)-channel_create_exn- (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.rfcnt := 1-//-local-val x = spin_create_exn()-in(*in-of-local*)-val () = ch.spin := unsafe_spin_t2vt(x)-end // end of [local]-//-local-val x = mutex_create_exn()-in(*in-of-local*)-val () = ch.mutex := unsafe_mutex_t2vt(x)-end // end of [local]-//-local-val x = condvar_create_exn()-in(*in-of-local*)-val () = ch.CVisnil := unsafe_condvar_t2vt(x)-end // end of [local]-//-local-val x = condvar_create_exn()-in(*in-of-local*)-val () = ch.CVisful := unsafe_condvar_t2vt(x)-end // end of [local]-//-val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))-//-in- fold@(chan); chan-end // end of [channel_create_exn]--(* ****** ****** *)--implement-{a}(*tmp*)-channel_ref- (chan) = let-//-val@CHANNEL(ch) = chan-//-val-spin =-unsafe_spin_vt2t(ch.spin)-//-val-(pf | ()) = spin_lock(spin)-val () = ch.rfcnt := ch.rfcnt + 1-val ((*void*)) = spin_unlock(pf | spin)-//-prval () = fold@(chan)-//-in- $UN.castvwtp1{channel(a)}(chan)-end // end of [channel_ref]--(* ****** ****** *)--implement-{a}(*tmp*)-channel_unref- (chan) = let-//-val-@CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val-spin =-unsafe_spin_vt2t(ch.spin)-//-val-(pf | ()) = spin_lock(spin)-val rfcnt = ch.rfcnt-val ((*void*)) = spin_unlock(pf | spin)-//-in (* in-of-let *)-//-if-(-rfcnt >= 2-)-then let- val () = ch.rfcnt := rfcnt - 1- prval ((*fold*)) = fold@(chan)- prval ((*freed*)) = $UN.cast2void(chan)-in- $UN.castvwtp0{queueopt(a)}(0)-end // end of [then]-else let- val que =- $UN.castvwtp0{queue(a)}(ch.queue)- // end of [val]- val ((*freed*)) = spin_vt_destroy(ch.spin)- val ((*freed*)) = mutex_vt_destroy(ch.mutex)- val ((*CVisnil*)) = condvar_vt_destroy(ch.CVisnil)- val ((*CVisful*)) = condvar_vt_destroy(ch.CVisful)- val ((*freed*)) = free@{l0,l1,l2,l3}(chan)-in- $UN.castvwtp0{queueopt(a)}(que)-end // end of [else]-//-end // end of [channel_unref]--(* ****** ****** *)--implement-{}(*tmp*)-channel_get_refcount- {a}(chan) = let-//-val@CHANNEL- {l0,l1,l2,l3}(ch) = chan-//-val rfcnt = ch.rfcnt-//-in- fold@(chan); rfcnt-end // end of [channel_get_refcount]--(* ****** ****** *)--local-//-extern-fun{a:vt0p}-channel_insert_buf- (!channel(a), !queue(a) >> _, a): void-//-in--(* ****** ****** *)--implement-{a}(*tmp*)-channel_insert- (chan, x0) = let-//-val+CHANNEL- {l0,l1,l2,l3}(ch) = chan-//-val-mutex = unsafe_mutex_vt2t(ch.mutex)-val (pfmut | ()) = mutex_lock(mutex)-//-val xs =- $UN.castvwtp0{queue(a)}((pfmut|ch.queue))-val () = channel_insert_buf<a>(chan, xs, x0)-//-prval-pfmut = $UN.castview0{locked_v(l1)}(xs)-val ((*void*)) = mutex_unlock(pfmut | mutex)-//-in- // nothing-end // end of [channel_insert]--(* ****** ****** *)--implement-{a}(*tmp*)-channel_insert_opt- (chan, x0) = opt where-{-//-val+-CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val-mutex = unsafe_mutex_vt2t(ch.mutex)-val (pfmut | ()) = mutex_lock(mutex)-//-val xs =- $UN.castvwtp0{queue(a)}((pfmut|ch.queue))-//-val (pf | isful) = queue_isful<a>(xs)-//-val opt =-(-if-isful-then Some_vt(x0)-else None_vt(*void*) where-{- val isnil =- queue_isnil<a>(xs)- val ((*void*)) =- queue_insert<a>(pf | xs, x0)- val ((*void*)) =- if isnil.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))- // end of [then] // end of [if]-}-) : Option_vt(a) // end of [val]-//-prval-pfmut = $UN.castview0{locked_v(l1)}(xs)-val ((*void*)) = mutex_unlock(pfmut | mutex)-//-} (* end of [channel_insert_opt] *)--(* ****** ****** *)--implement-{a}(*tmp*)-channel_insert_buf- (chan, xs, x0) = let-//-val+-CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val (pf | isful) = queue_isful<a>(xs)-//-in-//-if-isful-then let- prval- (pfmut, fpf) =- __assert((*void*)) where- {- extern- praxi- __assert- (- // argless- ) : vtakeout0(locked_v(l1))- }- val mutex =- unsafe_mutex_vt2t(ch.mutex)- val CVisful =- unsafe_condvar_vt2t(ch.CVisful)- val ((*void*)) =- condvar_wait(pfmut|CVisful,mutex)- prval ((* returned *)) = fpf(pfmut)-in- channel_insert_buf<a>(chan, xs, x0)-end // end of [then]-else let- val isnil =- queue_isnil<a>(xs)- val ((*void*)) =- queue_insert<a>(pf | xs, x0)- val ((*void*)) =- if isnil.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))- // end of [then] // end of [if]-in- // nothing-end // end of [else]-//-end // end of [channel_insert_buf]--end // end of [local]--(* ****** ****** *)--local-//-extern-fun{a:vt0p}-channel_takeout_buf- (chan: !channel(a), !queue(a) >> _): (a)-//-in (* in-of-local *)--(* ****** ****** *)--implement-{a}(*tmp*)-channel_takeout- (chan) = x0_out where-{-//-val+-CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val-mutex = unsafe_mutex_vt2t(ch.mutex)-val (pfmut | ()) = mutex_lock(mutex)-//-val xs =- $UN.castvwtp0{queue(a)}((pfmut|ch.queue))-//-val x0_out = channel_takeout_buf<a>(chan, xs)-//-prval-pfmut = $UN.castview0{locked_v(l1)}(xs)-val ((*void*)) = mutex_unlock(pfmut | mutex)-//-} // end of [channel_takeout_opt]--(* ****** ****** *)--implement-{a}(*tmp*)-channel_takeout_opt- (chan) = opt where-{-//-val+-CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val-mutex = unsafe_mutex_vt2t(ch.mutex)-val (pfmut | ()) = mutex_lock(mutex)-//-val xs =- $UN.castvwtp0{queue(a)}((pfmut|ch.queue))-//-val (pf | isnil) = queue_isnil<a>(xs)-//-val opt =-(-if-isnil-then None_vt()-else Some_vt(x0_out) where-{- val isful =- queue_isful<a>(xs)- val x0_out =- queue_takeout<a>(pf | xs)- val ((*void*)) =- if isful.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))- // end of [then] // end of [if]-} (* end of [else] *)-) : Option_vt(a) // end of [val]-//-prval pfmut =- $UN.castview0{locked_v(l1)}(xs)-//-val ((*void*)) = mutex_unlock(pfmut | mutex)-//-} // end of [channel_takeout_opt]--(* ****** ****** *)--implement-{a}(*tmp*)-channel_takeout_buf- (chan, xs) = let-//-val+-CHANNEL-{l0,l1,l2,l3}(ch) = chan-//-val (pf | isnil) = queue_isnil<a>(xs)-//-in-//-if-isnil-then let- prval- (pfmut, fpf) =- __assert((*void*)) where- {- extern- praxi- __assert- (- // argless- ) : vtakeout0(locked_v(l1))- }- val mutex =- unsafe_mutex_vt2t(ch.mutex)- val CVisnil =- unsafe_condvar_vt2t(ch.CVisnil)- val ((*void*)) =- condvar_wait(pfmut|CVisnil,mutex)- // end of [val]- prval ((* returned *)) = fpf (pfmut)-in- channel_takeout_buf<a>(chan, xs)-end // end of [then]-else let- val isful = queue_isful<a>(xs)- val x0_out = queue_takeout<a>(pf | xs)- val ((*void*)) =- if isful.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))- // end of [then] // end of [if]-in- x0_out-end // end of [else]-//-end // end of [channel_takeout_buf]--end // end of [local]--(* ****** ****** *)--(* end of [channel_vt.dats] *)
− test/data/channel_vt.out
@@ -1,362 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)-(*-** Copyright (C) 2015-2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)-(* ****** ****** *)-// HX-2015-01:-// An array-based linear channel-(* ****** ****** *)-staload UN = "prelude/SATS/unsafe.sats"--(* ****** ****** *)-staload "libats/SATS/athread.sats"-staload "libats/SATS/deqarray.sats"--(* ****** ****** *)-staload "./../SATS/channel_vt.sats"--(* ****** ****** *)-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)--(* ****** ****** *)-extern-fun {a:vt0p} queue_make (cap : sizeGt(0)) : queue(a)--extern-fun {a:t@ype} queue_free_type (que : queue(a)) : void--(* ****** ****** *)-absprop ISNIL (id : int, b : bool)--absprop ISFUL (id : int, b : bool)--(* ****** ****** *)-extern-fun {a:vt0p} queue_isnil {id:int} (que : !queue(a, id)) :- [b:bool] (ISNIL(id, b) | bool(b))--extern-fun {a:vt0p} queue_isful {id:int} (que : !queue(a, id)) :- [b:bool] (ISFUL(id, b) | bool(b))--(* ****** ****** *)-extern-fun {a:vt0p} queue_insert {id:int}-(pf : ISFUL(id, false) | xs : !queue(a, id) >> queue(a, id2), x0 : a) :- #[id2:int] void--extern-fun {a:vt0p} queue_takeout {id:int}-(pf : ISNIL(id, false) | xs : !queue(a, id) >> queue(a, id2)) :- #[id2:int] a--(* ****** ****** *)-local- assume ISFUL(id : int, b : bool) = unit_p- - assume ISNIL(id : int, b : bool) = unit_p- - assume queue_vtype(a : vt0p, id : int) = deqarray(a)- - staload "libats/SATS/deqarray.sats"-in- implement {a} queue_takeout (pf | xs) =- let- prval () = __assert(pf) where- { extern- praxi __assert {id:int} (pf : ISNIL(id, false)) : [ false ] void }- in- deqarray_takeout_atbeg<a>(xs)- end- - (* ****** ****** *)- implement {a} queue_insert (pf | xs, x0) =- {- prval () = __assert(pf) where- { extern- praxi __assert {id:int} (pf : ISFUL(id, false)) : [ false ] void }- val () = deqarray_insert_atend<a>(xs, x0)- }- - implement {a} queue_isful (xs) =- (unit_p() | deqarray_is_full<a>(xs))- - implement {a} queue_isnil (xs) =- (unit_p() | deqarray_is_nil{a}(xs))- - implement {a} queue_free_type (q0) =- deqarray_free_nil{a}($UN.castvwtp0{deqarray(a, 1, 0)}(q0))- - implement {a} queue_make (cap) =- deqarray_make_cap(cap)-end--(* ****** ****** *)-datavtype channel_ =- | { l0, l1, l2, l3 : agz } CHANNEL of @{ cap = sizeGt(0)- , spin = spin_vt(l0)- , rfcnt = intGt(0)- , mutex = mutex_vt(l1)- , CVisnil = condvar_vt(l2)- , CVisful = condvar_vt(l3)- , queue = ptr- }--(* ****** ****** *)-assume channel_vtype(a : vt0p) = channel_--(* ****** ****** *)-implement {a} channel_create_exn (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.rfcnt := 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.CVisful := unsafe_condvar_t2vt(x)- end- - val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))- in- (fold@(chan) ; chan)- end--(* ****** ****** *)-implement {a} channel_ref (chan) =- let- val @CHANNEL (ch) = chan- val spin = unsafe_spin_vt2t(ch.spin)- val (pf | ()) = spin_lock(spin)- val () = ch.rfcnt := ch.rfcnt + 1- val () = spin_unlock(pf | 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 (pf | ()) = spin_lock(spin)- val rfcnt = ch.rfcnt- val () = spin_unlock(pf | spin)- in- if (rfcnt >= 2) then- let- val () = ch.rfcnt := rfcnt - 1- prval () = fold@(chan)- prval () = $UN.cast2void(chan)- in- $UN.castvwtp0{queueopt(a)}(0)- end- else- 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.CVisful)- val () = free@{l0,l1,l2,l3}(chan)- in- $UN.castvwtp0{queueopt(a)}(que)- end- end--(* ****** ****** *)-implement channel_get_refcount {a} (chan) =- let- val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val rfcnt = ch.rfcnt- in- (fold@(chan) ; rfcnt)- end--(* ****** ****** *)-local- extern- fun {a:vt0p} channel_insert_buf (!channel(a), !queue(a) >> _, a) : void-in- implement {a} channel_insert_buf (chan, xs, x0) =- let- val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val (pf | isful) = queue_isful<a>(xs)- in- if isful then- let- prval (pfmut, fpf) = __assert() where- { extern- praxi __assert() : vtakeout0(locked_v(l1)) }- val mutex = unsafe_mutex_vt2t(ch.mutex)- val CVisful = unsafe_condvar_vt2t(ch.CVisful)- val () = condvar_wait(pfmut | CVisful, mutex)- prval () = fpf(pfmut)- in- channel_insert_buf<a>(chan, xs, x0)- end- else- let- val isnil = queue_isnil<a>(xs)- val () = queue_insert<a>(pf | xs, x0)- val () = if isnil.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))- in end- end- - (* ****** ****** *)- implement {a} channel_insert_opt (chan, x0) =- opt where- { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val mutex = unsafe_mutex_vt2t(ch.mutex)- val (pfmut | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))- val (pf | isful) = queue_isful<a>(xs)- val opt = (if isful then- Some_vt(x0)- else- None_vt where- { val isnil = queue_isnil<a>(xs)- val () = queue_insert<a>(pf | xs, x0)- val () = if isnil.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil)) }) : Option_vt(a)- prval pfmut = $UN.castview0{locked_v(l1)}(xs)- val () = mutex_unlock(pfmut | mutex) }- - (* ****** ****** *)- implement {a} channel_insert (chan, x0) =- let- val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val mutex = unsafe_mutex_vt2t(ch.mutex)- val (pfmut | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))- val () = channel_insert_buf<a>(chan, xs, x0)- prval pfmut = $UN.castview0{locked_v(l1)}(xs)- val () = mutex_unlock(pfmut | mutex)- in end- - (* ****** ****** *)-end--(* ****** ****** *)-local- extern- fun {a:vt0p} channel_takeout_buf (chan : !channel(a), !queue(a) >> _) :- a-in- implement {a} channel_takeout_buf (chan, xs) =- let- val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val (pf | isnil) = queue_isnil<a>(xs)- in- if isnil 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_takeout_buf<a>(chan, xs)- end- else- let- val isful = queue_isful<a>(xs)- val x0_out = queue_takeout<a>(pf | xs)- val () = if isful.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))- in- x0_out- end- end- - (* ****** ****** *)- implement {a} channel_takeout_opt (chan) =- opt where- { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val mutex = unsafe_mutex_vt2t(ch.mutex)- val (pfmut | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))- val (pf | isnil) = queue_isnil<a>(xs)- val opt = (if isnil then- None_vt()- else- Some_vt(x0_out) where- { val isful = queue_isful<a>(xs)- val x0_out = queue_takeout<a>(pf | xs)- val () = if isful.1 then- condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful)) }) : Option_vt(a)- prval pfmut = $UN.castview0{locked_v(l1)}(xs)- val () = mutex_unlock(pfmut | mutex) }- - (* ****** ****** *)- implement {a} channel_takeout (chan) =- x0_out where- { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan- val mutex = unsafe_mutex_vt2t(ch.mutex)- val (pfmut | ()) = mutex_lock(mutex)- val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))- val x0_out = channel_takeout_buf<a>(chan, xs)- prval pfmut = $UN.castview0{locked_v(l1)}(xs)- val () = mutex_unlock(pfmut | mutex) }- - (* ****** ****** *)-end--(* ****** ****** *)-(* end of [channel_vt.dats] *)
test/data/concurrency.out view
@@ -42,9 +42,7 @@ 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
− test/data/fworkshop.dats
@@ -1,467 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)--(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)--(* ****** ****** *)--(*-** HX-2017-02-07: Start it now!-*)--(* ****** ****** *)--(*-//-// HX-2017-02-11:-// It is supposed to be-// included rather than staloaded-//-#define-ATS_PACKNAME "ATSCNTRB.HX.fworkshop"-//-*)--(* ****** ****** *)-//-staload-UN =-"prelude/SATS/unsafe.sats"-//-(* ****** ****** *)-//-staload-AT =-"libats/SATS/athread.sats"-//-typedef tid = $AT.tid-typedef spin1 = $AT.spin1-//-(* ****** ****** *)-//-abstype-fws$store_type = ptr-typedef-fws$store = fws$store_type-//-(* ****** ****** *)-//-absvtype-fws$fwork_vtype = ptr-vtypedef-fws$fwork = fws$fwork_vtype-//-(* ****** ****** *)-//-extern-fun{}-fws$store_capacity- ((*void*)): intGte(1)-extern-fun{}-fws$store_insert- (fws$store, fws$fwork): void-extern-fun{}-fws$store_takeout- (store: fws$store): fws$fwork-//-extern-fun{}-fws$fwork_process(fws$fwork): int-//-(* ****** ****** *)-//-abstype-fworkshop_type = ptr-typedef-fworkshop = fworkshop_type-//-(* ****** ****** *)--vtypedef-fworkshop_struct =-@{-//-FWS_spin= spin1-//-,-FWS_store= fws$store-,-FWS_workerlst= List0_vt(tid)-//-} (* end of [fworkshop_struct] *)--(* ****** ****** *)-//-extern-fun{}-fworkshop_create_exn(): fworkshop-extern-fun{}-fws$store_create_exn(): fws$store-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_add_tid- (fws: fworkshop, tid): void-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_get_spin- (fws: fworkshop): spin1-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_get_store- (fws: fworkshop): fws$store-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_get_nworker- (fws: fworkshop): intGte(0)-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_insert_work-(- fws: fworkshop, fwork: fws$fwork-) : void // end-of-function-//-extern-fun{}-fworkshop_takeout_work- (fws: fworkshop): fws$fwork-extern-fun{}-fworkshop_process_work- (fws: fworkshop, fwork: fws$fwork): int-//-(* ****** ****** *)-//-extern-fun{}-fworkshop_add_worker- (fws: fworkshop): int(*err*)-extern-fun{}-fworkshop_add_nworker- {n:nat}- (fws: fworkshop, int(n)): natLte(n)-//-(* ****** ****** *)--local-//-assume-fworkshop_type = ref(fworkshop_struct)-//-in (* in-of-local *)--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_create_exn- ((*void*)) = let-//-val (-pf, fpf | p0-) = ptr_alloc<fworkshop_struct>()-//-val () =-p0->FWS_spin := $AT.spin_create_exn()-val () =-p0->FWS_store := fws$store_create_exn<>()-val () =-p0->FWS_workerlst := list_vt_nil((*void*))-//-in- $UN.castvwtp0{fworkshop}((pf, fpf | p0))-end // end of [fworkshop_create_exn]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_add_tid- (fws, tid) = let-//-val (- vbox pf | p0-) = ref_get_viewptr(fws)-//-val spn = p0->FWS_spin-val (- pflock | ()-) = $AT.spin_lock(spn)-val tids = p0->FWS_workerlst-val ((*void*)) =- p0->FWS_workerlst := list_vt_cons(tid, tids)-val ((*void*)) = $AT.spin_unlock(pflock | spn)-//-in- // nothing-end (* end of [fworkshop_add_tid] *)--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_get_spin- (fws) = let-//-val (- vbox pf | p0-) = ref_get_viewptr(fws) in p0->FWS_spin-//-end // end of [fworkshop_get_spin]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_get_store- (fws) = let-//-val (- vbox pf | p0-) = ref_get_viewptr(fws) in p0->FWS_store-//-end // end of [fworkshop_get_store]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_get_nworker- (fws) = let-//-val (- vbox pf | p0-) = ref_get_viewptr(fws)-//-val spn = p0->FWS_spin-val (- pflock | ()-) = $AT.spin_lock (spn)-val nworker =- list_vt_length(p0->FWS_workerlst)-val ((*void*)) = $AT.spin_unlock(pflock | spn)-//-in- nworker-end (* end of [fworkshop_get_nworker] *)--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_add_worker- (fws) = err where-{-//-fun-fworker-(- fws: fworkshop-) : void = let-//-val fwork =- fworkshop_takeout_work(fws)-val status =- fworkshop_process_work(fws, fwork)-//-in-//-if-(status >= 0)-then fworker(fws) else fworker_exit(fws)-//-end // end of [fworker]-//-and-fworker_exit-(- fws: fworkshop-) : void = let-//-val-tid0 = $AT.athread_self()-//-fun-auxrmv-(- tids: &List0_vt(tid) >> _-) : void =-(-case+ tids of-| list_vt_nil- () => ((*void*))- // list_vt_nil-| @list_vt_cons- (tid, tids_tl) =>- (- if (tid0 != tid)- then {- val () = auxrmv(tids_tl)- val ((*folded*)) = fold@(tids)- } (* then *)- else {- val tids_ = tids- val ((*void*)) = tids := tids_tl- val ((*freed*)) = free@{..}{0}(tids_)- } (* else *)- )-) (* end of [auxrmv] *)-//-val (- vbox pf | p0-) = ref_get_viewptr(fws)-//-val spn = p0->FWS_spin-val (- pflock | ()-) = $AT.spin_lock(spn)-val ((*void*)) =- $effmask_ref(auxrmv(p0->FWS_workerlst))-val ((*void*)) = $AT.spin_unlock(pflock | spn)-//-in- // nothing-end // end of [fworker_exit]-//-var tid: lint?-//-val err =-$AT.athread_create_cloptr<>- (tid, llam ((*void*)) => fworker(fws))-//-val-((*void*)) =-if (err = 0) then fworkshop_add_tid<>(fws, tid)-//-} // end of [fworkshop_add_worker]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_add_nworker- {n}(fws, n) =- loop(0, 0) where-{ -//-fun-loop-{i:nat | i <= n}-(- i: int(i), res: natLte(i)-) : natLte(n) = let-in-//-if-i < n-then let-//-val-err = fworkshop_add_worker<>(fws)-//-in-//-if err = 0- then loop(i + 1, res + 1) else res-// end of [if]-//-end // end of [then]-else res // end of [else]-//-end // end of [loop]-//-} (* end of [fworkshop_add_nworker] *)--(* ****** ****** *)--end // end of [local]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_insert_work- (fws, x0) = let-//-val-store =-fworkshop_get_store<>(fws)-// end of [val]-in- fws$store_insert<>(store, x0)-end // end of [fworkshop_insert_work]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_takeout_work- (fws) = let-//-val-store =-fworkshop_get_store<>(fws)-// end of [val]-in- fws$store_takeout<>(store)-end // end of [fworkshop_takeout_work]--(* ****** ****** *)--implement-{}(*tmp*)-fworkshop_process_work-(- fws, fwork-) = status where-{-//-val-status = fws$fwork_process<>(fwork)-//-} // end of [fworkshop_process_work]--(* ****** ****** *)--(* end of [fworkshop.dats] *)
− test/data/fworkshop.out
@@ -1,270 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)-(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)-(* ****** ****** *)-(*-** HX-2017-02-07: Start it now!-*)-(* ****** ****** *)-(*-//-// HX-2017-02-11:-// It is supposed to be-// included rather than staloaded-//-#define-ATS_PACKNAME "ATSCNTRB.HX.fworkshop"-//-*)-(* ****** ****** *)-staload UN = "prelude/SATS/unsafe.sats"--(* ****** ****** *)-staload AT = "libats/SATS/athread.sats"--typedef tid = $AT.tid-typedef spin1 = $AT.spin1--(* ****** ****** *)-abstype fws$store_type() = ptr--typedef fws$store = fws$store_type--(* ****** ****** *)-absvtype fws$fwork_vtype() = ptr--vtypedef fws$fwork = fws$fwork_vtype--(* ****** ****** *)-extern-fun fws$store_capacity() : intGte(1)--extern-fun fws$store_insert(fws$store, fws$fwork) : void--extern-fun fws$store_takeout(store : fws$store) : fws$fwork--extern-fun fws$fwork_process(fws$fwork) : int--(* ****** ****** *)-abstype fworkshop_type() = ptr--typedef fworkshop = fworkshop_type--(* ****** ****** *)-vtypedef fworkshop_struct = @{ FWS_spin = spin1- , FWS_store = fws$store- , FWS_workerlst = List0_vt(tid)- }--(* ****** ****** *)-extern-fun fworkshop_create_exn() : fworkshop--extern-fun fws$store_create_exn() : fws$store--(* ****** ****** *)-extern-fun fworkshop_add_tid(fws : fworkshop, tid) : void--(* ****** ****** *)-extern-fun fworkshop_get_spin(fws : fworkshop) : spin1--(* ****** ****** *)-extern-fun fworkshop_get_store(fws : fworkshop) : fws$store--(* ****** ****** *)-extern-fun fworkshop_get_nworker(fws : fworkshop) : intGte(0)--(* ****** ****** *)-extern-fun fworkshop_insert_work(fws : fworkshop, fwork : fws$fwork) : void--extern-fun fworkshop_takeout_work(fws : fworkshop) : fws$fwork--extern-fun fworkshop_process_work(fws : fworkshop, fwork : fws$fwork) : int--(* ****** ****** *)-extern-fun fworkshop_add_worker(fws : fworkshop) : int--extern-fun fworkshop_add_nworker {n:nat} (fws : fworkshop, int(n)) : natLte(n)--(* ****** ****** *)-local- assume fworkshop_type() = ref(fworkshop_struct)-in- (* ****** ****** *)- implement fworkshop_add_nworker {n} (fws, n) =- loop(0, 0) where- { fun loop { i : nat | i <= n } (i : int(i), res : natLte(i)) :- natLte(n) =- let- - in- if i < n then- let- val err = fworkshop_add_worker{}(fws)- in- if err = 0 then- loop(i + 1, res + 1)- else- res- end- else- res- end }- - (* ****** ****** *)- implement fworkshop_add_worker (fws) =- err where- { fun fworker(fws : fworkshop) : void =- let- val fwork = fworkshop_takeout_work(fws)- val status = fworkshop_process_work(fws, fwork)- in- if (status >= 0) then- fworker(fws)- else- fworker_exit(fws)- end- - and fworker_exit(fws : fworkshop) : void =- let- val tid0 = $AT.athread_self()- - fun auxrmv(tids : &List0_vt(tid) >> _) : void =- (case+ tids of- | list_vt_nil() => ()- | @list_vt_cons (tid, tids_tl) => (if (tid0 != tid) then- {- val () = auxrmv(tids_tl)- val () = fold@(tids)- }- else- {- val tids_ = tids- val () = tids := tids_tl- val () = free@{..,0}(tids_)- }))- - val (vbox pf | p0) = ref_get_viewptr(fws)- val spn = p0->FWS_spin- val (pflock | ()) = $AT.spin_lock(spn)- val () = $effmask_ref(auxrmv(p0->FWS_workerlst))- val () = $AT.spin_unlock(pflock | spn)- in end- - var tid: lint? with - val err = $AT.athread_create_cloptr{}(tid, llam () => fworker(fws))- val () = if (err = 0) then- fworkshop_add_tid{}(fws, tid) }- - (* ****** ****** *)- implement fworkshop_get_nworker (fws) =- let- val (vbox pf | p0) = ref_get_viewptr(fws)- val spn = p0->FWS_spin- val (pflock | ()) = $AT.spin_lock(spn)- val nworker = list_vt_length(p0->FWS_workerlst)- val () = $AT.spin_unlock(pflock | spn)- in- nworker- end- - (* ****** ****** *)- implement fworkshop_get_store (fws) =- let- val (vbox pf | p0) = ref_get_viewptr(fws)- in- p0->FWS_store- end- - (* ****** ****** *)- implement fworkshop_get_spin (fws) =- let- val (vbox pf | p0) = ref_get_viewptr(fws)- in- p0->FWS_spin- end- - (* ****** ****** *)- implement fworkshop_add_tid (fws, tid) =- let- val (vbox pf | p0) = ref_get_viewptr(fws)- val spn = p0->FWS_spin- val (pflock | ()) = $AT.spin_lock(spn)- val tids = p0->FWS_workerlst- val () = p0->FWS_workerlst := list_vt_cons(tid, tids)- val () = $AT.spin_unlock(pflock | spn)- in end- - (* ****** ****** *)- implement fworkshop_create_exn () =- let- val (pf, fpf | p0) = ptr_alloc<fworkshop_struct>()- val () = p0->FWS_spin := $AT.spin_create_exn()- val () = p0->FWS_store := fws$store_create_exn{}(())- val () = p0->FWS_workerlst := list_vt_nil()- in- $UN.castvwtp0{fworkshop}((p0, fpf, pf))- end- - (* ****** ****** *)-end--(* ****** ****** *)-implement fworkshop_insert_work (fws, x0) =- let- val store = fworkshop_get_store{}(fws)- in- fws$store_insert{}(store, x0)- end--(* ****** ****** *)-implement fworkshop_takeout_work (fws) =- let- val store = fworkshop_get_store{}(fws)- in- fws$store_takeout{}(store)- end--(* ****** ****** *)-implement fworkshop_process_work (fws, fwork) =- status where- { val status = fws$fwork_process{}(fwork) }--(* ****** ****** *)-(* end of [fworkshop.dats] *)
− test/data/fworkshop_channel.dats
@@ -1,174 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)--(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)--(* ****** ****** *)-//-// HX-2017-02-11:-//-// A fworkshop where:-//-// fws$store = channel-// fws$fwork = lincloptr-//-(* ****** ****** *)--#define-ATS_PACKNAME-"ATSCNTRB.HX.fworkshop_channel"-#define-ATS_DYNLOADFLAG 0 // no dynloading--(* ****** ****** *)--#include "./fworkshop.dats"--(* ****** ****** *)-//-extern-fun{}-fworkshop_insert_lincloptr-(- fws: fworkshop, fwork: () -<lincloptr1> int-) : void // end-of-function-//-(* ****** ****** *)--local-//-#include-"./../mydepies.hats"-#staload $CHANNEL_t // opening it-//-assume-fws$store_type = channel(fws$fwork)-//-vtypedef fwork = fws$fwork-//-in (* in-of-local *)-//-(*-extern-fun{}-fws$store_create_exn(): fws$store-*)-//-implement-{}(*tmp*)-fws$store_create_exn- ((*void*)) = let-//-val cap =- i2sz(fws$store_capacity<>())-//-in- channel_create_exn<fwork>(cap)-end // end of [fws$store_create_exn]-//-(*extern-fun{}-fws$store_insert- (fws$store, fws$fwork): void-*)-implement-{}(*tmp*)-fws$store_insert- (store, fwork) = let-//-val-opt =-channel_insert_opt<fwork>- (store, fwork)-//-in-//-case+ opt of-| ~None_vt() => ()-| ~Some_vt(fwork) => () where- {- val status = fws$fwork_process<>(fwork)- } (* end of [Some_vt] *)-//-end // end of [fws$store_insert]-//-(*-extern-fun{}-fws$store_takeout- (store: fws$store): fws$fwork-*)-implement-{}(*tmp*)-fws$store_takeout- (store) = channel_takeout<fwork>(store)-//-end // end of [local]--(* ****** ****** *)--local--assume-fws$fwork_vtype = () -<lincloptr1> int--in (* in-of-local *)-//-(*-extern-fun{}-fws$fwork_process(fws$fwork): int-*)-implement-{}(*tmp*)-fws$fwork_process-(- fwork-) = status where-{-//-val-status = fwork()-//-val () =-cloptr_free-(-$UN.castvwtp0{cloptr(void)}(fwork)-) (* cloptr_free *)-//-} // end of [fws$fwork_process]-//-implement-{}(*tmp*)-fworkshop_insert_lincloptr- (fws, fwork) =- fworkshop_insert_work<>(fws, fwork)-//-end // end of [local]--(* ****** ****** *)--(* end of [fworkshop_channel.dats] *)
− test/data/fworkshop_channel.out
@@ -1,114 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)-(*-** Copyright (C) 2017 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)-(* ****** ****** *)-// HX-2017-02-11:-// A fworkshop where:-// fws$store = channel-// fws$fwork = lincloptr-(* ****** ****** *)-#define ATS_PACKNAME"ATSCNTRB.HX.fworkshop_channel"--#define ATS_DYNLOADFLAG 0--(* ****** ****** *)-#include "./fworkshop.dats"--(* ****** ****** *)-extern-fun fworkshop_insert_lincloptr( fws : fworkshop- , fwork : () -<lincloptr1> int- ) : void--(* ****** ****** *)-local- vtypedef fwork = fws$fwork- - assume fws$store_type() = channel(fws$fwork)- - #staload $CHANNEL_t- - #include "./../mydepies.hats"-in- implement fws$store_takeout (store) =- channel_takeout<fwork>(store)- - (*- extern- fun{}- fws$store_takeout- (store: fws$store): fws$fwork- *)- implement fws$store_insert (store, fwork) =- let- val opt = channel_insert_opt<fwork>(store, fwork)- in- case+ opt of- | ~None_vt() => ()- | ~Some_vt (fwork) => () where- { val status = fws$fwork_process{}(fwork) }- end- - (*extern- fun{}- fws$store_insert- (fws$store, fws$fwork): void- *)- implement fws$store_create_exn () =- let- val cap = i2sz(fws$store_capacity{}(()))- in- channel_create_exn<fwork>(cap)- end- - (*- extern- fun{}- fws$store_create_exn(): fws$store- *)-end--(* ****** ****** *)-local- assume fws$fwork_vtype() = () -<lincloptr1> int-in- implement fworkshop_insert_lincloptr (fws, fwork) =- fworkshop_insert_work{}(fws, fwork)- - implement fws$fwork_process (fwork) =- status where- { val status = fwork()- val () = cloptr_free($UN.castvwtp0{cloptr(void)}(fwork)) }- - (*- extern- fun{}- fws$fwork_process(fws$fwork): int- *)-end--(* ****** ****** *)-(* end of [fworkshop_channel.dats] *)
− test/data/mylibies.out
@@ -1,1 +0,0 @@-
− test/data/nwaiter.dats
@@ -1,197 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)--(*-** Copyright (C) 2014 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)--(* ****** ****** *)-//-// HX-2014-05:-// For waiting until the proofs for-// a predeterminted view are all uploaded-// in a piecewise manner.-// Note that this version does not use types-// to ensure a correct match between the uploaded-// proofs and the downloaded proof.-//-(* ****** ****** *)-//-staload-UN =-"prelude/SATS/unsafe.sats"-//-(* ****** ****** *)-//-staload-"libats/SATS/athread.sats"-//-(* ****** ****** *)--staload "./../SATS/nwaiter.sats"--(* ****** ****** *)-//-datavtype-nwaiter() =-{l1,l2:agz}-NWAITER of-(- int, spin(l1), mutex(l2)-) (* nwaiter *)-//-(* ****** ****** *)--assume-nwaiter_vtype(i) = nwaiter()--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_create_exn- ((*void*)) = let-//-val spn = spin_create_exn()-val mtx = mutex_create_exn()-//-in- NWAITER(0(*n*), spn, mtx)-end // end of [nwaiter_create_exn]--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_destroy- (nw) = () where-{-//-val+~NWAITER(n, spn, mtx) = nw-//-val spn = unsafe_spin_t2vt(spn)-val ((*freed*)) = spin_vt_destroy(spn)--val mtx = unsafe_mutex_t2vt(mtx)-val ((*freed*)) = mutex_vt_destroy(mtx)-//-} (* end of [nwaiter_destroy] *)--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_initiate(nw) = let-//-val+-@NWAITER(n, spn, mtx) = nw-//-val () = n := 1-//-val (pf | ()) = mutex_lock(mtx)-prval ((*void*)) = $UN.castview0(pf)-//-prval ((*void*)) = fold@(nw)-//-in- $UN.castvwtp1{nwaiter_ticket}(nw)-end // end of [nwaiter_initiate]--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_waitfor(nw) = let-//-val+NWAITER(n, spn, mtx) = nw-//-val (pf | ()) = mutex_lock (mtx)-val ((*void*)) = mutex_unlock (pf | mtx)-//-in- // nothing-end // end of [nwaiter_waitfor]--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_ticket_put- (nwt) = () where-{-(*-val () =-println!("nwaiter_ticket_put")-*)-val nw =-$UN.castvwtp0{nwaiter(1)}(nwt)-val+@NWAITER (n, spn, mtx) = nw-//-val (pf | ()) = spin_lock(spn)-val () = n := n - 1-val ((*void*)) = spin_unlock(pf | spn)-(*-val () = println! ("nwaiter_ticket_put(aft): n = ", n)-*)-val () =-if (0 >= n) then let- prval pf =- __assert (mtx) where- {- extern- praxi __assert {l:addr} (!mutex(l)): locked_v(l)- } (* end of [prval] *)-in- mutex_unlock (pf | mtx)-end else () // end of [if]-//-prval () = fold@(nw)-prval () = $UN.castview0{void}(nw)-//-} (* end of [nwaiter_ticket_put] *)--(* ****** ****** *)--implement-{}(*tmp*)-nwaiter_ticket_split- (nwt) = let-//-val nw =-$UN.castvwtp1{nwaiter(1)}(nwt)-val+@NWAITER (n, spn, mtx) = nw-//-val (pf | ()) = spin_lock(spn)-val () = n := n + 1-val ((*void*)) = spin_unlock(pf | spn)-//-prval ((*folded*)) = fold@(nw)-//-in- $UN.castvwtp0{nwaiter_ticket}(nw)-end // end of [nwaiter_ticket_split]--(* ****** ****** *)--(* end of [nwaiter.dats] *)
− test/data/nwaiter.out
@@ -1,132 +0,0 @@-(***********************************************************************)-(* *)-(* ATS/contrib/libats-hwxi *)-(* *)-(***********************************************************************)-(*-** Copyright (C) 2014 Hongwei Xi, ATS Trustful Software, Inc.-**-** Permission is hereby granted, free of charge, to any person obtaining a-** copy of this software and associated documentation files (the "Software"),-** to deal in the Software without restriction, including without limitation-** the rights to use, copy, modify, merge, publish, distribute, sublicense,-** and/or sell copies of the Software, and to permit persons to whom the-** Software is furnished to do so, subject to the following stated conditions:-** -** The above copyright notice and this permission notice shall be included in-** all copies or substantial portions of the Software.-** -** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS-** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL-** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING-** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS-** IN THE SOFTWARE.-*)-(* ****** ****** *)-// HX-2014-05:-// For waiting until the proofs for-// a predeterminted view are all uploaded-// in a piecewise manner.-// Note that this version does not use types-// to ensure a correct match between the uploaded-// proofs and the downloaded proof.-(* ****** ****** *)-staload UN = "prelude/SATS/unsafe.sats"--(* ****** ****** *)-staload "libats/SATS/athread.sats"--(* ****** ****** *)-staload "./../SATS/nwaiter.sats"--(* ****** ****** *)-datavtype nwaiter =- | { l1, l2 : agz } NWAITER of (int, spin(l1), mutex(l2))--(* ****** ****** *)-assume nwaiter_vtype(i) = nwaiter()--(* ****** ****** *)-implement nwaiter_create_exn () =- let- val spn = spin_create_exn()- val mtx = mutex_create_exn()- in- NWAITER(0, spn, mtx)- end--(* ****** ****** *)-implement nwaiter_destroy (nw) =- () where- { val+ ~NWAITER (n, spn, mtx) = nw- val spn = unsafe_spin_t2vt(spn)- val () = spin_vt_destroy(spn)- val mtx = unsafe_mutex_t2vt(mtx)- val () = mutex_vt_destroy(mtx) }--(* ****** ****** *)-implement nwaiter_initiate (nw) =- let- val+ @NWAITER (n, spn, mtx) = nw- val () = n := 1- val (pf | ()) = mutex_lock(mtx)- prval () = $UN.castview0(pf)- prval () = fold@(nw)- in- $UN.castvwtp1{nwaiter_ticket}(nw)- end--(* ****** ****** *)-implement nwaiter_waitfor (nw) =- let- val+ NWAITER (n, spn, mtx) = nw- val (pf | ()) = mutex_lock(mtx)- val () = mutex_unlock(pf | mtx)- in end--(* ****** ****** *)-implement nwaiter_ticket_put (nwt) =- () where- { (*- val () =- println!("nwaiter_ticket_put")- *)- val nw = $UN.castvwtp0{nwaiter(1)}(nwt)- val+ @NWAITER (n, spn, mtx) = nw- val (pf | ()) = spin_lock(spn)- val () = n := n - 1- val () = spin_unlock(pf | spn)- - (*- val () = println! ("nwaiter_ticket_put(aft): n = ", n)- *)- val () = if (0 >= n) then- let- prval pf = __assert((mtx) where- { extern- praxi __assert {l:addr} (!mutex(l)) : locked_v(l) })- in- mutex_unlock(pf | mtx)- end- else- ()- prval () = fold@(nw)- prval () = $UN.castview0{void}(nw) }--(* ****** ****** *)-implement nwaiter_ticket_split (nwt) =- let- val nw = $UN.castvwtp1{nwaiter(1)}(nwt)- val+ @NWAITER (n, spn, mtx) = nw- val (pf | ()) = spin_lock(spn)- val () = n := n + 1- val () = spin_unlock(pf | spn)- prval () = fold@(nw)- in- $UN.castvwtp0{nwaiter_ticket}(nw)- end--(* ****** ****** *)-(* end of [nwaiter.dats] *)