import Wayland
open Wayland


def WLCallback.name : InterfaceName := "wl_callback"
def WLDisplay.name : InterfaceName := "wl_display"

def WLDisplay : Type := Object WLDisplay.name
def WLCallback : Type := Object WLCallback.name

inductive WLDisplay.Event where
  | error : (code : UInt32) → (message : String) → Event

instance : Interface WLDisplay.name where
  event := WLDisplay.Event
  requests :=
    #[ { name := "sync"
         args := #[.newID WLCallback.name]
         since := 0
         isDestructor := False } ]
  events :=
    #[ { name := "error"
         args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
         since := 0
         isDestructor := False } ]
  demarshalEvent
    | 0 => do
      (_ : Option (Object WLDisplay.name)) ← ArgumentDemarshaller.demarshalObject
      return .error
        (← ArgumentDemarshaller.demarshalUInt)
        ((← ArgumentDemarshaller.demarshalString).getD "")
    | _ => sorry
  version := 1

inductive WLCallback.Event where
  | done : (data : UInt32) → Event

instance : Interface WLCallback.name where
  event := WLCallback.Event
  requests :=
    #[]
  events :=
    #[ { name := "done"
         args := #[.uint]
         since := 0
         isDestructor := False } ]
  demarshalEvent
    | 0 => do
      return .done
        (← ArgumentDemarshaller.demarshalUInt)
    | _ => sorry
  version := 1

instance : ResolvedInterface WLDisplay.name where
  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩, ⟨WLCallback.name, inferInstance⟩]

instance : ResolvedInterface WLCallback.name where
  referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]

def WLDisplay.sync {σ : Type} (display : WLDisplay) : DisplayM σ WLCallback :=
  display.sendConstructor do
    return 0

structure State where
  count : Int
  callback : Option WLCallback

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

  let disp : WLDisplay ← DisplayM.getDisplay
  let callback : WLCallback ← disp.sync
  callback.listen fun ev ↦ match ev with
    | .done _ => DisplayM.liftIO (IO.println "Roundtrip complete")
  set { (← get) with callback := callback }

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