    ------------------------------------------------------------------------
    -- 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 using (Reflexive)
    open import Relation.Nary using (_⇒_; ∀[_])

    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