diff options
Diffstat (limited to 'lib/Wayland/Protocols/RiverXkbBindingsV1')
4 files changed, 294 insertions, 0 deletions
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 |