module UVMHS.Core.Data.List where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data.LazyList ()

instance Null (𝐿 a) where 
  null :: 𝐿 a
null = 𝐿 a
forall a. 𝐿 a
empty𝐿
instance Append (𝐿 a) where 
  ⧺ :: 𝐿 a -> 𝐿 a -> 𝐿 a
(⧺) = 𝐿 a -> 𝐿 a -> 𝐿 a
forall a. 𝐿 a -> 𝐿 a -> 𝐿 a
append𝐿
instance Monoid (𝐿 a)
instance Functor 𝐿 where 
  map :: forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
map = (a -> b) -> 𝐿 a -> 𝐿 b
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
map𝐿
instance Return 𝐿 where
  return :: forall a. a -> 𝐿 a
return = a -> 𝐿 a
forall a. a -> 𝐿 a
single𝐿
instance Bind 𝐿 where 
  ≫= :: forall a b. 𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
(≫=) = 𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
forall a b. 𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
bind𝐿
instance Monad 𝐿
instance FunctorM 𝐿 where 
  mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐿 a -> m (𝐿 b)
mapM = (a -> m b) -> 𝐿 a -> m (𝐿 b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐿 a -> m (𝐿 b)
mapM𝐿
instance Single a (𝐿 a) where 
  single :: a -> 𝐿 a
single = a -> 𝐿 a
forall a. a -> 𝐿 a
single𝐿
instance ToIter a (𝐿 a) where 
  iter :: 𝐿 a -> 𝐼 a
iter = 𝐿 a -> 𝐼 a
forall a. 𝐿 a -> 𝐼 a
iter𝐿

empty𝐿 ∷ 𝐿 a
empty𝐿 :: forall a. 𝐿 a
empty𝐿 = 𝐿 a
forall a. 𝐿 a
Nil

single𝐿 ∷ a → 𝐿 a
single𝐿 :: forall a. a -> 𝐿 a
single𝐿 a
x = a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
forall a. 𝐿 a
Nil

cons𝐿 ∷ a → 𝐿 a → 𝐿 a
cons𝐿 :: forall a. a -> 𝐿 a -> 𝐿 a
cons𝐿 = a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
(:&)

snoc𝐿 ∷ 𝐿 a → a → 𝐿 a
snoc𝐿 :: forall a. 𝐿 a -> a -> 𝐿 a
snoc𝐿 𝐿 a
xs a
x = case 𝐿 a
xs of
  𝐿 a
Nil → a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
forall a. 𝐿 a
Nil
  a
x' :& 𝐿 a
xs' → a
x' a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a -> a -> 𝐿 a
forall a. 𝐿 a -> a -> 𝐿 a
snoc𝐿 𝐿 a
xs' a
x

unsnoc𝐿 ∷ 𝐿 a → 𝑂 (𝐿 a ∧ a)
unsnoc𝐿 :: forall a. 𝐿 a -> 𝑂 (𝐿 a ∧ a)
unsnoc𝐿 = \case
  𝐿 a
Nil → 𝑂 (𝐿 a ∧ a)
forall a. 𝑂 a
None
  a
x₀ :& 𝐿 a
xs₀ → (𝐿 a ∧ a) -> 𝑂 (𝐿 a ∧ a)
forall a. a -> 𝑂 a
Some ((𝐿 a ∧ a) -> 𝑂 (𝐿 a ∧ a)) -> (𝐿 a ∧ a) -> 𝑂 (𝐿 a ∧ a)
forall a b. (a -> b) -> a -> b
$
    let loop :: t -> 𝐿 t -> 𝐿 t ∧ t
loop t
x 𝐿 t
xs = case 𝐿 t
xs of
          𝐿 t
Nil → 𝐿 t
forall a. 𝐿 a
Nil 𝐿 t -> t -> 𝐿 t ∧ t
forall a b. a -> b -> a ∧ b
:* t
x
          t
x' :& 𝐿 t
xs' →
            let 𝐿 t
xsᵣ :* t
xᵣ = t -> 𝐿 t -> 𝐿 t ∧ t
loop t
x' 𝐿 t
xs'
            in (t
x t -> 𝐿 t -> 𝐿 t
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 t
xsᵣ) 𝐿 t -> t -> 𝐿 t ∧ t
forall a b. a -> b -> a ∧ b
:* t
xᵣ
    in a -> 𝐿 a -> 𝐿 a ∧ a
forall {t}. t -> 𝐿 t -> 𝐿 t ∧ t
loop a
x₀ 𝐿 a
xs₀

append𝐿 ∷ 𝐿 a → 𝐿 a → 𝐿 a
append𝐿 :: forall a. 𝐿 a -> 𝐿 a -> 𝐿 a
append𝐿 𝐿 a
xs 𝐿 a
ys = case 𝐿 a
xs of
  𝐿 a
Nil → 𝐿 a
ys
  a
x :& 𝐿 a
xs' → a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a -> 𝐿 a -> 𝐿 a
forall a. 𝐿 a -> 𝐿 a -> 𝐿 a
append𝐿 𝐿 a
xs' 𝐿 a
ys

map𝐿 ∷ (a → b) → 𝐿 a → 𝐿 b
map𝐿 :: forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
map𝐿 a -> b
f 𝐿 a
xs = case 𝐿 a
xs of
  𝐿 a
Nil → 𝐿 b
forall a. 𝐿 a
Nil
  a
x :& 𝐿 a
xs' → a -> b
f a
x b -> 𝐿 b -> 𝐿 b
forall a. a -> 𝐿 a -> 𝐿 a
:& (a -> b) -> 𝐿 a -> 𝐿 b
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f 𝐿 a
xs'

bind𝐿 ∷ 𝐿 a → (a → 𝐿 b) → 𝐿 b
bind𝐿 :: forall a b. 𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
bind𝐿 𝐿 a
xs a -> 𝐿 b
k = case 𝐿 a
xs of
  𝐿 a
Nil → 𝐿 b
forall a. 𝐿 a
Nil
  a
x :& 𝐿 a
xs' → 𝐿 b -> 𝐿 b -> 𝐿 b
forall a. 𝐿 a -> 𝐿 a -> 𝐿 a
append𝐿 (a -> 𝐿 b
k a
x) (𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
forall a b. 𝐿 a -> (a -> 𝐿 b) -> 𝐿 b
bind𝐿 𝐿 a
xs' a -> 𝐿 b
k)

mapM𝐿 ∷ (Monad m) ⇒ (a → m b) → 𝐿 a → m (𝐿 b)
mapM𝐿 :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐿 a -> m (𝐿 b)
mapM𝐿 a -> m b
f 𝐿 a
xs = case 𝐿 a
xs of
  𝐿 a
Nil → 𝐿 b -> m (𝐿 b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐿 b
forall a. 𝐿 a
Nil
  a
x :& 𝐿 a
xs' → do
    b
y ← a -> m b
f a
x
    𝐿 b
ys ← (a -> m b) -> 𝐿 a -> m (𝐿 b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐿 a -> m (𝐿 b)
mapM𝐿 a -> m b
f 𝐿 a
xs'
    𝐿 b -> m (𝐿 b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 b -> m (𝐿 b)) -> 𝐿 b -> m (𝐿 b)
forall a b. (a -> b) -> a -> b
$ b
y b -> 𝐿 b -> 𝐿 b
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 b
ys

cart ∷ 𝐿 (𝐿 a) → 𝐿 (𝐿 a)
cart :: forall a. 𝐿 (𝐿 a) -> 𝐿 (𝐿 a)
cart 𝐿 (𝐿 a)
Nil = 𝐿 a
forall a. 𝐿 a
Nil 𝐿 a -> 𝐿 (𝐿 a) -> 𝐿 (𝐿 a)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (𝐿 a)
forall a. 𝐿 a
Nil
cart (𝐿 a
xs:&𝐿 (𝐿 a)
xss) = do
  a
x ← 𝐿 a
xs
  𝐿 a
xs' ← 𝐿 (𝐿 a) -> 𝐿 (𝐿 a)
forall a. 𝐿 (𝐿 a) -> 𝐿 (𝐿 a)
cart 𝐿 (𝐿 a)
xss
  𝐿 a -> 𝐿 (𝐿 a)
forall a. a -> 𝐿 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> 𝐿 (𝐿 a)) -> 𝐿 a -> 𝐿 (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs'

swivelL ∷ 𝐿 a → a → a ∧ 𝐿 a
swivelL :: forall a. 𝐿 a -> a -> a ∧ 𝐿 a
swivelL 𝐿 a
Nil a
x = a
x a -> 𝐿 a -> a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
forall a. 𝐿 a
Nil
swivelL (a
x :& 𝐿 a
xs) a
y =
  let a
x' :* 𝐿 a
xs' = 𝐿 a -> a -> a ∧ 𝐿 a
forall a. 𝐿 a -> a -> a ∧ 𝐿 a
swivelL 𝐿 a
xs a
y
  in a
x a -> 𝐿 a -> a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* (a
x' a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs')

swivelR ∷ a → 𝐿 a → 𝐿 a ∧ a
swivelR :: forall {t}. t -> 𝐿 t -> 𝐿 t ∧ t
swivelR a
x 𝐿 a
Nil = 𝐿 a
forall a. 𝐿 a
Nil 𝐿 a -> a -> 𝐿 a ∧ a
forall a b. a -> b -> a ∧ b
:* a
x
swivelR a
x (a
y :& 𝐿 a
xs) =
  let 𝐿 a
xs' :* a
x' = a -> 𝐿 a -> 𝐿 a ∧ a
forall {t}. t -> 𝐿 t -> 𝐿 t ∧ t
swivelR a
y 𝐿 a
xs
  in (a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs') 𝐿 a -> a -> 𝐿 a ∧ a
forall a b. a -> b -> a ∧ b
:* a
x'

iswivelL ∷ 𝐿 (a ∧ i) → a → a ∧ 𝐿 (i ∧ a)
iswivelL :: forall a i. 𝐿 (a ∧ i) -> a -> a ∧ 𝐿 (i ∧ a)
iswivelL 𝐿 (a ∧ i)
Nil a
x = a
x a -> 𝐿 (i ∧ a) -> a ∧ 𝐿 (i ∧ a)
forall a b. a -> b -> a ∧ b
:* 𝐿 (i ∧ a)
forall a. 𝐿 a
Nil
iswivelL ((a
x :* i
i) :& 𝐿 (a ∧ i)
xis) a
y =
  let a
x' :* 𝐿 (i ∧ a)
ixs = 𝐿 (a ∧ i) -> a -> a ∧ 𝐿 (i ∧ a)
forall a i. 𝐿 (a ∧ i) -> a -> a ∧ 𝐿 (i ∧ a)
iswivelL 𝐿 (a ∧ i)
xis a
y
  in a
x a -> 𝐿 (i ∧ a) -> a ∧ 𝐿 (i ∧ a)
forall a b. a -> b -> a ∧ b
:* ((i
i i -> a -> i ∧ a
forall a b. a -> b -> a ∧ b
:* a
x') (i ∧ a) -> 𝐿 (i ∧ a) -> 𝐿 (i ∧ a)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (i ∧ a)
ixs)

iswivelR ∷ a → 𝐿 (i ∧ a) → 𝐿 (a ∧ i) ∧ a
iswivelR :: forall a i. a -> 𝐿 (i ∧ a) -> 𝐿 (a ∧ i) ∧ a
iswivelR a
x 𝐿 (i ∧ a)
Nil = 𝐿 (a ∧ i)
forall a. 𝐿 a
Nil 𝐿 (a ∧ i) -> a -> 𝐿 (a ∧ i) ∧ a
forall a b. a -> b -> a ∧ b
:* a
x
iswivelR a
x ((i
i :* a
y) :& 𝐿 (i ∧ a)
ixs) =
  let 𝐿 (a ∧ i)
xis :* a
x' = a -> 𝐿 (i ∧ a) -> 𝐿 (a ∧ i) ∧ a
forall a i. a -> 𝐿 (i ∧ a) -> 𝐿 (a ∧ i) ∧ a
iswivelR a
y 𝐿 (i ∧ a)
ixs
  in ((a
x a -> i -> a ∧ i
forall a b. a -> b -> a ∧ b
:* i
i) (a ∧ i) -> 𝐿 (a ∧ i) -> 𝐿 (a ∧ i)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (a ∧ i)
xis) 𝐿 (a ∧ i) -> a -> 𝐿 (a ∧ i) ∧ a
forall a b. a -> b -> a ∧ b
:* a
x'

zipSameLength ∷ 𝐿 a → 𝐿 b → 𝑂 (𝐿 (a ∧ b))
zipSameLength :: forall a b. 𝐿 a -> 𝐿 b -> 𝑂 (𝐿 (a ∧ b))
zipSameLength 𝐿 a
xs 𝐿 b
ys = case (𝐿 a
xs,𝐿 b
ys) of
  (𝐿 a
Nil,𝐿 b
Nil) → 𝐿 (a ∧ b) -> 𝑂 (𝐿 (a ∧ b))
forall a. a -> 𝑂 a
Some 𝐿 (a ∧ b)
forall a. 𝐿 a
Nil
  (a
x:&𝐿 a
xs',b
y:&𝐿 b
ys') → case 𝐿 a -> 𝐿 b -> 𝑂 (𝐿 (a ∧ b))
forall a b. 𝐿 a -> 𝐿 b -> 𝑂 (𝐿 (a ∧ b))
zipSameLength 𝐿 a
xs' 𝐿 b
ys' of
    𝑂 (𝐿 (a ∧ b))
None → 𝑂 (𝐿 (a ∧ b))
forall a. 𝑂 a
None
    Some 𝐿 (a ∧ b)
xys → 𝐿 (a ∧ b) -> 𝑂 (𝐿 (a ∧ b))
forall a. a -> 𝑂 a
Some (𝐿 (a ∧ b) -> 𝑂 (𝐿 (a ∧ b))) -> 𝐿 (a ∧ b) -> 𝑂 (𝐿 (a ∧ b))
forall a b. (a -> b) -> a -> b
$ (a
x a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
y) (a ∧ b) -> 𝐿 (a ∧ b) -> 𝐿 (a ∧ b)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (a ∧ b)
xys
  (𝐿 a, 𝐿 b)
_ → 𝑂 (𝐿 (a ∧ b))
forall a. 𝑂 a
None

split ∷ 𝐿 (a ∧ b) → 𝐿 a ∧ 𝐿 b
split :: forall a b. 𝐿 (a ∧ b) -> 𝐿 a ∧ 𝐿 b
split = \case
  𝐿 (a ∧ b)
Nil → 𝐿 a
forall a. 𝐿 a
Nil 𝐿 a -> 𝐿 b -> 𝐿 a ∧ 𝐿 b
forall a b. a -> b -> a ∧ b
:* 𝐿 b
forall a. 𝐿 a
Nil
  (a
x :* b
y) :& 𝐿 (a ∧ b)
xys →
    let 𝐿 a
xs :* 𝐿 b
ys = 𝐿 (a ∧ b) -> 𝐿 a ∧ 𝐿 b
forall a b. 𝐿 (a ∧ b) -> 𝐿 a ∧ 𝐿 b
split 𝐿 (a ∧ b)
xys
    in (a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs) 𝐿 a -> 𝐿 b -> 𝐿 a ∧ 𝐿 b
forall a b. a -> b -> a ∧ b
:* (b
y b -> 𝐿 b -> 𝐿 b
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 b
ys)

firstSome ∷ 𝐿 (𝑂 a) → 𝑂 a
firstSome :: forall a. 𝐿 (𝑂 a) -> 𝑂 a
firstSome = \case
  𝐿 (𝑂 a)
Nil → 𝑂 a
forall a. 𝑂 a
None
  𝑂 a
None :& 𝐿 (𝑂 a)
xOs → 𝐿 (𝑂 a) -> 𝑂 a
forall a. 𝐿 (𝑂 a) -> 𝑂 a
firstSome 𝐿 (𝑂 a)
xOs
  Some a
x :& 𝐿 (𝑂 a)
_ → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x