Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Lean4 Tutorial/Notes on creating FFI bindings with GLFW as an example.

License

NotificationsYou must be signed in to change notification settings

DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

7 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

There seems to be no complete tutorial on creating C FFI bindings in Lean4. So I am writing notes here. I am putting the keyword "tutorial" in the GitHub project name just so people who search "Lean4 FFI tutorial" will land on this and hopefully get some guidances, but by no means does this markdown serve as a complete, 100% correct tutorial. I don't even know what is going on half of the time when reading the sources:

Introduction

(This section might need you to have some understanding in writing C FFIs in Haskell, or writing language bindings in general. Otherwise you might have no idea what is going on or why are things the way they are.)

Say you would like to write some C FFI bindings in Lean4 tolibglfw.so, a popular C library for creating windows and OpenGL contexts. Let's also say you plan to create Lean4 bindings toglfwInit,glfwTerminate,glfwPollEvents,glfwCreateWindow andglfwWindowShouldClose. In fact, I picked these examples because:

  • glfwInit,glfwTerminate, andglfwPollEvents are simple functions, great for an introduction to writing Lean4 bindings.
  • glfwCreateWindow involves passing an opaque object from C to Lean4. I will also demonstrate how to passStrings from Lean4 to C.
  • glfwWindowShouldClose involves passing an opaque object from Lean4 to C.
  • They provide the minimal set of functionalities to create a working GLFW window.

In short, you will basically have to: (You can skip this paragraph if you want and move on to the steps to creating FFIs for GLFW right now)

  1. Write a.c source file providing the right functions and function signatures that compiled Lean4 programs know how to talk to.
  2. Modify yourlakefile.lean to...
    1. compile the.c file to produce a static lib,
    2. and add the necessary compilation/linking flags to linklibglfw.so and the static lib of the.c to your Lean4 application executable whenever you do$ lake build.
  3. Writeopaque Lean4 definitions in a.lean module in your Lean4 project that point to the certain functions written in that.c file. You might also have to define some opaque structures if the FFI functions return pointers to, say, a C handle object.

A brief introduction on GLFW

For reference, here are the functions you would like to bind to:

// Initializes the GLFW library.// `GLFW_TRUE` if successful, or `GLFW_FALSE` if an error occurred.intglfwInit(void);// Terminates the GLFW library.voidglfwTerminate(void);// Creates a GLFW window,// and returns an abstract handle to it.GLFWwindow*glfwCreateWindow(intwidth,intheight,constchar*title,// window titleGLFWmonitor*monitor,// you may ignore this argumentGLFWwindow*share// you may ignore this argument);// See: https://www.glfw.org/docs/latest/group__window.html#ga37bd57223967b4211d60ca1a0bf3c832voidglfwPollEvents(void);// Did the user intend to close `window`? (e.g., pressing the [X] button)intglfwWindowShouldClose(GLFWwindow*window);

Here is a basic GLFW example that creates a blank GLFW window and ends when the user closes the GLFW window:

#include<GLFW/glfw3.h>#include<stdlib.h>intmain() {if (!glfwInit()) {perror("Cannot initialize GLFW!!\n");returnEXIT_FAILURE;  }GLFWwindow*win=glfwCreateWindow(800,600,"My GLFW window's title",NULL,NULL);while (!glfwWindowShouldClose(win)) {glfwPollEvents();  }glfwTerminate();printf("Goodbye.\n");}

Our goal will be to rewrite this program in "pure Lean4".

Writing the FFI

Setup

Suppose in the beginning, you did$ lake init and get the following:

.├── lakefile.lean├── lake-manifest.json├── lean-toolchain├── Main.lean├── <Your main library directory>/├── <Your main library name>.lean└── ... possibly more files

First, define the followingopaque functions in a.lean file in your Lean4 project (I will explain the details later). For simplicity, I will write them in./Main.lean.

