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

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

module Data.List.Relation.Binary.Infix.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
  using (Pointwise)
open import Data.List.Relation.Binary.Prefix.Heterogeneous
  as Prefix using (Prefix; []; _∷_; _++ᵖ_)

private
  variable
    a b r s : Level
    A : Set a
    B : Set b
    R : REL A B r
    S : REL A B s

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

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

  data View (as : List A) : List B → Set (a ⊔ b ⊔ r) where
    MkView : ∀ pref {inf} → Pointwise R as inf → ∀ suff →
            View as (pref List.++ inf List.++ suff)

infixr 5 _++ⁱ_ _ⁱ++_

_++ⁱ_ : ∀ xs {as bs} → Infix R as bs → Infix R as (xs ++ bs)
[]       ++ⁱ rs = rs
(x ∷ xs) ++ⁱ rs = there (xs ++ⁱ rs)

_ⁱ++_ : ∀ {as bs} → Infix R as bs → ∀ xs → Infix R as (bs ++ xs)
here  rs ⁱ++ xs = here (rs ++ᵖ xs)
there rs ⁱ++ xs = there (rs ⁱ++ xs)

map : R ⇒ S → Infix R ⇒ Infix S
map R⇒S (here pref) = here (Prefix.map R⇒S pref)
map R⇒S (there inf) = there (map R⇒S inf)

toView : ∀ {as bs} → Infix R as bs → View R as bs
toView (here p)  with inf Prefix.++ suff ← Prefix.toView p = MkView [] inf suff
toView (there p) with MkView pref inf suff ← toView p      = MkView (_ ∷ pref) inf suff

fromView : ∀ {as bs} → View R as bs → Infix R as bs
fromView (MkView []         inf suff) = here (Prefix.fromView (inf Prefix.++ suff))
fromView (MkView (a ∷ pref) inf suff) = there (fromView (MkView pref inf suff))