Open
Conversation
The existing FFI API (ABI v1) exposes enough to write simple primitives that construct and inspect individual terms, but not enough to walk, serialize, or reconstruct arbitrary term graphs. This limits what external plugins can do without modifying HVM4 internals. Bump to ABI v2 and add: Constructors: term_new_era, term_new_ref, term_new_mat Needed to reconstruct complete term graphs including erasure markers, book references, and pattern match nodes. Accessors: term_arity, term_sub_get, term_sub_set Needed to walk term children generically (arity), and to follow or create substitution chains (the SUB bit mechanism that linked binders use for variable resolution). Book/names: table_get, book_get, book_set table_get retrieves a name string by ID (reverse of table_find). book_get/book_set read and write BOOK entries, allowing plugins to inject definitions (e.g. mounting a deserialized term as @name) or read existing ones (e.g. collecting dependencies for serialization). These additions are append-only — existing struct fields are unchanged and existing FFI plugins continue to work after recompilation against the new header (ABI version check catches stale binaries).
o1lo01ol1o
force-pushed
the
ffi-extend-api
branch
from
9c5b318 to
e762a0e
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The current FFI API lets plugins construct and inspect individual terms, but can't walk term graphs generically (term_arity missing), can't follow substitution chains (term_sub_get/term_sub_set missing), can't reconstruct complete graphs (missing term_new_era/ref/mat), and can't inject or read book definitions (book_get/book_set missing).
These are the minimum additions needed to implement serialization, persistence, or any plugin that operates on term subgraphs rather than individual values. All additions are append-only to the struct — existing plugins just need recompilation.
@VictorTaelin My usecase here is for file-backed serialization. Let me know if you have any feedback!