import Wayland.Display
import Wayland.Protocols.RiverInputManagementV1.Header

namespace Wayland.Protocols

inductive RiverInputManagerV1.Event where
  | finished
  | inputDevice
    (id : RiverInputDeviceV1)

inductive RiverInputDeviceV1.Event where
  | removed
  | type
    (type : RiverInputDeviceV1.Type)
  | name
    (name : String)


instance instInterfaceRiverInputManagerV1 : Interface RiverInputManagerV1.name where
  event := RiverInputManagerV1.Event
  version := 1
  requests := #[
    {
      name := "stop"
      args := #[]
      since := 1
      isDestructor := false
    },
    {
      name := "destroy"
      args := #[]
      since := 1
      isDestructor := true
    },
    {
      name := "create_seat"
      args := #[.string .notNull]
      since := 1
      isDestructor := false
    },
    {
      name := "destroy_seat"
      args := #[.string .notNull]
      since := 1
      isDestructor := false
    },
  ]
  events := #[
    {
      name := "finished"
      args := #[]
      since := 1
      isDestructor := false
    },
    {
      name := "input_device"
      args := #[.newID (.some "river_input_device_v1")]
      since := 1
      isDestructor := false
    },
  ]
  demarshalEvent
    | 0 => do
      return .finished
    | 1 => do
      return .inputDevice
        (← Marshallable.demarshal .object)
    | _ => throw s!"Received invalid opcode"

instance instInterfaceRiverInputDeviceV1 : Interface RiverInputDeviceV1.name where
  event := RiverInputDeviceV1.Event
  version := 1
  requests := #[
    {
      name := "destroy"
      args := #[]
      since := 1
      isDestructor := true
    },
    {
      name := "assign_to_seat"
      args := #[.string .notNull]
      since := 1
      isDestructor := false
    },
    {
      name := "set_repeat_info"
      args := #[.int, .int]
      since := 1
      isDestructor := false
    },
    {
      name := "set_scroll_factor"
      args := #[.fixed]
      since := 1
      isDestructor := false
    },
    {
      name := "map_to_output"
      args := #[.object .nullable (.some "wl_output")]
      since := 1
      isDestructor := false
    },
    {
      name := "map_to_rectangle"
      args := #[.int, .int, .int, .int]
      since := 1
      isDestructor := false
    },
  ]
  events := #[
    {
      name := "removed"
      args := #[]
      since := 1
      isDestructor := false
    },
    {
      name := "type"
      args := #[.uint]
      since := 1
      isDestructor := false
    },
    {
      name := "name"
      args := #[.string .notNull]
      since := 1
      isDestructor := false
    },
  ]
  demarshalEvent
    | 0 => do
      return .removed
    | 1 => do
      return .type
        (← Marshallable.demarshal .uint)
    | 2 => do
      return .name
        (← Marshallable.demarshal .string)
    | _ => throw s!"Received invalid opcode"

end Wayland.Protocols