import Wayland
import Std.Data.HashMap

open Wayland Protocols

namespace Waylean

set_option linter.unusedVariables false
def Global (ι : InterfaceName) : Type := UInt32
  deriving BEq
set_option linter.unusedVariables true

variable {ι : InterfaceName} [ResolvedInterface ι]

namespace Registry

private structure GlobalInfo where
  ι : InterfaceName
  name : Global ι
  version : UInt32

structure State where
  private globals : Array GlobalInfo := #[]
  private registry : Option WlRegistry := .none

def State.new : State := {}

/-- Initialize the registry and start observing globals. -/
def init : DisplayM State Unit := do
  let registry ← DisplayM.getRegistry
  set ({ registry } : State)
  registry.listen fun
  | .global name iface version => do
    let s ← get
    set { s with
      globals := s.globals ++ #[
        ({ ι := iface, name, version } : GlobalInfo)
      ]
    }
  | .globalRemove name => do
    let s ← get
    set { s with
      globals := s.globals.filter fun info ↦
        info.name != name
    }

/-- Get a list of globals for a certain interface type. -/
def getGlobals : DisplayM State (Array (Global ι)) := do
  let minVersion := (inferInstance : Interface ι).version
  let globals := (← get).globals
  return globals.filterMap fun g ↦
    if g.ι == ι && g.version >= minVersion
    then .some g.name
    else .none

/-- Get a singleton instance for a global of a certain interface type. -/
def getSingleton? : DisplayM State (Option (Global ι)) := do
  match (← getGlobals) with
    | #[g] => pure (.some g)
    | _    => pure .none

/-- Require a singleton instance for a global of a certain interface type. -/
def requireSingleton : DisplayM State (Global ι) := do
  match (← getSingleton?) with
    | .some g => pure g
    | .none   => throw (.userError s!"No singleton instance for interface {ι}")

end Registry

/-- Bind a global instance. -/
def Global.bind (global : Global ι) : DisplayM Registry.State (Object ι) := do
  let registry ← (← get).registry
    |>.map pure
    |>.getD (throw (.userError "Registry not initialized"))
  registry.bind global

def Registry.bindSingleton : DisplayM Registry.State (Object ι) := do
  (← requireSingleton).bind

end Waylean