{-# OPTIONS --safe  #-}

open import Level
import DFA as D
open import Data.Nat
open import Data.Sum
open import Data.Empty
open import Data.List
import Data.Nat.Properties as ℕ
open import Data.Product
open import Function.Base
open import Relation.Binary.PropositionalEquality

module DFA-Examples.Enumerator (A : Set 0ℓ) (dfa[_] : ℕ → D.DFA A) where
-- Assume that we are provided with a function that sends a natural number
-- n to the n-th DFA. Then we can build a simple learner
-- that just enumerates all DFAs:

open import DFA A
open import DFALearning A
open import Game-Definitions DFA F
open import Learner-Correctness DFA F DFALearning-Semantics

δ : Learnerδ DFA ℕ
-- in state n, just guess the n-th DFA:
-- if its wrong, continue with the next one
δ n = equivalence dfa[ n ] dfa[ n ] (λ _ →  + n)

enumerator : Learner 0ℓ
enumerator = record
  { C = ℕ
  ; R = DFA
  ; q₀ = 
  ; learner-on = record {
    δ = δ
    }
  }

-- This learner is correct given that dfa[_] is surjective:
module enumerator-correct
       -- the index of a dfa in the sequence:
       (b : DFA → ℕ)
       -- so that dfa[ b M ] accepts the same language as M:
       (surjective : ∀ (M : DFA) → M ≈ dfa[ b M ])
       where

  -- for a dfa with index k, it takes k + 1 queries to learn it
  bound : DFA → ℕ
  bound M =  + b M

  enumerator-step-bounded : Learner-Stepping δ  bound
  enumerator-step-bounded =
    record
     { ticks = id
     ; allows = λ n M → n ≤ b M 
     ; q₀-correct = λ _ → z≤n
     ; ticks-below-bound = λ _ _ q≤idx → s≤s q≤idx
     ; preserve = λ {n} {M} n≤idx[M] w M⟦w⟧≢dfa[n]⟦w⟧ →
                case (ℕ.m≤n⇒m<n∨m≡n n≤idx[M]) of λ
                { (inj₁ n<idx[M]) → n<idx[M] , s≤s (ℕ.≤-reflexive refl)
                ; (inj₂ n≡idx[M]) →
                  -- a contradiction, because M⟦w⟧≢dfa[n]⟦w⟧ refutes
                  -- the most recent conjecture dfa[ n ]:
                  ⊥-elim (M⟦w⟧≢dfa[n]⟦w⟧ (begin
                    ⟦DFA M ⟧ w ≡⟨ (surjective M) w ⟩
                    ⟦DFA dfa[ b M ] ⟧ w ≡⟨ cong (λ - → ⟦DFA dfa[ - ] ⟧ w) n≡idx[M] ⟨
                    ⟦DFA dfa[ n ] ⟧ w
                  ∎))
                }
     }
     where open ≡-Reasoning

  -- This learner wins against every teacher:
  thm : ∀ {ℓt} (teacher : DFATeacher ℓt)
      → enumerator defeats teacher with-bound (λ - →  + b -)
  thm teacher =
    Correctness.learner-correct
      (Teacher.teacher-on (DFATeacher⇒Teacher teacher))
      (record { δ = δ })  bound enumerator-step-bounded (DFATeacher.st₀ teacher)
    where
      open TeacherNaturality F-map