module List where

open import Function
open import Data.Bool
open import Data.Nat
open import Data.Char
import Data.String as String
open String using (String)
import Data.List as L

data List A : Set where
  [] : List A
  _∷_ : A → List A → List A

infixr  _∷_ _++_

{-# COMPILED_DATA List [] [] (:) #-}

foldr : ∀ {A B} → (A → B → B) → B → List A → B
foldr f z []       = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

foldl : ∀ {A B} → (B → A → B) → B → List A → B
foldl f z []       = z
foldl f z (x ∷ xs) = foldl f (f z x) xs

map : ∀ {A B} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

and : List Bool → Bool
and = foldr _∧_ true

or : List Bool → Bool
or = foldr _∨_ false

any : ∀ {A} → (A → Bool) → List A → Bool
any p = or ∘ map p

all : ∀ {A} → (A → Bool) → List A → Bool
all p = and ∘ map p

filter : ∀ {A} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) = if p x then x ∷ filter p xs
                           else     filter p xs

_++_ : ∀ {A} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

length : ∀ {A} → List A → ℕ
length = foldr (λ _ → suc) 

reverse : ∀ {A} → List A → List A
reverse = foldl (λ xs x → x ∷ xs) []

dropWhile : ∀ {A} → (A → Bool) → List A → List A
dropWhile p [] = []
dropWhile p (x ∷ xs) =
  if p x then dropWhile p xs
         else x ∷ xs

fromList : ∀ {A} → L.List A → List A
fromList L.[] = []
fromList (L._∷_ x xs) = x ∷ fromList xs

toList : ∀ {A} → List A → L.List A
toList = foldr L._∷_ L.[]

stringFromList : List Char → String
stringFromList = String.fromList ∘ toList

stringToList : String → List Char
stringToList = fromList ∘ String.toList