{-# 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 Data.Vec using (Vec)
import Data.Vec as V
open import Function.Base using (case_of_; id)
open import Relation.Binary.PropositionalEquality
-- 
module MealyLearning (I : Set Level.0ℓ) (O : Set Level.0ℓ)  where
open import Mealy I O

data F {ℓr : Level} (R : Set ℓr) {ℓ : Level} (X : Set ℓ) : Set (ℓ ⊔ ℓr) where
  -- the membership query sends an input word w and an output word of the same
  -- length:
  membership : ∀ {n} → (w : Vec I n) → (next : Vec O n → X) → F R X
  -- the equivalence query sends a DFA and a possible outcome R of the entire
  -- game and receives a counterexample
  equivalence : Mealy-Machine → (ret : R) → (next : List I → X) → F R X

open import Game-Definitions Mealy-Machine F

module _ {ℓr : Level} {R : Set ℓr} where
  open Mealy-Machine using (⟦_⟧*; ⟦_⟧ⁿ)
  -- 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 ((Mealy-Machine → 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 → ⟦ 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 → ⟦ M ⟧* w ≢ ⟦ 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 TeacherNaturality F-map
 
 
MealyLearning-Semantics : GameSemantics
MealyLearning-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 Mealy learning game:
record MealyTeacher (ℓt : Level) : Set (Level.suc ℓt) where
  field
    -- 1. an internal set of states
    T : Set ℓt
    st₀ : T
    answer-member : T → ∀ {n} → Vec I n → Vec O n × T
    answer-equiv : T → Mealy-Machine → Maybe (List I × T)

mkTeacherδ : ∀ {ℓt} {T : Set ℓt} → (T → ∀ {n} → Vec I n → Vec O n × T) → (T → Mealy-Machine → Maybe (List I × 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 → ∀ {n} → Vec I n → Vec O n × T} → {eq : T → Mealy-Machine → Maybe (List I × 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 → ∀ {n} → Vec I n → Vec O n × 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 → Mealy-Machine → Maybe (List I × T))
Teacherδ⇒equivalence teacher st hyp =
  case teacher {R = ⊤} (equivalence hyp tt id) st of λ
  { (inj₁ tt) → nothing
  ; (inj₂ (st' , w)) → just (w , st)
  }

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

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

open ExplicitWinningConditions MealyLearning-Semantics F-map MealyTeacher MealyTeacher⇒Teacher public