------------------------------------------------------------------------
-- The Agda standard library
--
-- Generalised notion of interleaving two lists into one in an
-- order-preserving manner
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Ternary.Interleaving where
open import Level
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
open import Data.Product.Base as Product using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
------------------------------------------------------------------------
-- Definition
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
(L : REL A C l) (R : REL B C r) where
infixr 5 _∷ˡ_ _∷ʳ_
data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
[] : Interleaving [] [] []
_∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)
_∷ʳ_ : ∀ {b c l r cs} → R b c → Interleaving l r cs → Interleaving l (b ∷ r) (c ∷ cs)
------------------------------------------------------------------------
-- Operations
module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
{L : REL A C l} {R : REL B C r} where
-- injections
left : ∀ {as cs} → Pointwise L as cs → Interleaving L R as [] cs
left [] = []
left (l ∷ pw) = l ∷ˡ left pw
right : ∀ {bs cs} → Pointwise R bs cs → Interleaving L R [] bs cs
right [] = []
right (r ∷ pw) = r ∷ʳ right pw
-- swap
swap : ∀ {cs l r} → Interleaving L R l r cs → Interleaving R L r l cs
swap [] = []
swap (l ∷ˡ sp) = l ∷ʳ swap sp
swap (r ∷ʳ sp) = r ∷ˡ swap sp
-- extract the "proper" equality split from the pointwise relations
break : ∀ {cs l r} → Interleaving L R l r cs → ∃ $ uncurry $ λ csl csr →
Interleaving _≡_ _≡_ csl csr cs × Pointwise L l csl × Pointwise R r csr
break [] = -, [] , [] , []
break (l ∷ˡ sp) = let (_ , eq , pwl , pwr) = break sp in
-, refl ∷ˡ eq , l ∷ pwl , pwr
break (r ∷ʳ sp) = let (_ , eq , pwl , pwr) = break sp in
-, refl ∷ʳ eq , pwl , r ∷ pwr
-- map
module _ {a b c l r p q} {A : Set a} {B : Set b} {C : Set c}
{L : REL A C l} {R : REL B C r} {P : REL A C p} {Q : REL B C q} where
map : ∀ {cs l r} → L ⇒ P → R ⇒ Q → Interleaving L R l r cs → Interleaving P Q l r cs
map L⇒P R⇒Q [] = []
map L⇒P R⇒Q (l ∷ˡ sp) = L⇒P l ∷ˡ map L⇒P R⇒Q sp
map L⇒P R⇒Q (r ∷ʳ sp) = R⇒Q r ∷ʳ map L⇒P R⇒Q sp
module _ {a b c l r p} {A : Set a} {B : Set b} {C : Set c}
{L : REL A C l} {R : REL B C r} where
map₁ : ∀ {P : REL A C p} {as l r} → L ⇒ P →
Interleaving L R l r as → Interleaving P R l r as
map₁ L⇒P = map L⇒P id
map₂ : ∀ {P : REL B C p} {as l r} → R ⇒ P →
Interleaving L R l r as → Interleaving L P l r as
map₂ = map id
------------------------------------------------------------------------
-- Special case: The second and third list have the same type
module _ {a b l r} {A : Set a} {B : Set b} {L : REL A B l} {R : REL A B r} where
-- converting back and forth with pointwise
split : ∀ {as bs} → Pointwise (λ a b → L a b ⊎ R a b) as bs →
∃₂ λ asr asl → Interleaving L R asl asr bs
split [] = [] , [] , []
split (inj₁ l ∷ pw) = Product.map _ (Product.map _ (l ∷ˡ_)) (split pw)
split (inj₂ r ∷ pw) = Product.map _ (Product.map _ (r ∷ʳ_)) (split pw)
unsplit : ∀ {l r as} → Interleaving L R l r as →
∃ λ bs → Pointwise (λ a b → L a b ⊎ R a b) bs as
unsplit [] = -, []
unsplit (l ∷ˡ sp) = Product.map _ (inj₁ l ∷_) (unsplit sp)
unsplit (r ∷ʳ sp) = Product.map _ (inj₂ r ∷_) (unsplit sp)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4