diff options
Diffstat (limited to 'lib/Wayland/Protocols/RiverInputManagementV1/Header.lean')
| -rw-r--r-- | lib/Wayland/Protocols/RiverInputManagementV1/Header.lean | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean b/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean new file mode 100644 index 0000000..66e881f --- /dev/null +++ b/lib/Wayland/Protocols/RiverInputManagementV1/Header.lean @@ -0,0 +1,105 @@ +import Wayland.Display + +namespace Wayland.Protocols + +abbrev RiverInputManagerV1.name : InterfaceName := "river_input_manager_v1" +abbrev RiverInputDeviceV1.name : InterfaceName := "river_input_device_v1" + +abbrev RiverInputManagerV1 : Type := Object RiverInputManagerV1.name +abbrev RiverInputDeviceV1 : Type := Object RiverInputDeviceV1.name + +inductive RiverInputManagerV1.Error where + | invalidDestroy + +inductive RiverInputDeviceV1.Error where + | invalidRepeatInfo + | invalidScrollFactor + | invalidMapToRectangle + +inductive RiverInputDeviceV1.Type where + | keyboard + | pointer + | touch + | tablet + +namespace RiverInputManagerV1.Error + +instance : Marshallable RiverInputManagerV1.Error where + marshal + | .int, .invalidDestroy => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidDestroy => ArgumentMarshaller.marshalUInt 0 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidDestroy + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidDestroy + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverInputManagerV1.Error + +namespace RiverInputDeviceV1.Error + +instance : Marshallable RiverInputDeviceV1.Error where + marshal + | .int, .invalidRepeatInfo => ArgumentMarshaller.marshalInt 0 + | .uint, .invalidRepeatInfo => ArgumentMarshaller.marshalUInt 0 + | .int, .invalidScrollFactor => ArgumentMarshaller.marshalInt 1 + | .uint, .invalidScrollFactor => ArgumentMarshaller.marshalUInt 1 + | .int, .invalidMapToRectangle => ArgumentMarshaller.marshalInt 2 + | .uint, .invalidMapToRectangle => ArgumentMarshaller.marshalUInt 2 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .invalidRepeatInfo + | 1 => pure .invalidScrollFactor + | 2 => pure .invalidMapToRectangle + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .invalidRepeatInfo + | 1 => pure .invalidScrollFactor + | 2 => pure .invalidMapToRectangle + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverInputDeviceV1.Error + +namespace RiverInputDeviceV1.Type + +instance : Marshallable RiverInputDeviceV1.Type where + marshal + | .int, .keyboard => ArgumentMarshaller.marshalInt 0 + | .uint, .keyboard => ArgumentMarshaller.marshalUInt 0 + | .int, .pointer => ArgumentMarshaller.marshalInt 1 + | .uint, .pointer => ArgumentMarshaller.marshalUInt 1 + | .int, .touch => ArgumentMarshaller.marshalInt 2 + | .uint, .touch => ArgumentMarshaller.marshalUInt 2 + | .int, .tablet => ArgumentMarshaller.marshalInt 3 + | .uint, .tablet => ArgumentMarshaller.marshalUInt 3 + | _, _ => throw "Marshalling unexpected type, expected int or uint." + demarshal + | .int => do + match (← ArgumentDemarshaller.demarshalInt) with + | 0 => pure .keyboard + | 1 => pure .pointer + | 2 => pure .touch + | 3 => pure .tablet + | _ => throw "Invalid enum value." + | .uint => do + match (← ArgumentDemarshaller.demarshalUInt) with + | 0 => pure .keyboard + | 1 => pure .pointer + | 2 => pure .touch + | 3 => pure .tablet + | _ => throw "Invalid enum value." + | _ => throw "Demarshalling unexpected type, expected int or uint." + +end RiverInputDeviceV1.Type + +end Wayland.Protocols
\ No newline at end of file |