import Wayland.Display

namespace Wayland.Protocols

abbrev RiverLayerShellV1.name : InterfaceName := "river_layer_shell_v1"
abbrev RiverLayerShellOutputV1.name : InterfaceName := "river_layer_shell_output_v1"
abbrev RiverLayerShellSeatV1.name : InterfaceName := "river_layer_shell_seat_v1"

abbrev RiverLayerShellV1 : Type := Object RiverLayerShellV1.name
abbrev RiverLayerShellOutputV1 : Type := Object RiverLayerShellOutputV1.name
abbrev RiverLayerShellSeatV1 : Type := Object RiverLayerShellSeatV1.name

inductive RiverLayerShellV1.Error where
  | objectAlreadyCreated

namespace RiverLayerShellV1.Error

instance : Marshallable RiverLayerShellV1.Error where
  marshal
    | .int,  .objectAlreadyCreated => ArgumentMarshaller.marshalInt 0
    | .uint, .objectAlreadyCreated => ArgumentMarshaller.marshalUInt 0
    | _, _ => throw "Marshalling unexpected type, expected int or uint."
  demarshal
    | .int => do
      match (← ArgumentDemarshaller.demarshalInt) with
        | 0 => pure .objectAlreadyCreated
        | _ => throw "Invalid enum value."
    | .uint => do
      match (← ArgumentDemarshaller.demarshalUInt) with
        | 0 => pure .objectAlreadyCreated
        | _ => throw "Invalid enum value."
    | _ => throw "Demarshalling unexpected type, expected int or uint."

end RiverLayerShellV1.Error

end Wayland.Protocols