1 files changed, 142 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean
new file mode 100644
index 0000000..7b72050
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean
@@ -0,0 +1,142 @@
+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
+\ No newline at end of file