diff options
38 files changed, 8780 insertions, 32 deletions
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc index 3487f72..a8a80e3 100644 --- a/lib/CWayland/CWayland.cc +++ b/lib/CWayland/CWayland.cc @@ -5,8 +5,11 @@ #include <queue> #include <memory> #include <unordered_map> +#include <string_view> #include <chrono> +#include <algorithm> #include <cassert> +#include <cerrno> #include <poll.h> #include <fcntl.h> #include <unistd.h> @@ -239,7 +242,7 @@ namespace static void signal_handler(int signum) { - write(tx_fd, &signum, sizeof(signum)); + (void)write(tx_fd, &signum, sizeof(signum)); } public: @@ -845,8 +848,8 @@ namespace enum class type { uninitialized, i32, u32, fixed, string, object, array, fd }; struct meta { - type type{ type::uninitialized }; - ref ref{}; + type t{ type::uninitialized }; + ref r{}; }; static constexpr std::size_t max_args = 64; @@ -866,7 +869,7 @@ namespace { assert(reader_idx < writer_idx && "reached maximum number of arguments"); auto result = reader_idx++; - assert(meta[result].type == expected_type && "mismatching argument type"); + assert(meta[result].t == expected_type && "mismatching argument type"); return result; } @@ -878,29 +881,29 @@ namespace { auto i = next_write(); args[i].i = value; - meta[i].type = type::i32; + meta[i].t = type::i32; } void write_uint(uint32_t value) { auto i = next_write(); args[i].u = value; - meta[i].type = type::u32; + meta[i].t = type::u32; } void write_fixed(float value) { auto i = next_write(); args[i].f = wl_fixed_from_double(value); - meta[i].type = type::fixed; + meta[i].t = type::fixed; } void write_string(ref value) { auto i = next_write(); args[i].s = option_cstr_or_null(value.get()); - meta[i].type = type::string; - meta[i].ref = std::move(value); + meta[i].t = type::string; + meta[i].r = std::move(value); } void write_object(ref value) @@ -914,8 +917,8 @@ namespace { args[i].o = static_cast<wl_object*>(lean_get_external_data(lean_ctor_get(value.get(), 0))); } - meta[i].type = type::object; - meta[i].ref = std::move(value); + meta[i].t = type::object; + meta[i].r = std::move(value); } void write_array(ref value) @@ -925,15 +928,15 @@ namespace args[i].a->alloc = size; args[i].a->size = size; args[i].a->data = lean_sarray_cptr(value.get()); - meta[i].type = type::array; - meta[i].ref = std::move(value); + meta[i].t = type::array; + meta[i].r = std::move(value); } void write_fd(int32_t value) { auto i = next_write(); args[i].h = value; - meta[i].type = type::fd; + meta[i].t = type::fd; } void write(wl_argument arg, std::string_view signature_type) @@ -942,57 +945,57 @@ namespace args[i] = arg; if (signature_type == "i") { - meta[i].type = type::i32; + meta[i].t = type::i32; } else if (signature_type == "u") { - meta[i].type = type::u32; + meta[i].t = type::u32; } else if (signature_type == "f") { - meta[i].type = type::fixed; + meta[i].t = type::fixed; } else if (signature_type == "s" || signature_type == "?s") { - meta[i].type = type::string; + meta[i].t = type::string; if (arg.s) { auto s = std::string_view{ arg.s }; auto res = ref::steal(lean_alloc_ctor(1, 1, 0)); lean_ctor_set(res.get(), 0, lean_mk_string_from_bytes(s.data(), s.length())); - meta[i].ref = std::move(res); + meta[i].r = std::move(res); } else { - meta[i].ref = ref::steal(lean_box(0)); + meta[i].r = ref::steal(lean_box(0)); } } else if (signature_type == "o" || signature_type == "?o" || signature_type == "n") { - meta[i].type = type::object; + meta[i].t = type::object; if (arg.o) { auto res = ref::steal(lean_alloc_ctor(1, 1, 0)); auto proxy_obj = (lean_object*)(wl_proxy_get_listener((wl_proxy*)arg.o)); // set as dispatcher_data lean_inc(proxy_obj); lean_ctor_set(res.get(), 0, proxy_obj); - meta[i].ref = std::move(res); + meta[i].r = std::move(res); } else { - meta[i].ref = ref::steal(lean_box(0)); + meta[i].r = ref::steal(lean_box(0)); } } else if (signature_type == "a") { - meta[i].type = type::array; + meta[i].t = type::array; auto res = ref::steal(lean_alloc_sarray(1, arg.a->size, arg.a->size)); std::copy_n(static_cast<uint8_t*>(arg.a->data), arg.a->size, lean_sarray_cptr(res.get())); - meta[i].ref = std::move(res); + meta[i].r = std::move(res); } else if (signature_type == "h") { - meta[i].type = type::fd; + meta[i].t = type::fd; } else { @@ -1021,19 +1024,19 @@ namespace ref read_string() { auto i = next_read(type::string); - return ref{ std::move(meta[i].ref) }; + return ref{ std::move(meta[i].r) }; } ref read_object() { auto i = next_read(type::object); - return ref{ std::move(meta[i].ref) }; + return ref{ std::move(meta[i].r) }; } ref read_array() { auto i = next_read(type::array); - return ref{ std::move(meta[i].ref) }; + return ref{ std::move(meta[i].r) }; } ref read_fd() @@ -1287,4 +1290,4 @@ lean_obj_res waylean_proxy_get_type(b_lean_obj_arg proxy_obj) auto proxy = static_cast<wl_proxy*>(lean_get_external_data(proxy_obj)); auto name = wl_proxy_get_interface(proxy)->name; return lean_io_result_mk_ok(lean_mk_string(name)); -}
\ No newline at end of file +} diff --git a/lib/Wayland/.gitignore b/lib/Wayland/.gitignore deleted file mode 100644 index b39d86d..0000000 --- a/lib/Wayland/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -Protocols.lean -Protocols/**/*.lean
\ No newline at end of file diff --git a/lib/Wayland/Protocols.lean b/lib/Wayland/Protocols.lean index e69de29..0c8bcb8 100644 --- a/lib/Wayland/Protocols.lean +++ b/lib/Wayland/Protocols.lean @@ -0,0 +1,7 @@ +import Wayland.Protocols.RiverInputManagementV1 +import Wayland.Protocols.RiverLayerShellV1 +import Wayland.Protocols.RiverLibinputConfigV1 +import Wayland.Protocols.RiverWindowManagementV1 +import Wayland.Protocols.RiverXkbBindingsV1 +import Wayland.Protocols.RiverXkbConfigV1 +import Wayland.Protocols.Wayland diff --git a/lib/Wayland/Protocols/RiverInputManagementV1.lean b/lib/Wayland/Protocols/RiverInputManagementV1.lean new file mode 100644 index 0000000..8d44800 --- /dev/null +++ b/lib/Wayland/Protocols/RiverInputManagementV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverInputManagementV1.Header +import Wayland.Protocols.RiverInputManagementV1.Interface +import Wayland.Protocols.RiverInputManagementV1.Requests +import Wayland.Protocols.RiverInputManagementV1.Resolved 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 diff --git a/lib/Wayland/Protocols/RiverLayerShellV1.lean b/lib/Wayland/Protocols/RiverLayerShellV1.lean new file mode 100644 index 0000000..cab6bd5 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverLayerShellV1.Header +import Wayland.Protocols.RiverLayerShellV1.Interface +import Wayland.Protocols.RiverLayerShellV1.Requests +import Wayland.Protocols.RiverLayerShellV1.Resolved diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean new file mode 100644 index 0000000..7c01f90 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean @@ -0,0 +1,36 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverLayerShellV1.name : InterfaceName := "river_layer_shell_v1" +abbrev RiverLayerShellOutputV1.name : InterfaceName := "river_layer_shell_output_v1" +abbrev RiverLayerShellSeatV1.name : InterfaceName := "river_layer_shell_seat_v1" + +abbrev RiverLayerShellV1 : Type := Object RiverLayerShellV1.name +abbrev RiverLayerShellOutputV1 : Type := Object RiverLayerShellOutputV1.name +abbrev RiverLayerShellSeatV1 : Type := Object RiverLayerShellSeatV1.name + +inductive RiverLayerShellV1.Error where + | objectAlreadyCreated + +namespace RiverLayerShellV1.Error + +instance : Marshallable RiverLayerShellV1.Error where + marshal + | .int, .objectAlreadyCreated => ArgumentMarshaller.marshalInt 0 + | .uint, .objectAlreadyCreated => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLayerShellV1.Error + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean new file mode 100644 index 0000000..5e0cb2d --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean @@ -0,0 +1,123 @@ +import Wayland.Display +import Wayland.Protocols.RiverLayerShellV1.Header + +namespace Wayland.Protocols + +inductive RiverLayerShellV1.Event where + +inductive RiverLayerShellOutputV1.Event where + | nonExclusiveArea + (x : Int32) + (y : Int32) + (width : Int32) + (height : Int32) + +inductive RiverLayerShellSeatV1.Event where + | focusExclusive + | focusNonExclusive + | focusNone + + +instance instInterfaceRiverLayerShellV1 : Interface RiverLayerShellV1.name where + event := RiverLayerShellV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "get_output" + args := #[.newID (.some "river_layer_shell_output_v1"), .object .notNull (.some "river_output_v1")] + since := 1 + isDestructor := false + }, + { + name := "get_seat" + args := #[.newID (.some "river_layer_shell_seat_v1"), .object .notNull (.some "river_seat_v1")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverLayerShellOutputV1 : Interface RiverLayerShellOutputV1.name where + event := RiverLayerShellOutputV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_default" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "non_exclusive_area" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .nonExclusiveArea + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverLayerShellSeatV1 : Interface RiverLayerShellSeatV1.name where + event := RiverLayerShellSeatV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + ] + events := #[ + { + name := "focus_exclusive" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "focus_non_exclusive" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "focus_none" + args := #[] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .focusExclusive + | 1 => do + return .focusNonExclusive + | 2 => do + return .focusNone + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean new file mode 100644 index 0000000..8e7dc9f --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean @@ -0,0 +1,51 @@ +import Wayland.Display +import Wayland.Protocols.RiverLayerShellV1.Resolved +import Wayland.Protocols.RiverWindowManagementV1.Header + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverLayerShellV1.destroy + (ω : RiverLayerShellV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverLayerShellV1.getOutput + (ω : RiverLayerShellV1) + (output : RiverOutputV1) + : DisplayM σ RiverLayerShellOutputV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object output + return 1 + +def RiverLayerShellV1.getSeat + (ω : RiverLayerShellV1) + (seat : RiverSeatV1) + : DisplayM σ RiverLayerShellSeatV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object seat + return 2 + +def RiverLayerShellOutputV1.destroy + (ω : RiverLayerShellOutputV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverLayerShellOutputV1.setDefault + (ω : RiverLayerShellOutputV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverLayerShellSeatV1.destroy + (ω : RiverLayerShellSeatV1) + : DisplayM σ Unit := + ω.send do + return 0 + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean new file mode 100644 index 0000000..060dc6f --- /dev/null +++ b/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean @@ -0,0 +1,38 @@ +import Wayland.Display +import Wayland.Protocols.RiverLayerShellV1.Interface +import Wayland.Protocols.RiverWindowManagementV1.Interface +import Wayland.Protocols.Wayland.Interface + +namespace Wayland.Protocols + +instance instResolvedInterfaceRiverLayerShellV1 : ResolvedInterface RiverLayerShellV1.name where + referencedInterfaces := #[ + ⟨RiverLayerShellOutputV1.name, inferInstance⟩, + ⟨RiverLayerShellSeatV1.name, inferInstance⟩, + ⟨RiverLayerShellV1.name, inferInstance⟩, + ⟨RiverDecorationV1.name, inferInstance⟩, + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverOutputV1.name, inferInstance⟩, + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ⟨RiverSeatV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ⟨RiverWindowV1.name, inferInstance⟩, + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverLayerShellOutputV1 : ResolvedInterface RiverLayerShellOutputV1.name where + referencedInterfaces := #[ + ⟨RiverLayerShellOutputV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverLayerShellSeatV1 : ResolvedInterface RiverLayerShellSeatV1.name where + referencedInterfaces := #[ + ⟨RiverLayerShellSeatV1.name, inferInstance⟩, + ] + + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1.lean new file mode 100644 index 0000000..778da8d --- /dev/null +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverLibinputConfigV1.Header +import Wayland.Protocols.RiverLibinputConfigV1.Interface +import Wayland.Protocols.RiverLibinputConfigV1.Requests +import Wayland.Protocols.RiverLibinputConfigV1.Resolved diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean new file mode 100644 index 0000000..3f62b69 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Header.lean @@ -0,0 +1,691 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverLibinputConfigV1.name : InterfaceName := "river_libinput_config_v1" +abbrev RiverLibinputDeviceV1.name : InterfaceName := "river_libinput_device_v1" +abbrev RiverLibinputAccelConfigV1.name : InterfaceName := "river_libinput_accel_config_v1" +abbrev RiverLibinputResultV1.name : InterfaceName := "river_libinput_result_v1" + +abbrev RiverLibinputConfigV1 : Type := Object RiverLibinputConfigV1.name +abbrev RiverLibinputDeviceV1 : Type := Object RiverLibinputDeviceV1.name +abbrev RiverLibinputAccelConfigV1 : Type := Object RiverLibinputAccelConfigV1.name +abbrev RiverLibinputResultV1 : Type := Object RiverLibinputResultV1.name + +inductive RiverLibinputConfigV1.Error where + | invalidArg + | invalidDestroy + +inductive RiverLibinputDeviceV1.Error where + | invalidArg + +structure RiverLibinputDeviceV1.SendEventsModes where + enabled : Bool + disabled : Bool + disabledOnExternalMouse : Bool + +inductive RiverLibinputDeviceV1.TapState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.TapButtonMap where + | lrm + | lmr + +inductive RiverLibinputDeviceV1.DragState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.DragLockState where + | disabled + | enabledTimeout + | enabledSticky + +inductive RiverLibinputDeviceV1.ThreeFingerDragState where + | disabled + | enabled3fg + | enabled4fg + +inductive RiverLibinputDeviceV1.AccelProfile where + | none + | flat + | adaptive + | custom + +structure RiverLibinputDeviceV1.AccelProfiles where + none : Bool + flat : Bool + adaptive : Bool + custom : Bool + +inductive RiverLibinputDeviceV1.NaturalScrollState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.LeftHandedState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.ClickMethod where + | none + | buttonAreas + | clickfinger + +structure RiverLibinputDeviceV1.ClickMethods where + none : Bool + buttonAreas : Bool + clickfinger : Bool + +inductive RiverLibinputDeviceV1.ClickfingerButtonMap where + | lrm + | lmr + +inductive RiverLibinputDeviceV1.MiddleEmulationState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.ScrollMethod where + | noScroll + | twoFinger + | edge + | onButtonDown + +structure RiverLibinputDeviceV1.ScrollMethods where + noScroll : Bool + twoFinger : Bool + edge : Bool + onButtonDown : Bool + +inductive RiverLibinputDeviceV1.ScrollButtonLockState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.DwtState where + | disabled + | enabled + +inductive RiverLibinputDeviceV1.DwtpState where + | disabled + | enabled + +inductive RiverLibinputAccelConfigV1.Error where + | invalidArg + +inductive RiverLibinputAccelConfigV1.AccelType where + | fallback + | motion + | scroll + +namespace RiverLibinputConfigV1.Error + +instance : Marshallable RiverLibinputConfigV1.Error where + marshal + | .int, .invalidArg => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidArg => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidDestroy => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidDestroy => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidArg + | 1 => pure .invalidDestroy + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidArg + | 1 => pure .invalidDestroy + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputConfigV1.Error + +namespace RiverLibinputDeviceV1.Error + +instance : Marshallable RiverLibinputDeviceV1.Error where + marshal + | .int, .invalidArg => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidArg => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidArg + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidArg + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.Error + +namespace RiverLibinputDeviceV1.SendEventsModes + +instance : Marshallable RiverLibinputDeviceV1.SendEventsModes where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.enabled then 0 else 0) + ||| (if μ.disabled then 1 else 0) + ||| (if μ.disabledOnExternalMouse then 2 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + enabled := (μ &&& 0) == 0 + disabled := (μ &&& 1) == 1 + disabledOnExternalMouse := (μ &&& 2) == 2 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverLibinputDeviceV1.SendEventsModes + +namespace RiverLibinputDeviceV1.TapState + +instance : Marshallable RiverLibinputDeviceV1.TapState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.TapState + +namespace RiverLibinputDeviceV1.TapButtonMap + +instance : Marshallable RiverLibinputDeviceV1.TapButtonMap where + marshal + | .int, .lrm => ArgumentMarshaller.marshalInt 0 + | .uint, .lrm => ArgumentMarshaller.marshalUInt 0 + | .int, .lmr => ArgumentMarshaller.marshalInt 1 + | .uint, .lmr => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .lrm + | 1 => pure .lmr + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .lrm + | 1 => pure .lmr + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.TapButtonMap + +namespace RiverLibinputDeviceV1.DragState + +instance : Marshallable RiverLibinputDeviceV1.DragState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.DragState + +namespace RiverLibinputDeviceV1.DragLockState + +instance : Marshallable RiverLibinputDeviceV1.DragLockState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabledTimeout => ArgumentMarshaller.marshalInt 1 + | .uint, .enabledTimeout => ArgumentMarshaller.marshalUInt 1 + | .int, .enabledSticky => ArgumentMarshaller.marshalInt 2 + | .uint, .enabledSticky => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabledTimeout + | 2 => pure .enabledSticky + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabledTimeout + | 2 => pure .enabledSticky + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.DragLockState + +namespace RiverLibinputDeviceV1.ThreeFingerDragState + +instance : Marshallable RiverLibinputDeviceV1.ThreeFingerDragState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled3fg => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled3fg => ArgumentMarshaller.marshalUInt 1 + | .int, .enabled4fg => ArgumentMarshaller.marshalInt 2 + | .uint, .enabled4fg => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled3fg + | 2 => pure .enabled4fg + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled3fg + | 2 => pure .enabled4fg + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.ThreeFingerDragState + +namespace RiverLibinputDeviceV1.AccelProfile + +instance : Marshallable RiverLibinputDeviceV1.AccelProfile where + marshal + | .int, .none => ArgumentMarshaller.marshalInt 0 + | .uint, .none => ArgumentMarshaller.marshalUInt 0 + | .int, .flat => ArgumentMarshaller.marshalInt 1 + | .uint, .flat => ArgumentMarshaller.marshalUInt 1 + | .int, .adaptive => ArgumentMarshaller.marshalInt 2 + | .uint, .adaptive => ArgumentMarshaller.marshalUInt 2 + | .int, .custom => ArgumentMarshaller.marshalInt 4 + | .uint, .custom => ArgumentMarshaller.marshalUInt 4 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .none + | 1 => pure .flat + | 2 => pure .adaptive + | 4 => pure .custom + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .none + | 1 => pure .flat + | 2 => pure .adaptive + | 4 => pure .custom + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.AccelProfile + +namespace RiverLibinputDeviceV1.AccelProfiles + +instance : Marshallable RiverLibinputDeviceV1.AccelProfiles where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.flat then 1 else 0) + ||| (if μ.adaptive then 2 else 0) + ||| (if μ.custom then 4 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + flat := (μ &&& 1) == 1 + adaptive := (μ &&& 2) == 2 + custom := (μ &&& 4) == 4 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverLibinputDeviceV1.AccelProfiles + +namespace RiverLibinputDeviceV1.NaturalScrollState + +instance : Marshallable RiverLibinputDeviceV1.NaturalScrollState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.NaturalScrollState + +namespace RiverLibinputDeviceV1.LeftHandedState + +instance : Marshallable RiverLibinputDeviceV1.LeftHandedState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.LeftHandedState + +namespace RiverLibinputDeviceV1.ClickMethod + +instance : Marshallable RiverLibinputDeviceV1.ClickMethod where + marshal + | .int, .none => ArgumentMarshaller.marshalInt 0 + | .uint, .none => ArgumentMarshaller.marshalUInt 0 + | .int, .buttonAreas => ArgumentMarshaller.marshalInt 1 + | .uint, .buttonAreas => ArgumentMarshaller.marshalUInt 1 + | .int, .clickfinger => ArgumentMarshaller.marshalInt 2 + | .uint, .clickfinger => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .none + | 1 => pure .buttonAreas + | 2 => pure .clickfinger + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .none + | 1 => pure .buttonAreas + | 2 => pure .clickfinger + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.ClickMethod + +namespace RiverLibinputDeviceV1.ClickMethods + +instance : Marshallable RiverLibinputDeviceV1.ClickMethods where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.buttonAreas then 1 else 0) + ||| (if μ.clickfinger then 2 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + buttonAreas := (μ &&& 1) == 1 + clickfinger := (μ &&& 2) == 2 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverLibinputDeviceV1.ClickMethods + +namespace RiverLibinputDeviceV1.ClickfingerButtonMap + +instance : Marshallable RiverLibinputDeviceV1.ClickfingerButtonMap where + marshal + | .int, .lrm => ArgumentMarshaller.marshalInt 0 + | .uint, .lrm => ArgumentMarshaller.marshalUInt 0 + | .int, .lmr => ArgumentMarshaller.marshalInt 1 + | .uint, .lmr => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .lrm + | 1 => pure .lmr + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .lrm + | 1 => pure .lmr + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.ClickfingerButtonMap + +namespace RiverLibinputDeviceV1.MiddleEmulationState + +instance : Marshallable RiverLibinputDeviceV1.MiddleEmulationState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.MiddleEmulationState + +namespace RiverLibinputDeviceV1.ScrollMethod + +instance : Marshallable RiverLibinputDeviceV1.ScrollMethod where + marshal + | .int, .noScroll => ArgumentMarshaller.marshalInt 0 + | .uint, .noScroll => ArgumentMarshaller.marshalUInt 0 + | .int, .twoFinger => ArgumentMarshaller.marshalInt 1 + | .uint, .twoFinger => ArgumentMarshaller.marshalUInt 1 + | .int, .edge => ArgumentMarshaller.marshalInt 2 + | .uint, .edge => ArgumentMarshaller.marshalUInt 2 + | .int, .onButtonDown => ArgumentMarshaller.marshalInt 4 + | .uint, .onButtonDown => ArgumentMarshaller.marshalUInt 4 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .noScroll + | 1 => pure .twoFinger + | 2 => pure .edge + | 4 => pure .onButtonDown + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .noScroll + | 1 => pure .twoFinger + | 2 => pure .edge + | 4 => pure .onButtonDown + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.ScrollMethod + +namespace RiverLibinputDeviceV1.ScrollMethods + +instance : Marshallable RiverLibinputDeviceV1.ScrollMethods where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.noScroll then 0 else 0) + ||| (if μ.twoFinger then 1 else 0) + ||| (if μ.edge then 2 else 0) + ||| (if μ.onButtonDown then 4 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + noScroll := (μ &&& 0) == 0 + twoFinger := (μ &&& 1) == 1 + edge := (μ &&& 2) == 2 + onButtonDown := (μ &&& 4) == 4 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverLibinputDeviceV1.ScrollMethods + +namespace RiverLibinputDeviceV1.ScrollButtonLockState + +instance : Marshallable RiverLibinputDeviceV1.ScrollButtonLockState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.ScrollButtonLockState + +namespace RiverLibinputDeviceV1.DwtState + +instance : Marshallable RiverLibinputDeviceV1.DwtState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.DwtState + +namespace RiverLibinputDeviceV1.DwtpState + +instance : Marshallable RiverLibinputDeviceV1.DwtpState where + marshal + | .int, .disabled => ArgumentMarshaller.marshalInt 0 + | .uint, .disabled => ArgumentMarshaller.marshalUInt 0 + | .int, .enabled => ArgumentMarshaller.marshalInt 1 + | .uint, .enabled => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .disabled + | 1 => pure .enabled + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputDeviceV1.DwtpState + +namespace RiverLibinputAccelConfigV1.Error + +instance : Marshallable RiverLibinputAccelConfigV1.Error where + marshal + | .int, .invalidArg => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidArg => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidArg + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidArg + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputAccelConfigV1.Error + +namespace RiverLibinputAccelConfigV1.AccelType + +instance : Marshallable RiverLibinputAccelConfigV1.AccelType where + marshal + | .int, .fallback => ArgumentMarshaller.marshalInt 0 + | .uint, .fallback => ArgumentMarshaller.marshalUInt 0 + | .int, .motion => ArgumentMarshaller.marshalInt 1 + | .uint, .motion => ArgumentMarshaller.marshalUInt 1 + | .int, .scroll => ArgumentMarshaller.marshalInt 2 + | .uint, .scroll => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .fallback + | 1 => pure .motion + | 2 => pure .scroll + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .fallback + | 1 => pure .motion + | 2 => pure .scroll + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverLibinputAccelConfigV1.AccelType + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Interface.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Interface.lean new file mode 100644 index 0000000..b98b0e9 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Interface.lean @@ -0,0 +1,868 @@ +import Wayland.Display +import Wayland.Protocols.RiverInputManagementV1.Header +import Wayland.Protocols.RiverLibinputConfigV1.Header + +namespace Wayland.Protocols + +inductive RiverLibinputConfigV1.Event where + | finished + | libinputDevice + (id : RiverLibinputDeviceV1) + +inductive RiverLibinputDeviceV1.Event where + | removed + | inputDevice + (device : RiverInputDeviceV1) + | sendEventsSupport + (modes : RiverLibinputDeviceV1.SendEventsModes) + | sendEventsDefault + (mode : RiverLibinputDeviceV1.SendEventsModes) + | sendEventsCurrent + (mode : RiverLibinputDeviceV1.SendEventsModes) + | tapSupport + (fingerCount : Int32) + | tapDefault + (state : RiverLibinputDeviceV1.TapState) + | tapCurrent + (state : RiverLibinputDeviceV1.TapState) + | tapButtonMapDefault + (buttonMap : RiverLibinputDeviceV1.TapButtonMap) + | tapButtonMapCurrent + (buttonMap : RiverLibinputDeviceV1.TapButtonMap) + | dragDefault + (state : RiverLibinputDeviceV1.DragState) + | dragCurrent + (state : RiverLibinputDeviceV1.DragState) + | dragLockDefault + (state : RiverLibinputDeviceV1.DragLockState) + | dragLockCurrent + (state : RiverLibinputDeviceV1.DragLockState) + | threeFingerDragSupport + (fingerCount : Int32) + | threeFingerDragDefault + (state : RiverLibinputDeviceV1.ThreeFingerDragState) + | threeFingerDragCurrent + (state : RiverLibinputDeviceV1.ThreeFingerDragState) + | calibrationMatrixSupport + (supported : Int32) + | calibrationMatrixDefault + (matrix : ByteArray) + | calibrationMatrixCurrent + (matrix : ByteArray) + | accelProfilesSupport + (profiles : RiverLibinputDeviceV1.AccelProfiles) + | accelProfileDefault + (profile : RiverLibinputDeviceV1.AccelProfile) + | accelProfileCurrent + (profile : RiverLibinputDeviceV1.AccelProfile) + | accelSpeedDefault + (speed : ByteArray) + | accelSpeedCurrent + (speed : ByteArray) + | naturalScrollSupport + (supported : Int32) + | naturalScrollDefault + (state : RiverLibinputDeviceV1.NaturalScrollState) + | naturalScrollCurrent + (state : RiverLibinputDeviceV1.NaturalScrollState) + | leftHandedSupport + (supported : Int32) + | leftHandedDefault + (state : RiverLibinputDeviceV1.LeftHandedState) + | leftHandedCurrent + (state : RiverLibinputDeviceV1.LeftHandedState) + | clickMethodSupport + (methods : RiverLibinputDeviceV1.ClickMethods) + | clickMethodDefault + (method : RiverLibinputDeviceV1.ClickMethod) + | clickMethodCurrent + (method : RiverLibinputDeviceV1.ClickMethod) + | clickfingerButtonMapDefault + (buttonMap : RiverLibinputDeviceV1.ClickfingerButtonMap) + | clickfingerButtonMapCurrent + (buttonMap : RiverLibinputDeviceV1.ClickfingerButtonMap) + | middleEmulationSupport + (supported : Int32) + | middleEmulationDefault + (state : RiverLibinputDeviceV1.MiddleEmulationState) + | middleEmulationCurrent + (state : RiverLibinputDeviceV1.MiddleEmulationState) + | scrollMethodSupport + (methods : RiverLibinputDeviceV1.ScrollMethods) + | scrollMethodDefault + (method : RiverLibinputDeviceV1.ScrollMethod) + | scrollMethodCurrent + (method : RiverLibinputDeviceV1.ScrollMethod) + | scrollButtonDefault + (button : UInt32) + | scrollButtonCurrent + (button : UInt32) + | scrollButtonLockDefault + (state : RiverLibinputDeviceV1.ScrollButtonLockState) + | scrollButtonLockCurrent + (state : RiverLibinputDeviceV1.ScrollButtonLockState) + | dwtSupport + (supported : Int32) + | dwtDefault + (state : RiverLibinputDeviceV1.DwtState) + | dwtCurrent + (state : RiverLibinputDeviceV1.DwtState) + | dwtpSupport + (supported : Int32) + | dwtpDefault + (state : RiverLibinputDeviceV1.DwtpState) + | dwtpCurrent + (state : RiverLibinputDeviceV1.DwtpState) + | rotationSupport + (supported : Int32) + | rotationDefault + (angle : UInt32) + | rotationCurrent + (angle : UInt32) + +inductive RiverLibinputAccelConfigV1.Event where + +inductive RiverLibinputResultV1.Event where + | success + | unsupported + | invalid + + +instance instInterfaceRiverLibinputConfigV1 : Interface RiverLibinputConfigV1.name where + event := RiverLibinputConfigV1.Event + version := 1 + requests := #[ + { + name := "stop" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "create_accel_config" + args := #[.newID (.some "river_libinput_accel_config_v1"), .uint] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "finished" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "libinput_device" + args := #[.newID (.some "river_libinput_device_v1")] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .finished + | 1 => do + return .libinputDevice + (← Marshallable.demarshal .object) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverLibinputDeviceV1 : Interface RiverLibinputDeviceV1.name where + event := RiverLibinputDeviceV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_send_events" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_tap" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_tap_button_map" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_drag" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_drag_lock" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_three_finger_drag" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_calibration_matrix" + args := #[.newID (.some "river_libinput_result_v1"), .array] + since := 1 + isDestructor := false + }, + { + name := "set_accel_profile" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_accel_speed" + args := #[.newID (.some "river_libinput_result_v1"), .array] + since := 1 + isDestructor := false + }, + { + name := "apply_accel_config" + args := #[.newID (.some "river_libinput_result_v1"), .object .notNull (.some "river_libinput_accel_config_v1")] + since := 1 + isDestructor := false + }, + { + name := "set_natural_scroll" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_left_handed" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_click_method" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_clickfinger_button_map" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_middle_emulation" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_scroll_method" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_scroll_button" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_scroll_button_lock" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_dwt" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_dwtp" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_rotation" + args := #[.newID (.some "river_libinput_result_v1"), .uint] + 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 := "send_events_support" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "send_events_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "send_events_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "tap_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "tap_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "tap_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "tap_button_map_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "tap_button_map_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "drag_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "drag_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "drag_lock_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "drag_lock_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "three_finger_drag_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "three_finger_drag_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "three_finger_drag_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "calibration_matrix_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "calibration_matrix_default" + args := #[.array] + since := 1 + isDestructor := false + }, + { + name := "calibration_matrix_current" + args := #[.array] + since := 1 + isDestructor := false + }, + { + name := "accel_profiles_support" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "accel_profile_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "accel_profile_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "accel_speed_default" + args := #[.array] + since := 1 + isDestructor := false + }, + { + name := "accel_speed_current" + args := #[.array] + since := 1 + isDestructor := false + }, + { + name := "natural_scroll_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "natural_scroll_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "natural_scroll_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "left_handed_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "left_handed_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "left_handed_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "click_method_support" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "click_method_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "click_method_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "clickfinger_button_map_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "clickfinger_button_map_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "middle_emulation_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "middle_emulation_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "middle_emulation_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_method_support" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_method_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_method_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_button_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_button_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_button_lock_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "scroll_button_lock_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "dwt_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "dwt_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "dwt_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "dwtp_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "dwtp_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "dwtp_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "rotation_support" + args := #[.int] + since := 1 + isDestructor := false + }, + { + name := "rotation_default" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "rotation_current" + args := #[.uint] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .removed + | 1 => do + return .inputDevice + (← Marshallable.demarshal .object) + | 2 => do + return .sendEventsSupport + (← Marshallable.demarshal .uint) + | 3 => do + return .sendEventsDefault + (← Marshallable.demarshal .uint) + | 4 => do + return .sendEventsCurrent + (← Marshallable.demarshal .uint) + | 5 => do + return .tapSupport + (← Marshallable.demarshal .int) + | 6 => do + return .tapDefault + (← Marshallable.demarshal .uint) + | 7 => do + return .tapCurrent + (← Marshallable.demarshal .uint) + | 8 => do + return .tapButtonMapDefault + (← Marshallable.demarshal .uint) + | 9 => do + return .tapButtonMapCurrent + (← Marshallable.demarshal .uint) + | 10 => do + return .dragDefault + (← Marshallable.demarshal .uint) + | 11 => do + return .dragCurrent + (← Marshallable.demarshal .uint) + | 12 => do + return .dragLockDefault + (← Marshallable.demarshal .uint) + | 13 => do + return .dragLockCurrent + (← Marshallable.demarshal .uint) + | 14 => do + return .threeFingerDragSupport + (← Marshallable.demarshal .int) + | 15 => do + return .threeFingerDragDefault + (← Marshallable.demarshal .uint) + | 16 => do + return .threeFingerDragCurrent + (← Marshallable.demarshal .uint) + | 17 => do + return .calibrationMatrixSupport + (← Marshallable.demarshal .int) + | 18 => do + return .calibrationMatrixDefault + (← Marshallable.demarshal .array) + | 19 => do + return .calibrationMatrixCurrent + (← Marshallable.demarshal .array) + | 20 => do + return .accelProfilesSupport + (← Marshallable.demarshal .uint) + | 21 => do + return .accelProfileDefault + (← Marshallable.demarshal .uint) + | 22 => do + return .accelProfileCurrent + (← Marshallable.demarshal .uint) + | 23 => do + return .accelSpeedDefault + (← Marshallable.demarshal .array) + | 24 => do + return .accelSpeedCurrent + (← Marshallable.demarshal .array) + | 25 => do + return .naturalScrollSupport + (← Marshallable.demarshal .int) + | 26 => do + return .naturalScrollDefault + (← Marshallable.demarshal .uint) + | 27 => do + return .naturalScrollCurrent + (← Marshallable.demarshal .uint) + | 28 => do + return .leftHandedSupport + (← Marshallable.demarshal .int) + | 29 => do + return .leftHandedDefault + (← Marshallable.demarshal .uint) + | 30 => do + return .leftHandedCurrent + (← Marshallable.demarshal .uint) + | 31 => do + return .clickMethodSupport + (← Marshallable.demarshal .uint) + | 32 => do + return .clickMethodDefault + (← Marshallable.demarshal .uint) + | 33 => do + return .clickMethodCurrent + (← Marshallable.demarshal .uint) + | 34 => do + return .clickfingerButtonMapDefault + (← Marshallable.demarshal .uint) + | 35 => do + return .clickfingerButtonMapCurrent + (← Marshallable.demarshal .uint) + | 36 => do + return .middleEmulationSupport + (← Marshallable.demarshal .int) + | 37 => do + return .middleEmulationDefault + (← Marshallable.demarshal .uint) + | 38 => do + return .middleEmulationCurrent + (← Marshallable.demarshal .uint) + | 39 => do + return .scrollMethodSupport + (← Marshallable.demarshal .uint) + | 40 => do + return .scrollMethodDefault + (← Marshallable.demarshal .uint) + | 41 => do + return .scrollMethodCurrent + (← Marshallable.demarshal .uint) + | 42 => do + return .scrollButtonDefault + (← Marshallable.demarshal .uint) + | 43 => do + return .scrollButtonCurrent + (← Marshallable.demarshal .uint) + | 44 => do + return .scrollButtonLockDefault + (← Marshallable.demarshal .uint) + | 45 => do + return .scrollButtonLockCurrent + (← Marshallable.demarshal .uint) + | 46 => do + return .dwtSupport + (← Marshallable.demarshal .int) + | 47 => do + return .dwtDefault + (← Marshallable.demarshal .uint) + | 48 => do + return .dwtCurrent + (← Marshallable.demarshal .uint) + | 49 => do + return .dwtpSupport + (← Marshallable.demarshal .int) + | 50 => do + return .dwtpDefault + (← Marshallable.demarshal .uint) + | 51 => do + return .dwtpCurrent + (← Marshallable.demarshal .uint) + | 52 => do + return .rotationSupport + (← Marshallable.demarshal .int) + | 53 => do + return .rotationDefault + (← Marshallable.demarshal .uint) + | 54 => do + return .rotationCurrent + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverLibinputAccelConfigV1 : Interface RiverLibinputAccelConfigV1.name where + event := RiverLibinputAccelConfigV1.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_points" + args := #[.newID (.some "river_libinput_result_v1"), .uint, .array, .array] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverLibinputResultV1 : Interface RiverLibinputResultV1.name where + event := RiverLibinputResultV1.Event + version := 1 + requests := #[ + ] + events := #[ + { + name := "success" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "unsupported" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "invalid" + args := #[] + since := 1 + isDestructor := true + }, + ] + demarshalEvent + | 0 => do + return .success + | 1 => do + return .unsupported + | 2 => do + return .invalid + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean new file mode 100644 index 0000000..12fb676 --- /dev/null +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Requests.lean @@ -0,0 +1,244 @@ +import Wayland.Display +import Wayland.Protocols.RiverLibinputConfigV1.Header +import Wayland.Protocols.RiverLibinputConfigV1.Resolved + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverLibinputConfigV1.stop + (ω : RiverLibinputConfigV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverLibinputConfigV1.destroy + (ω : RiverLibinputConfigV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverLibinputConfigV1.createAccelConfig + (ω : RiverLibinputConfigV1) + (profile : RiverLibinputDeviceV1.AccelProfile) + : DisplayM σ RiverLibinputAccelConfigV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint profile + return 2 + +def RiverLibinputDeviceV1.destroy + (ω : RiverLibinputDeviceV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverLibinputDeviceV1.setSendEvents + (ω : RiverLibinputDeviceV1) + (mode : RiverLibinputDeviceV1.SendEventsModes) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint mode + return 1 + +def RiverLibinputDeviceV1.setTap + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.TapState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 2 + +def RiverLibinputDeviceV1.setTapButtonMap + (ω : RiverLibinputDeviceV1) + (buttonMap : RiverLibinputDeviceV1.TapButtonMap) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint buttonMap + return 3 + +def RiverLibinputDeviceV1.setDrag + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.DragState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 4 + +def RiverLibinputDeviceV1.setDragLock + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.DragLockState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 5 + +def RiverLibinputDeviceV1.setThreeFingerDrag + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.ThreeFingerDragState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 6 + +def RiverLibinputDeviceV1.setCalibrationMatrix + (ω : RiverLibinputDeviceV1) + (matrix : ByteArray) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .array matrix + return 7 + +def RiverLibinputDeviceV1.setAccelProfile + (ω : RiverLibinputDeviceV1) + (profile : RiverLibinputDeviceV1.AccelProfile) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint profile + return 8 + +def RiverLibinputDeviceV1.setAccelSpeed + (ω : RiverLibinputDeviceV1) + (speed : ByteArray) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .array speed + return 9 + +def RiverLibinputDeviceV1.applyAccelConfig + (ω : RiverLibinputDeviceV1) + (config : RiverLibinputAccelConfigV1) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object config + return 10 + +def RiverLibinputDeviceV1.setNaturalScroll + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.NaturalScrollState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 11 + +def RiverLibinputDeviceV1.setLeftHanded + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.LeftHandedState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 12 + +def RiverLibinputDeviceV1.setClickMethod + (ω : RiverLibinputDeviceV1) + (method : RiverLibinputDeviceV1.ClickMethod) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint method + return 13 + +def RiverLibinputDeviceV1.setClickfingerButtonMap + (ω : RiverLibinputDeviceV1) + (buttonMap : RiverLibinputDeviceV1.ClickfingerButtonMap) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint buttonMap + return 14 + +def RiverLibinputDeviceV1.setMiddleEmulation + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.MiddleEmulationState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 15 + +def RiverLibinputDeviceV1.setScrollMethod + (ω : RiverLibinputDeviceV1) + (method : RiverLibinputDeviceV1.ScrollMethod) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint method + return 16 + +def RiverLibinputDeviceV1.setScrollButton + (ω : RiverLibinputDeviceV1) + (button : UInt32) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint button + return 17 + +def RiverLibinputDeviceV1.setScrollButtonLock + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.ScrollButtonLockState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 18 + +def RiverLibinputDeviceV1.setDwt + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.DwtState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 19 + +def RiverLibinputDeviceV1.setDwtp + (ω : RiverLibinputDeviceV1) + (state : RiverLibinputDeviceV1.DwtpState) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint state + return 20 + +def RiverLibinputDeviceV1.setRotation + (ω : RiverLibinputDeviceV1) + (angle : UInt32) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint angle + return 21 + +def RiverLibinputAccelConfigV1.destroy + (ω : RiverLibinputAccelConfigV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverLibinputAccelConfigV1.setPoints + (ω : RiverLibinputAccelConfigV1) + (type : RiverLibinputAccelConfigV1.AccelType) + (step : ByteArray) + (points : ByteArray) + : DisplayM σ RiverLibinputResultV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint type + Marshallable.marshal .array step + Marshallable.marshal .array points + return 1 + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverLibinputConfigV1/Resolved.lean b/lib/Wayland/Protocols/RiverLibinputConfigV1/Resolved.lean new file mode 100644 index 0000000..1e538bd --- /dev/null +++ b/lib/Wayland/Protocols/RiverLibinputConfigV1/Resolved.lean @@ -0,0 +1,39 @@ +import Wayland.Display +import Wayland.Protocols.RiverInputManagementV1.Interface +import Wayland.Protocols.RiverLibinputConfigV1.Interface +import Wayland.Protocols.Wayland.Interface + +namespace Wayland.Protocols + +instance instResolvedInterfaceRiverLibinputConfigV1 : ResolvedInterface RiverLibinputConfigV1.name where + referencedInterfaces := #[ + ⟨RiverInputDeviceV1.name, inferInstance⟩, + ⟨RiverLibinputAccelConfigV1.name, inferInstance⟩, + ⟨RiverLibinputConfigV1.name, inferInstance⟩, + ⟨RiverLibinputDeviceV1.name, inferInstance⟩, + ⟨RiverLibinputResultV1.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverLibinputDeviceV1 : ResolvedInterface RiverLibinputDeviceV1.name where + referencedInterfaces := #[ + ⟨RiverInputDeviceV1.name, inferInstance⟩, + ⟨RiverLibinputAccelConfigV1.name, inferInstance⟩, + ⟨RiverLibinputDeviceV1.name, inferInstance⟩, + ⟨RiverLibinputResultV1.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverLibinputAccelConfigV1 : ResolvedInterface RiverLibinputAccelConfigV1.name where + referencedInterfaces := #[ + ⟨RiverLibinputAccelConfigV1.name, inferInstance⟩, + ⟨RiverLibinputResultV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverLibinputResultV1 : ResolvedInterface RiverLibinputResultV1.name where + referencedInterfaces := #[ + ⟨RiverLibinputResultV1.name, inferInstance⟩, + ] + + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1.lean b/lib/Wayland/Protocols/RiverWindowManagementV1.lean new file mode 100644 index 0000000..e6b3414 --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverWindowManagementV1.Header +import Wayland.Protocols.RiverWindowManagementV1.Interface +import Wayland.Protocols.RiverWindowManagementV1.Requests +import Wayland.Protocols.RiverWindowManagementV1.Resolved diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean new file mode 100644 index 0000000..4acaf02 --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean @@ -0,0 +1,336 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverWindowManagerV1.name : InterfaceName := "river_window_manager_v1" +abbrev RiverWindowV1.name : InterfaceName := "river_window_v1" +abbrev RiverDecorationV1.name : InterfaceName := "river_decoration_v1" +abbrev RiverShellSurfaceV1.name : InterfaceName := "river_shell_surface_v1" +abbrev RiverNodeV1.name : InterfaceName := "river_node_v1" +abbrev RiverOutputV1.name : InterfaceName := "river_output_v1" +abbrev RiverSeatV1.name : InterfaceName := "river_seat_v1" +abbrev RiverPointerBindingV1.name : InterfaceName := "river_pointer_binding_v1" + +abbrev RiverWindowManagerV1 : Type := Object RiverWindowManagerV1.name +abbrev RiverWindowV1 : Type := Object RiverWindowV1.name +abbrev RiverDecorationV1 : Type := Object RiverDecorationV1.name +abbrev RiverShellSurfaceV1 : Type := Object RiverShellSurfaceV1.name +abbrev RiverNodeV1 : Type := Object RiverNodeV1.name +abbrev RiverOutputV1 : Type := Object RiverOutputV1.name +abbrev RiverSeatV1 : Type := Object RiverSeatV1.name +abbrev RiverPointerBindingV1 : Type := Object RiverPointerBindingV1.name + +inductive RiverWindowManagerV1.Error where + | sequenceOrder + | role + | unresponsive + +inductive RiverWindowV1.Error where + | nodeExists + | invalidDimensions + | invalidBorder + | invalidClipBox + +inductive RiverWindowV1.DecorationHint where + | onlySupportsCsd + | prefersCsd + | prefersSsd + | noPreference + +structure RiverWindowV1.Edges where + none : Bool + top : Bool + bottom : Bool + left : Bool + right : Bool + +structure RiverWindowV1.Capabilities where + windowMenu : Bool + maximize : Bool + fullscreen : Bool + minimize : Bool + +inductive RiverDecorationV1.Error where + | noCommit + +inductive RiverShellSurfaceV1.Error where + | nodeExists + | noCommit + +inductive RiverOutputV1.Error where + | invalidPresentationMode + +inductive RiverOutputV1.PresentationMode where + | vsync + | async + +structure RiverSeatV1.Modifiers where + none : Bool + shift : Bool + ctrl : Bool + mod1 : Bool + mod3 : Bool + mod4 : Bool + mod5 : Bool + +namespace RiverWindowManagerV1.Error + +instance : Marshallable RiverWindowManagerV1.Error where + marshal + | .int, .sequenceOrder => ArgumentMarshaller.marshalInt 0 + | .uint, .sequenceOrder => ArgumentMarshaller.marshalUInt 0 + | .int, .role => ArgumentMarshaller.marshalInt 1 + | .uint, .role => ArgumentMarshaller.marshalUInt 1 + | .int, .unresponsive => ArgumentMarshaller.marshalInt 2 + | .uint, .unresponsive => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .sequenceOrder + | 1 => pure .role + | 2 => pure .unresponsive + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .sequenceOrder + | 1 => pure .role + | 2 => pure .unresponsive + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverWindowManagerV1.Error + +namespace RiverWindowV1.Error + +instance : Marshallable RiverWindowV1.Error where + marshal + | .int, .nodeExists => ArgumentMarshaller.marshalInt 0 + | .uint, .nodeExists => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidDimensions => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidDimensions => ArgumentMarshaller.marshalUInt 1 + | .int, .invalidBorder => ArgumentMarshaller.marshalInt 2 + | .uint, .invalidBorder => ArgumentMarshaller.marshalUInt 2 + | .int, .invalidClipBox => ArgumentMarshaller.marshalInt 3 + | .uint, .invalidClipBox => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .nodeExists + | 1 => pure .invalidDimensions + | 2 => pure .invalidBorder + | 3 => pure .invalidClipBox + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .nodeExists + | 1 => pure .invalidDimensions + | 2 => pure .invalidBorder + | 3 => pure .invalidClipBox + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverWindowV1.Error + +namespace RiverWindowV1.DecorationHint + +instance : Marshallable RiverWindowV1.DecorationHint where + marshal + | .int, .onlySupportsCsd => ArgumentMarshaller.marshalInt 0 + | .uint, .onlySupportsCsd => ArgumentMarshaller.marshalUInt 0 + | .int, .prefersCsd => ArgumentMarshaller.marshalInt 1 + | .uint, .prefersCsd => ArgumentMarshaller.marshalUInt 1 + | .int, .prefersSsd => ArgumentMarshaller.marshalInt 2 + | .uint, .prefersSsd => ArgumentMarshaller.marshalUInt 2 + | .int, .noPreference => ArgumentMarshaller.marshalInt 3 + | .uint, .noPreference => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .onlySupportsCsd + | 1 => pure .prefersCsd + | 2 => pure .prefersSsd + | 3 => pure .noPreference + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .onlySupportsCsd + | 1 => pure .prefersCsd + | 2 => pure .prefersSsd + | 3 => pure .noPreference + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverWindowV1.DecorationHint + +namespace RiverWindowV1.Edges + +instance : Marshallable RiverWindowV1.Edges where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.top then 1 else 0) + ||| (if μ.bottom then 2 else 0) + ||| (if μ.left then 4 else 0) + ||| (if μ.right then 8 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + top := (μ &&& 1) == 1 + bottom := (μ &&& 2) == 2 + left := (μ &&& 4) == 4 + right := (μ &&& 8) == 8 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverWindowV1.Edges + +namespace RiverWindowV1.Capabilities + +instance : Marshallable RiverWindowV1.Capabilities where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.windowMenu then 1 else 0) + ||| (if μ.maximize then 2 else 0) + ||| (if μ.fullscreen then 4 else 0) + ||| (if μ.minimize then 8 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + windowMenu := (μ &&& 1) == 1 + maximize := (μ &&& 2) == 2 + fullscreen := (μ &&& 4) == 4 + minimize := (μ &&& 8) == 8 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverWindowV1.Capabilities + +namespace RiverDecorationV1.Error + +instance : Marshallable RiverDecorationV1.Error where + marshal + | .int, .noCommit => ArgumentMarshaller.marshalInt 0 + | .uint, .noCommit => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .noCommit + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .noCommit + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverDecorationV1.Error + +namespace RiverShellSurfaceV1.Error + +instance : Marshallable RiverShellSurfaceV1.Error where + marshal + | .int, .nodeExists => ArgumentMarshaller.marshalInt 0 + | .uint, .nodeExists => ArgumentMarshaller.marshalUInt 0 + | .int, .noCommit => ArgumentMarshaller.marshalInt 1 + | .uint, .noCommit => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .nodeExists + | 1 => pure .noCommit + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .nodeExists + | 1 => pure .noCommit + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverShellSurfaceV1.Error + +namespace RiverOutputV1.Error + +instance : Marshallable RiverOutputV1.Error where + marshal + | .int, .invalidPresentationMode => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidPresentationMode => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidPresentationMode + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidPresentationMode + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverOutputV1.Error + +namespace RiverOutputV1.PresentationMode + +instance : Marshallable RiverOutputV1.PresentationMode where + marshal + | .int, .vsync => ArgumentMarshaller.marshalInt 0 + | .uint, .vsync => ArgumentMarshaller.marshalUInt 0 + | .int, .async => ArgumentMarshaller.marshalInt 1 + | .uint, .async => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .vsync + | 1 => pure .async + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .vsync + | 1 => pure .async + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverOutputV1.PresentationMode + +namespace RiverSeatV1.Modifiers + +instance : Marshallable RiverSeatV1.Modifiers where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.shift then 1 else 0) + ||| (if μ.ctrl then 4 else 0) + ||| (if μ.mod1 then 8 else 0) + ||| (if μ.mod3 then 32 else 0) + ||| (if μ.mod4 then 64 else 0) + ||| (if μ.mod5 then 128 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + shift := (μ &&& 1) == 1 + ctrl := (μ &&& 4) == 4 + mod1 := (μ &&& 8) == 8 + mod3 := (μ &&& 32) == 32 + mod4 := (μ &&& 64) == 64 + mod5 := (μ &&& 128) == 128 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end RiverSeatV1.Modifiers + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Interface.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Interface.lean new file mode 100644 index 0000000..32050e3 --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Interface.lean @@ -0,0 +1,893 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Header + +namespace Wayland.Protocols + +inductive RiverWindowManagerV1.Event where + | unavailable + | finished + | manageStart + | renderStart + | sessionLocked + | sessionUnlocked + | window + (id : RiverWindowV1) + | output + (id : RiverOutputV1) + | seat + (id : RiverSeatV1) + +inductive RiverWindowV1.Event where + | closed + | dimensionsHint + (minWidth : Int32) + (minHeight : Int32) + (maxWidth : Int32) + (maxHeight : Int32) + | dimensions + (width : Int32) + (height : Int32) + | appId + (appId : Option String) + | title + (title : Option String) + | parent + (parent : Option RiverWindowV1) + | decorationHint + (hint : RiverWindowV1.DecorationHint) + | pointerMoveRequested + (seat : RiverSeatV1) + | pointerResizeRequested + (seat : RiverSeatV1) + (edges : RiverWindowV1.Edges) + | showWindowMenuRequested + (x : Int32) + (y : Int32) + | maximizeRequested + | unmaximizeRequested + | fullscreenRequested + (output : Option RiverOutputV1) + | exitFullscreenRequested + | minimizeRequested + | unreliablePid + (unreliablePid : Int32) + | presentationHint + (hint : RiverOutputV1.PresentationMode) + | identifier + (identifier : String) + +inductive RiverDecorationV1.Event where + +inductive RiverShellSurfaceV1.Event where + +inductive RiverNodeV1.Event where + +inductive RiverOutputV1.Event where + | removed + | wlOutput + (name : UInt32) + | position + (x : Int32) + (y : Int32) + | dimensions + (width : Int32) + (height : Int32) + +inductive RiverSeatV1.Event where + | removed + | wlSeat + (name : UInt32) + | pointerEnter + (window : RiverWindowV1) + | pointerLeave + | windowInteraction + (window : RiverWindowV1) + | shellSurfaceInteraction + (shellSurface : RiverShellSurfaceV1) + | opDelta + (dx : Int32) + (dy : Int32) + | opRelease + | pointerPosition + (x : Int32) + (y : Int32) + +inductive RiverPointerBindingV1.Event where + | pressed + | released + + +instance instInterfaceRiverWindowManagerV1 : Interface RiverWindowManagerV1.name where + event := RiverWindowManagerV1.Event + version := 4 + requests := #[ + { + name := "stop" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "manage_finish" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "manage_dirty" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "render_finish" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "get_shell_surface" + args := #[.newID (.some "river_shell_surface_v1"), .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "exit_session" + args := #[] + since := 4 + isDestructor := false + }, + ] + events := #[ + { + name := "unavailable" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "finished" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "manage_start" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "render_start" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "session_locked" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "session_unlocked" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "window" + args := #[.newID (.some "river_window_v1")] + since := 1 + isDestructor := false + }, + { + name := "output" + args := #[.newID (.some "river_output_v1")] + since := 1 + isDestructor := false + }, + { + name := "seat" + args := #[.newID (.some "river_seat_v1")] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .unavailable + | 1 => do + return .finished + | 2 => do + return .manageStart + | 3 => do + return .renderStart + | 4 => do + return .sessionLocked + | 5 => do + return .sessionUnlocked + | 6 => do + return .window + (← Marshallable.demarshal .object) + | 7 => do + return .output + (← Marshallable.demarshal .object) + | 8 => do + return .seat + (← Marshallable.demarshal .object) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverWindowV1 : Interface RiverWindowV1.name where + event := RiverWindowV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "close" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "get_node" + args := #[.newID (.some "river_node_v1")] + since := 1 + isDestructor := false + }, + { + name := "propose_dimensions" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "hide" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "show" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "use_csd" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "use_ssd" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_borders" + args := #[.uint, .int, .uint, .uint, .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "set_tiled" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "get_decoration_above" + args := #[.newID (.some "river_decoration_v1"), .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "get_decoration_below" + args := #[.newID (.some "river_decoration_v1"), .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "inform_resize_start" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "inform_resize_end" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_capabilities" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "inform_maximized" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "inform_unmaximized" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "inform_fullscreen" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "inform_not_fullscreen" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "fullscreen" + args := #[.object .notNull (.some "river_output_v1")] + since := 1 + isDestructor := false + }, + { + name := "exit_fullscreen" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_clip_box" + args := #[.int, .int, .int, .int] + since := 2 + isDestructor := false + }, + { + name := "set_content_clip_box" + args := #[.int, .int, .int, .int] + since := 3 + isDestructor := false + }, + { + name := "set_dimension_bounds" + args := #[.int, .int] + since := 4 + isDestructor := false + }, + ] + events := #[ + { + name := "closed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "dimensions_hint" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + { + name := "dimensions" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "app_id" + args := #[.string .nullable] + since := 1 + isDestructor := false + }, + { + name := "title" + args := #[.string .nullable] + since := 1 + isDestructor := false + }, + { + name := "parent" + args := #[.object .nullable (.some "river_window_v1")] + since := 1 + isDestructor := false + }, + { + name := "decoration_hint" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "pointer_move_requested" + args := #[.object .notNull (.some "river_seat_v1")] + since := 1 + isDestructor := false + }, + { + name := "pointer_resize_requested" + args := #[.object .notNull (.some "river_seat_v1"), .uint] + since := 1 + isDestructor := false + }, + { + name := "show_window_menu_requested" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "maximize_requested" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "unmaximize_requested" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "fullscreen_requested" + args := #[.object .nullable (.some "river_output_v1")] + since := 1 + isDestructor := false + }, + { + name := "exit_fullscreen_requested" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "minimize_requested" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "unreliable_pid" + args := #[.int] + since := 2 + isDestructor := false + }, + { + name := "presentation_hint" + args := #[.uint] + since := 4 + isDestructor := false + }, + { + name := "identifier" + args := #[.string .notNull] + since := 4 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .closed + | 1 => do + return .dimensionsHint + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 2 => do + return .dimensions + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 3 => do + return .appId + (← Marshallable.demarshal .string) + | 4 => do + return .title + (← Marshallable.demarshal .string) + | 5 => do + return .parent + (← Marshallable.demarshal .object) + | 6 => do + return .decorationHint + (← Marshallable.demarshal .uint) + | 7 => do + return .pointerMoveRequested + (← Marshallable.demarshal .object) + | 8 => do + return .pointerResizeRequested + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .uint) + | 9 => do + return .showWindowMenuRequested + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 10 => do + return .maximizeRequested + | 11 => do + return .unmaximizeRequested + | 12 => do + return .fullscreenRequested + (← Marshallable.demarshal .object) + | 13 => do + return .exitFullscreenRequested + | 14 => do + return .minimizeRequested + | 15 => do + return .unreliablePid + (← Marshallable.demarshal .int) + | 16 => do + return .presentationHint + (← Marshallable.demarshal .uint) + | 17 => do + return .identifier + (← Marshallable.demarshal .string) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverDecorationV1 : Interface RiverDecorationV1.name where + event := RiverDecorationV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_offset" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "sync_next_commit" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverShellSurfaceV1 : Interface RiverShellSurfaceV1.name where + event := RiverShellSurfaceV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "get_node" + args := #[.newID (.some "river_node_v1")] + since := 1 + isDestructor := false + }, + { + name := "sync_next_commit" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverNodeV1 : Interface RiverNodeV1.name where + event := RiverNodeV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_position" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "place_top" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "place_bottom" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "place_above" + args := #[.object .notNull (.some "river_node_v1")] + since := 1 + isDestructor := false + }, + { + name := "place_below" + args := #[.object .notNull (.some "river_node_v1")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverOutputV1 : Interface RiverOutputV1.name where + event := RiverOutputV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_presentation_mode" + args := #[.uint] + since := 4 + isDestructor := false + }, + ] + events := #[ + { + name := "removed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "wl_output" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "position" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "dimensions" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .removed + | 1 => do + return .wlOutput + (← Marshallable.demarshal .uint) + | 2 => do + return .position + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 3 => do + return .dimensions + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverSeatV1 : Interface RiverSeatV1.name where + event := RiverSeatV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "focus_window" + args := #[.object .notNull (.some "river_window_v1")] + since := 1 + isDestructor := false + }, + { + name := "focus_shell_surface" + args := #[.object .notNull (.some "river_shell_surface_v1")] + since := 1 + isDestructor := false + }, + { + name := "clear_focus" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "op_start_pointer" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "op_end" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "get_pointer_binding" + args := #[.newID (.some "river_pointer_binding_v1"), .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "set_xcursor_theme" + args := #[.string .notNull, .uint] + since := 2 + isDestructor := false + }, + { + name := "pointer_warp" + args := #[.int, .int] + since := 3 + isDestructor := false + }, + ] + events := #[ + { + name := "removed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "wl_seat" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "pointer_enter" + args := #[.object .notNull (.some "river_window_v1")] + since := 1 + isDestructor := false + }, + { + name := "pointer_leave" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "window_interaction" + args := #[.object .notNull (.some "river_window_v1")] + since := 1 + isDestructor := false + }, + { + name := "shell_surface_interaction" + args := #[.object .notNull (.some "river_shell_surface_v1")] + since := 1 + isDestructor := false + }, + { + name := "op_delta" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "op_release" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "pointer_position" + args := #[.int, .int] + since := 2 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .removed + | 1 => do + return .wlSeat + (← Marshallable.demarshal .uint) + | 2 => do + return .pointerEnter + (← Marshallable.demarshal .object) + | 3 => do + return .pointerLeave + | 4 => do + return .windowInteraction + (← Marshallable.demarshal .object) + | 5 => do + return .shellSurfaceInteraction + (← Marshallable.demarshal .object) + | 6 => do + return .opDelta + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 7 => do + return .opRelease + | 8 => do + return .pointerPosition + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverPointerBindingV1 : Interface RiverPointerBindingV1.name where + event := RiverPointerBindingV1.Event + version := 4 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "enable" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "disable" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "pressed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "released" + args := #[] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .pressed + | 1 => do + return .released + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean new file mode 100644 index 0000000..ed70fed --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Requests.lean @@ -0,0 +1,436 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Header +import Wayland.Protocols.RiverWindowManagementV1.Resolved +import Wayland.Protocols.Wayland.Header + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverWindowManagerV1.stop + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverWindowManagerV1.destroy + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverWindowManagerV1.manageFinish + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverWindowManagerV1.manageDirty + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverWindowManagerV1.renderFinish + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverWindowManagerV1.getShellSurface + (ω : RiverWindowManagerV1) + (surface : WlSurface) + : DisplayM σ RiverShellSurfaceV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 5 + +def RiverWindowManagerV1.exitSession + (ω : RiverWindowManagerV1) + : DisplayM σ Unit := + ω.send do + return 6 + +def RiverWindowV1.destroy + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverWindowV1.close + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverWindowV1.getNode + (ω : RiverWindowV1) + : DisplayM σ RiverNodeV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 2 + +def RiverWindowV1.proposeDimensions + (ω : RiverWindowV1) + (width : Int32) + (height : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int width + Marshallable.marshal .int height + return 3 + +def RiverWindowV1.hide + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverWindowV1.show + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 5 + +def RiverWindowV1.useCsd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 6 + +def RiverWindowV1.useSsd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 7 + +def RiverWindowV1.setBorders + (ω : RiverWindowV1) + (edges : RiverWindowV1.Edges) + (width : Int32) + (r : UInt32) + (g : UInt32) + (b : UInt32) + (a : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint edges + Marshallable.marshal .int width + Marshallable.marshal .uint r + Marshallable.marshal .uint g + Marshallable.marshal .uint b + Marshallable.marshal .uint a + return 8 + +def RiverWindowV1.setTiled + (ω : RiverWindowV1) + (edges : RiverWindowV1.Edges) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint edges + return 9 + +def RiverWindowV1.getDecorationAbove + (ω : RiverWindowV1) + (surface : WlSurface) + : DisplayM σ RiverDecorationV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 10 + +def RiverWindowV1.getDecorationBelow + (ω : RiverWindowV1) + (surface : WlSurface) + : DisplayM σ RiverDecorationV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 11 + +def RiverWindowV1.informResizeStart + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 12 + +def RiverWindowV1.informResizeEnd + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 13 + +def RiverWindowV1.setCapabilities + (ω : RiverWindowV1) + (caps : RiverWindowV1.Capabilities) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint caps + return 14 + +def RiverWindowV1.informMaximized + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 15 + +def RiverWindowV1.informUnmaximized + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 16 + +def RiverWindowV1.informFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 17 + +def RiverWindowV1.informNotFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 18 + +def RiverWindowV1.fullscreen + (ω : RiverWindowV1) + (output : RiverOutputV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object output + return 19 + +def RiverWindowV1.exitFullscreen + (ω : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + return 20 + +def RiverWindowV1.setClipBox + (ω : RiverWindowV1) + (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 21 + +def RiverWindowV1.setContentClipBox + (ω : RiverWindowV1) + (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 22 + +def RiverWindowV1.setDimensionBounds + (ω : RiverWindowV1) + (maxWidth : Int32) + (maxHeight : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int maxWidth + Marshallable.marshal .int maxHeight + return 23 + +def RiverDecorationV1.destroy + (ω : RiverDecorationV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverDecorationV1.setOffset + (ω : RiverDecorationV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def RiverDecorationV1.syncNextCommit + (ω : RiverDecorationV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverShellSurfaceV1.destroy + (ω : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverShellSurfaceV1.getNode + (ω : RiverShellSurfaceV1) + : DisplayM σ RiverNodeV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 1 + +def RiverShellSurfaceV1.syncNextCommit + (ω : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverNodeV1.destroy + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverNodeV1.setPosition + (ω : RiverNodeV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def RiverNodeV1.placeTop + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverNodeV1.placeBottom + (ω : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverNodeV1.placeAbove + (ω : RiverNodeV1) + (other : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object other + return 4 + +def RiverNodeV1.placeBelow + (ω : RiverNodeV1) + (other : RiverNodeV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object other + return 5 + +def RiverOutputV1.destroy + (ω : RiverOutputV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverOutputV1.setPresentationMode + (ω : RiverOutputV1) + (mode : RiverOutputV1.PresentationMode) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint mode + return 1 + +def RiverSeatV1.destroy + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverSeatV1.focusWindow + (ω : RiverSeatV1) + (window : RiverWindowV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object window + return 1 + +def RiverSeatV1.focusShellSurface + (ω : RiverSeatV1) + (shellSurface : RiverShellSurfaceV1) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object shellSurface + return 2 + +def RiverSeatV1.clearFocus + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverSeatV1.opStartPointer + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 4 + +def RiverSeatV1.opEnd + (ω : RiverSeatV1) + : DisplayM σ Unit := + ω.send do + return 5 + +def RiverSeatV1.getPointerBinding + (ω : RiverSeatV1) + (button : UInt32) + (modifiers : RiverSeatV1.Modifiers) + : DisplayM σ RiverPointerBindingV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint button + Marshallable.marshal .uint modifiers + return 6 + +def RiverSeatV1.setXcursorTheme + (ω : RiverSeatV1) + (name : String) + (size : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string name + Marshallable.marshal .uint size + return 7 + +def RiverSeatV1.pointerWarp + (ω : RiverSeatV1) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 8 + +def RiverPointerBindingV1.destroy + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverPointerBindingV1.enable + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverPointerBindingV1.disable + (ω : RiverPointerBindingV1) + : DisplayM σ Unit := + ω.send do + return 2 + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverWindowManagementV1/Resolved.lean b/lib/Wayland/Protocols/RiverWindowManagementV1/Resolved.lean new file mode 100644 index 0000000..0022cb6 --- /dev/null +++ b/lib/Wayland/Protocols/RiverWindowManagementV1/Resolved.lean @@ -0,0 +1,83 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Interface +import Wayland.Protocols.Wayland.Interface + +namespace Wayland.Protocols + +instance instResolvedInterfaceRiverWindowManagerV1 : ResolvedInterface RiverWindowManagerV1.name where + referencedInterfaces := #[ + ⟨RiverDecorationV1.name, inferInstance⟩, + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverOutputV1.name, inferInstance⟩, + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ⟨RiverSeatV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ⟨RiverWindowManagerV1.name, inferInstance⟩, + ⟨RiverWindowV1.name, inferInstance⟩, + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverWindowV1 : ResolvedInterface RiverWindowV1.name where + referencedInterfaces := #[ + ⟨RiverDecorationV1.name, inferInstance⟩, + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverOutputV1.name, inferInstance⟩, + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ⟨RiverSeatV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ⟨RiverWindowV1.name, inferInstance⟩, + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverDecorationV1 : ResolvedInterface RiverDecorationV1.name where + referencedInterfaces := #[ + ⟨RiverDecorationV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverShellSurfaceV1 : ResolvedInterface RiverShellSurfaceV1.name where + referencedInterfaces := #[ + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverNodeV1 : ResolvedInterface RiverNodeV1.name where + referencedInterfaces := #[ + ⟨RiverNodeV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverOutputV1 : ResolvedInterface RiverOutputV1.name where + referencedInterfaces := #[ + ⟨RiverOutputV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverSeatV1 : ResolvedInterface RiverSeatV1.name where + referencedInterfaces := #[ + ⟨RiverDecorationV1.name, inferInstance⟩, + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverOutputV1.name, inferInstance⟩, + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ⟨RiverSeatV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ⟨RiverWindowV1.name, inferInstance⟩, + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverPointerBindingV1 : ResolvedInterface RiverPointerBindingV1.name where + referencedInterfaces := #[ + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ] + + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1.lean new file mode 100644 index 0000000..e041592 --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbBindingsV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverXkbBindingsV1.Header +import Wayland.Protocols.RiverXkbBindingsV1.Interface +import Wayland.Protocols.RiverXkbBindingsV1.Requests +import Wayland.Protocols.RiverXkbBindingsV1.Resolved diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean new file mode 100644 index 0000000..96d0cfa --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Header.lean @@ -0,0 +1,36 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverXkbBindingsV1.name : InterfaceName := "river_xkb_bindings_v1" +abbrev RiverXkbBindingV1.name : InterfaceName := "river_xkb_binding_v1" +abbrev RiverXkbBindingsSeatV1.name : InterfaceName := "river_xkb_bindings_seat_v1" + +abbrev RiverXkbBindingsV1 : Type := Object RiverXkbBindingsV1.name +abbrev RiverXkbBindingV1 : Type := Object RiverXkbBindingV1.name +abbrev RiverXkbBindingsSeatV1 : Type := Object RiverXkbBindingsSeatV1.name + +inductive RiverXkbBindingsV1.Error where + | objectAlreadyCreated + +namespace RiverXkbBindingsV1.Error + +instance : Marshallable RiverXkbBindingsV1.Error where + marshal + | .int, .objectAlreadyCreated => ArgumentMarshaller.marshalInt 0 + | .uint, .objectAlreadyCreated => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .objectAlreadyCreated + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverXkbBindingsV1.Error + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Interface.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Interface.lean new file mode 100644 index 0000000..1c4e3ac --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Interface.lean @@ -0,0 +1,139 @@ +import Wayland.Display +import Wayland.Protocols.RiverXkbBindingsV1.Header + +namespace Wayland.Protocols + +inductive RiverXkbBindingsV1.Event where + +inductive RiverXkbBindingV1.Event where + | pressed + | released + | stopRepeat + +inductive RiverXkbBindingsSeatV1.Event where + | ateUnboundKey + + +instance instInterfaceRiverXkbBindingsV1 : Interface RiverXkbBindingsV1.name where + event := RiverXkbBindingsV1.Event + version := 2 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "get_xkb_binding" + args := #[.object .notNull (.some "river_seat_v1"), .newID (.some "river_xkb_binding_v1"), .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "get_seat" + args := #[.newID (.some "river_xkb_bindings_seat_v1"), .object .notNull (.some "river_seat_v1")] + since := 2 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverXkbBindingV1 : Interface RiverXkbBindingV1.name where + event := RiverXkbBindingV1.Event + version := 2 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_layout_override" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "enable" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "disable" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "pressed" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "released" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "stop_repeat" + args := #[] + since := 2 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .pressed + | 1 => do + return .released + | 2 => do + return .stopRepeat + | _ => throw s!"Received invalid opcode" + +instance instInterfaceRiverXkbBindingsSeatV1 : Interface RiverXkbBindingsSeatV1.name where + event := RiverXkbBindingsSeatV1.Event + version := 2 + requests := #[ + { + name := "destroy" + args := #[] + since := 2 + isDestructor := true + }, + { + name := "ensure_next_key_eaten" + args := #[] + since := 2 + isDestructor := false + }, + { + name := "cancel_ensure_next_key_eaten" + args := #[] + since := 2 + isDestructor := false + }, + ] + events := #[ + { + name := "ate_unbound_key" + args := #[] + since := 2 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .ateUnboundKey + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean new file mode 100644 index 0000000..691e32e --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Requests.lean @@ -0,0 +1,81 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Header +import Wayland.Protocols.RiverXkbBindingsV1.Resolved + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def RiverXkbBindingsV1.destroy + (ω : RiverXkbBindingsV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverXkbBindingsV1.getXkbBinding + (ω : RiverXkbBindingsV1) + (seat : RiverSeatV1) + (keysym : UInt32) + (modifiers : RiverSeatV1.Modifiers) + : DisplayM σ RiverXkbBindingV1 := + ω.sendConstructor do + Marshallable.marshal .object seat + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .uint keysym + Marshallable.marshal .uint modifiers + return 1 + +def RiverXkbBindingsV1.getSeat + (ω : RiverXkbBindingsV1) + (seat : RiverSeatV1) + : DisplayM σ RiverXkbBindingsSeatV1 := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object seat + return 2 + +def RiverXkbBindingV1.destroy + (ω : RiverXkbBindingV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverXkbBindingV1.setLayoutOverride + (ω : RiverXkbBindingV1) + (layout : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint layout + return 1 + +def RiverXkbBindingV1.enable + (ω : RiverXkbBindingV1) + : DisplayM σ Unit := + ω.send do + return 2 + +def RiverXkbBindingV1.disable + (ω : RiverXkbBindingV1) + : DisplayM σ Unit := + ω.send do + return 3 + +def RiverXkbBindingsSeatV1.destroy + (ω : RiverXkbBindingsSeatV1) + : DisplayM σ Unit := + ω.send do + return 0 + +def RiverXkbBindingsSeatV1.ensureNextKeyEaten + (ω : RiverXkbBindingsSeatV1) + : DisplayM σ Unit := + ω.send do + return 1 + +def RiverXkbBindingsSeatV1.cancelEnsureNextKeyEaten + (ω : RiverXkbBindingsSeatV1) + : DisplayM σ Unit := + ω.send do + return 2 + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverXkbBindingsV1/Resolved.lean b/lib/Wayland/Protocols/RiverXkbBindingsV1/Resolved.lean new file mode 100644 index 0000000..1dfaa00 --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbBindingsV1/Resolved.lean @@ -0,0 +1,38 @@ +import Wayland.Display +import Wayland.Protocols.RiverWindowManagementV1.Interface +import Wayland.Protocols.RiverXkbBindingsV1.Interface +import Wayland.Protocols.Wayland.Interface + +namespace Wayland.Protocols + +instance instResolvedInterfaceRiverXkbBindingsV1 : ResolvedInterface RiverXkbBindingsV1.name where + referencedInterfaces := #[ + ⟨RiverDecorationV1.name, inferInstance⟩, + ⟨RiverNodeV1.name, inferInstance⟩, + ⟨RiverOutputV1.name, inferInstance⟩, + ⟨RiverPointerBindingV1.name, inferInstance⟩, + ⟨RiverSeatV1.name, inferInstance⟩, + ⟨RiverShellSurfaceV1.name, inferInstance⟩, + ⟨RiverWindowV1.name, inferInstance⟩, + ⟨RiverXkbBindingV1.name, inferInstance⟩, + ⟨RiverXkbBindingsSeatV1.name, inferInstance⟩, + ⟨RiverXkbBindingsV1.name, inferInstance⟩, + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverXkbBindingV1 : ResolvedInterface RiverXkbBindingV1.name where + referencedInterfaces := #[ + ⟨RiverXkbBindingV1.name, inferInstance⟩, + ] + +instance instResolvedInterfaceRiverXkbBindingsSeatV1 : ResolvedInterface RiverXkbBindingsSeatV1.name where + referencedInterfaces := #[ + ⟨RiverXkbBindingsSeatV1.name, inferInstance⟩, + ] + + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/RiverXkbConfigV1.lean b/lib/Wayland/Protocols/RiverXkbConfigV1.lean new file mode 100644 index 0000000..264bf7d --- /dev/null +++ b/lib/Wayland/Protocols/RiverXkbConfigV1.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.RiverXkbConfigV1.Header +import Wayland.Protocols.RiverXkbConfigV1.Interface +import Wayland.Protocols.RiverXkbConfigV1.Requests +import Wayland.Protocols.RiverXkbConfigV1.Resolved 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 diff --git a/lib/Wayland/Protocols/Wayland.lean b/lib/Wayland/Protocols/Wayland.lean new file mode 100644 index 0000000..076abba --- /dev/null +++ b/lib/Wayland/Protocols/Wayland.lean @@ -0,0 +1,4 @@ +import Wayland.Protocols.Wayland.Header +import Wayland.Protocols.Wayland.Interface +import Wayland.Protocols.Wayland.Requests +import Wayland.Protocols.Wayland.Resolved diff --git a/lib/Wayland/Protocols/Wayland/Header.lean b/lib/Wayland/Protocols/Wayland/Header.lean new file mode 100644 index 0000000..a12c0bf --- /dev/null +++ b/lib/Wayland/Protocols/Wayland/Header.lean @@ -0,0 +1,1488 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev WlDisplay.name : InterfaceName := "wl_display" +abbrev WlRegistry.name : InterfaceName := "wl_registry" +abbrev WlCallback.name : InterfaceName := "wl_callback" +abbrev WlCompositor.name : InterfaceName := "wl_compositor" +abbrev WlShmPool.name : InterfaceName := "wl_shm_pool" +abbrev WlShm.name : InterfaceName := "wl_shm" +abbrev WlBuffer.name : InterfaceName := "wl_buffer" +abbrev WlDataOffer.name : InterfaceName := "wl_data_offer" +abbrev WlDataSource.name : InterfaceName := "wl_data_source" +abbrev WlDataDevice.name : InterfaceName := "wl_data_device" +abbrev WlDataDeviceManager.name : InterfaceName := "wl_data_device_manager" +abbrev WlShell.name : InterfaceName := "wl_shell" +abbrev WlShellSurface.name : InterfaceName := "wl_shell_surface" +abbrev WlSurface.name : InterfaceName := "wl_surface" +abbrev WlSeat.name : InterfaceName := "wl_seat" +abbrev WlPointer.name : InterfaceName := "wl_pointer" +abbrev WlKeyboard.name : InterfaceName := "wl_keyboard" +abbrev WlTouch.name : InterfaceName := "wl_touch" +abbrev WlOutput.name : InterfaceName := "wl_output" +abbrev WlRegion.name : InterfaceName := "wl_region" +abbrev WlSubcompositor.name : InterfaceName := "wl_subcompositor" +abbrev WlSubsurface.name : InterfaceName := "wl_subsurface" +abbrev WlFixes.name : InterfaceName := "wl_fixes" + +abbrev WlDisplay : Type := Object WlDisplay.name +abbrev WlRegistry : Type := Object WlRegistry.name +abbrev WlCallback : Type := Object WlCallback.name +abbrev WlCompositor : Type := Object WlCompositor.name +abbrev WlShmPool : Type := Object WlShmPool.name +abbrev WlShm : Type := Object WlShm.name +abbrev WlBuffer : Type := Object WlBuffer.name +abbrev WlDataOffer : Type := Object WlDataOffer.name +abbrev WlDataSource : Type := Object WlDataSource.name +abbrev WlDataDevice : Type := Object WlDataDevice.name +abbrev WlDataDeviceManager : Type := Object WlDataDeviceManager.name +abbrev WlShell : Type := Object WlShell.name +abbrev WlShellSurface : Type := Object WlShellSurface.name +abbrev WlSurface : Type := Object WlSurface.name +abbrev WlSeat : Type := Object WlSeat.name +abbrev WlPointer : Type := Object WlPointer.name +abbrev WlKeyboard : Type := Object WlKeyboard.name +abbrev WlTouch : Type := Object WlTouch.name +abbrev WlOutput : Type := Object WlOutput.name +abbrev WlRegion : Type := Object WlRegion.name +abbrev WlSubcompositor : Type := Object WlSubcompositor.name +abbrev WlSubsurface : Type := Object WlSubsurface.name +abbrev WlFixes : Type := Object WlFixes.name + +inductive WlDisplay.Error where + | invalidObject + | invalidMethod + | noMemory + | implementation + +inductive WlShm.Error where + | invalidFormat + | invalidStride + | invalidFd + +inductive WlShm.Format where + | argb8888 + | xrgb8888 + | c8 + | rgb332 + | bgr233 + | xrgb4444 + | xbgr4444 + | rgbx4444 + | bgrx4444 + | argb4444 + | abgr4444 + | rgba4444 + | bgra4444 + | xrgb1555 + | xbgr1555 + | rgbx5551 + | bgrx5551 + | argb1555 + | abgr1555 + | rgba5551 + | bgra5551 + | rgb565 + | bgr565 + | rgb888 + | bgr888 + | xbgr8888 + | rgbx8888 + | bgrx8888 + | abgr8888 + | rgba8888 + | bgra8888 + | xrgb2101010 + | xbgr2101010 + | rgbx1010102 + | bgrx1010102 + | argb2101010 + | abgr2101010 + | rgba1010102 + | bgra1010102 + | yuyv + | yvyu + | uyvy + | vyuy + | ayuv + | nv12 + | nv21 + | nv16 + | nv61 + | yuv410 + | yvu410 + | yuv411 + | yvu411 + | yuv420 + | yvu420 + | yuv422 + | yvu422 + | yuv444 + | yvu444 + | r8 + | r16 + | rg88 + | gr88 + | rg1616 + | gr1616 + | xrgb16161616f + | xbgr16161616f + | argb16161616f + | abgr16161616f + | xyuv8888 + | vuy888 + | vuy101010 + | y210 + | y212 + | y216 + | y410 + | y412 + | y416 + | xvyu2101010 + | xvyu1216161616 + | xvyu16161616 + | y0l0 + | x0l0 + | y0l2 + | x0l2 + | yuv4208bit + | yuv42010bit + | xrgb8888A8 + | xbgr8888A8 + | rgbx8888A8 + | bgrx8888A8 + | rgb888A8 + | bgr888A8 + | rgb565A8 + | bgr565A8 + | nv24 + | nv42 + | p210 + | p010 + | p012 + | p016 + | axbxgxrx106106106106 + | nv15 + | q410 + | q401 + | xrgb16161616 + | xbgr16161616 + | argb16161616 + | abgr16161616 + | c1 + | c2 + | c4 + | d1 + | d2 + | d4 + | d8 + | r1 + | r2 + | r4 + | r10 + | r12 + | avuy8888 + | xvuy8888 + | p030 + +inductive WlDataOffer.Error where + | invalidFinish + | invalidActionMask + | invalidAction + | invalidOffer + +inductive WlDataSource.Error where + | invalidActionMask + | invalidSource + +inductive WlDataDevice.Error where + | role + | usedSource + +structure WlDataDeviceManager.DndAction where + none : Bool + copy : Bool + move : Bool + ask : Bool + +inductive WlShell.Error where + | role + +structure WlShellSurface.Resize where + none : Bool + top : Bool + bottom : Bool + left : Bool + topLeft : Bool + bottomLeft : Bool + right : Bool + topRight : Bool + bottomRight : Bool + +structure WlShellSurface.Transient where + inactive : Bool + +inductive WlShellSurface.FullscreenMethod where + | default + | scale + | driver + | fill + +inductive WlSurface.Error where + | invalidScale + | invalidTransform + | invalidSize + | invalidOffset + | defunctRoleObject + +structure WlSeat.Capability where + pointer : Bool + keyboard : Bool + touch : Bool + +inductive WlSeat.Error where + | missingCapability + +inductive WlPointer.Error where + | role + +inductive WlPointer.ButtonState where + | released + | pressed + +inductive WlPointer.Axis where + | verticalScroll + | horizontalScroll + +inductive WlPointer.AxisSource where + | wheel + | finger + | continuous + | wheelTilt + +inductive WlPointer.AxisRelativeDirection where + | identical + | inverted + +inductive WlKeyboard.KeymapFormat where + | noKeymap + | xkbV1 + +inductive WlKeyboard.KeyState where + | released + | pressed + | repeated + +inductive WlOutput.Subpixel where + | unknown + | none + | horizontalRgb + | horizontalBgr + | verticalRgb + | verticalBgr + +inductive WlOutput.Transform where + | normal + | _90 + | _180 + | _270 + | flipped + | flipped90 + | flipped180 + | flipped270 + +structure WlOutput.Mode where + current : Bool + preferred : Bool + +inductive WlSubcompositor.Error where + | badSurface + | badParent + +inductive WlSubsurface.Error where + | badSurface + +namespace WlDisplay.Error + +instance : Marshallable WlDisplay.Error where + marshal + | .int, .invalidObject => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidObject => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidMethod => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidMethod => ArgumentMarshaller.marshalUInt 1 + | .int, .noMemory => ArgumentMarshaller.marshalInt 2 + | .uint, .noMemory => ArgumentMarshaller.marshalUInt 2 + | .int, .implementation => ArgumentMarshaller.marshalInt 3 + | .uint, .implementation => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidObject + | 1 => pure .invalidMethod + | 2 => pure .noMemory + | 3 => pure .implementation + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidObject + | 1 => pure .invalidMethod + | 2 => pure .noMemory + | 3 => pure .implementation + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlDisplay.Error + +namespace WlShm.Error + +instance : Marshallable WlShm.Error where + marshal + | .int, .invalidFormat => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidFormat => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidStride => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidStride => ArgumentMarshaller.marshalUInt 1 + | .int, .invalidFd => ArgumentMarshaller.marshalInt 2 + | .uint, .invalidFd => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidFormat + | 1 => pure .invalidStride + | 2 => pure .invalidFd + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidFormat + | 1 => pure .invalidStride + | 2 => pure .invalidFd + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlShm.Error + +namespace WlShm.Format + +instance : Marshallable WlShm.Format where + marshal + | .int, .argb8888 => ArgumentMarshaller.marshalInt 0 + | .uint, .argb8888 => ArgumentMarshaller.marshalUInt 0 + | .int, .xrgb8888 => ArgumentMarshaller.marshalInt 1 + | .uint, .xrgb8888 => ArgumentMarshaller.marshalUInt 1 + | .int, .c8 => ArgumentMarshaller.marshalInt 538982467 + | .uint, .c8 => ArgumentMarshaller.marshalUInt 538982467 + | .int, .rgb332 => ArgumentMarshaller.marshalInt 943867730 + | .uint, .rgb332 => ArgumentMarshaller.marshalUInt 943867730 + | .int, .bgr233 => ArgumentMarshaller.marshalInt 944916290 + | .uint, .bgr233 => ArgumentMarshaller.marshalUInt 944916290 + | .int, .xrgb4444 => ArgumentMarshaller.marshalInt 842093144 + | .uint, .xrgb4444 => ArgumentMarshaller.marshalUInt 842093144 + | .int, .xbgr4444 => ArgumentMarshaller.marshalInt 842089048 + | .uint, .xbgr4444 => ArgumentMarshaller.marshalUInt 842089048 + | .int, .rgbx4444 => ArgumentMarshaller.marshalInt 842094674 + | .uint, .rgbx4444 => ArgumentMarshaller.marshalUInt 842094674 + | .int, .bgrx4444 => ArgumentMarshaller.marshalInt 842094658 + | .uint, .bgrx4444 => ArgumentMarshaller.marshalUInt 842094658 + | .int, .argb4444 => ArgumentMarshaller.marshalInt 842093121 + | .uint, .argb4444 => ArgumentMarshaller.marshalUInt 842093121 + | .int, .abgr4444 => ArgumentMarshaller.marshalInt 842089025 + | .uint, .abgr4444 => ArgumentMarshaller.marshalUInt 842089025 + | .int, .rgba4444 => ArgumentMarshaller.marshalInt 842088786 + | .uint, .rgba4444 => ArgumentMarshaller.marshalUInt 842088786 + | .int, .bgra4444 => ArgumentMarshaller.marshalInt 842088770 + | .uint, .bgra4444 => ArgumentMarshaller.marshalUInt 842088770 + | .int, .xrgb1555 => ArgumentMarshaller.marshalInt 892424792 + | .uint, .xrgb1555 => ArgumentMarshaller.marshalUInt 892424792 + | .int, .xbgr1555 => ArgumentMarshaller.marshalInt 892420696 + | .uint, .xbgr1555 => ArgumentMarshaller.marshalUInt 892420696 + | .int, .rgbx5551 => ArgumentMarshaller.marshalInt 892426322 + | .uint, .rgbx5551 => ArgumentMarshaller.marshalUInt 892426322 + | .int, .bgrx5551 => ArgumentMarshaller.marshalInt 892426306 + | .uint, .bgrx5551 => ArgumentMarshaller.marshalUInt 892426306 + | .int, .argb1555 => ArgumentMarshaller.marshalInt 892424769 + | .uint, .argb1555 => ArgumentMarshaller.marshalUInt 892424769 + | .int, .abgr1555 => ArgumentMarshaller.marshalInt 892420673 + | .uint, .abgr1555 => ArgumentMarshaller.marshalUInt 892420673 + | .int, .rgba5551 => ArgumentMarshaller.marshalInt 892420434 + | .uint, .rgba5551 => ArgumentMarshaller.marshalUInt 892420434 + | .int, .bgra5551 => ArgumentMarshaller.marshalInt 892420418 + | .uint, .bgra5551 => ArgumentMarshaller.marshalUInt 892420418 + | .int, .rgb565 => ArgumentMarshaller.marshalInt 909199186 + | .uint, .rgb565 => ArgumentMarshaller.marshalUInt 909199186 + | .int, .bgr565 => ArgumentMarshaller.marshalInt 909199170 + | .uint, .bgr565 => ArgumentMarshaller.marshalUInt 909199170 + | .int, .rgb888 => ArgumentMarshaller.marshalInt 875710290 + | .uint, .rgb888 => ArgumentMarshaller.marshalUInt 875710290 + | .int, .bgr888 => ArgumentMarshaller.marshalInt 875710274 + | .uint, .bgr888 => ArgumentMarshaller.marshalUInt 875710274 + | .int, .xbgr8888 => ArgumentMarshaller.marshalInt 875709016 + | .uint, .xbgr8888 => ArgumentMarshaller.marshalUInt 875709016 + | .int, .rgbx8888 => ArgumentMarshaller.marshalInt 875714642 + | .uint, .rgbx8888 => ArgumentMarshaller.marshalUInt 875714642 + | .int, .bgrx8888 => ArgumentMarshaller.marshalInt 875714626 + | .uint, .bgrx8888 => ArgumentMarshaller.marshalUInt 875714626 + | .int, .abgr8888 => ArgumentMarshaller.marshalInt 875708993 + | .uint, .abgr8888 => ArgumentMarshaller.marshalUInt 875708993 + | .int, .rgba8888 => ArgumentMarshaller.marshalInt 875708754 + | .uint, .rgba8888 => ArgumentMarshaller.marshalUInt 875708754 + | .int, .bgra8888 => ArgumentMarshaller.marshalInt 875708738 + | .uint, .bgra8888 => ArgumentMarshaller.marshalUInt 875708738 + | .int, .xrgb2101010 => ArgumentMarshaller.marshalInt 808669784 + | .uint, .xrgb2101010 => ArgumentMarshaller.marshalUInt 808669784 + | .int, .xbgr2101010 => ArgumentMarshaller.marshalInt 808665688 + | .uint, .xbgr2101010 => ArgumentMarshaller.marshalUInt 808665688 + | .int, .rgbx1010102 => ArgumentMarshaller.marshalInt 808671314 + | .uint, .rgbx1010102 => ArgumentMarshaller.marshalUInt 808671314 + | .int, .bgrx1010102 => ArgumentMarshaller.marshalInt 808671298 + | .uint, .bgrx1010102 => ArgumentMarshaller.marshalUInt 808671298 + | .int, .argb2101010 => ArgumentMarshaller.marshalInt 808669761 + | .uint, .argb2101010 => ArgumentMarshaller.marshalUInt 808669761 + | .int, .abgr2101010 => ArgumentMarshaller.marshalInt 808665665 + | .uint, .abgr2101010 => ArgumentMarshaller.marshalUInt 808665665 + | .int, .rgba1010102 => ArgumentMarshaller.marshalInt 808665426 + | .uint, .rgba1010102 => ArgumentMarshaller.marshalUInt 808665426 + | .int, .bgra1010102 => ArgumentMarshaller.marshalInt 808665410 + | .uint, .bgra1010102 => ArgumentMarshaller.marshalUInt 808665410 + | .int, .yuyv => ArgumentMarshaller.marshalInt 1448695129 + | .uint, .yuyv => ArgumentMarshaller.marshalUInt 1448695129 + | .int, .yvyu => ArgumentMarshaller.marshalInt 1431918169 + | .uint, .yvyu => ArgumentMarshaller.marshalUInt 1431918169 + | .int, .uyvy => ArgumentMarshaller.marshalInt 1498831189 + | .uint, .uyvy => ArgumentMarshaller.marshalUInt 1498831189 + | .int, .vyuy => ArgumentMarshaller.marshalInt 1498765654 + | .uint, .vyuy => ArgumentMarshaller.marshalUInt 1498765654 + | .int, .ayuv => ArgumentMarshaller.marshalInt 1448433985 + | .uint, .ayuv => ArgumentMarshaller.marshalUInt 1448433985 + | .int, .nv12 => ArgumentMarshaller.marshalInt 842094158 + | .uint, .nv12 => ArgumentMarshaller.marshalUInt 842094158 + | .int, .nv21 => ArgumentMarshaller.marshalInt 825382478 + | .uint, .nv21 => ArgumentMarshaller.marshalUInt 825382478 + | .int, .nv16 => ArgumentMarshaller.marshalInt 909203022 + | .uint, .nv16 => ArgumentMarshaller.marshalUInt 909203022 + | .int, .nv61 => ArgumentMarshaller.marshalInt 825644622 + | .uint, .nv61 => ArgumentMarshaller.marshalUInt 825644622 + | .int, .yuv410 => ArgumentMarshaller.marshalInt 961959257 + | .uint, .yuv410 => ArgumentMarshaller.marshalUInt 961959257 + | .int, .yvu410 => ArgumentMarshaller.marshalInt 961893977 + | .uint, .yvu410 => ArgumentMarshaller.marshalUInt 961893977 + | .int, .yuv411 => ArgumentMarshaller.marshalInt 825316697 + | .uint, .yuv411 => ArgumentMarshaller.marshalUInt 825316697 + | .int, .yvu411 => ArgumentMarshaller.marshalInt 825316953 + | .uint, .yvu411 => ArgumentMarshaller.marshalUInt 825316953 + | .int, .yuv420 => ArgumentMarshaller.marshalInt 842093913 + | .uint, .yuv420 => ArgumentMarshaller.marshalUInt 842093913 + | .int, .yvu420 => ArgumentMarshaller.marshalInt 842094169 + | .uint, .yvu420 => ArgumentMarshaller.marshalUInt 842094169 + | .int, .yuv422 => ArgumentMarshaller.marshalInt 909202777 + | .uint, .yuv422 => ArgumentMarshaller.marshalUInt 909202777 + | .int, .yvu422 => ArgumentMarshaller.marshalInt 909203033 + | .uint, .yvu422 => ArgumentMarshaller.marshalUInt 909203033 + | .int, .yuv444 => ArgumentMarshaller.marshalInt 875713881 + | .uint, .yuv444 => ArgumentMarshaller.marshalUInt 875713881 + | .int, .yvu444 => ArgumentMarshaller.marshalInt 875714137 + | .uint, .yvu444 => ArgumentMarshaller.marshalUInt 875714137 + | .int, .r8 => ArgumentMarshaller.marshalInt 538982482 + | .uint, .r8 => ArgumentMarshaller.marshalUInt 538982482 + | .int, .r16 => ArgumentMarshaller.marshalInt 540422482 + | .uint, .r16 => ArgumentMarshaller.marshalUInt 540422482 + | .int, .rg88 => ArgumentMarshaller.marshalInt 943212370 + | .uint, .rg88 => ArgumentMarshaller.marshalUInt 943212370 + | .int, .gr88 => ArgumentMarshaller.marshalInt 943215175 + | .uint, .gr88 => ArgumentMarshaller.marshalUInt 943215175 + | .int, .rg1616 => ArgumentMarshaller.marshalInt 842221394 + | .uint, .rg1616 => ArgumentMarshaller.marshalUInt 842221394 + | .int, .gr1616 => ArgumentMarshaller.marshalInt 842224199 + | .uint, .gr1616 => ArgumentMarshaller.marshalUInt 842224199 + | .int, .xrgb16161616f => ArgumentMarshaller.marshalInt 1211388504 + | .uint, .xrgb16161616f => ArgumentMarshaller.marshalUInt 1211388504 + | .int, .xbgr16161616f => ArgumentMarshaller.marshalInt 1211384408 + | .uint, .xbgr16161616f => ArgumentMarshaller.marshalUInt 1211384408 + | .int, .argb16161616f => ArgumentMarshaller.marshalInt 1211388481 + | .uint, .argb16161616f => ArgumentMarshaller.marshalUInt 1211388481 + | .int, .abgr16161616f => ArgumentMarshaller.marshalInt 1211384385 + | .uint, .abgr16161616f => ArgumentMarshaller.marshalUInt 1211384385 + | .int, .xyuv8888 => ArgumentMarshaller.marshalInt 1448434008 + | .uint, .xyuv8888 => ArgumentMarshaller.marshalUInt 1448434008 + | .int, .vuy888 => ArgumentMarshaller.marshalInt 875713878 + | .uint, .vuy888 => ArgumentMarshaller.marshalUInt 875713878 + | .int, .vuy101010 => ArgumentMarshaller.marshalInt 808670550 + | .uint, .vuy101010 => ArgumentMarshaller.marshalUInt 808670550 + | .int, .y210 => ArgumentMarshaller.marshalInt 808530521 + | .uint, .y210 => ArgumentMarshaller.marshalUInt 808530521 + | .int, .y212 => ArgumentMarshaller.marshalInt 842084953 + | .uint, .y212 => ArgumentMarshaller.marshalUInt 842084953 + | .int, .y216 => ArgumentMarshaller.marshalInt 909193817 + | .uint, .y216 => ArgumentMarshaller.marshalUInt 909193817 + | .int, .y410 => ArgumentMarshaller.marshalInt 808531033 + | .uint, .y410 => ArgumentMarshaller.marshalUInt 808531033 + | .int, .y412 => ArgumentMarshaller.marshalInt 842085465 + | .uint, .y412 => ArgumentMarshaller.marshalUInt 842085465 + | .int, .y416 => ArgumentMarshaller.marshalInt 909194329 + | .uint, .y416 => ArgumentMarshaller.marshalUInt 909194329 + | .int, .xvyu2101010 => ArgumentMarshaller.marshalInt 808670808 + | .uint, .xvyu2101010 => ArgumentMarshaller.marshalUInt 808670808 + | .int, .xvyu1216161616 => ArgumentMarshaller.marshalInt 909334104 + | .uint, .xvyu1216161616 => ArgumentMarshaller.marshalUInt 909334104 + | .int, .xvyu16161616 => ArgumentMarshaller.marshalInt 942954072 + | .uint, .xvyu16161616 => ArgumentMarshaller.marshalUInt 942954072 + | .int, .y0l0 => ArgumentMarshaller.marshalInt 810299481 + | .uint, .y0l0 => ArgumentMarshaller.marshalUInt 810299481 + | .int, .x0l0 => ArgumentMarshaller.marshalInt 810299480 + | .uint, .x0l0 => ArgumentMarshaller.marshalUInt 810299480 + | .int, .y0l2 => ArgumentMarshaller.marshalInt 843853913 + | .uint, .y0l2 => ArgumentMarshaller.marshalUInt 843853913 + | .int, .x0l2 => ArgumentMarshaller.marshalInt 843853912 + | .uint, .x0l2 => ArgumentMarshaller.marshalUInt 843853912 + | .int, .yuv4208bit => ArgumentMarshaller.marshalInt 942691673 + | .uint, .yuv4208bit => ArgumentMarshaller.marshalUInt 942691673 + | .int, .yuv42010bit => ArgumentMarshaller.marshalInt 808539481 + | .uint, .yuv42010bit => ArgumentMarshaller.marshalUInt 808539481 + | .int, .xrgb8888A8 => ArgumentMarshaller.marshalInt 943805016 + | .uint, .xrgb8888A8 => ArgumentMarshaller.marshalUInt 943805016 + | .int, .xbgr8888A8 => ArgumentMarshaller.marshalInt 943800920 + | .uint, .xbgr8888A8 => ArgumentMarshaller.marshalUInt 943800920 + | .int, .rgbx8888A8 => ArgumentMarshaller.marshalInt 943806546 + | .uint, .rgbx8888A8 => ArgumentMarshaller.marshalUInt 943806546 + | .int, .bgrx8888A8 => ArgumentMarshaller.marshalInt 943806530 + | .uint, .bgrx8888A8 => ArgumentMarshaller.marshalUInt 943806530 + | .int, .rgb888A8 => ArgumentMarshaller.marshalInt 943798354 + | .uint, .rgb888A8 => ArgumentMarshaller.marshalUInt 943798354 + | .int, .bgr888A8 => ArgumentMarshaller.marshalInt 943798338 + | .uint, .bgr888A8 => ArgumentMarshaller.marshalUInt 943798338 + | .int, .rgb565A8 => ArgumentMarshaller.marshalInt 943797586 + | .uint, .rgb565A8 => ArgumentMarshaller.marshalUInt 943797586 + | .int, .bgr565A8 => ArgumentMarshaller.marshalInt 943797570 + | .uint, .bgr565A8 => ArgumentMarshaller.marshalUInt 943797570 + | .int, .nv24 => ArgumentMarshaller.marshalInt 875714126 + | .uint, .nv24 => ArgumentMarshaller.marshalUInt 875714126 + | .int, .nv42 => ArgumentMarshaller.marshalInt 842290766 + | .uint, .nv42 => ArgumentMarshaller.marshalUInt 842290766 + | .int, .p210 => ArgumentMarshaller.marshalInt 808530512 + | .uint, .p210 => ArgumentMarshaller.marshalUInt 808530512 + | .int, .p010 => ArgumentMarshaller.marshalInt 808530000 + | .uint, .p010 => ArgumentMarshaller.marshalUInt 808530000 + | .int, .p012 => ArgumentMarshaller.marshalInt 842084432 + | .uint, .p012 => ArgumentMarshaller.marshalUInt 842084432 + | .int, .p016 => ArgumentMarshaller.marshalInt 909193296 + | .uint, .p016 => ArgumentMarshaller.marshalUInt 909193296 + | .int, .axbxgxrx106106106106 => ArgumentMarshaller.marshalInt 808534593 + | .uint, .axbxgxrx106106106106 => ArgumentMarshaller.marshalUInt 808534593 + | .int, .nv15 => ArgumentMarshaller.marshalInt 892425806 + | .uint, .nv15 => ArgumentMarshaller.marshalUInt 892425806 + | .int, .q410 => ArgumentMarshaller.marshalInt 808531025 + | .uint, .q410 => ArgumentMarshaller.marshalUInt 808531025 + | .int, .q401 => ArgumentMarshaller.marshalInt 825242705 + | .uint, .q401 => ArgumentMarshaller.marshalUInt 825242705 + | .int, .xrgb16161616 => ArgumentMarshaller.marshalInt 942953048 + | .uint, .xrgb16161616 => ArgumentMarshaller.marshalUInt 942953048 + | .int, .xbgr16161616 => ArgumentMarshaller.marshalInt 942948952 + | .uint, .xbgr16161616 => ArgumentMarshaller.marshalUInt 942948952 + | .int, .argb16161616 => ArgumentMarshaller.marshalInt 942953025 + | .uint, .argb16161616 => ArgumentMarshaller.marshalUInt 942953025 + | .int, .abgr16161616 => ArgumentMarshaller.marshalInt 942948929 + | .uint, .abgr16161616 => ArgumentMarshaller.marshalUInt 942948929 + | .int, .c1 => ArgumentMarshaller.marshalInt 538980675 + | .uint, .c1 => ArgumentMarshaller.marshalUInt 538980675 + | .int, .c2 => ArgumentMarshaller.marshalInt 538980931 + | .uint, .c2 => ArgumentMarshaller.marshalUInt 538980931 + | .int, .c4 => ArgumentMarshaller.marshalInt 538981443 + | .uint, .c4 => ArgumentMarshaller.marshalUInt 538981443 + | .int, .d1 => ArgumentMarshaller.marshalInt 538980676 + | .uint, .d1 => ArgumentMarshaller.marshalUInt 538980676 + | .int, .d2 => ArgumentMarshaller.marshalInt 538980932 + | .uint, .d2 => ArgumentMarshaller.marshalUInt 538980932 + | .int, .d4 => ArgumentMarshaller.marshalInt 538981444 + | .uint, .d4 => ArgumentMarshaller.marshalUInt 538981444 + | .int, .d8 => ArgumentMarshaller.marshalInt 538982468 + | .uint, .d8 => ArgumentMarshaller.marshalUInt 538982468 + | .int, .r1 => ArgumentMarshaller.marshalInt 538980690 + | .uint, .r1 => ArgumentMarshaller.marshalUInt 538980690 + | .int, .r2 => ArgumentMarshaller.marshalInt 538980946 + | .uint, .r2 => ArgumentMarshaller.marshalUInt 538980946 + | .int, .r4 => ArgumentMarshaller.marshalInt 538981458 + | .uint, .r4 => ArgumentMarshaller.marshalUInt 538981458 + | .int, .r10 => ArgumentMarshaller.marshalInt 540029266 + | .uint, .r10 => ArgumentMarshaller.marshalUInt 540029266 + | .int, .r12 => ArgumentMarshaller.marshalInt 540160338 + | .uint, .r12 => ArgumentMarshaller.marshalUInt 540160338 + | .int, .avuy8888 => ArgumentMarshaller.marshalInt 1498764865 + | .uint, .avuy8888 => ArgumentMarshaller.marshalUInt 1498764865 + | .int, .xvuy8888 => ArgumentMarshaller.marshalInt 1498764888 + | .uint, .xvuy8888 => ArgumentMarshaller.marshalUInt 1498764888 + | .int, .p030 => ArgumentMarshaller.marshalInt 808661072 + | .uint, .p030 => ArgumentMarshaller.marshalUInt 808661072 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .argb8888 + | 1 => pure .xrgb8888 + | 538982467 => pure .c8 + | 943867730 => pure .rgb332 + | 944916290 => pure .bgr233 + | 842093144 => pure .xrgb4444 + | 842089048 => pure .xbgr4444 + | 842094674 => pure .rgbx4444 + | 842094658 => pure .bgrx4444 + | 842093121 => pure .argb4444 + | 842089025 => pure .abgr4444 + | 842088786 => pure .rgba4444 + | 842088770 => pure .bgra4444 + | 892424792 => pure .xrgb1555 + | 892420696 => pure .xbgr1555 + | 892426322 => pure .rgbx5551 + | 892426306 => pure .bgrx5551 + | 892424769 => pure .argb1555 + | 892420673 => pure .abgr1555 + | 892420434 => pure .rgba5551 + | 892420418 => pure .bgra5551 + | 909199186 => pure .rgb565 + | 909199170 => pure .bgr565 + | 875710290 => pure .rgb888 + | 875710274 => pure .bgr888 + | 875709016 => pure .xbgr8888 + | 875714642 => pure .rgbx8888 + | 875714626 => pure .bgrx8888 + | 875708993 => pure .abgr8888 + | 875708754 => pure .rgba8888 + | 875708738 => pure .bgra8888 + | 808669784 => pure .xrgb2101010 + | 808665688 => pure .xbgr2101010 + | 808671314 => pure .rgbx1010102 + | 808671298 => pure .bgrx1010102 + | 808669761 => pure .argb2101010 + | 808665665 => pure .abgr2101010 + | 808665426 => pure .rgba1010102 + | 808665410 => pure .bgra1010102 + | 1448695129 => pure .yuyv + | 1431918169 => pure .yvyu + | 1498831189 => pure .uyvy + | 1498765654 => pure .vyuy + | 1448433985 => pure .ayuv + | 842094158 => pure .nv12 + | 825382478 => pure .nv21 + | 909203022 => pure .nv16 + | 825644622 => pure .nv61 + | 961959257 => pure .yuv410 + | 961893977 => pure .yvu410 + | 825316697 => pure .yuv411 + | 825316953 => pure .yvu411 + | 842093913 => pure .yuv420 + | 842094169 => pure .yvu420 + | 909202777 => pure .yuv422 + | 909203033 => pure .yvu422 + | 875713881 => pure .yuv444 + | 875714137 => pure .yvu444 + | 538982482 => pure .r8 + | 540422482 => pure .r16 + | 943212370 => pure .rg88 + | 943215175 => pure .gr88 + | 842221394 => pure .rg1616 + | 842224199 => pure .gr1616 + | 1211388504 => pure .xrgb16161616f + | 1211384408 => pure .xbgr16161616f + | 1211388481 => pure .argb16161616f + | 1211384385 => pure .abgr16161616f + | 1448434008 => pure .xyuv8888 + | 875713878 => pure .vuy888 + | 808670550 => pure .vuy101010 + | 808530521 => pure .y210 + | 842084953 => pure .y212 + | 909193817 => pure .y216 + | 808531033 => pure .y410 + | 842085465 => pure .y412 + | 909194329 => pure .y416 + | 808670808 => pure .xvyu2101010 + | 909334104 => pure .xvyu1216161616 + | 942954072 => pure .xvyu16161616 + | 810299481 => pure .y0l0 + | 810299480 => pure .x0l0 + | 843853913 => pure .y0l2 + | 843853912 => pure .x0l2 + | 942691673 => pure .yuv4208bit + | 808539481 => pure .yuv42010bit + | 943805016 => pure .xrgb8888A8 + | 943800920 => pure .xbgr8888A8 + | 943806546 => pure .rgbx8888A8 + | 943806530 => pure .bgrx8888A8 + | 943798354 => pure .rgb888A8 + | 943798338 => pure .bgr888A8 + | 943797586 => pure .rgb565A8 + | 943797570 => pure .bgr565A8 + | 875714126 => pure .nv24 + | 842290766 => pure .nv42 + | 808530512 => pure .p210 + | 808530000 => pure .p010 + | 842084432 => pure .p012 + | 909193296 => pure .p016 + | 808534593 => pure .axbxgxrx106106106106 + | 892425806 => pure .nv15 + | 808531025 => pure .q410 + | 825242705 => pure .q401 + | 942953048 => pure .xrgb16161616 + | 942948952 => pure .xbgr16161616 + | 942953025 => pure .argb16161616 + | 942948929 => pure .abgr16161616 + | 538980675 => pure .c1 + | 538980931 => pure .c2 + | 538981443 => pure .c4 + | 538980676 => pure .d1 + | 538980932 => pure .d2 + | 538981444 => pure .d4 + | 538982468 => pure .d8 + | 538980690 => pure .r1 + | 538980946 => pure .r2 + | 538981458 => pure .r4 + | 540029266 => pure .r10 + | 540160338 => pure .r12 + | 1498764865 => pure .avuy8888 + | 1498764888 => pure .xvuy8888 + | 808661072 => pure .p030 + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .argb8888 + | 1 => pure .xrgb8888 + | 538982467 => pure .c8 + | 943867730 => pure .rgb332 + | 944916290 => pure .bgr233 + | 842093144 => pure .xrgb4444 + | 842089048 => pure .xbgr4444 + | 842094674 => pure .rgbx4444 + | 842094658 => pure .bgrx4444 + | 842093121 => pure .argb4444 + | 842089025 => pure .abgr4444 + | 842088786 => pure .rgba4444 + | 842088770 => pure .bgra4444 + | 892424792 => pure .xrgb1555 + | 892420696 => pure .xbgr1555 + | 892426322 => pure .rgbx5551 + | 892426306 => pure .bgrx5551 + | 892424769 => pure .argb1555 + | 892420673 => pure .abgr1555 + | 892420434 => pure .rgba5551 + | 892420418 => pure .bgra5551 + | 909199186 => pure .rgb565 + | 909199170 => pure .bgr565 + | 875710290 => pure .rgb888 + | 875710274 => pure .bgr888 + | 875709016 => pure .xbgr8888 + | 875714642 => pure .rgbx8888 + | 875714626 => pure .bgrx8888 + | 875708993 => pure .abgr8888 + | 875708754 => pure .rgba8888 + | 875708738 => pure .bgra8888 + | 808669784 => pure .xrgb2101010 + | 808665688 => pure .xbgr2101010 + | 808671314 => pure .rgbx1010102 + | 808671298 => pure .bgrx1010102 + | 808669761 => pure .argb2101010 + | 808665665 => pure .abgr2101010 + | 808665426 => pure .rgba1010102 + | 808665410 => pure .bgra1010102 + | 1448695129 => pure .yuyv + | 1431918169 => pure .yvyu + | 1498831189 => pure .uyvy + | 1498765654 => pure .vyuy + | 1448433985 => pure .ayuv + | 842094158 => pure .nv12 + | 825382478 => pure .nv21 + | 909203022 => pure .nv16 + | 825644622 => pure .nv61 + | 961959257 => pure .yuv410 + | 961893977 => pure .yvu410 + | 825316697 => pure .yuv411 + | 825316953 => pure .yvu411 + | 842093913 => pure .yuv420 + | 842094169 => pure .yvu420 + | 909202777 => pure .yuv422 + | 909203033 => pure .yvu422 + | 875713881 => pure .yuv444 + | 875714137 => pure .yvu444 + | 538982482 => pure .r8 + | 540422482 => pure .r16 + | 943212370 => pure .rg88 + | 943215175 => pure .gr88 + | 842221394 => pure .rg1616 + | 842224199 => pure .gr1616 + | 1211388504 => pure .xrgb16161616f + | 1211384408 => pure .xbgr16161616f + | 1211388481 => pure .argb16161616f + | 1211384385 => pure .abgr16161616f + | 1448434008 => pure .xyuv8888 + | 875713878 => pure .vuy888 + | 808670550 => pure .vuy101010 + | 808530521 => pure .y210 + | 842084953 => pure .y212 + | 909193817 => pure .y216 + | 808531033 => pure .y410 + | 842085465 => pure .y412 + | 909194329 => pure .y416 + | 808670808 => pure .xvyu2101010 + | 909334104 => pure .xvyu1216161616 + | 942954072 => pure .xvyu16161616 + | 810299481 => pure .y0l0 + | 810299480 => pure .x0l0 + | 843853913 => pure .y0l2 + | 843853912 => pure .x0l2 + | 942691673 => pure .yuv4208bit + | 808539481 => pure .yuv42010bit + | 943805016 => pure .xrgb8888A8 + | 943800920 => pure .xbgr8888A8 + | 943806546 => pure .rgbx8888A8 + | 943806530 => pure .bgrx8888A8 + | 943798354 => pure .rgb888A8 + | 943798338 => pure .bgr888A8 + | 943797586 => pure .rgb565A8 + | 943797570 => pure .bgr565A8 + | 875714126 => pure .nv24 + | 842290766 => pure .nv42 + | 808530512 => pure .p210 + | 808530000 => pure .p010 + | 842084432 => pure .p012 + | 909193296 => pure .p016 + | 808534593 => pure .axbxgxrx106106106106 + | 892425806 => pure .nv15 + | 808531025 => pure .q410 + | 825242705 => pure .q401 + | 942953048 => pure .xrgb16161616 + | 942948952 => pure .xbgr16161616 + | 942953025 => pure .argb16161616 + | 942948929 => pure .abgr16161616 + | 538980675 => pure .c1 + | 538980931 => pure .c2 + | 538981443 => pure .c4 + | 538980676 => pure .d1 + | 538980932 => pure .d2 + | 538981444 => pure .d4 + | 538982468 => pure .d8 + | 538980690 => pure .r1 + | 538980946 => pure .r2 + | 538981458 => pure .r4 + | 540029266 => pure .r10 + | 540160338 => pure .r12 + | 1498764865 => pure .avuy8888 + | 1498764888 => pure .xvuy8888 + | 808661072 => pure .p030 + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlShm.Format + +namespace WlDataOffer.Error + +instance : Marshallable WlDataOffer.Error where + marshal + | .int, .invalidFinish => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidFinish => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidActionMask => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidActionMask => ArgumentMarshaller.marshalUInt 1 + | .int, .invalidAction => ArgumentMarshaller.marshalInt 2 + | .uint, .invalidAction => ArgumentMarshaller.marshalUInt 2 + | .int, .invalidOffer => ArgumentMarshaller.marshalInt 3 + | .uint, .invalidOffer => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidFinish + | 1 => pure .invalidActionMask + | 2 => pure .invalidAction + | 3 => pure .invalidOffer + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidFinish + | 1 => pure .invalidActionMask + | 2 => pure .invalidAction + | 3 => pure .invalidOffer + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlDataOffer.Error + +namespace WlDataSource.Error + +instance : Marshallable WlDataSource.Error where + marshal + | .int, .invalidActionMask => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidActionMask => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidSource => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidSource => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidActionMask + | 1 => pure .invalidSource + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidActionMask + | 1 => pure .invalidSource + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlDataSource.Error + +namespace WlDataDevice.Error + +instance : Marshallable WlDataDevice.Error where + marshal + | .int, .role => ArgumentMarshaller.marshalInt 0 + | .uint, .role => ArgumentMarshaller.marshalUInt 0 + | .int, .usedSource => ArgumentMarshaller.marshalInt 1 + | .uint, .usedSource => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .role + | 1 => pure .usedSource + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .role + | 1 => pure .usedSource + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlDataDevice.Error + +namespace WlDataDeviceManager.DndAction + +instance : Marshallable WlDataDeviceManager.DndAction where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.copy then 1 else 0) + ||| (if μ.move then 2 else 0) + ||| (if μ.ask then 4 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + copy := (μ &&& 1) == 1 + move := (μ &&& 2) == 2 + ask := (μ &&& 4) == 4 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end WlDataDeviceManager.DndAction + +namespace WlShell.Error + +instance : Marshallable WlShell.Error where + marshal + | .int, .role => ArgumentMarshaller.marshalInt 0 + | .uint, .role => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .role + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .role + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlShell.Error + +namespace WlShellSurface.Resize + +instance : Marshallable WlShellSurface.Resize where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.none then 0 else 0) + ||| (if μ.top then 1 else 0) + ||| (if μ.bottom then 2 else 0) + ||| (if μ.left then 4 else 0) + ||| (if μ.topLeft then 5 else 0) + ||| (if μ.bottomLeft then 6 else 0) + ||| (if μ.right then 8 else 0) + ||| (if μ.topRight then 9 else 0) + ||| (if μ.bottomRight then 10 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + none := (μ &&& 0) == 0 + top := (μ &&& 1) == 1 + bottom := (μ &&& 2) == 2 + left := (μ &&& 4) == 4 + topLeft := (μ &&& 5) == 5 + bottomLeft := (μ &&& 6) == 6 + right := (μ &&& 8) == 8 + topRight := (μ &&& 9) == 9 + bottomRight := (μ &&& 10) == 10 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end WlShellSurface.Resize + +namespace WlShellSurface.Transient + +instance : Marshallable WlShellSurface.Transient where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.inactive then 1 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + inactive := (μ &&& 1) == 1 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end WlShellSurface.Transient + +namespace WlShellSurface.FullscreenMethod + +instance : Marshallable WlShellSurface.FullscreenMethod where + marshal + | .int, .default => ArgumentMarshaller.marshalInt 0 + | .uint, .default => ArgumentMarshaller.marshalUInt 0 + | .int, .scale => ArgumentMarshaller.marshalInt 1 + | .uint, .scale => ArgumentMarshaller.marshalUInt 1 + | .int, .driver => ArgumentMarshaller.marshalInt 2 + | .uint, .driver => ArgumentMarshaller.marshalUInt 2 + | .int, .fill => ArgumentMarshaller.marshalInt 3 + | .uint, .fill => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .default + | 1 => pure .scale + | 2 => pure .driver + | 3 => pure .fill + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .default + | 1 => pure .scale + | 2 => pure .driver + | 3 => pure .fill + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlShellSurface.FullscreenMethod + +namespace WlSurface.Error + +instance : Marshallable WlSurface.Error where + marshal + | .int, .invalidScale => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidScale => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidTransform => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidTransform => ArgumentMarshaller.marshalUInt 1 + | .int, .invalidSize => ArgumentMarshaller.marshalInt 2 + | .uint, .invalidSize => ArgumentMarshaller.marshalUInt 2 + | .int, .invalidOffset => ArgumentMarshaller.marshalInt 3 + | .uint, .invalidOffset => ArgumentMarshaller.marshalUInt 3 + | .int, .defunctRoleObject => ArgumentMarshaller.marshalInt 4 + | .uint, .defunctRoleObject => ArgumentMarshaller.marshalUInt 4 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidScale + | 1 => pure .invalidTransform + | 2 => pure .invalidSize + | 3 => pure .invalidOffset + | 4 => pure .defunctRoleObject + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidScale + | 1 => pure .invalidTransform + | 2 => pure .invalidSize + | 3 => pure .invalidOffset + | 4 => pure .defunctRoleObject + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlSurface.Error + +namespace WlSeat.Capability + +instance : Marshallable WlSeat.Capability where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.pointer then 1 else 0) + ||| (if μ.keyboard then 2 else 0) + ||| (if μ.touch then 4 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + pointer := (μ &&& 1) == 1 + keyboard := (μ &&& 2) == 2 + touch := (μ &&& 4) == 4 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end WlSeat.Capability + +namespace WlSeat.Error + +instance : Marshallable WlSeat.Error where + marshal + | .int, .missingCapability => ArgumentMarshaller.marshalInt 0 + | .uint, .missingCapability => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .missingCapability + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .missingCapability + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlSeat.Error + +namespace WlPointer.Error + +instance : Marshallable WlPointer.Error where + marshal + | .int, .role => ArgumentMarshaller.marshalInt 0 + | .uint, .role => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .role + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .role + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlPointer.Error + +namespace WlPointer.ButtonState + +instance : Marshallable WlPointer.ButtonState where + marshal + | .int, .released => ArgumentMarshaller.marshalInt 0 + | .uint, .released => ArgumentMarshaller.marshalUInt 0 + | .int, .pressed => ArgumentMarshaller.marshalInt 1 + | .uint, .pressed => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .released + | 1 => pure .pressed + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .released + | 1 => pure .pressed + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlPointer.ButtonState + +namespace WlPointer.Axis + +instance : Marshallable WlPointer.Axis where + marshal + | .int, .verticalScroll => ArgumentMarshaller.marshalInt 0 + | .uint, .verticalScroll => ArgumentMarshaller.marshalUInt 0 + | .int, .horizontalScroll => ArgumentMarshaller.marshalInt 1 + | .uint, .horizontalScroll => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .verticalScroll + | 1 => pure .horizontalScroll + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .verticalScroll + | 1 => pure .horizontalScroll + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlPointer.Axis + +namespace WlPointer.AxisSource + +instance : Marshallable WlPointer.AxisSource where + marshal + | .int, .wheel => ArgumentMarshaller.marshalInt 0 + | .uint, .wheel => ArgumentMarshaller.marshalUInt 0 + | .int, .finger => ArgumentMarshaller.marshalInt 1 + | .uint, .finger => ArgumentMarshaller.marshalUInt 1 + | .int, .continuous => ArgumentMarshaller.marshalInt 2 + | .uint, .continuous => ArgumentMarshaller.marshalUInt 2 + | .int, .wheelTilt => ArgumentMarshaller.marshalInt 3 + | .uint, .wheelTilt => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .wheel + | 1 => pure .finger + | 2 => pure .continuous + | 3 => pure .wheelTilt + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .wheel + | 1 => pure .finger + | 2 => pure .continuous + | 3 => pure .wheelTilt + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlPointer.AxisSource + +namespace WlPointer.AxisRelativeDirection + +instance : Marshallable WlPointer.AxisRelativeDirection where + marshal + | .int, .identical => ArgumentMarshaller.marshalInt 0 + | .uint, .identical => ArgumentMarshaller.marshalUInt 0 + | .int, .inverted => ArgumentMarshaller.marshalInt 1 + | .uint, .inverted => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .identical + | 1 => pure .inverted + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .identical + | 1 => pure .inverted + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlPointer.AxisRelativeDirection + +namespace WlKeyboard.KeymapFormat + +instance : Marshallable WlKeyboard.KeymapFormat where + marshal + | .int, .noKeymap => ArgumentMarshaller.marshalInt 0 + | .uint, .noKeymap => ArgumentMarshaller.marshalUInt 0 + | .int, .xkbV1 => ArgumentMarshaller.marshalInt 1 + | .uint, .xkbV1 => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .noKeymap + | 1 => pure .xkbV1 + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .noKeymap + | 1 => pure .xkbV1 + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlKeyboard.KeymapFormat + +namespace WlKeyboard.KeyState + +instance : Marshallable WlKeyboard.KeyState where + marshal + | .int, .released => ArgumentMarshaller.marshalInt 0 + | .uint, .released => ArgumentMarshaller.marshalUInt 0 + | .int, .pressed => ArgumentMarshaller.marshalInt 1 + | .uint, .pressed => ArgumentMarshaller.marshalUInt 1 + | .int, .repeated => ArgumentMarshaller.marshalInt 2 + | .uint, .repeated => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .released + | 1 => pure .pressed + | 2 => pure .repeated + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .released + | 1 => pure .pressed + | 2 => pure .repeated + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlKeyboard.KeyState + +namespace WlOutput.Subpixel + +instance : Marshallable WlOutput.Subpixel where + marshal + | .int, .unknown => ArgumentMarshaller.marshalInt 0 + | .uint, .unknown => ArgumentMarshaller.marshalUInt 0 + | .int, .none => ArgumentMarshaller.marshalInt 1 + | .uint, .none => ArgumentMarshaller.marshalUInt 1 + | .int, .horizontalRgb => ArgumentMarshaller.marshalInt 2 + | .uint, .horizontalRgb => ArgumentMarshaller.marshalUInt 2 + | .int, .horizontalBgr => ArgumentMarshaller.marshalInt 3 + | .uint, .horizontalBgr => ArgumentMarshaller.marshalUInt 3 + | .int, .verticalRgb => ArgumentMarshaller.marshalInt 4 + | .uint, .verticalRgb => ArgumentMarshaller.marshalUInt 4 + | .int, .verticalBgr => ArgumentMarshaller.marshalInt 5 + | .uint, .verticalBgr => ArgumentMarshaller.marshalUInt 5 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .unknown + | 1 => pure .none + | 2 => pure .horizontalRgb + | 3 => pure .horizontalBgr + | 4 => pure .verticalRgb + | 5 => pure .verticalBgr + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .unknown + | 1 => pure .none + | 2 => pure .horizontalRgb + | 3 => pure .horizontalBgr + | 4 => pure .verticalRgb + | 5 => pure .verticalBgr + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlOutput.Subpixel + +namespace WlOutput.Transform + +instance : Marshallable WlOutput.Transform where + marshal + | .int, .normal => ArgumentMarshaller.marshalInt 0 + | .uint, .normal => ArgumentMarshaller.marshalUInt 0 + | .int, ._90 => ArgumentMarshaller.marshalInt 1 + | .uint, ._90 => ArgumentMarshaller.marshalUInt 1 + | .int, ._180 => ArgumentMarshaller.marshalInt 2 + | .uint, ._180 => ArgumentMarshaller.marshalUInt 2 + | .int, ._270 => ArgumentMarshaller.marshalInt 3 + | .uint, ._270 => ArgumentMarshaller.marshalUInt 3 + | .int, .flipped => ArgumentMarshaller.marshalInt 4 + | .uint, .flipped => ArgumentMarshaller.marshalUInt 4 + | .int, .flipped90 => ArgumentMarshaller.marshalInt 5 + | .uint, .flipped90 => ArgumentMarshaller.marshalUInt 5 + | .int, .flipped180 => ArgumentMarshaller.marshalInt 6 + | .uint, .flipped180 => ArgumentMarshaller.marshalUInt 6 + | .int, .flipped270 => ArgumentMarshaller.marshalInt 7 + | .uint, .flipped270 => ArgumentMarshaller.marshalUInt 7 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .normal + | 1 => pure ._90 + | 2 => pure ._180 + | 3 => pure ._270 + | 4 => pure .flipped + | 5 => pure .flipped90 + | 6 => pure .flipped180 + | 7 => pure .flipped270 + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .normal + | 1 => pure ._90 + | 2 => pure ._180 + | 3 => pure ._270 + | 4 => pure .flipped + | 5 => pure .flipped90 + | 6 => pure .flipped180 + | 7 => pure .flipped270 + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlOutput.Transform + +namespace WlOutput.Mode + +instance : Marshallable WlOutput.Mode where + marshal + | .uint, μ => ArgumentMarshaller.marshalUInt <| + 0 + ||| (if μ.current then 1 else 0) + ||| (if μ.preferred then 2 else 0) + | _, _ => throw "Marshalling unexpected type, expected uint." + demarshal + | .uint => do + let μ ← ArgumentDemarshaller.demarshalUInt + return { + current := (μ &&& 1) == 1 + preferred := (μ &&& 2) == 2 + } + | _ => throw "Demarshalling unexpected type, expected uint." + +end WlOutput.Mode + +namespace WlSubcompositor.Error + +instance : Marshallable WlSubcompositor.Error where + marshal + | .int, .badSurface => ArgumentMarshaller.marshalInt 0 + | .uint, .badSurface => ArgumentMarshaller.marshalUInt 0 + | .int, .badParent => ArgumentMarshaller.marshalInt 1 + | .uint, .badParent => ArgumentMarshaller.marshalUInt 1 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .badSurface + | 1 => pure .badParent + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .badSurface + | 1 => pure .badParent + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlSubcompositor.Error + +namespace WlSubsurface.Error + +instance : Marshallable WlSubsurface.Error where + marshal + | .int, .badSurface => ArgumentMarshaller.marshalInt 0 + | .uint, .badSurface => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .badSurface + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .badSurface + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end WlSubsurface.Error + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/Wayland/Interface.lean b/lib/Wayland/Protocols/Wayland/Interface.lean new file mode 100644 index 0000000..b91b44f --- /dev/null +++ b/lib/Wayland/Protocols/Wayland/Interface.lean @@ -0,0 +1,1468 @@ +import Wayland.Display +import Wayland.Protocols.Wayland.Header + +namespace Wayland.Protocols + +inductive WlDisplay.Event where + | error + (objectId : AnyObject) + (code : UInt32) + (message : String) + | deleteId + (id : UInt32) + +inductive WlRegistry.Event where + | global + (name : UInt32) + (interface : String) + (version : UInt32) + | globalRemove + (name : UInt32) + +inductive WlCallback.Event where + | done + (callbackData : UInt32) + +inductive WlCompositor.Event where + +inductive WlShmPool.Event where + +inductive WlShm.Event where + | format + (format : WlShm.Format) + +inductive WlBuffer.Event where + | release + +inductive WlDataOffer.Event where + | offer + (mimeType : String) + | sourceActions + (sourceActions : WlDataDeviceManager.DndAction) + | action + (dndAction : WlDataDeviceManager.DndAction) + +inductive WlDataSource.Event where + | target + (mimeType : Option String) + | send + (mimeType : String) + (fd : Fd) + | cancelled + | dndDropPerformed + | dndFinished + | action + (dndAction : WlDataDeviceManager.DndAction) + +inductive WlDataDevice.Event where + | dataOffer + (id : WlDataOffer) + | enter + (serial : UInt32) + (surface : WlSurface) + (x : Float32) + (y : Float32) + (id : Option WlDataOffer) + | leave + | motion + (time : UInt32) + (x : Float32) + (y : Float32) + | drop + | selection + (id : Option WlDataOffer) + +inductive WlDataDeviceManager.Event where + +inductive WlShell.Event where + +inductive WlShellSurface.Event where + | ping + (serial : UInt32) + | configure + (edges : WlShellSurface.Resize) + (width : Int32) + (height : Int32) + | popupDone + +inductive WlSurface.Event where + | enter + (output : WlOutput) + | leave + (output : WlOutput) + | preferredBufferScale + (factor : Int32) + | preferredBufferTransform + (transform : WlOutput.Transform) + +inductive WlSeat.Event where + | capabilities + (capabilities : WlSeat.Capability) + | name + (name : String) + +inductive WlPointer.Event where + | enter + (serial : UInt32) + (surface : WlSurface) + (surfaceX : Float32) + (surfaceY : Float32) + | leave + (serial : UInt32) + (surface : WlSurface) + | motion + (time : UInt32) + (surfaceX : Float32) + (surfaceY : Float32) + | button + (serial : UInt32) + (time : UInt32) + (button : UInt32) + (state : WlPointer.ButtonState) + | axis + (time : UInt32) + (axis : WlPointer.Axis) + (value : Float32) + | frame + | axisSource + (axisSource : WlPointer.AxisSource) + | axisStop + (time : UInt32) + (axis : WlPointer.Axis) + | axisDiscrete + (axis : WlPointer.Axis) + (discrete : Int32) + | axisValue120 + (axis : WlPointer.Axis) + (value120 : Int32) + | axisRelativeDirection + (axis : WlPointer.Axis) + (direction : WlPointer.AxisRelativeDirection) + +inductive WlKeyboard.Event where + | keymap + (format : WlKeyboard.KeymapFormat) + (fd : Fd) + (size : UInt32) + | enter + (serial : UInt32) + (surface : WlSurface) + (keys : ByteArray) + | leave + (serial : UInt32) + (surface : WlSurface) + | key + (serial : UInt32) + (time : UInt32) + (key : UInt32) + (state : WlKeyboard.KeyState) + | modifiers + (serial : UInt32) + (modsDepressed : UInt32) + (modsLatched : UInt32) + (modsLocked : UInt32) + (group : UInt32) + | repeatInfo + (rate : Int32) + (delay : Int32) + +inductive WlTouch.Event where + | down + (serial : UInt32) + (time : UInt32) + (surface : WlSurface) + (id : Int32) + (x : Float32) + (y : Float32) + | up + (serial : UInt32) + (time : UInt32) + (id : Int32) + | motion + (time : UInt32) + (id : Int32) + (x : Float32) + (y : Float32) + | frame + | cancel + | shape + (id : Int32) + (major : Float32) + (minor : Float32) + | orientation + (id : Int32) + (orientation : Float32) + +inductive WlOutput.Event where + | geometry + (x : Int32) + (y : Int32) + (physicalWidth : Int32) + (physicalHeight : Int32) + (subpixel : WlOutput.Subpixel) + (make : String) + (model : String) + (transform : WlOutput.Transform) + | mode + (flags : WlOutput.Mode) + (width : Int32) + (height : Int32) + (refresh : Int32) + | done + | scale + (factor : Int32) + | name + (name : String) + | description + (description : String) + +inductive WlRegion.Event where + +inductive WlSubcompositor.Event where + +inductive WlSubsurface.Event where + +inductive WlFixes.Event where + + +instance instInterfaceWlDisplay : Interface WlDisplay.name where + event := WlDisplay.Event + version := 1 + requests := #[ + { + name := "sync" + args := #[.newID (.some "wl_callback")] + since := 1 + isDestructor := false + }, + { + name := "get_registry" + args := #[.newID (.some "wl_registry")] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "error" + args := #[.object .notNull .none, .uint, .string .notNull] + since := 1 + isDestructor := false + }, + { + name := "delete_id" + args := #[.uint] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .error + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .string) + | 1 => do + return .deleteId + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlRegistry : Interface WlRegistry.name where + event := WlRegistry.Event + version := 1 + requests := #[ + { + name := "bind" + args := #[.uint, .string .notNull, .uint, .newID .none] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "global" + args := #[.uint, .string .notNull, .uint] + since := 1 + isDestructor := false + }, + { + name := "global_remove" + args := #[.uint] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .global + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .string) + (← Marshallable.demarshal .uint) + | 1 => do + return .globalRemove + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlCallback : Interface WlCallback.name where + event := WlCallback.Event + version := 1 + requests := #[ + ] + events := #[ + { + name := "done" + args := #[.uint] + since := 1 + isDestructor := true + }, + ] + demarshalEvent + | 0 => do + return .done + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlCompositor : Interface WlCompositor.name where + event := WlCompositor.Event + version := 6 + requests := #[ + { + name := "create_surface" + args := #[.newID (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "create_region" + args := #[.newID (.some "wl_region")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlShmPool : Interface WlShmPool.name where + event := WlShmPool.Event + version := 2 + requests := #[ + { + name := "create_buffer" + args := #[.newID (.some "wl_buffer"), .int, .int, .int, .int, .uint] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "resize" + args := #[.int] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlShm : Interface WlShm.name where + event := WlShm.Event + version := 2 + requests := #[ + { + name := "create_pool" + args := #[.newID (.some "wl_shm_pool"), .fd, .int] + since := 1 + isDestructor := false + }, + { + name := "release" + args := #[] + since := 2 + isDestructor := true + }, + ] + events := #[ + { + name := "format" + args := #[.uint] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .format + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlBuffer : Interface WlBuffer.name where + event := WlBuffer.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + ] + events := #[ + { + name := "release" + args := #[] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .release + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlDataOffer : Interface WlDataOffer.name where + event := WlDataOffer.Event + version := 3 + requests := #[ + { + name := "accept" + args := #[.uint, .string .nullable] + since := 1 + isDestructor := false + }, + { + name := "receive" + args := #[.string .notNull, .fd] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "finish" + args := #[] + since := 3 + isDestructor := false + }, + { + name := "set_actions" + args := #[.uint, .uint] + since := 3 + isDestructor := false + }, + ] + events := #[ + { + name := "offer" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + { + name := "source_actions" + args := #[.uint] + since := 3 + isDestructor := false + }, + { + name := "action" + args := #[.uint] + since := 3 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .offer + (← Marshallable.demarshal .string) + | 1 => do + return .sourceActions + (← Marshallable.demarshal .uint) + | 2 => do + return .action + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlDataSource : Interface WlDataSource.name where + event := WlDataSource.Event + version := 3 + requests := #[ + { + name := "offer" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_actions" + args := #[.uint] + since := 3 + isDestructor := false + }, + ] + events := #[ + { + name := "target" + args := #[.string .nullable] + since := 1 + isDestructor := false + }, + { + name := "send" + args := #[.string .notNull, .fd] + since := 1 + isDestructor := false + }, + { + name := "cancelled" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "dnd_drop_performed" + args := #[] + since := 3 + isDestructor := false + }, + { + name := "dnd_finished" + args := #[] + since := 3 + isDestructor := false + }, + { + name := "action" + args := #[.uint] + since := 3 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .target + (← Marshallable.demarshal .string) + | 1 => do + return .send + (← Marshallable.demarshal .string) + (← Marshallable.demarshal .fd) + | 2 => do + return .cancelled + | 3 => do + return .dndDropPerformed + | 4 => do + return .dndFinished + | 5 => do + return .action + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlDataDevice : Interface WlDataDevice.name where + event := WlDataDevice.Event + version := 3 + requests := #[ + { + name := "start_drag" + args := #[.object .nullable (.some "wl_data_source"), .object .notNull (.some "wl_surface"), .object .nullable (.some "wl_surface"), .uint] + since := 1 + isDestructor := false + }, + { + name := "set_selection" + args := #[.object .nullable (.some "wl_data_source"), .uint] + since := 1 + isDestructor := false + }, + { + name := "release" + args := #[] + since := 2 + isDestructor := true + }, + ] + events := #[ + { + name := "data_offer" + args := #[.newID (.some "wl_data_offer")] + since := 1 + isDestructor := false + }, + { + name := "enter" + args := #[.uint, .object .notNull (.some "wl_surface"), .fixed, .fixed, .object .nullable (.some "wl_data_offer")] + since := 1 + isDestructor := false + }, + { + name := "leave" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "motion" + args := #[.uint, .fixed, .fixed] + since := 1 + isDestructor := false + }, + { + name := "drop" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "selection" + args := #[.object .nullable (.some "wl_data_offer")] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .dataOffer + (← Marshallable.demarshal .object) + | 1 => do + return .enter + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .object) + | 2 => do + return .leave + | 3 => do + return .motion + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 4 => do + return .drop + | 5 => do + return .selection + (← Marshallable.demarshal .object) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlDataDeviceManager : Interface WlDataDeviceManager.name where + event := WlDataDeviceManager.Event + version := 3 + requests := #[ + { + name := "create_data_source" + args := #[.newID (.some "wl_data_source")] + since := 1 + isDestructor := false + }, + { + name := "get_data_device" + args := #[.newID (.some "wl_data_device"), .object .notNull (.some "wl_seat")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlShell : Interface WlShell.name where + event := WlShell.Event + version := 1 + requests := #[ + { + name := "get_shell_surface" + args := #[.newID (.some "wl_shell_surface"), .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlShellSurface : Interface WlShellSurface.name where + event := WlShellSurface.Event + version := 1 + requests := #[ + { + name := "pong" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "move" + args := #[.object .notNull (.some "wl_seat"), .uint] + since := 1 + isDestructor := false + }, + { + name := "resize" + args := #[.object .notNull (.some "wl_seat"), .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "set_toplevel" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_transient" + args := #[.object .notNull (.some "wl_surface"), .int, .int, .uint] + since := 1 + isDestructor := false + }, + { + name := "set_fullscreen" + args := #[.uint, .uint, .object .nullable (.some "wl_output")] + since := 1 + isDestructor := false + }, + { + name := "set_popup" + args := #[.object .notNull (.some "wl_seat"), .uint, .object .notNull (.some "wl_surface"), .int, .int, .uint] + since := 1 + isDestructor := false + }, + { + name := "set_maximized" + args := #[.object .nullable (.some "wl_output")] + since := 1 + isDestructor := false + }, + { + name := "set_title" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + { + name := "set_class" + args := #[.string .notNull] + since := 1 + isDestructor := false + }, + ] + events := #[ + { + name := "ping" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "configure" + args := #[.uint, .int, .int] + since := 1 + isDestructor := false + }, + { + name := "popup_done" + args := #[] + since := 1 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .ping + (← Marshallable.demarshal .uint) + | 1 => do + return .configure + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 2 => do + return .popupDone + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlSurface : Interface WlSurface.name where + event := WlSurface.Event + version := 6 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "attach" + args := #[.object .nullable (.some "wl_buffer"), .int, .int] + since := 1 + isDestructor := false + }, + { + name := "damage" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + { + name := "frame" + args := #[.newID (.some "wl_callback")] + since := 1 + isDestructor := false + }, + { + name := "set_opaque_region" + args := #[.object .nullable (.some "wl_region")] + since := 1 + isDestructor := false + }, + { + name := "set_input_region" + args := #[.object .nullable (.some "wl_region")] + since := 1 + isDestructor := false + }, + { + name := "commit" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_buffer_transform" + args := #[.int] + since := 2 + isDestructor := false + }, + { + name := "set_buffer_scale" + args := #[.int] + since := 3 + isDestructor := false + }, + { + name := "damage_buffer" + args := #[.int, .int, .int, .int] + since := 4 + isDestructor := false + }, + { + name := "offset" + args := #[.int, .int] + since := 5 + isDestructor := false + }, + ] + events := #[ + { + name := "enter" + args := #[.object .notNull (.some "wl_output")] + since := 1 + isDestructor := false + }, + { + name := "leave" + args := #[.object .notNull (.some "wl_output")] + since := 1 + isDestructor := false + }, + { + name := "preferred_buffer_scale" + args := #[.int] + since := 6 + isDestructor := false + }, + { + name := "preferred_buffer_transform" + args := #[.uint] + since := 6 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .enter + (← Marshallable.demarshal .object) + | 1 => do + return .leave + (← Marshallable.demarshal .object) + | 2 => do + return .preferredBufferScale + (← Marshallable.demarshal .int) + | 3 => do + return .preferredBufferTransform + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlSeat : Interface WlSeat.name where + event := WlSeat.Event + version := 10 + requests := #[ + { + name := "get_pointer" + args := #[.newID (.some "wl_pointer")] + since := 1 + isDestructor := false + }, + { + name := "get_keyboard" + args := #[.newID (.some "wl_keyboard")] + since := 1 + isDestructor := false + }, + { + name := "get_touch" + args := #[.newID (.some "wl_touch")] + since := 1 + isDestructor := false + }, + { + name := "release" + args := #[] + since := 5 + isDestructor := true + }, + ] + events := #[ + { + name := "capabilities" + args := #[.uint] + since := 1 + isDestructor := false + }, + { + name := "name" + args := #[.string .notNull] + since := 2 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .capabilities + (← Marshallable.demarshal .uint) + | 1 => do + return .name + (← Marshallable.demarshal .string) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlPointer : Interface WlPointer.name where + event := WlPointer.Event + version := 10 + requests := #[ + { + name := "set_cursor" + args := #[.uint, .object .nullable (.some "wl_surface"), .int, .int] + since := 1 + isDestructor := false + }, + { + name := "release" + args := #[] + since := 3 + isDestructor := true + }, + ] + events := #[ + { + name := "enter" + args := #[.uint, .object .notNull (.some "wl_surface"), .fixed, .fixed] + since := 1 + isDestructor := false + }, + { + name := "leave" + args := #[.uint, .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "motion" + args := #[.uint, .fixed, .fixed] + since := 1 + isDestructor := false + }, + { + name := "button" + args := #[.uint, .uint, .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "axis" + args := #[.uint, .uint, .fixed] + since := 1 + isDestructor := false + }, + { + name := "frame" + args := #[] + since := 5 + isDestructor := false + }, + { + name := "axis_source" + args := #[.uint] + since := 5 + isDestructor := false + }, + { + name := "axis_stop" + args := #[.uint, .uint] + since := 5 + isDestructor := false + }, + { + name := "axis_discrete" + args := #[.uint, .int] + since := 5 + isDestructor := false + }, + { + name := "axis_value120" + args := #[.uint, .int] + since := 8 + isDestructor := false + }, + { + name := "axis_relative_direction" + args := #[.uint, .uint] + since := 9 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .enter + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 1 => do + return .leave + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + | 2 => do + return .motion + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 3 => do + return .button + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + | 4 => do + return .axis + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .fixed) + | 5 => do + return .frame + | 6 => do + return .axisSource + (← Marshallable.demarshal .uint) + | 7 => do + return .axisStop + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + | 8 => do + return .axisDiscrete + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + | 9 => do + return .axisValue120 + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + | 10 => do + return .axisRelativeDirection + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlKeyboard : Interface WlKeyboard.name where + event := WlKeyboard.Event + version := 10 + requests := #[ + { + name := "release" + args := #[] + since := 3 + isDestructor := true + }, + ] + events := #[ + { + name := "keymap" + args := #[.uint, .fd, .uint] + since := 1 + isDestructor := false + }, + { + name := "enter" + args := #[.uint, .object .notNull (.some "wl_surface"), .array] + since := 1 + isDestructor := false + }, + { + name := "leave" + args := #[.uint, .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "key" + args := #[.uint, .uint, .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "modifiers" + args := #[.uint, .uint, .uint, .uint, .uint] + since := 1 + isDestructor := false + }, + { + name := "repeat_info" + args := #[.int, .int] + since := 4 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .keymap + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .fd) + (← Marshallable.demarshal .uint) + | 1 => do + return .enter + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .array) + | 2 => do + return .leave + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + | 3 => do + return .key + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + | 4 => do + return .modifiers + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + | 5 => do + return .repeatInfo + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlTouch : Interface WlTouch.name where + event := WlTouch.Event + version := 10 + requests := #[ + { + name := "release" + args := #[] + since := 3 + isDestructor := true + }, + ] + events := #[ + { + name := "down" + args := #[.uint, .uint, .object .notNull (.some "wl_surface"), .int, .fixed, .fixed] + since := 1 + isDestructor := false + }, + { + name := "up" + args := #[.uint, .uint, .int] + since := 1 + isDestructor := false + }, + { + name := "motion" + args := #[.uint, .int, .fixed, .fixed] + since := 1 + isDestructor := false + }, + { + name := "frame" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "cancel" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "shape" + args := #[.int, .fixed, .fixed] + since := 6 + isDestructor := false + }, + { + name := "orientation" + args := #[.int, .fixed] + since := 6 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .down + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .object) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 1 => do + return .up + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + | 2 => do + return .motion + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 3 => do + return .frame + | 4 => do + return .cancel + | 5 => do + return .shape + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .fixed) + (← Marshallable.demarshal .fixed) + | 6 => do + return .orientation + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .fixed) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlOutput : Interface WlOutput.name where + event := WlOutput.Event + version := 4 + requests := #[ + { + name := "release" + args := #[] + since := 3 + isDestructor := true + }, + ] + events := #[ + { + name := "geometry" + args := #[.int, .int, .int, .int, .int, .string .notNull, .string .notNull, .int] + since := 1 + isDestructor := false + }, + { + name := "mode" + args := #[.uint, .int, .int, .int] + since := 1 + isDestructor := false + }, + { + name := "done" + args := #[] + since := 2 + isDestructor := false + }, + { + name := "scale" + args := #[.int] + since := 2 + isDestructor := false + }, + { + name := "name" + args := #[.string .notNull] + since := 4 + isDestructor := false + }, + { + name := "description" + args := #[.string .notNull] + since := 4 + isDestructor := false + }, + ] + demarshalEvent + | 0 => do + return .geometry + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .string) + (← Marshallable.demarshal .string) + (← Marshallable.demarshal .int) + | 1 => do + return .mode + (← Marshallable.demarshal .uint) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + (← Marshallable.demarshal .int) + | 2 => do + return .done + | 3 => do + return .scale + (← Marshallable.demarshal .int) + | 4 => do + return .name + (← Marshallable.demarshal .string) + | 5 => do + return .description + (← Marshallable.demarshal .string) + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlRegion : Interface WlRegion.name where + event := WlRegion.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "add" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + { + name := "subtract" + args := #[.int, .int, .int, .int] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlSubcompositor : Interface WlSubcompositor.name where + event := WlSubcompositor.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "get_subsurface" + args := #[.newID (.some "wl_subsurface"), .object .notNull (.some "wl_surface"), .object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlSubsurface : Interface WlSubsurface.name where + event := WlSubsurface.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "set_position" + args := #[.int, .int] + since := 1 + isDestructor := false + }, + { + name := "place_above" + args := #[.object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "place_below" + args := #[.object .notNull (.some "wl_surface")] + since := 1 + isDestructor := false + }, + { + name := "set_sync" + args := #[] + since := 1 + isDestructor := false + }, + { + name := "set_desync" + args := #[] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +instance instInterfaceWlFixes : Interface WlFixes.name where + event := WlFixes.Event + version := 1 + requests := #[ + { + name := "destroy" + args := #[] + since := 1 + isDestructor := true + }, + { + name := "destroy_registry" + args := #[.object .notNull (.some "wl_registry")] + since := 1 + isDestructor := false + }, + ] + events := #[ + ] + demarshalEvent + | _ => throw s!"Received invalid opcode" + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/Wayland/Requests.lean b/lib/Wayland/Protocols/Wayland/Requests.lean new file mode 100644 index 0000000..2e275dd --- /dev/null +++ b/lib/Wayland/Protocols/Wayland/Requests.lean @@ -0,0 +1,616 @@ +import Wayland.Display +import Wayland.Protocols.Wayland.Header +import Wayland.Protocols.Wayland.Resolved + +namespace Wayland.Protocols + +variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι] + +def WlDisplay.sync.raw + (ω : WlDisplay) + : DisplayM σ WlCallback := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 0 + +def WlDisplay.sync + (ω : WlDisplay) + (γ : DisplayM σ Unit) + : DisplayM σ Unit := do + let ρ ← WlDisplay.sync.raw ω + ρ.listen fun + | .done _ => do ρ.keep; γ + +def WlDisplay.getRegistry + (ω : WlDisplay) + : DisplayM σ WlRegistry := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 1 + +def WlRegistry.bind + (ω : WlRegistry) + (name : UInt32) + : DisplayM σ (Object ι) := + ω.sendConstructor do + Marshallable.marshal .uint name + ArgumentMarshaller.marshalString (.some ι) + ArgumentMarshaller.marshalUInt (inferInstanceAs (Interface ι)).version + ArgumentMarshaller.marshalAnyObject .none + return 0 + +def WlCompositor.createSurface + (ω : WlCompositor) + : DisplayM σ WlSurface := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 0 + +def WlCompositor.createRegion + (ω : WlCompositor) + : DisplayM σ WlRegion := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 1 + +def WlShmPool.createBuffer + (ω : WlShmPool) + (offset : Int32) + (width : Int32) + (height : Int32) + (stride : Int32) + (format : WlShm.Format) + : DisplayM σ WlBuffer := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .int offset + Marshallable.marshal .int width + Marshallable.marshal .int height + Marshallable.marshal .int stride + Marshallable.marshal .uint format + return 0 + +def WlShmPool.destroy + (ω : WlShmPool) + : DisplayM σ Unit := + ω.send do + return 1 + +def WlShmPool.resize + (ω : WlShmPool) + (size : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int size + return 2 + +def WlShm.createPool + (ω : WlShm) + (fd : Fd) + (size : Int32) + : DisplayM σ WlShmPool := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .fd fd + Marshallable.marshal .int size + return 0 + +def WlShm.release + (ω : WlShm) + : DisplayM σ Unit := + ω.send do + return 1 + +def WlBuffer.destroy + (ω : WlBuffer) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlDataOffer.accept + (ω : WlDataOffer) + (serial : UInt32) + (mimeType : Option String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint serial + Marshallable.marshal .string mimeType + return 0 + +def WlDataOffer.receive + (ω : WlDataOffer) + (mimeType : String) + (fd : Fd) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string mimeType + Marshallable.marshal .fd fd + return 1 + +def WlDataOffer.destroy + (ω : WlDataOffer) + : DisplayM σ Unit := + ω.send do + return 2 + +def WlDataOffer.finish + (ω : WlDataOffer) + : DisplayM σ Unit := + ω.send do + return 3 + +def WlDataOffer.setActions + (ω : WlDataOffer) + (dndActions : WlDataDeviceManager.DndAction) + (preferredAction : WlDataDeviceManager.DndAction) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint dndActions + Marshallable.marshal .uint preferredAction + return 4 + +def WlDataSource.offer + (ω : WlDataSource) + (mimeType : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string mimeType + return 0 + +def WlDataSource.destroy + (ω : WlDataSource) + : DisplayM σ Unit := + ω.send do + return 1 + +def WlDataSource.setActions + (ω : WlDataSource) + (dndActions : WlDataDeviceManager.DndAction) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint dndActions + return 2 + +def WlDataDevice.startDrag + (ω : WlDataDevice) + (source : Option WlDataSource) + (origin : WlSurface) + (icon : Option WlSurface) + (serial : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object source + Marshallable.marshal .object origin + Marshallable.marshal .object icon + Marshallable.marshal .uint serial + return 0 + +def WlDataDevice.setSelection + (ω : WlDataDevice) + (source : Option WlDataSource) + (serial : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object source + Marshallable.marshal .uint serial + return 1 + +def WlDataDevice.release + (ω : WlDataDevice) + : DisplayM σ Unit := + ω.send do + return 2 + +def WlDataDeviceManager.createDataSource + (ω : WlDataDeviceManager) + : DisplayM σ WlDataSource := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 0 + +def WlDataDeviceManager.getDataDevice + (ω : WlDataDeviceManager) + (seat : WlSeat) + : DisplayM σ WlDataDevice := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object seat + return 1 + +def WlShell.getShellSurface + (ω : WlShell) + (surface : WlSurface) + : DisplayM σ WlShellSurface := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + return 0 + +def WlShellSurface.pong + (ω : WlShellSurface) + (serial : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint serial + return 0 + +def WlShellSurface.move + (ω : WlShellSurface) + (seat : WlSeat) + (serial : UInt32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object seat + Marshallable.marshal .uint serial + return 1 + +def WlShellSurface.resize + (ω : WlShellSurface) + (seat : WlSeat) + (serial : UInt32) + (edges : WlShellSurface.Resize) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object seat + Marshallable.marshal .uint serial + Marshallable.marshal .uint edges + return 2 + +def WlShellSurface.setToplevel + (ω : WlShellSurface) + : DisplayM σ Unit := + ω.send do + return 3 + +def WlShellSurface.setTransient + (ω : WlShellSurface) + (parent : WlSurface) + (x : Int32) + (y : Int32) + (flags : WlShellSurface.Transient) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object parent + Marshallable.marshal .int x + Marshallable.marshal .int y + Marshallable.marshal .uint flags + return 4 + +def WlShellSurface.setFullscreen + (ω : WlShellSurface) + (method : WlShellSurface.FullscreenMethod) + (framerate : UInt32) + (output : Option WlOutput) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint method + Marshallable.marshal .uint framerate + Marshallable.marshal .object output + return 5 + +def WlShellSurface.setPopup + (ω : WlShellSurface) + (seat : WlSeat) + (serial : UInt32) + (parent : WlSurface) + (x : Int32) + (y : Int32) + (flags : WlShellSurface.Transient) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object seat + Marshallable.marshal .uint serial + Marshallable.marshal .object parent + Marshallable.marshal .int x + Marshallable.marshal .int y + Marshallable.marshal .uint flags + return 6 + +def WlShellSurface.setMaximized + (ω : WlShellSurface) + (output : Option WlOutput) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object output + return 7 + +def WlShellSurface.setTitle + (ω : WlShellSurface) + (title : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string title + return 8 + +def WlShellSurface.setClass + (ω : WlShellSurface) + (_class : String) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .string _class + return 9 + +def WlSurface.destroy + (ω : WlSurface) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlSurface.attach + (ω : WlSurface) + (buffer : Option WlBuffer) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object buffer + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def WlSurface.damage + (ω : WlSurface) + (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 2 + +def WlSurface.frame.raw + (ω : WlSurface) + : DisplayM σ WlCallback := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 3 + +def WlSurface.frame + (ω : WlSurface) + (γ : DisplayM σ Unit) + : DisplayM σ Unit := do + let ρ ← WlSurface.frame.raw ω + ρ.listen fun + | .done _ => do ρ.keep; γ + +def WlSurface.setOpaqueRegion + (ω : WlSurface) + (region : Option WlRegion) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object region + return 4 + +def WlSurface.setInputRegion + (ω : WlSurface) + (region : Option WlRegion) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object region + return 5 + +def WlSurface.commit + (ω : WlSurface) + : DisplayM σ Unit := + ω.send do + return 6 + +def WlSurface.setBufferTransform + (ω : WlSurface) + (transform : WlOutput.Transform) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int transform + return 7 + +def WlSurface.setBufferScale + (ω : WlSurface) + (scale : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int scale + return 8 + +def WlSurface.damageBuffer + (ω : WlSurface) + (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 9 + +def WlSurface.offset + (ω : WlSurface) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 10 + +def WlSeat.getPointer + (ω : WlSeat) + : DisplayM σ WlPointer := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 0 + +def WlSeat.getKeyboard + (ω : WlSeat) + : DisplayM σ WlKeyboard := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 1 + +def WlSeat.getTouch + (ω : WlSeat) + : DisplayM σ WlTouch := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + return 2 + +def WlSeat.release + (ω : WlSeat) + : DisplayM σ Unit := + ω.send do + return 3 + +def WlPointer.setCursor + (ω : WlPointer) + (serial : UInt32) + (surface : Option WlSurface) + (hotspotX : Int32) + (hotspotY : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .uint serial + Marshallable.marshal .object surface + Marshallable.marshal .int hotspotX + Marshallable.marshal .int hotspotY + return 0 + +def WlPointer.release + (ω : WlPointer) + : DisplayM σ Unit := + ω.send do + return 1 + +def WlKeyboard.release + (ω : WlKeyboard) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlTouch.release + (ω : WlTouch) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlOutput.release + (ω : WlOutput) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlRegion.destroy + (ω : WlRegion) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlRegion.add + (ω : WlRegion) + (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 1 + +def WlRegion.subtract + (ω : WlRegion) + (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 2 + +def WlSubcompositor.destroy + (ω : WlSubcompositor) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlSubcompositor.getSubsurface + (ω : WlSubcompositor) + (surface : WlSurface) + (parent : WlSurface) + : DisplayM σ WlSubsurface := + ω.sendConstructor do + ArgumentMarshaller.marshalAnyObject .none + Marshallable.marshal .object surface + Marshallable.marshal .object parent + return 1 + +def WlSubsurface.destroy + (ω : WlSubsurface) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlSubsurface.setPosition + (ω : WlSubsurface) + (x : Int32) + (y : Int32) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .int x + Marshallable.marshal .int y + return 1 + +def WlSubsurface.placeAbove + (ω : WlSubsurface) + (sibling : WlSurface) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object sibling + return 2 + +def WlSubsurface.placeBelow + (ω : WlSubsurface) + (sibling : WlSurface) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object sibling + return 3 + +def WlSubsurface.setSync + (ω : WlSubsurface) + : DisplayM σ Unit := + ω.send do + return 4 + +def WlSubsurface.setDesync + (ω : WlSubsurface) + : DisplayM σ Unit := + ω.send do + return 5 + +def WlFixes.destroy + (ω : WlFixes) + : DisplayM σ Unit := + ω.send do + return 0 + +def WlFixes.destroyRegistry + (ω : WlFixes) + (registry : WlRegistry) + : DisplayM σ Unit := + ω.send do + Marshallable.marshal .object registry + return 1 + +end Wayland.Protocols
\ No newline at end of file diff --git a/lib/Wayland/Protocols/Wayland/Resolved.lean b/lib/Wayland/Protocols/Wayland/Resolved.lean new file mode 100644 index 0000000..5de40f6 --- /dev/null +++ b/lib/Wayland/Protocols/Wayland/Resolved.lean @@ -0,0 +1,209 @@ +import Wayland.Display +import Wayland.Protocols.Wayland.Interface + +namespace Wayland.Protocols + +instance instResolvedInterfaceWlDisplay : ResolvedInterface WlDisplay.name where + referencedInterfaces := #[ + ⟨WlCallback.name, inferInstance⟩, + ⟨WlDisplay.name, inferInstance⟩, + ⟨WlRegistry.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlRegistry : ResolvedInterface WlRegistry.name where + referencedInterfaces := #[ + ⟨WlRegistry.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlCallback : ResolvedInterface WlCallback.name where + referencedInterfaces := #[ + ⟨WlCallback.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlCompositor : ResolvedInterface WlCompositor.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlCompositor.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlShmPool : ResolvedInterface WlShmPool.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlShmPool.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlShm : ResolvedInterface WlShm.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlShm.name, inferInstance⟩, + ⟨WlShmPool.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlBuffer : ResolvedInterface WlBuffer.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlDataOffer : ResolvedInterface WlDataOffer.name where + referencedInterfaces := #[ + ⟨WlDataOffer.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlDataSource : ResolvedInterface WlDataSource.name where + referencedInterfaces := #[ + ⟨WlDataSource.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlDataDevice : ResolvedInterface WlDataDevice.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlDataDevice.name, inferInstance⟩, + ⟨WlDataOffer.name, inferInstance⟩, + ⟨WlDataSource.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlDataDeviceManager : ResolvedInterface WlDataDeviceManager.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlDataDevice.name, inferInstance⟩, + ⟨WlDataDeviceManager.name, inferInstance⟩, + ⟨WlDataOffer.name, inferInstance⟩, + ⟨WlDataSource.name, inferInstance⟩, + ⟨WlKeyboard.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlPointer.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSeat.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ⟨WlTouch.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlShell : ResolvedInterface WlShell.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlKeyboard.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlPointer.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSeat.name, inferInstance⟩, + ⟨WlShell.name, inferInstance⟩, + ⟨WlShellSurface.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ⟨WlTouch.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlShellSurface : ResolvedInterface WlShellSurface.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlKeyboard.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlPointer.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSeat.name, inferInstance⟩, + ⟨WlShellSurface.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ⟨WlTouch.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlSurface : ResolvedInterface WlSurface.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlSeat : ResolvedInterface WlSeat.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlKeyboard.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlPointer.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSeat.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ⟨WlTouch.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlPointer : ResolvedInterface WlPointer.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlPointer.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlKeyboard : ResolvedInterface WlKeyboard.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlKeyboard.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlTouch : ResolvedInterface WlTouch.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ⟨WlTouch.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlOutput : ResolvedInterface WlOutput.name where + referencedInterfaces := #[ + ⟨WlOutput.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlRegion : ResolvedInterface WlRegion.name where + referencedInterfaces := #[ + ⟨WlRegion.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlSubcompositor : ResolvedInterface WlSubcompositor.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSubcompositor.name, inferInstance⟩, + ⟨WlSubsurface.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlSubsurface : ResolvedInterface WlSubsurface.name where + referencedInterfaces := #[ + ⟨WlBuffer.name, inferInstance⟩, + ⟨WlCallback.name, inferInstance⟩, + ⟨WlOutput.name, inferInstance⟩, + ⟨WlRegion.name, inferInstance⟩, + ⟨WlSubsurface.name, inferInstance⟩, + ⟨WlSurface.name, inferInstance⟩, + ] + +instance instResolvedInterfaceWlFixes : ResolvedInterface WlFixes.name where + referencedInterfaces := #[ + ⟨WlFixes.name, inferInstance⟩, + ⟨WlRegistry.name, inferInstance⟩, + ] + + +end Wayland.Protocols
\ No newline at end of file |