------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the heterogeneous prefix relation
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.Relation.Binary.Prefix.Heterogeneous where
 
open import Level
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise
  using (Pointwise; []; _∷_)
open import Data.Product.Base using (∃; _×_; _,_; uncurry)
open import Relation.Binary.Core using (REL; _⇒_)
 
module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
 
  infixr  _∷_ _++_
 
  data Prefix : REL (List A) (List B) (a ⊔ b ⊔ r) where
    []  : ∀ {bs} → Prefix [] bs
    _∷_ : ∀ {a b as bs} → R a b → Prefix as bs → Prefix (a ∷ as) (b ∷ bs)
 
  data PrefixView (as : List A) : List B → Set (a ⊔ b ⊔ r) where
    _++_ : ∀ {cs} → Pointwise R as cs → ∀ ds → PrefixView as (cs List.++ ds)
 
module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a b as bs} where
 
  head : Prefix R (a ∷ as) (b ∷ bs) → R a b
  head (r ∷ rs) = r
 
  tail : Prefix R (a ∷ as) (b ∷ bs) → Prefix R as bs
  tail (r ∷ rs) = rs
 
  uncons : Prefix R (a ∷ as) (b ∷ bs) → R a b × Prefix R as bs
  uncons (r ∷ rs) = r , 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 → Prefix R ⇒ Prefix S
  map R⇒S []       = []
  map R⇒S (r ∷ rs) = R⇒S r ∷ map R⇒S rs
 
module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
  infixr  _++ᵖ_
 
  _++ᵖ_ : ∀ {as bs} → Prefix R as bs → ∀ suf → Prefix R as (bs List.++ suf)
  []       ++ᵖ suf = []
  (r ∷ rs) ++ᵖ suf = r ∷ (rs ++ᵖ suf)
 
  toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs
  toView []       = [] ++ _
  toView (r ∷ rs) with rs′ ++ ds ← toView rs = (r ∷ rs′) ++ ds
 
  fromView : ∀ {as bs} → PrefixView R as bs → Prefix R as bs
  fromView ([]       ++ ds) = []
  fromView ((r ∷ rs) ++ ds) = r ∷ fromView (rs ++ ds)