Issue#4: Multisided new take one

Ling.cf

@@ -97,7 +97,7 @@ PDot.     Proc ::= Proc1 "." Proc ;
 _.        Proc ::= Proc1 ;
 separator Proc "|" ;
 
-Nu.       Act ::= "new" "(" ChanDec "," ChanDec ")" ;
+Nu.       Act ::= "new" "(" [ChanDec] ")" ;
 ParSplit. Act ::= Name "{" [ChanDec] "}" ;
 TenSplit. Act ::= Name "[" [ChanDec] "]" ;
 SeqSplit. Act ::= Name "[:" [ChanDec] ":]" ;

Ling/Abs.hs

@@ -72,7 +72,7 @@ data Proc
   deriving (Eq, Ord, Show, Read)
 
 data Act
-    = Nu ChanDec ChanDec
+    = Nu [ChanDec]
     | ParSplit Name [ChanDec]
     | TenSplit Name [ChanDec]
     | SeqSplit Name [ChanDec]

Ling/Check/Base.hs

@@ -118,25 +118,19 @@ checkEqSessions c s0 s1 =
     "Given session (expanded):" (pure s0)
     "Inferred session:"         (pure s1)
 
--- checkUnused c ms s: Check if the channel c is used given the inferred session ms, and its dual
--- ds.
-checkUnused :: (MonadError TCErr m, Print channel)
-            => channel -> Maybe RSession -> RSession -> m ()
-checkUnused _ (Just _) _ = return ()
-checkUnused c Nothing  s = assert (endRS `is` s) ["Unused channel " ++ pretty c]
-
 checkOneR :: MonadError TCErr m => RFactor -> m ()
 checkOneR r = assert (r == ø) ["Unexpected replication:", pretty r]
 
-checkDual :: MonadTC m => RSession -> RSession -> m ()
-checkDual (Repl s0 r0) (Repl s1 r1) = do
+checkDual :: MonadTC m => [RSession] -> m ()
+checkDual [Repl s0 r0, Repl s1 r1] = do
   checkOneR r0
   checkOneR r1
   (b, us0, us1) <- isEquiv (pure s0) (pure (dual s1))
   assertDiff
     "Sessions are not dual." (\_ _ -> b)
     "Given session (expanded):" us0
     "Inferred dual session:"    (dual us1)
+checkDual _ = error "checkDual"
 
 checkSlice :: (Print channel, MonadError TCErr m) => (channel -> Bool) -> channel -> RSession -> m ()
 checkSlice cond c (s `Repl` r) = when (cond c) $ do

Ling/Check/Core.hs

@@ -15,16 +15,19 @@ import           Ling.Session
 import           Ling.Prelude         hiding (subst1)
 import           Prelude              hiding (log)
 
--- The first session is the potential annotation.
--- The second session is inferred or absent.
-checkOptSession :: Print channel => channel -> Maybe RSession -> Maybe RSession -> TC ()
-checkOptSession c ms0 ms1 =
+-- The protocol is the result of inferrence.
+-- The channel has a potential session annotation.
+checkChanDec :: Proto -> ChanDec -> TC RSession
+checkChanDec proto (Arg c ms0) = do
   case ms0 of
     Nothing -> return ()
     Just s0 ->
       case ms1 of
-        Nothing -> checkUnused c Nothing s0
+        Nothing -> assert (endRS `is` s0) ["Unused channel " ++ pretty c]
         Just s1 -> errorScope c (checkRSession s0) >> checkEqSessions c s0 s1
+  return $ ms1 ^. endedRS
+
+  where ms1 = proto ^. chanSession c
 
 checkProc :: Proc -> TC Proto
 checkProc (pref `Dot` procs) = do
@@ -67,10 +70,6 @@ checkPref pref proto
 checkProcs :: [Proc] -> TC Proto
 checkProcs procs = mconcat <$> traverse checkProc procs
 
-checkChanDec :: Proto -> ChanDec -> TC RSession
-checkChanDec proto (Arg c s) = checkOptSession c s s' $> s' ^. endedRS
-  where s' = proto ^. chanSession c
-
 checkRFactor :: RFactor -> TC ()
 checkRFactor (RFactor t) = checkTerm intTyp t
 
@@ -124,23 +123,20 @@ checkAct act proto =
               [ "Inferred protocol for the whole process:"
               ] ++ prettyError prettyProto proto') $
   case act of
