------------------------------------------------------------------------
-- The Agda standard library
--
-- Fresh lists, a proof relevant variant of Catarina Coquand!$\prime$!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 --without-K --safe #-}

module Data.List.Fresh where

open import Level using (Level; _!$\sqcup$!_)
open import Data.Bool.Base using (true; false)
open import Data.Unit.Polymorphic.Base using (!$\top$!)
open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\text{1}$!; proj!$\text{2}$!)
open import Data.List.Relation.Unary.All using (All; []; _!$\text{::}$!_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _!$\text{::}$!_)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Nat.Base using (!$\mathbb{N}$!; zero; suc)
open import Function using (_∘′_; flip; id; _on_)
open import Relation.Nullary      using (does)
open import Relation.Unary   as U using (Pred)
open import Relation.Binary  as B using (Rel)
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 !$\sqcup$! r)
  fresh : (a : A) (as : List#) !$\rightarrow$! Set r

  data List# where
    []   : List#
    cons : (a : A) (as : List#) !$\rightarrow$! fresh a as !$\rightarrow$! 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 _!$\text{::}$!#_
  pattern _!$\text{::}$!#_ x xs = cons x xs _

  fresh a []        = !$\top$!
  fresh a (x !$\text{::}$!# xs) = R a x !$\times$! 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) !$\rightarrow$! Set r
_#_ = fresh _ _

------------------------------------------------------------------------
-- Operations for modifying fresh lists

module _ {R : Rel A r} {S : Rel B s} (f : A !$\rightarrow$! B) (R!$\Rightarrow$!S : ∀[ R !$\Rightarrow$! (S on f) ]) where

  map   : List# A R !$\rightarrow$! List# B S
  map-# : ∀ {a} as !$\rightarrow$! a # as !$\rightarrow$! f a # map as

  map []             = []
  map (cons a as ps) = cons (f a) (map as) (map-# as ps)

  map-# []        _        = _
  map-# (a !$\text{::}$!# as) (p , ps) = R!$\Rightarrow$!S p , map-# as ps

module _ {R : Rel B r} (f : A !$\rightarrow$! B) where

  map!$\text{1}$! : List# A (R on f) !$\rightarrow$! List# B R
  map!$\text{1}$! = map f id

module _ {R : Rel A r} {S : Rel A s} (R!$\Rightarrow$!S : ∀[ R !$\Rightarrow$! S ]) where

  map!$\text{2}$! : List# A R !$\rightarrow$! List# A S
  map!$\text{2}$! = map id R!$\Rightarrow$!S

------------------------------------------------------------------------
-- Views

data Empty {A : Set a} {R : Rel A r} : List# A R !$\rightarrow$! Set (a !$\sqcup$! r) where
  [] : Empty []

data NonEmpty {A : Set a} {R : Rel A r} : List# A R !$\rightarrow$! Set (a !$\sqcup$! r) where
  cons : ∀ x xs pr !$\rightarrow$! NonEmpty (cons x xs pr)

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

length : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! !$\mathbb{N}$!
length []        = 0
length (_ !$\text{::}$!# xs) = suc (length xs)

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

pattern [_] a = a !$\text{::}$!# []

fromMaybe : {R : Rel A r} !$\rightarrow$! Maybe A !$\rightarrow$! List# A R
fromMaybe nothing  = []
fromMaybe (just a) = [ a ]

module _ {R : Rel A r} (R-refl : B.Reflexive R) where

  replicate   : !$\mathbb{N}$! !$\rightarrow$! A !$\rightarrow$! List# A R
  replicate-# : (n : !$\mathbb{N}$!) (a : A) !$\rightarrow$! 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} !$\rightarrow$! List# A R !$\rightarrow$! Maybe (A !$\times$! List# A R)
uncons []        = nothing
uncons (a !$\text{::}$!# as) = just (a , as)

head : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! Maybe A
head = Maybe.map proj!$\text{1}$! ∘′ uncons

tail : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! Maybe (List# A R)
tail = Maybe.map proj!$\text{2}$! ∘′ uncons

take   : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List# A R !$\rightarrow$! List# A R
take-# : {R : Rel A r} !$\rightarrow$! ∀ n a (as : List# A R) !$\rightarrow$! a # as !$\rightarrow$! 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 !$\text{::}$!# xs) (p , ps) = p , take-# n a xs ps

drop : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List# A R !$\rightarrow$! List# A R
drop zero    as        = as
drop (suc n) []        = []
drop (suc n) (a !$\text{::}$!# as) = drop n as

module _ {P : Pred A p} (P? : U.Decidable P) where

  takeWhile   : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! List# A R
  takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) !$\rightarrow$! a # as !$\rightarrow$! a # takeWhile as

  takeWhile []             = []
  takeWhile (cons a as ps) with does (P? a)
  ... | true  = cons a (takeWhile as) (takeWhile-# a as ps)
  ... | false = []

  takeWhile-# a []        _        = _
  takeWhile-# a (x !$\text{::}$!# xs) (p , ps) with does (P? x)
  ... | true  = p , takeWhile-# a xs ps
  ... | false = _

  dropWhile : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! List# A R
  dropWhile []            = []
  dropWhile aas@(a !$\text{::}$!# as) with does (P? a)
  ... | true  = dropWhile as
  ... | false = aas

  filter   : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! List# A R
  filter-# : ∀ {R : Rel A r} a (as : List# A R) !$\rightarrow$! a # as !$\rightarrow$! a # filter as

  filter []             = []
  filter (cons a as ps) with does (P? a)
  ... | true  = cons a (filter as) (filter-# a as ps)
  ... | false = filter as

  filter-# a []        _        = _
  filter-# a (x !$\text{::}$!# 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} !$\rightarrow$! List# A R !$\rightarrow$! ∃ (AllPairs R)
toAll  : ∀ {R : Rel A r} {a} as !$\rightarrow$! fresh A R a as !$\rightarrow$! All (R a) (proj!$\text{1}$! (toList as))

toList []             = -, []
toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj!$\text{2}$! (toList xs)

toAll []        ps       = []
toAll (a !$\text{::}$!# as) (p , ps) = p !$\text{::}$! toAll as ps

fromList   : ∀ {R : Rel A r} {xs} !$\rightarrow$! AllPairs R xs !$\rightarrow$! List# A R
fromList-# : ∀ {R : Rel A r} {x xs} (ps : AllPairs R xs) !$\rightarrow$!
             All (R x) xs !$\rightarrow$! x # fromList ps

fromList []       = []
fromList (r !$\text{::}$! rs) = cons _ (fromList rs) (fromList-# rs r)

fromList-# []       _        = _
fromList-# (p !$\text{::}$! ps) (r !$\text{::}$! rs) = r , fromList-# ps rs