------------------------------------------------------------------------
-- Lists
------------------------------------------------------------------------
{-# OPTIONS --universe-polymorphism #-}

module Data.List where

open import Data.Nat
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Product as Prod using (_×_; _,_)
open import Data.Function
open import Algebra
import Relation.Binary.PropositionalEquality as PropEq
import Algebra.FunctionProperties as FunProp

infixr 5 _∷_ _++_

------------------------------------------------------------------------
-- Types

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A)  List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

------------------------------------------------------------------------
-- Some operations

-- * Basic functions

[_] :  {a} {A : Set a}  A  List A
[ x ] = x  []

_++_ :  {a} {A : Set a}  List A  List A  List A
[]       ++ ys = ys
(x  xs) ++ ys = x  (xs ++ ys)

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ :  {a} {A : Set a}  List A  A  List A
xs ∷ʳ x = xs ++ [ x ]

null :  {a} {A : Set a}  List A  Bool
null []       = true
null (x  xs) = false

-- * List transformations

map :  {a b} {A : Set a} {B : Set b}  (A  B)  List A  List B
map f []       = []
map f (x  xs) = f x  map f xs

reverse :  {a} {A : Set a}  List A  List A
reverse xs = rev xs []
  where
  rev :  {a} {A : Set a}  List A  List A  List A
  rev []       ys = ys
  rev (x  xs) ys = rev xs (x  ys)

replicate :  {a} {A : Set a}  (n : )  A  List A
replicate zero    x = []
replicate (suc n) x = x  replicate n x

zipWith :  {a b c} {A : Set a} {B : Set b} {C : Set c}
           (A  B  C)  List A  List B  List C
zipWith f (x  xs) (y  ys) = f x y  zipWith f xs ys
zipWith f _        _        = []

zip :  {a b} {A : Set a} {B : Set b}  List A  List B  List (A × B)
zip = zipWith (_,_)

intersperse :  {a} {A : Set a}  A  List A  List A
intersperse x []           = []
intersperse x (y  [])     = [ y ]
intersperse x (y  z  zs) = y  x  intersperse x (z  zs)

-- * Reducing lists (folds)

foldr :  {a b} {A : Set a} {B : Set b}  (A  B  B)  B  List A  B
foldr c n []       = n
foldr c n (x  xs) = c x (foldr c n xs)

foldl :  {a b} {A : Set a} {B : Set b}  (A  B  A)  A  List B  A
foldl c n []       = n
foldl c n (x  xs) = foldl c (c n x) xs

-- ** Special folds

concat :  {a} {A : Set a}  List (List A)  List A
concat = foldr _++_ []

concatMap :  {a b} {A : Set a} {B : Set b} 
            (A  List B)  List A  List B
concatMap f = concat  map f

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

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

any :  {a} {A : Set a}  (A  Bool)  List A  Bool
any p = or  map p

all :  {a} {A : Set a}  (A  Bool)  List A  Bool
all p = and  map p

sum : List   
sum = foldr _+_ 0

product : List   
product = foldr _*_ 1

length :  {a} {A : Set a}  List A  
length = foldr  _  suc) 0

-- * Building lists

-- ** Scans

scanr :  {a b} {A : Set a} {B : Set b} 
        (A  B  B)  B  List A  List B
scanr f e []       = e  []
scanr f e (x  xs) with scanr f e xs
... | []     = []                -- dead branch
... | y  ys = f x y  y  ys

scanl :  {a b} {A : Set a} {B : Set b} 
        (A  B  A)  A  List B  List A
scanl f e []       = e  []
scanl f e (x  xs) = e  scanl f (f e x) xs

-- ** Unfolding

-- Unfold. Uses a measure (a natural number) to ensure termination.

unfold :  {a b} {A : Set a} (B :   Set b)
         (f :  {n}  B (suc n)  Maybe (A × B n)) 
          {n}  B n  List A
unfold B f {n = zero}  s = []
unfold B f {n = suc n} s with f s
... | nothing       = []
... | just (x , s') = x  unfold B f s'

-- downFrom 3 = 2 ∷ 1 ∷ 0 ∷ [].

downFrom :   List 
downFrom n = unfold Singleton f (wrap n)
  where
  data Singleton :   Set where
    wrap : (n : )  Singleton n

  f :  {n}  Singleton (suc n)  Maybe ( × Singleton n)
  f {n} (wrap .(suc n)) = just (n , wrap n)

-- ** Conversions

fromMaybe :  {a} {A : Set a}  Maybe A  List A
fromMaybe (just x) = [ x ]
fromMaybe nothing  = []

-- * Sublists

-- ** Extracting sublists

take :  {a} {A : Set a}    List A  List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x  xs) = x  take n xs

