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/RiverWindowManagementV1/Header.lean | 336 +++++++++++++++++++++ 1 file changed, 336 insertions(+) create mode 100644 lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean (limited to 'lib/Wayland/Protocols/RiverWindowManagementV1/Header.lean') 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 -- cgit v1.3.1