```------------------------------------------------------------------------
-- Various utility functions
------------------------------------------------------------------------

module Utilities where

open import Data.Bool
open import Data.Bool.Properties using (T-∧)
open import Data.Char as Char
open import Data.List
open import Data.List.NonEmpty as List⁺
open import Data.Nat as Nat
open import Data.Product
open import Data.String as String using (String)
open import Function
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence
using () renaming (module Equivalence to Eq)
open import Relation.Binary
import Relation.Binary.Props.DecTotalOrder as DTO
import Relation.Binary.Props.StrictTotalOrder as STO
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Some comparison operators

-- Is one number strictly smaller than another?

_<?ℕ_ : ℕ → ℕ → Bool
n₁ <?ℕ n₂ = ⌊ StrictTotalOrder._<?_
(DTO.strictTotalOrder Nat.decTotalOrder)
n₁ n₂ ⌋

-- Is one character smaller than or equal to another?

_≤?C_ : Char → Char → Bool
c₁ ≤?C c₂ = ⌊ DecTotalOrder._≤?_
(STO.decTotalOrder Char.strictTotalOrder)
c₁ c₂ ⌋

------------------------------------------------------------------------
-- Conversion of strings satisfying given predicates to annotated
-- lists

private
mutual

str′ : {p : Char → Bool}
(s : List Char) → T (all p s) → List (∃ (T ∘ p))
str′ []       _  = []
str′ (t ∷ ts) ok = List⁺.toList (str⁺′ (t ∷ ts) ok)

str⁺′ : {p : Char → Bool}
(s : List⁺ Char) → T (all p (List⁺.toList s)) →
List⁺ (∃ (T ∘ p))
str⁺′ (t ∷ ts) ok =
let (ok₁ , ok₂) = Eq.to T-∧ ⟨\$⟩ ok in
(t , ok₁) ∷ str′ ts ok₂

str : {p : Char → Bool}
(s : String)
{ok : T (all p \$ String.toList s)} →
List (∃ (T ∘ p))
str s {ok} = str′ (String.toList s) ok

str⁺ : {p : Char → Bool}
(s : String)
{ok₁ : T (all p \$ String.toList s)}
{ok₂ : T (not \$ null \$ String.toList s)} →
List⁺ (∃ (T ∘ p))
str⁺ s {ok₂ = _} with String.toList s
str⁺ s {ok₂ = ()} | []
str⁺ s {ok₁ = ok} | c ∷ cs = str⁺′ (c ∷ cs) ok
```