{-# 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))