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