Skip to content

Refactor DialectFileMap to use IO.Ref for LoadedDialects#516

Merged
joehendrix merged 2 commits intomainfrom
jhx/filemap
Mar 5, 2026
Merged

Refactor DialectFileMap to use IO.Ref for LoadedDialects#516
joehendrix merged 2 commits intomainfrom
jhx/filemap

Conversation

@joehendrix
Copy link
Copy Markdown
Contributor

@joehendrix joehendrix commented Mar 4, 2026

Summary

This PR replaces the pure DialectFileMap.preloaded field with a mutable
IO.Ref LoadedDialects, eliminating the need to thread LoadedDialects
through parameters and return types across every dialect-loading call
site.

The main benefit is that strata print and other DDM CLI subcommands should be much easier to work with since they don't require dialects that are already precompiled into Strata.

Details

  • Mutable ref in DialectFileMap. Added loaded : IO.Ref LoadedDialects with new, getLoaded, modifyLoaded helpers.
  • Removed LoadedDialects threading. Removed LoadedDialects from
    parameters and return tuples throughout the dialect-loading mutual
    block, public API (loadDialect, elabDialect), Util/IO, and
    SimpleAPI. Functions now read/write the ref directly.
  • Removed DialectState.loaded field. Added getLoadedDialects in
    DialectM that reads from the ref, eliminating the sync pattern and
    stale-snapshot risk.
  • Simplified LoadDialectCallback. Reduced from two-argument
    callback returning a pair to a single-argument callback.
  • Refactored text dialect loading. Extracted header parsing into
    readDialectTextfileHeader; made loadDialectFromPath private with
    a public loadDialectFromFile wrapper.
  • Preload production dialects. Core, Laurel, Python, PythonSpecs and the SMT family are
    now registered in buildDialectFileMap so strata DDM commands do not need them added as arguments.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@joehendrix joehendrix force-pushed the jhx/filemap branch 2 times, most recently from 22b3f8c to dfaac22 Compare March 4, 2026 23:11
@joehendrix joehendrix marked this pull request as ready for review March 4, 2026 23:31
@joehendrix joehendrix requested a review from a team March 4, 2026 23:31
@shigoel shigoel enabled auto-merge March 5, 2026 00:31
Simplify dialect-loading by replacing the pure `preloaded` field with a
mutable `IO.Ref`, eliminating the need to thread `LoadedDialects` through
return types across every call site.

- Replace `DialectFileMap.preloaded` with `DialectFileMap.loaded : IO.Ref
  LoadedDialects`; add `new`, `getLoaded`, `modifyLoaded` helpers
- Remove the `LoadedDialects` element from return tuples in the mutual
  block (`loadDialectFromIonFragment`, `loadDialectFromPath`,
  `loadDialectRec`, `elabDialectRest`) and public wrappers (`loadDialect`,
  `elabDialect`)
- Remove `DialectState.loaded` field; add `getLoadedDialects` helper in
  `DialectM` that reads directly from `DialectContext.loadedRef`,
  eliminating the sync pattern and stale-snapshot risk
- Simplify `LoadDialectCallback` from
  `LoadedDialects → DialectName → BaseIO (LoadedDialects × Except ...)`
  to `DialectName → BaseIO (Except ...)`
- Simplify `readStrataText`, `readStrataIon`, `readFile` return types in
  Util/IO and SimpleAPI from `IO (LoadedDialects × ...)` to `IO ...`
- Make `loadDialectFromPath` private; add public `loadDialectFromFile`
  wrapper for the `#load_dialect` call site in HashCommands
- Extract `readDialectTextfileHeader` from the mutual block for header
  parsing; inline `readDialectTextfile` body into `loadDialectFromPath`
- Preload production dialects (Core, Laurel, SMT, SMTCore, SMTResponse,
  smtReservedKeywordsDialect) in `buildDialectFileMap` alongside Python
  and PythonSpecs
- Change `DialectFileMap.ofDirs` to accept an `init` parameter and
  `addEntry` to preserve existing map fields with `{ m with ... }`
- Fix `printCommand` to use `exitFailure` instead of silent return on
  internal error
- Fix line lengths and complete truncated `DialectFileMap` docstring

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Comment thread StrataMain.lean
Comment thread Strata/DDM/Elab.lean
Copy link
Copy Markdown
Contributor

@shigoel shigoel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, left a couple of questions for my own understanding.

@joehendrix joehendrix disabled auto-merge March 5, 2026 17:55
@joehendrix joehendrix added this pull request to the merge queue Mar 5, 2026
Merged via the queue into main with commit 20e4449 Mar 5, 2026
15 checks passed
@joehendrix joehendrix deleted the jhx/filemap branch March 5, 2026 18:21
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.

3 participants