{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Unary.Grouped where
open import Data.List.Base using (List; []; _∷_; map)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Product.Base using (_×_; _,_)
open import Relation.Binary.Core using (REL; Rel)
open import Relation.Binary.Definitions as B
open import Relation.Unary as U using (Pred)
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_)
open import Level using (Level; _⊔_)
private
variable
a ℓ : Level
A : Set a
x y : A
xs : List A
infixr 5 _∷≉_ _∷≈_
data Grouped {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where
[] : Grouped _≈_ []
_∷≉_ : All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs)
_∷≈_ : x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
module _ {_≈_ : Rel A ℓ} where
grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_)
grouped? _≟_ [] = yes []
grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
grouped? _≟_ (x ∷ y ∷ xs) =
Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
where
from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
from (inj₁ x≈y , grouped[y∷xs]) = x≈y ∷≈ grouped[y∷xs]
from (inj₂ all[x≉,y∷xs] , grouped[y∷xs]) = all[x≉,y∷xs] ∷≉ grouped[y∷xs]
to : Grouped _≈_ (x ∷ y ∷ xs) → ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs)
to (all[x≉,y∷xs] ∷≉ grouped[y∷xs]) = inj₂ all[x≉,y∷xs] , grouped[y∷xs]
to (x≈y ∷≈ grouped[y∷xs]) = inj₁ x≈y , grouped[y∷xs]