[ fix ] Seq1

src/Data/Seq1/Unsized.idr

@@ -22,15 +22,15 @@ export
 empty : F1 s (Seq1 s e)
 empty t =
   let tr # t := ref1 Empty t
-    in (MkSeq1 tr) # t
+    in MkSeq1 tr # t
 
 ||| O(1). A singleton sequence.
 export
 singleton :  e
           -> F1 s (Seq1 s e)
 singleton a t =
   let tr # t := ref1 (Single (MkElem a)) t
-    in (MkSeq1 tr) # t
+    in MkSeq1 tr # t
 
 ||| O(n). A sequence of length n with a the value of every element.
 export
@@ -39,23 +39,22 @@ replicate :  (n : Nat)
           -> F1 s (Seq1 s e)
 replicate n a t =
   let tr # t := ref1 (replicate' n a) t
-    in (MkSeq1 tr) # t
+    in MkSeq1 tr # t
 
 ||| O(1). The number of elements in the sequence.
 export
 length :  Seq1 s a
        -> F1 s Nat
 length (MkSeq1 tr) t =
   let tr' # t := read1 tr t
-    in (length' tr') # t
+    in length' tr' # t
 
 ||| O(n). Reverse the sequence.
 export
 reverse :  Seq1 s a
         -> F1' s
 reverse (MkSeq1 tr) t =
