Skip to content

ReScript→AffineScript migration: finish the compiler/src port (modules 7–17) - #30

Merged
hyperpolymath merged 11 commits into
mainfrom
claude/youthful-fermat-90bhhu
Jun 24, 2026
Merged

ReScript→AffineScript migration: finish the compiler/src port (modules 7–17)#30
hyperpolymath merged 11 commits into
mainfrom
claude/youthful-fermat-90bhhu

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Jun 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Completes the entire compiler/src ReScript→AffineScript port (this branch accumulated the batch before the previous PR merged). On top of modules 1–6 already on main, this adds the remaining 11 modules — all independently re-verified green with affinescript check and the full 17-source harness (all .affine sources check.).

Execution path (modules 7–9)

  • Bytecode.affine (251) — 44 opcodes + Value/Chunk/BytecodeProgram.
  • Codegen.affine (526) — AST → bytecode; immutable Compiler threaded; jump backpatching via array rebuild.
  • VM.affine (727) — stack interpreter; runtime errors are values (ExecResult); Echo runtime semantics byte-faithful (OpEchoToResidue debits the erase cost, pushes VResidue, idempotent — the operational detach).

Remaining compiler/src (modules 10–17)

  • Stability (307) · Pretty (515, AST→source printer) · TokenStream (537) · LayerNavigator (333) · Analyzer (233) · FiveWhys (297) · IncrementalLexer (231) · IncrementalParser (332).

Documented omissions (one AffineScript limitation, 3 call sites)