-- There are no need for more additional imports.@[extern "lean_glfwInit"]opaque glfwInit : IO Bool@[extern "lean_glfwTerminate"]opaque glfwTerminate : IO Unit@[extern "lean_glfwPollEvents"]opaque glfwPollEvents : IO Unit-- An opaque type to represent `GLFWwindow *`opaque WindowP : NonemptyTypedef Window := WindowP.type@[extern "lean_glfwCreateWindow"]opaque glfwCreateWindow (width : UInt32) (height : UInt32) (title : String) : IO Window-- We will ignore `monitor` and `share`.@[extern "lean_glfwWindowShouldClose"]opaque glfwWindowShouldClose (win : Window) : IO Booldef main : IO Unit := do  IO.println "Hello world!"

Next, create a file called./native.c (the name is arbitrary) and put the following:

#include<lean/lean.h>// IMPORTANT!!lean_obj_reslean_glfwInit(lean_obj_argworld) {// TODO:}lean_obj_reslean_glfwTerminate(lean_obj_argworld) {// TODO:}lean_obj_reslean_glfwCreateWindow(uint32_twidth,uint32_theight,b_lean_obj_argtitle,lean_obj_argworld) {// TODO:}lean_obj_reslean_glfwWindowShouldClose(lean_obj_argwinp,lean_obj_argworld) {// TODO:}lean_obj_reslean_glfwPollEvents(lean_obj_argworld) {// TODO:}

After that, modify your./lakefile.lean to automatically compile./native.c and link the generated static lib andlibglfw.so to your Lean4 application executable for future$ lake build calls. Here is an example:

