{-# OPTIONS --safe #-}

open import Level

open import Data.Empty
open import Data.Nat as ℕ hiding (_⊔_)
open import Data.Nat.Properties as ℕ
open import Data.Product
open import Data.Maybe
open import Data.Product.Base as Σ
open import Data.Sum as ⊎
open import Data.Unit
open import Function.Base using (case_of_; id)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation

open import Utils

module NatLearning where

-- A simple learning interface for the game of guessing natural numbers.
-- Here, there is only one query: the learner guesses a number.
-- Together with the hypothesis, the learner provides a value of type 'R'
-- (intuitively the return type) which is the result of the entire game if
-- the hypothesis is correct.
-- If the guess is wrong, the teacher responds either
-- 'too-low' or 'too-high', which we define first:
data WrongNat : Set where
  too-high : WrongNat -- the learner's guess was too high
  too-low : WrongNat -- the learner's guess was too low

-- With this type, we can define the interface 
data F {ℓr : Level} (R : Set ℓr) {ℓ : Level} (X : Set ℓ) : Set (ℓ ⊔ ℓr) where
  -- there is only one kind of query: guessing a number
  guess : (hyp : ℕ) → (ret : R) → (next : WrongNat → X) → F R X

open import Game-Definitions ℕ F public

-- We can define the semantics of such a query by first defining the
-- semantics of WrongNat:
⟦WrongNat_⟧ : WrongNat → ℕ → ℕ → Set
⟦WrongNat_⟧ too-low hyp truth = hyp < truth
⟦WrongNat_⟧ too-high hyp truth = hyp > truth

module NatSem {ℓr : Level} {R : Set ℓr} where
  -- 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 hidden number satisfies the predicate.
  ⟦F_⟧ : {ℓ : Level} {X : Set ℓ} → F R X → F R ((ℕ → Set) × X)
  ⟦F_⟧ (guess hyp ret next) = guess hyp ret λ wn → ⟦WrongNat wn ⟧ hyp , next wn
  
  -- 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 (guess hyp ret next) = guess hyp ret (λ r → f (next r))
  
  -- 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 = guess hyp 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 ℓ'
  _⊧F∀_ (guess hyp ret next) P = ∀ resp → P (next resp)
  
  -- 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 (guess hyp ret next) prop = guess hyp ret (λ resp → next resp , prop resp)
  
  -- 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 = guess hyp ret next} _ = refl

open NatSem public

-- Above learning game is an instance of the general definition
-- of a type of learning game:
NatLearning-Semantics : GameSemantics
NatLearning-Semantics = record
  { ⟦F_⟧ = ⟦F_⟧
  ; F-map = F-map
  ; proj₂∘⟦F⟧ = proj₂∘⟦F⟧
  ; _⊧F∀_ = _⊧F∀_
  ; F∀-elim = F∀-elim
  ; proj₁∘F∀elim = proj₁∘F∀elim
  }

-- The explicit definition of a teacher with internal states T:
NatTeacher-on : ∀ {ℓt : Level} (T : Set ℓt) → Set ℓt
NatTeacher-on T = (T → ℕ → Maybe (WrongNat × T))

-- The explicit definition of a teacher for the nat learning game:
record NatTeacher (ℓt : Level) : Set (Level.suc ℓt) where
  field
    -- 1. an internal set of states
    T : Set ℓt
    st₀ : T
    -- 2. a map that answers the only type of query available:
    δ : NatTeacher-on T

NatLearner : (ℓ : Level) → Set (Level.suc ℓ)
-- A learner for the natural number learning game
-- is literally a set C with a map C → F R C
-- for above F:
NatLearner = Learner

open TeacherNaturality F-map public

-- In the simple example of NatLearning, a teacher is essentially a map
-- from internal state and hypothesis to either 'nothing' if the hypothesis
-- is correct or a pair of a new successor state and the answer of type WrongNat.
mkTeacherδ : ∀ {ℓt : Level} {T : Set ℓt} → NatTeacher-on T → Teacherδ T
mkTeacherδ f (guess hyp ret next) st =
  case (f st hyp) of λ
  { nothing → inj₁ ret
  ; (just (wrong , st')) → inj₂ (st' , next wrong)
  }

mkTeacherδ-IsNatural : ∀ {ℓt : Level} {T : Set ℓt} → (f : NatTeacher-on T) → TeacherIsNatural (mkTeacherδ f)
mkTeacherδ-IsNatural δ f (guess hyp ret next) st with (δ st hyp)
... | just x = refl
... | nothing = refl

mkTeacher-on : ∀ {ℓt : Level} {T : Set ℓt} → NatTeacher-on T → Teacher-on T
mkTeacher-on f = record { δ = mkTeacherδ f ; natural = mkTeacherδ-IsNatural f }

mkTeacher : ∀ {ℓt : Level} → NatTeacher ℓt → Teacher ℓt
mkTeacher teacher =
    record { T = T ; st₀ = st₀ ; teacher-on = mkTeacher-on δ }
    where open NatTeacher teacher

mkTeacher-on⁻¹ : ∀ {ℓt : Level} {T : Set ℓt} → Teacher-on T → NatTeacher-on T
mkTeacher-on⁻¹ teacher st hyp with (Teacher-on.δ teacher (guess hyp tt id) st)
... | inj₁ tt = nothing
... | inj₂ (st' , wn) = just (wn , st')

mkTeacher⁻¹ : ∀ {ℓt : Level} → Teacher ℓt → NatTeacher ℓt
mkTeacher⁻¹ teacher = record { T = T ; st₀ = st₀ ; δ = mkTeacher-on⁻¹ teacher-on }
  where
    open Teacher teacher


open ExplicitWinningConditions NatLearning-Semantics F-map NatTeacher mkTeacher public