3 files changed, 71 insertions, 0 deletions
diff --git a/lib/Wayland/Basic/Duration.lean b/lib/Wayland/Basic/Duration.lean
new file mode 100644
index 0000000..5212ff0
--- /dev/null
+++ b/lib/Wayland/Basic/Duration.lean
@@ -0,0 +1,26 @@
+/-!
+# Time Durations
+
+This interface abstracts the unit of time duration values.
+-/
+
+namespace Wayland
+
+/-- A duration value. -/
+structure Duration where
+  private milliseconds : UInt32
+  deriving Repr, BEq, Inhabited
+
+def Duration.ofMilliseconds (val : UInt32) : Duration := ⟨val⟩
+def Duration.ofSeconds (val : UInt32) : Duration := .ofMilliseconds (val * 1000)
+def Duration.ofMinutes (val : UInt32) : Duration := .ofSeconds (val * 60)
+
+def Duration.toMilliseconds (val : Duration) : UInt32 := val.milliseconds
+def Duration.toSeconds (val : Duration) : UInt32 := val.toMilliseconds / 1000
+def Duration.toMinutes (val : Duration) : UInt32 := val.toSeconds / 60
+
+notation:2000 val "ms" => Duration.ofMilliseconds val
+notation:2000 val "sec" => Duration.ofSeconds val
+notation:2000 val "min" => Duration.ofMinutes val
+
+end Wayland
diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean
new file mode 100644
index 0000000..16de458
--- /dev/null
+++ b/lib/Wayland/Basic/Lens.lean
@@ -0,0 +1,22 @@
+/-!
+# Lenses
+
+A `Lens` bundles a getter and an (updating) setter which can be used to elegantly describe a field of a structure.
+-/
+
+namespace Wayland
+
+/-- A lens that points into a substructure of type `I` within a structure of type `O`. -/
+structure Lens (O I : Type) where
+  /-- Get the substructure from the outer structure. -/
+  get : O → I
+  /-- Update the outer structure to contain the updated substructure. -/
+  set : I → O → O
+
+/-- Helper for writing a `Lens` constructor for a named field of a structure. -/
+macro "mk_lens " field:ident : term => do
+  let lvalNode := Lean.mkNode `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode #[]]
+  let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩
+  `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } })
+
+end Wayland
diff --git a/lib/Wayland/Basic/PosixSignal.lean b/lib/Wayland/Basic/PosixSignal.lean
new file mode 100644
index 0000000..45c7361
--- /dev/null
+++ b/lib/Wayland/Basic/PosixSignal.lean
@@ -0,0 +1,23 @@
+import Wayland.Native
+
+/-!
+# POSIX Signals
+
+Data type representing a POSIX signal number.
+-/
+
+namespace Wayland
+
+/-- A POSIX signal number. -/
+structure PosixSignal where
+  signum : UInt32
+  deriving Repr, BEq, Inhabited
+
+/-- The SIGINT (interrupted) signal. -/
+def PosixSignal.SIGINT : PosixSignal := ⟨Native.SIGINT ()⟩
+/-- The SIGUSR1 (first user-defined) signal. -/
+def PosixSignal.SIGUSR1 : PosixSignal := ⟨Native.SIGUSR1 ()⟩
+/-- The SIGUSR2 (second user-defined) signal. -/
+def PosixSignal.SIGUSR2 : PosixSignal := ⟨Native.SIGUSR2 ()⟩
+
+end Wayland