Skip to content

Commit 727c428

Browse files
ReScript→AffineScript migration: toolchain + Types.affine (module 1 of 17) (#26)
* error-lang: replace fabricated ABI "proofs" with machine-checked ones 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 * docs: design Error-Lang as a Trope IR front end (trope-particularity 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 * docs: qualify external repo paths to clear structural_drift (SD022) 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 * compiler: begin ReScript->AffineScript migration — port Types.res 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 * compiler: fix AffineScript module system to unblock the per-module port 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 --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 4766c27 commit 727c428

5 files changed

Lines changed: 527 additions & 0 deletions

File tree

compiler/src/Types.affine

Lines changed: 241 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,241 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Types.affine — core type definitions for Error-Lang
3+
// Ported from compiler/src/Types.res. Port conventions:
4+
// * ReScript inline-record variants -> positional constructor args.
5+
// * array<T> -> [T]; option<T> -> Option<T>; dict<k,v> -> Dict<k,v>; tuples kept.
6+
// * Token variants `Float`/`String` renamed `FloatTok`/`StringTok`
7+
// (`Float`/`String` are reserved type keywords in AffineScript).
8+
//
9+
// This is the `Types` module; sibling compiler modules `use Types::{...}`.
10+
// Cross-module struct field access requires the affinescript module-resolver
11+
// fix in patches/affinescript-module-struct-fields.patch.
12+
13+
module Types;
14+
15+
use prelude::*;
16+
17+
pub struct Position {
18+
line: Int,
19+
column: Int,
20+
offset: Int
21+
}
22+
23+
pub struct Location {
24+
start: Position,
25+
end_: Position,
26+
file: String
27+
}
28+
29+
pub enum TokenType {
30+
// Keywords
31+
Main, End, Let, Mutable, Function, Struct, If, Elseif, Else, While, For, In,
32+
Break, Continue, Return, And, Or, Not, True, False, Nil, Gutter, Fn,
33+
// Types
34+
TInt, TFloat, TString, TBool, TArray, TEcho, TEchoR,
35+
// Literals
36+
Integer(Int),
37+
FloatTok(Float), // ReScript Float(float)
38+
StringTok(String), // ReScript String(string)
39+
Identifier(String),
40+
// Operators
41+
Plus, Minus, Star, Slash, Percent, EqualEqual, BangEqual, Less, Greater,
42+
LessEqual, GreaterEqual, Ampersand, Pipe, Caret, Tilde, LessLess, GreaterGreater,
43+
Equal, Arrow, Question, Colon,
44+
// Delimiters
45+
LParen, RParen, LBracket, RBracket, LBrace, RBrace, Comma, Dot,
46+
// Special
47+
Newline, EOF, Error(String)
48+
}
49+
50+
pub struct Token {
51+
type_: TokenType,
52+
lexeme: String,
53+
loc: Location
54+
}
55+
56+
// ============================================
57+
// AST
58+
// ============================================
59+
60+
pub enum Expr {
61+
IntLit(Int, Location),
62+
FloatLit(Float, Location),
63+
StringLit(String, Location),
64+
BoolLit(Bool, Location),
65+
NilLit(Location),
66+
Ident(String, Location),
67+
Array([Expr], Location),
68+
Binary(Expr, BinaryOp, Expr, Location),
69+
Unary(UnaryOp, Expr, Location),
70+
Call(Expr, [Expr], Location),
71+
Index(Expr, Expr, Location),
72+
Member(Expr, String, Location),
73+
Ternary(Expr, Expr, Expr, Location),
74+
Lambda([Param], Option<TypeExpr>, LambdaBody, Location)
75+
}
76+
77+
pub enum BinaryOp {
78+
Add, Sub, Mul, Div, Mod,
79+
Eq, Neq, Lt, Gt, Lte, Gte,
80+
BAnd, BOr, BXor, Shl, Shr,
81+
LAnd, LOr
82+
}
83+
84+
pub enum UnaryOp { Neg, LNot, BNot }
85+
86+
pub struct Param {
87+
name: String,
88+
type_: Option<TypeExpr>,
89+
loc: Location
90+
}
91+
92+
pub enum TypeExpr {
93+
TyInt,
94+
TyFloat,
95+
TyString,
96+
TyBool,
97+
TyArray(TypeExpr),
98+
// Echo types (Trope-IR-ready, see docs/Trope-Particularity-Integration.adoc):
99+
// TyEcho ~ Trope[Phi] (retained witness)
100+
// TyEchoResidue ~ FloatingQuality (witness severed)
101+
TyEcho(Option<TypeExpr>, Option<TypeExpr>),
102+
TyEchoResidue(Option<TypeExpr>, Option<TypeExpr>),
103+
TyIdent(String)
104+
}
105+
106+
pub enum LambdaBody {
107+
LambdaExpr(Expr),
108+
LambdaBlock([Stmt])
109+
}
110+
111+
pub enum Stmt {
112+
// inline records -> positional: (mutable_, name, type_, value, loc)
113+
LetStmt(Bool, String, Option<TypeExpr>, Expr, Location),
114+
// (target, value, loc)
115+
AssignStmt(Expr, Expr, Location),
116+
// (cond, then_, elseifs, else_, loc)
117+
IfStmt(Expr, [Stmt], [(Expr, [Stmt])], Option<[Stmt]>, Location),
118+
// (cond, body, loc)
119+
WhileStmt(Expr, [Stmt], Location),
120+
// (var, iter, body, loc)
121+
ForStmt(String, Expr, [Stmt], Location),
122+
// (value, loc)
123+
ReturnStmt(Option<Expr>, Location),
124+
BreakStmt(Location),
125+
ContinueStmt(Location),
126+
// (println, args, loc)
127+
PrintStmt(Bool, [Expr], Location),
128+
// (tokens, recovered, loc)
129+
GutterBlock([Token], Bool, Location),
130+
ExprStmt(Expr)
131+
}
132+
133+
pub enum Decl {
134+
// (name, params, returnType, body, loc)
135+
FunctionDecl(String, [Param], Option<TypeExpr>, [Stmt], Location),
136+
// (name, fields, loc)
137+
StructDecl(String, [(String, TypeExpr)], Location),
138+
// (body, loc)
139+
MainBlock([Stmt], Location),
140+
StmtDecl(Stmt)
141+
}
142+
143+
pub struct Program {
144+
declarations: [Decl],
145+
loc: Location
146+
}
147+
148+
// ============================================
149+
// Errors
150+
// ============================================
151+
152+
pub enum ErrorCode {
153+
E0001, E0002, E0003, E0004, E0005, E0006, E0007, E0008, E0009, E0010
154+
}
155+
156+
pub struct Diagnostic {
157+
code: ErrorCode,
158+
message: String,
159+
loc: Location,
160+
runNumber: Int,
161+
hint: Option<String>
162+
}
163+
164+
// ============================================
165+
// Runtime state & stability
166+
// ============================================
167+
168+
pub enum StabilityFactor {
169+
MutableState(Int, Int), // mutations, readers
170+
TypeInstability(Int), // reassignments
171+
NullPropagation(Int), // depth
172+
GlobalState(Int, Int), // mutations, dependencies
173+
UnhandledError(Int), // paths
174+
AlgorithmComplexity(Float), // time_ms
175+
MemoryLeak(Int), // bytes
176+
RaceCondition(Int) // conflicts
177+
}
178+
179+
pub struct StabilityReport {
180+
score: Int,
181+
factors: [StabilityFactor],
182+
breakdown: Dict<String, Int>,
183+
recommendations: [String]
184+
}
185+
186+
pub struct RuntimeState {
187+
runCounter: Int,
188+
stabilityScore: Int,
189+
lastError: Option<ErrorCode>,
190+
seed: Int,
191+
stabilityFactors: [StabilityFactor],
192+
discoveredRules: [String],
193+
historicalRuns: [Int]
194+
}
195+
196+
pub fn make_default_state() -> RuntimeState {
197+
#{
198+
runCounter: 0,
199+
stabilityScore: 100,
200+
lastError: None,
201+
seed: 0,
202+
stabilityFactors: [],
203+
discoveredRules: [],
204+
historicalRuns: []
205+
}
206+
}
207+
208+
// Stability impact (non-positive), mirrors Types.res `stabilityImpact`.
209+
pub fn stability_impact(factor: StabilityFactor) -> Int {
210+
match factor {
211+
MutableState(mutations, readers) => -(10 * mutations + 5 * readers),
212+
TypeInstability(reassignments) => -(15 * reassignments),
213+
NullPropagation(depth) => -(20 * depth),
214+
GlobalState(mutations, dependencies) => -(30 * mutations + 5 * dependencies),
215+
UnhandledError(paths) => -(25 * paths),
216+
AlgorithmComplexity(time_ms) => -trunc(time_ms / 10.0),
217+
MemoryLeak(bytes) => -(10 * (bytes / 1024)),
218+
RaceCondition(conflicts) => -(40 * conflicts)
219+
}
220+
}
221+
222+
// mirrors Types.res `calculateStability`: max(0, 100 + sum(impacts))
223+
pub fn calculate_stability(factors: [StabilityFactor]) -> Int {
224+
let penalties = fold(factors, 0, |acc, x| acc + stability_impact(x));
225+
max(0, 100 + penalties)
226+
}
227+
228+
pub fn error_code_to_string(code: ErrorCode) -> String {
229+
match code {
230+
E0001 => "E0001",
231+
E0002 => "E0002",
232+
E0003 => "E0003",
233+
E0004 => "E0004",
234+
E0005 => "E0005",
235+
E0006 => "E0006",
236+
E0007 => "E0007",
237+
E0008 => "E0008",
238+
E0009 => "E0009",
239+
E0010 => "E0010"
240+
}
241+
}

patches/README.adoc

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= AffineScript toolchain patches
4+
:toc:
5+
6+
Patches applied to a fresh `hyperpolymath/affinescript` checkout by
7+
`scripts/install-affinescript-toolchain.sh` before building the compiler, to
8+
support the ReScript -> AffineScript migration. Each is a stop-gap pending
9+
upstream; drop it from the install script once upstreamed.
10+
11+
== affinescript-module-struct-fields.patch
12+
13+
*Problem.* AffineScript's module resolver exported imported *enum* constructors
14+
but dropped imported *struct/alias* type definitions: `lib/resolve.ml` registered
15+
`TyEnum` variant constructors for imported modules but had a bare
16+
`| TyAlias _ | TyStruct _ | TyExtern -> ()`. Field access on an imported struct
17+
therefore failed with `Field 'x' not found in type T` — the named type stayed an
18+
opaque `TCon` and never expanded to its `TRecord`.
19+
20+
This blocked a per-module `.res -> .affine` port: the shared AST in
21+
`compiler/src/Types.affine` (`Location`, `Token`, `Position`, ...) is
22+
field-accessed by every other compiler module.
23+
24+
*Fix.* Thread imported modules' `type_env` (struct/alias/enum type definitions)
25+
and `constructor_env` into the importing module's type-check context, mirroring
26+
the existing `name_types` (scheme) threading that already made enums cross:
27+
28+
* `lib/typecheck.ml` — `check_program` gains `?import_type_env` /
29+
`?import_constructor_env`, seeding `ctx.type_env` / `ctx.constructor_env`.
30+
* `lib/resolve.ml` — a new `import_type_defs` copies a resolved module's
31+
`type_env` / `constructor_env` into the destination context, called from all
32+
three import forms (`use M;`, `use M::{...}`, `use M::*`); the imported-module
33+
check site passes the new params.
34+
* `bin/main.ml` — the `check` / `compile` / `eval` entry points pass the threaded
35+
`type_env` / `constructor_env` to `check_program`.
36+
37+
*Verification.* A module importing a struct and accessing its (nested) fields,
38+
constructing it, and matching on an imported enum field now type-checks; existing
39+
stdlib cross-module imports (`http_fetch`, `option`, `io`) still pass.
40+
41+
*Upstream.* This belongs in `hyperpolymath/affinescript` — it fixes any multi-file
42+
AffineScript program, not only error-lang. It could not be pushed from the
43+
migration session (affinescript was outside the session's repo scope); upstream
44+
when convenient, then delete this patch and its hook in the install script.

0 commit comments

Comments
 (0)