From 1b19624d6224e32bf26b554a0a4a56720b45aa0a Mon Sep 17 00:00:00 2001
From: Matthew-Mosior <mattm.github@gmail.com>
Date: Fri, 13 Dec 2024 14:38:45 -0600
Subject: [PATCH] Moving Data.Seq.Internal, Data.Seq.Sized, and
 Data.Seq.Unsized from contrib.

---
 containers.ipkg           |   4 +-
 src/Data/Seq/Internal.idr | 682 ++++++++++++++++++++++++++++++++++++++
 src/Data/Seq/Sized.idr    | 213 ++++++++++++
 src/Data/Seq/Unsized.idr  | 224 +++++++++++++
 4 files changed, 1122 insertions(+), 1 deletion(-)
 create mode 100644 src/Data/Seq/Internal.idr
 create mode 100644 src/Data/Seq/Sized.idr
 create mode 100644 src/Data/Seq/Unsized.idr

diff --git a/containers.ipkg b/containers.ipkg
index 0bd0686..e44187a 100644
--- a/containers.ipkg
+++ b/containers.ipkg
@@ -6,7 +6,6 @@ version    = 0.6.0
 sourcedir  = "src"
 depends    = base         >= 0.6.0
            , array
-           , contrib
            , elab-util
 
 modules = Data.Map
@@ -15,5 +14,8 @@ modules = Data.Map
         , Data.RRBVector.Internal
         , Data.Set
         , Data.Set.Internal
+        , Data.Seq.Sized
+        , Data.Seq.Unsized
+        , Data.Seq.Internal
         , Data.Queue
         , Data.Tree
