------------------------------------------------------------------------
-- An example: A function that, given a stream, tries to find an
-- element satisfying a predicate
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Search where

open import Equality.Propositional
open import Interval using (⟨ext⟩)
open import Prelude hiding (; head; tail)

open import Monad equality-with-J
open import Univalence-axiom equality-with-J

open import Partiality-algebra.Monotone
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints
open import Partiality-monad.Inductive.Monad

-- Streams.

infixr 5 _∷_

record Stream {a} (A : Set a) : Set a where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A

open Stream

-- A direct implementation of the function.

module Direct {a} {A : Set a} (q : A  Bool) where

  Φ : Trans (Stream A)  _  A)
  Φ f xs = if q (head xs) then return (head xs) else f (tail xs)

  Φ-monotone :
     {f₁ f₂}  (∀ xs  f₁ xs  f₂ xs)   xs  Φ f₁ xs  Φ f₂ xs
  Φ-monotone f₁⊑f₂ xs with q (head xs)
  ... | true  = return (head xs)  
  ... | false = f₁⊑f₂ (tail xs)

  Φ-⊑ : Trans-⊑ (Stream A)  _  A)
  Φ-⊑ = record { function = Φ; monotone = Φ-monotone }

  search : Stream A  A 
  search = fix→ Φ-⊑

  search-least :
     f  (∀ xs  Φ f xs  f xs) 
     xs  search xs  f xs
  search-least = fix→-is-least Φ-⊑

  Φ-ω-continuous :
    (s :  λ (f :   Stream A  A ) 
            n xs  f n xs  f (suc n) xs) 
    Φ (  at s)    at [ Φ-⊑ $ s ]-inc
  Φ-ω-continuous s = ⟨ext⟩ helper
    where
    helper :  xs  Φ (  at s) xs   (at [ Φ-⊑ $ s ]-inc xs)
    helper xs with q (head xs)
    ... | true  = return (head xs)               ≡⟨ sym ⨆-const ⟩∎
                   (constˢ (return (head xs)))  
    ... | false =  (at s (tail xs))             

  Φ-ω : Trans-ω (Stream A)  _  A)
  Φ-ω = record
    { monotone-function = Φ-⊑
    ; ω-continuous      = Φ-ω-continuous
    }

  search-fixpoint : search  Φ search
  search-fixpoint = fix→-is-fixpoint-combinator Φ-ω

-- An arguably more convenient implementation, with the potential
-- drawback that one of the lemmas depends on propositional
-- extensionality.

module Indirect {a} {A : Set a} (q : A  Bool) where

  ΦP : Stream A  Partial (Stream A)  _  A) A
  ΦP xs =
    if q (head xs) then
      return (head xs)
    else
      rec (tail xs)

  Φ : Trans (Stream A)  _  A)
  Φ = Trans-⊑.function (transformer ΦP)

  search : Stream A  A 
  search = fixP ΦP

  search-least :
     f  (∀ xs  Φ f xs  f xs) 
     xs  search xs  f xs
  search-least = fixP-is-least ΦP

  search-fixpoint :
    Propositional-extensionality a 
    search  Φ search
  search-fixpoint prop-ext = fixP-is-fixpoint-combinator prop-ext ΦP