import Lakeopen Lake DSLpackage «YourProjectName» where  -- add package configuration options here@[default_target]lean_exe «glfw_test_exe» where  root := `Main  moreLinkArgs := #["-lglfw", "-Wl,--allow-shlib-undefined"] -- To link `libglfw.so` to your Lean4 app exe.-- Create target named `native.o` by compile `./native.c`-- Honestly, this is kind of like writing Makefilestarget native.o (pkg : NPackage _package.name) : FilePath := do  let native_src := "native.c"  let native_c := pkg.dir / native_src  let native_o := pkg.buildDir / "native.o"  buildFileAfterDep native_o (<- inputFile native_c) fun native_src => do    let lean_dir := (<- getLeanIncludeDir).toString    compileO      "My native.o compilation"      native_o      native_src #["-I", lean_dir, "-fPIC"]-- Create a static lib from `native.o`extern_lib native (pkg : NPackage _package.name) := do  let name := nameToStaticLib "native"  let native_o <- fetch <| pkg.target ``native.o  buildStaticLib    (pkg.buildDir / "lib" / name)    #[native_o]

On./native.c and./Main.lean

What is going on with./native.c and those@[extern "XXX"] opaque definitions in our./Main.lean?

In./Main.lean:

  1. Each@[extern <func_name>] marked opaque function in./Main.lean corresponds to a function with the name<func_name> defined in./native.c.
  2. TheWindowP andWindow part in./Main.lean will become apparent later when we start passingGLFWwindow * objects around between Lean4 and C. I don't have an explanation as to why it is written like this, so just copy it and change the names for other opaque C types.

Now, let's take a look at./native.c. We will first inspectlean_glfwInit:

// Lean4's counterpart in ./Main.lean://   @[extern "lean_glfwInit"]//   opaque glfwInit : IO Boollean_obj_reslean_glfwInit(lean_obj_argworld) {// TODO: we will call glfwInit() here and return the initialization status code back as a Bool}

lean_glfwInit corresponds toopaque glfwInit : IO Bool in our./Main.lean as indicated by us marking the Lean4 function@[extern "lean_glfwInit"]. Whenever we callopaque glfwInit : IO Bool in our Lean4 program,lean_glfwInit from./native.c will be called.

Inlean_glfwInit's function signature, you can see that the function takes in onelean_obj_arg and returns alean_obj_res. These are Lean4 objects, the typedefs come from#include <lean/lean.h>.

In fact,lean_obj_arg andlean_obj_res are just aliases to the typelean_object *. Here are their definitions ripped out fromlean/lean.h:

/* The following typedef's are used to document the calling convention for the primitives. */typedeflean_object*lean_obj_arg;/* Standard object argument. */typedeflean_object*b_lean_obj_arg;/* Borrowed object argument. */typedeflean_object*u_lean_obj_arg;/* Unique (aka non shared) object argument. */typedeflean_object*lean_obj_res;/* Standard object result. */typedeflean_object*b_lean_obj_res;/* Borrowed object result. */

and here islean_object's definition if you are curious:

typedefstruct {intm_rc;unsignedm_cs_sz:16;unsignedm_other:8;unsignedm_tag:8;}lean_object;

Do be informed that Lean4's usages oflean_object andlean_object * are non-trivial. There are some tricks likelean_object * pointer tagging for constants and other black magics in play for optimization. I will NOT touch on them. However, you can find all the disgusting details in the comments written onhttps://github.com/leanprover/lean4/blob/master/src/include/lean/lean.h (The whole header only has around 2000 lines).

Before explaining more onlean_glfwInit's actual function signature, observe the following translations between Lean4 function types and C function types:

A function that takes inno arguments and returnsUnit.

// @[extern "foo1"]// opaque foo1 : Unitlean_obj_resfoo1();// [!] Returning a `Unit` requires returning a `lean_obj_res`.

A function that takes in aUnit and returnsUnit.

// @[extern "foo2"]// opaque foo2 : (a : Unit) -> Unitlean_obj_resfoo2(lean_obj_arga);// [!] Taking in 1 argument.

...and now 3Units as input.

// @[extern "foo3"]// opaque foo3 : (a : Unit) -> (b : Unit) -> (c : Unit) -> Unitlean_obj_resfoo3(lean_obj_arga,lean_obj_argb,lean_obj_argc);// [!] Taking in 3 arguments.

Here is a function with "special Lean4 types" (uint8_t,uint32_t).

// @[extern "foo4"]// opaque foo4 : (a : UInt8) -> (b : UInt32) -> (c : Unit) -> Unitlean_obj_resfoo4(uint8_ta,uint32_tb,lean_obj_argc);// [!] Certain Lean4 types have special translations//     Please see https://lean-lang.org/lean4/doc/dev/ffi.html#translating-types-from-lean-to-c for a complete(?) list.//     Here, UInt8 maps to uint8_t, and UInt32 maps to uint32_t.

..and here is one that takes in aBool, which is mapped touint8_t. It is also a "special Lean4 type".

// @[extern "foo5"]// opaque foo5 : (mybool : Bool) -> Unitlean_obj_resfoo5(uint8_tmybool);// [!] Bool maps to uint8_t, where 0 is false and 1 is true.//     See https://lean-lang.org/lean4/doc/dev/ffi.html#translating-types-from-lean-to-c.

Here is a function that takes inuint8_t (a special Lean4 type) and returnsuint16_t (another special Lean4 type). Notice that we are not returning alean_obj_res, but auint16_t. (TODO: cite an official reference on this behaviour, I learnt this through experimenting with FFIs and see what segfaults.)

// @[extern "foo6"]// opaque foo6 : (mybool : Bool) -> UInt16uint16_tfoo6(uint8_tmybool);// [!] Returning a uint16_t instead of the usual `lean_obj_res` here because UInt16 translates to uint16_t.

foo7 is the most important example. It does I/O.

// @[extern "foo7"]// opaque foo7 : (mybool : Bool) -> IO Unitlean_obj_resfoo7(uint8_tmybool,lean_obj_argworld);// [!] Functions with the return type `IO` are quite interesting,//     Lean4 expects them to take in an extra lean_obj_arg,//       and they *MUST* return a lean_obj_res.// =======================================================================================// I have not been able to find an official explanation for this seemingly strange function signature.// But here is my guess:////   We have://     opaque foo7 : (mybool : Bool) -> IO Unit////   Consider that, in Lean4://     abbrev IO : Type → Type := EIO Error//     def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld//     def IO.RealWorld : Type := Unit//     def EStateM (ε σ α : Type u) := σ → Result ε σ α//     inductive Result (ε σ α : Type u) where//       | ok    : α → σ → Result ε σ α//       | error : ε → σ → Result ε σ α////   This means that://       IO a//     = EIO Error a//     = EStateM Error IO.RealWorld a//     = IO.RealWorld -> Result Error IO.RealWorld a//     = Unit -> Result Error Unit a (IO.RealWorld is just Unit)////   Therefore,//       foo7 : (mybool : Bool) -> IO Unit//     = foo7 : (mybool : Bool) -> IO.RealWorld -> Result Error IO.RealWorld Unit//     = foo7 : (mybool : Bool) -> (world : Unit) -> Result Error Unit Unit//              ^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^//              first arg          second arg////   This matches what we see in foo7's type signature://     lean_obj_res foo7(uint8_t mybool, lean_obj_arg world);//                       ^^^^^^^^^^^^^^  ^^^^^^^^^^^^^^^^^^//                       first arg       second arg////   This also implies that the returned `lean_obj_res` will in fact be a `Result` object,//     and indeed we will later see that we will use functions like `lean_io_result_mk_ok`//     to construct `Result` Lean4 objects and return them back to our Lean4 program.

Here is another IO function, it returns aUInt32 (a special type), but in fact we return alean_obj_res unlikefoo6 because IO functions return aResult object.

// @[extern "foo8"]// opaque foo8 : (mybool : Bool) -> IO UInt32lean_obj_resfoo8(uint8_tmybool,lean_obj_argworld);// [!] IMPORTANT! Even if we are technically returning a UInt32, we still return a//       `lean_obj_res` because we are suppose return a `Result` Lean4 object, of which//       will contain our uint32_t result.

Now, hopefully you can see now whylean_glfwInit has this type signature:

// @[extern "lean_glfwInit"]// opaque glfwInit : IO Boollean_obj_reslean_glfwInit(lean_obj_argworld);

Implementinglean_glfwInit()

DISCLAIMER: THE FOLLOWING DETAILS COULD BE VERY, VERY WRONG, but the final code does produce a working GLFW program.

Let's implementlean_glfwInit:

lean_obj_reslean_glfwInit(lean_obj_argworld) {// `world` is unused.intresult=glfwInit();returnlean_io_result_mk_ok(lean_box(result));}

Here, we callglfwInit(), and call some functions provided bylean/lean.h to build alean_obj_res as a Lean4Result object as required byIO functions, where...

// Construct a `lean_object *` representing `Result.ok r ()`lean_obj_reslean_io_result_mk_ok(lean_obj_argr);// Construct a `lean_object *` representing the signed integer nlean_object*lean_box(size_tn);

Hopefully this is enough to explain why we are writing this to build ourlean_obj_res:

returnlean_io_result_mk_ok(lean_box(result));// ~ Result IO.Error IO.RealWorld Bool

You can now try usingopaque glfwInit : IO Bool in./Main.lean:

@[extern "lean_glfwInit"]opaque glfwInit : IO Bool-- ...main : IO Unitmain = do  IO.println "Initializing GLFW"  let init_ok <- glfwInit  unless init_ok do    IO.println "Cannot initialize GLFW!!"     return // end program    IO.println "Initialized GLFW!!"

Implementinglean_glfwTerminate() andlean_glfwPollEvents()

Let's move on toglfwTerminate andglfwPollEvents, although they are not so interesting:

// @[extern "lean_glfwTerminate"]// opaque glfwTerminate : IO Unitlean_obj_reslean_glfwTerminate(lean_obj_argworld) {glfwTerminate();// [!] lean_box(0) means 0 or an Unit object.returnlean_io_result_mk_ok(lean_box(0)); }// @[extern "lean_glfwPollEvents"]// opaque glfwPollEvents : IO Unitlean_obj_reslean_glfwPollEvents(lean_obj_argworld) {// In fact, `world` is also just lean_box(0)... I think.glfwPollEvents();returnlean_io_result_mk_ok(lean_box(0));}

Implementinglean_glfwCreateWindow() + opaqueGLFWwindow *

Let's get toglfwCreateWindow. Here, things get more complicated because we have to handle the opaque typeGLFWwindow *:

staticvoidnoop_foreach(void*data,b_lean_obj_argarg) {// NOTHING}staticvoidglfw_window_finalizer(void*ptr) {glfwDestroyWindow((GLFWwindow*)ptr);}// opaque WindowP : NonemptyType// def Window := WindowP.typestaticlean_external_class*get_glfw_window_class() {staticlean_external_class*g_glfw_window_class=NULL;if (!g_glfw_window_class) {g_glfw_window_class=lean_register_external_class(&glfw_window_finalizer,&noop_foreach);  }returng_glfw_window_class;}// @[extern "lean_glfwCreateWindow"]// opaque glfwCreateWindow (width : UInt32) (height : UInt32) (title : String) : IO Windowlean_obj_reslean_glfwCreateWindow(uint32_twidth,uint32_theight,b_lean_obj_argtitle,lean_obj_argworld) {printf("lean_glfwCreateWindow %dx%d\n",width,height);// Here for debuggingcharconst*title_cstr=lean_string_cstr(title);// Read below for what `lean_string_cstr` doesGLFWwindow*win=glfwCreateWindow(width,height,title,NULL,NULL);// Returns (GLFWwindow *) -- an opaque type!returnlean_io_result_mk_ok(lean_alloc_external(get_glfw_window_class(),win));}// where...// Suppose o is a `String` Lean4 object, get the pointer pointing to the UTF8 bytes of the String.charconst*lean_string_cstr(b_lean_obj_argo);

Here, we see new functions related to constructinglean_object * from custom pointers (e.g.,GLFWwindow *):

  • lean_alloc_external
  • lean_external_class
  • lean_register_external_class

You already know whatlean_io_result_mk_ok does.

Onlean_alloc_external() andlean_external_class

Here is the function signature oflean_alloc_external fromlean/lean.h:

// Constructs a `lean_object *` representing an externally-defined C object//   cls:  Lean4's representation of the "type" of the externally-defined C object//   data: the pointer to that externally-defined C objectlean_object*lean_alloc_external(lean_external_class*cls,void*data);

lean_external_class is used by Lean4 internally to understand more about thevoid *data you pass in. Itapparently has two purposes:

  1. to tell how to deallocate/finalizedata when thelean_object * goes out of scope in your Lean4 program,
  2. (My guess) to tell how to iterate overdata. (Like how you can havechar *c and doc + 3 to get the address of the 3rdchar by displacement.)

Here is the definition oflean_external_class if that is of any help:

typedefvoid (*lean_external_finalize_proc)(void*data);typedefvoid (*lean_external_foreach_proc)(void*data,b_lean_obj_arg*idk_what_this_arg_is_for);typedefstruct {lean_external_finalize_procm_finalize;lean_external_foreach_procm_foreach;}lean_external_class;

It is okay if you don't understand whatlean_external_class actually does, because I also don't.

Onlean_register_external_class() andget_glfw_window_class()

Anyway, recall that to create alean_object * out ofGLFWwindow *win, we need to dolean_alloc_external(get_glfw_window_class(), win), which then will be wrapped bylean_lean_io_result_mk_ok. Having already explained whatlean_alloc_external() is, I will now explain theget_glfw_window_class() part.

Here is the functionget_glfw_window_class again:

// opaque WindowP : NonemptyType// def Window := WindowP.typestaticlean_external_class*get_glfw_window_class() {staticlean_external_class*g_glfw_window_class=NULL;if (!g_glfw_window_class) {g_glfw_window_class=lean_register_external_class(&glfw_window_finalizer,&noop_foreach);  }returng_glfw_window_class;}// where...typedefvoid (*lean_external_finalize_proc)(void*);typedefvoid (*lean_external_foreach_proc)(void*,b_lean_obj_arg);// Creates a (lean_external_class *), for use in lean_alloc_external()lean_external_class*lean_register_external_class(lean_external_finalize_proc,lean_external_foreach_proc);

Inget_glfw_window_class, essentially, we are callinglean_register_external_class to tell Lean4 to create alean_external_class representingGLFWwindow * withglfw_window_finalizer as its finalizer andnoop_foreach as its "foreach" part,

whereglfw_window_finalizer is defined as...

staticvoidglfw_window_finalizer(void*ptr) {// Here, I defined it to destroy the GLFWwindow object as an example.// In reality, I would put nothing here, and instead write a new opaque Lean4 function + C function for this destroying windows explicitly.glfwDestroyWindow((GLFWwindow*)ptr);}

...andnoop_foreach is defined as:

staticvoidnoop_foreach(void*data,b_lean_obj_argarg) {// NOTHING}

I am usingnoop_foreach for thelean_external_class representingGLFWwindow * here becauseGLFWwindow * points to an handle object instead of the start of an array of something. There is no need for a "foreach" functionality.

get_glfw_window_class is also written in such a way that the first call toget_glfw_window_class will register thelean_external_class that representsGLFWwindow * and return it, and subsequent classes will return the already createdlean_external_class. I am making use of a function-scopedstatic variable here to do this trick.

Now, this should clarify whatlean_glfwCreateWindow does.

OnWindow,WindowP and theGLFWwindow * opaque type

As for the opaqueWindow/WindowP definition in our./Main.lean, we as programmers will have to make sure that whenever aGLFWwindow * is the return type or a argument type in our functions, we must useWindow in our Lean4 code.

opaque WindowP : NonemptyTypedef Window := WindowP.type@[extern "lean_glfwCreateWindow"]opaque glfwCreateWindow (width : UInt32) (height : UInt32) (title : String) : IO Window // [!] Returns `Window`// lean_obj_res lean_glfwCreateWindow(uint32_t width, uint32_t height, b_lean_obj_arg title, lean_obj_arg world);@[extern "lean_glfwWindowShouldClose"]opaque glfwWindowShouldClose (win : Window) : IO Bool // [!] Takes in `Window`// lean_obj_res lean_glfwWindowShouldClose(lean_obj_arg winp, lean_obj_arg world);

Implementinglean_glfwWindowShouldClose()

Finally, let's implementlean_glfwWindowShouldClose:

// @[extern "lean_glfwWindowShouldClose"]// opaque glfwWindowShouldClose (win : Window) : IO Bool // [!] Takes in `Window`lean_obj_reslean_glfwWindowShouldClose(lean_obj_argwinp,lean_obj_argworld) {assert(lean_is_external(winp));// For debugging// This is how we extract the `void *data` from a `lean_obj_arg` if the arg is indeed representing some external data.GLFWwindow*win= (GLFWwindow*)lean_get_external_data(winp);boolstatus=glfwWindowShouldClose(win);returnlean_io_result_mk_ok(lean_box(status));}// where...void*lean_get_external_data(lean_object*o);

Hopefully you can understand the definitionlean_glfwWindowShouldClose without any explanations now.

And that is it!

GLFW in Lean4

We can now implement the following C code:

#include<GLFW/glfw3.h>#include<stdlib.h>intmain() {if (!glfwInit()) {perror("Cannot initialize GLFW!!\n");returnEXIT_FAILURE;  }GLFWwindow*win=glfwCreateWindow(800,600,"My GLFW window's title",NULL,NULL);while (!glfwWindowShouldClose(win)) {glfwPollEvents();  }glfwTerminate();printf("Goodbye.\n");}

...in Lean4:

def main : IO Unit := do  unless (<- glfwInit) do    (<- IO.getStderr).putStrLn "Cannot initialize GLFW!!"    return -- TODO: how to exit with EXIT_FAILURE?  let win <- glfwCreateWindow 800 600 "My GLFW window's title"  while (not (<- glfwWindowShouldClose win)) do    glfwPollEvents  glfwTerminate  (<- IO.getStdout).putStrLn "Goodbye."

All the code is in this repository. Do$ ./run.sh to build and run the final GLFW example app.

TODOs

  • Investigate on constructinglean_obj_res * objects of Lean4 inductive types in C.
  • Understand what borrowing is and how it affects programming an FFI.

About

Lean4 Tutorial/Notes on creating FFI bindings with GLFW as an example.

Topics

Resources

License

Stars

Watchers

Forks

[8]ページ先頭
©2009-2025 Movatter.jp