import Wayland
open Wayland


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

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

inductive WLDisplay.Request where
  | sync : (callback : WLCallback) → Request

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

def WLDisplay.Request.sync.signature : MessageDesc :=
  { name := "sync"
    args := #[.newID WLCallback.name]
    since := 0
    isDestructor := False }

instance : Request WLDisplay.Request where
  messages := #[WLDisplay.Request.sync.signature]
  signature
    | .sync _ => WLDisplay.Request.sync.signature
  marshal
    | .sync callback => do
      ArgumentMarshaller.marshalNewID callback
      return 0

def WLDisplay.Event.error.signature : MessageDesc :=
  { name := "error"
    args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
    since := 0
    isDestructor := False }

instance : Event WLDisplay.Event where
  messages := #[WLDisplay.Event.error.signature]
  signature
    | .error _ _ => WLDisplay.Event.error.signature
  demarshal opcode := match opcode with
    | 0 => do
      (_ : Option (Object WLDisplay.name)) ← ArgumentDemarshaller.demarshalObject
      return .error
        (← ArgumentDemarshaller.demarshalUInt)
        ((← ArgumentDemarshaller.demarshalString).getD "")
    | _ => sorry

instance : Interface WLDisplay.name where
  request := WLDisplay.Request
  event := WLDisplay.Event
  version := 1

inductive WLCallback.Request where

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

def WLCallback.Event.done.signature : MessageDesc :=
  { name := "done"
    args := #[.uint]
    since := 0
    isDestructor := False }

instance : Request WLCallback.Request where
  messages := #[]
  signature req := by cases req
  marshal req := by cases req

instance : Event WLCallback.Event where
  messages := #[WLCallback.Event.done.signature]
  signature
    | .done _ => WLCallback.Event.done.signature
  demarshal opcode := match opcode with
    | 0 => do
      return .done
        (← ArgumentDemarshaller.demarshalUInt)
    | _ => sorry

instance : Interface WLCallback.name where
  request := WLCallback.Request
  event := WLCallback.Event
  version := 1

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

instance : ResolvedInterface WLCallback.name where
  referencedInterfaces := #[⟨WLCallback.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

  let disp : WLDisplay ← DisplayM.getDisplay
  let callback : WLCallback ← DisplayM.createObject disp
  callback.listen fun ev ↦ match ev with
    | .done _ => DisplayM.liftIO (IO.println "Roundtrip complete")
  disp.send (.sync callback)
  DisplayM.liftIO (IO.println "Test 5")

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