[ test ] for the new feature

Fixing other tests impacted by the refactoring

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

tests/idris2/linear/linear010/Door.idr

@@ -1,4 +1,5 @@
 import Control.Linear.LIO
+import Data.Linear.Notation
 
 foo : LinearIO io => L io ()
 foo = do putStrLn "Hello"

tests/idris2/linear/linear011/Network.idr

@@ -1,4 +1,5 @@
 import Control.Linear.LIO
+import Data.Linear.Notation
 
 import Network.Socket
 

tests/linear/system_concurrency_session/Main.idr

@@ -0,0 +1,29 @@
+import Control.Linear.LIO
+import System.Concurrency.Session
+import Data.Linear.Notation
+
+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}"

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

tests/linear/system_concurrency_session/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run -p linear Main.idr