{-# OPTIONS --safe #-}

-- ------------------------------
-- Learning of DFAs when tracking the size of
-- the longest counter example
-- ------------------------------

open import Level

open import Data.Empty
open import Data.List
open import Data.Bool hiding (T; _≤_)
open import Data.Product
open import Data.Maybe
open import Data.Nat hiding (_⊔_)
open import Data.Sum
open import Data.Unit
open import Function.Base using (case_of_; id)
open import Relation.Binary.PropositionalEquality

module DFA-CE-Size-Learning (A : Set Level.0ℓ)  where
open import DFA A

⟦DFA_⟧ = DFA.⟦DFA⟧₀

data F {ℓr : Level} (R : Set ℓr) {ℓ : Level} (X : Set ℓ) : Set (ℓ ⊔ ℓr) where
  -- the membership query sends an input word w and receives a boolean
  membership : (w : List A) → (next : Bool → X) → F R X
  -- the equivalence query sends a DFA and a possible outcome R of the entire
  -- game and receives a counterexample
  equivalence : DFA → (ret : R) → (next : List A → X) → F R X

open import Game-Definitions (DFA × ℕ) F

module DFA-CE-Sem {ℓr : Level} {R : Set ℓr} where
  -- The semantics of a query 'F X' annotates each successor state in X
  -- with a predicate on DFAs reporting the information obtained from the query.
  -- This means that in the respective successor state after a query, we can assume
  -- that the hidden number satisfies the predicate.
  ⟦F_⟧ : {ℓ : Level} {X : Set ℓ} → F R X → F R ((DFA × ℕ → Set) × X)
  -- The semantics of the membership query is: when receiving b ∈ Bool,
  -- we know that the output of the secret DFA M for input w is b
  ⟦F membership w next ⟧ = membership w (λ b → (λ { (M , _) → ⟦DFA M ⟧ w ≡ b}) , (next b))
  -- The semantics of the equivalence query: when receiving the
  -- counter example w, it means that the secret DFA M sends w
  -- to a different output than the hypothesis 'hyp'
  ⟦F equivalence hyp ret next ⟧ =
    equivalence hyp ret
        λ w → (λ { (M , len) → ⟦DFA M ⟧ w ≢ ⟦DFA hyp ⟧ w × length w ≤ len }) , (next w)

  
  -- The datatype F allows the map operations of functors:
  F-map :  {ℓ ℓ'  : Level} {X : Set ℓ} {Y : Set ℓ'} → (f : X → Y) → F R X → F R Y
  F-map f (membership w next) = membership w (λ x → f (next x))
  F-map f (equivalence hyp ret next) = equivalence hyp ret λ x → f (next x)
  
  -- If we project away the predicate of the semantics, we obtain the original query:
  proj₂∘⟦F⟧ : ∀  {ℓ : Level} {X : Set ℓ} {query : F R X} → F-map proj₂ (⟦F query ⟧) ≡ query
  proj₂∘⟦F⟧ {query = membership w next} = refl
  proj₂∘⟦F⟧ {query = equivalence x ret next} = refl

  -- The following is a property stating every successor state in a query satisfies the
  -- predicate P:
  _⊧F∀_ : {ℓ ℓ' : Level} {X : Set ℓ} → F R X → (P : X → Set ℓ') → Set ℓ'
  membership w next ⊧F∀ P = ∀ b → P (next b)
  equivalence x ret next ⊧F∀ P = ∀ w → P (next w)

  -- If every successor state satisfies P, then we can pull this predicate into the query:
  F∀-elim : {ℓ ℓ' : Level} {X : Set ℓ} → (query : F R X) → {P : X → Set ℓ'} → query ⊧F∀ P → F R (Σ X P)
  F∀-elim (membership w next) q⊧P = membership w (λ b → next b , q⊧P b)
  F∀-elim (equivalence hyp ret next) q⊧P = equivalence hyp ret λ w → (next w) , (q⊧P w)

  -- And if we project the predicate away, we again obtain the original query:
  proj₁∘F∀elim : {ℓ ℓ' : Level} {X : Set ℓ} → {query : F R X} → {P : X → Set ℓ'} → (res : query ⊧F∀ P) → F-map proj₁ (F∀-elim query res) ≡ query
  proj₁∘F∀elim {query = membership w next} _ = refl
  proj₁∘F∀elim {query = equivalence x ret next} _ = refl

open DFA-CE-Sem public

open TeacherNaturality F-map


DFALearning-Semantics : GameSemantics
DFALearning-Semantics = record
  { F-map = F-map
  ; ⟦F_⟧ = ⟦F_⟧
  ; proj₂∘⟦F⟧ = proj₂∘⟦F⟧
  ; _⊧F∀_ = _⊧F∀_
  ; F∀-elim = F∀-elim
  ; proj₁∘F∀elim = proj₁∘F∀elim
  }