import Wayland
open Wayland


def WLDisplay.name : InterfaceName := "wl_display"
abbrev WLDisplay : Type := Object WLDisplay.name

inductive WLDisplay.Request where
  | sync : Request

inductive WLDisplay.Event where
  | error : Event
  | other : Event

instance : Request WLDisplay.Request where
  messages := #[{ name := "sync", args := #[], since := 0, isDestructor := False }]
  signature _ := sorry
  marshal _ := do return 0
instance : Event WLDisplay.Event where
  messages := #[{ name := "error", args := #[.string .notNull], since := 0, isDestructor := False },
                { name := "other", args := #[.object .nullable WLDisplay.name], since := 99, isDestructor := False}]
  signature _ := sorry
  demarshal _ := do return .error
instance : Interface WLDisplay.name where
  request := WLDisplay.Request
  event := WLDisplay.Event
  version := 1
instance : ResolvedInterface WLDisplay.name where
  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩]



structure State where
  count : Int

partial def nextTimer : DisplayM Int Unit := do
  _ ← DisplayM.registerTimer 16ms do
    let newCount := (← get) + 1
    set newCount
    DisplayM.liftIO (IO.println s!"Timer tick {newCount}")
    nextTimer

def launch : DisplayM State Unit := do
  _ ← DisplayM.registerSignal .SIGINT do
    DisplayM.liftIO (IO.println "Received SIGINT")
    DisplayM.requestQuit
  DisplayM.zoom (mk_lens count) nextTimer

def main : IO Unit :=
  DisplayM.run launch { count := 0 }