summaryrefslogtreecommitdiff
path: root/lib/Wayland/Protocols/RiverXkbConfigV1
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Wayland/Protocols/RiverXkbConfigV1')
-rw-r--r--lib/Wayland/Protocols/RiverXkbConfigV1/Header.lean92
-rw-r--r--lib/Wayland/Protocols/RiverXkbConfigV1/Interface.lean225
-rw-r--r--lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean92
-rw-r--r--lib/Wayland/Protocols/RiverXkbConfigV1/Resolved.lean31
4 files changed, 440 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1/Header.lean b/lib/Wayland/Protocols/RiverXkbConfigV1/Header.lean
new file mode 100644
index 0000000..b63f35f
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverXkbConfigV1/Header.lean
@@ -0,0 +1,92 @@
+import Wayland.Display
+
+namespace Wayland.Protocols
+
+abbrev RiverXkbConfigV1.name : InterfaceName := "river_xkb_config_v1"
+abbrev RiverXkbKeymapV1.name : InterfaceName := "river_xkb_keymap_v1"
+abbrev RiverXkbKeyboardV1.name : InterfaceName := "river_xkb_keyboard_v1"
+
+abbrev RiverXkbConfigV1 : Type := Object RiverXkbConfigV1.name
+abbrev RiverXkbKeymapV1 : Type := Object RiverXkbKeymapV1.name
+abbrev RiverXkbKeyboardV1 : Type := Object RiverXkbKeyboardV1.name
+
+inductive RiverXkbConfigV1.Error where
+ | invalidDestroy
+ | invalidFormat
+
+inductive RiverXkbConfigV1.KeymapFormat where
+ | textV1
+ | textV2
+
+inductive RiverXkbKeyboardV1.Error where
+ | invalidKeymap
+
+namespace RiverXkbConfigV1.Error
+
+instance : Marshallable RiverXkbConfigV1.Error where
+ marshal
+ | .int, .invalidDestroy => ArgumentMarshaller.marshalInt 0
+ | .uint, .invalidDestroy => ArgumentMarshaller.marshalUInt 0
+ | .int, .invalidFormat => ArgumentMarshaller.marshalInt 1
+ | .uint, .invalidFormat => ArgumentMarshaller.marshalUInt 1
+ | _, _ => throw "Marshalling unexpected type, expected int or uint."
+ demarshal
+ | .int => do
+ match (← ArgumentDemarshaller.demarshalInt) with
+ | 0 => pure .invalidDestroy
+ | 1 => pure .invalidFormat
+ | _ => throw "Invalid enum value."
+ | .uint => do
+ match (← ArgumentDemarshaller.demarshalUInt) with
+ | 0 => pure .invalidDestroy
+ | 1 => pure .invalidFormat
+ | _ => throw "Invalid enum value."
+ | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverXkbConfigV1.Error
+
+namespace RiverXkbConfigV1.KeymapFormat
+
+instance : Marshallable RiverXkbConfigV1.KeymapFormat where
+ marshal
+ | .int, .textV1 => ArgumentMarshaller.marshalInt 1
+ | .uint, .textV1 => ArgumentMarshaller.marshalUInt 1
+ | .int, .textV2 => ArgumentMarshaller.marshalInt 2
+ | .uint, .textV2 => ArgumentMarshaller.marshalUInt 2
+ | _, _ => throw "Marshalling unexpected type, expected int or uint."
+ demarshal
+ | .int => do
+ match (← ArgumentDemarshaller.demarshalInt) with
+ | 1 => pure .textV1
+ | 2 => pure .textV2
+ | _ => throw "Invalid enum value."
+ | .uint => do
+ match (← ArgumentDemarshaller.demarshalUInt) with
+ | 1 => pure .textV1
+ | 2 => pure .textV2
+ | _ => throw "Invalid enum value."
+ | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverXkbConfigV1.KeymapFormat
+
+namespace RiverXkbKeyboardV1.Error
+
+instance : Marshallable RiverXkbKeyboardV1.Error where
+ marshal
+ | .int, .invalidKeymap => ArgumentMarshaller.marshalInt 0
+ | .uint, .invalidKeymap => ArgumentMarshaller.marshalUInt 0
+ | _, _ => throw "Marshalling unexpected type, expected int or uint."
+ demarshal
+ | .int => do
+ match (← ArgumentDemarshaller.demarshalInt) with
+ | 0 => pure .invalidKeymap
+ | _ => throw "Invalid enum value."
+ | .uint => do
+ match (← ArgumentDemarshaller.demarshalUInt) with
+ | 0 => pure .invalidKeymap
+ | _ => throw "Invalid enum value."
+ | _ => throw "Demarshalling unexpected type, expected int or uint."
+
+end RiverXkbKeyboardV1.Error
+
+end Wayland.Protocols \ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1/Interface.lean b/lib/Wayland/Protocols/RiverXkbConfigV1/Interface.lean
new file mode 100644
index 0000000..f14c075
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverXkbConfigV1/Interface.lean
@@ -0,0 +1,225 @@
+import Wayland.Display
+import Wayland.Protocols.RiverInputManagementV1.Header
+import Wayland.Protocols.RiverXkbConfigV1.Header
+
+namespace Wayland.Protocols
+
+inductive RiverXkbConfigV1.Event where
+ | finished
+ | xkbKeyboard
+ (id : RiverXkbKeyboardV1)
+
+inductive RiverXkbKeymapV1.Event where
+ | success
+ | failure
+ (errorMsg : String)
+
+inductive RiverXkbKeyboardV1.Event where
+ | removed
+ | inputDevice
+ (device : RiverInputDeviceV1)
+ | layout
+ (index : UInt32)
+ (name : Option String)
+ | capslockEnabled
+ | capslockDisabled
+ | numlockEnabled
+ | numlockDisabled
+
+
+instance instInterfaceRiverXkbConfigV1 : Interface RiverXkbConfigV1.name where
+ event := RiverXkbConfigV1.Event
+ version := 1
+ requests := #[
+ {
+ name := "stop"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "destroy"
+ args := #[]
+ since := 1
+ isDestructor := true
+ },
+ {
+ name := "create_keymap"
+ args := #[.newID (.some "river_xkb_keymap_v1"), .fd, .uint]
+ since := 1
+ isDestructor := false
+ },
+ ]
+ events := #[
+ {
+ name := "finished"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "xkb_keyboard"
+ args := #[.newID (.some "river_xkb_keyboard_v1")]
+ since := 1
+ isDestructor := false
+ },
+ ]
+ demarshalEvent
+ | 0 => do
+ return .finished
+ | 1 => do
+ return .xkbKeyboard
+ (← Marshallable.demarshal .object)
+ | _ => throw s!"Received invalid opcode"
+
+instance instInterfaceRiverXkbKeymapV1 : Interface RiverXkbKeymapV1.name where
+ event := RiverXkbKeymapV1.Event
+ version := 1
+ requests := #[
+ {
+ name := "destroy"
+ args := #[]
+ since := 1
+ isDestructor := true
+ },
+ ]
+ events := #[
+ {
+ name := "success"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "failure"
+ args := #[.string .notNull]
+ since := 1
+ isDestructor := false
+ },
+ ]
+ demarshalEvent
+ | 0 => do
+ return .success
+ | 1 => do
+ return .failure
+ (← Marshallable.demarshal .string)
+ | _ => throw s!"Received invalid opcode"
+
+instance instInterfaceRiverXkbKeyboardV1 : Interface RiverXkbKeyboardV1.name where
+ event := RiverXkbKeyboardV1.Event
+ version := 1
+ requests := #[
+ {
+ name := "destroy"
+ args := #[]
+ since := 1
+ isDestructor := true
+ },
+ {
+ name := "set_keymap"
+ args := #[.object .notNull (.some "river_xkb_keymap_v1")]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "set_layout_by_index"
+ args := #[.int]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "set_layout_by_name"
+ args := #[.string .notNull]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "capslock_enable"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "capslock_disable"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "numlock_enable"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "numlock_disable"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ ]
+ events := #[
+ {
+ name := "removed"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "input_device"
+ args := #[.object .notNull (.some "river_input_device_v1")]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "layout"
+ args := #[.uint, .string .nullable]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "capslock_enabled"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "capslock_disabled"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "numlock_enabled"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ {
+ name := "numlock_disabled"
+ args := #[]
+ since := 1
+ isDestructor := false
+ },
+ ]
+ demarshalEvent
+ | 0 => do
+ return .removed
+ | 1 => do
+ return .inputDevice
+ (← Marshallable.demarshal .object)
+ | 2 => do
+ return .layout
+ (← Marshallable.demarshal .uint)
+ (← Marshallable.demarshal .string)
+ | 3 => do
+ return .capslockEnabled
+ | 4 => do
+ return .capslockDisabled
+ | 5 => do
+ return .numlockEnabled
+ | 6 => do
+ return .numlockDisabled
+ | _ => throw s!"Received invalid opcode"
+
+end Wayland.Protocols \ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean b/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean
new file mode 100644
index 0000000..7cae24d
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverXkbConfigV1/Requests.lean
@@ -0,0 +1,92 @@
+import Wayland.Display
+import Wayland.Protocols.RiverXkbConfigV1.Header
+import Wayland.Protocols.RiverXkbConfigV1.Resolved
+
+namespace Wayland.Protocols
+
+variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
+
+def RiverXkbConfigV1.stop
+ (ω : RiverXkbConfigV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 0
+
+def RiverXkbConfigV1.destroy
+ (ω : RiverXkbConfigV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 1
+
+def RiverXkbConfigV1.createKeymap
+ (ω : RiverXkbConfigV1)
+ (fd : Fd)
+ (format : RiverXkbConfigV1.KeymapFormat)
+ : DisplayM σ RiverXkbKeymapV1 :=
+ ω.sendConstructor do
+ ArgumentMarshaller.marshalAnyObject .none
+ Marshallable.marshal .fd fd
+ Marshallable.marshal .uint format
+ return 2
+
+def RiverXkbKeymapV1.destroy
+ (ω : RiverXkbKeymapV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 0
+
+def RiverXkbKeyboardV1.destroy
+ (ω : RiverXkbKeyboardV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 0
+
+def RiverXkbKeyboardV1.setKeymap
+ (ω : RiverXkbKeyboardV1)
+ (keymap : RiverXkbKeymapV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ Marshallable.marshal .object keymap
+ return 1
+
+def RiverXkbKeyboardV1.setLayoutByIndex
+ (ω : RiverXkbKeyboardV1)
+ (index : Int32)
+ : DisplayM σ Unit :=
+ ω.send do
+ Marshallable.marshal .int index
+ return 2
+
+def RiverXkbKeyboardV1.setLayoutByName
+ (ω : RiverXkbKeyboardV1)
+ (name : String)
+ : DisplayM σ Unit :=
+ ω.send do
+ Marshallable.marshal .string name
+ return 3
+
+def RiverXkbKeyboardV1.capslockEnable
+ (ω : RiverXkbKeyboardV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 4
+
+def RiverXkbKeyboardV1.capslockDisable
+ (ω : RiverXkbKeyboardV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 5
+
+def RiverXkbKeyboardV1.numlockEnable
+ (ω : RiverXkbKeyboardV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 6
+
+def RiverXkbKeyboardV1.numlockDisable
+ (ω : RiverXkbKeyboardV1)
+ : DisplayM σ Unit :=
+ ω.send do
+ return 7
+
+end Wayland.Protocols \ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1/Resolved.lean b/lib/Wayland/Protocols/RiverXkbConfigV1/Resolved.lean
new file mode 100644
index 0000000..a7bcc7e
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverXkbConfigV1/Resolved.lean
@@ -0,0 +1,31 @@
+import Wayland.Display
+import Wayland.Protocols.RiverInputManagementV1.Interface
+import Wayland.Protocols.RiverXkbConfigV1.Interface
+import Wayland.Protocols.Wayland.Interface
+
+namespace Wayland.Protocols
+
+instance instResolvedInterfaceRiverXkbConfigV1 : ResolvedInterface RiverXkbConfigV1.name where
+ referencedInterfaces := #[
+ ⟨RiverInputDeviceV1.name, inferInstance⟩,
+ ⟨RiverXkbConfigV1.name, inferInstance⟩,
+ ⟨RiverXkbKeyboardV1.name, inferInstance⟩,
+ ⟨RiverXkbKeymapV1.name, inferInstance⟩,
+ ⟨WlOutput.name, inferInstance⟩,
+ ]
+
+instance instResolvedInterfaceRiverXkbKeymapV1 : ResolvedInterface RiverXkbKeymapV1.name where
+ referencedInterfaces := #[
+ ⟨RiverXkbKeymapV1.name, inferInstance⟩,
+ ]
+
+instance instResolvedInterfaceRiverXkbKeyboardV1 : ResolvedInterface RiverXkbKeyboardV1.name where
+ referencedInterfaces := #[
+ ⟨RiverInputDeviceV1.name, inferInstance⟩,
+ ⟨RiverXkbKeyboardV1.name, inferInstance⟩,
+ ⟨RiverXkbKeymapV1.name, inferInstance⟩,
+ ⟨WlOutput.name, inferInstance⟩,
+ ]
+
+
+end Wayland.Protocols \ No newline at end of file
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 15:11:40 +0000