    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An inductive definition of the heterogeneous suffix relation
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Suffix.Heterogeneous where

    open import Level
    open import Relation.Binary.Core using (REL; _⇒_)
    open import Data.List.Base as List using (List; []; _∷_)
    open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
      using (Pointwise; []; _∷_)

    module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where

      infixr 5 _++_

      data Suffix : REL (List A) (List B) (a ⊔ b ⊔ r) where
        here  : ∀ {as bs} → Pointwise R as bs → Suffix as bs
        there : ∀ {b as bs} → Suffix as bs → Suffix as (b ∷ bs)

      data SuffixView (as : List A) : List B → Set (a ⊔ b ⊔ r) where
        _++_ : ∀ cs {ds} → Pointwise R as ds → SuffixView as (cs List.++ ds)

    module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

      tail : ∀ {a as bs} → Suffix R (a ∷ as) bs → Suffix R as bs
      tail (here (_ ∷ rs)) = there (here rs)
      tail (there x) = there (tail x)

      infixr 5 _++ˢ_

      _++ˢ_ : ∀ pre {as bs} → Suffix R as bs → Suffix R as (pre List.++ bs)
      []       ++ˢ rs = rs
      (x ∷ xs) ++ˢ rs = there (xs ++ˢ rs)

    module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where

      map : R ⇒ S → Suffix R ⇒ Suffix S
      map R⇒S (here rs)   = here (Pointwise.map R⇒S rs)
      map R⇒S (there suf) = there (map R⇒S suf)

    module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

      toView : ∀ {as bs} → Suffix R as bs → SuffixView R as bs
      toView (here rs) = [] ++ rs
      toView (there {c} suf) with cs ++ rs ← toView suf = (c ∷ cs) ++ rs

      fromView : ∀ {as bs} → SuffixView R as bs → Suffix R as bs
      fromView ([]       ++ rs) = here rs
      fromView ((c ∷ cs) ++ rs) = there (fromView (cs ++ rs))