{-# OPTIONS --safe #-}

open import Level

open import Data.Product as Σ
open import Data.Sum as ⊎
open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation


open import Game-Basics

module Game-Definitions {ℓd : Level} (𝔻 : Set ℓd) (F : Game-Type) where
-- Games for learning something from the set 𝔻
-- for which games have the outcome R

record GameSemantics : Setω where
  field
    -- The datatype F allows the map operations of functors:
    F-map : Functorial F

    -- The semantics of a query 'F X' annotates each successor state in X
    -- with a predicate on ℕ reporting the information obtained from the query.
    -- This means that in the respective successor state after a query, we can assume
    -- that the secret from the learning domain 𝔻 satisfies the predicate.
    ⟦F_⟧ : {ℓr : Level} {R : Set ℓr} {ℓ : Level} {X : Set ℓ} → F R X → F R ((𝔻 → Set) × X)

    -- If we project away the predicate of the semantics, we obtain the original query:
    proj₂∘⟦F⟧ : ∀ {ℓr : Level} {R : Set ℓr} {ℓ : Level} {X : Set ℓ} {query : F R X} → F-map proj₂ (⟦F query ⟧) ≡ query

    -- The following is a property stating every successor state in a query satisfies the
    -- predicate P. In other words, _⊧F∀_ lifts the predicate from 'successors' of type X
    -- to 'queries' of type F X.
    -- One could define it for generic game types F but we require F to implement it explicitly
    -- because then working with it in examples becomes more instructive.
    _⊧F∀_ : {ℓr : Level} {R : Set ℓr} {ℓ ℓ' : Level} {X : Set ℓ} → F R X → (P : X → Set ℓ') → Set ℓ'

    -- If every successor state satisfies P, then we can pull this predicate into the query:
    F∀-elim : {ℓr : Level} {R : Set ℓr} {ℓ ℓ' : Level} {X : Set ℓ} → (query : F R X) → {P : X → Set ℓ'} → query ⊧F∀ P → F R (Σ X P)

    -- And if we project the predicate away, we again reobtain the original query:
    proj₁∘F∀elim : {ℓr : Level} {R : Set ℓr} {ℓ ℓ' : Level} {X : Set ℓ} → {query : F R X} → {P : X → Set ℓ'} → (res : query ⊧F∀ P) → F-map proj₁ (F∀-elim query res) ≡ query


-- A student/learner with internal state set C is an F-coalgebra:
-- in each state q in C it determines some query 'F C' with successor
-- states in C, which is then chosen depending on the teacher's response.
Learnerδ : ∀ {ℓr : Level} (R : Set ℓr) {ℓc : Level} (C : Set ℓc) → Set (ℓr Level.⊔ ℓc)
Learnerδ R C = C → F R C


record Learner-on {ℓr : Level} (R : Set ℓr) {ℓ} (C : Set ℓ) : Set (ℓr Level.⊔ ℓ) where
  field
    δ : Learnerδ R C

record Learner (ℓ : Level) : Set (Level.suc ℓ) where
  field
    C : Set ℓ
    R : Set ℓ
    q₀ : C
    learner-on : Learner-on R C
  open Learner-on learner-on public

-- A teacher with the internal state T:
Teacherδ : ∀ {ℓt : Level} (T : Set ℓt) → Setω
Teacherδ T = ∀ {ℓr : Level} {R : Set ℓr} {ℓ : Level} {X : Set ℓ} → F R X → M R T X
-- ^- the teacher is essentially an F-algebra in the kleisli category
--    of the state monad (with state T) extended by the exception monad
--    transformer (R ⊎ (-)). If the teacher returns R, then this
--    means 'surrendering' in the game, or in other words, the hypothesis
--    was correct.


-- The teacher may not interact with X, which means, that δ is natural in X,
-- so the teacher is a natural transformation from F to M T.
-- Naturality is almost enforced by X being an entirely opaque type.

module TeacherNaturality (F-map : Functorial F) where
   TeacherIsNaturalFor : ∀ {ℓr : Level} {R : Set ℓr} {ℓt : Level} {T : Set ℓt} → Teacherδ T → {ℓ1 ℓ2 : Level} → {X : Set ℓ1} → {Y : Set ℓ2} → (f : X → Y) → Set _
   TeacherIsNaturalFor {R = R} {T = T} δ {X = X} f = ∀ (q : F R X) → M-map f (δ q) ≗ δ (F-map f q)
   
   TeacherIsNatural : ∀ {ℓt : Level} {T : Set ℓt} → Teacherδ T → Setω
   TeacherIsNatural δ = ∀ {ℓr : Level} {R : Set ℓr} {ℓ1 ℓ2 : Level} → {X : Set ℓ1} → {Y : Set ℓ2}
                 → (f : X → Y) → TeacherIsNaturalFor {R = R} δ f

   record Teacher-on {ℓ} (T : Set ℓ) : Setω where
     field
       δ : Teacherδ T
       -- the teacher may not interact with X, which means, that δ is natural in X:
       natural : TeacherIsNatural δ
   
   record Teacher (ℓ : Level) : Setω where
     field
       T : Set ℓ
       st₀ : T
       teacher-on : Teacher-on T
     open Teacher-on teacher-on public
   
   

module Game (sem : GameSemantics) {ℓr : Level} {R : Set ℓr} {ℓ} {C : Set ℓ} {ℓt : Level} {T : Set ℓt} (teacher : Teacherδ T) (learner : Learnerδ R C) where
  open GameSemantics sem
  -- The definition of the game: with the teacher and the learner in respective states t and l,
  -- the learner first makes a move to a query that is then responded by the teacher
  game-step : T × C → R ⊎ (T × C)
  game-step (t , l) = teacher (learner l) t

  -- The same as the game step but annotated with the predicate of numbers
  -- that are still possible according to the teacher's current response:
  game-step-prop : T × C → R ⊎ (T × (𝔻 → Set) × C)
  game-step-prop (t , l) = teacher ⟦F learner l ⟧ t

  -- We encode the 'potential secret' as a predicat P on natural numbers
  -- meaning:
  --
  --       P holds for k
  --         <===>
  --    we do not know whether k is the secret or not.
  --
  -- So in particular, if the teacher accepts a hypothesis (or if the teacher
  -- simply surrenders), then the predicate is empty, because we then know
  -- for every natural number whether it was the secret or not
  still-possible : T × C → ℕ → (𝔻 → Set)
  still-possible q ℕ.zero = λ x → ⊤
  still-possible q (ℕ.suc r) =
    case game-step-prop q of λ
    { (inj₁ ret) → (λ x → ⊥)
    ; (inj₂ (t' , _∈response , l')) →
      λ x → x ∈response × still-possible (t' , l') r x
    }

  -- The following property states that in the state q of the game (i.e. teacher
  -- and learner state), the learner within the next r rounds, if the hidden
  -- number was 'cand'.
  learner_finds_within_rounds : T × C → 𝔻 → ℕ → Set
  learner q finds secret within ℕ.zero rounds = ⊥ -- learner didn't guess n
  learner q finds secret within ℕ.suc r rounds =
    case game-step-prop q of λ
    { (inj₁ _) → ⊤ -- learner either guessed correctly or teacher surrendered
    ; (inj₂ (t' , _∈response , l')) →
       -- if the teacher's response did not yet refute 'secret'
       secret ∈response
       -- then the learner will guess it within the next r rounds:
       → learner (t' , l') finds secret within r rounds
    }

  -- when running the game from state q for r rounds,
  -- if the number x is still possible, it indeed means that the learner has not
  -- yet guessed it:
  still-possible⇒¬finds : ∀ q r x → still-possible q r x → ¬ (learner q finds x within r rounds)
  still-possible⇒¬finds q ℕ.zero x still-poss = λ ()
  still-possible⇒¬finds q (ℕ.suc r) x still-poss with (game-step-prop q)
  still-possible⇒¬finds q (ℕ.suc r) x (x∈resp , x-still-poss) | inj₂ (t' , _∈response , l') =
    λ x∈resp⇒learner-guess → still-possible⇒¬finds (t' , l') r x x-still-poss (x∈resp⇒learner-guess x∈resp)

  open TeacherNaturality F-map
  -- only a sanity check: if the teacher is natural, then game-step-prop yields same data
  -- as game-step, just with the additional predicate: 
  proj∘game-step-prop : TeacherIsNatural teacher → (q : T × C) → game-step q ≡ ⊎.map₂ (Σ.map₂ proj₂) (game-step-prop q)
  proj∘game-step-prop teacher-natural (t , l) =
    begin
    game-step (t , l)  ≡⟨⟩
    teacher (learner l) t ≡⟨ cong (λ - → teacher - t) proj₂∘⟦F⟧ ⟨
    teacher (F-map proj₂ ⟦F learner l ⟧) t ≡⟨ teacher-natural proj₂ _ t ⟨
    M-map proj₂ (teacher ⟦F learner l ⟧) t   ≡⟨⟩
    ⊎.map₂ (Σ.map₂ proj₂) (game-step-prop (t , l))
    ∎
    where
      open ≡-Reasoning

module ExplicitWinningConditions
       (sem : GameSemantics)       
       (F-map : Functorial F)
       (ExplicitTeacher : (ℓt : Level) → Set (Level.suc ℓt))
       (mkTeacher : ∀ {ℓt : Level} → ExplicitTeacher ℓt → TeacherNaturality.Teacher F-map ℓt)
       where
  open TeacherNaturality F-map

  -- The property that a learner finds a given secret number of a teacher within
  -- n rounds:
  _learns_from_within_rounds : ∀ {ℓ} {ℓ'} → Learner ℓ → 𝔻 → ExplicitTeacher ℓ' → ℕ → Set
  _learns_from_within_rounds learner secret teacher r =
    learner teacher.st₀ , learner.q₀ finds secret within r rounds
    where
      module teacher = Teacher (mkTeacher (teacher))
      module learner = Learner learner
      open Game sem teacher.δ learner.δ

  _defeats_with-bound_ : ∀ {ℓ} {ℓ'} → Learner ℓ → ExplicitTeacher ℓ' → (𝔻 → ℕ) → Set ℓd
  _defeats_with-bound_ learner teacher bound =
    ∀ secret → learner learns secret from teacher within bound (secret) rounds 

  _can't-learn_from_within_rounds : ∀ {ℓ} {ℓ'} → Learner ℓ → 𝔻 → ExplicitTeacher ℓ' → ℕ → Set
  _can't-learn_from_within_rounds learner secret teacher r =
    still-possible (teacher.st₀ , learner.q₀) r secret
    where
      module teacher = Teacher (mkTeacher teacher)
      module learner = Learner learner
      open Game sem teacher.δ learner.δ