Fresh
{-# OPTIONS --without-K --safe #-}
module Data.List.Fresh where
open import Level using (Level; _⊔_)
open import Data.Bool.Base using (true; false; if_then_else_)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Data.Product.Base using (∃; _×_; _,_; -,_; proj₁; proj₂)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function.Base using (_∘′_; flip; id; _on_)
open import Relation.Binary.Core using (Rel; REL)
open import Relation.Binary.Definitions as Binary using (Reflexive)
open import Relation.Nary using (_⇒_; ∀[_])
open import Relation.Nullary using (does)
open import Relation.Unary as Unary using (Pred; Decidable)
private
variable
a b p r s : Level
A : Set a
B : Set b
R : Rel A r
S : Rel A s
x y : A
module _ (A : Set a) (R : Rel A r) where
data List# : Set (a ⊔ r)
fresh : REL A List# r
data List# where
[] : List#
cons : (x : A) (xs : List#) → fresh x xs → List#
infixr 5 _∷#_
pattern _∷#_ x xs = cons x xs _
fresh a [] = ⊤
fresh a (x ∷# xs) = R a x × fresh a xs
infix 5 _#[_]_ _#_
_#[_]_ : A → (R : Rel A r) → Pred (List# A R) _
x #[ R ] xs = fresh _ R x xs
_#_ : REL A (List# A R) _
x # xs = x #[ _ ] xs
module _ (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
map : List# A R → List# B S
map-# : ∀ xs → x # xs → f x # map xs
map [] = []
map (cons x xs ps) = cons (f x) (map xs) (map-# xs ps)
map-# [] _ = _
map-# (x ∷# xs) (p , ps) = R⇒S p , map-# xs ps
module _ (f : A → B) where
map₁ : List# A (R on f) → List# B R
map₁ = map f id
module _ {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
map₂ : List# A R → List# A S
map₂ = map id R⇒S
data Empty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
[] : Empty []
data NonEmpty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
cons : ∀ x xs pr → NonEmpty (cons x xs pr)
length : List# A R → ℕ
length [] = 0
length (_ ∷# xs) = suc (length xs)
pattern [_] x = x ∷# []
fromMaybe : Maybe A → List# A R
fromMaybe nothing = []
fromMaybe (just x) = [ x ]
module _ (refl : Reflexive {A = A} R) where
replicate : ℕ → A → List# A R
replicate-# : ∀ n x → x # replicate n x
replicate zero x = []
replicate (suc n) x = cons x (replicate n x) (replicate-# n x)
replicate-# zero x = _
replicate-# (suc n) x = refl , replicate-# n x
uncons : List# A R → Maybe (A × List# A R)
uncons [] = nothing
uncons (x ∷# xs) = just (x , xs)
head : List# A R → Maybe A
head = Maybe.map proj₁ ∘′ uncons
tail : List# A R → Maybe (List# A R)
tail = Maybe.map proj₂ ∘′ uncons
take : ℕ → List# A R → List# A R
take-# : ∀ n y xs → y # xs → y # take {R = R} n xs
take zero xs = []
take (suc n) [] = []
take (suc n) (cons x xs ps) = cons x (take n xs) (take-# n x xs ps)
take-# zero y xs _ = _
take-# (suc n) y [] ps = _
take-# (suc n) y (x ∷# xs) (p , ps) = p , take-# n y xs ps
drop : ℕ → List# A R → List# A R
drop zero xs = xs
drop (suc n) [] = []
drop (suc n) (x ∷# xs) = drop n xs
module _ {P : Pred A p} (P? : Decidable P) where
takeWhile : List# A R → List# A R
takeWhile-# : ∀ y xs → y # xs → y # takeWhile {R = R} xs
takeWhile [] = []
takeWhile (cons x xs ps) =
if does (P? x) then cons x (takeWhile xs) (takeWhile-# x xs ps) else []
takeWhile-# y [] _ = _
takeWhile-# y (x ∷# xs) (p , ps) with does (P? x)
... | true = p , takeWhile-# y xs ps
... | false = _
dropWhile : List# A R → List# A R
dropWhile [] = []
dropWhile xxs@(x ∷# xs) = if does (P? x) then dropWhile xs else xxs
filter : List# A R → List# A R
filter-# : ∀ y xs → y # xs → y # filter {R = R} xs
filter [] = []
filter (cons x xs ps) =
let l = filter xs in
if does (P? x) then cons x l (filter-# x xs ps) else l
filter-# y [] _ = _
filter-# y (x ∷# xs) (p , ps) with does (P? x)
... | true = p , filter-# y xs ps
... | false = filter-# y xs ps
toList : List# A R → ∃ (AllPairs R)
toAll : ∀ xs → x #[ R ] xs → All (R x) (proj₁ (toList xs))
toList [] = -, []
toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)
toAll [] ps = []
toAll (x ∷# xs) (p , ps) = p ∷ toAll xs ps
fromList : ∀ {xs} → AllPairs R xs → List# A R
fromList-# : ∀ {xs} (ps : AllPairs R xs) →
All (R x) xs → x # fromList ps
fromList [] = []
fromList (r ∷ rs) = cons _ (fromList rs) (fromList-# rs r)
fromList-# [] _ = _
fromList-# (p ∷ ps) (r ∷ rs) = r , fromList-# ps rs