import Wayland.Display
import Wayland.Protocols.RiverLayerShellV1.Header

namespace Wayland.Protocols

inductive RiverLayerShellV1.Event where

inductive RiverLayerShellOutputV1.Event where
  | nonExclusiveArea
    (x : Int32)
    (y : Int32)
    (width : Int32)
    (height : Int32)

inductive RiverLayerShellSeatV1.Event where
  | focusExclusive
  | focusNonExclusive
  | focusNone


instance instInterfaceRiverLayerShellV1 : Interface RiverLayerShellV1.name where
  event := RiverLayerShellV1.Event
  version := 1
  requests := #[
    {
      name := "destroy"
      args := #[]
      since := 1
      isDestructor := true
    },
    {
      name := "get_output"
      args := #[.newID (.some "river_layer_shell_output_v1"), .object .notNull (.some "river_output_v1")]
      since := 1
      isDestructor := false
    },
    {
      name := "get_seat"
      args := #[.newID (.some "river_layer_shell_seat_v1"), .object .notNull (.some "river_seat_v1")]
      since := 1
      isDestructor := false
    },
  ]
  events := #[
  ]
  demarshalEvent
    | _ => throw s!"Received invalid opcode"

instance instInterfaceRiverLayerShellOutputV1 : Interface RiverLayerShellOutputV1.name where
  event := RiverLayerShellOutputV1.Event
  version := 1
  requests := #[
    {
      name := "destroy"
      args := #[]
      since := 1
      isDestructor := true
    },
    {
      name := "set_default"
      args := #[]
      since := 1
      isDestructor := false
    },
  ]
  events := #[
    {
      name := "non_exclusive_area"
      args := #[.int, .int, .int, .int]
      since := 1
      isDestructor := false
    },
  ]
  demarshalEvent
    | 0 => do
      return .nonExclusiveArea
        (← Marshallable.demarshal .int)
        (← Marshallable.demarshal .int)
        (← Marshallable.demarshal .int)
        (← Marshallable.demarshal .int)
    | _ => throw s!"Received invalid opcode"

instance instInterfaceRiverLayerShellSeatV1 : Interface RiverLayerShellSeatV1.name where
  event := RiverLayerShellSeatV1.Event
  version := 1
  requests := #[
    {
      name := "destroy"
      args := #[]
      since := 1
      isDestructor := true
    },
  ]
  events := #[
    {
      name := "focus_exclusive"
      args := #[]
      since := 1
      isDestructor := false
    },
    {
      name := "focus_non_exclusive"
      args := #[]
      since := 1
      isDestructor := false
    },
    {
      name := "focus_none"
      args := #[]
      since := 1
      isDestructor := false
    },
  ]
  demarshalEvent
    | 0 => do
      return .focusExclusive
    | 1 => do
      return .focusNonExclusive
    | 2 => do
      return .focusNone
    | _ => throw s!"Received invalid opcode"

end Wayland.Protocols