display connect/disconnect

10 files changed, 134 insertions, 24 deletions

diff --git a/flake.nix b/flake.nix
index 3c32dcc..90f47cb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -17,6 +17,9 @@
       lean-shell = pkgs.mkShell {
         name = "Lean";
         packages = [ pkgs.lean4 pkgs.wayland pkgs.pkg-config ];
+        shellHook = pkgs.lib.optionalString pkgs.stdenv.isDarwin ''
+          export XDG_RUNTIME_DIR="$(pwd)/server"
+        '';
       };
     in {
     devShells = {
diff --git a/lakefile.lean b/lakefile.lean
index ecee22d..660403d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,7 +18,7 @@ package «CWayland» {
 
 target «LibCWayland.o» pkg : System.FilePath := do
   let objectFile := pkg.buildDir / "LibCWayland.o"
-  let srcJob ← inputFile (text := .true) <| pkg.dir / "lib" / "CWayland" / "CWayland.c"
+  let srcJob ← inputFile (text := .true) <| pkg.dir / "lib" / "CWayland" / "CWayland.cc"
   let cFlags ← evalPkgConfig #["--cflags", "wayland-client"]
   buildFileAfterDep objectFile srcJob (fun srcFile ↦ do
     let cFlags := cFlags ++ #["-I", (← getLeanIncludeDir).toString, "-I", (← IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC"]
diff --git a/lib/CWayland/CWayland.c b/lib/CWayland/CWayland.c
deleted file mode 100644
index 10c1cc2..0000000
--- a/lib/CWayland/CWayland.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include "CWayland.h"
-#include <wayland-client.h>
-
-lean_obj_res lean_test_answer()
-{
-    struct wl_display* disp = wl_display_connect(NULL);
-    wl_fixed_t fixed = wl_fixed_from_double(42.0);
-    return lean_io_result_mk_ok(lean_int_to_int(wl_fixed_to_int(fixed)));
-}
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.cc b/lib/CWayland/CWayland.cc
new file mode 100644
index 0000000..5877ad4
--- /dev/null
+++ b/lib/CWayland/CWayland.cc
@@ -0,0 +1,60 @@
+#include "CWayland.h"
+#include <wayland-client.h>
+
+static void noop_foreach(void *ptr, b_lean_obj_arg fn)
+{
+}
+
+static void waylean_display_finalize(void* ptr)
+{
+    wl_display* disp = static_cast<wl_display*>(ptr);
+    wl_display_disconnect(disp);
+}
+
+static lean_external_class* waylean_display_class()
+{
+    static lean_external_class* klass = lean_register_external_class(&waylean_display_finalize, &noop_foreach);
+    return klass;
+}
+
+static char const* option_cstr_or_null(b_lean_obj_arg str)
+{
+    if (lean_is_scalar(str))
+    {
+        return nullptr;
+    }
+    else
+    {
+        lean_object* val = lean_ctor_get(str, 0);
+        return lean_string_cstr(val);
+    }
+}
+
+static lean_obj_res io_result_mk_from_errno(char const* file_name)
+{
+    int err = errno;
+    lean_object* file_name_str = lean_mk_string(file_name);
+    lean_object* error = lean_decode_io_error(err, file_name_str);
+    lean_dec(file_name_str);
+
+    return lean_io_result_mk_error(error);
+}
+
+// Display.new : (name : @& Option String) → IO Display
+lean_obj_res waylean_display_new(b_lean_obj_arg name)
+{
+    char const* name_cstr = option_cstr_or_null(name);
+    wl_display* disp = wl_display_connect(name_cstr);
+    if (!disp) { return io_result_mk_from_errno(name_cstr ? name_cstr : "<default>"); }
+
+    lean_object* waylean_disp = lean_alloc_external(waylean_display_class(), disp);
+    return lean_io_result_mk_ok(waylean_disp);
+}
+
+// Display.getVersion : (display : @& Display) → IO UInt32
+lean_obj_res waylean_display_get_version(b_lean_obj_arg display)
+{
+    wl_display* disp = static_cast<wl_display*>(lean_get_external_data(display));
+    lean_object* version = lean_box_uint32(wl_display_get_version(disp));
+    return lean_io_result_mk_ok(version);
+}
\ No newline at end of file
diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h
index 42bc5ee..adcadc0 100644
--- a/lib/CWayland/CWayland.h
+++ b/lib/CWayland/CWayland.h
@@ -2,19 +2,29 @@
 
 #include <lean/lean.h>
 
+#ifdef __cplusplus
+extern "C"
+{
+#endif
+
 // Display
 
-lean_obj_res waylean_display_new(void);
+lean_obj_res waylean_display_new        (b_lean_obj_arg name);
+lean_obj_res waylean_display_get_version(b_lean_obj_arg display);
 
 // Event Loop
 
 lean_obj_res waylean_event_loop_new        (void);
-lean_obj_res waylean_event_loop_add_display(lean_obj_arg event_loop,
-                                            lean_obj_arg display);
-lean_obj_res waylean_event_loop_add_timer  (lean_obj_arg event_loop,
-                                            unsigned     delay_ms,
-                                            lean_obj_arg message);
-lean_obj_res waylean_event_loop_add_signal (lean_obj_arg event_loop,
-                                            int          signum,
-                                            lean_obj_arg message);
-lean_obj_res waylean_event_loop_poll       (lean_obj_arg event_loop);
\ No newline at end of file
+lean_obj_res waylean_event_loop_add_display(b_lean_obj_arg event_loop,
+                                            b_lean_obj_arg display);
+lean_obj_res waylean_event_loop_add_timer  (b_lean_obj_arg event_loop,
+                                            unsigned       delay_ms,
+                                            b_lean_obj_arg message);
+lean_obj_res waylean_event_loop_add_signal (b_lean_obj_arg event_loop,
+                                            int            signum,
+                                            b_lean_obj_arg message);
+lean_obj_res waylean_event_loop_poll       (b_lean_obj_arg event_loop);
+
+#ifdef __cplusplus
+}
+#endif
\ No newline at end of file
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
index ded2e3a..c529b63 100644
--- a/lib/Wayland/Native.lean
+++ b/lib/Wayland/Native.lean
@@ -1,2 +1,9 @@
-@[extern "lean_test_answer"]
-opaque testAnswer : IO Int
+private opaque DisplayP : NonemptyType
+def Display : Type := DisplayP.type
+instance : Nonempty Display := DisplayP.property
+
+@[extern "waylean_display_new"]
+opaque Display.new : (name : @& Option String) → IO Display
+
+@[extern "waylean_display_get_version"]
+opaque Display.getVersion : (display : @& Display) → IO UInt32
diff --git a/server/.gitignore b/server/.gitignore
new file mode 100644
index 0000000..75e973c
--- /dev/null
+++ b/server/.gitignore
@@ -0,0 +1,2 @@
+wayland-*
+server
\ No newline at end of file
diff --git a/server/makefile b/server/makefile
new file mode 100644
index 0000000..520636c
--- /dev/null
+++ b/server/makefile
@@ -0,0 +1,12 @@
+CC = clang
+CFLAGS = -std=c17 -pedantic -Wall -Werror $(shell pkg-config --libs --cflags wayland-server)
+
+.PHONY: all clean
+
+all: server
+
+clean:
+	rm -f server
+
+server: server.c
+	$(CC) $(CFLAGS) -o $@ $<
diff --git a/server/server.c b/server/server.c
new file mode 100644
index 0000000..3687865
--- /dev/null
+++ b/server/server.c
@@ -0,0 +1,25 @@
+#include <wayland-server.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+static void die(char const* s)
+{
+	perror(s);
+	exit(EXIT_FAILURE);
+}
+
+int main(int argc, char** argv)
+{
+	struct wl_display* disp = wl_display_create();
+	if (!disp) { die("wl_display_create"); }
+	
+	char const* sock = wl_display_add_socket_auto(disp);
+	if (!sock) { die("wl_display_add_socket_auto"); }
+
+	printf("Compositor running on %s\n", sock);
+
+	wl_display_run(disp);
+
+	wl_display_destroy(disp);
+	return EXIT_SUCCESS;
+}
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 5445f25..d05df11 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -1,5 +1,5 @@
 import Wayland
 
 def main : IO Unit := do
-  let answer ← testAnswer
-  IO.println s!"Hello, world! The answer is {answer}."
+  let disp ← Display.new .none
+  IO.println s!"Hello, world! Version: {← disp.getVersion}"