------------------------------------------------------------------------
-- The Agda standard library
--
-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts
-- in "A Formalised Proof of the Soundness and Completeness of a Simply
-- Typed Lambda-Calculus with Explicit Substitutions"
------------------------------------------------------------------------
-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
-- examples of how to use fresh lists.
{-# OPTIONS --cubical-compatible --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.Nullary using (does)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (Rel)
import Relation.Binary.Definitions as B
open import Relation.Nary
private
variable
a b p r s : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Basic type
-- If we pick an R such that (R a b) means that a is different from b
-- then we have a list of distinct values.
module _ {a} (A : Set a) (R : Rel A r) where
data List# : Set (a ⊔ r)
fresh : (a : A) (as : List#) → Set r
data List# where
[] : List#
cons : (a : A) (as : List#) → fresh a as → List#
-- Whenever R can be reconstructed by η-expansion (e.g. because it is
-- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
-- do not care about the proof, it is convenient to get back list syntax.
-- We use a different symbol to avoid conflict when importing both
-- Data.List and Data.List.Fresh.
infixr 5 _∷#_
pattern _∷#_ x xs = cons x xs _
fresh a [] = ⊤
fresh a (x ∷# xs) = R a x × fresh a xs
-- Convenient notation for freshness making A and R implicit parameters
infix 5 _#_
_#_ : {R : Rel A r} (a : A) (as : List# A R) → Set r
_#_ = fresh _ _
------------------------------------------------------------------------
-- Operations for modifying fresh lists
module _ {R : Rel A r} {S : Rel B s} (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
map : List# A R → List# B S
map-# : ∀ {a} as → a # as → f a # map as
map [] = []
map (cons a as ps) = cons (f a) (map as) (map-# as ps)
map-# [] _ = _
map-# (a ∷# as) (p , ps) = R⇒S p , map-# as ps
module _ {R : Rel B r} (f : A → B) where
map₁ : List# A (R on f) → List# B R
map₁ = map f id
module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
map₂ : List# A R → List# A S
map₂ = map id R⇒S
------------------------------------------------------------------------
-- Views
data Empty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
[] : Empty []
data NonEmpty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
cons : ∀ x xs pr → NonEmpty (cons x xs pr)
------------------------------------------------------------------------
-- Operations for reducing fresh lists
length : {R : Rel A r} → List# A R → ℕ
length [] = 0
length (_ ∷# xs) = suc (length xs)
------------------------------------------------------------------------
-- Operations for constructing fresh lists
pattern [_] a = a ∷# []
fromMaybe : {R : Rel A r} → Maybe A → List# A R
fromMaybe nothing = []
fromMaybe (just a) = [ a ]
module _ {R : Rel A r} (R-refl : B.Reflexive R) where
replicate : ℕ → A → List# A R
replicate-# : (n : ℕ) (a : A) → a # replicate n a
replicate zero a = []
replicate (suc n) a = cons a (replicate n a) (replicate-# n a)
replicate-# zero a = _
replicate-# (suc n) a = R-refl , replicate-# n a
------------------------------------------------------------------------
-- Operations for deconstructing fresh lists
uncons : {R : Rel A r} → List# A R → Maybe (A × List# A R)
uncons [] = nothing
uncons (a ∷# as) = just (a , as)
head : {R : Rel A r} → List# A R → Maybe A
head = Maybe.map proj₁ ∘′ uncons
tail : {R : Rel A r} → List# A R → Maybe (List# A R)
tail = Maybe.map proj₂ ∘′ uncons
take : {R : Rel A r} → ℕ → List# A R → List# A R
take-# : {R : Rel A r} → ∀ n a (as : List# A R) → a # as → a # take n as
take zero xs = []
take (suc n) [] = []
take (suc n) (cons a as ps) = cons a (take n as) (take-# n a as ps)
take-# zero a xs _ = _
take-# (suc n) a [] ps = _
take-# (suc n) a (x ∷# xs) (p , ps) = p , take-# n a xs ps
drop : {R : Rel A r} → ℕ → List# A R → List# A R
drop zero as = as
drop (suc n) [] = []
drop (suc n) (a ∷# as) = drop n as
module _ {P : Pred A p} (P? : U.Decidable P) where
takeWhile : {R : Rel A r} → List# A R → List# A R
takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as
takeWhile [] = []
takeWhile (cons a as ps) =
if does (P? a) then cons a (takeWhile as) (takeWhile-# a as ps) else []
-- this 'with' is needed to cause reduction in the type of 'takeWhile (a ∷# as)'
takeWhile-# a [] _ = _
takeWhile-# a (x ∷# xs) (p , ps) with does (P? x)
... | true = p , takeWhile-# a xs ps
... | false = _
dropWhile : {R : Rel A r} → List# A R → List# A R
dropWhile [] = []
dropWhile aas@(a ∷# as) = if does (P? a) then dropWhile as else aas
filter : {R : Rel A r} → List# A R → List# A R
filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as
filter [] = []
filter (cons a as ps) =
let l = filter as in
if does (P? a) then cons a l (filter-# a as ps) else l
-- this 'with' is needed to cause reduction in the type of 'filter-# a (x ∷# xs)'
filter-# a [] _ = _
filter-# a (x ∷# xs) (p , ps) with does (P? x)
... | true = p , filter-# a xs ps
... | false = filter-# a xs ps
------------------------------------------------------------------------
-- Relationship to List and AllPairs
toList : {R : Rel A r} → List# A R → ∃ (AllPairs R)
toAll : ∀ {R : Rel A r} {a} as → fresh A R a as → All (R a) (proj₁ (toList as))
toList [] = -, []
toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)
toAll [] ps = []
toAll (a ∷# as) (p , ps) = p ∷ toAll as ps
fromList : ∀ {R : Rel A r} {xs} → AllPairs R xs → List# A R
fromList-# : ∀ {R : Rel A r} {x 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