{-# OPTIONS --safe #-}

open import Level hiding (suc)
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Nat as ℕ hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Nat.Logarithm
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality.Core

open import NatLearning
open import Learner-Correctness ℕ F NatLearning-Semantics

open import Utils

module NatExamples.SimpleLogLearner where

-- A learner that guesses a secret k within 2 + 2 * log(k) steps.

bound : ℕ → ℕ
bound sec =  + ⌊log₂ sec ⌋ + ⌊log₂ sec ⌋

data SimpleLogLearner : Set where
  [_,∞] : (n : ℕ) → SimpleLogLearner
  [_,_] : (n : ℕ) → (m : ℕ)  → SimpleLogLearner

-- instead of commenting on the semantics of above constructors,
-- we directly *define* the semantics:
_⊧_ : SimpleLogLearner → ℕ → Set
-- Case 1: the secret is greater or equal than 0 (we know nothing)
_⊧_ [ n ,∞] secret = n ≤ secret
_⊧_ [ n , m ] secret = n ≤ secret × secret ≤ m

-- -- Initially, we only know that the secret is ≥ 0
q₀ : SimpleLogLearner
q₀ = [  ,∞]

mid : ℕ → ℕ → ℕ
mid n m = ⌊ n + m /2⌋

δ : SimpleLogLearner → F ℕ SimpleLogLearner 
δ [ n ,∞] = guess ( +  * n) ( +  * n) (λ
  { too-low → [ ( * (suc n)) ,∞]
  ; too-high → [ n , ( * n) ]
  })
δ [ n , m ] = guess (mid n m) (mid n m) λ
  { too-low → [ suc (mid n m) , m ]
  ; too-high → [ n , pred (mid n m) ]
  }


simple-bisect : Learner 0ℓ
simple-bisect = record
  { C = SimpleLogLearner
  ; R = ℕ -- the game results in natural numbers
  ; q₀ = q₀
  ; learner-on = record { δ = δ }
  }