fix build on linux

4 files changed, 248 insertions, 0 deletions

diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean
new file mode 100644
index 0000000..7c01f90
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverLayerShellV1/Header.lean
@@ -0,0 +1,36 @@
+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
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean
new file mode 100644
index 0000000..5e0cb2d
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverLayerShellV1/Interface.lean
@@ -0,0 +1,123 @@
+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
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean
new file mode 100644
index 0000000..8e7dc9f
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverLayerShellV1/Requests.lean
@@ -0,0 +1,51 @@
+import Wayland.Display
+import Wayland.Protocols.RiverLayerShellV1.Resolved
+import Wayland.Protocols.RiverWindowManagementV1.Header
+
+namespace Wayland.Protocols
+
+variable {σ : Type} {ι : InterfaceName} [iface : ResolvedInterface ι]
+
+def RiverLayerShellV1.destroy
+    (ω : RiverLayerShellV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 0
+
+def RiverLayerShellV1.getOutput
+    (ω : RiverLayerShellV1)
+    (output : RiverOutputV1)
+    : DisplayM σ RiverLayerShellOutputV1 :=
+  ω.sendConstructor do
+    ArgumentMarshaller.marshalAnyObject .none
+    Marshallable.marshal .object output
+    return 1
+
+def RiverLayerShellV1.getSeat
+    (ω : RiverLayerShellV1)
+    (seat : RiverSeatV1)
+    : DisplayM σ RiverLayerShellSeatV1 :=
+  ω.sendConstructor do
+    ArgumentMarshaller.marshalAnyObject .none
+    Marshallable.marshal .object seat
+    return 2
+
+def RiverLayerShellOutputV1.destroy
+    (ω : RiverLayerShellOutputV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 0
+
+def RiverLayerShellOutputV1.setDefault
+    (ω : RiverLayerShellOutputV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 1
+
+def RiverLayerShellSeatV1.destroy
+    (ω : RiverLayerShellSeatV1)
+    : DisplayM σ Unit :=
+  ω.send do
+    return 0
+
+end Wayland.Protocols
\ No newline at end of file
diff --git a/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean b/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean
new file mode 100644
index 0000000..060dc6f
--- /dev/null
+++ b/lib/Wayland/Protocols/RiverLayerShellV1/Resolved.lean
@@ -0,0 +1,38 @@
+import Wayland.Display
+import Wayland.Protocols.RiverLayerShellV1.Interface
+import Wayland.Protocols.RiverWindowManagementV1.Interface
+import Wayland.Protocols.Wayland.Interface
+
+namespace Wayland.Protocols
+
+instance instResolvedInterfaceRiverLayerShellV1 : ResolvedInterface RiverLayerShellV1.name where
+  referencedInterfaces := #[
+    ⟨RiverLayerShellOutputV1.name, inferInstance⟩,
+    ⟨RiverLayerShellSeatV1.name, inferInstance⟩,
+    ⟨RiverLayerShellV1.name, inferInstance⟩,
+    ⟨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 instResolvedInterfaceRiverLayerShellOutputV1 : ResolvedInterface RiverLayerShellOutputV1.name where
+  referencedInterfaces := #[
+    ⟨RiverLayerShellOutputV1.name, inferInstance⟩,
+  ]
+
+instance instResolvedInterfaceRiverLayerShellSeatV1 : ResolvedInterface RiverLayerShellSeatV1.name where
+  referencedInterfaces := #[
+    ⟨RiverLayerShellSeatV1.name, inferInstance⟩,
+  ]
+
+
+end Wayland.Protocols
\ No newline at end of file