drop :  {a} {A : Set a}    List A  List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x  xs) = drop n xs

splitAt :  {a} {A : Set a}    List A  (List A × List A)
splitAt zero    xs       = ([] , xs)
splitAt (suc n) []       = ([] , [])
splitAt (suc n) (x  xs) with splitAt n xs
... | (ys , zs) = (x  ys , zs)

takeWhile :  {a} {A : Set a}  (A  Bool)  List A  List A
takeWhile p []       = []
takeWhile p (x  xs) with p x
... | true  = x  takeWhile p xs
... | false = []

dropWhile :  {a} {A : Set a}  (A  Bool)  List A  List A
dropWhile p []       = []
dropWhile p (x  xs) with p x
... | true  = dropWhile p xs
... | false = x  xs

span :  {a} {A : Set a}  (A  Bool)  List A  (List A × List A)
span p []       = ([] , [])
span p (x  xs) with p x
... | true  = Prod.map (_∷_ x) id (span p xs)
... | false = ([] , x  xs)

break :  {a} {A : Set a}  (A  Bool)  List A  (List A × List A)
break p = span (not  p)

inits :  {a} {A : Set a}   List A  List (List A)
inits []       = []  []
inits (x  xs) = []  map (_∷_ x) (inits xs)

tails :  {a} {A : Set a}  List A  List (List A)
tails []       = []  []
tails (x  xs) = (x  xs)  tails xs

infixl 5 _∷ʳ'_

data InitLast {a} {A : Set a} : List A  Set a where
  []    : InitLast []
  _∷ʳ'_ : (xs : List A) (x : A)  InitLast (xs ∷ʳ x)

initLast :  {a} {A : Set a} (xs : List A)  InitLast xs
initLast []               = []
initLast (x  xs)         with initLast xs
initLast (x  .[])        | []       = [] ∷ʳ' x
initLast (x  .(ys ∷ʳ y)) | ys ∷ʳ' y = (x  ys) ∷ʳ' y

-- * Searching lists

-- ** Searching with a predicate

-- A generalised variant of filter.

gfilter :  {a b} {A : Set a} {B : Set b} 
          (A  Maybe B)  List A  List B
gfilter p []       = []
gfilter p (x  xs) with p x
... | just y  = y  gfilter p xs
... | nothing =     gfilter p xs

filter :  {a} {A : Set a}  (A  Bool)  List A  List A
filter p = gfilter  x  if p x then just x else nothing)

partition :  {a} {A : Set a}  (A  Bool)  List A  (List A × List A)
partition p []       = ([] , [])
partition p (x  xs) with p x | partition p xs
... | true  | (ys , zs) = (x  ys , zs)
... | false | (ys , zs) = (ys , x  zs)

------------------------------------------------------------------------
-- List monoid

monoid : Set  Monoid
monoid A = record
  { Carrier  = List A
  ; _≈_      = _≡_
  ; _∙_      = _++_
  ; ε        = []
  ; isMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = assoc
      ; ∙-cong        = cong₂ _++_
      }
    ; identity = ((λ _  refl) , identity)
    }
  }
  where
  open PropEq
  open FunProp _≡_

  identity : RightIdentity [] _++_
  identity []       = refl
  identity (x  xs) = cong (_∷_ x) (identity xs)

  assoc : Associative _++_
  assoc []       ys zs = refl
  assoc (x  xs) ys zs = cong (_∷_ x) (assoc xs ys zs)

------------------------------------------------------------------------
-- List monad

open import Category.Monad

monad : RawMonad List
monad = record
  { return = λ x  x  []
  ; _>>=_  = λ xs f  concat (map f xs)
  }

monadZero : RawMonadZero List
monadZero = record
  { monad = monad
  ;      = []
  }

monadPlus : RawMonadPlus List
monadPlus = record
  { monadZero = monadZero
  ; _∣_       = _++_
  }

------------------------------------------------------------------------
-- Monadic functions

private
 module Monadic {M} (Mon : RawMonad M) where

  open RawMonad Mon

  sequence :  {A : Set}  List (M A)  M (List A)
  sequence []       = return []
  sequence (x  xs) = _∷_ <$> x  sequence xs

  mapM :  {a} {A : Set a} {B}  (A  M B)  List A  M (List B)
  mapM f = sequence  map f

open Monadic public