Merged
Conversation
arthurpaulino
force-pushed
the
aiur-interpreter
branch
2 times, most recently
from
5d1a7a7 to
e61a7f0
Compare
Reason is that checking a term is useful whether you want to compile or not
- Kernel.lean: --dbg flag runs the interpreter instead of bytecode execution - Interpreter: IOBuffer added to state, IO operations fully implemented, assertEq generalized to any Value, u8Sub returns (result, underflow) tuple, debug prints label and optional value - Flatten/unflatten functions for converting between structured Values and flat Array G (matching bytecode layout) - Tests/Aiur/Common.lean: every test case now also runs the interpreter and checks that output and IOBuffer match bytecode execution
gabriel-barrett
force-pushed
the
aiur-interpreter
branch
from
e61a7f0 to
be08970
Compare
Use a single `store : IndexMap (Array Value) Unit` instead of separate `heap : Array Value` and `storeCache : Std.HashMap Value Nat` fields. Replace derived BEq on Value with a manual DecidableEq instance (via mutual recursion through Array/List) so that IndexMap's EquivBEq and LawfulHashable requirements are satisfied without sorry.
arthurpaulino
force-pushed
the
aiur-interpreter
branch
from
a47175f to
ff1ee7d
Compare
samuelburnham
approved these changes
Apr 9, 2026
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
3 participants
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.
This PR implements an interpreter of Aiur terms, used for debugging. Features