refactor: introduce generic Env<T> and consolidate environment handlng#46
Merged
iljakuklic merged 4 commits intodevelfrom Apr 6, 2026
Merged
refactor: introduce generic Env<T> and consolidate environment handlng#46iljakuklic merged 4 commits intodevelfrom
iljakuklic merged 4 commits intodevelfrom
Conversation
…ng (closes #31) Add `common::env::Env<T>`, a level-indexed environment backed by a Vec with typed `depth()`/`push`/`pop`/`truncate`/`get(Lvl)` accessors. Port all four environment sites to use it: - `core/pretty.rs`: `Vec<&Name>` → `Env<&Name>` - `core/value.rs`: `Vec<Value>` type alias → `Env<Value>`; `eval`, `eval_pi`, `eval_lam` now take `&Env` instead of `&[Value]` - `checker/ctx.rs`: three parallel vecs (`names`, `env`, `types`) → single `Env<CtxEntry>` with a `value_env()` helper - `staging/mod.rs`: inner `Vec<Binding>` → `LevelEnv<Binding>` Also fix `Ix::lvl_at` to return `Lvl` instead of `Self`, and add `Display` to `Lvl`, `Ix`, and `Depth` via `derive_more`. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
iljakuklic
commented
Apr 6, 2026
Address all 12 review comments on Env<T> with the following improvements: T1: Add De Bruijn index (Ix) based access and conversion methods: - Rename get/get_mut → get_at_lvl/get_at_lvl_mut - Add ix_to_lvl/lvl_to_ix conversion helpers - Add get_at_ix/get_at_ix_mut for direct index access - Implement Index<Ix>/IndexMut<Ix> traits - Simplify call sites in pretty.rs and staging/mod.rs T2: Add predicate-based and name-based lookup methods: - Add find_innermost<F>() for generic innermost-first search - Add lookup<N, F>() for name-based lookup with key extractor - Simplify Ctx::lookup_local to use the new lookup() method T3: Rename and remove iterator methods: - Rename iter() → iter_by_lvl() for clarity (oldest-first = by level) - Remove unused iter_mut() method - Update all call sites in value.rs and ctx.rs T4: Widen iter_with_lvl() trait bounds: - Declare impl DoubleEndedIterator + ExactSizeIterator - No implementation change needed, just accurate bounds T5: Replace extend() method with Extend trait impl: - Remove pub fn extend() - Implement std::iter::Extend<T> trait - Call sites unchanged (same method name) T6: Add FromIterator impl and simplify inst_n: - Implement FromIterator<T> for Env<T> - Replace two-step extend in inst_n with single collect() T7: Clean up documentation: - Trim struct doc comment to first line only - Remove premature panic documentation blocks T8: Fix misleading variable name in pretty.rs: - Rename env_before → depth_before (it holds a Depth, not an Env) All tests pass (55 snapshots, 0 failures). CI clean (no clippy warnings). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Replace get_at_ix/get_at_lvl method calls with idiomatic indexing operators now that Index<Ix>/Index<Lvl> traits are implemented. This is cleaner and more consistent with Rust conventions. Changes: - pretty.rs: env.get_at_ix(*ix) → &env[*ix] - value.rs: env.get_at_ix(*ix) → env[*ix] - value.rs: doc comment updated to reference env[lvl] - staging/mod.rs: self.bindings.get_at_ix(ix) → &self.bindings[ix] Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Break up the iterator chain in inst_n to name the closure environment iterator separately, making the code structure clearer. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
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.
Add
common::env::Env<T>, a level-indexed environment backed by a Vec with typeddepth()/push/pop/truncate/get(Lvl)accessors.Port all four environment sites to use it:
core/pretty.rs:Vec<&Name>→Env<&Name>core/value.rs:Vec<Value>type alias →Env<Value>;eval,eval_pi,eval_lamnow take&Envinstead of&[Value]checker/ctx.rs: three parallel vecs (names,env,types) → singleEnv<CtxEntry>with avalue_env()helperstaging/mod.rs: innerVec<Binding>→LevelEnv<Binding>Also fix
Ix::lvl_atto returnLvlinstead ofSelf, and addDisplaytoLvl,Ix, andDepthviaderive_more.