diff options
| -rw-r--r-- | flake.nix | 3 | ||||
| -rw-r--r-- | lakefile.lean | 2 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.c | 9 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.cc | 60 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 30 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 11 | ||||
| -rw-r--r-- | server/.gitignore | 2 | ||||
| -rw-r--r-- | server/makefile | 12 | ||||
| -rw-r--r-- | server/server.c | 25 | ||||
| -rw-r--r-- | src/Waylean.lean | 4 |
10 files changed, 134 insertions, 24 deletions
@@ -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}" |