open import 1Lab.Type.Sigma
open import 1Lab.Path
open import 1Lab.Type

open import Data.Product.NAry
open import Data.Maybe.Base
open import Data.Dec.Base
open import Data.Fin.Base
open import Data.Bool

open import Meta.Traversable
open import Meta.Foldable
open import Meta.Append
open import Meta.Idiom
open import Meta.Bind
open import Meta.Alt

module Data.List.Base where


# The type of listsπ

This module contains the definition of the type of lists, and some basic operations on lists. Properties of these operations are in the module Data.List, not here.

private variable
β : Level
A B : Type β

infixr 20 _β·_

data List {β} (A : Type β) : Type β where
[] : List A
_β·_ : A β List A β List A

{-# BUILTIN LIST List #-}


One of the first things we set up is list literal syntax (the From-product class) for lists. The list corresponding to an n-ary product is the list of its elements.

instance
From-prod-List : From-product A (Ξ» _ β List A)
From-prod-List .From-product.from-prod = go where
go : β n β Vecβ A n β List A
go zero xs                = []
go (suc zero) xs          = xs β· []
go (suc (suc n)) (x , xs) = x β· go (suc n) xs

-- Test:
_ : Path (List Nat) [ 1 , 2 , 3 ] (1 β· 2 β· 3 β· [])
_ = refl


## βFieldsβπ

head : A β List A β A
head _   (x β· _) = x

tail : List A β List A
tail []       = []
tail (_ β· xs) = xs


## Eliminationπ

As with any inductive type, the type of lists-of-As has a canonically-defined eliminator, but it also has some fairly popular recursors, called βfoldsβ:

List-elim
: β {β β'} {A : Type β} (P : List A β Type β')
β P []
β (β x xs β P xs β P (x β· xs))
β β x β P x
List-elim P p[] pβ· []       = p[]
List-elim P p[] pβ· (x β· xs) = pβ· x xs (List-elim P p[] pβ· xs)

instance
Foldable-List : Foldable (eff List)
Foldable-List .foldr f x = List-elim _ x (Ξ» x _ β f x)

Traversable-List : Traversable (eff List)
Traversable-List = record { traverse = go } where
go
: β {M : Effect} β¦ _ : Idiom M β¦ (let module M = Effect M) {β β'}
{a : Type β} {b : Type β'}
β (a β M.β b) β List a β M.β (List b)
go f []       = pure []
go f (x β· xs) = β¦ f x β· go f xs β¦

foldl : (B β A β B) β B β List A β B
foldl f x []       = x
foldl f x (a β· as) = foldl f (f x a) as


## Functorial actionπ

Itβs also possible to lift a function A β B to a function List A β List B.

instance
Map-List : Map (eff List)
Map-List = record { map = go } where
go : (A β B) β List A β List B
go f []       = []
go f (x β· xs) = f x β· go f xs


## Monoidal structureπ

We can define concatenation of lists by recursion:

_++_ : β {β} {A : Type β} β List A β List A β List A
[]       ++ ys = ys
(x β· xs) ++ ys = x β· (xs ++ ys)

infixr 5 _++_

instance
Append-List : β {β} {A : Type β} β Append (List A)
Append-List = record { mempty = [] ; _<>_ = _++_ }

map-up : (Nat β A β B) β Nat β List A β List B
map-up f _ []       = []
map-up f n (x β· xs) = f n x β· map-up f (suc n) xs

length : List A β Nat
length []       = zero
length (x β· xs) = suc (length xs)

concat : List (List A) β List A
concat [] = []
concat (x β· xs) = x ++ concat xs

count : Nat β List Nat
count zero = []
count (suc n) = 0 β· map suc (count n)

reverse : List A β List A
reverse = go [] where
go : List A β List A β List A
go acc [] = acc
go acc (x β· xs) = go (x β· acc) xs

_β·r_ : List A β A β List A
xs β·r x = xs ++ (x β· [])

infixl 20 _β·r_

all=? : (A β A β Bool) β List A β List A β Bool
all=? eq=? [] [] = true
all=? eq=? [] (x β· ys) = false
all=? eq=? (x β· xs) [] = false
all=? eq=? (x β· xs) (y β· ys) = and (eq=? x y) (all=? eq=? xs ys)

enumerate : β {β} {A : Type β} β List A β List (Nat Γ A)
enumerate = go 0 where
go : Nat β List _ β List (Nat Γ _)
go x [] = []
go x (a β· b) = (x , a) β· go (suc x) b

take : β {β} {A : Type β} β Nat β List A β List A
take 0       xs       = []
take (suc n) []       = []
take (suc n) (x β· xs) = x β· take n xs

drop : β {β} {A : Type β} β Nat β List A β List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x β· xs) = drop n xs

split-at : β {β} {A : Type β} β Nat β List A β List A Γ List A
split-at 0       xs       = [] , xs
split-at (suc n) []       = [] , []
split-at (suc n) (x β· xs) = Γ-mapβ (x β·_) (split-at n xs)

span : β {β} {A : Type β} (p : A β Bool) β List A β List A Γ List A
span p [] = [] , []
span p (x β· xs) with p x
... | true  = Γ-mapβ (x β·_) (span p xs)
... | false = [] , x β· xs

filter : β {β} {A : Type β} (p : A β Bool) β List A β List A
filter p [] = []
filter p (x β· xs) with p x
... | true  = x β· filter p xs
... | false = filter p xs

intercalate : β {β} {A : Type β} (x : A) (xs : List A) β List A
intercalate x []           = []
intercalate x (y β· [])     = y β· []
intercalate x (y β· z β· xs) = y β· x β· intercalate x (z β· xs)

zip : β {β β'} {A : Type β} {B : Type β'} β List A β List B β List (A Γ B)
zip [] _ = []
zip _ [] = []
zip (a β· as) (b β· bs) = (a , b) β· zip as bs

unzip : β {β β'} {A : Type β} {B : Type β'} β List (A Γ B) β List A Γ List B
unzip [] = [] , []
unzip ((a , b) β· xs) = Γ-map (a β·_) (b β·_) (unzip xs)

instance
Idiom-List : Idiom (eff List)
Idiom-List .pure a = a β· []
Idiom-List ._<*>_ f a = concat ((_<$> a) <$> f)

Bind-List : Bind (eff List)
Bind-List ._>>=_ a f = concat (f <\$> a)

Alt-List : Alt (eff List)
Alt-List .Alt.fail  = []
Alt-List .Alt._<|>_ = _<>_


## Predicatesπ

We can define a function that determines if a boolean-valued predicate holds on every element of a list.

all-of : β {β} {A : Type β} β (A β Bool) β List A β Bool
all-of f [] = true
all-of f (x β· xs) = and (f x) (all-of f xs)


Dually, we can also define a function that determines if a boolean-valued predicate holds on some element of a list.

any-of : β {β} {A : Type β} β (A β Bool) β List A β Bool
any-of f [] = false
any-of f (x β· xs) = or (f x) (any-of f xs)

β·-head-inj : β {x y : A} {xs ys} β (x β· xs) β‘ (y β· ys) β x β‘ y

β·-tail-inj : β {x y : A} {xs ys} β (x β· xs) β‘ (y β· ys) β xs β‘ ys
β·-tail-inj p = ap tail p

β·β [] : β {x : A} {xs} β Β¬ (x β· xs) β‘ []
β·β [] {A = A} p = subst distinguish p tt where
distinguish : List A β Type
distinguish []     = β₯
distinguish (_ β· _) = β€

instance
Discrete-List : β β¦ d : Discrete A β¦ β Discrete (List A)
Discrete-List {x = []}     {y = []}     = yes refl
Discrete-List {x = []}     {y = x β· y}  = no Ξ» p β β·β [] (sym p)
Discrete-List {x = x β· xs} {y = []}     = no β·β []
Discrete-List {x = x β· xs} {y = y β· ys} = case x β‘? y of Ξ» where
(yes x=y) β case Discrete-List {x = xs} {ys} of Ξ» where
(yes xs=ys) β yes (apβ _β·_ x=y xs=ys)
(no  xsβ ys) β no Ξ» p β xsβ ys (β·-tail-inj p)
(no xβ y)      β no Ξ» p β xβ y (β·-head-inj p)

traverse-up
: β {M : Effect} β¦ _ : Idiom M β¦ (let module M = Effect M) {β β'}
{a : Type β} {b : Type β'}
β (Nat β a β M.β b) β Nat β List a β M.β (List b)
traverse-up f n xs = sequence (map-up f n xs)

lookup : β¦ _ : Discrete A β¦ β A β List (A Γ B) β Maybe B
lookup x [] = nothing
lookup x ((k , v) β· xs) with x β‘? k
... | yes _ = just v
... | no  _ = lookup x xs

_!_ : (l : List A) β Fin (length l) β A
(x β· xs) ! fzero  = x
(x β· xs) ! fsuc n = xs ! n

tabulate : β {n} (f : Fin n β A) β List A
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f fzero β· tabulate (f β fsuc)