-    Nu (Arg c cOS) (Arg d dOS) -> do
-      let ds = [c,d]
-          [cSession,dSession] = chanSessions ds proto
-          cNSession = cSession ^. endedRS
-          dNSession = dSession ^. endedRS
-      checkUnused c cSession dNSession
-      checkUnused d dSession cNSession
-      checkOptSession c cOS cSession
-      checkOptSession d dOS dSession
-      checkDual cNSession dNSession
+    Nu cds -> do
+      let cs = cds ^.. each . argName
+          csNSession = [ proto ^. chanSession c . endedRS | Arg c _ <- cds ]
+      unless (all (is endRS) csNSession) $
+        for_ cs $ assertUsed proto
+      for_ cds $ checkChanDec proto
+      checkDual csNSession
       -- This rmChans is potentially partly redundant.
-      -- We might `assert` that `ds` is no longer in the `skel`
-      rmChans ds <$> checkConflictingChans proto Nothing ds
+      -- We might `assert` that `cs` is no longer in the `skel`
+      rmChans cs <$> checkConflictingChans proto Nothing cs
     Split k c dOSs -> do
-      assertAbsent c proto
+      assertAbsent proto c
       let ds         = dOSs ^.. each . argName
-          dsSessions = chanSessions ds proto ^.. each . endedRS
+          dsSessions = ds & each %~ \d -> proto ^. chanSession d . endedRS
           s          = array k dsSessions
       for_ dOSs $ checkChanDec proto
       proto' <-

Ling/Compile/C.hs

@@ -263,14 +263,16 @@ transProcs = concatMap . transProc
 transAct :: Env -> Act -> (Env, Endom [C.Stm])
 transAct env act =
   case act of
-    Nu (Arg c0 c0OS) (Arg c1 c1OS) ->
+    Nu cds ->
       (env', (sDec typ cid C.NoInit ++))
       where
-        s    = log $ extractSession [c0OS, c1OS]
-        cid  = transName c0
+        cs   = cds ^.. each . argName
+        cOSs = cds ^.. each . argBody
+        s    = log $ extractSession cOSs
+        cid  = transName (cs ^?! _head)
         l    = C.LVar cid
         typ  = transRSession env s
-        env' = addChans [(c0,l),(c1,l)] env
+        env' = addChans [(c,l) | c <- cs] env
     Split _ c ds ->
       (transSplit c ds env, id)
     Send c expr ->

Ling/Defs.hs

@@ -90,7 +90,7 @@ instance PushDefs Act where
       Split k c ds    -> Split k c $ mkLet__ (sa $> ds)
       Send c e        -> Send c $ mkLet_ id (sa $> e)
       Recv c arg      -> Recv c $ mkLet_ varDecTerms (sa $> arg)
-      Nu c d          -> _Nu # mkLet__ (sa $> (c, d))
+      Nu cs           -> Nu $ mkLet__ (sa $> cs)
       NewSlice cs t x -> NewSlice cs (mkLet__ (sa $> t)) x
       LetA{}          -> error "`let` is not supported in parallel actions (pushDefs)"
       Ax s cs         -> _Ax # mkLet_ (subTerms `beside` ignored) (sa $> (s, cs))

Ling/Doc.txt

@@ -127,7 +127,7 @@ All other symbols are terminals.
   | //[Proc]// | -> | **eps**
   |  |  **|**  | //Proc// 
   |  |  **|**  | //Proc// ``|`` //[Proc]// 
-  | //Act// | -> | ``new`` ``(`` //ChanDec// ``,`` //ChanDec// ``)`` 
+  | //Act// | -> | ``new`` ``(`` //[ChanDec]// ``)`` 
   |  |  **|**  | //Name// ``{`` //[ChanDec]// ``}`` 
   |  |  **|**  | //Name// ``[`` //[ChanDec]// ``]`` 
   |  |  **|**  | //Name// ``[:`` //[ChanDec]// ``:]`` 

Ling/Equiv.hs

@@ -198,8 +198,8 @@ instance Equiv Act where
     (Recv c0 _b0, Recv c1 _b1) -> c0 == c1
     (Send c0 t0, Send c1 t1) -> c0 == c1 && equiv env t0 t1
     (At t0 p0, At t1 p1) -> equiv env t0 t1 && p0 == p1
-    (Nu cd0 cd0', Nu cd1 cd1') ->
-       on (==) (both %~ _argName) (cd0, cd0') (cd1, cd1')
+    (Nu cds0, Nu cds1) ->
+       on (==) (each %~ _argName) cds0 cds1
     (Split k0 c0 cds0, Split k1 c1 cds1) ->
        (k0, c0) == (k1, c1) && on (==) (_argName <$>) cds0 cds1
     (NewSlice cs0 r0 _x0, NewSlice cs1 r1 _x1) ->

Ling/Fmt/Albert.cf

@@ -103,7 +103,7 @@ PDot.     Proc ::= Proc1 "." Proc ;
 _.        Proc ::= Proc1 ;
 separator Proc "|" ;
 
-Nu.       Act ::= "new" "(" ChanDec "," ChanDec ")" ;
+Nu.       Act ::= "new" "(" [ChanDec] ")" ;
 ParSplit. Act ::= Name "{" [ChanDec] "}" ;
 TenSplit. Act ::= Name "[" [ChanDec] "]" ;
 SeqSplit. Act ::= Name "[:" [ChanDec] ":]" ;

Ling/Fmt/Albert/Abs.hs

@@ -79,7 +79,7 @@ data Proc
   deriving (Eq, Ord, Show, Read)
 
 data Act
-    = Nu ChanDec ChanDec
+    = Nu [ChanDec]
     | ParSplit Name [ChanDec]
     | TenSplit Name [ChanDec]
     | SeqSplit Name [ChanDec]

Ling/Fmt/Albert/Doc.txt

@@ -132,7 +132,7 @@ All other symbols are terminals.
   | //[Proc]// | -> | **eps**
   |  |  **|**  | //Proc// 
   |  |  **|**  | //Proc// ``|`` //[Proc]// 
-  | //Act// | -> | ``new`` ``(`` //ChanDec// ``,`` //ChanDec// ``)`` 
+  | //Act// | -> | ``new`` ``(`` //[ChanDec]// ``)`` 
   |  |  **|**  | //Name// ``{`` //[ChanDec]// ``}`` 
   |  |  **|**  | //Name// ``[`` //[ChanDec]// ``]`` 
   |  |  **|**  | //Name// ``[:`` //[ChanDec]// ``:]`` 

Ling/Fmt/Albert/Lex.x

@@ -9,6 +9,7 @@ module Ling.Fmt.Albert.Lex where
 
 import qualified Data.Bits
 import Data.Word (Word8)
+import Data.Char (ord)
 }
 
 