diff --git a/src/Data/Seq/Internal.idr b/src/Data/Seq/Internal.idr
new file mode 100644
index 0000000..a54f39c
--- /dev/null
+++ b/src/Data/Seq/Internal.idr
@@ -0,0 +1,682 @@
+||| This module is not intended to be imported directly.
+||| Please use Data.Seq or Data.Seq.Seq' instead.
+|||
+||| The implementation of fingertree comes from
+||| <http://hackage.haskell.org/package/containers-0.2.0.1/docs/src/Data-Sequence.html>
+|||
+||| The original code is under a BSD-style license, compatible with this project.
+|||
+||| Original Copyrights: Copyright 2004, The University Court of the University of Glasgow
+|||                      (c) Ross Paterson 2005
+module Data.Seq.Internal
+
+import Control.WellFounded
+import Data.Zippable
+
+%default total
+
+err : String -> a
+err s = assert_total (idris_crash s)
+
+showApp : Show a => a -> String
+showApp = showPrec App
+
+prettyShow : Prec -> String -> String
+prettyShow p s = if p >= PrefixMinus
+  then "(" ++ s ++ ")"
+  else s
+
+-- Digit
+data Digit : (e : Type) -> Type where
+  One : (a : e) -> Digit e
+  Two : (a : e) -> (b : e) -> Digit e
+  Three : (a : e) -> (b : e) -> (c : e) -> Digit e
+  Four : (a : e) -> (b : e) -> (c : e) -> (d : e) -> Digit e
+
+implementation Functor Digit where
+  map f (One a) = One (f a)
+  map f (Two a b) = Two (f a) (f b)
+  map f (Three a b c) = Three (f a) (f b) (f c)
+  map f (Four a b c d) = Four (f a) (f b) (f c) (f d)
+
+implementation Foldable Digit where
+  foldr f z (One a) = a `f` z
+  foldr f z (Two a b) = a `f` (b `f` z)
+  foldr f z (Three a b c) = a `f` (b `f` (c `f` z))
+  foldr f z (Four a b c d) = a `f` (b `f` (c `f` (d `f` z)))
+
+  foldl f z (One a) = z `f` a
+  foldl f z (Two a b) = (z `f` a) `f` b
+  foldl f z (Three a b c) = ((z `f` a) `f` b) `f` c
+  foldl f z (Four a b c d) = (((z `f` a) `f` b) `f` c) `f` d
+
+implementation Traversable Digit where
+  traverse f (One a) = [|One (f a)|]
+  traverse f (Two a b) = [|Two (f a) (f b)|]
+  traverse f (Three a b c) = [|Three (f a) (f b) (f c)|]
+  traverse f (Four a b c d) = [|Four (f a) (f b) (f c) (f d)|]
+
+implementation Sized e => Sized (Digit e) where
+  size = foldr (\a, z => size a + z) 0
+
+implementation Show a => Show (Digit a) where
+  showPrec p (One a)        = prettyShow p $
+    "One " ++ showApp a
+  showPrec p (Two a b)      = prettyShow p $
+    "Two " ++ showApp a ++ " " ++ showApp b
+  showPrec p (Three a b c)  = prettyShow p $
+    "Three " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c
+  showPrec p (Four a b c d) = prettyShow p $
+    "Four " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c ++ " " ++ showApp d
+
+-- Node
+data Node : (e : Type) -> Type where
+  Node2 : Nat -> (a : e) -> (b : e) -> Node e
+  Node3 : Nat -> (a : e) -> (b : e) -> (c : e) -> Node e
+
+implementation Functor Node where
+  map f (Node2 s a b)   = Node2 s (f a) (f b)
+  map f (Node3 s a b c) = Node3 s (f a) (f b) (f c)
+
+implementation Foldable Node where
+  foldr f z (Node2 _ a b)   = a `f` (b `f` z)
+  foldr f z (Node3 _ a b c) = a `f` (b `f` (c `f` z))
+
+  foldl f z (Node2 _ a b)   = (z `f` a) `f` b
+  foldl f z (Node3 _ a b c) = ((z `f` a) `f` b) `f` c
+
+implementation Traversable Node where
+  traverse f (Node2 s a b)   = Node2 s <$> f a <*> f b
+  traverse f (Node3 s a b c) = Node3 s <$> f a <*> f b <*> f c
+
+implementation Sized e => Sized (Node e) where
+  size (Node2 s _ _)   = s
+  size (Node3 s _ _ _) = s
+
+implementation Show a => Show (Node a) where
+  showPrec p (Node2 _ a b)   = prettyShow p $
+    "Node2 " ++ showApp a ++ " " ++ showApp b
+  showPrec p (Node3 _ a b c) = prettyShow p $
+    "Node3 " ++ showApp a ++ " " ++ showApp b ++ " " ++ showApp c
+
+-- Smart Constructors
+node2 : Sized e => e -> e -> Node e
+node2 a b = Node2 (size a + size b) a b
+
+node3 : Sized e => e -> e -> e -> Node e
+node3 a b c = Node3 (size a + size b + size c) a b c
+
+-- Elem
+public export
+data Elem a = MkElem a
+
+export
+unElem : Elem a -> a
+unElem (MkElem a) = a
+
+public export
+implementation Sized (Elem a) where
+  size _ = 1
+
+public export
+implementation Eq a => Eq (Elem a) where
+  MkElem a == MkElem b = a == b
+
+public export
+implementation Ord a => Ord (Elem a) where
+  compare (MkElem a) (MkElem b) = compare a b
+
+public export
+implementation Functor Elem where
+  map f (MkElem a) = MkElem (f a)
+
+public export
+implementation Applicative Elem where
+  pure = MkElem
+  MkElem f <*> MkElem a = MkElem (f a)
+
+public export
+implementation Show a => Show (Elem a) where
+  showPrec p (MkElem a) = showPrec p a
+
+
+-- FingerTree
+public export
+data FingerTree : (e : Type) -> Type where
+  Empty : FingerTree e
+  Single : (a : e) -> FingerTree e
+  Deep : Nat -> Digit e -> FingerTree (Node e) -> Digit e -> FingerTree e
+
+public export
+implementation Sized e => Sized (FingerTree e) where
+  size Empty          = 0
+  size (Single a)     = size a
+  size (Deep s _ _ _) = s
+
+-- Smart Constructor
+deep : Sized e => Digit e -> FingerTree (Node e) -> Digit e -> FingerTree e
+deep d1 st d2 = Deep (size d1 + size st + size d2) d1 st d2
+
+
+-- Reversing
+reverseDigit : (a -> a) -> Digit a -> Digit a
+reverseDigit f (One a) = One (f a)
+reverseDigit f (Two a b) = Two (f b) (f a)
+reverseDigit f (Three a b c) = Three (f c) (f b) (f a)
+reverseDigit f (Four a b c d) = Four (f d) (f c) (f b) (f a)
+
+reverseNode : (a -> a) -> Node a -> Node a
+reverseNode f (Node2 s a b) = Node2 s (f b) (f a)
+reverseNode f (Node3 s a b c) = Node3 s (f c) (f b) (f a)
+
+export
+reverseTree : (a -> a) -> FingerTree a -> FingerTree a
+reverseTree _ Empty = Empty
+reverseTree f (Single x) = Single (f x)
+reverseTree f (Deep s pr m sf) =
+  Deep s (reverseDigit f sf)
+    (reverseTree (reverseNode f) m)
+    (reverseDigit f pr)
+
+
+-- Looking up
+lookupDigit : Sized a => Nat -> Digit a -> (Nat, a)
+lookupDigit i (One a) = (i, a)
+lookupDigit i (Two a b) =
+  let sa = size a
+  in if i < sa
+    then (i, a)
+    else (i `minus` sa, b)
+lookupDigit i (Three a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then (i, a)
+    else if i < sab
+      then (i `minus` sa, b)
+      else ((i `minus` sa) `minus` sab, c)
+lookupDigit i (Four a b c d) =
+  let sa   = size a
+      sab  = sa + size b
+      sabc = sab + size c
+  in if i < sab
+    then if i < sa
+      then (i, a)
+      else (i `minus` sa, b)
+    else if i < sabc
+      then (i `minus` sab, c)
+      else (i `minus` sabc, d)
+
+lookupNode : Sized a => Nat -> Node a -> (Nat, a)
+lookupNode i (Node2 _ a b) =
+  let sa = size a
+  in if i < sa
+    then (i, a)
+    else (i `minus` sa, b)
+lookupNode i (Node3 _ a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then (i, a)
+    else if i < sab
+      then (i `minus` sa, b)
+      else (i `minus` sab, c)
+
+export
+lookupTree : Sized a => Nat -> FingerTree a -> (Nat, a)
+lookupTree _ Empty = err "lookupTree of empty tree"
+lookupTree i (Single x) = (i, x)
+lookupTree i (Deep _ pr m sf) =
+  let spr = size pr
+      spm = spr + size m
+  in if i < spr
+    then lookupDigit i pr
+    else if i < spm
+      then let (i', xs) = lookupTree (i `minus` spr) m
+           in lookupNode i' xs
+      else lookupDigit (i `minus` spm) sf
+
+-- Adjusting
+adjustDigit : Sized a => (Nat -> a -> a) -> Nat -> Digit a -> Digit a
+adjustDigit f i (One a) = One (f i a)
+adjustDigit f i (Two a b) =
+  let sa = size a
+  in if i < sa
+    then Two (f i a) b
+    else Two a (f (i `minus` sa) b)
+adjustDigit f i (Three a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then Three (f i a) b c
+    else if i < sab
+      then Three a (f (i `minus` sa) b) c
+      else Three a b (f (i `minus` sab) c)
+adjustDigit f i (Four a b c d) =
+  let sa   = size a
+      sab  = sa + size b
+      sabc = sab + size c
+  in if i < sab
+    then if i < sa
+      then Four (f i a) b c d
+      else Four a (f (i `minus` sa) b) c d
+    else if i < sabc
+      then Four a b (f (i `minus` sab) c) d
+      else Four a b c (f (i `minus` sabc) d)
+
+adjustNode : Sized a => (Nat -> a -> a) -> Nat -> Node a -> Node a
+adjustNode f i (Node2 s a b) =
+  let sa = size a
+  in if i < sa
+    then Node2 s (f i a) b
+    else Node2 s a (f (i `minus` sa) b)
+adjustNode f i (Node3 s a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then Node3 s (f i a) b c
+    else if i < sab
+      then Node3 s a (f (i `minus` sa) b) c
+      else Node3 s a b (f (i `minus` sab) c)
+
+export
+adjustTree : Sized a => (Nat -> a -> a) -> Nat -> FingerTree a -> FingerTree a
+adjustTree _ _ Empty = err "adjustTree of empty tree"
+adjustTree f i (Single x) = Single (f i x)
+adjustTree f i (Deep s pr m sf) =
+  let spr = size pr
+      spm = spr + size m
+  in if i < spr
+    then Deep s (adjustDigit f i pr) m sf
+    else if i < spm
+      then Deep s pr (adjustTree (adjustNode f) (i `minus` spr) m) sf
+      else Deep s pr m (adjustDigit f (i `minus` spm) sf)
+
+
+-- Casting between types
+digitToTree : Sized a => Digit a -> FingerTree a
+digitToTree (One a)        = Single a
+digitToTree (Two a b)      = deep (One a) Empty (One b)
+digitToTree (Three a b c)  = deep (Two a b) Empty (One c)
+digitToTree (Four a b c d) = deep (Two a b) Empty (Two c d)
+
+nodeToDigit : Node e -> Digit e
+nodeToDigit (Node2 _ a b)   = Two a b
+nodeToDigit (Node3 _ a b c) = Three a b c
+
+
+-- Viewing
+export
+viewLTree  : Sized a => FingerTree a -> Maybe (a, FingerTree a)
+viewLTree Empty = Nothing
+viewLTree (Single a) = Just (a, Empty)
+viewLTree (Deep s (One a) m sf) =
+  let tr =
+    case viewLTree m of
+        Nothing      => digitToTree sf
+        Just (b, m') => Deep (s `minus` size a) (nodeToDigit b) m' sf
+  in Just (a, tr)
+viewLTree (Deep s (Two a b) m sf) =
+  Just (a, Deep (s `minus` size a) (One b) m sf)
+viewLTree (Deep s (Three a b c) m sf) =
+  Just (a, Deep (s `minus` size a) (Two b c) m sf)
+viewLTree (Deep s (Four a b c d) m sf) =
+  Just (a, Deep (s `minus` size a) (Three b c d) m sf)
+
+export
+viewRTree  : Sized a => FingerTree a -> Maybe (FingerTree a, a)
+viewRTree Empty = Nothing
+viewRTree (Single z) = Just (Empty, z)
+viewRTree (Deep s pr m (One z)) =
+  let tr =
+    case viewRTree m of
+        Nothing      => digitToTree pr
+        Just (m', y) => Deep (s `minus` size z) pr m' (nodeToDigit y)
+  in Just (tr, z)
+viewRTree (Deep s pr m (Two y z)) =
+  Just (Deep (s `minus` size z) pr m (One y), z)
+viewRTree (Deep s pr m (Three x y z)) =
+  Just (Deep (s `minus` size z) pr m (Two x y), z)
+viewRTree (Deep s pr m (Four w x y z)) =
+  Just (Deep (s `minus` size z) pr m (Three w x y), z)
+
+
+-- Construction
+export infixr 5 `consTree`
+export
+consTree : Sized e => (r : e) -> FingerTree e -> FingerTree e
+a `consTree` Empty                       = Single a
+a `consTree` Single b                    = deep (One a) Empty (One b)
+a `consTree` Deep s (One b) st d2        = Deep (size a + s) (Two a b) st d2
+a `consTree` Deep s (Two b c) st d2      = Deep (size a + s) (Three a b c) st d2
+a `consTree` Deep s (Three b c d) st d2  = Deep (size a + s) (Four a b c d) st d2
+a `consTree` Deep s (Four b c d f) st d2 = Deep (size a + s) (Two a b) (node3 c d f `consTree` st) d2
+
+export infixl 5 `snocTree`
+export
+snocTree : Sized e => FingerTree e -> (r : e) -> FingerTree e
+Empty `snocTree` a                       = Single a
+Single a `snocTree` b                    = deep (One a) Empty (One b)
+Deep s d1 st (One a) `snocTree` f        = Deep (s + size a) d1 st (Two a f)
+Deep s d1 st (Two a b) `snocTree` f      = Deep (s + size a) d1 st (Three a b f)
+Deep s d1 st (Three a b c) `snocTree` f  = Deep (s + size a) d1 st (Four a b c f)
+Deep s d1 st (Four a b c d) `snocTree` f = Deep (s + size f) d1 (st `snocTree` node3 a b c) (Two d f)
+
+
+-- Splitting
+data Split t a = MkSplit t a t
+
+splitDigit : Sized a => Nat -> Digit a -> Split (Maybe (Digit a)) a
+splitDigit i (One a) = MkSplit Nothing a Nothing
+splitDigit i (Two a b) =
+  let sa = size a
+  in if i < sa
+    then MkSplit Nothing a (Just (One b))
+    else MkSplit (Just (One a)) b Nothing
+splitDigit i (Three a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then MkSplit Nothing a (Just (Two b c))
+    else if i < sab
+      then MkSplit (Just (One a)) b (Just (One c))
+      else MkSplit (Just (Two a b)) c Nothing
+splitDigit i (Four a b c d) =
+  let sa   = size a
+      sab  = sa + size b
+      sabc = sab + size c
+  in if i < sab
+    then if i < sa
+      then MkSplit Nothing a (Just (Three b c d))
+      else MkSplit (Just (One a)) b (Just (Two c d))
+    else if i < sabc
+      then MkSplit (Just (Two a b)) c (Just (One d))
+      else MkSplit (Just (Three a b c)) d Nothing
+
+splitNode : Sized a => Nat -> Node a -> Split (Maybe (Digit a)) a
+splitNode i (Node2 _ a b) =
+  let sa = size a
+  in if i < sa
+    then MkSplit Nothing a (Just (One b))
+    else MkSplit (Just (One a)) b Nothing
+splitNode i (Node3 _ a b c) =
+  let sa  = size a
+      sab = sa + size b
+  in if i < sa
+    then MkSplit Nothing a (Just (Two b c))
+    else if i < sab
+      then MkSplit (Just (One a)) b (Just (One c))
+      else MkSplit (Just (Two a b)) c Nothing
+
+deepL : Sized a => Maybe (Digit a) -> FingerTree (Node a) -> Digit a -> FingerTree a
+deepL Nothing m sf = case viewLTree m of
+  Nothing      => digitToTree sf
+  Just (a, m') => Deep (size m + size sf) (nodeToDigit a) m' sf
+deepL (Just pr) m sf = deep pr m sf
+
+deepR : Sized a => Digit a -> FingerTree (Node a) -> Maybe (Digit a) -> FingerTree a
+deepR pr m Nothing = case viewRTree m of
+  Nothing      => digitToTree pr
+  Just (m', a) => Deep (size pr + size m) pr m' (nodeToDigit a)
+deepR pr m (Just sf) = deep pr m sf
+
+splitTree : Sized a => Nat -> FingerTree a -> Split (FingerTree a) a
+splitTree _ Empty = err "splitTree of empty tree"
+splitTree i (Single x) = MkSplit Empty x Empty
+splitTree i (Deep _ pr m sf) =
+  let spr = size pr
+      spm = spr + size m
+      im  = i `minus` spr
+  in if i < spr
+    then let MkSplit l x r = splitDigit i pr
+         in MkSplit (maybe Empty digitToTree l) x (deepL r m sf)
+    else if i < spm
+      then let MkSplit ml xs mr = splitTree im m
+               MkSplit l x r = splitNode (im `minus` size ml) xs
+           in MkSplit (deepR pr  ml l) x (deepL r mr sf)
+      else let MkSplit l x r = splitDigit (i `minus` spm) sf
+           in MkSplit (deepR pr  m  l) x (maybe Empty digitToTree r)
+
+export
+split : Nat -> FingerTree (Elem a) -> (FingerTree (Elem a), FingerTree (Elem a))
+split _ Empty = (Empty, Empty)
+split i xs =
+  if size xs > i
+   then let MkSplit l x r = splitTree i xs in (l, x `consTree` r)
+   else (xs, Empty)
+
+
+-- Concatenation
+mutual
+  addDigits4 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
+  addDigits4 m1 (One a) b c d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits4 m1 (One a) b c d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits4 m1 (One a) b c d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits4 m1 (One a) b c d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits4 m1 (Two a b) c d e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits4 m1 (Two a b) c d e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits4 m1 (Two a b) c d e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits4 m1 (Two a b) c d e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+  addDigits4 m1 (Three a b c) d e f g (One h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits4 m1 (Three a b c) d e f g (Two h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits4 m1 (Three a b c) d e f g (Three h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+  addDigits4 m1 (Three a b c) d e f g (Four h i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
+  addDigits4 m1 (Four a b c d) e f g h (One i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits4 m1 (Four a b c d) e f g h (Two i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+  addDigits4 m1 (Four a b c d) e f g h (Three i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
+  addDigits4 m1 (Four a b c d) e f g h (Four i j k l) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node3 j k l) m2
+
+  appendTree4 : Sized e => FingerTree (Node e) -> Node e -> Node e -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
+  appendTree4 Empty a b c d xs = a `consTree` b `consTree` c `consTree` d `consTree` xs
+  appendTree4 xs a b c d Empty = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` d
+  appendTree4 (Single x) a b c d xs = x `consTree` a `consTree` b `consTree` c `consTree` d `consTree` xs
+  appendTree4 xs a b c d (Single x) = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` d `snocTree` x
+  appendTree4 (Deep s1 pr1 m1 sf1) a b c d (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + size c + size d + s2) pr1 (addDigits4 m1 sf1 a b c d pr2 m2) sf2
+
+  addDigits3 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
+  addDigits3 m1 (One a) b c d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits3 m1 (One a) b c d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits3 m1 (One a) b c d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits3 m1 (One a) b c d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits3 m1 (Two a b) c d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits3 m1 (Two a b) c d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits3 m1 (Two a b) c d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits3 m1 (Two a b) c d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits3 m1 (Three a b c) d e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits3 m1 (Three a b c) d e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits3 m1 (Three a b c) d e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits3 m1 (Three a b c) d e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+  addDigits3 m1 (Four a b c d) e f g (One h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits3 m1 (Four a b c d) e f g (Two h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits3 m1 (Four a b c d) e f g (Three h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+  addDigits3 m1 (Four a b c d) e f g (Four h i j k) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) m2
+
+  appendTree3 : Sized e => FingerTree (Node e) -> Node e -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
+  appendTree3 Empty a b c xs = a `consTree` b `consTree` c `consTree` xs
+  appendTree3 xs a b c Empty = xs `snocTree` a `snocTree` b `snocTree` c
+  appendTree3 (Single x) a b c xs = x `consTree` a `consTree` b `consTree` c `consTree` xs
+  appendTree3 xs a b c (Single x) = xs `snocTree` a `snocTree` b `snocTree` c `snocTree` x
+  appendTree3 (Deep s1 pr1 m1 sf1) a b c (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + size c + s2) pr1 (addDigits3 m1 sf1 a b c pr2 m2) sf2
+
+  addDigits2 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
+  addDigits2 m1 (One a) b c (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+  addDigits2 m1 (One a) b c (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits2 m1 (One a) b c (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits2 m1 (One a) b c (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits2 m1 (Two a b) c d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits2 m1 (Two a b) c d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits2 m1 (Two a b) c d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits2 m1 (Two a b) c d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits2 m1 (Three a b c) d e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits2 m1 (Three a b c) d e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits2 m1 (Three a b c) d e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits2 m1 (Three a b c) d e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits2 m1 (Four a b c d) e f (One g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits2 m1 (Four a b c d) e f (Two g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits2 m1 (Four a b c d) e f (Three g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+  addDigits2 m1 (Four a b c d) e f (Four g h i j) m2 = appendTree4 m1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) m2
+
+  appendTree2 : Sized e => FingerTree (Node e) -> Node e -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
+  appendTree2 Empty a b xs = a `consTree` b `consTree` xs
+  appendTree2 xs a b Empty = xs `snocTree` a `snocTree` b
+  appendTree2 (Single x) a b xs = x `consTree` a `consTree` b `consTree` xs
+  appendTree2 xs a b (Single x) = xs `snocTree` a `snocTree` b `snocTree` x
+  appendTree2 (Deep s1 pr1 m1 sf1) a b (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + size b + s2) pr1 (addDigits2 m1 sf1 a b pr2 m2) sf2
+
+mutual
+  addDigits1 : Sized e => FingerTree (Node (Node e)) -> Digit (Node e) -> Node e -> Digit (Node e) -> FingerTree (Node (Node e)) -> FingerTree (Node (Node e))
+  addDigits1 m1 (One a) b (One c) m2 = appendTree1 m1 (node3 a b c) m2
+  addDigits1 m1 (One a) b (Two c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+  addDigits1 m1 (One a) b (Three c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits1 m1 (One a) b (Four c d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits1 m1 (Two a b) c (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+  addDigits1 m1 (Two a b) c (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits1 m1 (Two a b) c (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits1 m1 (Two a b) c (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits1 m1 (Three a b c) d (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+  addDigits1 m1 (Three a b c) d (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits1 m1 (Three a b c) d (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits1 m1 (Three a b c) d (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits1 m1 (Four a b c d) e (One f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+  addDigits1 m1 (Four a b c d) e (Two f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+  addDigits1 m1 (Four a b c d) e (Three f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+  addDigits1 m1 (Four a b c d) e (Four f g h i) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node3 g h i) m2
+
+  appendTree1 : Sized e => FingerTree (Node e) -> Node e -> FingerTree (Node e) -> FingerTree (Node e)
+  appendTree1 Empty a xs = a `consTree` xs
+  appendTree1 xs a Empty = xs `snocTree` a
+  appendTree1 (Single x) a xs = x `consTree` a `consTree` xs
+  appendTree1 xs a (Single x) = xs `snocTree` a `snocTree` x
+  appendTree1 (Deep s1 pr1 m1 sf1) a (Deep s2 pr2 m2 sf2) = Deep (s1 + size a + s2) pr1 (addDigits1 m1 sf1 a pr2 m2) sf2
+
+addDigits0 : FingerTree (Node (Elem a)) -> Digit (Elem a) -> Digit (Elem a) -> FingerTree (Node (Elem a)) -> FingerTree (Node (Elem a))
+addDigits0 m1 (One a) (One b) m2 = appendTree1 m1 (node2 a b) m2
+addDigits0 m1 (One a) (Two b c) m2 = appendTree1 m1 (node3 a b c) m2
+addDigits0 m1 (One a) (Three b c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+addDigits0 m1 (One a) (Four b c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+addDigits0 m1 (Two a b) (One c) m2 = appendTree1 m1 (node3 a b c) m2
+addDigits0 m1 (Two a b) (Two c d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+addDigits0 m1 (Two a b) (Three c d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+addDigits0 m1 (Two a b) (Four c d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+addDigits0 m1 (Three a b c) (One d) m2 = appendTree2 m1 (node2 a b) (node2 c d) m2
+addDigits0 m1 (Three a b c) (Two d e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+addDigits0 m1 (Three a b c) (Three d e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+addDigits0 m1 (Three a b c) (Four d e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+addDigits0 m1 (Four a b c d) (One e) m2 = appendTree2 m1 (node3 a b c) (node2 d e) m2
+addDigits0 m1 (Four a b c d) (Two e f) m2 = appendTree2 m1 (node3 a b c) (node3 d e f) m2
+addDigits0 m1 (Four a b c d) (Three e f g) m2 = appendTree3 m1 (node3 a b c) (node2 d e) (node2 f g) m2
+addDigits0 m1 (Four a b c d) (Four e f g h) m2 = appendTree3 m1 (node3 a b c) (node3 d e f) (node2 g h) m2
+
+export
+addTree0 : FingerTree (Elem a) -> FingerTree (Elem a) -> FingerTree (Elem a)
+addTree0 Empty xs = xs
+addTree0 xs Empty = xs
+addTree0 (Single x) xs = x `consTree` xs
+addTree0 xs (Single x) = xs `snocTree` x
+addTree0 (Deep s1 pr1 m1 sf1) (Deep s2 pr2 m2 sf2) = Deep (s1 + s2) pr1 (addDigits0 m1 sf1 pr2 m2) sf2
+
+-- List-like
+export
+toList' : FingerTree (Elem a) -> List a
+toList' tr = case viewLTree tr of
+    Just (MkElem a, tr') => a :: assert_total (toList' tr')
+    Nothing              => Nil
+
+export
+replicate' : Nat -> e -> FingerTree (Elem e)
+replicate' n a = replicate1 n Empty
+  where
+    elem : Elem e
+    elem = MkElem a
+    replicate1 : Nat -> FingerTree (Elem e) -> FingerTree (Elem e)
+    replicate1 Z tr = tr
+    replicate1 (S k) tr = replicate1 k (elem `consTree` tr)
+
+export
+length' : FingerTree (Elem e) -> Nat
+length' = size
+
+-- FingerTree Implementations
+public export
+implementation Functor FingerTree where
+  map _ Empty = Empty
+  map f (Single x) = Single (f x)
+  map f (Deep s d1 st d2) =
+    Deep s (map f d1) (map (map f) st) (map f d2)
+
+public export
+implementation Foldable FingerTree where
+  foldr _ z Empty            = z
+  foldr f z (Single x)       = x `f` z
+  foldr f z (Deep _ pr m sf) = foldr f (foldr (flip (foldr f)) (foldr f z sf) m) pr
+
+  foldl _ z Empty            = z
+  foldl f z (Single x)       = z `f` x
+  foldl f z (Deep _ pr m sf) = foldl f (foldl (foldl f) (foldl f z pr) m) sf
+
+public export
+implementation Traversable FingerTree where
+  traverse _ Empty            = pure Empty
+  traverse f (Single x)       = Single <$> f x
+  traverse f (Deep v pr m sf) =
+    Deep v <$> traverse f pr <*> traverse (traverse f) m <*> traverse f sf
+
+public export
+implementation Show a => Show (FingerTree a) where
+  showPrec _ Empty             = "Empty"
+  showPrec p (Single a)        = prettyShow p $ "Single " ++ showApp a
+  showPrec p (Deep _ d1 st d2) = prettyShow p $
+    "Deep " ++ showApp d1 ++ " " ++ assert_total (showApp st) ++ " " ++ showApp d2
+
+public export
+implementation Sized a => Eq a => Eq (FingerTree a) where
+  x == y = case (viewLTree x, viewLTree y) of
+    (Just (x1, xs), Just (y1, ys)) => if x1 == y1
+      then assert_total (xs == ys)
+      else False
+    (Nothing, Nothing) => True
+    _                  => False
+
+public export
+implementation Sized a => Ord a => Ord (FingerTree a) where
+  compare x y = case (viewLTree x, viewLTree y) of
+    (Just (x1, xs), Just (y1, ys)) =>
+      let res = compare x1 y1
+      in if res == EQ
+        then assert_total (compare xs ys)
+        else res
+    (Nothing, Nothing) => EQ
+    (_      , Nothing) => GT
+    (Nothing, _      ) => LT
+
+
+-- Zipping
+export
+zipWith' : (a -> b -> c) -> FingerTree (Elem a) -> FingerTree (Elem b) -> FingerTree (Elem c)
+zipWith' f x y = case (viewLTree x, viewLTree y) of
+  (Just (x1, xs), Just (y1, ys)) => [|f x1 y1|] `consTree` assert_total (zipWith' f xs ys)
+  _ => Empty
+
+export
+zipWith3' : (a -> b -> c -> d) -> FingerTree (Elem a) -> FingerTree (Elem b) -> FingerTree (Elem c) -> FingerTree (Elem d)
+zipWith3' f x y z = case (viewLTree x, viewLTree y, viewLTree z) of
+  (Just (x1, xs), Just (y1, ys), Just (z1, zs)) => [|f x1 y1 z1|] `consTree` assert_total (zipWith3' f xs ys zs)
+  _ => Empty
+
+export
+unzipWith' : (a -> (b, c)) -> FingerTree (Elem a) -> (FingerTree (Elem b), FingerTree (Elem c))
+unzipWith' f zs = foldr app (Empty, Empty) zs
+  where
+    app : Elem a -> (FingerTree (Elem b), FingerTree (Elem c)) -> (FingerTree (Elem b), FingerTree (Elem c))
+    app (MkElem z) (xs, ys) = let (x, y) = f z in (MkElem x `consTree` xs, MkElem y `consTree` ys)
+
+export
+unzipWith3' : (a -> (b, c, d)) -> FingerTree (Elem a)
+            -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
+unzipWith3' f ws = foldr app (Empty, Empty, Empty) ws
+  where
+    app : Elem a -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
+        -> (FingerTree (Elem b), FingerTree (Elem c), FingerTree (Elem d))
+    app (MkElem w) (xs, ys, zs) =
+      let (x, y, z) = f w
+      in (MkElem x `consTree` xs, MkElem y `consTree` ys, MkElem z `consTree` zs)
diff --git a/src/Data/Seq/Sized.idr b/src/Data/Seq/Sized.idr
new file mode 100644
index 0000000..79ca527
--- /dev/null
+++ b/src/Data/Seq/Sized.idr
@@ -0,0 +1,213 @@
+||| General purpose two-end finite sequences,
+||| with length in its type.
+|||
+||| This is implemented by finger tree.
+module Data.Seq.Sized
+
+import Control.WellFounded
+
+import public Data.Fin
+import public Data.Nat
+import public Data.Vect
+import public Data.Zippable
+
+import Data.Seq.Internal
+
+%default total
+
+err : String -> a
+err s = assert_total (idris_crash s)
+
+||| A two-end finite sequences, with length in its type.
+export
+data Seq : Nat -> Type -> Type where
+  MkSeq : FingerTree (Elem e) -> Seq n e
+
+||| O(1). The empty sequence.
+export
+empty : Seq 0 e
+empty = MkSeq Empty
+
+||| O(1). A singleton sequence.
+export
+singleton : e -> Seq 1 e
+singleton a = MkSeq (Single (MkElem a))
+
+||| O(n). A sequence of length n with a the value of every element.
+export
+replicate : (n : Nat) -> (a : e) -> Seq n e
+replicate n a = MkSeq (replicate' n a)
+
+||| O(1). The number of elements in the sequence.
+export
+length : {n : Nat} -> Seq n a -> Nat
+length _ = n
+
+||| O(n). Reverse the sequence.
+export
+reverse : Seq n a -> Seq n a
+reverse (MkSeq tr) = MkSeq (reverseTree id tr)
+
+export infixr 5 `cons`
+||| O(1). Add an element to the left end of a sequence.
+export
+cons : e -> Seq n e -> Seq (S n) e
+a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
+
+export infixl 5 `snoc`
+||| O(1). Add an element to the right end of a sequence.
+export
+snoc : Seq n e -> e -> Seq (S n) e
+MkSeq tr `snoc` a = MkSeq (tr `snocTree` MkElem a)
+
+||| O(log(min(m, n))). Concatenate two sequences.
+export
+(++) : Seq m e -> Seq n e -> Seq (m + n) e
+MkSeq t1 ++ MkSeq t2 = MkSeq (addTree0 t1 t2)
+
+||| O(1). View from the left of the sequence.
+export
+viewl : Seq (S n) a -> (a, Seq n a)
+viewl (MkSeq tr) = case viewLTree tr of
+  Just (MkElem a, tr') => (a, MkSeq tr')
+  Nothing              => err "viewl"
+
+||| O(1). The first element of the sequence.
+export
+head : Seq (S n) a -> a
+head = fst . viewl
+
+||| O(1). The elements after the head of the sequence.
+export
+tail : Seq (S n) a -> Seq n a
+tail = snd . viewl
+
+||| O(1). View from the right of the sequence.
+export
+viewr : Seq (S n) a -> (Seq n a, a)
+viewr (MkSeq tr) = case viewRTree tr of
+  Just (tr', MkElem a) => (MkSeq tr', a)
+  Nothing              => err "viewr"
+
+||| O(1). The elements before the last element of the sequence.
+export
+init : Seq (S n) a -> Seq n a
+init = fst . viewr
+
+||| O(1). The last element of the sequence.
+export
+last : Seq (S n) a -> a
+last = snd . viewr
+
+||| O(n). Turn a vector into a sequence.
+export
+fromVect : Vect n a -> Seq n a
+fromVect xs = MkSeq (foldr (\x, t => MkElem x `consTree` t) Empty xs)
+
+||| O(n). Turn a list into a sequence.
+export
+fromList : (xs : List a) -> Seq (length xs) a
+fromList xs = fromVect (Vect.fromList xs)
+
+||| O(n). Turn a sequence into a vector.
+export
+toVect : {n :Nat} -> Seq n a -> Vect n a
+toVect _  {n = 0}   = []
+toVect ft {n = S _} =
+  let (x, ft') = viewl ft
+  in x :: toVect ft'
+
+||| O(log(min(i, n-i))). The element at the specified position.
+export
+index : (i : Nat) -> (t : Seq n a) -> {auto ok : LT i n} -> a
+index i (MkSeq t) = let (_, MkElem a) = lookupTree i t in a
+
+||| O(log(min(i, n-i))). The element at the specified position.
+||| Use Fin n to index instead.
+export
+index' : (t : Seq n a) -> (i : Fin n) -> a
+index' (MkSeq t) fn = let (_, MkElem a) = lookupTree (finToNat fn) t in a
+
+||| O(log(min(i, n-i))). Update the element at the specified position.
+export
+adjust : (f : a -> a) -> (i : Nat) -> (t : Seq n a) -> {auto ok : LT i n} -> Seq n a
+adjust f i (MkSeq t) = MkSeq $ adjustTree (const (map f)) i t
+
+||| O(log(min(i, n-i))). Replace the element at the specified position.
+export
+update : (i : Nat) -> a -> (t : Seq n a) -> {auto ok : LT i n} -> Seq n a
+update i a t = adjust (const a) i t
+
+||| O(log(min(i, n-i))). Split a sequence at a given position.
+export
+splitAt : (i : Nat) -> Seq (i + j) a -> (Seq i a, Seq j a)
+splitAt i (MkSeq xs) =
+  let (l, r) = split i xs
+  in (MkSeq l, MkSeq r)
+
+||| O(log(min(i, n-i))). The first i elements of a sequence.
+export
+take : (i : Nat) -> Seq (i + j) a -> Seq i a
+take i seq = fst (splitAt i seq)
+
+||| O(log(min(i, n-i))). Elements of a sequence after the first i.
+export
+drop : (i : Nat) -> Seq (i + j) a -> Seq j a
+drop i seq = snd (splitAt i seq)
+
+||| Dump the internal structure of the finger tree.
+export
+show' : Show a => Seq n a -> String
+show' (MkSeq tr) = showPrec Open tr
+
+public export
+implementation Eq a => Eq (Seq n a) where
+  MkSeq x == MkSeq y = x == y
+
+public export
+implementation Ord a => Ord (Seq n a) where
+  compare (MkSeq x) (MkSeq y) = compare x y
+
+public export
+implementation Functor (Seq n) where
+  map f (MkSeq tr) = MkSeq (map (map f) tr)
+
+public export
+implementation Foldable (Seq n) where
+  foldr f z (MkSeq tr) = foldr (f . unElem) z tr
+
+  foldl f z (MkSeq tr) = foldl (\acc, (MkElem elem) => f acc elem) z tr
+
+  toList (MkSeq tr) = toList' tr
+
+  null (MkSeq Empty) = True
+  null _ = False
+
+public export
+implementation Traversable (Seq n) where
+  traverse f (MkSeq tr) = MkSeq <$> traverse (map MkElem . f . unElem) tr
+
+public export
+implementation Show a => Show (Seq n a) where
+  showPrec p = showPrec p . toList
+
+public export
+implementation Zippable (Seq n) where
+  zipWith f (MkSeq x) (MkSeq y) = MkSeq (zipWith' f x y)
+
+  zipWith3 f (MkSeq x) (MkSeq y) (MkSeq z) = MkSeq (zipWith3' f x y z)
+
+  unzipWith f (MkSeq zs) = let (xs, ys) = unzipWith' f zs in (MkSeq xs, MkSeq ys)
+
+  unzipWith3 f (MkSeq ws) = let (xs, ys, zs) = unzipWith3' f ws in (MkSeq xs, MkSeq ys, MkSeq zs)
+
+||| This implementation works like a ZipList,
+||| and is differnt from that of Seq.Unsized.
+public export
+implementation {n : Nat} -> Applicative (Seq n) where
+  pure = replicate n
+  (<*>) = zipWith ($)
+
+public export
+implementation Sized (Seq n a) where
+  size (MkSeq s) = size s
diff --git a/src/Data/Seq/Unsized.idr b/src/Data/Seq/Unsized.idr
new file mode 100644
index 0000000..ce011cc
--- /dev/null
+++ b/src/Data/Seq/Unsized.idr
@@ -0,0 +1,224 @@
+||| General purpose two-end finite sequences.
+|||
+||| This is implemented by finger tree.
+module Data.Seq.Unsized
+
+import Control.WellFounded
+import public Data.Zippable
+
+import Data.Seq.Internal
+
+%default total
+
+||| A two-end finite sequences.
+export
+data Seq : Type -> Type where
+  MkSeq : FingerTree (Elem e) -> Seq e
+
+||| O(1). The empty sequence.
+export
+empty : Seq e
+empty = MkSeq Empty
+
+||| O(1). A singleton sequence.
+export
+singleton : e -> Seq e
+singleton a = MkSeq (Single (MkElem a))
+
+||| O(n). A sequence of length n with a the value of every element.
+export
+replicate : (n : Nat) -> (a : e) -> Seq e
+replicate n a = MkSeq (replicate' n a)
+
+||| O(1). The number of elements in the sequence.
+export
+length : Seq a -> Nat
+length (MkSeq tr) = length' tr
+
+||| O(n). Reverse the sequence.
+export
+reverse : Seq a -> Seq a
+reverse (MkSeq tr) = MkSeq (reverseTree id tr)
+
+export infixr 5 `cons`
+||| O(1). Add an element to the left end of a sequence.
+export
+cons : e -> Seq e -> Seq e
+a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
+
+export infixl 5 `snoc`
+||| O(1). Add an element to the right end of a sequence.
+export
+snoc : Seq e -> e -> Seq e
+MkSeq tr `snoc` a = MkSeq (tr `snocTree` MkElem a)
+
+||| O(log(min(m, n))). Concatenate two sequences.
+export
+(++) : Seq e -> Seq e -> Seq e
+MkSeq t1 ++ MkSeq t2 = MkSeq (addTree0 t1 t2)
+
+||| O(1). View from the left of the sequence.
+export
+viewl : Seq a -> Maybe (a, Seq a)
+viewl (MkSeq tr) = case viewLTree tr of
+  Just (MkElem a, tr') => Just (a, MkSeq tr')
+  Nothing              => Nothing
+
+||| O(1). The first element of the sequence.
+export
+head : Seq a -> Maybe a
+head s = fst <$> viewl s
+
+||| O(1). The elements after the head of the sequence.
+||| Returns an empty sequence when the sequence is empty.
+export
+tail : Seq a -> Seq a
+tail s = case viewl s of
+  Just (_, s') => s'
+  Nothing      => empty
+
+||| O(1). View from the right of the sequence.
+export
+viewr : Seq a -> Maybe (Seq a, a)
+viewr (MkSeq tr) = case viewRTree tr of
+  Just (tr', MkElem a) => Just (MkSeq tr', a)
+  Nothing              => Nothing
+
+||| O(1). The elements before the last element of the sequence.
+||| Returns an empty sequence when the sequence is empty.
+export
+init : Seq a -> Seq a
+init s = case viewr s of
+  Just (s', _) => s'
+  Nothing      => empty
+
+||| O(1). The last element of the sequence.
+export
+last : Seq a -> Maybe a
+last s = snd <$> viewr s
+
+||| O(n). Turn a list into a sequence.
+export
+fromList : List a -> Seq a
+fromList xs = MkSeq (foldr (\x, t => MkElem x `consTree` t) Empty xs)
+
+||| O(log(min(i, n-i))). The element at the specified position.
+export
+index : Nat -> Seq a -> Maybe a
+index i (MkSeq t) = if i < length' t
+  then let (_, MkElem a) = lookupTree i t in Just a
+  else Nothing
+
+||| O(log(min(i, n-i))). Update the element at the specified position.
+||| If the position is out of range, the original sequence is returned.
+export
+adjust : (a -> a) -> Nat -> Seq a -> Seq a
+adjust f i s@(MkSeq t) = if i < length' t
+  then MkSeq $ adjustTree (const (map f)) i t
+  else s
+
+||| 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 -> a -> Seq a -> Seq a
+update i a t = adjust (const a) i 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 -> Seq a -> (Seq a, Seq a)
+splitAt i s@(MkSeq t) = if i < length' t
+  then let (l, r) = split i t
+       in (MkSeq l, MkSeq r)
+  else (s, empty)
+
+||| 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 -> Seq a -> Seq a
+take i seq = fst (splitAt i seq)
+
+||| 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 -> Seq a -> Seq a
+drop i seq = snd (splitAt i seq)
+
+||| Dump the internal structure of the finger tree.
+export
+show' : Show a => Seq a -> String
+show' (MkSeq tr) = showPrec Open tr
+
+public export
+implementation Eq a => Eq (Seq a) where
+  MkSeq x == MkSeq y = x == y
+
+public export
+implementation Ord a => Ord (Seq a) where
+  compare (MkSeq x) (MkSeq y) = compare x y
+
+public export
+implementation Functor Seq where
+  map f (MkSeq tr) = MkSeq (map (map f) tr)
+
+public export
+implementation Foldable Seq where
+  foldr f z (MkSeq tr) = foldr (f . unElem) z tr
+
+  foldl f z (MkSeq tr) = foldl (\acc, (MkElem elem) => f acc elem) z tr
+
+  toList (MkSeq tr) = toList' tr
+
+  null (MkSeq Empty) = True
+  null _ = False
+
+public export
+implementation Traversable Seq where
+  traverse f (MkSeq tr) = MkSeq <$> traverse (map MkElem . f . unElem) tr
+
+public export
+implementation Show a => Show (Seq a) where
+  showPrec p = showPrec p . toList
+
+public export
+implementation Zippable Seq where
+  zipWith f (MkSeq x) (MkSeq y) = MkSeq (zipWith' f x y)
+
+  zipWith3 f (MkSeq x) (MkSeq y) (MkSeq z) = MkSeq (zipWith3' f x y z)
+
+  unzipWith f (MkSeq zs) = let (xs, ys) = unzipWith' f zs in (MkSeq xs, MkSeq ys)
+
+  unzipWith3 f (MkSeq ws) = let (xs, ys, zs) = unzipWith3' f ws in (MkSeq xs, MkSeq ys, MkSeq zs)
+
+public export
+implementation Semigroup (Seq a) where
+  (<+>) = (++)
+
+public export
+implementation Monoid (Seq a) where
+  neutral = empty
+
+||| This implementation is differnt from that of Seq.
+public export
+implementation Applicative Seq where
+  pure = singleton
+  fs <*> xs = foldMap (\f => map f xs) fs
+
+public export
+[ListLike] Alternative Seq where
+  empty = empty
+  a <|> b = a ++ b
+
+public export
+[MaybeLike] Alternative Seq where
+  empty = empty
+  MkSeq Empty <|> b = b
+  a <|> _ = a
+
+public export
+implementation Monad Seq where
+  xs >>= f = foldMap f xs
+
+public export
+implementation Sized (Seq a) where
+  size (MkSeq s) = size s