------------------------------------------------------------------------
-- The Agda standard library
--
-- Reverse view
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Reverse where

open import Data.List.Base as L using (List; []; _∷_; _∷ʳ_)
open import Data.List.Properties
  using (unfold-reverse; reverse-involutive)
open import Function.Base using (_$_)
open import Relation.Binary.PropositionalEquality.Core
  using (subst; sym)

-- If you want to traverse a list from the end, then you can use the
-- reverse view of it.

infixl  _∶_∶ʳ_

data Reverse {a} {A : Set a} : List A → Set a where
  []     : Reverse []
  _∶_∶ʳ_ : ∀ xs (rs : Reverse xs) (x : A) → Reverse (xs ∷ʳ x)

module _ {a} {A : Set a} where

  reverse : (xs : List A) → Reverse (L.reverse xs)
  reverse []       = []
  reverse (x ∷ xs) = cast $ _ ∶ reverse xs ∶ʳ x where
    cast = subst Reverse (sym $ unfold-reverse x xs)

  reverseView : (xs : List A) → Reverse xs
  reverseView xs = cast $ reverse (L.reverse xs) where
    cast = subst Reverse (reverse-involutive xs)