Ling/Fmt/Albert/Migrate.hs

@@ -94,7 +94,7 @@ transProc = \case
 
 transAct :: Act -> L.Act
 transAct = \case
-  Nu chandec1 chandec2 -> L.Nu (transChanDec chandec1) (transChanDec chandec2)
+  Nu chandecs -> L.Nu (transChanDec <$> chandecs)
   ParSplit name chandecs -> L.ParSplit (transName name) (transChanDec <$> chandecs)
   TenSplit name chandecs -> L.TenSplit (transName name) (transChanDec <$> chandecs)
   SeqSplit name chandecs -> L.SeqSplit (transName name) (transChanDec <$> chandecs)

Ling/Fmt/Albert/Par.y

@@ -196,7 +196,7 @@ ListProc : {- empty -} { [] }
          | Proc { (:[]) $1 }
          | Proc '|' ListProc { (:) $1 $3 }
 Act :: { Act }
-Act : 'new' '(' ChanDec ',' ChanDec ')' { Ling.Fmt.Albert.Abs.Nu $3 $5 }
+Act : 'new' '(' ListChanDec ')' { Ling.Fmt.Albert.Abs.Nu $3 }
     | Name '{' ListChanDec '}' { Ling.Fmt.Albert.Abs.ParSplit $1 $3 }
     | Name '[' ListChanDec ']' { Ling.Fmt.Albert.Abs.TenSplit $1 $3 }
     | Name '[:' ListChanDec ':]' { Ling.Fmt.Albert.Abs.SeqSplit $1 $3 }

Ling/Fmt/Albert/Print.hs

@@ -186,7 +186,7 @@ instance Print Proc where
   prtList _ (x:xs) = (concatD [prt 0 x, doc (showString "|"), prt 0 xs])
 instance Print Act where
   prt i e = case e of
-    Nu chandec1 chandec2 -> prPrec i 0 (concatD [doc (showString "new"), doc (showString "("), prt 0 chandec1, doc (showString ","), prt 0 chandec2, doc (showString ")")])
+    Nu chandecs -> prPrec i 0 (concatD [doc (showString "new"), doc (showString "("), prt 0 chandecs, doc (showString ")")])
     ParSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "{"), prt 0 chandecs, doc (showString "}")])
     TenSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "["), prt 0 chandecs, doc (showString "]")])
     SeqSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "[:"), prt 0 chandecs, doc (showString ":]")])

Ling/Fmt/Albert/Skel.hs

@@ -88,7 +88,7 @@ transProc x = case x of
   PDot proc1 proc2 -> failure x
 transAct :: Act -> Result
 transAct x = case x of
