ReScript→AffineScript migration: Lexer.affine (module 2) - #27
Merged
Conversation
The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded,
positionalDeterministic, paradoxMonotonic) were not proofs: each fabricated
its evidence with cast ()/cast Refl over an IO action. Replace them with
genuine, self-contained Idris2 modules, machine-checked under Idris 2 v0.8.0
(no believe_me / assert_total / cast / postulate):
- Stability.idr : stability score is bounded in [0,100] (clamp model of
compiler/src/Types.res calculateStability).
- Positional.idr : positional-operator behaviour is deterministic over the
pure model of the Zig FFI (a genuine Refl, not IO cast Refl).
- Paradox.idr : the two threshold-gated factors are monotone; the blanket
"paradox detection monotonic" claim is RETRACTED -- proving
it honestly surfaced that scope_leakage is prime-gated and
therefore non-monotone (line 7 prime, line 8 not).
Foreign.idr is reduced to an honest, self-contained ABI binding layer.
Add error-lang-abi.ipkg and verification/check-proofs.sh (idris2 --check all
four modules). Rewrite PROOF-NEEDS.md to record what is proved, what is
retracted, the toolchain, and open conformance obligations.
The language's satirical "100% production-ready / formally verified"
self-presentation in README/WHITEPAPER is intentional and left intact; this
change only makes the underlying proof artifacts real and honest.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
…integration) Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented) for lowering Error-Lang's Echo operations and stability factors to the language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile) and consuming the verified verdict + witness. - Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <-> FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/ detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable), matching the [Stab-Erase] debit and "decomposition must be visible". - stabilityFactor -> grade mapping; the silent instabilities (GlobalState, RaceCondition) land on the deceptive Conflated bottom -> a lowering fault under the prevent profile. - Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/ p-insufficient + witness edge (the invariant-path argmin Stability.idr already reasons about). - Architecture (reference, never vendor; schema is the trust boundary), the per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/ L-Floor), and a 4-phase plan. Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and trope-particularity-workbench by URL only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the trope-integration design as dangling references "surviving a directory rename". Both are deliberately *external*: the trope-checker repo's Idris2 core and the panic-attack repo's aggregate module. Reword as unambiguously external (drop the bare `src/<dir>/` form) so the heuristic no longer reads them as internal error-lang tree paths. No substantive content change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
First module of the compiler's migration to AffineScript (the Hyperpolymath language policy bans ReScript). Adds compiler/src/Types.affine, a faithful port of compiler/src/Types.res, verified green with `affinescript check`: - all token / AST / error / stability types (structs + enums + match) - ReScript inline-record variants lowered to positional constructor args - token variants Float/String renamed FloatTok/StringTok (reserved type keywords in AffineScript) - Echo types (TyEcho / TyEchoResidue) shaped Trope-IR-ready per docs/Trope-Particularity-Integration.adoc (Phase 0) - make_default_state, stability_impact, calculate_stability, error_code_to_string Toolchain, so the .affine sources are reproducibly CI-verifiable: - scripts/install-affinescript-toolchain.sh — builds the AffineScript compiler from distro OCaml packages (independent of opam.ocaml.org) + installs the binary and stdlib under a discoverable share/ path - verification/check-affinescript.sh — typechecks all compiler/src/*.affine Types.res is retained until its dependents migrate; format_diagnostic is deferred pending the string / affine-borrow pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
The .res -> .affine port needs sibling compiler modules to import the shared AST
(Location/Token/Position/...) from Types. AffineScript's module resolver exported
imported enum constructors but dropped imported struct/alias type definitions, so
cross-module struct field access failed ("Field not found"). Per the chosen
approach (fix the resolver, not single-file/accessors):
- patches/affinescript-module-struct-fields.patch: threads imported modules'
type_env + constructor_env into the importing module's typecheck context
(typecheck.ml check_program gains ?import_type_env/?import_constructor_env;
resolve.ml import_type_defs copies them across all three import forms;
bin/main.ml passes them at the check/compile/eval entry points). Documented in
patches/README.adoc; pending upstream to hyperpolymath/affinescript.
- compiler/src/Types.affine: now a proper `module Types;` with `pub` exports.
- verification/check-affinescript.sh: checks from compiler/src so `use Types::{...}`
resolves via the loader's current-dir search.
- scripts/install-affinescript-toolchain.sh: applies the patch after cloning,
before building (idempotent).
Verified: a module importing Types' structs with nested field access, struct
construction, and enum-field matching type-checks; affinescript's own stdlib
cross-module imports (http_fetch/option/io) still pass.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Second compiler module. Lexer.affine imports Types (`use Types::*;`) and ports the tokenizer in AffineScript's functional style: with no mutable struct fields or record-spread, state-mutating helpers take a LexerState and return a new one, and the scanners + driver loop a `let mut` local. Single chars are Char (char_at / char_to_int); lexemes and the escape buffer use substring; numeric literals use the parse_int / parse_float builtins; the keyword Dict becomes a string-equality lookup. Verified green with `affinescript check`. Faithful for the core path (identifiers/keywords, decimal int + float + exponent, strings with escapes, all operators/delimiters, comments, newline + EOF, error recovery + diagnostics E0001-E0004). Documented parity gaps for a follow-up pass: hex/binary integer prefixes, triple-quoted strings + \0 escape, smart-quote E0007. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
hyperpolymath
marked this pull request as ready for review
June 24, 2026 06:38
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.
What
Ports
compiler/src/Lexer.res→compiler/src/Lexer.affine(the tokenizer), verified green withaffinescript check. Builds on the merged module-system fix:Lexer.affinedoesuse Types::*;and freely usesTypes' structs/enums across the module boundary.The state-threading pattern (applies to all stateful modules)
AffineScript has no mutable struct fields and no record-spread, so the imperative ReScript lexer is rendered functionally:
LexerStateand return a new one (full-record reconstruction);let mutlocal (let mut s = …; while … { s = step(s) }) — affine-clean, since each state value flows linearly.Other mechanics: single chars are
Char(char_at→Option<Char>,char_to_intfor codes); lexemes and the escape buffer usesubstring; numeric literals use theparse_int/parse_floatbuiltins; the keywordDictbecomes a string-equality lookup. This is the template forParser/VM/TypeChecker.Faithful vs documented gaps
Faithful: identifiers/keywords, decimal integer + float + exponent, strings with escapes, every operator/delimiter (incl. multi-char
->==!=<=<<>=>>), comments, newline + EOF tokens, and error recovery with diagnostics E0001–E0004.Tracked parity gaps (decimal/core path is faithful; noted in-file for a follow-up pass): hex (
0x) / binary (0b) integer prefixes, triple-quoted strings +\0escape, and smart-quote (U+201C/U+201D) detection (E0007).Status
Roadmap: ✅ Toolchain · ✅ Types · ✅ Module-system unblock · ✅ Lexer · next:
Cst/Parser.Lexer.resretained until dependents migrate. PR will show the pre-existingCheck Workflow Stalenessred (stalestandardspins; fails onmaintoo).🤖 Generated with Claude Code
https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Generated by Claude Code