module UVMHS.Lib.Window where

import UVMHS.Core

import UVMHS.Lib.Pretty

-------------
-- WindowL --
-------------

data WindowL i a =
    ZerWindowL a
  | OneWindowL 𝔹 a i a
  deriving (WindowL i a -> WindowL i a -> Bool
(WindowL i a -> WindowL i a -> Bool)
-> (WindowL i a -> WindowL i a -> Bool) -> Eq (WindowL i a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i a. (Eq i, Eq a) => WindowL i a -> WindowL i a -> Bool
$c== :: forall i a. (Eq i, Eq a) => WindowL i a -> WindowL i a -> Bool
== :: WindowL i a -> WindowL i a -> Bool
$c/= :: forall i a. (Eq i, Eq a) => WindowL i a -> WindowL i a -> Bool
/= :: WindowL i a -> WindowL i a -> Bool
Eq,Eq (WindowL i a)
Eq (WindowL i a) =>
(WindowL i a -> WindowL i a -> Ordering)
-> (WindowL i a -> WindowL i a -> Bool)
-> (WindowL i a -> WindowL i a -> Bool)
-> (WindowL i a -> WindowL i a -> Bool)
-> (WindowL i a -> WindowL i a -> Bool)
-> (WindowL i a -> WindowL i a -> WindowL i a)
-> (WindowL i a -> WindowL i a -> WindowL i a)
-> Ord (WindowL i a)
WindowL i a -> WindowL i a -> Bool
WindowL i a -> WindowL i a -> Ordering
WindowL i a -> WindowL i a -> WindowL i a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall i a. (Ord i, Ord a) => Eq (WindowL i a)
forall i a. (Ord i, Ord a) => WindowL i a -> WindowL i a -> Bool
forall i a.
(Ord i, Ord a) =>
WindowL i a -> WindowL i a -> Ordering
forall i a.
(Ord i, Ord a) =>
WindowL i a -> WindowL i a -> WindowL i a
$ccompare :: forall i a.
(Ord i, Ord a) =>
WindowL i a -> WindowL i a -> Ordering
compare :: WindowL i a -> WindowL i a -> Ordering
$c< :: forall i a. (Ord i, Ord a) => WindowL i a -> WindowL i a -> Bool
< :: WindowL i a -> WindowL i a -> Bool
$c<= :: forall i a. (Ord i, Ord a) => WindowL i a -> WindowL i a -> Bool
<= :: WindowL i a -> WindowL i a -> Bool
$c> :: forall i a. (Ord i, Ord a) => WindowL i a -> WindowL i a -> Bool
> :: WindowL i a -> WindowL i a -> Bool
$c>= :: forall i a. (Ord i, Ord a) => WindowL i a -> WindowL i a -> Bool
>= :: WindowL i a -> WindowL i a -> Bool
$cmax :: forall i a.
(Ord i, Ord a) =>
WindowL i a -> WindowL i a -> WindowL i a
max :: WindowL i a -> WindowL i a -> WindowL i a
$cmin :: forall i a.
(Ord i, Ord a) =>
WindowL i a -> WindowL i a -> WindowL i a
min :: WindowL i a -> WindowL i a -> WindowL i a
Ord,Int -> WindowL i a -> ShowS
[WindowL i a] -> ShowS
WindowL i a -> String
(Int -> WindowL i a -> ShowS)
-> (WindowL i a -> String)
-> ([WindowL i a] -> ShowS)
-> Show (WindowL i a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i a. (Show i, Show a) => Int -> WindowL i a -> ShowS
forall i a. (Show i, Show a) => [WindowL i a] -> ShowS
forall i a. (Show i, Show a) => WindowL i a -> String
$cshowsPrec :: forall i a. (Show i, Show a) => Int -> WindowL i a -> ShowS
showsPrec :: Int -> WindowL i a -> ShowS
$cshow :: forall i a. (Show i, Show a) => WindowL i a -> String
show :: WindowL i a -> String
$cshowList :: forall i a. (Show i, Show a) => [WindowL i a] -> ShowS
showList :: [WindowL i a] -> ShowS
Show)

eWindowL ∷ a → WindowL i a
eWindowL :: forall a i. a -> WindowL i a
eWindowL = a -> WindowL i a
forall i a. a -> WindowL i a
ZerWindowL

iWindowL ∷ (Null a) ⇒ i → WindowL i a
iWindowL :: forall a i. Null a => i -> WindowL i a
iWindowL i
i = Bool -> a -> i -> a -> WindowL i a
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
False a
forall a. Null a => a
null i
i a
forall a. Null a => a
null

overflowL ∷ WindowL i a → 𝔹
overflowL :: forall i a. WindowL i a -> Bool
overflowL (ZerWindowL a
_) = Bool
False
overflowL (OneWindowL Bool
o a
_ i
_ a
_) = Bool
o

instance (Null a) ⇒ Null (WindowL i a) where 
  null :: WindowL i a
null = a -> WindowL i a
forall i a. a -> WindowL i a
ZerWindowL a
forall a. Null a => a
null
instance (Append a) ⇒ Append (WindowL i a) where
  ZerWindowL a
x ⧺ :: WindowL i a -> WindowL i a -> WindowL i a
⧺ ZerWindowL a
y = a -> WindowL i a
forall i a. a -> WindowL i a
ZerWindowL (a -> WindowL i a) -> a -> WindowL i a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y
  ZerWindowL a
x ⧺ OneWindowL Bool
o a
y i
i a
z = Bool -> a -> i -> a -> WindowL i a
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
o (a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y) i
i a
z
  OneWindowL Bool
True a
x i
i a
y ⧺ WindowL i a
_ = Bool -> a -> i -> a -> WindowL i a
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
True a
x i
i a
y
  OneWindowL Bool
False a
x i
i a
y ⧺ ZerWindowL a
z = Bool -> a -> i -> a -> WindowL i a
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
False a
x i
i (a -> WindowL i a) -> a -> WindowL i a
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
z
  OneWindowL Bool
False a
x i
i a
y ⧺ OneWindowL Bool
_ a
z i
_ a
_ = Bool -> a -> i -> a -> WindowL i a
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
True a
x i
i (a -> WindowL i a) -> a -> WindowL i a
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
z
instance (Monoid a) ⇒ Monoid (WindowL i a) 

instance ToIter a (WindowL a a) where
  iter :: WindowL a a -> 𝐼 a
iter (ZerWindowL a
x) = a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x
  iter (OneWindowL Bool
_ a
x a
i a
y) = [a] -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter [a
x,a
i,a
y]

mapWindowL ∷ (i → j) → (a → b) → WindowL i a → WindowL j b
mapWindowL :: forall i j a b. (i -> j) -> (a -> b) -> WindowL i a -> WindowL j b
mapWindowL i -> j
_ a -> b
f (ZerWindowL a
x) = b -> WindowL j b
forall i a. a -> WindowL i a
ZerWindowL (b -> WindowL j b) -> b -> WindowL j b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
mapWindowL i -> j
g a -> b
f (OneWindowL Bool
o a
x i
i a
y) = Bool -> b -> j -> b -> WindowL j b
forall i a. Bool -> a -> i -> a -> WindowL i a
OneWindowL Bool
o (a -> b
f a
x) (i -> j
g i
i) (b -> WindowL j b) -> b -> WindowL j b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
y

-------------
-- WindowR --
-------------

data WindowR i a =
    ZerWindowR a
  | OneWindowR 𝔹 a i a
  deriving (WindowR i a -> WindowR i a -> Bool
(WindowR i a -> WindowR i a -> Bool)
-> (WindowR i a -> WindowR i a -> Bool) -> Eq (WindowR i a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall i a. (Eq i, Eq a) => WindowR i a -> WindowR i a -> Bool
$c== :: forall i a. (Eq i, Eq a) => WindowR i a -> WindowR i a -> Bool
== :: WindowR i a -> WindowR i a -> Bool
$c/= :: forall i a. (Eq i, Eq a) => WindowR i a -> WindowR i a -> Bool
/= :: WindowR i a -> WindowR i a -> Bool
Eq,Eq (WindowR i a)
Eq (WindowR i a) =>
(WindowR i a -> WindowR i a -> Ordering)
-> (WindowR i a -> WindowR i a -> Bool)
-> (WindowR i a -> WindowR i a -> Bool)
-> (WindowR i a -> WindowR i a -> Bool)
-> (WindowR i a -> WindowR i a -> Bool)
-> (WindowR i a -> WindowR i a -> WindowR i a)
-> (WindowR i a -> WindowR i a -> WindowR i a)
-> Ord (WindowR i a)
WindowR i a -> WindowR i a -> Bool
WindowR i a -> WindowR i a -> Ordering
WindowR i a -> WindowR i a -> WindowR i a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall i a. (Ord i, Ord a) => Eq (WindowR i a)
forall i a. (Ord i, Ord a) => WindowR i a -> WindowR i a -> Bool
forall i a.
(Ord i, Ord a) =>
WindowR i a -> WindowR i a -> Ordering
forall i a.
(Ord i, Ord a) =>
WindowR i a -> WindowR i a -> WindowR i a
$ccompare :: forall i a.
(Ord i, Ord a) =>
WindowR i a -> WindowR i a -> Ordering
compare :: WindowR i a -> WindowR i a -> Ordering
$c< :: forall i a. (Ord i, Ord a) => WindowR i a -> WindowR i a -> Bool
< :: WindowR i a -> WindowR i a -> Bool
$c<= :: forall i a. (Ord i, Ord a) => WindowR i a -> WindowR i a -> Bool
<= :: WindowR i a -> WindowR i a -> Bool
$c> :: forall i a. (Ord i, Ord a) => WindowR i a -> WindowR i a -> Bool
> :: WindowR i a -> WindowR i a -> Bool
$c>= :: forall i a. (Ord i, Ord a) => WindowR i a -> WindowR i a -> Bool
>= :: WindowR i a -> WindowR i a -> Bool
$cmax :: forall i a.
(Ord i, Ord a) =>
WindowR i a -> WindowR i a -> WindowR i a
max :: WindowR i a -> WindowR i a -> WindowR i a
$cmin :: forall i a.
(Ord i, Ord a) =>
WindowR i a -> WindowR i a -> WindowR i a
min :: WindowR i a -> WindowR i a -> WindowR i a
Ord,Int -> WindowR i a -> ShowS
[WindowR i a] -> ShowS
WindowR i a -> String
(Int -> WindowR i a -> ShowS)
-> (WindowR i a -> String)
-> ([WindowR i a] -> ShowS)
-> Show (WindowR i a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall i a. (Show i, Show a) => Int -> WindowR i a -> ShowS
forall i a. (Show i, Show a) => [WindowR i a] -> ShowS
forall i a. (Show i, Show a) => WindowR i a -> String
$cshowsPrec :: forall i a. (Show i, Show a) => Int -> WindowR i a -> ShowS
showsPrec :: Int -> WindowR i a -> ShowS
$cshow :: forall i a. (Show i, Show a) => WindowR i a -> String
show :: WindowR i a -> String
$cshowList :: forall i a. (Show i, Show a) => [WindowR i a] -> ShowS
showList :: [WindowR i a] -> ShowS
Show)

eWindowR ∷ a → WindowR i a
eWindowR :: forall a i. a -> WindowR i a
eWindowR = a -> WindowR i a
forall i a. a -> WindowR i a
ZerWindowR

iWindowR ∷ (Null a) ⇒ i → WindowR i a
iWindowR :: forall a i. Null a => i -> WindowR i a
iWindowR i
i = Bool -> a -> i -> a -> WindowR i a
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
False a
forall a. Null a => a
null i
i a
forall a. Null a => a
null

overflowR ∷ WindowR i a → 𝔹
overflowR :: forall i a. WindowR i a -> Bool
overflowR (ZerWindowR a
_) = Bool
False
overflowR (OneWindowR Bool
o a
_ i
_ a
_) = Bool
o

instance (Null a) ⇒ Null (WindowR i a) where 
  null :: WindowR i a
null = a -> WindowR i a
forall i a. a -> WindowR i a
ZerWindowR a
forall a. Null a => a
null
instance (Append a) ⇒ Append (WindowR i a) where
  ZerWindowR a
x ⧺ :: WindowR i a -> WindowR i a -> WindowR i a
⧺ ZerWindowR a
y = a -> WindowR i a
forall i a. a -> WindowR i a
ZerWindowR (a -> WindowR i a) -> a -> WindowR i a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y
  OneWindowR Bool
o a
x i
i a
y ⧺ ZerWindowR a
z = Bool -> a -> i -> a -> WindowR i a
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
o a
x i
i (a -> WindowR i a) -> a -> WindowR i a
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
z
  WindowR i a
_ ⧺ OneWindowR Bool
True a
x i
i a
y = Bool -> a -> i -> a -> WindowR i a
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
True a
x i
i a
y
  ZerWindowR a
x ⧺ OneWindowR Bool
False a
y i
i a
z = Bool -> a -> i -> a -> WindowR i a
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
False (a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y) i
i a
z
  OneWindowR Bool
_ a
_ i
_ a
x ⧺ OneWindowR Bool
False a
y i
i a
z = Bool -> a -> i -> a -> WindowR i a
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
True (a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y) i
i a
z
instance (Monoid a) ⇒ Monoid (WindowR i a) 

instance ToIter a (WindowR a a) where
  iter :: WindowR a a -> 𝐼 a
iter (ZerWindowR a
x) = a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x
  iter (OneWindowR Bool
_ a
x a
i a
y) = [a] -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter [a
x,a
i,a
y]

mapWindowR ∷ (i → j) → (a → b) → WindowR i a → WindowR j b
mapWindowR :: forall i j a b. (i -> j) -> (a -> b) -> WindowR i a -> WindowR j b
mapWindowR i -> j
_ a -> b
f (ZerWindowR a
x) = b -> WindowR j b
forall i a. a -> WindowR i a
ZerWindowR (b -> WindowR j b) -> b -> WindowR j b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
mapWindowR i -> j
g a -> b
f (OneWindowR Bool
o a
x i
i a
y) = Bool -> b -> j -> b -> WindowR j b
forall i a. Bool -> a -> i -> a -> WindowR i a
OneWindowR Bool
o (a -> b
f a
x) (i -> j
g i
i) (b -> WindowR j b) -> b -> WindowR j b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
y

makePrettySum ''WindowL
makePrettySum ''WindowR

-- RENDER --

renderWindowL ∷ WindowL Doc Doc → Doc
renderWindowL :: WindowL Doc Doc -> Doc
renderWindowL WindowL Doc Doc
dL
  | WindowL Doc Doc -> Bool
forall i a. WindowL i a -> Bool
overflowL WindowL Doc Doc
dL = [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
      [ WindowL Doc Doc -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat WindowL Doc Doc
dL
      , Formats -> Doc -> Doc
ppFormat ([Format] -> Formats
forall t. ToIter Format t => t -> Formats
formats [Color -> Format
BG Color
grayLight]) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"…"
      ]
  | Bool
otherwise = WindowL Doc Doc -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat WindowL Doc Doc
dL

renderWindowR ∷ WindowR Doc Doc → Doc
renderWindowR :: WindowR Doc Doc -> Doc
renderWindowR WindowR Doc Doc
dR
  | WindowR Doc Doc -> Bool
forall i a. WindowR i a -> Bool
overflowR WindowR Doc Doc
dR = [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
      [ Formats -> Doc -> Doc
ppFormat ([Format] -> Formats
forall t. ToIter Format t => t -> Formats
formats [Color -> Format
BG Color
grayLight]) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"…"
      , WindowR Doc Doc -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat WindowR Doc Doc
dR
      ]
  | Bool
otherwise = WindowR Doc Doc -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat WindowR Doc Doc
dR
        
-- import UVMHS.Core

-- ------------
-- -- Swivel --
-- ------------
-- 
-- swivelL ∷ 𝐿 a → a → a ∧ 𝐿 a
-- swivelL Nil x = x :* Nil
-- swivelL (x :& xs) y =
--   let x' :* xs' = swivelL xs y
--   in x :* (x' :& xs')
-- 
-- swivelR ∷ a → 𝐿 a → 𝐿 a ∧ a
-- swivelR x Nil = Nil :* x
-- swivelR x (y :& xs) =
--   let xs' :* x' = swivelR y xs
--   in (x :& xs') :* x'
-- 
-- iswivelL ∷ 𝐿 (a ∧ i) → a → a ∧ 𝐿 (i ∧ a)
-- iswivelL Nil x = x :* Nil
-- iswivelL ((x :* i) :& xis) y =
--   let x' :* ixs = iswivelL xis y
--   in x :* ((i :* x') :& ixs)
-- 
-- iswivelR ∷ a → 𝐿 (i ∧ a) → 𝐿 (a ∧ i) ∧ a
-- iswivelR x Nil = Nil :* x
-- iswivelR x ((i :* y) :& ixs) =
--   let xis :* x' = iswivelR y ixs
--   in ((x :* i) :& xis) :* x'
-- 
-- ------------
-- -- Window --
-- ------------
-- 
-- data Window i a = 
--     WindowE a
--   | WindowS ℕ64 a i (𝐼 (a ∧ i)) a
-- 
-- windowI ∷ (Null a) ⇒ i → Window i a
-- windowI i = WindowS one null i null null
-- 
-- instance (Null a) ⇒ Null (Window i a) where null = WindowE null
-- instance (Append a) ⇒ Append (Window i a) where
--   WindowE x₁ ⧺ WindowE x₂ = WindowE $ x₁ ⧺ x₂
--   WindowE x₁ ⧺ WindowS n x₂₁ i₂ xis₂ x₂₂ = WindowS n (x₁ ⧺ x₂₁) i₂ xis₂ x₂₂
--   WindowS n x₁₁ i₁ xis₁ x₁₂ ⧺ WindowE x₂ = WindowS n x₁₁ i₁ xis₁ $ x₁₂ ⧺ x₂
--   WindowS n₁ x₁₁ i₁ xis₁ x₁₂ ⧺ WindowS n₂ x₂₁ i₂ xis₂ x₂₂ = 
--     let xis' = xis₁ ⧺ single ((x₁₁ ⧺ x₂₁) :* i₂) ⧺ xis₂
--     in WindowS (n₁ + n₂) x₁₁ i₁ xis' x₂₂
-- instance (Monoid a) ⇒ Monoid (Window i a)
-- 
-- -------------
-- -- FWindow --
-- -------------
-- 
-- windowWidth ∷ ℕ64
-- windowWidth = 𝕟64 2
-- 
-- data FWindow i a = 
--     FWindowE a
--   | FWindowS ℕ64 a i (𝐿 (a ∧ i)) a
-- 
-- fwindowI ∷ (Null a) ⇒ i → FWindow i a
-- fwindowI i = FWindowS one null i null null
-- 
-- instance (Null a) ⇒ Null (FWindow i a) where null = FWindowE null
-- instance (Append a) ⇒ Append (FWindow i a) where
--   FWindowE x₁ ⧺ FWindowE x₂ = FWindowE $ x₁ ⧺ x₂
--   FWindowE x₁ ⧺ FWindowS n x₂₁ i₂ xis₂ x₂₂ = FWindowS n (x₁ ⧺ x₂₁) i₂ xis₂ x₂₂
--   FWindowS n x₁₁ i₁ xis₁ x₁₂ ⧺ FWindowE x₂ = FWindowS n x₁₁ i₁ xis₁ $ x₁₂ ⧺ x₂
--   FWindowS n₁ x₁₁ i₁ xis₁ x₁₂ ⧺ FWindowS n₂ x₂₁ i₂ xis₂ x₂₂ = 
--     | n₂ ≡ windowWidth + 1 = FWindowS n₂ (x₁₂ ⧺ x₂₁) i₂ xis₂ x₂₂
--     let n = n₁ + n₂
--     in case n > (windowWidth + one) of
--       True →
--         let xis :* xi = swivelR (x₁₁ :* i₁) $ xis₁ ⧺ ((x₁₂ ⧺ x₂₁) :* i₂) :& xis₂
--             (x' :* i') :* xis' = swivelL (lastN windowWidth xis) xi
--         in FWindowS (windowWidth + one) x' i' xis' x₂₂
--       False →
--         let xis = xis₁ ⧺ ((x₁₂ ⧺ x₂₁) :* i₂) :& xis₂
--         in FWindowS n x₁₁ i₁ xis x₂₂
-- instance (Monoid a) ⇒ Monoid (FWindow i a)
-- 
-- data LWindow i a = 
--     LWindowE a
--   | LWindowS ℕ64 a i (𝐼 (a ∧ i)) a
-- 
-- lwindowI ∷ (Null a) ⇒ i → LWindow i a
-- lwindowI i = LWindowS null i null null
-- 
-- instance (Null a) ⇒ Null (LWindow i a) where null = LWindowE null
-- instance (Append a) ⇒ Append (LWindow i a) where
--   LWindowE x₁ ⧺ LWindowE x₂ = LWindowE $ x₁ ⧺ x₂
--   LWindowE x₁ ⧺ LWindowS x₂₁ i₂ xis₂ x₂₂ = LWindowS (x₁ ⧺ x₂₁) i₂ xis₂ x₂₂
--   LWindowS x₁₁ i₁ xis₁ x₁₂ ⧺ LWindowE x₂ = LWindowS x₁₁ i₁ xis₁ $ x₁₂ ⧺ x₂
--   LWindowS x₁₁ i₁ xis₁ x₁₂ ⧺ LWindowS x₂₁ i₂ xis₂ x₂₂ = 
--     let xis' = reverse $ iter $ firstN (nat windowWidth) $ list $ reverse $ xis₁ ⧺ single ((x₁₁ ⧺ x₂₁) :* i₂) ⧺ xis₂
--     in LWindowS x₁₁ i₁ xis' x₂₂
-- instance (Monoid a) ⇒ Monoid (LWindow i a)
-- 
-- -- data WindowR i a = WindowR 
-- --   { windowRHead ∷ 𝐿 (a ∧ i)
-- --   , windowRTail ∷ a
-- --   } deriving (Eq,Ord,Show)
-- -- 
-- -- instance (Null a) ⇒ Null (WindowR i a) where null = WindowR null null
-- -- instance (Append a) ⇒ Append (WindowR i a) where
-- --   WindowR xss₁ x₁ ⧺ WindowR xss₂ x₂ = case xxs₂ of
-- --     Nil → WindowL xss₁ (x₁ ⧺ x₂)
-- --     (x₂' :* s₂) :& xss₂' → WindowL (xss₁ ⧺ ((x₁ ⧺ x₂') :* xss₂)) x₂
-- -- instance (Monoid a) ⇒ Monoid (WindowL i a)
-- -- instance ToStream a (SepL a a) where 
-- --   stream (WindowL x sxs) = stream $ list $ concat
-- --     [ single x 
-- --     , concat $ mapOn (reverse sxs) $ \ (i' :* x') → 
-- --         iter [i',x']
-- --     ]
-- -- instance ToIter a (WindowL a a) where iter = iter ∘ stream
-- -- 
-- -- data WindowL i a = WindowL 
-- --   { windowLHead ∷ a
-- --   , windowLTail ∷ 𝐿 (i ∧ a)
-- --   } deriving (Eq,Ord,Show)
-- -- 
-- -- instance (Null a) ⇒ Null (WindowL i a) where null = WindowL null null
-- -- instance (Append a) ⇒ Append (WindowL i a) where
-- --   WindowL x₁ sxs₁ ⧺ WindowL x₂ sxs₂ = case sxs₁ of
-- --     Nil → WindowL (x₁ ⧺ x₂) sxs₂
-- --     (s₁ :* x₁') :& sxs₁' → WindowL x₁ $ firstN windowWidth $ sxs₂ ⧺ ((s₁ :* (x₁' ⧺ x₂)) :& sxs₁)
-- -- instance (Monoid a) ⇒ Monoid (WindowL i a)
-- -- instance ToStream a (WindowL a a) where 
-- --   stream (WindowL x sxs) = stream $ list $ concat
-- --     [ single x 
-- --     , concat $ mapOn (reverse sxs) $ \ (i' :* x') → 
-- --         iter [i',x']
-- --     ]
-- -- instance ToIter a (WindowL a a) where iter = iter ∘ stream
-- --