------------------------------------------------------------------------
-- The Agda standard library
--
-- 'Sufficient' lists: a structurally inductive view of lists xs
-- as given by xs ≡ non-empty prefix + sufficient suffix
--
-- Useful for termination arguments for function definitions
-- which provably consume a non-empty (but otherwise arbitrary) prefix
-- *without* having to resort to ancillary WF induction on length etc.
-- e.g. lexers, parsers etc.
--
-- Credited by Conor McBride as originally due to James McKinna
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.List.Relation.Unary.Sufficient where

open import Level using (Level; _⊔_)
open import Data.List.Base using (List; []; _∷_; [_]; _++_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private
  variable

    a b : Level
    A : Set a
    x : A
    xs : List A

------------------------------------------------------------------------
-- Sufficient builder

suffAcc : {A : Set a} (B :  List A → Set b) (xs : List A) → Set (a ⊔ b)
suffAcc B xs = ∀ {x} {prefix} suffix → xs ≡ x ∷ prefix ++ suffix → B suffix

------------------------------------------------------------------------
-- Sufficient view

data Sufficient {A : Set a} : (xs : List A) → Set a where

  acc : ∀ {xs} (ih : suffAcc Sufficient xs) → Sufficient xs


------------------------------------------------------------------------
-- Sufficient properties

-- constructors

module Constructors where

  []⁺ : Sufficient {A = A} []
  []⁺ = acc λ _ ()

  ∷⁺ : Sufficient xs → Sufficient (x ∷ xs)
  ∷⁺ {xs = xs} suffices@(acc hyp) = acc λ { _ refl → suf _ refl }
    where
      suf : ∀ prefix {suffix} → xs ≡ prefix ++ suffix → Sufficient suffix
      suf []               refl = suffices
      suf (_ ∷ _) {suffix} eq   = hyp suffix eq

-- destructors

module Destructors where

  acc-inverse : ∀ ys → Sufficient (x ∷ xs ++ ys) → Sufficient ys
  acc-inverse ys (acc hyp) = hyp ys refl

  ++⁻ : ∀ xs {ys : List A} → Sufficient (xs ++ ys) → Sufficient ys
  ++⁻ []            suffices = suffices
  ++⁻ (x ∷ xs) {ys} suffices = acc-inverse ys suffices

  ∷⁻ : Sufficient (x ∷ xs) → Sufficient xs
  ∷⁻ {x = x} = ++⁻ [ x ]


------------------------------------------------------------------------
-- Sufficient view covering property

module View where

  open Constructors

  sufficient : (xs : List A) → Sufficient xs
  sufficient []       = []⁺
  sufficient (x ∷ xs) = ∷⁺ (sufficient xs)

------------------------------------------------------------------------
-- Recursion on the sufficient view

module _ (B : List A → Set b) (rec : ∀ ys → (ih : suffAcc B ys) → B ys)
  where

  open View

  suffRec′ : ∀ {zs} → Sufficient zs → B zs
  suffRec′ {zs} (acc hyp) = rec zs (λ xs eq → suffRec′ (hyp xs eq))

  suffRec : ∀ zs → B zs
  suffRec zs = suffRec′ (sufficient zs)