------------------------------------------------------------------------
-- 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!$\_{1}$!; proj!$\_{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 : !$\forall$![ R !$\Rightarrow$! (S on f) ]) where

  map   : List!$\#$! A R !$\rightarrow$! List!$\#$! B S
  map-!$\#$! : !$\forall$! {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!$\_{1}$! : List!$\#$! A (R on f) !$\rightarrow$! List!$\#$! B R
  map!$\_{1}$! = map f id

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

  map!$\_{2}$! : List!$\#$! A R !$\rightarrow$! List!$\#$! A S
  map!$\_{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 : !$\forall$! 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!$\_{1}$! ∘′ uncons

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

take   : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List!$\#$! A R !$\rightarrow$! List!$\#$! A R
take-!$\#$! : {R : Rel A r} !$\rightarrow$! !$\forall$! 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-!$\#$! : !$\forall$! {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-!$\#$! : !$\forall$! {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  : !$\forall$! {R : Rel A r} {a} as !$\rightarrow$! fresh A R a as !$\rightarrow$! All (R a) (proj!$\_{1}$! (toList as))

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

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

fromList   : !$\forall$! {R : Rel A r} {xs} !$\rightarrow$! AllPairs R xs !$\rightarrow$! List!$\#$! A R
fromList-!$\#$! : !$\forall$! {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