Skip to content

kframework_ffi: Fixes and Improvements#11

Merged
tothtamas28 merged 5 commits into
masterfrom
marshaller-fixes
May 8, 2026
Merged

kframework_ffi: Fixes and Improvements#11
tothtamas28 merged 5 commits into
masterfrom
marshaller-fixes

Conversation

@gtrepta
Copy link
Copy Markdown
Contributor

@gtrepta gtrepta commented May 8, 2026

Fixed a problem with kllvm::Marshaller where caching Symbols caused inj lookups to produce incorrect sorts. Symbol caching is being disabled for now.

Fixed a problem where there wasn't a proper representation for marshalling over Bytes domain values. Created Str::to_kore for this.

Added fmt::Display for kllvm::Block. This lets you get a kore string from a block without needing to convert it to a kllvm::Pattern first.

gtrepta added 3 commits May 7, 2026 19:45
There was a bug here where the 'inj' symbol got interned and was reused
for every production with the wrong sorts. The symbol interning is being
left unused for now until this is investigated some more.
@tothtamas28 tothtamas28 merged commit 490532e into master May 8, 2026
2 checks passed
@tothtamas28 tothtamas28 deleted the marshaller-fixes branch May 8, 2026 08:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants