diff --git a/libs/contrib/Data/Bool/Decidable.idr b/libs/base/Data/Bool/Decidable.idr similarity index 100% rename from libs/contrib/Data/Bool/Decidable.idr rename to libs/base/Data/Bool/Decidable.idr diff --git a/libs/contrib/Data/List/AtIndex.idr b/libs/base/Data/List/AtIndex.idr similarity index 83% rename from libs/contrib/Data/List/AtIndex.idr rename to libs/base/Data/List/AtIndex.idr index ee8cf6c7b..508913147 100644 --- a/libs/contrib/Data/List/AtIndex.idr +++ b/libs/base/Data/List/AtIndex.idr @@ -1,3 +1,10 @@ +||| Indexing into Lists. +||| +||| `Elem` proofs give existential quantification that a given element +||| *is* in the list, but not where in the list it is! Here we give a +||| predicate that presents proof that a given index in a list, given +||| by a natural number, will return a certain element. + module Data.List.AtIndex import Data.DPair @@ -51,25 +58,6 @@ find x (y :: xs) with (decEq x y) (Element Z p) => void (neqxy (inverseZ p)) (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf))) -||| If the equality is not decidable, we may instead rely on interface resolution -public export -interface Member (0 t : a) (0 ts : List a) where - isMember' : Subset Nat (AtIndex t ts) - -public export -isMember : (0 t : a) -> (0 ts : List a) -> Member t ts => - Subset Nat (AtIndex t ts) -isMember t ts @{p} = isMember' @{p} - -public export -Member t (t :: ts) where - isMember' = Element 0 Z - -public export -Member t ts => Member t (u :: ts) where - isMember' = let (Element n prf) = isMember t ts in - Element (S n) (S prf) - ||| Given an index, we can decide whether there is a value corresponding to it public export lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n)) @@ -86,18 +74,22 @@ inRange n [] p = void (absurd p) inRange Z (x :: xs) p = LTEZero inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p)) -||| +||| An index remains unchanged if we extend the list to the right export weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n weakenR Z = Z weakenR (S p) = S (weakenR p) +||| An index into `xs` is shifted by `m` if we prepend a list of size `m` +||| in front of it export weakenL : (p : Subset Nat (flip HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n) weakenL m p with (view m) weakenL (Element 0 Z) p | Z = p weakenL (Element (S (fst m)) (S (snd m))) p | (S m) = S (weakenL m p) +||| Conversely to `weakenR`, if an index is smaller than the length of +||| a prefix then it points into that prefix. export strengthenL : (p : Subset Nat (flip HasLength xs)) -> lt n (fst p) === True -> @@ -106,6 +98,8 @@ strengthenL m lt idx with (view m) strengthenL (Element (S (fst m)) (S (snd m))) lt Z | (S m) = Z strengthenL (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = S (strengthenL m lt k) +||| Conversely to `weakenL`, if an index is larger than the length of +||| a prefix then it points into the suffix. export strengthenR : (p : Subset Nat (flip HasLength ws)) -> lte (fst p) n === True -> @@ -113,4 +107,3 @@ strengthenR : (p : Subset Nat (flip HasLength ws)) -> strengthenR m lt idx with (view m) strengthenR (Element 0 Z) lt idx | Z = rewrite minusZeroRight n in idx strengthenR (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = strengthenR m lt k - diff --git a/libs/contrib/Data/Nat/Order/Properties.idr b/libs/base/Data/Nat/Order/Properties.idr similarity index 100% rename from libs/contrib/Data/Nat/Order/Properties.idr rename to libs/base/Data/Nat/Order/Properties.idr diff --git a/libs/papers/Data/OpenUnion.idr b/libs/base/Data/OpenUnion.idr similarity index 60% rename from libs/papers/Data/OpenUnion.idr rename to libs/base/Data/OpenUnion.idr index d955626f6..5cac3f12a 100644 --- a/libs/papers/Data/OpenUnion.idr +++ b/libs/base/Data/OpenUnion.idr @@ -2,8 +2,8 @@ ||| Freer Monads, More Extensible Effects ||| by Oleg Kiselyov and Hiromi Ishii ||| -||| By using an AtIndex proof, we are able to get rid of all of the unsafe -||| coercions in the original module. +||| By using an AtIndex proof, we are able to get rid of all of +||| the unsafe coercions in the original module. module Data.OpenUnion @@ -17,49 +17,47 @@ import Syntax.WithProof %default total -||| An open union of families is an index picking a family out together with -||| a value in the family thus picked. +||| An open union transformer takes +||| @ts a list of type descriptions +||| @elt a method to turn descriptions into types +||| and returns a union of the types described in the list. +||| Elements are given by an index selecting a value in the list +||| together with a value of the appropriately decoded type. public export -data Union : (elt : a -> Type) -> (ts : List a) -> Type where - Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts +data UnionT : (elt : a -> Type) -> (ts : List a) -> Type where + Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts + +||| A union of types is obtained by taking the union transformer +||| where the decoding function is the identity. +public export +Union : List Type -> Type +Union = UnionT Prelude.id ||| An empty open union of families is empty public export -Uninhabited (Union elt []) where +Uninhabited (UnionT elt []) where uninhabited (Element _ p _) = void (uninhabited p) ||| Injecting a value into an open union, provided we know the index of ||| the appropriate type family. -inj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts -inj' = Element +export +inj : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts +inj = Element ||| Projecting out of an open union, provided we know the index of the ||| appropriate type family. This may obviously fail if the value stored ||| actually corresponds to another family. -prj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> Union elt ts -> Maybe (elt t) -prj' k p (Element k' q t) with (decEq k k') - prj' k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t - prj' k p (Element k' q t) | No neq = Nothing - -||| Given that equality of type families is not decidable, we have to -||| rely on the interface `Member` to automatically find the index of a -||| given family. -public export -inj : Member t ts => elt t -> Union elt ts -inj = let (Element n p) = isMember t ts in inj' n p - -||| Given that equality of type families is not decidable, we have to -||| rely on the interface `Member` to automatically find the index of a -||| given family. -public export -prj : Member t ts => Union elt ts -> Maybe (elt t) -prj = let (Element n p) = isMember t ts in prj' n p +export +prj : (k : Nat) -> (0 _ : AtIndex t ts k) -> UnionT elt ts -> Maybe (elt t) +prj k p (Element k' q t) with (decEq k k') + prj k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t + prj k p (Element k' q t) | No neq = Nothing ||| By doing a bit of arithmetic we can figure out whether the union's value ||| came from the left or the right list used in the index. public export split : Subset Nat (flip HasLength ss) -> - Union elt (ss ++ ts) -> Either (Union elt ss) (Union elt ts) + UnionT elt (ss ++ ts) -> Either (UnionT elt ss) (UnionT elt ts) split m (Element n p t) with (@@ lt n (fst m)) split m (Element n p t) | (True ** lt) = Left (Element n (strengthenL m lt p) t) @@ -72,25 +70,25 @@ split m (Element n p t) with (@@ lt n (fst m)) ||| whether the value it contains belongs either to the first family or any ||| other in the tail. public export -decomp : Union elt (t :: ts) -> Either (Union elt ts) (elt t) +decomp : UnionT elt (t :: ts) -> Either (UnionT elt ts) (elt t) decomp (Element 0 (Z) t) = Right t decomp (Element (S n) (S p) t) = Left (Element n p t) ||| An open union over a singleton list is just a wrapper public export -decomp0 : Union elt [t] -> elt t +decomp0 : UnionT elt [t] -> elt t decomp0 elt = case decomp elt of Left t => absurd t Right t => t ||| Inserting new union members on the right leaves the index unchanged. public export -weakenR : Union elt ts -> Union elt (ts ++ us) +weakenR : UnionT elt ts -> UnionT elt (ts ++ us) weakenR (Element n p t) = Element n (weakenR p) t ||| Inserting new union members on the left, requires shifting the index by ||| the number of members introduced. Note that this number is the only ||| thing we need to keep around at runtime. public export -weakenL : Subset Nat (flip HasLength ss) -> Union elt ts -> Union elt (ss ++ ts) +weakenL : Subset Nat (flip HasLength ss) -> UnionT elt ts -> UnionT elt (ss ++ ts) weakenL m (Element n p t) = Element (fst m + n) (weakenL m p) t diff --git a/libs/contrib/Data/Void.idr b/libs/base/Data/Void.idr similarity index 100% rename from libs/contrib/Data/Void.idr rename to libs/base/Data/Void.idr diff --git a/libs/contrib/Syntax/WithProof.idr b/libs/base/Syntax/WithProof.idr similarity index 100% rename from libs/contrib/Syntax/WithProof.idr rename to libs/base/Syntax/WithProof.idr diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 603d6c6c5..7ef7dd840 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -38,6 +38,7 @@ modules = Control.App, Data.Bifoldable, Data.Bits, Data.Bool, + Data.Bool.Decidable, Data.Bool.Xor, Data.Buffer, Data.Colist, @@ -55,6 +56,7 @@ modules = Control.App, Data.IORef, Data.Integral, Data.List, + Data.List.AtIndex, Data.List.Elem, Data.List.HasLength, Data.List.Lazy, @@ -69,7 +71,9 @@ modules = Control.App, Data.Morphisms, Data.Nat, Data.Nat.Order, + Data.Nat.Order.Properties, Data.Nat.Views, + Data.OpenUnion, Data.Primitives.Interpolation, Data.Primitives.Views, Data.Ref, @@ -91,6 +95,7 @@ modules = Control.App, Data.Vect.AtIndex, Data.Vect.Elem, Data.Vect.Quantifiers, + Data.Void, Data.Zippable, Debug.Trace, @@ -112,6 +117,7 @@ modules = Control.App, Syntax.PreorderReasoning, Syntax.PreorderReasoning.Ops, Syntax.PreorderReasoning.Generic, + Syntax.WithProof, System, System.Clock, diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 627d59fdc..b02d1dee9 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -24,7 +24,6 @@ modules = Control.ANSI, Data.Binary, Data.Bool.Algebra, - Data.Bool.Decidable, Data.Fin.Extra, @@ -48,7 +47,6 @@ modules = Control.ANSI, Data.List.Reverse, Data.List.Views.Extra, Data.List.Palindrome, - Data.List.AtIndex, Data.List.Alternating, Data.List.Sufficient, @@ -69,7 +67,6 @@ modules = Control.ANSI, Data.Nat.Factor, Data.Nat.Fib, Data.Nat.Order.Strict, - Data.Nat.Order.Properties, Data.Nat.Order.Relation, Data.Nat.Properties, @@ -111,8 +108,6 @@ modules = Control.ANSI, Data.Vect.Sort, Data.Vect.Views.Extra, - Data.Void, - Debug.Buffer, Decidable.Finite.Fin, @@ -129,8 +124,6 @@ modules = Control.ANSI, Language.JSON.String.Tokens, Language.JSON.Tokens, - Syntax.WithProof, - System.Console.GetOpt, System.Directory.Tree, System.Future, diff --git a/libs/linear/Control/Linear/LIO.idr b/libs/linear/Control/Linear/LIO.idr index 30488381f..92301befd 100644 --- a/libs/linear/Control/Linear/LIO.idr +++ b/libs/linear/Control/Linear/LIO.idr @@ -1,10 +1,13 @@ module Control.Linear.LIO +import public Data.Linear.Notation +import System + ||| Like `Monad`, but the action and continuation must be run exactly once ||| to ensure that the computation is linear. public export interface LinearBind io where - bindL : (1 _ : io a) -> (1 _ : a -> io b) -> io b + bindL : io a -@ (a -> io b) -@ io b export LinearBind IO where @@ -71,7 +74,7 @@ RunCont Unrestricted t b = t -> b -- concrete type of the continuation is. runK : {use : _} -> LinearBind io => - (1 _ : L io {use} a) -> (1 _ : RunCont use a (io b)) -> io b + L io {use} a -@ RunCont use a (io b) -@ io b runK (Pure0 x) k = k x runK (Pure1 x) k = k x runK (PureW x) k = k x @@ -86,7 +89,7 @@ runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k) ||| underlying context export run : Applicative io => LinearBind io => - (1 _ : L io a) -> io a + L io a -@ io a run prog = runK prog pure export @@ -110,12 +113,12 @@ export export %inline (>>=) : {u_act : _} -> LinearBind io => - (1 _ : L io {use=u_act} a) -> - (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b + L io {use=u_act} a -@ + ContType io u_act u_k a b -@ L io {use=u_k} b (>>=) = Bind export -delay : {u_act : _} -> (1 _ : L io {use=u_k} b) -> ContType io u_act u_k () b +delay : {u_act : _} -> L io {use=u_k} b -@ ContType io u_act u_k () b delay mb = case u_act of None => \ _ => mb Linear => \ () => mb @@ -124,8 +127,8 @@ delay mb = case u_act of export %inline (>>) : {u_act : _} -> LinearBind io => - (1 _ : L io {use=u_act} ()) -> - (1 _ : L io {use=u_k} b) -> L io {use=u_k} b + L io {use=u_act} () -@ + L io {use=u_k} b -@ L io {use=u_k} b ma >> mb = ma >>= delay mb export %inline @@ -133,9 +136,16 @@ pure0 : (0 x : a) -> L io {use=0} a pure0 = Pure0 export %inline -pure1 : (1 x : a) -> L io {use=1} a +pure1 : a -@ L io {use=1} a pure1 = Pure1 +||| Shuffling around linearity annotations: a computation of an +||| unrestricted value can be seen as a computation of a linear +||| value that happens to be unrestricted. +export %inline +bang : L IO t -@ L1 IO (!* t) +bang io = io >>= \ a => pure1 (MkBang a) + export (LinearBind io, HasLinearIO io) => HasLinearIO (L io) where liftIO1 p = Action (liftIO1 p) @@ -143,3 +153,10 @@ export public export LinearIO : (Type -> Type) -> Type LinearIO io = (LinearBind io, HasLinearIO io) + +||| Linear version of `die` +export +die1 : LinearIO io => String -> L1 io a +die1 err = do + x <- die err + pure1 x diff --git a/libs/linear/System/Concurrency/Linear.idr b/libs/linear/System/Concurrency/Linear.idr new file mode 100644 index 000000000..41520287b --- /dev/null +++ b/libs/linear/System/Concurrency/Linear.idr @@ -0,0 +1,33 @@ +module System.Concurrency.Linear + +import Control.Linear.LIO +import System.Concurrency + +||| Run two linear computations in parallel and return the results. +export +par1 : L1 IO a -@ L1 IO b -@ L1 IO (LPair a b) +par1 x y + = do aChan <- makeChannel + bChan <- makeChannel + aId <- liftIO1 $ fork $ withChannel aChan x + bId <- liftIO1 $ fork $ withChannel bChan y + a <- channelGet aChan + b <- channelGet bChan + pure1 (a # b) + + where + + -- This unsafe implementation temporarily bypasses the linearity checker. + -- However `par`'s implementation does not duplicate the values + -- and the type of `par` ensures that client code is not allowed to either! + withChannel : Channel t -> L1 IO t -@ IO () + withChannel ch = assert_linear $ \ act => do + a <- LIO.run (act >>= assert_linear pure) + channelPut ch a + +||| Run two unrestricted computations in parallel and return the results. +export +par : L IO a -@ L IO b -@ L IO (a, b) +par x y = do + (MkBang a # MkBang b) <- par1 (bang x) (bang y) + pure (a, b) diff --git a/libs/linear/System/Concurrency/Session.idr b/libs/linear/System/Concurrency/Session.idr new file mode 100644 index 000000000..dcf95592e --- /dev/null +++ b/libs/linear/System/Concurrency/Session.idr @@ -0,0 +1,218 @@ +module System.Concurrency.Session + +import Control.Linear.LIO + +import Data.List.AtIndex +import Data.Nat + +import Data.OpenUnion +import System +import System.File +import System.Concurrency as Threads +import System.Concurrency.Linear + +import Language.Reflection + +%default total + +------------------------------------------------------------------------ +-- Session types + +namespace Session + + ||| A session type describes the interactions one thread may have with + ||| another over a shared bidirectional channel: it may send or receive + ||| values of arbitrary types, or be done communicating. + public export + data Session : Type where + Send : (ty : Type) -> (s : Session) -> Session + Recv : (ty : Type) -> (s : Session) -> Session + End : Session + + ||| Dual describes how the other party to the communication sees the + ||| interactions: our sends become their receives and vice-versa. + public export + Dual : Session -> Session + Dual (Send ty s) = Recv ty (Dual s) + Dual (Recv ty s) = Send ty (Dual s) + Dual End = End + + ||| Duality is involutive: the dual of my dual is me + export + dualInvolutive : (s : Session) -> Dual (Dual s) === s + dualInvolutive (Send ty s) = cong (Send ty) (dualInvolutive s) + dualInvolutive (Recv ty s) = cong (Recv ty) (dualInvolutive s) + dualInvolutive End = Refl + +||| We can collect the list of types that will be sent over the +||| course of a session by walking down its description +||| This definition is purely internal and will not show up in +||| the library's interface. +SendTypes : Session -> List Type +SendTypes (Send ty s) = ty :: SendTypes s +SendTypes (Recv ty s) = SendTypes s +SendTypes End = [] + +||| We can collect the list of types that will be received over +||| the course of a session by walking down its description +||| This definition is purely internal and will not show up in +||| the library's interface. +RecvTypes : Session -> List Type +RecvTypes (Send ty s) = RecvTypes s +RecvTypes (Recv ty s) = ty :: RecvTypes s +RecvTypes End = [] + +||| The types received by my dual are exactly the ones I am sending +||| This definition is purely internal and will not show up in +||| the library's interface. +RecvDualTypes : (s : Session) -> RecvTypes (Dual s) === SendTypes s +RecvDualTypes (Send ty s) = cong (ty ::) (RecvDualTypes s) +RecvDualTypes (Recv ty s) = RecvDualTypes s +RecvDualTypes End = Refl + +||| The types sent by my dual are exactly the ones I receive +||| This definition is purely internal and will not show up in +||| the library's interface. +SendDualTypes : (s : Session) -> SendTypes (Dual s) === RecvTypes s +SendDualTypes (Send ty s) = SendDualTypes s +SendDualTypes (Recv ty s) = cong (ty ::) (SendDualTypes s) +SendDualTypes End = Refl + +namespace Seen + + ||| The inductive family (Seen m n f) states that the function `f` + ||| was obtained by composing an interleaving of `m` receiving + ||| steps and `n` sending ones. + public export + data Seen : Nat -> Nat -> (Session -> Session) -> Type where + None : Seen 0 0 Prelude.id + Recv : (ty : Type) -> Seen m n f -> Seen (S m) n (f . Recv ty) + Send : (ty : Type) -> Seen m n f -> Seen m (S n) (f . Send ty) + +||| If we know that `ty` is at index `n` in the list of received types +||| and that `f` is a function defined using an interleaving of steps +||| comprising `m` receiving stepsx then `ty` is at index `m + n` in `f s`. +atRecvIndex : Seen m _ f -> + (s : Session) -> + AtIndex ty (RecvTypes s) n -> + AtIndex ty (RecvTypes (f s)) (m + n) +atRecvIndex None accS accAt = accAt +atRecvIndex (Recv ty s) accS accAt + = rewrite plusSuccRightSucc (pred m) n in + atRecvIndex s (Recv ty accS) (S accAt) +atRecvIndex (Send ty s) accS accAt + = atRecvIndex s (Send ty accS) accAt + +||| If we know that `ty` is at index `n` in the list of sent types +||| and that `f` is a function defined using an interleaving of steps +||| comprising `m` sending steps then `ty` is at index `m + n` in `f s`. +atSendIndex : Seen _ m f -> + (s : Session) -> + AtIndex ty (SendTypes s) n -> + AtIndex ty (SendTypes (f s)) (m + n) +atSendIndex None accS accAt = accAt +atSendIndex (Recv ty s) accS accAt + = atSendIndex s (Recv ty accS) accAt +atSendIndex (Send ty s) accS accAt + = rewrite plusSuccRightSucc (pred m) n in + atSendIndex s (Send ty accS) (S accAt) + + +||| A (bidirectional) channel is parametrised by a session it must respect. +||| +||| It is implemented in terms of two low-level channels: one for sending +||| and one for receiving. This ensures that we never are in a situation +||| where a thread with session (Send Nat (Recv String ...)) sends a natural +||| number and subsequently performs a receive before the other party +||| to the communication had time to grab the Nat thus receiving it +||| instead of a String. +||| +||| The low-level channels can only carry values of a single type. And so +||| they are given respective union types corresponding to the types that +||| can be sent on the one hand and the ones that can be received on the +||| other. +||| These union types are tagged unions where if `ty` is at index `k` in +||| the list of types `tys` then `(k, v)` is a value of `Union tys` provided +||| that `v` has type `ty`. +||| +||| `sendStep`, `recvStep`, `seePrefix`, and `seen` encode the fact that +||| we have already performed some of the protocol and so the low-level +||| channels' respective types necessarily mention types that we won't +||| see anymore. +export +record Channel (s : Session) where + constructor MkChannel + {sendStep : Nat} + {recvStep : Nat} + {0 seenPrefix : Session -> Session} + 0 seen : Seen recvStep sendStep seenPrefix + + sendChan : Threads.Channel (Union (SendTypes (seenPrefix s))) + recvChan : Threads.Channel (Union (RecvTypes (seenPrefix s))) + +||| Consume a linear channel with a `Recv ty` step at the head of the +||| session type in order to obtain a value of type `ty` together with +||| a linear channel for the rest of the session. +export +recv : LinearIO io => + Channel (Recv ty s) -@ + L1 io (Res ty (const (Channel s))) +recv (MkChannel {recvStep} seen sendCh recvCh) = do + x@(Element k prf val) <- channelGet recvCh + -- Here we check that we got the right message by projecting out of + -- the union type using the current `recvStep`. Both ends should be + -- in sync because of the `RecvDualTypes` and `SendDualTypes` lemmas. + let Just val = prj (recvStep + 0) (atRecvIndex seen (Recv ty s) Z) x + | Nothing => die1 "Error: invalid recv expected \{show recvStep} but got \{show k}" + pure1 (val # MkChannel (Recv ty seen) sendCh recvCh) + + +||| Consume a linear channel with a `Send ty` step at the head of the +||| session type in order to send a value of type `ty` and obtain a +||| linear channel for the rest of the session. +export +send : LinearIO io => + (1 _ : Channel (Send ty s)) -> + ty -> + L1 io (Channel s) +send (MkChannel {sendStep} seen sendCh recvCh) x = do + let val = inj (sendStep + 0) (atSendIndex seen (Send ty s) Z) x + channelPut sendCh val + pure1 (MkChannel (Send ty seen) sendCh recvCh) + +||| Discard the channel provided that the session has reached its `End`. +export +end : LinearIO io => Channel End -@ L io () +end (MkChannel _ _ _) = do + pure () + +||| Given a session, create a bidirectional communiaction channel and +||| return its two endpoints +export +makeChannel : + LinearIO io => + (0 s : Session) -> + L1 io (LPair (Channel s) (Channel (Dual s))) +makeChannel s = do + sendChan <- Threads.makeChannel + recvChan <- Threads.makeChannel + let 1 posCh : Channel s + := MkChannel None sendChan recvChan + let 1 negCh : Channel (Dual s) + := MkChannel None + (rewrite SendDualTypes s in recvChan) + (rewrite RecvDualTypes s in sendChan) + pure1 (posCh # negCh) + +||| Given a session and two functions communicating according to that +||| sesion, we can run the two programs concurrently and collect their +||| final results. +export +fork : (0 s : Session) -> + (Channel s -@ L IO a) -@ + (Channel (Dual s) -@ L IO b) -@ + L IO (a, b) +fork s kA kB = do + let 1 io = makeChannel s + (posCh # negCh) <- io + par (kA posCh) (kB negCh) diff --git a/libs/linear/linear.ipkg b/libs/linear/linear.ipkg index cd7cbe5f2..311910e10 100644 --- a/libs/linear/linear.ipkg +++ b/libs/linear/linear.ipkg @@ -15,4 +15,7 @@ modules = Control.Linear.LIO, Data.Linear.LMaybe, Data.Linear.LNat, Data.Linear.LVect, - Data.Linear.Notation + Data.Linear.Notation, + + System.Concurrency.Linear, + System.Concurrency.Session diff --git a/libs/papers/papers.ipkg b/libs/papers/papers.ipkg index 9cc5d3130..b0f4c1e2e 100644 --- a/libs/papers/papers.ipkg +++ b/libs/papers/papers.ipkg @@ -24,8 +24,6 @@ modules = Control.DivideAndConquer, Data.Linear.Diff, Data.Linear.Inverse, - Data.OpenUnion, - Data.ProofDelay, Data.Recursion.Free, diff --git a/tests/Main.idr b/tests/Main.idr index 44c46caef..6d36a6347 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -192,6 +192,10 @@ baseLibraryTests = testsInDir "base" "Base library" {requirements = [Chez, Node] contribLibraryTests : IO TestPool contribLibraryTests = testsInDir "contrib" "Contrib library" {requirements = [Chez, Node]} +-- same behavior as `baseLibraryTests` +linearLibraryTests : IO TestPool +linearLibraryTests = testsInDir "linear" "Linear library" {requirements = [Chez, Node]} + codegenTests : IO TestPool codegenTests = testsInDir "codegen" "Code generation" @@ -227,6 +231,7 @@ main = runner $ , !ideModeTests , !preludeTests , !baseLibraryTests + , !linearLibraryTests , !contribLibraryTests , !chezTests , !refcTests diff --git a/tests/linear/system_concurrency_session/Main.idr b/tests/linear/system_concurrency_session/Main.idr new file mode 100644 index 000000000..1e4f99435 --- /dev/null +++ b/tests/linear/system_concurrency_session/Main.idr @@ -0,0 +1,28 @@ +import Control.Linear.LIO +import System.Concurrency.Session + +main : IO () +main = LIO.run $ do + let nm1 : String := "natrando" + let nm2 : String := "computer" + putStrLn "main: Forking two threads \{nm1} and \{nm2}" + res <- fork (Send Nat $ Send Nat $ Recv Nat End) + (\ ch => do let m : Nat := 100 + putStrLn "\{nm1}: picked the natural \{show m}" + ch <- send ch m + let n : Nat := 50 + putStrLn "\{nm1}: picked the natural \{show n}" + ch <- send ch n + (s # ch) <- recv ch + end ch + pure (m, n)) + (\ ch => do (m # ch) <- recv ch + (n # ch) <- recv ch + putStrLn "\{nm2}: summing \{show m} and \{show n}" + let s = m + n + ch <- send ch s + end ch + pure s) + let mn = fst res + let mplusn = snd res + putStrLn {io = L IO} "main: Threads have finished and returned \{show mn} and \{show mplusn}" diff --git a/tests/linear/system_concurrency_session/expected b/tests/linear/system_concurrency_session/expected new file mode 100644 index 000000000..172e46213 --- /dev/null +++ b/tests/linear/system_concurrency_session/expected @@ -0,0 +1,5 @@ +main: Forking two threads natrando and computer +natrando: picked the natural 100 +natrando: picked the natural 50 +computer: summing 100 and 50 +main: Threads have finished and returned (100, 50) and 150 diff --git a/tests/linear/system_concurrency_session/run b/tests/linear/system_concurrency_session/run new file mode 100755 index 000000000..5d2267bbc --- /dev/null +++ b/tests/linear/system_concurrency_session/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +run -p linear Main.idr