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

namespace Wayland.Protocols

variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]

def RiverInputManagerV1.stop
    (ω : RiverInputManagerV1)
    : DisplayM σ Unit :=
  ω.send false do
    return 0

def RiverInputManagerV1.destroy
    (ω : RiverInputManagerV1)
    : DisplayM σ Unit :=
  ω.send true do
    return 1

def RiverInputManagerV1.createSeat
    (ω : RiverInputManagerV1)
    (name : String)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .string name
    return 2

def RiverInputManagerV1.destroySeat
    (ω : RiverInputManagerV1)
    (name : String)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .string name
    return 3

def RiverInputDeviceV1.destroy
    (ω : RiverInputDeviceV1)
    : DisplayM σ Unit :=
  ω.send true do
    return 0

def RiverInputDeviceV1.assignToSeat
    (ω : RiverInputDeviceV1)
    (name : String)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .string name
    return 1

def RiverInputDeviceV1.setRepeatInfo
    (ω : RiverInputDeviceV1)
    (rate : Int32)
    (delay : Int32)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .int rate
    Marshallable.marshal .int delay
    return 2

def RiverInputDeviceV1.setScrollFactor
    (ω : RiverInputDeviceV1)
    (factor : Float32)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .fixed factor
    return 3

def RiverInputDeviceV1.mapToOutput
    (ω : RiverInputDeviceV1)
    (output : Option WlOutput)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .object output
    return 4

def RiverInputDeviceV1.mapToRectangle
    (ω : RiverInputDeviceV1)
    (x : Int32)
    (y : Int32)
    (width : Int32)
    (height : Int32)
    : DisplayM σ Unit :=
  ω.send false do
    Marshallable.marshal .int x
    Marshallable.marshal .int y
    Marshallable.marshal .int width
    Marshallable.marshal .int height
    return 5

end Wayland.Protocols