Open
Conversation
Keep plan files local to working trees, not tracked in git. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
When inserting a tile, select a mold appropriate for the local sort context rather than just taking the first available mold. This prevents wrong-sort molds (e.g., Exp mold for `-` in a Pat context) from being assigned during insertion. - Form.Molds: split into get_base, try_get (strict), try_get_permissive, and get (with fallback). Strict filtering for remolding, permissive for insertion (allows wrong-sort multi-delimiter forms to expand) - Relatives.sort: compute local sort at insertion point from left sibling's right nib (handles heterogeneous infix like `:`) - Insert.re: use sort-aware Form.Molds.get - Segment.remold_tile: use strict try_get - Ancestor.re: remove unused functions 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Expansion now considers sort context when deciding how to expand delimiters. This prevents wrong-sort expansions (e.g., `let` expanding in Pat context) and enables sort-specific forms (e.g., `[` expanding to ListLitPat vs ListLitExp based on context). Key changes: - Form.re: Register expansions using nib sort (the context you're typing in) rather than mold.out (what the form produces). Rul context is permissive and falls back to any expansion since rules contain Exp/Pat operands but have no operand forms of their own. - Insert.re: Handle `|` entirely here when inside case expressions, bypassing sort-specific lookup. This is needed because ascriptions (expr : Type) have Typ right nib even though they produce Exp. - TyDiForms.re: Pass sort to Form.Expansion.get. See plans/sort-specific-expansion.md for detailed analysis of the case/rule structure and known limitations. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add Mod sort for module-level items - Add module forms: ModBody, ModSeq, ModLet, ModType - Add mk_pre' helper for heterogeneous prefix forms (body sort differs from out) - Add MakeTerm parsing for modules with semicolon sequence flattening - Add remold_mod function with Exp fallback for bare expressions - Add CSS styling for Mod sort (greenish color) - Add Module(list(Mod.t)) to exp_term for module expressions - Add stubs in dynamics/statics for Module expression type Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
In Insert.re: When in Mod context and no Mod expansion exists, try Exp (allows if/test/etc forms to expand inside module bodies). Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Module expansion: - ExpandModule.re: Transform module syntax into nested let/type + labeled tuple - Statics.re: Type-check modules by expanding and checking expanded form - Elaborator.re: Elaborate modules directly to expanded form Menhir parser: - AST.re: Add Module and mod_item types - Lexer.mll: Add OPEN_CURLY and CLOSE_CURLY tokens - Parser.mly: Add modItem rule and module expression grammar - Conversion.re: Add ModItem conversion functions - Grammar.re: Add mod_ type alias for Factory module Also includes formatting fixes from dune fmt. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Statics tests: - Empty module - Single and multiple bindings - Shadowing behavior - Type aliases - Bare expressions - Module access via dot notation - Module as labeled tuple Evaluator tests: - Module evaluation to labeled tuple - Access via dot notation - Sequential bindings - Type aliases - Shadowing 2 tests skipped for features not yet fully working: - Nested modules - Module with function binding access All 1446 tests pass. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Fixes:
- Empty module atomic form: {} now creates atomic EmptyModule token
(like () and []) instead of compound form with hole. Added {} to
Token.is_potential_token and EmptyModule to Form.re atomic forms.
- Singleton labeled tuple pattern bug: Fixed incorrect elaboration
when Var pattern has Unknown synth type. Now only elaborates
(destructures) if pattern name matches the tuple label.
e.g., `let m = (y=1) in m` now correctly has type (y=Int), not Int.
Documentation:
- Added detailed Menhir parser section explaining semicolon ambiguity
(shift-reduce conflict between Seq and module item separator) and
potential fix options (grammar duplication, GLR, lexer hack, etc.)
- Replaced incomplete "Capitalized Names in Patterns" section with
comprehensive "Capitalized Module Names: Design Considerations"
covering both pattern/binding AND expression/reference sides,
with analysis of 5 options and trade-offs. Decision deferred.
Tests:
- All 1461 tests pass
- Added nested module tests to Test_MakeTerm.re
- Expanded statics and evaluator module tests
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This commit enables cursor inspector support for module constructs by: 1. Preserving IDs on wrapper expressions during module expansion: - ModLet ID → wrapper Let expression - ModType ID → wrapper TyAlias expression - ModExp uses fresh ID (synthetic, inner expr has its own IDs) 2. Absorbing semicolon IDs in MakeTerm (like ListLit absorbs comma IDs): - Module expression now includes semicolon IDs from inner Mod sequence - Enables cursor inspector to show info for both braces and semicolons 3. Using fresh IDs for the final labeled tuple: - Prevents overwriting Module statics map entry - Avoids infinite loops in Elaborator Key insight: ModExp differs from ModLet/ModType - it wraps an existing expression that already has its own IDs. The synthetic let _ = e wrapper needs a fresh ID to avoid conflicts. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Use is_mod_seq to handle any number of semicolons (not just 2 items) - Only absorb IDs when body is MultiHole (avoids duplicating single-item IDs) - Fixes infinite loop that occurred with single-item modules Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add semicolons to is_chainable when both tiles have mold.out == Sort.Mod. This produces flat Bin structures for module semicolons (like commas do for tuples), instead of nested binary structures. CellJoin (Exp-sort semicolons) is unaffected due to the Sort.Mod guard. Flat structure means is_mod_seq in MakeTerm sees all semicolons at once, which is prerequisite for collecting all semicolon IDs for cursor inspector. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
With flat Skel structure, body.annotation.ids now contains ALL semicolon IDs for multi-item modules. The existing MultiHole absorption path in MakeTerm naturally handles this. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add signature (Sig) sort for module type annotations:
- Sig sort infrastructure parallel to Mod (Sort, Grammar, Form,
Segment, Skel, Arms, Insert, MakeTerm)
- Sig as Typ variant with desugar_sig bridge to labeled tuples
- Type-directed module expansion for error attribution
- Cursor inspector integration (Mod/Sig cls, colors, bolding)
- Menhir parser support for Sig syntax
- ExpToSegment: full Module and Sig pretty-printing with whitespace
- Sig pretty_print in Typ.re for cursor inspector display
- Module abbreviation in Abbreviate.re
Tests added across 8 test files (1502 total, all pass):
- 14 statics, 11 evaluator, 4 elaboration, 6 ExpToSegment roundtrip,
4 editing, 2 abbreviation, 5 Menhir Sig roundtrip tests
Bug fixes:
- ExpToSegment: wrap mod/sig items with secondary for whitespace
- ExpToSegment: ModType mk_form children count (1 inner sort, not 2)
- Typ.re: Sig pretty_print renders { let x : Int } not {sig}
- Abbreviate.re: recursive module item abbreviation
Docs and plans consolidated.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Module width mismatches (sig wider/narrower than module) now produce
type errors. The fix builds the actual Prod type from the module's
exported bindings rather than using expanded_info.ty, which masked
width errors via fixed_typ_exp.
Empty module signatures ({} in type position) now parse correctly
as Sig([]) by adding a Typ mold to the EmptyModule atomic form.
Adds 16 new statics tests covering sig annotations, width errors,
and module/tuple equivalence limitations. Updates modules doc slide.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
In Mod/Sig sort context, concave grout now uses mod_seq precedence (very loose) instead of concave_grout (tight). This means deleting a semicolon between module items leaves them as separate items rather than absorbing everything into one broken expression body. Threaded via optional ~sort parameter on Skel.mk and Segment.skel, defaulting to Exp. MakeTerm passes the child sort from tile molds. Also makes flatten_mod/flatten_sig handle non-Mod/Sig children in multi-holes by wrapping them as module items, isolating parse breakage. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Add InfoMod and InfoSig record types and variants to Info.t - Update all Info.re helpers (sort_of, cls_of, ctx_of, etc.) - Statics: create InfoSig for Sig items, InfoMod for edge cases - Statics: Mod items inside Module() stay as InfoExp with Mod cls (elaborator needs InfoExp data for expansion wrappers sharing IDs) - CursorInspector: Mod/Sig items show empty div (cls shown by term_view) - ExplainThis: 6 data files for Module, ModLet, ModType, Sig, SigLet, SigType - ExplainThis: dispatcher handles InfoMod, InfoSig, and InfoExp with Mod cls - Rename Mod cls strings: "Let definition" -> "Let declaration" - Update ErrorPrint, ChatLSP for new Info variants - Remove plans/ from tracking (gitignored) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Without this, { and } are treated as potential operator characters,
which prevents them from being recognized as paired delimiters for
module syntax.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Preserve adopted IDs original sort in consolidate_adopted so ModSeq/SigSeq semicolons keep sort:Mod/Sig instead of being overwritten with Exp/Typ. Narrow defs_exclude_bodies match to let/type/=/in labels. Set Mod/Sig sort colors to neutral stone and type color respectively. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Process module expansion in syn mode so type inconsistencies are only reported on the Module expression itself, not also on the internal expansion tuple. Add Sig to is_module check in Arms.re for semicolon decoration. Update docs/modules.md formatting and remove resolved ExplainThis crash section. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The Menhir parser failed on multi-item modules like `{ let x = 1; let y = 2 }`
because `;` was ambiguous between Seq (expression sequencing) and the module
item separator. Add MOD_ITEM_EXP precedence level above SEMI_COLON so the
parser reduces exp to modItemExp rather than shifting `;` for Seq.
Unskip Menhir tests for multi-item modules and type alias modules. Unskip
evaluator tests for function bindings and nested modules (both were already
working but untested).
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…or subsystems, tests Add `module` keyword with MPat sort for capitalized module name bindings. Implement ModuleExp/ModuleMod term variants with statics expansion to Let/ModLet. Add capitalized-name-as-variable fallback in Statics.re and Elaborator.re. Polish all editor subsystems: ExpToSegment (Mod/Sig/MPat pretty-printing), ErrorPrint, Abbreviate, ChatLSP, SyntaxTest, Exercise, CursorInspector, ExplainThis (6 data files), Equality (alpha-equivalence for modules). Fix Menhir parser: singleton labeled tuple types, capitalized dot names, QUOTED_LABEL as exp production, QCheck round-trip normalization. 73/73 pass. Auto-probe: skip module declarations (ModLet/ModType/ModuleMod), probe their definition subexpressions instead. Bare expressions (ModExp) still probed. 1036 tests pass (4 pre-existing Pattern Coverage failures unrelated). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…sitions Thread dot_labels through Statics, Info, and TyDi so that typing a label prefix after a dot (e.g. m.le) suggests available fields (e.g. length). Labels are extracted from the normalized type of e1 (Prod or List(Prod)) in the Dot case. Also check label_sort in TyDi to suppress non-label suggestions (variables, function applications) in all dot positions, not just when cls happens to be Label. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
New Test_TyDi module with 26 tests across 8 categories: DotLabel, Variables, Constructors, Operands, LeadingForms, Operators, Types, and Suppression. Tests use the caret convention from Test_Editing to position the cursor and verify the suggestion buffer output. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add qualified module member completions to TyDi: typing a module name prefix in a typed position now suggests Module.member or Module.member( based on field types and expected type. Fix base type names (String, Int, etc.) leaking into Exp/Pat operand suggestions with Unknown type. Filter base_typs from const_mono_exp and const_mono_pat in TyDiForms. Update Token.base_typs to include all 6 base types (Bool, Float, Int, Nat, SInt, String) with cross-reference comments to Ctx.is_base_typ. Rename ModuleExp cls to Module definition, ModuleMod cls to Module declaration. Update ExplainThis descriptions accordingly. Update Modules doc slide to use module keyword syntax throughout. Add Select.re support for module keyword in current_term selection. Clean up modules-pre-merge.md (completed items removed). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## dev #2123 +/- ##
==========================================
+ Coverage 50.12% 51.30% +1.18%
==========================================
Files 231 235 +4
Lines 25516 27014 +1498
==========================================
+ Hits 12789 13860 +1071
- Misses 12727 13154 +427
🚀 New features to boost your workflow:
|
…s, MultiHole rendering - remold_typ_uni: check Sort.Sig (not just Sort.Mod) when handing semicolons back to parent sort, fixing type declarations in signatures - flatten_sig: preserve non-Sig children as MultiHole instead of discarding as EmptyHole, matching flatten_mod behavior - ExpToSegment: render Mod/Sig MultiHole items via any_to_pretty instead of "?" - Segment.skel: document removed memoization and rationale - docs/modules.md: remove ExplainThis crash from Known Limitations (already fixed) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Inject TVarEntry for module bindings so type-level M.T resolves through lookup_alias → ProdProjection → project_type. Also fix capitalized label quoting and dot spacing for constructor names in type display. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Phase 1b: Propagate TVarEntry for variable/module aliasing so `let n = M in n.T` and `module N = M in N.T` resolve type exports. Phase 1c: 10 new statics tests for qualified type access (basic, multiple exports, internal refs, nested, lowercase, aliasing, chained). Phase 1d: Add bound_qualified_types to TyDi for type-position dot-completion suggestions (M.T, M.U etc). Phase 1e: Improve InvalidLabel error messages to say "Member X not found. Available: ..." instead of "Invalid label". Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Add type-level dot completion in TyDi (suggest type members after M. in type position) - Remove bound_qualified_types from general type suggestions (never suggest full qualified names) - Fix nested module aliasing in collect_type_exports (module Geo = Geometry propagates type exports) - Add Constructor-to-Var fallback in get_binding_site for jump-to-definition on module names - Add DotTyp.re explain-this for type-level dot projection (M.T) - Wire ProdProjection to DotTyp in ExplainThis.re - Add 3 TyDi tests (prefix match, exact match, no match for type-level dot) - Add 3 statics tests (nested with values, nested alias, nested alias with sibling type) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Update docs/modules.md with qualified type access, aliasing, and architecture sections - Update Modules.ml doc slide with semantic examples and new feature coverage Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
cyrus-
requested changes
Feb 18, 2026
Member
cyrus-
left a comment
cyrus-
left a comment
There was a problem hiding this comment.
- auto probe on a module binding shouldn't probe the signature
- auto probe on a module binding shouldn't probe the body
- make referencing a bare module name an error
cyrus-
requested changes
Feb 18, 2026
Member
cyrus-
left a comment
cyrus-
left a comment
There was a problem hiding this comment.
additional:
- hole in module bodies says "Whitespace or Comment" in the cursor inspector
Member
|
additionally either in this PR or make an issue for removing the type alias shadowing restriction: |
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
2 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.
Replaces #2104.
This adds a basic version of modules, suitable for namespacing and code organization, which is really just a syntactic gloss over labelled tuples. This is intended to be transitional progress toward a full modules system including proper statics and dynamics. However this does now include module keyword syntax, capitalized module variables, and type member access; see docs slide and docs.
See docs here for a comprehensive description