diff --git a/language-ats.cabal b/language-ats.cabal --- a/language-ats.cabal +++ b/language-ats.cabal @@ -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 diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x --- a/src/Language/ATS/Lexer.x +++ b/src/Language/ATS/Lexer.x @@ -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 = (\*+ [^\)] | [^\*] \)) diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y --- a/src/Language/ATS/Parser.y +++ b/src/Language/ATS/Parser.y @@ -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 } diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs --- a/src/Language/ATS/PrettyPrint.hs +++ b/src/Language/ATS/PrettyPrint.hs @@ -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 diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs --- a/src/Language/ATS/Types.hs +++ b/src/Language/ATS/Types.hs @@ -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: , 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 diff --git a/test/data/DivideConquerPar.dats b/test/data/DivideConquerPar.dats deleted file mode 100644 --- a/test/data/DivideConquerPar.dats +++ /dev/null @@ -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 = () - 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(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(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 - (x, env) = - let val () = (x := x - 1) in env := x end -// -in -// -let val () = - spinref_process_env(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 - (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 - ( - 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(n0), res) - prval ((*void*)) = $UN.cast2void(rs) -// - in - // nothing - end // end of [n0 >= 2] -// -end // end of [DivideConquer_cont$conquer] - -(* ****** ****** *) - -(* end of [DivideConquerPar.dats] *) diff --git a/test/data/DivideConquerPar.out b/test/data/DivideConquerPar.out deleted file mode 100644 --- a/test/data/DivideConquerPar.out +++ /dev/null @@ -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 = () - 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(addr@res, r0) - val NWT = $UN.castvwtp0{nwaiter_ticket}(NWT) } - ) - val () = nwaiter_waitfor(NW) - val () = nwaiter_destroy(NW) - in - $UN.ptr0_get(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( 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(n0), res) - prval () = $UN.cast2void(rs) - in end - end - -(* ****** ****** *) -(* end of [DivideConquerPar.dats] *) diff --git a/test/data/chanlst_t.dats b/test/data/chanlst_t.dats deleted file mode 100644 --- a/test/data/chanlst_t.dats +++ /dev/null @@ -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(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(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(chan, buf_p) - end // end of [list_vt_nil] -| ~list_vt_cons(x0_out, xs0) => x0_out where - { - val () = - $UN.ptr1_set(aptr2ptr(buf_p), xs0) - } -// -end // end of [chanlst_takeout_buf] - -(* ****** ****** *) - -(* end of [chanlst_t.dats] *) diff --git a/test/data/chanlst_t.out b/test/data/chanlst_t.out deleted file mode 100644 --- a/test/data/chanlst_t.out +++ /dev/null @@ -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(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(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(chan, buf_p) - end - | ~list_vt_cons (x0_out, xs0) => x0_out where - { val () = $UN.ptr1_set(aptr2ptr(buf_p), xs0) } - end - -(* ****** ****** *) -(* end of [chanlst_t.dats] *) diff --git a/test/data/channel_vt.dats b/test/data/channel_vt.dats deleted file mode 100644 --- a/test/data/channel_vt.dats +++ /dev/null @@ -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(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(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(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(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(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(xs) -// -val opt = -( -if -isful -then Some_vt(x0) -else None_vt(*void*) where -{ - val isnil = - queue_isnil(xs) - val ((*void*)) = - queue_insert(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(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(chan, xs, x0) -end // end of [then] -else let - val isnil = - queue_isnil(xs) - val ((*void*)) = - queue_insert(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(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(xs) -// -val opt = -( -if -isnil -then None_vt() -else Some_vt(x0_out) where -{ - val isful = - queue_isful(xs) - val x0_out = - queue_takeout(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(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(chan, xs) -end // end of [then] -else let - val isful = queue_isful(xs) - val x0_out = queue_takeout(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] *) diff --git a/test/data/channel_vt.out b/test/data/channel_vt.out deleted file mode 100644 --- a/test/data/channel_vt.out +++ /dev/null @@ -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(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(xs, x0) - } - - implement {a} queue_isful (xs) = - (unit_p() | deqarray_is_full(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(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(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(chan, xs, x0) - end - else - let - val isnil = queue_isnil(xs) - val () = queue_insert(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(xs) - val opt = (if isful then - Some_vt(x0) - else - None_vt where - { val isnil = queue_isnil(xs) - val () = queue_insert(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(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(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(chan, xs) - end - else - let - val isful = queue_isful(xs) - val x0_out = queue_takeout(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(xs) - val opt = (if isnil then - None_vt() - else - Some_vt(x0_out) where - { val isful = queue_isful(xs) - val x0_out = queue_takeout(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(chan, xs) - prval pfmut = $UN.castview0{locked_v(l1)}(xs) - val () = mutex_unlock(pfmut | mutex) } - - (* ****** ****** *) -end - -(* ****** ****** *) -(* end of [channel_vt.dats] *) diff --git a/test/data/concurrency.out b/test/data/concurrency.out --- a/test/data/concurrency.out +++ b/test/data/concurrency.out @@ -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 diff --git a/test/data/fworkshop.dats b/test/data/fworkshop.dats deleted file mode 100644 --- a/test/data/fworkshop.dats +++ /dev/null @@ -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() -// -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] *) diff --git a/test/data/fworkshop.out b/test/data/fworkshop.out deleted file mode 100644 --- a/test/data/fworkshop.out +++ /dev/null @@ -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() - 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] *) diff --git a/test/data/fworkshop_channel.dats b/test/data/fworkshop_channel.dats deleted file mode 100644 --- a/test/data/fworkshop_channel.dats +++ /dev/null @@ -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: () - 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(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 - (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(store) -// -end // end of [local] - -(* ****** ****** *) - -local - -assume -fws$fwork_vtype = () - 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] *) diff --git a/test/data/fworkshop_channel.out b/test/data/fworkshop_channel.out deleted file mode 100644 --- a/test/data/fworkshop_channel.out +++ /dev/null @@ -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 : () - 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(store) - - (* - extern - fun{} - fws$store_takeout - (store: fws$store): fws$fwork - *) - implement fws$store_insert (store, fwork) = - let - val opt = channel_insert_opt(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(cap) - end - - (* - extern - fun{} - fws$store_create_exn(): fws$store - *) -end - -(* ****** ****** *) -local - assume fws$fwork_vtype() = () - 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] *) diff --git a/test/data/mylibies.out b/test/data/mylibies.out deleted file mode 100644 --- a/test/data/mylibies.out +++ /dev/null @@ -1,1 +0,0 @@ - diff --git a/test/data/nwaiter.dats b/test/data/nwaiter.dats deleted file mode 100644 --- a/test/data/nwaiter.dats +++ /dev/null @@ -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] *) diff --git a/test/data/nwaiter.out b/test/data/nwaiter.out deleted file mode 100644 --- a/test/data/nwaiter.out +++ /dev/null @@ -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] *)