module Data.List.Relation.Binary.Suffix where

open import Data.Bool using (true; false; _∧_; _∨_)
open import Data.Empty using (⊥-elim)
open import Data.List using (List; []; _∷_; length)
open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_; setoid)
open import Data.Nat using (suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (n<1+n; ≤-step; <⇒≱; module ≤-Reasoning)
open import Data.Sum using (inj₁; inj₂; [_,_])
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Nullary using (yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Sum using (_⊎-dec_)

private
  variable
    a ℓ : Level

module _
  {A : Set a} (_≈_ : Rel A ℓ)
  where

  data Suffix : Rel (List A) (a ⊔ ℓ) where
    base : ∀ {xs ys} → (xs≋ys : Pointwise _≈_ xs ys) → Suffix xs ys
    next : ∀ y {xs ys} → Suffix xs ys → Suffix xs (y ∷ ys)

module _
  {A : Set a} {_≈_ : Rel A ℓ}
  where

  private
    _≋_ = Pointwise _≈_
    _<_ = Suffix _≈_

  length≤ : ∀ {xs ys} → xs < ys → length xs ≤ length ys
  length≤ (base [])            = z≤n
  length≤ (base (x∼y ∷ xs≋ys)) = s≤s (length≤ (base xs≋ys))
  length≤ (next y xs<ys)       = ≤-step (length≤ xs<ys)

  refl : Reflexive _≈_ → Reflexive _<_
  refl refl {xs} = base (Pointwise.refl refl)

  transitive : Transitive _≈_ → Transitive _<_
  transitive trans xs<ys          (next z ys<zs)       = next z (transitive trans xs<ys ys<zs)
  transitive trans (base xs≋ys)   (base ys≋zs)         = base (Pointwise.transitive trans xs≋ys ys≋zs)
  transitive trans (next y xs<ys) (base (y∼z ∷ ys≋zs)) = next _ (transitive trans xs<ys (base ys≋zs))

  antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
  antisymmetric sym (base xs≋ys) _ = xs≋ys
  antisymmetric sym (next _ _) (base ys≋xs) = Pointwise.symmetric sym ys≋xs
  antisymmetric sym (next y {x ∷ xs} {ys} x∷xs<ys) (next x y∷ys<xs) =
    ⊥-elim
      (<⇒≱ (≤-step (n<1+n (length xs)))
           (begin
             suc (suc (length xs)) ≡⟨⟩
             suc (length (x ∷ xs)) ≤⟨ s≤s (length≤ x∷xs<ys) ⟩
             suc (length ys) ≡⟨⟩
             length (y ∷ ys) ≤⟨ length≤ y∷ys<xs ⟩
             length xs ∎))
    where open ≤-Reasoning

  minimum : Minimum _<_ []
  minimum []       = base []
  minimum (x ∷ xs) = next x (minimum xs)

  decidable : Decidable _≈_ → Decidable _<_
  decidable ≈? [] ys = yes (minimum ys)
  decidable ≈? (x ∷ xs) [] = no (λ { (base ()) })
  decidable ≈? (x ∷ xs) (y ∷ ys) =
    Dec.map′ [ base , next y ]
             (λ { (base xs≋ys) → inj₁ xs≋ys ; (next _ xs<ys) → inj₂ xs<ys })
             (Pointwise.decidable ≈? (x ∷ xs) (y ∷ ys) ⊎-dec decidable ≈? (x ∷ xs) ys)