-  Nu chandec1 chandec2 -> failure x
+  Nu chandecs -> failure x
   ParSplit name chandecs -> failure x
   TenSplit name chandecs -> failure x
   SeqSplit name chandecs -> failure x

Ling/Free.hs

@@ -41,7 +41,7 @@ fcAct = \case
 
 bcAct :: BoundChans Act
 bcAct = \case
-  Nu c d       -> bcChanDecs [c, d]
+  Nu cs        -> bcChanDecs cs
   Split _ _ ds -> bcChanDecs ds
   Send{}       -> ø
   Recv{}       -> ø

Ling/Norm.hs

@@ -58,7 +58,7 @@ data CPatt
   deriving (Eq, Ord, Show, Read)
 
 data Act
-  = Nu       ChanDec ChanDec
+  = Nu       [ChanDec]
   -- TODO? Split Channel CPatt
   | Split    TraverseKind Channel [ChanDec]
   | Send     Channel Term

Ling/Par.y

@@ -187,7 +187,7 @@ ListProc : {- empty -} { [] }
          | Proc { (:[]) $1 }
          | Proc '|' ListProc { (:) $1 $3 }
 Act :: { Act }
-Act : 'new' '(' ChanDec ',' ChanDec ')' { Ling.Abs.Nu $3 $5 }
+Act : 'new' '(' ListChanDec ')' { Ling.Abs.Nu $3 }
     | Name '{' ListChanDec '}' { Ling.Abs.ParSplit $1 $3 }
     | Name '[' ListChanDec ']' { Ling.Abs.TenSplit $1 $3 }
     | Name '[:' ListChanDec ':]' { Ling.Abs.SeqSplit $1 $3 }

Ling/Print.hs

@@ -200,7 +200,7 @@ instance Print Proc where
   prtList _ (x:xs) = (concatD [prt 0 x, doc (showString "\n|"), prt 0 xs])
 instance Print Act where
   prt i e = case e of
-    Nu chandec1 chandec2 -> prPrec i 0 (concatD [doc (showString "new"), doc (showString "("), prt 0 chandec1, doc (showString ","), prt 0 chandec2, doc (showString ")")])
+    Nu chandecs -> prPrec i 0 (concatD [doc (showString "new"), doc (showString "("), prt 0 chandecs, doc (showString ")")])
     ParSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "{"), prt 0 chandecs, doc (showString "}")])
     TenSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "["), prt 0 chandecs, doc (showString "]")])
     SeqSplit name chandecs -> prPrec i 0 (concatD [prt 0 name, doc (showString "[:"), prt 0 chandecs, doc (showString ":]")])

Ling/Proto.hs

@@ -23,6 +23,7 @@ module Ling.Proto
   , protoAx
   , protoSendRecv
   , replProtoWhen
+  , assertUsed
   , assertAbsent
   , checkOrderedChans
   , checkSomeOrderChans
@@ -148,9 +149,16 @@ protoSendRecv cfs p =
   where crs = [ (c,mapR f (p ^. chanSession c . endedRS)) | (c,f) <- cfs ]
         cs = fst <$> cfs
 
-assertAbsent :: MonadError TCErr m => Channel -> Proto -> m ()
-assertAbsent c p =
-  assert (p ^. chans . hasNoKey c)
+-- Make sure the channel is used.
+-- When the session is ended we want to skip this check and allow the
+-- the channel to be unused.
+assertUsed :: MonadError TCErr m => Proto -> Channel -> m ()
+assertUsed proto c = assert (_Just `is` s) ["Unused channel " ++ pretty c]
+  where s = proto ^. chanSession c
+
+assertAbsent :: MonadError TCErr m => Proto -> Channel -> m ()
+assertAbsent proto c =
+  assert (proto ^. chans . hasNoKey c)
     ["The channel " ++ pretty c ++ " has been re-used"]
 
 checkConflictingChans :: MonadTC m => Proto -> Maybe Channel -> [Channel] -> m Proto

Ling/Reify.hs

@@ -146,7 +146,7 @@ normAct = \case
     SplitAx  n s c    -> go (splitAx        n (norm s) c)
 -}
 
-    Nu c d            -> go [N.Nu (norm c) (norm d)]
+    Nu cs             -> go [N.Nu (norm cs)]
     ParSplit c ds     -> go [N.Split N.ParK c (norm ds)]
     TenSplit c ds     -> go [N.Split N.TenK c (norm ds)]
     SeqSplit c ds     -> go [N.Split N.SeqK c (norm ds)]
@@ -168,7 +168,7 @@ reifyDefsA defs = pDots $ defs ^.. each . to reifyLetA . to PAct
 
 reifyAct :: N.Act -> Proc
 reifyAct = \case
