------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists, basic types and operations
------------------------------------------------------------------------

module Data.List.Base where

open import Data.Nat.Base using (; zero; suc; _+_; _*_)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool.Base
  using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Product as Prod using (_×_; _,_)
open import Function using (id; _∘_)
open import Relation.Nullary using (yes; no)
open import Relation.Unary using (Decidable)

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

open import Agda.Builtin.List public
  using (List; []; _∷_)

------------------------------------------------------------------------
-- Operations for transforming lists

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

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

infixr 5 _++_

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

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)

------------------------------------------------------------------------
-- Operations for reducing lists

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

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

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

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

------------------------------------------------------------------------
-- Operations for constructing lists

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

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

-- 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

-- Tabulation

applyUpTo :  {a} {A : Set a}  (  A)    List A
applyUpTo f zero    = []
applyUpTo f (suc n) = f zero  applyUpTo (f  suc) n

applyDownFrom :  {a} {A : Set a}  (  A)    List A
applyDownFrom f zero = []
applyDownFrom f (suc n) = f n  applyDownFrom f n

tabulate :  {a n} {A : Set a} (f : Fin n  A)  List A
tabulate {_} {zero}  f = []
tabulate {_} {suc n} f = f fzero  tabulate (f  fsuc)

lookup :  {a} {A : Set a} (xs : List A)  Fin (length xs)  A
lookup [] ()
lookup (x  xs) fzero = x
lookup (x  xs) (fsuc i) = lookup xs i

-- Numerical

upTo :   List 
upTo = applyUpTo id

downFrom :   List 
downFrom = applyDownFrom id

allFin :  n  List (Fin n)
allFin n = tabulate id

-- Other

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'

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

------------------------------------------------------------------------
-- Operations for deconstructing lists

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

filter :  {a p} {A : Set a} {P : A  Set p} 
         Decidable P  List A  List A
filter P? [] = []
filter P? (x  xs) with P? x
... | no  _ = filter P? xs
... | yes _ = x  filter P? xs

partition :  {a p} {A : Set a} {P : A  Set p} 
            Decidable P  List A  (List A × List A)
partition P? []       = ([] , [])
partition P? (x  xs) with P? x | partition P? xs
... | yes _ | (ys , zs) = (x  ys , zs)
... | no  _ | (ys , zs) = (ys , x  zs)

------------------------------------------------------------------------
-- Operations for reversing lists

reverse :  {a} {A : Set a}  List A  List A
reverse = foldl  rev x  x  rev) []

-- Snoc.

infixl 5 _∷ʳ_

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

-- Backwards initialisation

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

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------

gfilter = mapMaybe

-- Please use `filter` instead
boolFilter :  {a} {A : Set a}  (A  Bool)  List A  List A
boolFilter p = mapMaybe  x  if p x then just x else nothing)

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