module Data.List.Relation.Binary.Prefix where

open import Data.Empty using (⊥-elim)
open import Data.List.Base using (List; []; _∷_; _++_; length; inits; map)
open import Data.List.Properties using (length-++)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_; setoid)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Nat using (_≤_; z≤n; s≤s; _+_) renaming (_<_ to _<ⁿ_)
open import Data.Nat.Properties using (<⇒≱; m<m+n; module ≤-Reasoning)
open import Data.Product using (_,_; uncurry)
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Nullary using (Dec; yes; no; ¬_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Unary using (Pred)

private
  variable
    a ℓ : Level

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

  data Prefix : Rel (List A) ℓ where
    base : P                                    → Prefix [] []
    halt : ∀ {y ys}                             → Prefix [] (y ∷ ys)
    next : ∀ {x xs y ys}
           (x≈y : x ≈ y) (xs<ys : Prefix xs ys) → Prefix (x ∷ xs) (y ∷ ys)

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

  private
    _≋_ = Pointwise _≈_
    _<_ = Prefix P _≈_

  initsPrefixes : P → Reflexive _≈_ → ∀ xs → All (_< xs) (inits xs)
  initsPrefixes p refl []       = base p ∷ []
  initsPrefixes p refl (x ∷ xs) = halt ∷ map′ (x ∷_ ) (next refl) (initsPrefixes p refl xs)
    where
    map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
           (f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → All P xs → All Q (map f xs)
    map′ f pres []         = []
    map′ f pres (px ∷ pxs) = pres px ∷ map′ f pres pxs

  module _
    (equivalence : IsEquivalence _≈_)
    where

    open IsEquivalence equivalence
    open import Data.List.Membership.Setoid (setoid (record { isEquivalence = equivalence })) using (_∈_)
    open import Data.List.Relation.Unary.Any using (Any; here; there)

    prefix∈inits : ∀ {xs ys} → xs < ys → xs ∈ inits ys
    prefix∈inits (base x)         = here []
    prefix∈inits halt             = here []
    prefix∈inits (next x≈y xs<ys) = there (map′ (_∷_ _) (x≈y ∷_) (prefix∈inits xs<ys))
      where
      map′ : ∀ {a b p q} {A : Set a} {B : Set b} {P : Pred A p} {Q : Pred B q} →
           (f : A → B) → (∀ {x} → P x → Q (f x)) → ∀ {xs} → Any P xs → Any Q (map f xs)
      map′ f pres (here px) = here (pres px)
      map′ f pres (there pxs) = there (map′ f pres pxs)

  reflexive : P → Reflexive _≈_ → Reflexive _<_
  reflexive p refl {[]}      = base p
  reflexive p refl {x ∷ xs} = next refl (reflexive p refl)

  irreflexive : ¬ P → Irreflexive _≋_ _<_
  irreflexive ¬p []          (base p)       = ¬p p
  irreflexive ¬p (_ ∷ xs≋ys) (next _ xs<ys) = irreflexive ¬p xs≋ys xs<ys

  transitive : Transitive _≈_ → Transitive _<_
  transitive trans (base _)         ys<zs            = ys<zs
  transitive trans halt             (next _ _)       = halt
  transitive trans (next x≈y xs<ys) (next y≈z ys<zs) =
    next (trans x≈y y≈z) (transitive trans xs<ys ys<zs)

  antisymmetric : Symmetric _≈_ → Antisymmetric _≋_ _<_
  antisymmetric sym (base _)         (base _)         = []
  antisymmetric sym (next x≈y xs<ys) (next y≈x ys<xs) =
    x≈y ∷ antisymmetric sym xs<ys ys<xs

  decidable : Dec P → Decidable _≈_ → Decidable _<_
  decidable P? _≈?_ []       []       = Dec.map′ base (λ { (base p) → p }) P?
  decidable P? _≈?_ []       (x ∷ ys) = yes halt
  decidable P? _≈?_ (x ∷ xs) []       = no λ ()
  decidable P? _≈?_ (x ∷ xs) (y ∷ ys) =
    Dec.map′ (uncurry next)
             (λ { (next x≈y xs<ys) → x≈y , xs<ys })
             ((x ≈? y) ×-dec (decidable P? _≈?_ xs ys))

  length≤ : ∀ {xs} {ys} → xs < ys → length xs ≤ length ys
  length≤ (base x)         = z≤n
  length≤ halt             = z≤n
  length≤ (next x≈y xs<ys) = s≤s (length≤ xs<ys)

  length< : ∀ {xs} {ys} → ¬ P → xs < ys → length xs <ⁿ length ys
  length< ¬p (base p)         = ⊥-elim (¬p p)
  length< ¬p halt             = s≤s z≤n
  length< ¬p (next x≈y xs<ys) = s≤s (length< ¬p xs<ys)

  minimum : P → Minimum _<_ []
  minimum p []       = base p
  minimum p (x ∷ xs) = halt

  ¬maximum : A → ∀ xs → ¬ Maximum _<_ xs
  ¬maximum a xs max =
    <⇒≱
      (begin-strict
        length xs                   <⟨  m<m+n (length xs) (s≤s z≤n) ⟩
        length xs + length (a ∷ []) ≡˘⟨ length-++ xs ⟩
        length (xs ++ a ∷ [])       ∎)
      (length≤ (max (xs ++ a ∷ [])))
    where open ≤-Reasoning