generate_report / analyze_program / create_layer_views build records whose fields are typed Dict<K,V> in the shipped types. Dict<K,V> is effectively a phantom type in AffineScript — accepted in annotations but with no value-level introduction (no literal/constructor/Dict-returning builtin; the stdlib dict is a distinct assoc-list type that doesn't unify). Those records can't be constructed; everything that reads such a field is ported. Closing them needs the Dict fields switched to the idiomatic assoc-list [(K,V)] (or affinescript's Dict made constructable) — a tracked follow-up.

AffineScript bugs surfaced this migration

  1. module resolver dropped imported struct fields — fixed & merged (ReScript→AffineScript migration: toolchain + Types.affine (module 1 of 17) #26). 2. global len/builtin shadow. 3. if-then-tuple E0104. 4. Dict<K,V> phantom type. (2–4 worked around + documented; all worth upstreaming.)

Heads-up: this PR is blocked on the required Check Workflow Staleness check (stale hyperpolymath/standards workflow pins — pre-existing, fails on main too), so auto-merge won't complete until that's resolved or the merge is overridden.

🤖 Generated with Claude Code

https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM

hyperpolymath and others added 10 commits June 23, 2026 15:58
@hyperpolymath @claude
error-lang: replace fabricated ABI "proofs" with machine-checked ones
450c32a 
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
@hyperpolymath @claude
docs: design Error-Lang as a Trope IR front end (trope-particularity …
52f57e0 
…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
@hyperpolymath @claude
docs: qualify external repo paths to clear structural_drift (SD022)
a3c0df8 
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
@hyperpolymath @claude
compiler: begin ReScript->AffineScript migration — port Types.res
27571a3 
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
@hyperpolymath @claude
compiler: fix AffineScript module system to unblock the per-module port
8691fc6 
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
@hyperpolymath @claude
compiler: port Lexer.res -> Lexer.affine
15480f5 
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 @claude
compiler: port Cst.res -> Cst.affine (concrete syntax tree + trivia)
5adb0fb 
Third module. Trivia-preserving CST with source round-trip. Functional port:
classify_trivia loops a `let mut` local; lex_with_trivia folds the raw tokens
carrying the last token in hand, so newline-trailing-trivia and trailing source
attach without array-index mutation. Selective `Types` import (Cst's node kinds
collide with Types' Decl/Stmt constructors). Verified with `affinescript check`.

Omitted, documented in-file:
- node_at: returning a deepest *subtree* needs a node used both to recurse into
  AND to return — not expressible under affine ownership without a shared/clone
  type. Auxiliary (IDE cursor lookup); deferred.
- run_tests: the Console-based test harness is not compiler code.

Encountered an affinescript resolver bug along the way: a local `let len = ...`
shadows the builtin `len` *globally* (so a later `len(xs)` typed as Int). Worked
around by renaming the local; worth an upstream fix in affinescript.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
@hyperpolymath @claude
compiler: port Parser.res -> Parser.affine (recursive-descent parser)
0f89d0d 
Fourth and largest module (1150 lines). Complete error-tolerant recursive-descent
parser, faithful grammar and precedence. Functional state-threading: ParserState
is immutable; producers return (Option<X>, ParserState) and callers thread via
`let (x, st) = f(st)`; ReScript `ref` accumulators became `let mut` locals with
(acc, state) while-loops.

Full coverage: the expression ladder (ternary -> logical-or/and -> equality ->
comparison -> term -> factor -> unary -> postfix -> primary), array/lambda/grouped
primaries, call/index/member postfix chains; type expressions incl. Echo<A,B> /
EchoR<A,B> and the >>-split close-angle; the full statement set incl. gutter-block
error recovery; function/struct/main declarations; and the `parse` driver returning
(Program, [Diagnostic]). Verified green with `affinescript check` and the full
harness (Types/Lexer/Cst/Parser all ok).

Documented faithful deviations: the >>-split token rewrite reproduced via array
rebuild (tokens are immutable); the pre-existing node-`start` quirk reproduced
exactly rather than corrected; minor error-recovery loop hardening to guarantee
progress on a stray token.

AffineScript checker bug found + worked around: an if-statement immediately
followed by a tuple literal in tail position fails with E0104 "Expected a function,
got Unit" (the if's () is applied to the tuple). Used explicit `return (...)`.
Third affinescript bug this migration (after the module-resolver struct-field gap
and the global `len` builtin-shadow); all worth upstreaming.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
@hyperpolymath @claude
compiler: port TypeChecker.res + TypeSuperposition.res -> .affine
17acf9b 
Modules 5 + 6 (1123 + 323 lines), both verified green with affinescript check and
the full harness (all six modules ok).

TypeChecker.affine: the static checker. The .res's shared-mutable env (fresh-var
counter + substitution map) and checkResult.errors are unified into one immutable,
threaded CheckState, returned via (result, CheckState) tuples. The lexical
environment is a frame-stack [[(String, Binding)]] (head = innermost); the
substitution map is an Int-keyed assoc list. Unification is faithful arm-for-arm
including numeric widening and the Echo/EchoR rule: same-kind structural only,
Echo<_,_> deliberately NOT unifying with EchoR<_,_> (erasure is irreversible). The
Echo builtins (echo / echo_to_residue / residue_strictly_loses / echo_input /
echo_output) mirror the .res including the [Stab-Erase] diagnostics. Internal `ty`
constructors are C-prefixed (CInt..CVar) to avoid colliding with Types' TypeExpr.

TypeSuperposition.affine: the quantum-type demo (Collapsed | Superposition(...));
the deterministic collapse index is byte-faithful.

Documented faithful deviations: the .res `exprLoc` helper is omitted — `infer_expr`
returns the expression's own Location (a copyable summary) alongside the type, so
diagnostics keep exact locations without re-traversing a consumed node;
Array.zip/every/forEach over state-mutating callbacks become state-threading folds;
minor local renames to avoid global-constructor collisions. No type rule,
diagnostic, Echo/EchoR behaviour, or collapse arithmetic was changed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
@hyperpolymath @claude
compiler: port Bytecode.res + Codegen.res + VM.res -> .affine
bfcee30 
Modules 7-9 (251 + 526 + 727 = 1504 lines), all verified green with affinescript
check and the full 9-module harness. Completes the core compiler execution path.

Bytecode.affine: 44 opcodes (stack/vars/arith-with-position-metadata/comparison/
control-flow/arrays/haptics/the five Echo ops/print/halt) + Value/Chunk/
BytecodeProgram + value_to_string/opcode_to_string. paradoxType constructors
Px-prefixed to avoid colliding with Types' StabilityFactor::NullPropagation.

Codegen.affine: AST -> bytecode. Immutable Compiler threaded; compile_expr returns
the expression Location (so ExprStmt's trailing OpPop needs no re-traversal of a
consumed node); jump backpatching via array rebuild (set_code_at). Echo lowering
pushes args left-to-right then emits the dedicated OpEcho* op.

VM.affine: stack interpreter. Immutable Vm; stack is a [Value] with an sp mirror;
globals an assoc list. Runtime errors are values (Result + ExecResult =
ExContinue|ExHalt|ExError), not exceptions -- error strings preserved verbatim.
Echo runtime semantics byte-faithful: OpEchoToResidue debits echo_erase_cost (15.0),
erases the witness, pushes VResidue (idempotent on a residue); OpEchoInput errors on
a residue; OpEchoOutput returns the retained output. Pop-order, OpArray ordering,
and OpSub/OpDiv operand order all match VM.res arm-for-arm.

Documented faithful deviations: float pow uses repeated multiplication (integer-
exact; the stdlib has no ln/log) -- the only numeric divergence; the .res
"Not implemented" ops (OpLte/OpGte, OpCall) reproduced exactly; the Console *debug*
disassembler omitted (its pure helpers kept); real VM print/IO kept.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
@hyperpolymath
hyperpolymath marked this pull request as ready for review June 24, 2026 07:39
@hyperpolymath
hyperpolymath enabled auto-merge (squash) June 24, 2026 07:39
@hyperpolymath @claude
compiler: port the remaining 8 compiler/src modules -> .affine
852c215 
Completes the compiler/src ReScript->AffineScript port: all 17 modules are now
.affine. 2785 lines across Stability, Pretty, TokenStream, LayerNavigator,
Analyzer, FiveWhys, IncrementalLexer, IncrementalParser. All verified green with
affinescript check and the full 17-source harness.

- Stability: paradox/consequence/discovery detection + stability arithmetic.
- Pretty: AST->source pretty-printer (immutable Printer threaded through pp_*).
- TokenStream: proc-macro-style token-stream API + of_string lexer.
- LayerNavigator: 5-layer (Grammar/Parser/AST/Semantics/Runtime) views; owns Layer.
- Analyzer: paradox/report formatters, causality, forensic trace.
- FiveWhys: automated root-cause why-chains.
- IncrementalLexer / IncrementalParser: edit-driven re-lex / re-parse + splice.

Documented omissions (one AffineScript limitation, three call sites): the
record-constructor functions generate_report (Stability), analyze_program
(Analyzer) and create_layer_views (LayerNavigator) build records whose fields are
typed Dict<K,V> in the shipped types. Dict<K,V> is effectively a PHANTOM TYPE in
AffineScript -- accepted in annotations but with no value-level introduction (no
literal, no constructor, no Dict-returning builtin; the stdlib `dict` is a distinct
assoc-list type that does not unify). Those records therefore cannot be
constructed; every function that READS such a field is ported. Closing them needs
the Dict fields switched to the idiomatic assoc-list representation [(K,V)] (or
affinescript's Dict made constructable) -- tracked as a follow-up. format_diagnostic
is reimplemented locally (byte-faithful) since the shipped Types.affine omitted it.

Confirmed all three prior affinescript bugs (builtin-shadow bit once via a `length`
param). The Dict phantom-type is the fourth distinct affinescript limitation found
this migration.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
@hyperpolymath hyperpolymath changed the title ReScript→AffineScript migration: Bytecode + Codegen + VM (modules 7–9) ReScript→AffineScript migration: finish the compiler/src port (modules 7–17) Jun 24, 2026
@hyperpolymath
hyperpolymath disabled auto-merge June 24, 2026 08:15
@hyperpolymath
hyperpolymath merged commit b5b124a into main Jun 24, 2026
5 of 6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@hyperpolymath