fix build on linux

4 files changed, 359 insertions, 0 deletions

diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean
new file mode 100644
index 0000000..66e881f
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean
@@ -0,0 +1,105 @@
+import Wayland.Display
+
+namespace Wayland.Protocols
+
+abbrev RiverInputManagerV1.name : InterfaceName := "river_input_manager_v1"
+abbrev RiverInputDeviceV1.name : InterfaceName := "river_input_device_v1"
+
+abbrev RiverInputManagerV1 : Type := Object RiverInputManagerV1.name
+abbrev RiverInputDeviceV1 : Type := Object RiverInputDeviceV1.name
+
+inductive RiverInputManagerV1.Error where
+  | invalidDestroy
+
+inductive RiverInputDeviceV1.Error where
+  | invalidRepeatInfo
+  | invalidScrollFactor
+  | invalidMapToRectangle
+
+inductive RiverInputDeviceV1.Type where
+  | keyboard
+  | pointer
+  | touch
+  | tablet
+
+namespace RiverInputManagerV1.Error
+
+instance : Marshallable RiverInputManagerV1.Error where
+  marshal
+    | .int,  .invalidDestroy => ArgumentMarshaller.marshalInt 0
+    | .uint, .invalidDestroy => ArgumentMarshaller.marshalUInt 0
+    | _, _ => throw "Marshalling unexpected type, expected int or uint."
+  demarshal
+    | .int => do
+      match (← ArgumentDemarshaller.demarshalInt) with
+        | 0 => pure .invalidDestroy
+        | _ => throw "Invalid enum value."
+    | .uint => do
+      match (← ArgumentDemarshaller.demarshalUInt) with
+        | 0 => pure .invalidDestroy
+        | _ => throw "Invalid enum value."
+    | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverInputManagerV1.Error
+
+namespace RiverInputDeviceV1.Error
+
+instance : Marshallable RiverInputDeviceV1.Error where
+  marshal
+    | .int,  .invalidRepeatInfo => ArgumentMarshaller.marshalInt 0
+    | .uint, .invalidRepeatInfo => ArgumentMarshaller.marshalUInt 0
+    | .int,  .invalidScrollFactor => ArgumentMarshaller.marshalInt 1
+    | .uint, .invalidScrollFactor => ArgumentMarshaller.marshalUInt 1
+    | .int,  .invalidMapToRectangle => ArgumentMarshaller.marshalInt 2
+    | .uint, .invalidMapToRectangle => ArgumentMarshaller.marshalUInt 2
+    | _, _ => throw "Marshalling unexpected type, expected int or uint."
+  demarshal
+    | .int => do
+      match (← ArgumentDemarshaller.demarshalInt) with
+        | 0 => pure .invalidRepeatInfo
+        | 1 => pure .invalidScrollFactor
+        | 2 => pure .invalidMapToRectangle
+        | _ => throw "Invalid enum value."
+    | .uint => do
+      match (← ArgumentDemarshaller.demarshalUInt) with
+        | 0 => pure .invalidRepeatInfo
+        | 1 => pure .invalidScrollFactor
+        | 2 => pure .invalidMapToRectangle
+        | _ => throw "Invalid enum value."
+    | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverInputDeviceV1.Error
+
+namespace RiverInputDeviceV1.Type
+
+instance : Marshallable RiverInputDeviceV1.Type where
+  marshal
+    | .int,  .keyboard => ArgumentMarshaller.marshalInt 0
+    | .uint, .keyboard => ArgumentMarshaller.marshalUInt 0
+    | .int,  .pointer => ArgumentMarshaller.marshalInt 1
+    | .uint, .pointer => ArgumentMarshaller.marshalUInt 1
+    | .int,  .touch => ArgumentMarshaller.marshalInt 2
+    | .uint, .touch => ArgumentMarshaller.marshalUInt 2
+    | .int,  .tablet => ArgumentMarshaller.marshalInt 3
+    | .uint, .tablet => ArgumentMarshaller.marshalUInt 3
+    | _, _ => throw "Marshalling unexpected type, expected int or uint."
+  demarshal
+    | .int => do
+      match (← ArgumentDemarshaller.demarshalInt) with
+        | 0 => pure .keyboard
+        | 1 => pure .pointer
+        | 2 => pure .touch
+        | 3 => pure .tablet
+        | _ => throw "Invalid enum value."
+    | .uint => do
+      match (← ArgumentDemarshaller.demarshalUInt) with
+        | 0 => pure .keyboard
+        | 1 => pure .pointer
+        | 2 => pure .touch
+        | 3 => pure .tablet
+        | _ => throw "Invalid enum value."
+    | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverInputDeviceV1.Type
+
+end Wayland.Protocols
\ No newline at end of file
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
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean
new file mode 100644
index 0000000..3c9c44e
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean
@@ -0,0 +1,91 @@
+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 do
+    return 0
+
+def RiverInputManagerV1.destroy
+    (ω : RiverInputManagerV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 1
+
+def RiverInputManagerV1.createSeat
+    (ω : RiverInputManagerV1)
+    (name : String)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .string name
+    return 2
+
+def RiverInputManagerV1.destroySeat
+    (ω : RiverInputManagerV1)
+    (name : String)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .string name
+    return 3
+
+def RiverInputDeviceV1.destroy
+    (ω : RiverInputDeviceV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 0
+
+def RiverInputDeviceV1.assignToSeat
+    (ω : RiverInputDeviceV1)
+    (name : String)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .string name
+    return 1
+
+def RiverInputDeviceV1.setRepeatInfo
+    (ω : RiverInputDeviceV1)
+    (rate : Int32)
+    (delay : Int32)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .int rate
+    Marshallable.marshal .int delay
+    return 2
+
+def RiverInputDeviceV1.setScrollFactor
+    (ω : RiverInputDeviceV1)
+    (factor : Float32)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .fixed factor
+    return 3
+
+def RiverInputDeviceV1.mapToOutput
+    (ω : RiverInputDeviceV1)
+    (output : Option WlOutput)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .object output
+    return 4
+
+def RiverInputDeviceV1.mapToRectangle
+    (ω : RiverInputDeviceV1)
+    (x : Int32)
+    (y : Int32)
+    (width : Int32)
+    (height : Int32)
+    : DisplayM σ Unit :=
+  ω.send do
+    Marshallable.marshal .int x
+    Marshallable.marshal .int y
+    Marshallable.marshal .int width
+    Marshallable.marshal .int height
+    return 5
+
+end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Resolved.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Resolved.lean
new file mode 100644
index 0000000..558dee2
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverInputManagementV1/Resolved.lean
@@ -0,0 +1,21 @@
+import Wayland.Display
+import Wayland.Protocols.RiverInputManagementV1.Interface
+import Wayland.Protocols.Wayland.Interface
+
+namespace Wayland.Protocols
+
+instance instResolvedInterfaceRiverInputManagerV1 : ResolvedInterface RiverInputManagerV1.name where
+  referencedInterfaces := #[
+    ⟨RiverInputDeviceV1.name, inferInstance⟩,
+    ⟨RiverInputManagerV1.name, inferInstance⟩,
+    ⟨WlOutput.name, inferInstance⟩,
+  ]
+
+instance instResolvedInterfaceRiverInputDeviceV1 : ResolvedInterface RiverInputDeviceV1.name where
+  referencedInterfaces := #[
+    ⟨RiverInputDeviceV1.name, inferInstance⟩,
+    ⟨WlOutput.name, inferInstance⟩,
+  ]
+
+
+end Wayland.Protocols
\ No newline at end of file