{-# OPTIONS --safe #-}

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.Sum
open import Data.Unit
open import Function.Base using (case_of_; id)
open import Relation.Binary.PropositionalEquality

module DFALearning (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 DFASem {ℓ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 → ⟦DFA M ⟧ w ≢ ⟦DFA hyp ⟧ w) , (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 DFASem 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
  }


-- The explicit definition of a teacher for the DFA learning game:
record DFATeacher (ℓt : Level) : Set (Level.suc ℓt) where
  field
    -- 1. an internal set of states
    T : Set ℓt
    st₀ : T
    answer-member : T → List A → Bool × T
    answer-equiv : T → DFA → Maybe (List A × T)

mkTeacherδ : ∀ {ℓt} {T : Set ℓt} → (T → List A → Bool × T) → (T → DFA → Maybe (List A × T)) → Teacherδ T
mkTeacherδ member equiv (membership w next) st with (member st w)
... | b , st' = inj₂ (st' , next b)
mkTeacherδ member equiv (equivalence hyp ret next) st with (equiv st hyp)
... | just (w , st') = inj₂ (st' , (next w))
... | nothing = inj₁ ret

mkTeacherδ-natural : ∀ {ℓt} {T : Set ℓt} → {mq : T → List A → Bool × T} → {eq : T → DFA → Maybe (List A × T)} → TeacherIsNatural (mkTeacherδ mq eq)
mkTeacherδ-natural f (membership w next) st = refl
mkTeacherδ-natural {eq = eq} f (equivalence hyp ret next) st with (eq st hyp)
... | just _ = refl
... | nothing = refl

Teacherδ⇒membership : ∀ {ℓt} {T : Set ℓt} → Teacherδ T → (T → List A → Bool × T)
Teacherδ⇒membership teacher st w =
  case teacher {R = ⊥} (membership w id) st  of λ
  { (inj₂ (st' , b)) → b , st' }

Teacherδ⇒equivalence : ∀ {ℓt} {T : Set ℓt} → Teacherδ T → (T → DFA → Maybe (List A × T))
Teacherδ⇒equivalence teacher st hyp =
  case teacher {R = ⊤} (equivalence hyp tt id) st of λ
  { (inj₁ tt) → nothing
  ; (inj₂ (st' , w)) → just (w , st)
  }

DFATeacher⇒Teacher : ∀ {ℓt} → DFATeacher ℓt → Teacher ℓt
DFATeacher⇒Teacher teacher = record
  { T = T
  ; st₀ = st₀
  ; teacher-on = record
    { δ = mkTeacherδ answer-member answer-equiv
    ; natural = mkTeacherδ-natural
    }
  }
  where
    open DFATeacher teacher

Teacher⇒DFATeacher : ∀ {ℓt} → Teacher ℓt → DFATeacher ℓt
Teacher⇒DFATeacher teacher =
  record
  { T = T
  ; st₀ = st₀
  ; answer-member = Teacherδ⇒membership δ
  ; answer-equiv = Teacherδ⇒equivalence δ
  }
  where
    open Teacher teacher

open ExplicitWinningConditions DFALearning-Semantics F-map DFATeacher DFATeacher⇒Teacher public