module list where open import level open import bool open import eq open import maybe open import nat open import unit open import product open import empty open import sum ---------------------------------------------------------------------- -- datatypes ---------------------------------------------------------------------- data 𝕃 {β„“} (A : Set β„“) : Set β„“ where [] : 𝕃 A _::_ : (x : A) (xs : 𝕃 A) β†’ 𝕃 A {-# BUILTIN LIST 𝕃 #-} {-# BUILTIN NIL [] #-} {-# BUILTIN CONS _::_ #-} list = 𝕃 ---------------------------------------------------------------------- -- syntax ---------------------------------------------------------------------- infixr 6 _::_ _++_ infixr 5 _shorter_ _longer_ ---------------------------------------------------------------------- -- operations ---------------------------------------------------------------------- [_] : βˆ€ {β„“} {A : Set β„“} β†’ A β†’ 𝕃 A [ x ] = x :: [] is-empty : βˆ€{β„“}{A : Set β„“} β†’ 𝕃 A β†’ 𝔹 is-empty [] = tt is-empty (_ :: _) = ff tail : βˆ€ {β„“} {A : Set β„“} β†’ 𝕃 A β†’ 𝕃 A tail [] = [] tail (x :: xs) = xs head : βˆ€{β„“}{A : Set β„“} β†’ (l : 𝕃 A) β†’ .(is-empty l ≑ ff) β†’ A head [] () head (x :: xs) _ = x head2 : βˆ€{β„“}{A : Set β„“} β†’ (l : 𝕃 A) β†’ maybe A head2 [] = nothing head2 (a :: _) = just a last : βˆ€{β„“}{A : Set β„“} β†’ (l : 𝕃 A) β†’ is-empty l ≑ ff β†’ A last [] () last (x :: []) _ = x last (x :: (y :: xs)) _ = last (y :: xs) refl _++_ : βˆ€ {β„“} {A : Set β„“} β†’ 𝕃 A β†’ 𝕃 A β†’ 𝕃 A [] ++ ys = ys (x :: xs) ++ ys = x :: (xs ++ ys) concat : βˆ€{β„“}{A : Set β„“} β†’ 𝕃 (𝕃 A) β†’ 𝕃 A concat [] = [] concat (l :: ls) = l ++ concat ls repeat : βˆ€{β„“}{A : Set β„“} β†’ β„• β†’ A β†’ 𝕃 A repeat 0 a = [] repeat (suc n) a = a :: (repeat n a) map : βˆ€ {β„“ β„“'} {A : Set β„“} {B : Set β„“'} β†’ (A β†’ B) β†’ 𝕃 A β†’ 𝕃 B map f [] = [] map f (x :: xs) = f x :: map f xs -- The hom part of the list functor. list-funct : {A B : Set} β†’ (A β†’ B) β†’ (𝕃 A β†’ 𝕃 B) list-funct f l = map f l {- (maybe-map f xs) returns (just ys) if f returns (just y_i) for each x_i in the list xs. Otherwise, (maybe-map f xs) returns nothing. -} 𝕃maybe-map : βˆ€ {β„“ β„“'} {A : Set β„“} {B : Set β„“'} β†’ (A β†’ maybe B) β†’ 𝕃 A β†’ maybe (𝕃 B) 𝕃maybe-map f [] = just [] 𝕃maybe-map f (x :: xs) with f x 𝕃maybe-map f (x :: xs) | nothing = nothing 𝕃maybe-map f (x :: xs) | just y with 𝕃maybe-map f xs 𝕃maybe-map f (x :: xs) | just y | nothing = nothing 𝕃maybe-map f (x :: xs) | just y | just ys = just (y :: ys) foldr : βˆ€{β„“ β„“'}{A : Set β„“}{B : Set β„“'} β†’ (A β†’ B β†’ B) β†’ B β†’ 𝕃 A β†’ B foldr f b [] = b foldr f b (a :: as) = f a (foldr f b as) length : βˆ€{β„“}{A : Set β„“} β†’ 𝕃 A β†’ β„• length [] = 0 length (x :: xs) = suc (length xs) reverse-helper : βˆ€ {β„“}{A : Set β„“} β†’ 𝕃 A β†’ 𝕃 A β†’ 𝕃 A reverse-helper h [] = h reverse-helper h (x :: xs) = reverse-helper (x :: h) xs reverse : βˆ€ {β„“}{A : Set β„“} β†’ 𝕃 A β†’ 𝕃 A reverse l = reverse-helper [] l list-member : βˆ€{β„“}{A : Set β„“}(eq : A β†’ A β†’ 𝔹)(a : A)(l : 𝕃 A) β†’ 𝔹 list-member eq a [] = ff list-member eq a (x :: xs) = eq a x || list-member eq a xs list-minus : βˆ€{β„“}{A : Set β„“}(eq : A β†’ A β†’ 𝔹)(l1 l2 : 𝕃 A) β†’ 𝕃 A list-minus eq [] l2 = [] list-minus eq (x :: xs) l2 = let r = list-minus eq xs l2 in if list-member eq x l2 then r else x :: r _longer_ : βˆ€{β„“}{A : Set β„“}(l1 l2 : 𝕃 A) β†’ 𝔹 [] longer y = ff (x :: xs) longer [] = tt (x :: xs) longer (y :: ys) = xs longer ys _shorter_ : βˆ€{β„“}{A : Set β„“}(l1 l2 : 𝕃 A) β†’ 𝔹 x shorter y = y longer x -- return tt iff all elements in the list satisfy the given predicate pred. list-all : βˆ€{β„“}{A : Set β„“}(pred : A β†’ 𝔹)(l : 𝕃 A) β†’ 𝔹 list-all pred [] = tt list-all pred (x :: xs) = pred x && list-all pred xs all-pred : {X : Set} β†’ (X β†’ Set) β†’ 𝕃 X β†’ Set all-pred f [] = ⊀ all-pred f (x₁ :: xs) = (f x₁) ∧ (all-pred f xs) -- return tt iff at least one element in the list satisfies the given predicate pred. list-any : βˆ€{β„“}{A : Set β„“}(pred : A β†’ 𝔹)(l : 𝕃 A) β†’ 𝔹 list-any pred [] = ff list-any pred (x :: xs) = pred x || list-any pred xs list-and : (l : 𝕃 𝔹) β†’ 𝔹 list-and [] = tt list-and (x :: xs) = x && (list-and xs) list-or : (l : 𝕃 𝔹) β†’ 𝔹 list-or [] = ff list-or (x :: l) = x || list-or l list-max : βˆ€{β„“}{A : Set β„“} (lt : A β†’ A β†’ 𝔹) β†’ 𝕃 A β†’ A β†’ A list-max lt [] x = x list-max lt (y :: ys) x = list-max lt ys (if lt y x then x else y) isSublist : βˆ€{β„“}{A : Set β„“} β†’ 𝕃 A β†’ 𝕃 A β†’ (A β†’ A β†’ 𝔹) β†’ 𝔹 isSublist l1 l2 eq = list-all (Ξ» a β†’ list-member eq a l2) l1 =𝕃 : βˆ€{β„“}{A : Set β„“} β†’ (A β†’ A β†’ 𝔹) β†’ (l1 : 𝕃 A) β†’ (l2 : 𝕃 A) β†’ 𝔹 =𝕃 eq (a :: as) (b :: bs) = eq a b && =𝕃 eq as bs =𝕃 eq [] [] = tt =𝕃 eq _ _ = ff filter : βˆ€{β„“}{A : Set β„“} β†’ (A β†’ 𝔹) β†’ 𝕃 A β†’ 𝕃 A filter p [] = [] filter p (x :: xs) = let r = filter p xs in if p x then x :: r else r -- remove all elements equal to the given one remove : βˆ€{β„“}{A : Set β„“}(eq : A β†’ A β†’ 𝔹)(a : A)(l : 𝕃 A) β†’ 𝕃 A remove eq a l = filter (Ξ» x β†’ ~ (eq a x)) l {- nthTail n l returns the part of the list after the first n elements, or [] if the list has fewer than n elements -} nthTail : βˆ€{β„“}{A : Set β„“} β†’ β„• β†’ 𝕃 A β†’ 𝕃 A nthTail 0 l = l nthTail n [] = [] nthTail (suc n) (x :: l) = nthTail n l nth : βˆ€{β„“}{A : Set β„“} β†’ β„• β†’ 𝕃 A β†’ maybe A nth _ [] = nothing nth 0 (x :: xs) = just x nth (suc n) (x :: xs) = nth n xs -- nats-down N returns N :: (N-1) :: ... :: 0 :: [] nats-down : β„• β†’ 𝕃 β„• nats-down 0 = [ 0 ] nats-down (suc x) = suc x :: nats-down x zip : βˆ€{ℓ₁ β„“β‚‚}{A : Set ℓ₁}{B : Set β„“β‚‚} β†’ 𝕃 A β†’ 𝕃 B β†’ 𝕃 (A Γ— B) zip [] [] = [] zip [] (x :: lβ‚‚) = [] zip (x :: l₁) [] = [] zip (x :: l₁) (y :: lβ‚‚) = (x , y) :: zip l₁ lβ‚‚ unzip : βˆ€{ℓ₁ β„“β‚‚}{A : Set ℓ₁}{B : Set β„“β‚‚} β†’ 𝕃 (A Γ— B) β†’ (𝕃 A Γ— 𝕃 B) unzip [] = ([] , []) unzip ((x , y) :: ps) with unzip ps ... | (xs , ys) = x :: xs , y :: ys map-⊎ : {ℓ₁ β„“β‚‚ ℓ₃ : Level} β†’ {A : Set ℓ₁}{B : Set β„“β‚‚}{C : Set ℓ₃} β†’ (A β†’ C) β†’ (B β†’ C) β†’ 𝕃 (A ⊎ B) β†’ 𝕃 C map-⊎ f g [] = [] map-⊎ f g (inj₁ x :: l) = f x :: map-⊎ f g l map-⊎ f g (injβ‚‚ y :: l) = g y :: map-⊎ f g l proj-βŠŽβ‚ : {β„“ β„“' : Level}{A : Set β„“}{B : Set β„“'} β†’ 𝕃 (A ⊎ B) β†’ (𝕃 A) proj-βŠŽβ‚ [] = [] proj-βŠŽβ‚ (inj₁ x :: l) = x :: proj-βŠŽβ‚ l proj-βŠŽβ‚ (injβ‚‚ y :: l) = proj-βŠŽβ‚ l proj-βŠŽβ‚‚ : {β„“ β„“' : Level}{A : Set β„“}{B : Set β„“'} β†’ 𝕃 (A ⊎ B) β†’ (𝕃 B) proj-βŠŽβ‚‚ [] = [] proj-βŠŽβ‚‚ (inj₁ x :: l) = proj-βŠŽβ‚‚ l proj-βŠŽβ‚‚ (injβ‚‚ y :: l) = y :: proj-βŠŽβ‚‚ l drop-nothing : βˆ€{β„“}{A : Set β„“} β†’ 𝕃 (maybe A) β†’ 𝕃 A drop-nothing [] = [] drop-nothing (nothing :: aa) = drop-nothing aa drop-nothing (just a :: aa) = a :: drop-nothing aa