-  let tr' # t := read1 tr t
-    in casswap1 tr (reverseTree id tr') t
+  casmod1 tr (\tr' => reverseTree id tr') t
 
 export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
@@ -64,8 +63,7 @@ cons :  e
      -> Seq1 s e
      -> F1' s
 (a `cons` (MkSeq1 tr)) t =
-  let tr' # t := read1 tr t
-    in casswap1 tr (MkElem a `consTree` tr') t
+  casmod1 tr (\tr' => MkElem a `consTree` tr') t
 
 export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
@@ -74,102 +72,97 @@ snoc :  Seq1 s e
      -> e
      -> F1' s
 ((MkSeq1 tr) `snoc` a) t =
-  let tr' # t := read1 tr t
-    in casswap1 tr (tr' `snocTree` MkElem a) t
-
-||| O(log(min(m, n))). Concatenate two sequences.
-export
-(++) :  Seq1 s e
-     -> Seq1 s e
-     -> F1 s (Seq1 s e)
-((MkSeq1 t1) ++ (MkSeq1 t2)) t =
-  let t1'  # t := read1 t1 t
-      t2'  # t := read1 t2 t
-      t1t2 # t := ref1 (addTree0 t1' t2') t
-    in (MkSeq1 t1t2) # t
+  casmod1 tr (\tr' => tr' `snocTree` MkElem a) t
 
 ||| O(1). View from the left of the sequence.
 export
 viewl :  Seq1 s e
       -> F1 s (Maybe (e, Seq1 s e))
 viewl (MkSeq1 tr) t =
-  let tr' # t := read1 tr t
-    in case viewLTree tr' of
-         Just (MkElem a, tr') =>
-           let () # t := casswap1 tr tr' t
-             in (Just (a, MkSeq1 tr)) # t
-         Nothing              =>
-           Nothing # t
+  casupdate1 tr
+    (\tr' =>
+      case viewLTree tr' of
+        Just (MkElem a, tr'') =>
+          (tr'', Just (a, MkSeq1 tr))
+        Nothing               =>
+          (tr', Nothing)
+    ) t
 
 ||| O(1). The first element of the sequence.
 export
 head :  Seq1 s e
      -> F1 s (Maybe e)
-head seq t =
-  let seq' # t := viewl seq t
-    in case seq' of
-         Nothing     =>
-           Nothing # t
-         Just (h, _) =>
-           (Just h) # t
+head (MkSeq1 tr) t =
+  let tr' # t := read1 tr t
+   in case viewLTree tr' of
+        Just (MkElem a, _) =>
+          Just a # t
+        Nothing            =>
+          Nothing # t
+
 ||| O(1). The elements after the head of the sequence.
 ||| Returns an empty sequence when the sequence is empty.
 export
 tail :  Seq1 s e
-     -> F1 s (Seq1 s e)
-tail seq t =
-  let seq' # t := viewl seq t
-    in case seq' of
-         Just (_, seq'') =>
-           seq'' # t
-         Nothing          =>
-           empty t
+     -> F1' s
+tail (MkSeq1 tr) t =
+  casmod1 tr
+    (\tr' =>
+      case viewLTree tr' of
+        Just (MkElem _, tr'') =>
+          tr''
+        Nothing               =>
+          tr'
+    ) t
 
 ||| O(1). View from the right of the sequence.
 export
 viewr :  Seq1 s e
       -> F1 s (Maybe (Seq1 s e, e))
 viewr (MkSeq1 tr) t =
-  let tr' # t := read1 tr t
-    in case viewRTree tr' of
-         Just (tr', MkElem a) =>
-           let () # t := casswap1 tr tr' t
-             in (Just (MkSeq1 tr, a)) # t
-         Nothing              =>
-          Nothing # t
+  casupdate1 tr
+    (\tr' =>
+      case viewRTree tr' of
+        Just (tr'', MkElem a) =>
+          (tr'', Just (MkSeq1 tr, a))
+        Nothing               =>
+          (tr', Nothing)
+    ) t
 
 ||| O(1). The elements before the last element of the sequence.
 ||| Returns an empty sequence when the sequence is empty.
 export
 init :  Seq1 s e
-     -> F1 s (Seq1 s e)
-init seq t =
-  let seq' # t := viewr seq t
-    in case seq' of
-         Just (seq'', _) =>
-           seq'' # t
-         Nothing         =>
-           empty t
+     -> F1' s
+init (MkSeq1 tr) t =
+  casmod1 tr
+    (\tr' =>
+      case viewRTree tr' of
+        Just (tr'', MkElem _) =>
+          tr''
+        Nothing               =>
+          tr'
+    ) t
 
 ||| O(1). The last element of the sequence.
 export
 last :  Seq1 s e
      -> F1 s (Maybe e)
-last seq t =
-  let seq' # t := viewr seq t
-    in case seq' of
-         Nothing     =>
+last (MkSeq1 tr) t =
+  let tr' # t := read1 tr t
+    in case viewRTree tr' of
+         Just (_, MkElem a) =>
+           Just a # t
+         Nothing            =>
            Nothing # t
-         Just (_, l) =>
-           (Just l) # t
 
 ||| O(n). Turn a list into a sequence.
 export
 fromList :  List e
          -> F1 s (Seq1 s e)
 fromList xs t =
-  let seq # t := ref1 (foldr (\x, t => MkElem x `consTree` t) Empty xs) t
-    in (MkSeq1 seq) # t
+  let tr # t := ref1 (foldr (\x, acc => MkElem x `consTree` acc) Empty xs) t
+    in (MkSeq1 tr) # t
 
 ||| Turn a sequence into a list. O(n)
 export
@@ -182,12 +175,12 @@ toList seq t =
        -> (sl : SnocList e)
        -> F1 s (List e)
     go seq sl t =
-      let seq' # t := viewl seq t
-        in case seq' of
-             Nothing         =>
+      let tr # t := Data.Seq1.Unsized.viewl seq t
+        in case tr of
+             Nothing       =>
                (sl <>> []) # t
-             Just (x, seq'') =>
-               (assert_total (go seq'' (sl :< x))) t
+             Just (x, tr') =>
+               (assert_total (go tr' (sl :< x))) t
 
 ||| O(log(min(i, n-i))). The element at the specified position.
 export
@@ -199,7 +192,7 @@ index i (MkSeq1 tr) t =
     in case i < length' tr' of
          True  =>
            let (_, MkElem a) := lookupTree i tr'
-             in (Just a) # t
+            in Just a # t
          False =>
            Nothing # t
 
@@ -209,69 +202,31 @@ export
 adjust :  (e -> e)
        -> Nat
        -> Seq1 s e
-       -> F1 s (Seq1 s e)
+       -> F1' s
 adjust f i (MkSeq1 tr) t =
-  let tr' # t := read1 tr t
-    in case i < length' tr' of
-         True  =>
-           let () # t := casswap1 tr (adjustTree (const (map f)) i tr') t
-             in (MkSeq1 tr) # t
-         False =>
-           (MkSeq1 tr) # t
+  casmod1 tr
+    (\tr' =>
+      case i < length' tr' of
+        True  =>
+          adjustTree (const (map f)) i tr'
+        False => tr'
+    ) t
 
 ||| O(log(min(i, n-i))). Replace the element at the specified position.
 ||| If the position is out of range, the original sequence is returned.
 export
 update :  Nat
        -> e
        -> Seq1 s e
-       -> F1 s (Seq1 s e)
+       -> F1' s
 update i a seq t =
   adjust (const a) i seq t
 
-||| O(log(min(i, n-i))). Split a sequence at a given position.
-||| splitAt i s = (take i s, drop i s)
-export
-splitAt :  Nat
-        -> Seq1 s e
-        -> F1 s ((Seq1 s e, Seq1 s e))
-splitAt i (MkSeq1 tr) t =
-  let tr' # t := read1 tr t
-    in case i < length' tr' of
-         True  =>
-           let (l, r) := split i tr'
-               l' # t := ref1 l t
-               r' # t := ref1 r t
-             in (MkSeq1 l', MkSeq1 r') # t
-         False =>
-           let seq' # t := Data.Seq1.Unsized.empty t
-             in (MkSeq1 tr, seq') # t
-
-||| O(log(min(i,n-i))). The first i elements of a sequence.
-||| If the sequence contains fewer than i elements, the whole sequence is returned.
-export
-take :  Nat
-     -> Seq1 s e
-     -> F1 s (Seq1 s e)
-take i seq t =
-  let (seq1, _) # t := Data.Seq1.Unsized.splitAt i seq t
-    in seq1 # t
-
-||| O(log(min(i,n-i))). Elements of a sequence after the first i.
-||| If the sequence contains fewer than i elements, the empty sequence is returned.
-export
-drop :  Nat
-     -> Seq1 s e
-     -> F1 s (Seq1 s e)
-drop i seq t =
-  let (_, seq2) # t := Data.Seq1.Unsized.splitAt i seq t
-    in seq2 # t
-
 ||| Dump the internal structure of the finger tree.
 export
 show' :  Show e
       => Seq1 s e
       -> F1 s String
 show' (MkSeq1 tr) t =
   let tr' # t := read1 tr t
-    in (showPrec Open tr') # t
+    in showPrec Open tr' # t

test/src/Concurrent/Seq1.idr

@@ -0,0 +1,36 @@
+module Concurrent.Seq1
+
+import Data.Seq.Internal
+import Data.Seq.Unsized
+import Data.Seq1.Unsized
+import Data.Linear.Ref1
+import Data.Vect as V
+import System
+import System.Concurrency
+
+%default total
+
+ITER : Nat
+ITER = 10_000
+
+DELAY : Nat
+DELAY = 100_000
+
+inc : Seq1 s Nat -> Nat -> F1' s
+inc seq 0     t = snoc seq Z t
+inc seq (S k) t = snoc seq k t
+
+prog : Seq1 World Nat -> IO ()
+prog q = runIO (forN ITER $ inc q DELAY)
+
+runProg : Nat -> IO (List Nat)
+runProg n = do
+  q  <- runIO empty
+  ts <- sequence $ V.replicate n (fork $ prog q)
+  traverse_ (\t => threadWait t) ts
+  runIO (toList q)
+
+main : IO ()
+main = do
+  us <- runProg 4
+  printLn (length us)

test/src/Seq1/Unsized.idr

@@ -47,16 +47,6 @@ prop_snoc = property $ do
           _   # t := Data.Seq1.Unsized.snoc vs' 1 t
         in Data.Seq1.Unsized.toList vs' t ) === vs ++ [1]
 
-prop_concat : Property
-prop_concat = property $ do
-  xs <- forAll (list (linear 0 20) anyBits8)
-  ys <- forAll (list (linear 0 20) anyBits8)
-  ( run1 $ \t =>
-      let xs'  # t := Data.Seq1.Unsized.fromList xs t
-          ys'  # t := Data.Seq1.Unsized.fromList ys t
-          xsys # t := Data.Seq1.Unsized.(++) xs' ys' t
-        in Data.Seq1.Unsized.toList xsys t ) === xs ++ ys
-
 export
 props : Group
 props = MkGroup "Seq1 (Unsized)"
@@ -65,5 +55,4 @@ props = MkGroup "Seq1 (Unsized)"
   , ("prop_replicate", prop_replicate)
   , ("prop_cons", prop_cons)
   , ("prop_snoc", prop_snoc)
-  , ("prop_concat", prop_concat)
   ]