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