-  N.Nu c d            -> PAct $ Nu (reify c) (reify d)
+  N.Nu cs             -> PAct $ Nu (reify cs)
   N.Split N.ParK c ds -> PAct $ ParSplit c (reify ds)
   N.Split N.TenK c ds -> PAct $ TenSplit c (reify ds)
   N.Split N.SeqK c ds -> PAct $ SeqSplit c (reify ds)

Ling/Rename.hs

@@ -71,7 +71,7 @@ instance Rename Act where
     Split k c ds    -> Split k (rename f c) (rename f ds)
     Send c e        -> Send (rename f c) (rename f e)
     Recv c arg      -> Recv (rename f c) (rename f arg)
-    Nu c d          -> Nu (rename f c) (rename f d)
+    Nu cs           -> Nu (rename f cs)
     NewSlice cs t x -> NewSlice (rename f cs) (rename f t) (rename f x)
     Ax s cs         -> Ax (rename f s) (rename f cs)
     At t cs         -> At (rename f t) (rename f cs)

Ling/Sequential.hs

@@ -148,14 +148,16 @@ transPref env pref0 procs k =
 transAct :: Act -> Endom Env
 transAct act =
   case act of
-    Nu (Arg c0 c0ORS) (Arg c1 c1ORS) ->
-      let c0OS = unRepl <$> c0ORS
-          c1OS = unRepl <$> c1ORS
-          Just (c0S , c1S) = extractDuals (c0OS, c1OS)
-          l = Root c0
+    Nu [] ->
+      id
+    Nu cds ->
+      let
+        cds'@(Arg c0 c0S:_) = cds & each . argBody . _Just %~ unRepl
+                                  & unsafePartsOf (each . argBody) %~ extractDuals
+        l = Root c0
       in
       addLocs  (sessionStatus (const Empty) l c0S) .
-      addChans [(c0,(l,oneS c0S)),(c1,(l,oneS c1S))]
+      addChans [(c,(l,oneS cS)) | Arg c cS <- cds']
     Split _ c ds ->
       transSplit c ds
     Send c _ ->

Ling/Session.hs

@@ -182,15 +182,18 @@ sessionStep :: Endom Session
 sessionStep (IO _ _ s) = s
 sessionStep s          = error $ "sessionStep: no steps " ++ show s
 
-extractDuals :: Dual a => (Maybe a, Maybe a) -> Maybe (a, a)
-extractDuals (Nothing, Nothing) = Nothing
-extractDuals (Just s0, Nothing) = Just (s0, dual s0)
-extractDuals (Nothing, Just s1) = Just (dual s1, s1)
-extractDuals (Just s0, Just s1) = Just (s0, s1)
+-- Should be length preserving
+extractDuals :: Dual a => [Maybe a] -> [a]
+extractDuals = \case
+  [Just s0, Nothing] -> [s0, dual s0]
+  [Nothing, Just s1] -> [dual s1, s1]
+
+  -- Appart from the two cases above the general rule
+  -- so far is that all sessions should be annotated
+  mas -> mas ^? below _Just ?| error "Missing type signature in `new` (extractDuals)"
 
--- TODO: would it be nicer with the First monoid
 extractSession :: [Maybe a] -> a
-extractSession l = l ^? each . _Just ?| error "Missing type signature in `new`"
+extractSession l = l ^? each . _Just ?| error "Missing type signature in `new` (extractSession)"
 
 -- See flatRSession in Ling.Reduce
 unsafeFlatRSession :: RSession -> [Session]

Ling/Skel.hs

@@ -79,7 +79,7 @@ transProc x = case x of
   PDot proc1 proc2 -> failure x
 transAct :: Act -> Result
 transAct x = case x of
-  Nu chandec1 chandec2 -> failure x
+  Nu chandecs -> failure x
   ParSplit name chandecs -> failure x
   TenSplit name chandecs -> failure x
   SeqSplit name chandecs -> failure x

Ling/Subst.hs

@@ -63,7 +63,7 @@ instance Subst Act where
     Split k c ds    -> Split k c (subst f ds)
     Send c e        -> Send c (subst f e)
     Recv c arg      -> Recv c (subst f arg)
-    Nu c d          -> Nu (subst f c) (subst f d)
+    Nu cs           -> Nu (subst f cs)
     NewSlice cs t x -> NewSlice cs (subst f t) x
     LetA{}          -> error "Subst/LetA"
     Ax s cs         -> Ax (subst f s) cs

fixtures/all/unused_chan.ll

@@ -0,0 +1 @@
+unused_chan = proc(c) c{i : !Int}