------------------------------------------------------------------------
-- 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 5 _∷_ _++_
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 5 _++ᵖ_
_++ᵖ_ : ∀ {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)
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