PFAD2章の最初のmsc

PFAD2.agda

module PFAD2 where

open import Function
open import Relation.Binary

module Ord {t₁ t₂ t₃} (T : DecTotalOrder t₁ t₂ t₃) where
  open import Data.List.NonEmpty
  open import Relation.Nullary

  open Relation.Binary.DecTotalOrder T
  private
    _?≤?_ = IsDecTotalOrder._≤?_ isDecTotalOrder
    X = Carrier

  max : X → X → X
  max a b with a ?≤? b
  ... | yes _ = b
  ... | no _ = a

  maximum : List⁺ X → X
  maximum = foldr max (λ x → x)

module Surpasser {t₁ t₂ t₃} (T : DecTotalOrder t₁ t₂ t₃) where
  open import Data.Bool
  open import Data.Nat
  open import Data.List using (List; []; length; filter)
  open import Data.List.NonEmpty
  open import Relation.Nullary.Decidable using (⌊_⌋)

  open Relation.Binary.DecTotalOrder T
  private
    _?≡?_ = IsDecTotalOrder._≟_ isDecTotalOrder
    _?≤?_ = IsDecTotalOrder._≤?_ isDecTotalOrder
    X = Carrier

  tails⁺ : ∀{x} {X : Set x} → List⁺ X → List⁺ (List⁺ X)
  tails⁺ [ x ] = [ [ x ] ]
  tails⁺ (x ∷ xs) = (x ∷ xs) ∷ tails⁺ xs

  scount : X → List X → ℕ
  scount x = length ∘ filter (λ y → not ⌊ x ?≡? y ⌋ ∧ ⌊ x ?≤? y ⌋ )

  msc : List⁺ X → ℕ
  msc = maximum ∘ map count ∘ tails⁺
    where
      open Ord decTotalOrder
      count : List⁺ Carrier → ℕ
      count [ x ] = scount x []
      count (x ∷ xs) = scount x $ toList xs

private
  module Test where
    import Relation.Binary.On as On
    import Data.String as Str
    import Data.Nat as Nat
    import Data.Char as Char
    import Data.List.NonEmpty as List⁺
    open import Relation.Binary.PropositionalEquality using (_≡_; refl)
    open Surpasser (On.decTotalOrder Nat.decTotalOrder Char.toNat)

    GENERATION = List⁺.fromList 'G' $ Str.toList "ENERATION"

    test-msc1 : msc GENERATION ≡ 6
    test-msc1 = refl