From 80317994ba8a8b7f72c0bf0d824e4ade59a4b6c8 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 9 Apr 2026 23:07:23 +0200 Subject: fix build on linux --- .../Protocols/RiverInputManagementV1/Header.lean | 105 +++++++++++++++ .../RiverInputManagementV1/Interface.lean | 142 +++++++++++++++++++++ .../Protocols/RiverInputManagementV1/Requests.lean | 91 +++++++++++++ .../Protocols/RiverInputManagementV1/Resolved.lean | 21 +++ 4 files changed, 359 insertions(+) create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Header.lean create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Interface.lean create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Requests.lean create mode 100644 lib/Wayland/Protocols/RiverInputManagementV1/Resolved.lean (limited to 'lib/Wayland/Protocols/RiverInputManagementV1') 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 -- cgit v1.3.1