diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 566ed20..f8b5a30 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -4,11 +4,91 @@ Copyright (c) Jonathan D.A. Jewell --> # PROOF-NEEDS.md -## Template ABI Cleanup (2026-03-29) +> Engineering ledger for the error-lang **formal core**. This is the honest +> substrate beneath the language's deliberately tongue-in-cheek "100% +> production-ready, formally verified" self-presentation: it records what is +> *actually* machine-checked, what is not, and how to reproduce the checks. +> The language may dissemble about itself on purpose — this file does not. -Template ABI removed -- was creating false impression of formal verification. -The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template -scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs. +## Formal core (`src/abi/`) -When this project needs formal ABI verification, create domain-specific Idris2 proofs -following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`. +Three properties of the computational-haptics engine are proved in Idris2 and +**machine-checked under Idris 2, version 0.8.0**, with **no escape hatches** +(no `believe_me`, `assert_total`, `cast`-coerced equality, or `postulate`): + +| Property | Module | Status | +|---|---|---| +| Stability score ∈ [0, 100] | `src/abi/Stability.idr` | ✅ proved (`stabilityUpperBound`, `stabilityLowerBound`) | +| Positional-operator determinism | `src/abi/Positional.idr` | ✅ proved (`positionalDeterministic`) + sanity evaluations | +| Paradox-factor monotonicity | `src/abi/Paradox.idr` | ⚠️ partial — two factors proved, blanket claim retracted (below) | + +`src/abi/Foreign.idr` is an honest, self-contained ABI **binding-declaration** +layer (it asserts no theorems). All four modules are listed in +`src/abi/error-lang-abi.ipkg`. + +### Reproduce + +```sh +# idris2 is not in apt here, and the ziglang/deno mirrors are blocked by the +# environment network policy, so build the proof checker from source via Chez: +sudo apt-get install -y chezscheme libgmp-dev make gcc +git clone https://github.com/idris-lang/Idris2 && cd Idris2 +make bootstrap SCHEME=chezscheme && make install +export PATH="$HOME/.idris2/bin:$PATH" + +# then, from the error-lang repo root: +./verification/check-proofs.sh +# or: cd src/abi && idris2 --typecheck error-lang-abi.ipkg +``` + +### The monotonicity retraction (an honest finding) + +The previously-advertised property *"paradox detection is monotonic with +complexity"* is **false of the implementation** — and attempting to prove it +honestly is what surfaced that. `error_lang_detect_paradoxes` +(`ffi/zig/src/main.zig`) gates `scope_leakage` on `isPrime(line_count)`, which +is not monotone: line **7** is prime → active, line **8** is composite → +inactive, even though 8 > 7. + +`src/abi/Paradox.idr` therefore proves the part that *is* true — the two +threshold-gated factors are monotone in their driving metric +(`superpositionMonotone` for `var_count > 10`; `temporalMonotone` for +`depth > 5`) — and retracts the blanket claim, recording the scope-leakage +obstruction explicitly. Non-monotone scope leakage is intentional; it is the +pedagogical point of the paradox. The difference now is that the proof says so +out loud, instead of hiding it behind `cast Refl`. + +## What was removed (2026-06-23) + +`src/abi/Foreign.idr` previously carried three "Safety Proofs" — +`stabilityBounded`, `positionalDeterministic`, `paradoxMonotonic` — that were +**not proofs**. Each manufactured its evidence with `cast ()` / `cast Refl` +over an `IO` action (e.g. calling an FFI function twice and coercing +`Refl : x = x` onto the two distinct results, with a comment that it "should +hold in practice"). An earlier note in this file claimed these files had been +removed; in fact `Foreign.idr` was still present and still exported the fakes. + +They are now deleted and replaced by the genuine, machine-checked modules above. + +## Open obligations + +1. **CI gate.** Add an Idris2 `--typecheck error-lang-abi.ipkg` job so the core + is checked on every push. (The dev image has no idris2 by default; it was + built from source for this change.) +2. **Implementation conformance.** The proofs are stated over abstract models + that mirror `ffi/zig/src/main.zig` and `compiler/src/Types.res`. Two of those + implementations **disagree**: positional behaviour is `column % 2` (two-way) + in the Zig FFI but `(line*31 + column) mod 4` (four-way) in `Stability.res`. + Reconcile them, then bind the proofs to the chosen implementation by + extraction or conformance tests rather than parallel models. +3. **Zig weighted-average path.** `error_lang_calculate_stability` is a convex + combination (weights sum to 1) of per-factor scores in [0,100]; its [0,100] + bound holds for a *different* reason than the `Stability.res` clamp proved + here. Prove that path too. +4. **Programs not executed in this environment.** Under the current network + policy the Deno runtime's JSR std deps (`jsr.io`) and Zig 0.13.0 + (`ziglang.org`) are unreachable, and the ReScript compiler does not currently + build (`return` is not valid ReScript — `VM.res:407`; `dict` + applies the one-argument `dict` constructor to two arguments — + `Types.res:233`). These were **not** run or fixed as part of this change and + are tracked as separate work — they are not claimed to pass. diff --git a/compiler/src/Cst.affine b/compiler/src/Cst.affine new file mode 100644 index 0000000..6f37a7c --- /dev/null +++ b/compiler/src/Cst.affine @@ -0,0 +1,228 @@ +// SPDX-License-Identifier: MPL-2.0 +// Cst.affine — Concrete Syntax Tree for Error-Lang (ported from compiler/src/Cst.res). +// +// A CST preserves all source text (whitespace, comments, exact tokens) so source +// round-trips. Ported to AffineScript's functional style (no mut struct fields / +// record spread): stateful classify_trivia loops a `let mut` local; lex_with_trivia +// folds raw tokens carrying the last token in hand (so newline-trailing-trivia and +// trailing source are attached without array-index mutation). +// +// Selective `Types` import: Cst's node kinds (MainBlock/FunctionDecl/LetStmt/...) +// would collide with Types' Decl/Stmt constructors under a glob import, so only the +// token/location types (+ the Newline constructor for matching) are imported. +// +// Omitted vs Cst.res (documented): +// - 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 test harness (Console-based) is not part of the compiler. + +module Cst; + +use prelude::*; +use string::{length, substring, join, char_at}; +use collections::{flat_map}; +use Types::{TokenType, Position, Location, Token, Newline}; +use Lexer::{lex}; + +// ---- trivia ---- + +enum TriviaKind { TkWhitespace, TkLineComment, TkNewline } + +struct Trivia { + kind: TriviaKind, + text: String, + loc: Location +} + +struct CstToken { + tokenKind: TokenType, + text: String, + leadingTrivia: [Trivia], + trailingTrivia: [Trivia], + loc: Location +} + +enum CstNodeKind { + SourceFile, MainBlock, FunctionDecl, StructDecl, LetStmt, IfStmt, WhileStmt, + ForStmt, ReturnStmt, BreakStmt, ContinueStmt, PrintStmt, GutterBlock, ExprStmt, + BinaryExpr, UnaryExpr, CallExpr, IndexExpr, MemberExpr, TernaryExpr, LambdaExpr, + ArrayLitExpr, ParamList, ArgList, ErrorNode +} + +enum CstNode { + NodeToken(CstToken), + NodeTree(CstTree) +} + +struct CstTree { + kind: CstNodeKind, + children: [CstNode], + loc: Location +} + +// ---- location helpers ---- + +fn mk_pos(line: Int, column: Int, offset: Int) -> Position { + #{ line: line, column: column, offset: offset } +} + +fn mk_loc(start_off: Int, end_off: Int, file: String) -> Location { + #{ start: mk_pos(0, 0, start_off), end_: mk_pos(0, 0, end_off), file: file } +} + +fn code_at_str(s: String, i: Int) -> Int { + match char_at(s, i) { + Some(c) => char_to_int(c), + None => -1 + } +} + +fn is_ws_code(c: Int) -> Bool { c == 32 || c == 9 || c == 13 } + +// ---- source reconstruction (round-trip) ---- + +fn trivia_text(t: Trivia) -> String { t.text } + +pub fn to_source(node: CstNode) -> String { + match node { + NodeToken(tok) => { + let leading = join(map(tok.leadingTrivia, trivia_text), ""); + let trailing = join(map(tok.trailingTrivia, trivia_text), ""); + leading ++ tok.text ++ trailing + }, + NodeTree(tree) => tree_to_source(tree) + } +} + +pub fn tree_to_source(tree: CstTree) -> String { + join(map(tree.children, to_source), "") +} + +// ---- token collection (document order) ---- + +fn node_tokens(node: CstNode) -> [CstToken] { + match node { + NodeToken(tok) => [tok], + NodeTree(subtree) => tokens(subtree) + } +} + +pub fn tokens(tree: CstTree) -> [CstToken] { + flat_map(node_tokens, tree.children) +} + +// ---- trivia classification (gap of source -> trivia items) ---- + +pub fn classify_trivia(gap: String, file: String, base_offset: Int) -> [Trivia] { + let mut result = []; + let mut i = 0; + let glen = length(gap); + while i < glen { + let c = code_at_str(gap, i); + if c == 35 { // '#': line comment to end of line + let start = i; + let mut j = i; + while (j < glen) && (code_at_str(gap, j) != 10) { j = j + 1; } + let loc = mk_loc(base_offset + start, base_offset + j, file); + result = result ++ [#{ kind: TkLineComment, text: substring(gap, start, j), loc: loc }]; + i = j; + } else if c == 10 { // newline + let loc = mk_loc(base_offset + i, base_offset + i + 1, file); + result = result ++ [#{ kind: TkNewline, text: "\n", loc: loc }]; + i = i + 1; + } else if is_ws_code(c) { // contiguous whitespace + let start = i; + let mut j = i; + while (j < glen) && is_ws_code(code_at_str(gap, j)) { j = j + 1; } + let loc = mk_loc(base_offset + start, base_offset + j, file); + result = result ++ [#{ kind: TkWhitespace, text: substring(gap, start, j), loc: loc }]; + i = j; + } else { // anything else (shouldn't occur in gaps) + let loc = mk_loc(base_offset + i, base_offset + i + 1, file); + result = result ++ [#{ kind: TkWhitespace, text: substring(gap, i, i + 1), loc: loc }]; + i = i + 1; + } + } + result +} + +// ---- trivia-aware lexing ---- + +struct LexAcc { + committed: [CstToken], + last: Option, + prev_end: Int +} + +fn set_trailing(t: CstToken, trailing: [Trivia]) -> CstToken { + #{ tokenKind: t.tokenKind, text: t.text, leadingTrivia: t.leadingTrivia, + trailingTrivia: trailing, loc: t.loc } +} + +pub fn lex_with_trivia(source: String, file: String, run_number: Int) -> [CstToken] { + let (raw_tokens, _diags) = lex(source, file, run_number); + + let final = fold(raw_tokens, #{ committed: [], last: None, prev_end: 0 }, |acc, tok| { + let tok_start = tok.loc.start.offset; + let tok_end = tok.loc.end_.offset; + let leading = if tok_start > acc.prev_end { + classify_trivia(substring(source, acc.prev_end, tok_start), file, acc.prev_end) + } else { + [] + }; + match tok.type_ { + Newline => { + let nl = #{ kind: TkNewline, text: tok.lexeme, loc: tok.loc }; + match acc.last { + None => { + let synth = #{ tokenKind: tok.type_, text: tok.lexeme, leadingTrivia: leading, + trailingTrivia: [], loc: tok.loc }; + #{ committed: acc.committed, last: Some(synth), prev_end: tok_end } + }, + Some(lt) => { + let updated = set_trailing(lt, lt.trailingTrivia ++ leading ++ [nl]); + #{ committed: acc.committed, last: Some(updated), prev_end: tok_end } + } + } + }, + _ => { + let new_committed = match acc.last { + Some(lt) => acc.committed ++ [lt], + None => acc.committed + }; + let new_tok = #{ tokenKind: tok.type_, text: tok.lexeme, leadingTrivia: leading, + trailingTrivia: [], loc: tok.loc }; + #{ committed: new_committed, last: Some(new_tok), prev_end: tok_end } + } + } + }); + + // attach trailing source after the last token, then commit the last token + let total_len = length(source); + match final.last { + None => final.committed, + Some(lt) => { + let lt2 = if final.prev_end < total_len { + set_trailing(lt, lt.trailingTrivia ++ classify_trivia(substring(source, final.prev_end, total_len), file, final.prev_end)) + } else { + lt + }; + final.committed ++ [lt2] + } + } +} + +// ---- public API ---- + +pub fn parse_to_cst(source: String, file: String, run_number: Int) -> CstTree { + let cst_tokens = lex_with_trivia(source, file, run_number); + let children = map(cst_tokens, |tok| NodeToken(tok)); + let n = len(cst_tokens); + let loc = if n == 0 { + mk_loc(0, 0, file) + } else { + #{ start: cst_tokens[0].loc.start, end_: cst_tokens[n - 1].loc.end_, file: file } + }; + #{ kind: SourceFile, children: children, loc: loc } +} diff --git a/compiler/src/Lexer.affine b/compiler/src/Lexer.affine new file mode 100644 index 0000000..78f3ea1 --- /dev/null +++ b/compiler/src/Lexer.affine @@ -0,0 +1,363 @@ +// SPDX-License-Identifier: MPL-2.0 +// Lexer.affine — tokenizer for Error-Lang (ported from compiler/src/Lexer.res). +// +// AffineScript has no mutable struct fields or record-spread, so the imperative +// ReScript lexer is rendered functionally: state-mutating helpers take a +// LexerState and return a new one (full-record reconstruction); the scanners and +// driver loop a `let mut` local. Single chars are Char (char_at / char_to_int); +// the escape buffer is built with single-char substrings. +// +// Known parity gaps vs Lexer.res (decimal/core path is faithful; these are +// tracked for a follow-up parity pass): +// - hex (0x) / binary (0b) integer prefixes +// - triple-quoted strings and the \0 null escape +// - smart-quote (U+201C / U+201D) detection (diagnostic E0007) + +module Lexer; + +use prelude::*; +use string::{char_at, length, substring, is_digit, is_alpha, is_alphanumeric}; +use Types::*; + +pub struct LexerState { + source: String, + file: String, + pos: Int, + line: Int, + column: Int, + tokens: [Token], + diagnostics: [Diagnostic], + runNumber: Int +} + +pub fn make(source: String, file: String, run_number: Int) -> LexerState { + #{ source: source, file: file, pos: 0, line: 1, column: 1, + tokens: [], diagnostics: [], runNumber: run_number } +} + +// ---- peeking (read copyable fields only; never consume the state) ---- + +fn peek_at(source: String, pos: Int, offset: Int) -> Option { + char_at(source, pos + offset) +} + +// code point of the char at pos+offset, or -1 at end of input +fn code_at(source: String, pos: Int, offset: Int) -> Int { + match char_at(source, pos + offset) { + Some(c) => char_to_int(c), + None => -1 + } +} + +fn mk_pos(line: Int, column: Int, offset: Int) -> Position { + #{ line: line, column: column, offset: offset } +} + +fn is_hex_digit(c: Char) -> Bool { + let k = char_to_int(c); + (k >= 48 && k <= 57) || (k >= 97 && k <= 102) || (k >= 65 && k <= 70) +} + +// ---- keyword table (ReScript Dict -> match on string equality) ---- + +fn keyword_lookup(w: String) -> Option { + if w == "main" { Some(Main) } + else if w == "end" { Some(End) } + else if w == "let" { Some(Let) } + else if w == "mutable" { Some(Mutable) } + else if w == "function" { Some(Function) } + else if w == "struct" { Some(Struct) } + else if w == "if" { Some(If) } + else if w == "elseif" { Some(Elseif) } + else if w == "else" { Some(Else) } + else if w == "while" { Some(While) } + else if w == "for" { Some(For) } + else if w == "in" { Some(In) } + else if w == "break" { Some(Break) } + else if w == "continue" { Some(Continue) } + else if w == "return" { Some(Return) } + else if w == "and" { Some(And) } + else if w == "or" { Some(Or) } + else if w == "not" { Some(Not) } + else if w == "true" { Some(True) } + else if w == "false" { Some(False) } + else if w == "nil" { Some(Nil) } + else if w == "gutter" { Some(Gutter) } + else if w == "fn" { Some(Fn) } + else if w == "Int" { Some(TInt) } + else if w == "Float" { Some(TFloat) } + else if w == "String" { Some(TString) } + else if w == "Bool" { Some(TBool) } + else if w == "Array" { Some(TArray) } + else if w == "Echo" { Some(TEcho) } + else if w == "EchoR" { Some(TEchoR) } + else if w == "print" { Some(Identifier("print")) } + else if w == "println" { Some(Identifier("println")) } + else { None } +} + +// ---- state transitions (consume + rebuild) ---- + +fn advance(s: LexerState) -> LexerState { + let is_nl = code_at(s.source, s.pos, 0) == 10; + let new_line = if is_nl { s.line + 1 } else { s.line }; + let new_col = if is_nl { 1 } else { s.column + 1 }; + #{ source: s.source, file: s.file, pos: s.pos + 1, + line: new_line, column: new_col, + tokens: s.tokens, diagnostics: s.diagnostics, runNumber: s.runNumber } +} + +fn add_token(s: LexerState, type_: TokenType, lexeme: String, loc: Location) -> LexerState { + let tok = #{ type_: type_, lexeme: lexeme, loc: loc }; + #{ source: s.source, file: s.file, pos: s.pos, line: s.line, column: s.column, + tokens: s.tokens ++ [tok], diagnostics: s.diagnostics, runNumber: s.runNumber } +} + +fn add_diagnostic(s: LexerState, code: ErrorCode, message: String, loc: Location) -> LexerState { + let diag = #{ code: code, message: message, loc: loc, + runNumber: s.runNumber, hint: None }; + #{ source: s.source, file: s.file, pos: s.pos, line: s.line, column: s.column, + tokens: s.tokens, diagnostics: s.diagnostics ++ [diag], runNumber: s.runNumber } +} + +// Advance once, emitting a token whose location spans the single consumed char. +fn single_tok(s: LexerState, t: TokenType, lex: String) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, t, lex, loc) +} + +// ---- scanners ---- + +fn scan_comment(s: LexerState) -> LexerState { + let mut st = s; + while (code_at(st.source, st.pos, 0) != 10) && (st.pos < length(st.source)) { + st = advance(st); + } + st +} + +fn scan_identifier(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let start_pos = s.pos; + let mut st = s; + while (match char_at(st.source, st.pos) { Some(c) => is_alphanumeric(c), None => false }) { + st = advance(st); + } + let lexeme = substring(st.source, start_pos, st.pos); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let type_ = match keyword_lookup(lexeme) { + Some(kw) => kw, + None => Identifier(lexeme) + }; + add_token(st, type_, lexeme, loc) +} + +fn scan_number(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let start_pos = s.pos; + let mut st = s; + + // integer part + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + + // optional fractional part: '.' followed by a digit + let mut is_float = false; + if (code_at(st.source, st.pos, 0) == 46) && (match char_at(st.source, st.pos + 1) { Some(c) => is_digit(c), None => false }) { + is_float = true; + st = advance(st); // '.' + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + } + + // optional exponent + let ec = code_at(st.source, st.pos, 0); + if ec == 101 || ec == 69 { // e / E + is_float = true; + st = advance(st); + let sgn = code_at(st.source, st.pos, 0); + if sgn == 43 || sgn == 45 { st = advance(st); } // + / - + while (match char_at(st.source, st.pos) { Some(c) => is_digit(c), None => false }) { + st = advance(st); + } + } + + let lexeme = substring(st.source, start_pos, st.pos); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + if is_float { + match parse_float(lexeme) { + Some(f) => add_token(st, FloatTok(f), lexeme, loc), + None => add_token(st, Error("Invalid float"), lexeme, loc) + } + } else { + match parse_int(lexeme) { + Some(n) => add_token(st, Integer(n), lexeme, loc), + None => add_token(st, Error("Invalid integer"), lexeme, loc) + } + } +} + +// String literal (single-quote-aware double-quoted; escapes; no triple-quote — +// simplified from the .res triple-quote handling, noted for the parity pass). +fn scan_string(s: LexerState) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let mut st = advance(s); // opening quote + let mut buf = ""; + let mut done = false; + let mut result = st; + + while !done { + let c = code_at(st.source, st.pos, 0); + if c == -1 { + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let st2 = add_diagnostic(st, E0002, "Unterminated string literal", loc); + result = add_token(st2, Error("Unterminated string"), buf, loc); + done = true; + } else if c == 34 { // closing " + st = advance(st); + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let quoted = "\"" ++ buf ++ "\""; + result = add_token(st, StringTok(buf), quoted, loc); + done = true; + } else if c == 92 { // backslash escape + st = advance(st); + let e = code_at(st.source, st.pos, 0); + if e == 110 { buf = buf ++ "\n"; st = advance(st); } + else if e == 114 { buf = buf ++ "\r"; st = advance(st); } + else if e == 116 { buf = buf ++ "\t"; st = advance(st); } + else if e == 92 { buf = buf ++ "\\"; st = advance(st); } + else if e == 34 { buf = buf ++ "\""; st = advance(st); } + else if e == -1 { done = true; result = st; } + else { + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + st = add_diagnostic(st, E0003, "Invalid escape sequence", loc); + st = advance(st); + } + } else if c == 10 { // newline in string + let loc = #{ start: start, end_: mk_pos(st.line, st.column, st.pos), file: st.file }; + let st2 = add_diagnostic(st, E0002, "Unterminated string literal (newline in string)", loc); + result = add_token(st2, Error("Unterminated string"), buf, loc); + done = true; + } else { + buf = buf ++ substring(st.source, st.pos, st.pos + 1); + st = advance(st); + } + } + result +} + +// ---- main dispatch + driver ---- + +fn step(s: LexerState) -> LexerState { + let c = code_at(s.source, s.pos, 0); + if c == 32 || c == 9 || c == 13 { + advance(s) + } else if c == 10 { // newline token + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, Newline, "\\n", loc) + } else if c == 35 { // # + scan_comment(s) + } else if c == 43 { single_tok(s, Plus, "+") } + else if c == 45 { // - or -> + if code_at(s.source, s.pos, 1) == 62 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, Arrow, "->", loc) + } else { single_tok(s, Minus, "-") } + } + else if c == 42 { single_tok(s, Star, "*") } + else if c == 47 { single_tok(s, Slash, "/") } + else if c == 37 { single_tok(s, Percent, "%") } + else if c == 61 { // = or == + if code_at(s.source, s.pos, 1) == 61 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, EqualEqual, "==", loc) + } else { single_tok(s, Equal, "=") } + } + else if c == 33 { // ! -> != or error + if code_at(s.source, s.pos, 1) == 61 { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, BangEqual, "!=", loc) + } else { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_diagnostic(s2, E0001, "Unexpected character '!'", loc) + } + } + else if c == 60 { // < <= << + let n = code_at(s.source, s.pos, 1); + if n == 61 { two_char(s, LessEqual, "<=") } + else if n == 60 { two_char(s, LessLess, "<<") } + else { single_tok(s, Less, "<") } + } + else if c == 62 { // > >= >> + let n = code_at(s.source, s.pos, 1); + if n == 61 { two_char(s, GreaterEqual, ">=") } + else if n == 62 { two_char(s, GreaterGreater, ">>") } + else { single_tok(s, Greater, ">") } + } + else if c == 38 { single_tok(s, Ampersand, "&") } + else if c == 124 { single_tok(s, Pipe, "|") } + else if c == 94 { single_tok(s, Caret, "^") } + else if c == 126 { single_tok(s, Tilde, "~") } + else if c == 63 { single_tok(s, Question, "?") } + else if c == 58 { single_tok(s, Colon, ":") } + else if c == 40 { single_tok(s, LParen, "(") } + else if c == 41 { single_tok(s, RParen, ")") } + else if c == 91 { single_tok(s, LBracket, "[") } + else if c == 93 { single_tok(s, RBracket, "]") } + else if c == 123 { single_tok(s, LBrace, "{") } + else if c == 125 { single_tok(s, RBrace, "}") } + else if c == 44 { single_tok(s, Comma, ",") } + else if c == 46 { single_tok(s, Dot, ".") } + else if c == 34 { scan_string(s) } // " + else { + match char_at(s.source, s.pos) { + Some(ch) => + if is_digit(ch) { scan_number(s) } + else if is_alpha(ch) { scan_identifier(s) } + else { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(s); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + let lex = substring(s2.source, start.offset, s2.pos); + add_token(add_diagnostic(s2, E0004, "Illegal character", loc), Error("Illegal"), lex, loc) + }, + None => s + } + } +} + +fn two_char(s: LexerState, t: TokenType, lex: String) -> LexerState { + let start = mk_pos(s.line, s.column, s.pos); + let s2 = advance(advance(s)); + let loc = #{ start: start, end_: mk_pos(s2.line, s2.column, s2.pos), file: s2.file }; + add_token(s2, t, lex, loc) +} + +pub fn tokenize(s0: LexerState) -> LexerState { + let mut s = s0; + while s.pos < length(s.source) { + s = step(s); + } + let eof = mk_pos(s.line, s.column, s.pos); + let loc = #{ start: eof, end_: mk_pos(s.line, s.column, s.pos), file: s.file }; + add_token(s, EOF, "", loc) +} + +pub fn lex(source: String, file: String, run_number: Int) -> ([Token], [Diagnostic]) { + let s = tokenize(make(source, file, run_number)); + (s.tokens, s.diagnostics) +} diff --git a/compiler/src/Parser.affine b/compiler/src/Parser.affine new file mode 100644 index 0000000..bde513e --- /dev/null +++ b/compiler/src/Parser.affine @@ -0,0 +1,1150 @@ +// SPDX-License-Identifier: MPL-2.0 +// Parser.affine — error-tolerant recursive-descent parser for Error-Lang +// (ported from compiler/src/Parser.res). +// +// AffineScript has no mutable struct fields and no record-spread, so the +// imperative ReScript parser (which mutates `state.pos`/`state.diagnostics` +// in place and uses `ref` cells for `left`/`args`/...) is rendered +// functionally: +// * ParserState is an immutable struct; every consuming helper TAKES a +// ParserState and RETURNS a new one (full-record reconstruction). +// * Token/expression producers return a tuple `(Option, ParserState)` +// — the result paired with the threaded state — and callers destructure +// `let (x, st) = f(st);`. +// * ReScript `ref` accumulators become `let mut` locals; loops that both +// accumulate and advance the cursor carry a `(acc, state)` (or +// `(left_opt, state)`) tuple through a `while`. +// +// Token/AST constructors come from the `Types` module. Note the two +// reserved-keyword renames carried over from Types.affine: the literal token +// variants are `Integer`/`FloatTok`/`StringTok` (not `Float`/`String`), and +// inline-record AST variants are positional (e.g. `LetStmt(mutable_, name, +// type_, value, loc)`). +// +// ── Faithfulness notes: documented gaps / simplifications vs Parser.res ── +// * expectCloseAngle's in-place token rewrite: when the lexer fuses a +// closing `>>` (GreaterGreater) that must close two nested type-arg +// lists (e.g. `Echo>`), Parser.res MUTATES tokens[pos] to +// leave a `Greater` behind. With an immutable token array we reproduce +// this faithfully by REBUILDING the array (`set_token_at`) with the +// split `Greater` token at `pos`; behaviour is identical, cost is O(n) +// per split (type-arg lists are short, so this is negligible). +// * The `start` position of binary/call/index/member nodes: Parser.res +// computes it with `switch l { | IntLit(_, loc) => loc.start | _ => +// currentLoc(state).start }` — i.e. it only recovers a precise start +// when the left operand is an integer literal (the Call site also peeks +// `Ident`), otherwise it falls back to the *current* token. This is a +// pre-existing quirk of Parser.res; it is reproduced EXACTLY here (see +// `start_or_current` / `start_or_current_call`) rather than "fixed", to +// keep node construction byte-for-byte faithful. +// * No omitted grammar: every production in Parser.res (ternary → +// logical-or → … → unary → postfix → primary, the full statement set +// incl. gutter-block error recovery, type-expression parsing, function/ +// struct/main declarations, and the top-level `parse` driver) is ported. +// * `runTests`/Console code: none exists in Parser.res, so nothing to omit. + +module Parser; + +use prelude::*; +use Types::*; + +// ============================================ +// Parser state +// ============================================ + +pub struct ParserState { + tokens: [Token], + pos: Int, + diagnostics: [Diagnostic], + runNumber: Int, + file: String +} + +pub fn make(tokens: [Token], file: String, run_number: Int) -> ParserState { + #{ tokens: tokens, pos: 0, diagnostics: [], runNumber: run_number, file: file } +} + +// Rebuild state advancing the cursor by one (bounded by token count). +fn with_pos(s: ParserState, new_pos: Int) -> ParserState { + #{ tokens: s.tokens, pos: new_pos, diagnostics: s.diagnostics, + runNumber: s.runNumber, file: s.file } +} + +// Replace tokens[idx] with `v`, returning a new state (used by the +// GreaterGreater split — see header note). +fn set_token_at(s: ParserState, idx: Int, v: Token) -> ParserState { + let mut out = []; + let mut i = 0; + let n = len(s.tokens); + while i < n { + if i == idx { out = out ++ [v]; } else { out = out ++ [s.tokens[i]]; } + i = i + 1; + } + #{ tokens: out, pos: s.pos, diagnostics: s.diagnostics, + runNumber: s.runNumber, file: s.file } +} + +// ============================================ +// Cursor primitives (read-only: never rebuild state) +// ============================================ + +fn peek(s: ParserState) -> Option { + if s.pos < len(s.tokens) { Some(s.tokens[s.pos]) } else { None } +} + +fn peek_ahead(s: ParserState, offset: Int) -> Option { + let idx = s.pos + offset; + if idx < len(s.tokens) { Some(s.tokens[idx]) } else { None } +} + +// The token just consumed (Parser.res reads `state.tokens[state.pos - 1]`). +fn prev_token(s: ParserState) -> Option { + let idx = s.pos - 1; + if idx >= 0 && idx < len(s.tokens) { Some(s.tokens[idx]) } else { None } +} + +// Advance one token (returns just the new state; the consumed token, when +// needed, is read via prev_token afterwards — mirrors ReScript `advance`). +fn advance(s: ParserState) -> ParserState { + if s.pos < len(s.tokens) { with_pos(s, s.pos + 1) } else { s } +} + +fn is_at_end(s: ParserState) -> Bool { + match peek(s) { + Some(tok) => match tok.type_ { EOF => true, _ => false }, + None => true + } +} + +fn check(s: ParserState, t: TokenType) -> Bool { + match peek(s) { + Some(tok) => tok.type_ == t, + None => false + } +} + +// Consume if the current token is any of `ts` (ReScript `match_`/Array.some). +fn match_any(s: ParserState, ts: [TokenType]) -> (Bool, ParserState) { + let mut st = s; + let mut matched = false; + let mut i = 0; + let n = len(ts); + while i < n && !matched { + if check(st, ts[i]) { + st = advance(st); + matched = true; + } + i = i + 1; + } + (matched, st) +} + +fn skip_newlines(s: ParserState) -> ParserState { + let mut st = s; + while check(st, Newline) { + st = advance(st); + } + st +} + +fn add_diagnostic(s: ParserState, code: ErrorCode, message: String, loc: Location) -> ParserState { + let diag = #{ code: code, message: message, loc: loc, + runNumber: s.runNumber, hint: None }; + #{ tokens: s.tokens, pos: s.pos, + diagnostics: s.diagnostics ++ [diag], + runNumber: s.runNumber, file: s.file } +} + +fn zero_pos() -> Position { #{ line: 0, column: 0, offset: 0 } } + +fn zero_loc(file: String) -> Location { + #{ start: zero_pos(), end_: zero_pos(), file: file } +} + +fn current_loc(s: ParserState) -> Location { + match peek(s) { + Some(tok) => tok.loc, + None => zero_loc(s.file) + } +} + +// Expect a token type; on success consume and return Ok(token); on failure +// emit E0001 and return Err. (ReScript returns `result` but +// every caller `->ignore`s it, so callers here just take the state.) +fn expect(s: ParserState, t: TokenType, message: String) -> (Result, ParserState) { + match peek(s) { + Some(tok) => + if tok.type_ == t { + (Ok(tok), advance(s)) + } else { + (Err(()), add_diagnostic(s, E0001, message, tok.loc)) + }, + None => (Err(()), add_diagnostic(s, E0001, message, zero_loc(s.file))) + } +} + +// Discard the Result, keep the state (the common `expect(...)->ignore` use). +fn expect_(s: ParserState, t: TokenType, message: String) -> ParserState { + let (_r, st) = expect(s, t, message); + st +} + +// ============================================ +// Location helpers (mirror Parser.res start-position quirk; see header) +// ============================================ + +fn mk_loc(start: Position, end_: Position, file: String) -> Location { + #{ start: start, end_: end_, file: file } +} + +// `switch l { | IntLit(_, loc) => loc.start | _ => current.start }` +fn start_or_current(l: Expr, s: ParserState) -> Position { + match l { + IntLit(_n, loc) => loc.start, + _ => current_loc(s).start + } +} + +// Call site additionally peeks `Ident`: +// `| IntLit(_, loc) => loc.start | Ident(_, loc) => loc.start | _ => ...` +fn start_or_current_call(l: Expr, s: ParserState) -> Position { + match l { + IntLit(_n, loc) => loc.start, + Ident(_nm, loc) => loc.start, + _ => current_loc(s).start + } +} + +// ============================================ +// Expression parsing +// parseExpression → parseTernary → parseLogicalOr → parseLogicalAnd +// → parseEquality → parseComparison → parseTerm → parseFactor +// → parseUnary → parsePostfix → parsePrimary +// Each returns (Option, ParserState). +// ============================================ + +fn parse_expression(s: ParserState) -> (Option, ParserState) { + parse_ternary(s) +} + +fn parse_ternary(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_logical_or(s); + match left { + Some(cond) => + if check(s1, Question) { + let start_loc = current_loc(s1); + let s2 = advance(s1); // ? + let (then_opt, s3) = parse_expression(s2); + match then_opt { + Some(then_) => { + let (got_colon, s4) = match_any(s3, [Colon]); + if got_colon { + let (else_opt, s5) = parse_expression(s4); + match else_opt { + Some(else_) => { + let loc = mk_loc(start_loc.start, current_loc(s5).end_, s5.file); + (Some(Ternary(cond, then_, else_, loc)), s5) + }, + None => (Some(cond), s5) + } + } else { + (Some(cond), s4) + } + }, + None => (Some(cond), s3) + } + } else { + (Some(cond), s1) + }, + None => (left, s1) + } +} + +// Shared left-associative binary loop: given an already-parsed `left`, while +// the current token is one of `ops`, consume it, parse the rhs with `next`, +// and fold into a Binary node whose op is `op_of(prevTokenType)`. +fn binary_loop( + left0: Option, + s0: ParserState, + ops: [TokenType], + op_of: TokenType -> BinaryOp, + next: ParserState -> (Option, ParserState) +) -> (Option, ParserState) { + let mut left = left0; + let mut st = s0; + let mut go = true; + while go { + let has_left = match left { Some(_e) => true, None => false }; + if !has_left { go = false; } + else { + let (matched, s_after) = match_any(st, ops); + if !matched { + st = s_after; + go = false; + } else { + let op = match prev_token(s_after) { + Some(t) => op_of(t.type_), + None => op_of(EOF) + }; + let (right, s_rhs) = next(s_after); + match (left, right) { + (Some(l), Some(r)) => { + let loc = mk_loc(start_or_current(l, s_rhs), current_loc(s_rhs).end_, s_rhs.file); + left = Some(Binary(l, op, r, loc)); + st = s_rhs; + }, + _ => { + // Parser.res keeps `left` unchanged on a missing rhs but has + // already advanced past the operator; replicate that. + st = s_rhs; + } + } + } + } + } + (left, st) +} + +fn parse_logical_or(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_logical_and(s); + binary_loop(left, s1, [Or], op_logical_or, parse_logical_and) +} +fn op_logical_or(_t: TokenType) -> BinaryOp { LOr } + +fn parse_logical_and(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_equality(s); + binary_loop(left, s1, [And], op_logical_and, parse_equality) +} +fn op_logical_and(_t: TokenType) -> BinaryOp { LAnd } + +fn parse_equality(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_comparison(s); + binary_loop(left, s1, [EqualEqual, BangEqual], op_equality, parse_comparison) +} +fn op_equality(t: TokenType) -> BinaryOp { + match t { + EqualEqual => Eq, + BangEqual => Neq, + _ => Eq + } +} + +fn parse_comparison(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_term(s); + binary_loop(left, s1, [Less, Greater, LessEqual, GreaterEqual], op_comparison, parse_term) +} +fn op_comparison(t: TokenType) -> BinaryOp { + match t { + Less => Lt, + Greater => Gt, + LessEqual => Lte, + GreaterEqual => Gte, + _ => Lt + } +} + +fn parse_term(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_factor(s); + binary_loop(left, s1, [Plus, Minus], op_term, parse_factor) +} +fn op_term(t: TokenType) -> BinaryOp { + match t { + Plus => Add, + Minus => Sub, + _ => Add + } +} + +fn parse_factor(s: ParserState) -> (Option, ParserState) { + let (left, s1) = parse_unary(s); + binary_loop(left, s1, [Star, Slash, Percent], op_factor, parse_unary) +} +fn op_factor(t: TokenType) -> BinaryOp { + match t { + Star => Mul, + Slash => Div, + Percent => Mod, + _ => Mul + } +} + +fn parse_unary(s: ParserState) -> (Option, ParserState) { + let (matched, s1) = match_any(s, [Minus, Not, Tilde]); + if matched { + let op_tok = match prev_token(s1) { + Some(t) => t, + None => #{ type_: Minus, lexeme: "-", loc: zero_loc(s1.file) } + }; + let op = match op_tok.type_ { + Minus => Neg, + Not => LNot, + Tilde => BNot, + _ => Neg + }; + let (right, s2) = parse_unary(s1); + match right { + Some(r) => { + let loc = mk_loc(op_tok.loc.start, current_loc(s2).end_, s2.file); + (Some(Unary(op, r, loc)), s2) + }, + None => (None, s2) + } + } else { + parse_postfix(s) + } +} + +fn parse_postfix(s: ParserState) -> (Option, ParserState) { + let (left0, s0) = parse_primary(s); + let mut left = left0; + let mut st = s0; + let mut go = true; + while go { + let has_left = match left { Some(_e) => true, None => false }; + if !has_left { + go = false; + } else if check(st, LParen) { + // Function call + let s1 = advance(st); + let s2 = skip_newlines(s1); + let (args, s3) = parse_arg_list(s2, RParen); + let s4 = skip_newlines(s3); + let s5 = expect_(s4, RParen, "Expected ')' after arguments"); + match left { + Some(l) => { + let loc = mk_loc(start_or_current_call(l, s5), current_loc(s5).end_, s5.file); + left = Some(Call(l, args, loc)); + st = s5; + }, + None => { st = s5; } + } + } else if check(st, LBracket) { + // Index + let s1 = advance(st); + let s2 = skip_newlines(s1); + let (idx_opt, s3) = parse_expression(s2); + match idx_opt { + Some(idx) => { + let s4 = skip_newlines(s3); + let s5 = expect_(s4, RBracket, "Expected ']' after index"); + match left { + Some(l) => { + let loc = mk_loc(start_or_current(l, s5), current_loc(s5).end_, s5.file); + left = Some(Index(l, idx, loc)); + st = s5; + }, + None => { st = s5; } + } + }, + None => { st = s3; } + } + } else if check(st, Dot) { + // Member access + let s1 = advance(st); + match peek(s1) { + Some(tok) => match tok.type_ { + Identifier(name) => { + let member_loc = tok.loc; + let s2 = advance(s1); + match left { + Some(l) => { + let loc = mk_loc(start_or_current(l, s2), member_loc.end_, s2.file); + left = Some(Member(l, name, loc)); + st = s2; + }, + None => { st = s2; } + } + }, + _ => { + st = add_diagnostic(s1, E0001, "Expected identifier after '.'", current_loc(s1)); + go = false; + } + }, + None => { + st = add_diagnostic(s1, E0001, "Expected identifier after '.'", current_loc(s1)); + go = false; + } + } + } else { + go = false; + } + } + (left, st) +} + +// Parse a comma-separated expression list up to (but not consuming) `closer`. +// Mirrors the repeated `parseExpression` + `while match_(Comma)` blocks used +// for call args, array elements, and print args. +fn parse_arg_list(s: ParserState, closer: TokenType) -> ([Expr], ParserState) { + let mut args = []; + let mut st = s; + if !check(st, closer) { + let (first, s1) = parse_expression(st); + args = match first { + Some(e) => args ++ [e], + None => args + }; + st = s1; + let mut go = true; + while go { + let (got_comma, s_c) = match_any(st, [Comma]); + if !got_comma { + st = s_c; + go = false; + } else { + let s_sn = skip_newlines(s_c); + let (e_opt, s_e) = parse_expression(s_sn); + args = match e_opt { + Some(e) => args ++ [e], + None => args + }; + st = s_e; + } + } + } + // `return` (not a bare trailing tuple): an if-statement immediately + // followed by a tuple tail trips an AffineScript checker bug (E0104 + // "Expected a function, got Unit", no span) — the `()` of the if is + // applied to the tuple. Verified minimal repro; `return` sidesteps it. + return (args, st); +} + +fn parse_primary(s: ParserState) -> (Option, ParserState) { + match peek(s) { + Some(tok) => parse_primary_tok(s, tok), + None => (None, s) + } +} + +fn parse_primary_tok(s: ParserState, tok: Token) -> (Option, ParserState) { + let loc = tok.loc; + match tok.type_ { + Integer(n) => (Some(IntLit(n, loc)), advance(s)), + FloatTok(f) => (Some(FloatLit(f, loc)), advance(s)), + StringTok(str) => (Some(StringLit(str, loc)), advance(s)), + True => (Some(BoolLit(true, loc)), advance(s)), + False => (Some(BoolLit(false, loc)), advance(s)), + Nil => (Some(NilLit(loc)), advance(s)), + Identifier(name) => (Some(Ident(name, loc)), advance(s)), + LBracket => parse_array_literal(s, loc), + LParen => parse_grouped(s), + Fn => parse_lambda(s, loc), + _ => { + let s1 = add_diagnostic(s, E0001, "Unexpected token '" ++ tok.lexeme ++ "'", tok.loc); + (None, s1) + } + } +} + +fn parse_array_literal(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // [ + let s2 = skip_newlines(s1); + let (elems, s3) = parse_arg_list(s2, RBracket); + let s4 = skip_newlines(s3); + let s5 = expect_(s4, RBracket, "Expected ']' after array elements"); + let loc = mk_loc(start_loc.start, current_loc(s5).end_, s5.file); + (Some(Array(elems, loc)), s5) +} + +fn parse_grouped(s: ParserState) -> (Option, ParserState) { + let s1 = advance(s); // ( + let s2 = skip_newlines(s1); + let (expr, s3) = parse_expression(s2); + let s4 = skip_newlines(s3); + let s5 = expect_(s4, RParen, "Expected ')' after expression"); + (expr, s5) +} + +fn parse_lambda(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // fn + let s2 = expect_(s1, LParen, "Expected '(' after 'fn'"); + let (params, s3) = parse_lambda_params(s2); + let s4 = expect_(s3, RParen, "Expected ')' after parameters"); + let (got_arrow, s5) = match_any(s4, [Arrow]); + if got_arrow { + let (body_opt, s6) = parse_expression(s5); + match body_opt { + Some(body) => { + let loc = mk_loc(start_loc.start, current_loc(s6).end_, s6.file); + (Some(Lambda(params, None, LambdaExpr(body), loc)), s6) + }, + None => (None, s6) + } + } else { + // Block body (future) — Parser.res returns None here. + (None, s5) + } +} + +// Lambda params: untyped identifiers (Parser.res `type_: None`). +fn parse_lambda_params(s: ParserState) -> ([Param], ParserState) { + let mut params = []; + let mut st = skip_newlines(s); + if !check(st, RParen) { + let (p0, st0) = lambda_param_at(params, st); + params = p0; + st = st0; + let mut go = true; + while go { + let (got_comma, s_c) = match_any(st, [Comma]); + if !got_comma { + st = s_c; + go = false; + } else { + let s_sn = skip_newlines(s_c); + let (pn, stn) = lambda_param_at(params, s_sn); + params = pn; + st = stn; + } + } + } + return (params, st); // `return` works around the if-then-tuple checker bug +} + +// If the current token is an identifier, append an untyped Param and advance; +// otherwise leave both unchanged. Returns (params, state). +fn lambda_param_at(params: [Param], s: ParserState) -> ([Param], ParserState) { + match peek(s) { + Some(tok) => match tok.type_ { + Identifier(name) => (params ++ [#{ name: name, type_: None, loc: tok.loc }], advance(s)), + _ => (params, s) + }, + None => (params, s) + } +} + +// ============================================ +// Type-annotation parsing +// ============================================ + +// Consume a closing '>' for a type-arg list. The lexer fuses `>>` into a +// single GreaterGreater; if a closing angle sits against an enclosing one we +// split it in place (rebuild the token array, leaving a `Greater` at pos). +fn expect_close_angle(s: ParserState) -> ParserState { + match peek(s) { + Some(tok) => match tok.type_ { + Greater => advance(s), + GreaterGreater => { + let split = #{ type_: Greater, lexeme: ">", loc: tok.loc }; + set_token_at(s, s.pos, split) + }, + _ => add_diagnostic(s, E0006, "Expected '>' to close type arguments", tok.loc) + }, + None => s + } +} + +// Optional `` / ``. Returns ((first, second), state). +fn parse_type_args(s: ParserState) -> ((Option, Option), ParserState) { + if check(s, Less) { + let s1 = advance(s); + let (first, s2) = parse_type_expr(s1); + let (got_comma, s3) = match_any(s2, [Comma]); + let (second, s4) = if got_comma { + parse_type_expr(s3) + } else { + (None, s3) + }; + let s5 = expect_close_angle(s4); + ((first, second), s5) + } else { + ((None, None), s) + } +} + +fn parse_type_expr(s: ParserState) -> (Option, ParserState) { + match peek(s) { + Some(tok) => match tok.type_ { + TInt => (Some(TyInt), advance(s)), + TFloat => (Some(TyFloat), advance(s)), + TString => (Some(TyString), advance(s)), + TBool => (Some(TyBool), advance(s)), + TArray => { + let s1 = advance(s); + let ((first, _second), s2) = parse_type_args(s1); + match first { + Some(inner) => (Some(TyArray(inner)), s2), + // Bare `Array`: default element type to `Any`. + None => (Some(TyArray(TyIdent("Any"))), s2) + } + }, + TEcho => { + let s1 = advance(s); + let ((a, b), s2) = parse_type_args(s1); + (Some(TyEcho(a, b)), s2) + }, + TEchoR => { + let s1 = advance(s); + let ((a, b), s2) = parse_type_args(s1); + (Some(TyEchoResidue(a, b)), s2) + }, + Identifier(name) => (Some(TyIdent(name)), advance(s)), + _ => (None, s) + }, + None => (None, s) + } +} + +// Optional `: Type` annotation (used after let-names and parameter names). +fn parse_optional_type(s: ParserState) -> (Option, ParserState) { + let (got_colon, s1) = match_any(s, [Colon]); + if got_colon { + parse_type_expr(s1) + } else { + (None, s1) + } +} + +// ============================================ +// Statement parsing +// ============================================ + +fn parse_statement(s: ParserState) -> (Option, ParserState) { + let s0 = skip_newlines(s); + match peek(s0) { + Some(tok) => parse_statement_tok(s0, tok), + None => (None, s0) + } +} + +fn parse_statement_tok(s: ParserState, tok: Token) -> (Option, ParserState) { + let start_loc = tok.loc; + match tok.type_ { + Let => parse_let(s, start_loc), + If => parse_if(s, start_loc), + While => parse_while(s, start_loc), + For => parse_for(s, start_loc), + Return => parse_return(s, start_loc), + Break => (Some(BreakStmt(start_loc)), advance(s)), + Continue => (Some(ContinueStmt(start_loc)), advance(s)), + Identifier(name) => + if name == "print" { + parse_print(s, start_loc, false) + } else if name == "println" { + parse_print(s, start_loc, true) + } else { + parse_expr_stmt(s) + }, + Gutter => parse_gutter(s, start_loc), + _ => parse_expr_stmt(s) + } +} + +fn parse_let(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // let + let (mutable_, s2) = match_any(s1, [Mutable]); + match peek(s2) { + Some(tok) => match tok.type_ { + Identifier(name) => { + let s3 = advance(s2); + let (type_, s4) = parse_optional_type(s3); + let s5 = expect_(s4, Equal, "Expected '=' after variable name"); + let (value_opt, s6) = parse_expression(s5); + match value_opt { + Some(value) => { + let loc = mk_loc(start_loc.start, current_loc(s6).end_, s6.file); + (Some(LetStmt(mutable_, name, type_, value, loc)), s6) + }, + None => (None, s6) + } + }, + _ => { + let s3 = add_diagnostic(s2, E0001, "Expected identifier after 'let'", current_loc(s2)); + (None, s3) + } + }, + None => { + let s3 = add_diagnostic(s2, E0001, "Expected identifier after 'let'", current_loc(s2)); + (None, s3) + } + } +} + +fn parse_if(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // if + let (cond_opt, s2) = parse_expression(s1); + match cond_opt { + Some(cond) => { + let s3 = skip_newlines(s2); + let (then_, s4) = parse_block(s3); + // elseif chains + let (elseifs, s5) = parse_elseifs(s4); + // optional else + let (else_, s6) = if check(s5, Else) { + let s_e = advance(s5); + let s_e2 = skip_newlines(s_e); + let (body, s_e3) = parse_block(s_e2); + (Some(body), s_e3) + } else { + (None, s5) + }; + let loc = mk_loc(start_loc.start, current_loc(s6).end_, s6.file); + (Some(IfStmt(cond, then_, elseifs, else_, loc)), s6) + }, + None => (None, s2) + } +} + +fn parse_elseifs(s: ParserState) -> ([(Expr, [Stmt])], ParserState) { + let mut elseifs = []; + let mut st = s; + let mut go = true; + while go { + if check(st, Elseif) { + let s1 = advance(st); + let (elif_cond_opt, s2) = parse_expression(s1); + match elif_cond_opt { + Some(elif_cond) => { + let s3 = skip_newlines(s2); + let (elif_body, s4) = parse_block(s3); + elseifs = elseifs ++ [(elif_cond, elif_body)]; + st = s4; + }, + None => { st = s2; } + } + } else { + go = false; + } + } + (elseifs, st) +} + +fn parse_while(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // while + let (cond_opt, s2) = parse_expression(s1); + match cond_opt { + Some(cond) => { + let s3 = skip_newlines(s2); + let (body, s4) = parse_block(s3); + let loc = mk_loc(start_loc.start, current_loc(s4).end_, s4.file); + (Some(WhileStmt(cond, body, loc)), s4) + }, + None => (None, s2) + } +} + +fn parse_for(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // for + match peek(s1) { + Some(tok) => match tok.type_ { + Identifier(var) => { + let s2 = advance(s1); + let s3 = expect_(s2, In, "Expected 'in' after loop variable"); + let (iter_opt, s4) = parse_expression(s3); + match iter_opt { + Some(iter) => { + let s5 = skip_newlines(s4); + let (body, s6) = parse_block(s5); + let loc = mk_loc(start_loc.start, current_loc(s6).end_, s6.file); + (Some(ForStmt(var, iter, body, loc)), s6) + }, + None => (None, s4) + } + }, + _ => { + let s2 = add_diagnostic(s1, E0001, "Expected identifier after 'for'", current_loc(s1)); + (None, s2) + } + }, + None => { + let s2 = add_diagnostic(s1, E0001, "Expected identifier after 'for'", current_loc(s1)); + (None, s2) + } + } +} + +fn parse_return(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // return + let (value, s2) = if check(s1, Newline) || check(s1, End) || check(s1, EOF) { + (None, s1) + } else { + parse_expression(s1) + }; + let loc = mk_loc(start_loc.start, current_loc(s2).end_, s2.file); + (Some(ReturnStmt(value, loc)), s2) +} + +// `is_println` distinguishes print vs println. NB: a parameter literally named +// `println` shadows the `println` builtin, which trips the resolver's global +// "Expected a function, got Unit" (E0104, no span) — so we avoid that name. +fn parse_print(s: ParserState, start_loc: Location, is_println: Bool) -> (Option, ParserState) { + let s1 = advance(s); // print / println + let msg = if is_println { "Expected '(' after 'println'" } else { "Expected '(' after 'print'" }; + let s2 = expect_(s1, LParen, msg); + let s3 = skip_newlines(s2); + let (args, s4) = parse_arg_list(s3, RParen); + let s5 = skip_newlines(s4); + let s6 = expect_(s5, RParen, "Expected ')' after arguments"); + let loc = mk_loc(start_loc.start, current_loc(s6).end_, s6.file); + (Some(PrintStmt(is_println, args, loc)), s6) +} + +// Gutter block — error-injection zone: swallow tokens until `end`, recover. +fn parse_gutter(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // gutter + let s2 = skip_newlines(s1); + + let mut gutter_tokens = []; + let mut st = s2; + let mut scanning = true; + while scanning { + if !check(st, End) && !is_at_end(st) { + match peek(st) { + Some(tok) => { + gutter_tokens = gutter_tokens ++ [tok]; + st = advance(st); + }, + None => { scanning = false; } + } + } else { + scanning = false; + } + } + + let (recovered, s3) = if check(st, End) { + (true, advance(st)) + } else { + (false, add_diagnostic(st, E0005, "Missing 'end' for gutter block", start_loc)) + }; + + let loc = mk_loc(start_loc.start, current_loc(s3).end_, s3.file); + (Some(GutterBlock(gutter_tokens, recovered, loc)), s3) +} + +fn parse_expr_stmt(s: ParserState) -> (Option, ParserState) { + let (expr_opt, s1) = parse_expression(s); + match expr_opt { + Some(expr) => (Some(ExprStmt(expr)), s1), + None => { + // Skip bad token + let s2 = advance(s1); + (None, s2) + } + } +} + +fn parse_block(s: ParserState) -> ([Stmt], ParserState) { + let mut stmts = []; + let mut st = skip_newlines(s); + let mut go = true; + while go { + if !check(st, End) && !check(st, Elseif) && !check(st, Else) && !is_at_end(st) { + let (stmt_opt, s1) = parse_statement(st); + stmts = match stmt_opt { + Some(stmt) => stmts ++ [stmt], + None => stmts + }; + st = skip_newlines(s1); + } else { + go = false; + } + } + let st2 = if check(st, End) { advance(st) } else { st }; + (stmts, st2) +} + +// ============================================ +// Declaration parsing +// ============================================ + +fn parse_declaration(s: ParserState) -> (Option, ParserState) { + let s0 = skip_newlines(s); + match peek(s0) { + Some(tok) => parse_declaration_tok(s0, tok), + None => (None, s0) + } +} + +fn parse_declaration_tok(s: ParserState, tok: Token) -> (Option, ParserState) { + let start_loc = tok.loc; + match tok.type_ { + Function => parse_function(s, start_loc), + Main => parse_main(s, start_loc), + Struct => parse_struct(s, start_loc), + _ => { + // Top-level statement + let (stmt_opt, s1) = parse_statement(s); + match stmt_opt { + Some(stmt) => (Some(StmtDecl(stmt)), s1), + None => (None, s1) + } + } + } +} + +fn parse_function(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // function + match peek(s1) { + Some(tok) => match tok.type_ { + Identifier(name) => { + let s2 = advance(s1); + let s3 = expect_(s2, LParen, "Expected '(' after function name"); + let (params, s4) = parse_typed_params(s3); + let s5 = expect_(s4, RParen, "Expected ')' after parameters"); + // optional return type `-> Type` + let (got_arrow, s6) = match_any(s5, [Arrow]); + let (return_type, s7) = if got_arrow { + parse_type_expr(s6) + } else { + (None, s6) + }; + let s8 = skip_newlines(s7); + let (body, s9) = parse_block(s8); + let loc = mk_loc(start_loc.start, current_loc(s9).end_, s9.file); + (Some(FunctionDecl(name, params, return_type, body, loc)), s9) + }, + _ => { + let s2 = add_diagnostic(s1, E0001, "Expected function name", current_loc(s1)); + (None, s2) + } + }, + None => { + let s2 = add_diagnostic(s1, E0001, "Expected function name", current_loc(s1)); + (None, s2) + } + } +} + +// Function params: each an identifier with an optional `: Type` annotation. +fn parse_typed_params(s: ParserState) -> ([Param], ParserState) { + let mut params = []; + let mut st = skip_newlines(s); + if !check(st, RParen) { + let (p0, st0) = typed_param_at(params, st); + params = p0; + st = st0; + let mut go = true; + while go { + let (got_comma, s_c) = match_any(st, [Comma]); + if !got_comma { + st = s_c; + go = false; + } else { + let s_sn = skip_newlines(s_c); + let (pn, stn) = typed_param_at(params, s_sn); + params = pn; + st = stn; + } + } + } + return (params, st); // `return` works around the if-then-tuple checker bug +} + +// If the current token is an identifier, append a Param with optional `: Type` +// and advance past name (+ annotation); otherwise leave both unchanged. +fn typed_param_at(params: [Param], s: ParserState) -> ([Param], ParserState) { + match peek(s) { + Some(tok) => match tok.type_ { + Identifier(pname) => { + let ploc = tok.loc; + let s1 = advance(s); + let (ptype, s2) = parse_optional_type(s1); + (params ++ [#{ name: pname, type_: ptype, loc: ploc }], s2) + }, + _ => (params, s) + }, + None => (params, s) + } +} + +fn parse_main(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // main + let s2 = skip_newlines(s1); + let (body, s3) = parse_block(s2); + let loc = mk_loc(start_loc.start, current_loc(s3).end_, s3.file); + (Some(MainBlock(body, loc)), s3) +} + +fn parse_struct(s: ParserState, start_loc: Location) -> (Option, ParserState) { + let s1 = advance(s); // struct + match peek(s1) { + Some(tok) => match tok.type_ { + Identifier(name) => { + let s2 = advance(s1); + let s3 = skip_newlines(s2); + let (fields, s4) = parse_struct_fields(s3); + let s5 = if check(s4, End) { advance(s4) } else { s4 }; + let loc = mk_loc(start_loc.start, current_loc(s5).end_, s5.file); + (Some(StructDecl(name, fields, loc)), s5) + }, + _ => { + let s2 = add_diagnostic(s1, E0001, "Expected struct name", current_loc(s1)); + (None, s2) + } + }, + None => { + let s2 = add_diagnostic(s1, E0001, "Expected struct name", current_loc(s1)); + (None, s2) + } + } +} + +fn parse_struct_fields(s: ParserState) -> ([(String, TypeExpr)], ParserState) { + let mut fields = []; + let mut st = s; + let mut go = true; + while go { + if !check(st, End) && !is_at_end(st) { + let (fn2, st2, keep) = struct_field_at(fields, st); + fields = fn2; + st = st2; + go = keep; + } else { + go = false; + } + } + (fields, st) +} + +// Parse one struct field (`name: Type`) if present. Returns +// (fields, state, keep_going). `keep_going` is false only when the cursor is +// exhausted (mirrors the `None => ()` arm that would otherwise spin). +fn struct_field_at(fields: [(String, TypeExpr)], s: ParserState) -> ([(String, TypeExpr)], ParserState, Bool) { + match peek(s) { + Some(tok) => match tok.type_ { + Identifier(fname) => { + let s1 = advance(s); + let s2 = expect_(s1, Colon, "Expected ':' after field name"); + let (ty_opt, s3) = parse_type_expr(s2); + let new_fields = match ty_opt { + Some(ty) => fields ++ [(fname, ty)], + None => fields + }; + (new_fields, skip_newlines(s3), true) + }, + // Non-identifier: Parser.res's `| _ => ()` does not advance; the trailing + // skipNewlines then runs. We advance past the stray token to guarantee + // progress (a non-newline non-identifier would otherwise loop forever), + // which is a benign termination hardening over the .res source. + _ => (fields, skip_newlines(advance(s)), true) + }, + None => (fields, s, false) + } +} + +// ============================================ +// Main entry point +// ============================================ + +pub fn parse(tokens: [Token], file: String, run_number: Int) -> (Program, [Diagnostic]) { + let s0 = make(tokens, file, run_number); + let mut declarations = []; + let mut st = s0; + let mut go = true; + while go { + if !is_at_end(st) { + let (decl_opt, s1) = parse_declaration(st); + declarations = match decl_opt { + Some(decl) => declarations ++ [decl], + None => declarations + }; + st = skip_newlines(s1); + } else { + go = false; + } + } + + let prog_loc = mk_loc(#{ line: 1, column: 1, offset: 0 }, current_loc(st).end_, file); + let program = #{ declarations: declarations, loc: prog_loc }; + (program, st.diagnostics) +} diff --git a/compiler/src/TypeChecker.affine b/compiler/src/TypeChecker.affine new file mode 100644 index 0000000..5f463d3 --- /dev/null +++ b/compiler/src/TypeChecker.affine @@ -0,0 +1,1123 @@ +// SPDX-License-Identifier: MPL-2.0 +// TypeChecker.affine — static type checker for Error-Lang +// (ported from compiler/src/TypeChecker.res). +// +// Typing rules (unchanged from the .res): +// - `let x = expr` — infer type from expr +// - `let x: Type = expr` — check expr against Type +// - `mutable` variables can be reassigned (same type only) +// - `if/elseif/else` — condition must be Bool, branches checked in nested scopes +// - `while` — condition must be Bool +// - `for x in expr` — expr must be Array +// - `function` — standard arrow type +// - `gutter` blocks — skip type checking (error injection zone) +// - `print/println` — accept any type +// - Operators: arithmetic on Int/Float, comparison returns Bool, logical on Bool +// +// ── AffineScript port: state model ── +// The ReScript checker mutates a shared `env` (mutable `nextVar`, a shared +// `Dict` of substitutions) and a mutable `checkResult.errors` +// array, all in place. AffineScript has no mutable struct fields / record +// spread, so: +// * The unification "globals" — fresh-var counter, substitution map, and +// accumulated errors — live in a single immutable `CheckState` that is +// THREADED through every function (`(result, CheckState)` tuples; +// callers `let (x, st) = f(st, ...);`). Because they live in one +// threaded value they are automatically shared exactly as the .res's +// parent-linked env shared them — so the .res's explicit +// "propagate state back" after a lambda becomes a no-op here. +// * The lexical environment (the .res `env.bindings` + `parent` chain) is +// a frame STACK `[[ (String, Binding) ]]` (head = innermost scope). +// `extend` pushes an empty frame; `bind` extends the head frame; +// `lookup` searches head→tail. Statements that bind (`let`, `for`, +// params) return the updated frame stack so later siblings see them. +// * The substitution map is `Int`-keyed, but stdlib `dict` is +// String-keyed; a tiny assoc-list `[(Int, Ty)]` with linear get/set is +// used instead (the same purely-functional style as stdlib `dict`). +// +// ── Internal type representation ── +// The .res internal `ty` constructors are named `TyInt`/`TyFloat`/… which +// would COLLIDE with the global `TypeExpr` constructors of the same name in +// `Types.affine` (constructor names are global in AffineScript). They are +// therefore prefixed `C` (for "check"): CInt/CFloat/CString/CBool/CNil/ +// CArray/CFun/CStruct/CEcho/CEchoR/CAny/CVar. The mapping is 1:1 with the +// .res `ty`; only the spelling changes. The `Types::TypeExpr` constructors +// (TyInt, TyArray, TyEcho, TyEchoResidue, TyIdent) are used unprefixed when +// translating annotations. +// +// ── Faithfulness notes: documented gaps / simplifications vs the .res ── +// * Echo / EchoR unification is reproduced EXACTLY: same-kind structural +// unification only; Echo<_,_> deliberately does NOT unify with +// EchoR<_,_> (irreversibility of erasure). The [Stab-Erase] residue +// rules in `infer_echo_builtin` (echo / echo_to_residue / +// residue_strictly_loses / echo_input / echo_output) match the .res +// arm-for-arm, including the "echo_input on a residue is illegal" +// diagnostic and "echo_output retained by both Echo and residue". +// * The standalone `exprLoc` helper of the .res is OMITTED. It existed +// only to recover an error location from an expression the checker was +// about to consume — a use-and-consume that is awkward under affine +// ownership. Instead `infer_expr` RETURNS the expression's own +// `Location` (a copyable summary) alongside the inferred type, so every +// error already has the precise location without re-traversing a moved +// node. Behaviour is identical (same locations attached to the same +// diagnostics). The thin wrapper `infer` drops the location for the +// majority of callers that ignore it. +// * `Array.getUnsafe(0)` / `sliceToEnd(~start=1)` -> head/tail via +// indexing (`xs[0]`, `xs[1:]`); `Array.zip(a,b)->Array.every(f)` and +// `->Array.forEach` over a state-mutating body become explicit +// state-threading folds (`unify_lists`, `*_list` helpers) since the +// callbacks mutate the shared substitution/error state. +// * Empty-array element type uses a fresh var exactly as the .res. +// * No `runTests`/Console code exists in the .res, so nothing is omitted. + +module TypeChecker; + +use prelude::*; +use string::{join}; +use Types::*; + +// ============================================ +// Internal Type Representation (`ty` in the .res; C-prefixed here) +// ============================================ + +pub enum Ty { + CInt, + CFloat, + CString, + CBool, + CNil, + CArray(Ty), + CFun([Ty], Ty), + CStruct(String), + // Echo — fiber / retained-loss witness type (domain A, codomain B). + CEcho(Ty, Ty), + // EchoR — residue: the A-witness has been erased (non-recoverable). + // Deliberately does NOT unify with CEcho. + CEchoR(Ty, Ty), + CAny, + CVar(Int) +} + +// ============================================ +// Bindings / scopes / threaded state +// ============================================ + +pub struct Binding { + ty: Ty, + mutable_: Bool +} + +// One lexical frame is an assoc list of name -> binding. +// The environment is a stack of frames (head = innermost). + +pub struct TypeError { + message: String, + loc: Location +} + +// The threaded unification + error state (the .res's shared env globals + +// checkResult.errors, all in one immutable value). +pub struct CheckState { + nextVar: Int, + subs: [(Int, Ty)], + errors: [TypeError] +} + +pub fn make_state() -> CheckState { + #{ nextVar: 0, subs: [], errors: [] } +} + +fn add_error(st: CheckState, message: String, loc: Location) -> CheckState { + #{ nextVar: st.nextVar, subs: st.subs, + errors: st.errors ++ [#{ message: message, loc: loc }] } +} + +fn fresh_var(st: CheckState) -> (Ty, CheckState) { + let id = st.nextVar; + let st2 = #{ nextVar: st.nextVar + 1, subs: st.subs, errors: st.errors }; + (CVar(id), st2) +} + +// ---- substitution map (Int-keyed assoc list; last-write-wins) ---- + +fn subs_get(st: CheckState, id: Int) -> Option { + let mut out = None; + let mut found = false; + for pair in st.subs { + let (k, v) = pair; + if !found && k == id { + out = Some(v); + found = true; + } + } + out +} + +fn subs_set(st: CheckState, id: Int, t: Ty) -> CheckState { + let mut rest = []; + for pair in st.subs { + let (k, v) = pair; + if k != id { + rest = rest ++ [(k, v)]; + } + } + #{ nextVar: st.nextVar, subs: [(id, t)] ++ rest, errors: st.errors } +} + +// ---- scopes ---- + +fn empty_scopes() -> [[(String, Binding)]] { + [[]] +} + +// Push a fresh innermost frame. +fn extend(scopes: [[(String, Binding)]]) -> [[(String, Binding)]] { + [[]] ++ scopes +} + +// Extend the innermost frame with a new binding (shadowing-friendly: the +// new pair is prepended so lookups find it first). +fn bind(scopes: [[(String, Binding)]], name: String, ty: Ty, mutable_: Bool) -> [[(String, Binding)]] { + let n = len(scopes); + if n == 0 { + [[(name, #{ ty: ty, mutable_: mutable_ })]] + } else { + let head = scopes[0]; + let new_head = [(name, #{ ty: ty, mutable_: mutable_ })] ++ head; + [new_head] ++ scopes[1:] + } +} + +fn lookup_frame(frame: [(String, Binding)], name: String) -> Option { + let mut out = None; + let mut found = false; + for pair in frame { + let (k, b) = pair; + if !found && k == name { + out = Some(b); + found = true; + } + } + out +} + +fn lookup_var(scopes: [[(String, Binding)]], name: String) -> Option { + let mut out = None; + let mut found = false; + for frame in scopes { + if !found { + match lookup_frame(frame, name) { + Some(b) => { out = Some(b); found = true; }, + None => {} + } + } + } + out +} + +// ============================================ +// AST Type -> Internal Type +// ============================================ + +pub fn type_expr_to_ty(te: TypeExpr) -> Ty { + match te { + TyInt => CInt, + TyFloat => CFloat, + TyString => CString, + TyBool => CBool, + TyArray(inner) => CArray(type_expr_to_ty(inner)), + TyEcho(a, b) => CEcho(opt_type_expr_to_ty(a), opt_type_expr_to_ty(b)), + TyEchoResidue(a, b) => CEchoR(opt_type_expr_to_ty(a), opt_type_expr_to_ty(b)), + TyIdent(name) => CStruct(name) + } +} + +// An omitted Echo type argument (`Echo` or bare `Echo`) is treated as +// `Any`, which unifies with everything. +fn opt_type_expr_to_ty(o: Option) -> Ty { + match o { + Some(t) => type_expr_to_ty(t), + None => CAny + } +} + +// ============================================ +// Type Display +// ============================================ + +pub fn ty_to_string(t: Ty) -> String { + match t { + CInt => "Int", + CFloat => "Float", + CString => "String", + CBool => "Bool", + CNil => "Nil", + CArray(inner) => "Array<" ++ ty_to_string(inner) ++ ">", + CFun(params, ret) => { + let param_str = join(map(params, ty_to_string), ", "); + "(" ++ param_str ++ ") -> " ++ ty_to_string(ret) + }, + CStruct(name) => name, + CEcho(a, b) => "Echo<" ++ ty_to_string(a) ++ ", " ++ ty_to_string(b) ++ ">", + CEchoR(a, b) => "EchoR<" ++ ty_to_string(a) ++ ", " ++ ty_to_string(b) ++ ">", + CAny => "Any", + CVar(id) => "?" ++ int_to_string(id) + } +} + +// ============================================ +// Unification +// ============================================ + +// Resolve a type through the substitution map (read-only; threads no state). +pub fn resolve(st: CheckState, t: Ty) -> Ty { + match t { + CVar(id) => + match subs_get(st, id) { + Some(resolved) => resolve(st, resolved), + None => CVar(id) + }, + CArray(inner) => CArray(resolve(st, inner)), + CFun(params, ret) => CFun(map(params, |p| resolve(st, p)), resolve(st, ret)), + CEcho(a, b) => CEcho(resolve(st, a), resolve(st, b)), + CEchoR(a, b) => CEchoR(resolve(st, a), resolve(st, b)), + _ => t + } +} + +// Unify two types, possibly extending the substitution map. Returns +// (success, new_state). +pub fn unify(st: CheckState, a0: Ty, b0: Ty) -> (Bool, CheckState) { + let a = resolve(st, a0); + let b = resolve(st, b0); + match (a, b) { + (CAny, _) => (true, st), + (_, CAny) => (true, st), + (CNil, _) => (true, st), + (_, CNil) => (true, st), + (CInt, CInt) => (true, st), + (CFloat, CFloat) => (true, st), + (CString, CString) => (true, st), + (CBool, CBool) => (true, st), + (CVar(id), other) => (true, subs_set(st, id, other)), + (other, CVar(id)) => (true, subs_set(st, id, other)), + (CArray(ia), CArray(ib)) => unify(st, ia, ib), + (CStruct(na), CStruct(nb)) => (na == nb, st), + // Echo and EchoR unify structurally with their own kind only. Echo<_,_> + // does NOT unify with EchoR<_,_>: once a witness is erased the residue + // cannot be passed where a recoverable Echo is required. + (CEcho(a1, b1), CEcho(a2, b2)) => { + let (ok1, st1) = unify(st, a1, a2); + if ok1 { + let (ok2, st2) = unify(st1, b1, b2); + (ok2, st2) + } else { + (false, st1) + } + }, + (CEchoR(a1, b1), CEchoR(a2, b2)) => { + let (ok1, st1) = unify(st, a1, a2); + if ok1 { + let (ok2, st2) = unify(st1, b1, b2); + (ok2, st2) + } else { + (false, st1) + } + }, + (CFun(pa, ra), CFun(pb, rb)) => + if len(pa) != len(pb) { + (false, st) + } else { + let (params_ok, st1) = unify_lists(st, pa, pb); + if params_ok { + unify(st1, ra, rb) + } else { + (false, st1) + } + }, + _ => (false, st) + } +} + +// Unify two equal-length type lists pairwise, threading state and ANDing +// success (the .res `Array.zip(pa,pb)->Array.every(unify)`). +fn unify_lists(st: CheckState, xs: [Ty], ys: [Ty]) -> (Bool, CheckState) { + let n = len(xs); + let mut i = 0; + let mut ok = true; + let mut state = st; + while i < n { + let (one_ok, s2) = unify(state, xs[i], ys[i]); + state = s2; + if !one_ok { ok = false; } + i = i + 1; + } + (ok, state) +} + +// Numeric widening: Int can widen to Float. +fn is_numeric(t: Ty) -> Bool { + match t { + CInt => true, + CFloat => true, + _ => false + } +} + +fn widen_numeric(a: Ty, b: Ty) -> Ty { + match (a, b) { + (CFloat, _) => CFloat, + (_, CFloat) => CFloat, + _ => CInt + } +} + +// ============================================ +// Echo Builtins +// ============================================ + +// Runtime operations over Echo types (mirroring EchoTypes.jl): +// echo(x, y) : (A, B) -> Echo +// echo_to_residue(e) : Echo -> EchoR (erases witness) +// residue_strictly_loses(r) : EchoR -> Bool +// echo_input(e) : Echo -> A (illegal on residue) +// echo_output(e) : Echo | EchoR -> B +fn is_echo_builtin(name: String) -> Bool { + name == "echo" || name == "echo_to_residue" || name == "residue_strictly_loses" + || name == "echo_input" || name == "echo_output" +} + +// ============================================ +// Expression Type Inference +// +// `infer_expr` returns (ty, Location, CheckState): the inferred type, the +// expression's own location (copyable — replaces the .res `exprLoc`), and +// the threaded state. `infer` is the location-dropping wrapper most callers +// use. Scopes are read-only here (expressions never bind), so they are +// passed by value (cloned into recursive calls). +// ============================================ + +fn infer(st: CheckState, scopes: [[(String, Binding)]], e: Expr) -> (Ty, CheckState) { + let (t, _loc, st2) = infer_expr(st, scopes, e); + (t, st2) +} + +fn infer_expr(st: CheckState, scopes: [[(String, Binding)]], e: Expr) -> (Ty, Location, CheckState) { + match e { + IntLit(_n, loc) => (CInt, loc, st), + FloatLit(_f, loc) => (CFloat, loc, st), + StringLit(_s, loc) => (CString, loc, st), + BoolLit(_b, loc) => (CBool, loc, st), + NilLit(loc) => (CNil, loc, st), + + Ident(name, loc) => + match lookup_var(scopes, name) { + Some(b) => (b.ty, loc, st), + None => { + let st2 = add_error(st, "Undefined variable '" ++ name ++ "'", loc); + (CAny, loc, st2) + } + }, + + Array(elements, loc) => + if len(elements) == 0 { + let (fv, st2) = fresh_var(st); + (CArray(fv), loc, st2) + } else { + let (elem_ty, st_head) = infer(st, scopes, elements[0]); + let rest = elements[1:]; + let (final_elem, st_rest) = infer_array_rest(st_head, scopes, elem_ty, rest); + (CArray(resolve(st_rest, final_elem)), loc, st_rest) + }, + + Binary(left, op, right, loc) => { + let (t, st2) = infer_binary_op(st, scopes, left, op, right, loc); + (t, loc, st2) + }, + + Unary(op, operand, loc) => { + let (t, st2) = infer_unary_op(st, scopes, op, operand, loc); + (t, loc, st2) + }, + + Call(callee, args, loc) => + match callee { + Ident(name, id_loc) => + if is_echo_builtin(name) { + let (t, st2) = infer_echo_builtin(st, scopes, name, args, loc); + (t, loc, st2) + } else { + let (t, st2) = infer_call(st, scopes, Ident(name, id_loc), args, loc); + (t, loc, st2) + }, + _ => { + let (t, st2) = infer_call(st, scopes, callee, args, loc); + (t, loc, st2) + } + }, + + Index(base, idx, loc) => { + let (base_ty, st1) = infer(st, scopes, base); + let (idx_ty, st2) = infer(st1, scopes, idx); + let (ok, st3) = unify(st2, idx_ty, CInt); + let st4 = if !ok { + add_error(st3, "Array index must be Int, got " ++ ty_to_string(idx_ty), loc) + } else { + st3 + }; + match resolve(st4, base_ty) { + CArray(elem_ty) => (elem_ty, loc, st4), + CAny => (CAny, loc, st4), + other => { + let st5 = add_error(st4, "Cannot index non-array type " ++ ty_to_string(other), loc); + (CAny, loc, st5) + } + } + }, + + Member(base, _field, loc) => { + // Struct field access requires a type database; return Any for now. + let (_bt, st2) = infer(st, scopes, base); + (CAny, loc, st2) + }, + + Ternary(cond, then_expr, else_expr, loc) => { + let (cond_ty, st1) = infer(st, scopes, cond); + let (ok_c, st2) = unify(st1, cond_ty, CBool); + let st3 = if !ok_c { + add_error(st2, "Ternary condition must be Bool, got " ++ ty_to_string(cond_ty), loc) + } else { + st2 + }; + let (then_ty, st4) = infer(st3, scopes, then_expr); + let (else_ty, st5) = infer(st4, scopes, else_expr); + let (ok_b, st6) = unify(st5, then_ty, else_ty); + let st7 = if !ok_b { + add_error(st6, + "Ternary branches have different types: " ++ ty_to_string(then_ty) ++ " vs " ++ ty_to_string(else_ty), + loc) + } else { + st6 + }; + (resolve(st7, then_ty), loc, st7) + }, + + Lambda(params, ret_ann, body, loc) => { + let lambda_scopes = extend(scopes); + let (param_tys, scopes2, st1) = bind_lambda_params(st, lambda_scopes, params); + let (body_ty, st2) = match body { + LambdaExpr(expr) => infer(st1, scopes2, expr), + LambdaBlock(stmts) => check_stmts(st1, scopes2, stmts) + }; + let st3 = match ret_ann { + Some(ann) => { + let ann_ty = type_expr_to_ty(ann); + let (ok, sa) = unify(st2, body_ty, ann_ty); + if !ok { + add_error(sa, + "Lambda return type mismatch: declared " ++ ty_to_string(ann_ty) ++ ", body is " ++ ty_to_string(body_ty), + loc) + } else { + sa + } + }, + None => st2 + }; + (CFun(param_tys, resolve(st3, body_ty)), loc, st3) + } + } +} + +// Fold the tail of an array literal, unifying each element type with the +// head element type and threading state (the .res `sliceToEnd(1)->forEach`). +fn infer_array_rest(st: CheckState, scopes: [[(String, Binding)]], elem_ty: Ty, rest: [Expr]) -> (Ty, CheckState) { + let n = len(rest); + let mut i = 0; + let mut state = st; + while i < n { + let (t, loc, s2) = infer_expr(state, scopes, rest[i]); + let (ok, s3) = unify(s2, elem_ty, t); + state = if !ok { + add_error(s3, + "Array element type mismatch: expected " ++ ty_to_string(elem_ty) ++ ", got " ++ ty_to_string(t), + loc) + } else { + s3 + }; + i = i + 1; + } + (elem_ty, state) +} + +// Bind lambda params (each typed-or-fresh, mutable_=false), returning their +// types in order, the extended scopes, and threaded state. +fn bind_lambda_params(st: CheckState, scopes: [[(String, Binding)]], params: [Param]) -> ([Ty], [[(String, Binding)]], CheckState) { + let n = len(params); + let mut i = 0; + let mut tys = []; + let mut sc = scopes; + let mut state = st; + while i < n { + let p = params[i]; + let (ty, s2) = match p.type_ { + Some(te) => (type_expr_to_ty(te), state), + None => fresh_var(state) + }; + sc = bind(sc, p.name, ty, false); + tys = tys ++ [ty]; + state = s2; + i = i + 1; + } + (tys, sc, state) +} + +// Non-echo call inference (the .res Call(callee, args) arm). +fn infer_call(st: CheckState, scopes: [[(String, Binding)]], callee: Expr, args: [Expr], loc: Location) -> (Ty, CheckState) { + let (callee_ty, st1) = infer(st, scopes, callee); + match resolve(st1, callee_ty) { + CFun(param_tys, ret_ty) => + if len(args) != len(param_tys) { + let st2 = add_error(st1, + "Function expects " ++ int_to_string(len(param_tys)) ++ " arguments, got " ++ int_to_string(len(args)), + loc); + (ret_ty, st2) + } else { + let st2 = check_args(st1, scopes, args, param_tys); + (ret_ty, st2) + }, + CAny => (CAny, st1), + other => { + let st2 = add_error(st1, "Cannot call non-function type " ++ ty_to_string(other), loc); + (CAny, st2) + } + } +} + +// Check each argument against its parameter type, threading state. +fn check_args(st: CheckState, scopes: [[(String, Binding)]], args: [Expr], param_tys: [Ty]) -> CheckState { + let n = len(args); + let mut i = 0; + let mut state = st; + while i < n { + let (arg_ty, loc, s2) = infer_expr(state, scopes, args[i]); + let pty = param_tys[i]; + let (ok, s3) = unify(s2, arg_ty, pty); + state = if !ok { + add_error(s3, + "Argument type mismatch: expected " ++ ty_to_string(pty) ++ ", got " ++ ty_to_string(arg_ty), + loc) + } else { + s3 + }; + i = i + 1; + } + state +} + +fn infer_binary_op( + st: CheckState, + scopes: [[(String, Binding)]], + left: Expr, + op: BinaryOp, + right: Expr, + loc: Location +) -> (Ty, CheckState) { + let (lt, st1) = infer(st, scopes, left); + let (rt, st2) = infer(st1, scopes, right); + let lt_r = resolve(st2, lt); + let rt_r = resolve(st2, rt); + + match op { + // Arithmetic + Add => arith_op(st2, op, lt_r, rt_r, loc), + Sub => arith_op(st2, op, lt_r, rt_r, loc), + Mul => arith_op(st2, op, lt_r, rt_r, loc), + Div => arith_op(st2, op, lt_r, rt_r, loc), + Mod => arith_op(st2, op, lt_r, rt_r, loc), + + // Comparison + Eq => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + Neq => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + Lt => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + Gt => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + Lte => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + Gte => cmp_op(st2, lt, rt, lt_r, rt_r, loc), + + // Logical + LAnd => logical_op(st2, lt_r, rt_r, loc), + LOr => logical_op(st2, lt_r, rt_r, loc), + + // Bitwise + BAnd => bitwise_op(st2, lt_r, rt_r, loc), + BOr => bitwise_op(st2, lt_r, rt_r, loc), + BXor => bitwise_op(st2, lt_r, rt_r, loc), + Shl => bitwise_op(st2, lt_r, rt_r, loc), + Shr => bitwise_op(st2, lt_r, rt_r, loc) + } +} + +fn arith_op(st: CheckState, op: BinaryOp, lt_r: Ty, rt_r: Ty, loc: Location) -> (Ty, CheckState) { + if is_numeric(lt_r) && is_numeric(rt_r) { + (widen_numeric(lt_r, rt_r), st) + } else { + let is_add = match op { Add => true, _ => false }; + let str_concat = is_add && (lt_r == CString) && (rt_r == CString); + if str_concat { + (CString, st) + } else { + let st2 = add_error(st, + "Operator requires numeric operands, got " ++ ty_to_string(lt_r) ++ " and " ++ ty_to_string(rt_r), + loc); + (CAny, st2) + } + } +} + +fn cmp_op(st: CheckState, lt: Ty, rt: Ty, lt_r: Ty, rt_r: Ty, loc: Location) -> (Ty, CheckState) { + let (ok, st1) = unify(st, lt, rt); + let st2 = if !ok { + add_error(st1, "Cannot compare " ++ ty_to_string(lt_r) ++ " with " ++ ty_to_string(rt_r), loc) + } else { + st1 + }; + (CBool, st2) +} + +fn logical_op(st: CheckState, lt_r: Ty, rt_r: Ty, loc: Location) -> (Ty, CheckState) { + let st1 = if lt_r != CBool { + add_error(st, "Logical operator requires Bool, got " ++ ty_to_string(lt_r), loc) + } else { + st + }; + let st2 = if rt_r != CBool { + add_error(st1, "Logical operator requires Bool, got " ++ ty_to_string(rt_r), loc) + } else { + st1 + }; + (CBool, st2) +} + +fn bitwise_op(st: CheckState, lt_r: Ty, rt_r: Ty, loc: Location) -> (Ty, CheckState) { + let st1 = if lt_r != CInt { + add_error(st, "Bitwise operator requires Int, got " ++ ty_to_string(lt_r), loc) + } else { + st + }; + let st2 = if rt_r != CInt { + add_error(st1, "Bitwise operator requires Int, got " ++ ty_to_string(rt_r), loc) + } else { + st1 + }; + (CInt, st2) +} + +fn infer_unary_op( + st: CheckState, + scopes: [[(String, Binding)]], + op: UnaryOp, + operand: Expr, + loc: Location +) -> (Ty, CheckState) { + let (t, st1) = infer(st, scopes, operand); + let t_r = resolve(st1, t); + match op { + Neg => { + let st2 = if !is_numeric(t_r) { + add_error(st1, "Negation requires numeric type, got " ++ ty_to_string(t_r), loc) + } else { + st1 + }; + (t_r, st2) + }, + LNot => { + let st2 = if t_r != CBool { + add_error(st1, "Logical NOT requires Bool, got " ++ ty_to_string(t_r), loc) + } else { + st1 + }; + (CBool, st2) + }, + BNot => { + let st2 = if t_r != CInt { + add_error(st1, "Bitwise NOT requires Int, got " ++ ty_to_string(t_r), loc) + } else { + st1 + }; + (CInt, st2) + } + } +} + +// Echo / EchoR builtins. Arguments are inferred first (so nested errors +// surface regardless of arity), mirroring the .res. +fn infer_echo_builtin( + st: CheckState, + scopes: [[(String, Binding)]], + name: String, + args: [Expr], + loc: Location +) -> (Ty, CheckState) { + let (arg_tys0, st1) = infer_all(st, scopes, args); + // Pre-resolve each argument type against the substitution map. + let arg_tys = map(arg_tys0, |t| resolve(st1, t)); + let arity = len(arg_tys); + + if name == "echo" { + let st2 = expect_arity(st1, name, 2, arity, loc); + if arity == 2 { + (CEcho(arg_tys[0], arg_tys[1]), st2) + } else { + (CEcho(CAny, CAny), st2) + } + } else if name == "echo_to_residue" { + let st2 = expect_arity(st1, name, 1, arity, loc); + if arity >= 1 { + match arg_tys[0] { + CEcho(a, b) => (CEchoR(a, b), st2), + CAny => (CEchoR(CAny, CAny), st2), + other => { + let st3 = add_error(st2, "echo_to_residue expects Echo, got " ++ ty_to_string(other), loc); + (CEchoR(CAny, CAny), st3) + } + } + } else { + (CEchoR(CAny, CAny), st2) + } + } else if name == "residue_strictly_loses" { + let st2 = expect_arity(st1, name, 1, arity, loc); + if arity >= 1 { + match arg_tys[0] { + CEchoR(_a, _b) => (CBool, st2), + CAny => (CBool, st2), + other => { + let st3 = add_error(st2, "residue_strictly_loses expects EchoR, got " ++ ty_to_string(other), loc); + (CBool, st3) + } + } + } else { + (CBool, st2) + } + } else if name == "echo_input" { + let st2 = expect_arity(st1, name, 1, arity, loc); + if arity >= 1 { + match arg_tys[0] { + CEcho(a, _b) => (a, st2), + CAny => (CAny, st2), + CEchoR(_a, _b) => { + let st3 = add_error(st2, + "echo_input: the input witness was erased by echo_to_residue — a residue is non-recoverable", + loc); + (CAny, st3) + }, + other => { + let st3 = add_error(st2, "echo_input expects Echo, got " ++ ty_to_string(other), loc); + (CAny, st3) + } + } + } else { + (CAny, st2) + } + } else if name == "echo_output" { + let st2 = expect_arity(st1, name, 1, arity, loc); + if arity >= 1 { + // The output is retained by both the Echo and its residue. + match arg_tys[0] { + CEcho(_a, b) => (b, st2), + CEchoR(_a, b) => (b, st2), + CAny => (CAny, st2), + other => { + let st3 = add_error(st2, "echo_output expects Echo or EchoR, got " ++ ty_to_string(other), loc); + (CAny, st3) + } + } + } else { + (CAny, st2) + } + } else { + (CAny, st1) + } +} + +// Infer all argument types, threading state. +fn infer_all(st: CheckState, scopes: [[(String, Binding)]], args: [Expr]) -> ([Ty], CheckState) { + let n = len(args); + let mut i = 0; + let mut tys = []; + let mut state = st; + while i < n { + let (t, s2) = infer(state, scopes, args[i]); + tys = tys ++ [t]; + state = s2; + i = i + 1; + } + (tys, state) +} + +fn expect_arity(st: CheckState, name: String, n: Int, arity: Int, loc: Location) -> CheckState { + if arity != n { + add_error(st, + name ++ " expects " ++ int_to_string(n) ++ " argument(s), got " ++ int_to_string(arity), + loc) + } else { + st + } +} + +// ============================================ +// Statement Type Checking +// +// `check_stmt` returns (CheckState, scopes): a `let`/`for` extends the +// current scope, so later sibling statements see the new binding. Nested +// blocks (`if`/`while`/`for` bodies) run in a pushed scope that is then +// discarded (the outer scope is unchanged), matching the .res's +// extendEnv-per-block. +// ============================================ + +fn check_stmt(st: CheckState, scopes: [[(String, Binding)]], stmt: Stmt) -> (CheckState, [[(String, Binding)]]) { + match stmt { + LetStmt(mutable_, name, type_, value, loc) => { + let (value_ty, st1) = infer(st, scopes, value); + match type_ { + Some(ann) => { + let ann_ty = type_expr_to_ty(ann); + let (ok, st2) = unify(st1, value_ty, ann_ty); + let st3 = if !ok { + add_error(st2, + "Type annotation mismatch for '" ++ name ++ "': declared " ++ ty_to_string(ann_ty) ++ ", value is " ++ ty_to_string(value_ty), + loc) + } else { + st2 + }; + (st3, bind(scopes, name, ann_ty, mutable_)) + }, + None => { + let resolved = resolve(st1, value_ty); + (st1, bind(scopes, name, resolved, mutable_)) + } + } + }, + + AssignStmt(target, value, loc) => + match target { + Ident(name, _id_loc) => + match lookup_var(scopes, name) { + Some(b) => + if b.mutable_ { + let (value_ty, st1) = infer(st, scopes, value); + let (ok, st2) = unify(st1, value_ty, b.ty); + let st3 = if !ok { + add_error(st2, + "Cannot assign " ++ ty_to_string(value_ty) ++ " to " ++ ty_to_string(b.ty) ++ " variable '" ++ name ++ "'", + loc) + } else { + st2 + }; + (st3, scopes) + } else { + let st1 = add_error(st, "Cannot reassign immutable variable '" ++ name ++ "'", loc); + let (_vt, st2) = infer(st1, scopes, value); + (st2, scopes) + }, + None => { + let st1 = add_error(st, "Undefined variable '" ++ name ++ "'", loc); + let (_vt, st2) = infer(st1, scopes, value); + (st2, scopes) + } + }, + _ => { + // Complex assignment targets (index, member) — infer both sides. + let (_tt, st1) = infer(st, scopes, target); + let (_vt, st2) = infer(st1, scopes, value); + (st2, scopes) + } + }, + + IfStmt(cond, then_, elseifs, else_, loc) => { + let (cond_ty, st1) = infer(st, scopes, cond); + let (ok_c, st2) = unify(st1, cond_ty, CBool); + let st3 = if !ok_c { + add_error(st2, "If condition must be Bool, got " ++ ty_to_string(cond_ty), loc) + } else { + st2 + }; + let then_scopes = extend(scopes); + let (st4, _ts) = check_block(st3, then_scopes, then_); + let st5 = check_elseifs(st4, scopes, elseifs, loc); + let st6 = match else_ { + Some(else_body) => { + let else_scopes = extend(scopes); + let (s, _es) = check_block(st5, else_scopes, else_body); + s + }, + None => st5 + }; + (st6, scopes) + }, + + WhileStmt(cond, body, loc) => { + let (cond_ty, st1) = infer(st, scopes, cond); + let (ok_c, st2) = unify(st1, cond_ty, CBool); + let st3 = if !ok_c { + add_error(st2, "While condition must be Bool, got " ++ ty_to_string(cond_ty), loc) + } else { + st2 + }; + let body_scopes = extend(scopes); + let (st4, _bs) = check_block(st3, body_scopes, body); + (st4, scopes) + }, + + ForStmt(var_name, iter, body, loc) => { + let (iter_ty, st1) = infer(st, scopes, iter); + let (elem_ty, st2) = match resolve(st1, iter_ty) { + CArray(inner) => (inner, st1), + CAny => (CAny, st1), + other => { + let s = add_error(st1, "For loop requires Array, got " ++ ty_to_string(other), loc); + (CAny, s) + } + }; + let body_scopes = bind(extend(scopes), var_name, elem_ty, false); + let (st3, _bs) = check_block(st2, body_scopes, body); + (st3, scopes) + }, + + ReturnStmt(value, _loc) => + match value { + Some(expr) => { + let (_t, st1) = infer(st, scopes, expr); + (st1, scopes) + }, + None => (st, scopes) + }, + + BreakStmt(_loc) => (st, scopes), + ContinueStmt(_loc) => (st, scopes), + + PrintStmt(_println, args, _loc) => { + // print/println accept any type. + let st1 = infer_for_effect(st, scopes, args); + (st1, scopes) + }, + + // Gutter blocks are intentional error injection zones — skip checking. + GutterBlock(_tokens, _recovered, _loc) => (st, scopes), + + ExprStmt(expr) => { + let (_t, st1) = infer(st, scopes, expr); + (st1, scopes) + } + } +} + +// Check a list of elseif (cond, body) pairs, each in its own pushed scope. +fn check_elseifs(st: CheckState, scopes: [[(String, Binding)]], elseifs: [(Expr, [Stmt])], loc: Location) -> CheckState { + let n = len(elseifs); + let mut i = 0; + let mut state = st; + while i < n { + let (eif_cond, eif_body) = elseifs[i]; + let (eif_ty, s1) = infer(state, scopes, eif_cond); + let (ok, s2) = unify(s1, eif_ty, CBool); + let s3 = if !ok { + add_error(s2, "Elseif condition must be Bool, got " ++ ty_to_string(eif_ty), loc) + } else { + s2 + }; + let eif_scopes = extend(scopes); + let (s4, _es) = check_block(s3, eif_scopes, eif_body); + state = s4; + i = i + 1; + } + state +} + +// Infer each expression purely for side effects (errors), discarding types. +fn infer_for_effect(st: CheckState, scopes: [[(String, Binding)]], exprs: [Expr]) -> CheckState { + let n = len(exprs); + let mut i = 0; + let mut state = st; + while i < n { + let (_t, s2) = infer(state, scopes, exprs[i]); + state = s2; + i = i + 1; + } + state +} + +// Check a block of statements in a (already-extended) scope. Bindings made +// by a statement are visible to its successors within the block. +fn check_block(st: CheckState, scopes: [[(String, Binding)]], stmts: [Stmt]) -> (CheckState, [[(String, Binding)]]) { + let n = len(stmts); + let mut i = 0; + let mut state = st; + let mut sc = scopes; + while i < n { + let (s2, sc2) = check_stmt(state, sc, stmts[i]); + state = s2; + sc = sc2; + i = i + 1; + } + (state, sc) +} + +// Check statements and return their (block) type: TyNil, as in the .res +// `checkStmts`. Used as a lambda block body. +fn check_stmts(st: CheckState, scopes: [[(String, Binding)]], stmts: [Stmt]) -> (Ty, CheckState) { + let (state, _sc) = check_block(st, scopes, stmts); + (CNil, state) +} + +// ============================================ +// Declaration Checking +// ============================================ + +fn check_decl(st: CheckState, scopes: [[(String, Binding)]], decl: Decl) -> (CheckState, [[(String, Binding)]]) { + match decl { + FunctionDecl(name, params, return_type, body, _loc) => { + let fn_scopes = extend(scopes); + let (param_tys, scopes2, st1) = bind_lambda_params(st, fn_scopes, params); + // Infer body in the function scope (errors surface; result discarded). + let (st2, _bs) = check_block(st1, scopes2, body); + let ret_ty = match return_type { + Some(ann) => type_expr_to_ty(ann), + None => CNil + }; + // Bind the function in the OUTER environment. + (st2, bind(scopes, name, CFun(param_tys, ret_ty), false)) + }, + + StructDecl(name, _fields, _loc) => + // Register the struct name as a type. + (st, bind(scopes, name, CStruct(name), false)), + + MainBlock(body, _loc) => { + let main_scopes = extend(scopes); + let (st1, _ms) = check_block(st, main_scopes, body); + (st1, scopes) + }, + + StmtDecl(stmt) => check_stmt(st, scopes, stmt) + } +} + +// ============================================ +// Program Entry Point +// ============================================ + +// Type-check a complete Error-Lang program. Returns the accumulated errors. +pub fn check_program(prog: Program) -> [TypeError] { + let st0 = make_state(); + let scopes0 = empty_scopes(); + let n = len(prog.declarations); + let mut i = 0; + let mut state = st0; + let mut scopes = scopes0; + while i < n { + let (s2, sc2) = check_decl(state, scopes, prog.declarations[i]); + state = s2; + scopes = sc2; + i = i + 1; + } + state.errors +} diff --git a/compiler/src/TypeSuperposition.affine b/compiler/src/TypeSuperposition.affine new file mode 100644 index 0000000..ed73b59 --- /dev/null +++ b/compiler/src/TypeSuperposition.affine @@ -0,0 +1,323 @@ +// SPDX-License-Identifier: MPL-2.0 +// TypeSuperposition.affine — quantum type system (ported from +// compiler/src/TypeSuperposition.res). +// +// "Variables exist in multiple types simultaneously until observed +// (printed, used in arithmetic, compared, …)." Observation collapses the +// superposition deterministically (context-hash + seed indexes the +// possible-types array). +// +// ── AffineScript port conventions ── +// * `open Types` -> `use Types::*;`. The `typeExpr` constructors +// TyInt/TyFloat/TyString/TyBool/TyArray/… come from the `Types` +// module unchanged (they are global constructors of `TypeExpr`), so +// the quantum machinery reuses them directly. +// * ReScript inline-record variant `Superposition({possibleTypes, seed, +// declaredAt})` -> positional `Superposition([TypeExpr], Int, +// Location)`. `quantumVariable` is a struct (no mutable fields); the +// "update on observe" rebuilds the whole record. +// * `detectSuperposition` mutates a `quantumVars` array in ReScript; here +// the recursion threads an accumulator `[(String, QuantumVariable)]` +// through fold/helper calls and returns the grown list (immutable). +// * `Array.length(possibleTypes)` -> `len(...)`; `arr->Option.getOr(d)` +// -> indexed read with an explicit bounds guard (`arr[i]` is the +// builtin indexer); `mod` -> `%`. +// +// ── Faithfulness notes: documented gaps / simplifications vs the .res ── +// * Collapse arithmetic, context hashing, and the per-literal +// possible-type sets are reproduced exactly (same constants, same +// order, same TyInt default). +// * `quantumType` field on `quantumVariable` is renamed to `qtype` +// (struct fields and a same-named outer type would otherwise read +// ambiguously); purely a local rename, semantics identical. +// * No `runTests`/Console code exists in the .res, so nothing is omitted. + +module TypeSuperposition; + +use prelude::*; +use string::{join}; +use Types::*; + +// ============================================ +// Quantum type states +// ============================================ + +// ReScript: Collapsed(typeExpr) | Superposition({possibleTypes, seed, declaredAt}) +pub enum QuantumType { + Collapsed(TypeExpr), + Superposition([TypeExpr], Int, Location) +} + +// Type observation contexts +pub enum ObservationContext { + Arithmetic, // Used in +, -, *, / + StringOp, // Used in ++, interpolation + Comparison, // Used in ==, !=, <, > + Print, // Used in println + Assignment, // Assigned to typed variable + FunctionArg // Passed to typed parameter +} + +// Variable with quantum type state. +// `qtype` mirrors the .res field `quantumType`; `observedAt` keeps the +// (location, context) pair as in the source. +pub struct QuantumVariable { + name: String, + qtype: QuantumType, + observedAt: Option<(Location, ObservationContext)>, + declaredAt: Location +} + +// ============================================ +// Possible types for a literal +// ============================================ + +// Determine possible types for a literal based on its form. +pub fn possible_types_for_literal(e: Expr) -> [TypeExpr] { + match e { + // Integer literal could be Int, Float (via coercion), or String. + IntLit(_n, _loc) => [TyInt, TyFloat, TyString], + // Float could be Float or String. + FloatLit(_f, _loc) => [TyFloat, TyString], + // String is always String (but might be coercible to Int/Float). + StringLit(_s, _loc) => [TyString, TyInt, TyFloat], + // Bool could be Bool, Int (0/1), or String. + BoolLit(_b, _loc) => [TyBool, TyInt, TyString], + // Unknown expression — full superposition. + _ => [TyInt, TyFloat, TyString, TyBool] + } +} + +// ============================================ +// Collapse +// ============================================ + +// Context -> deterministic hash contribution (mirrors the .res switch). +fn context_hash(context: ObservationContext) -> Int { + match context { + Arithmetic => 0, + StringOp => 1, + Comparison => 2, + Print => 3, + Assignment => 4, + FunctionArg => 5 + } +} + +// Collapse a quantum type given an observation context and seed. +// Collapse is deterministic but depends on context, seed, and the +// variable's own seed; the index wraps modulo the possible-type count. +pub fn collapse_type(qt: QuantumType, context: ObservationContext, seed: Int) -> TypeExpr { + match qt { + Collapsed(t) => t, // Already collapsed. + Superposition(possible_types, var_seed, _declared) => { + let ch = context_hash(context); + let n = len(possible_types); + // `mod 0` is undefined; the .res relies on non-empty possibleTypes. + // Guard defensively, defaulting to TyInt (the .res getOr default). + if n == 0 { + TyInt + } else { + let hash = (var_seed + seed + ch) % n; + if hash >= 0 && hash < n { + possible_types[hash] + } else { + TyInt + } + } + } + } +} + +// Check if an observation would cause a type mismatch. +pub fn would_cause_mismatch( + qt: QuantumType, + context: ObservationContext, + expected_type: TypeExpr, + seed: Int +) -> Bool { + let collapsed = collapse_type(qt, context, seed); + collapsed != expected_type +} + +// ============================================ +// Construction & observation +// ============================================ + +// Create a quantum variable from a let statement. +pub fn create_quantum_variable( + name: String, + value: Expr, + type_annotation: Option, + loc: Location, + seed: Int +) -> QuantumVariable { + let qt = match type_annotation { + // Explicit type annotation — collapsed from the start. + Some(annotated) => Collapsed(annotated), + // No type annotation — quantum superposition! + None => { + let possible_types = possible_types_for_literal(value); + Superposition(possible_types, seed, loc) + } + }; + #{ name: name, qtype: qt, observedAt: None, declaredAt: loc } +} + +// Observe a quantum variable (collapse its type). Returns the updated +// variable paired with the collapsed type (Some unless somehow absent). +pub fn observe_variable( + qvar: QuantumVariable, + context: ObservationContext, + observe_loc: Location, + seed: Int +) -> (QuantumVariable, Option) { + match qvar.qtype { + // Already collapsed — just return it. + Collapsed(t) => (qvar, Some(t)), + // COLLAPSE THE WAVEFUNCTION! + Superposition(possible_types, var_seed, declared) => { + let collapsed = collapse_type(Superposition(possible_types, var_seed, declared), context, seed); + let updated = #{ + name: qvar.name, + qtype: Collapsed(collapsed), + observedAt: Some((observe_loc, context)), + declaredAt: qvar.declaredAt + }; + (updated, Some(collapsed)) + } + } +} + +// ============================================ +// Superposition detection over a program +// ============================================ + +// Whether a quantum variable is (still) in superposition. +fn is_superposed(qt: QuantumType) -> Bool { + match qt { + Superposition(_p, _s, _d) => true, + _ => false + } +} + +// Analyze a single statement, growing the accumulator of detected quantum +// variables. Only `let` without a type annotation introduces a quantum +// variable; if/elseif/else bodies are descended into. +fn analyze_stmt(acc: [(String, QuantumVariable)], seed: Int, stmt: Stmt) -> [(String, QuantumVariable)] { + match stmt { + LetStmt(_mutable, name, type_, value, loc) => + match type_ { + None => { + let qvar = create_quantum_variable(name, value, type_, loc, seed); + if is_superposed(qvar.qtype) { + acc ++ [(name, qvar)] + } else { + acc + } + }, + Some(_t) => acc + }, + IfStmt(_cond, then_, elseifs, else_, _loc) => { + let a1 = analyze_stmts(acc, seed, then_); + let a2 = fold(elseifs, a1, |a, pair| { + let (_eif_cond, body) = pair; + analyze_stmts(a, seed, body) + }); + match else_ { + Some(body) => analyze_stmts(a2, seed, body), + None => a2 + } + }, + _ => acc + } +} + +fn analyze_stmts(acc: [(String, QuantumVariable)], seed: Int, stmts: [Stmt]) -> [(String, QuantumVariable)] { + fold(stmts, acc, |a, s| analyze_stmt(a, seed, s)) +} + +// Analyze a declaration: only main-block and function bodies contain +// statements to scan. +fn analyze_decl(acc: [(String, QuantumVariable)], seed: Int, decl: Decl) -> [(String, QuantumVariable)] { + match decl { + MainBlock(body, _loc) => analyze_stmts(acc, seed, body), + FunctionDecl(_name, _params, _ret, body, _loc) => analyze_stmts(acc, seed, body), + _ => acc + } +} + +// Detect type-superposition paradoxes in a program. +pub fn detect_superposition(prog: Program, seed: Int) -> [(String, QuantumVariable)] { + fold(prog.declarations, [], |acc, decl| analyze_decl(acc, seed, decl)) +} + +// ============================================ +// Display +// ============================================ + +// Render a single typeExpr to its short name (mirrors the inner switch). +fn type_name(t: TypeExpr) -> String { + match t { + TyInt => "Int", + TyFloat => "Float", + TyString => "String", + TyBool => "Bool", + _ => "Unknown" + } +} + +// Format a quantum type for display. +pub fn format_quantum_type(qt: QuantumType) -> String { + match qt { + Collapsed(t) => type_name(t), + Superposition(possible_types, _s, _d) => + join(map(possible_types, type_name), " | ") + } +} + +// ============================================ +// Prediction & visualization +// ============================================ + +// Predict the collapse target and supply a human reason for it. +pub fn predict_collapse( + qt: QuantumType, + context: ObservationContext, + seed: Int +) -> (TypeExpr, String) { + let collapsed = collapse_type(qt, context, seed); + let reason = match context { + Arithmetic => "Used in arithmetic operation", + StringOp => "Used in string operation", + Comparison => "Used in comparison", + Print => "Printed to console", + Assignment => "Assigned to typed variable", + FunctionArg => "Passed as function argument" + }; + (collapsed, reason) +} + +// Generate a visualization of a type collapse. +pub fn visualize_collapse( + var_name: String, + before: QuantumType, + after: TypeExpr, + context: ObservationContext +) -> String { + let before_str = format_quantum_type(before); + let after_str = format_quantum_type(Collapsed(after)); + let context_str = match context { + Arithmetic => "arithmetic", + StringOp => "string operation", + Comparison => "comparison", + Print => "println", + Assignment => "assignment", + FunctionArg => "function call" + }; + "\n🌀 TYPE COLLAPSE DETECTED\n\nVariable: " ++ var_name + ++ "\nBefore: " ++ before_str ++ " (superposition)" + ++ "\nAfter: " ++ after_str ++ " (collapsed)" + ++ "\nContext: " ++ context_str + ++ "\n\nThe act of observation collapsed the type!\n" +} diff --git a/compiler/src/Types.affine b/compiler/src/Types.affine new file mode 100644 index 0000000..75f41c2 --- /dev/null +++ b/compiler/src/Types.affine @@ -0,0 +1,241 @@ +// SPDX-License-Identifier: MPL-2.0 +// Types.affine — core type definitions for Error-Lang +// Ported from compiler/src/Types.res. Port conventions: +// * ReScript inline-record variants -> positional constructor args. +// * array -> [T]; option -> Option; dict -> Dict; tuples kept. +// * Token variants `Float`/`String` renamed `FloatTok`/`StringTok` +// (`Float`/`String` are reserved type keywords in AffineScript). +// +// This is the `Types` module; sibling compiler modules `use Types::{...}`. +// Cross-module struct field access requires the affinescript module-resolver +// fix in patches/affinescript-module-struct-fields.patch. + +module Types; + +use prelude::*; + +pub struct Position { + line: Int, + column: Int, + offset: Int +} + +pub struct Location { + start: Position, + end_: Position, + file: String +} + +pub enum TokenType { + // Keywords + Main, End, Let, Mutable, Function, Struct, If, Elseif, Else, While, For, In, + Break, Continue, Return, And, Or, Not, True, False, Nil, Gutter, Fn, + // Types + TInt, TFloat, TString, TBool, TArray, TEcho, TEchoR, + // Literals + Integer(Int), + FloatTok(Float), // ReScript Float(float) + StringTok(String), // ReScript String(string) + Identifier(String), + // Operators + Plus, Minus, Star, Slash, Percent, EqualEqual, BangEqual, Less, Greater, + LessEqual, GreaterEqual, Ampersand, Pipe, Caret, Tilde, LessLess, GreaterGreater, + Equal, Arrow, Question, Colon, + // Delimiters + LParen, RParen, LBracket, RBracket, LBrace, RBrace, Comma, Dot, + // Special + Newline, EOF, Error(String) +} + +pub struct Token { + type_: TokenType, + lexeme: String, + loc: Location +} + +// ============================================ +// AST +// ============================================ + +pub enum Expr { + IntLit(Int, Location), + FloatLit(Float, Location), + StringLit(String, Location), + BoolLit(Bool, Location), + NilLit(Location), + Ident(String, Location), + Array([Expr], Location), + Binary(Expr, BinaryOp, Expr, Location), + Unary(UnaryOp, Expr, Location), + Call(Expr, [Expr], Location), + Index(Expr, Expr, Location), + Member(Expr, String, Location), + Ternary(Expr, Expr, Expr, Location), + Lambda([Param], Option, LambdaBody, Location) +} + +pub enum BinaryOp { + Add, Sub, Mul, Div, Mod, + Eq, Neq, Lt, Gt, Lte, Gte, + BAnd, BOr, BXor, Shl, Shr, + LAnd, LOr +} + +pub enum UnaryOp { Neg, LNot, BNot } + +pub struct Param { + name: String, + type_: Option, + loc: Location +} + +pub enum TypeExpr { + TyInt, + TyFloat, + TyString, + TyBool, + TyArray(TypeExpr), + // Echo types (Trope-IR-ready, see docs/Trope-Particularity-Integration.adoc): + // TyEcho ~ Trope[Phi] (retained witness) + // TyEchoResidue ~ FloatingQuality (witness severed) + TyEcho(Option, Option), + TyEchoResidue(Option, Option), + TyIdent(String) +} + +pub enum LambdaBody { + LambdaExpr(Expr), + LambdaBlock([Stmt]) +} + +pub enum Stmt { + // inline records -> positional: (mutable_, name, type_, value, loc) + LetStmt(Bool, String, Option, Expr, Location), + // (target, value, loc) + AssignStmt(Expr, Expr, Location), + // (cond, then_, elseifs, else_, loc) + IfStmt(Expr, [Stmt], [(Expr, [Stmt])], Option<[Stmt]>, Location), + // (cond, body, loc) + WhileStmt(Expr, [Stmt], Location), + // (var, iter, body, loc) + ForStmt(String, Expr, [Stmt], Location), + // (value, loc) + ReturnStmt(Option, Location), + BreakStmt(Location), + ContinueStmt(Location), + // (println, args, loc) + PrintStmt(Bool, [Expr], Location), + // (tokens, recovered, loc) + GutterBlock([Token], Bool, Location), + ExprStmt(Expr) +} + +pub enum Decl { + // (name, params, returnType, body, loc) + FunctionDecl(String, [Param], Option, [Stmt], Location), + // (name, fields, loc) + StructDecl(String, [(String, TypeExpr)], Location), + // (body, loc) + MainBlock([Stmt], Location), + StmtDecl(Stmt) +} + +pub struct Program { + declarations: [Decl], + loc: Location +} + +// ============================================ +// Errors +// ============================================ + +pub enum ErrorCode { + E0001, E0002, E0003, E0004, E0005, E0006, E0007, E0008, E0009, E0010 +} + +pub struct Diagnostic { + code: ErrorCode, + message: String, + loc: Location, + runNumber: Int, + hint: Option +} + +// ============================================ +// Runtime state & stability +// ============================================ + +pub enum StabilityFactor { + MutableState(Int, Int), // mutations, readers + TypeInstability(Int), // reassignments + NullPropagation(Int), // depth + GlobalState(Int, Int), // mutations, dependencies + UnhandledError(Int), // paths + AlgorithmComplexity(Float), // time_ms + MemoryLeak(Int), // bytes + RaceCondition(Int) // conflicts +} + +pub struct StabilityReport { + score: Int, + factors: [StabilityFactor], + breakdown: Dict, + recommendations: [String] +} + +pub struct RuntimeState { + runCounter: Int, + stabilityScore: Int, + lastError: Option, + seed: Int, + stabilityFactors: [StabilityFactor], + discoveredRules: [String], + historicalRuns: [Int] +} + +pub fn make_default_state() -> RuntimeState { + #{ + runCounter: 0, + stabilityScore: 100, + lastError: None, + seed: 0, + stabilityFactors: [], + discoveredRules: [], + historicalRuns: [] + } +} + +// Stability impact (non-positive), mirrors Types.res `stabilityImpact`. +pub fn stability_impact(factor: StabilityFactor) -> Int { + match factor { + MutableState(mutations, readers) => -(10 * mutations + 5 * readers), + TypeInstability(reassignments) => -(15 * reassignments), + NullPropagation(depth) => -(20 * depth), + GlobalState(mutations, dependencies) => -(30 * mutations + 5 * dependencies), + UnhandledError(paths) => -(25 * paths), + AlgorithmComplexity(time_ms) => -trunc(time_ms / 10.0), + MemoryLeak(bytes) => -(10 * (bytes / 1024)), + RaceCondition(conflicts) => -(40 * conflicts) + } +} + +// mirrors Types.res `calculateStability`: max(0, 100 + sum(impacts)) +pub fn calculate_stability(factors: [StabilityFactor]) -> Int { + let penalties = fold(factors, 0, |acc, x| acc + stability_impact(x)); + max(0, 100 + penalties) +} + +pub fn error_code_to_string(code: ErrorCode) -> String { + match code { + E0001 => "E0001", + E0002 => "E0002", + E0003 => "E0003", + E0004 => "E0004", + E0005 => "E0005", + E0006 => "E0006", + E0007 => "E0007", + E0008 => "E0008", + E0009 => "E0009", + E0010 => "E0010" + } +} diff --git a/docs/Trope-Particularity-Integration.adoc b/docs/Trope-Particularity-Integration.adoc new file mode 100644 index 0000000..ea4ad12 --- /dev/null +++ b/docs/Trope-Particularity-Integration.adoc @@ -0,0 +1,246 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Trope-Particularity Integration: Error-Lang as a Trope IR Front End +:toc: +:sectnums: +:source-highlighter: rouge + +[abstract] +This is a *design* (not yet implemented). It proposes that Error-Lang become a +second *front end* to the portable trope-checker +(https://github.com/hyperpolymath/trope-checker[`hyperpolymath/trope-checker`]), +lowering its Echo operations and its stability factors to the language-neutral +*Trope IR* (v0.1, `prevent` profile) and consuming the checker's verified verdict +and witness. It defines the object/effect/grade correspondence, the verdict +mapping, the architecture (reference, never vendor), and — most importantly — the +per-front-end *lowering-correctness obligations* the trope-checker does **not** +discharge for us. + +Both systems already sit on the same substrate: the +https://github.com/hyperpolymath/echo-types[echo-types] graded-loss line, cited +verbatim by `docs/Echo-Decomposition.adoc` and by the trope calculus +(`trope-checker/spec/calculus.adoc`, "Provenance of the ideas"). This document +makes that shared lineage *operational*. + +== Motivation: a stability score is a scalar; loss is not + +Error-Lang grades instability with `calculateStability` (`compiler/src/Types.res` +lines 270–274): + +[source] +---- +calculateStability(factors) = max(0, 100 + Σ stabilityImpact(factor)) +---- + +Every `stabilityFactor` is mapped to a single negative integer and the integers +are summed. That is a *scalar collapse* of structured loss. The trope-particularity +calculus exists to reject exactly this move — its load-bearing thesis +(`calculus.adoc` §3) is: + +[quote] +A grade is *not a scalar*: two operations can lose the same _amount_ yet differ +in _kind_ and in _honesty_. + +So the calculus's three-coordinate grade is a principled *upgrade* of Error-Lang's +stability model. It lets us keep _which_ particularity degraded, whether the loss +is _recoverable_, and whether it is _honest_ — and it yields a use-relative +*verdict* with a *witness edge* ("the operation to repair") in place of an opaque +`0–100` number. For a language whose entire identity is the *visible decomposition* +of structure (`Echo-Decomposition.adoc`, "Decomposition must be visible"), this is +a capability upgrade, not ornament. + +Two further alignments make the fit unusually tight: + +* **The Echo operations already _are_ trope effects.** `echo`, `echo_to_residue`, + `echo_input`, `echo_output` implement witness-retention and irreversible erasure + — which the calculus names `preserve`, `detach`, and field `project` (§5). +* **The verification toolchains already overlap.** The trope-checker's core is an + Agda reference plus an Idris2 implementation (the `trope-checker` repo's Idris2 core, `Main.idr`); + Error-Lang already carries an Idris2 proof of the *scalar* bound + (`src/abi/Stability.idr`). The integration generalises that proof's target from + a clamped integer to a checked grade. + +== The correspondence + +=== Objects: Echo ↔ trope, EchoR ↔ FloatingQuality + +A trope is a property-instance over the field set +`Φ = {quality, bearer, context, record}` (`calculus.adoc` §2). Error-Lang's +`Echo` — a retained witness `x : A` with the visible output `y : B` it +reached — populates Φ as: + +[cols="1,2,3",options="header"] +|=== +| Φ field | Echo content | Justification + +| `bearer` | the witness `x : A` | the *particular* entity the result is a result _of_ +| `quality` | the reached output `y : B` (and `f x ≡ y`) | the situated property borne by `x` +| `context` | the function `f` / evaluation site | what individuates this fibre element +| `record` | the runtime pairing `VEcho{input,output}` | honest provenance of how `y` arose +|=== + +[cols="1,2",options="header"] +|=== +| Echo form | Trope IR node + +| `Echo` | `type: "Trope"`, `present: ["quality","bearer","context","record"]` +| `EchoR` | `type: "FloatingQuality"`, `present: ["quality"]` (no `bearer` — the severance is structurally visible) +|=== + +The type change `Echo → EchoR` is exactly the type change `Trope → FloatingQuality`, +and the reason `echo_input` is *illegal on a residue* (`Echo-Decomposition.adoc` +Plane 3) is, in IR terms, that a `FloatingQuality` node has *no bearer field to +project*. The same fact, two vocabularies. + +=== Echo operations → writable effects + +[cols="2,2,3",options="header"] +|=== +| Echo op | Effect | Grade (per `calculus.adoc` §5) + +| `echo(x,y)` | `preserve` | `ε` — all fields `Present`, `bond=Intact`, `merge=Single` +| `echo_output(e)` | `project[quality]` | drop `bearer,context,record`; quality survives; `bond=Withheld` +| `echo_input(e)` | `project[bearer]` | legal only while `bearer ∈ S`; *undefined on `FloatingQuality`* +| `echo_to_residue(e)`| `detach` | `sever`: `fate(quality)=Present`, others `Dropped`, `bond=Severed`, `merge=Single` +|=== + +The `[Stab-Erase]` rule (`spec/type-system.md` §7) debits stability *exactly once*, +on `echo_to_residue`, and never on projection. That is precisely the calculus's +accounting: `detach` carries the `Severed` (irrecoverable) loss; `project` carries +only a recoverable `Withheld`. The educational invariant "`echo_to_residue` must +**not** become a silent cast" is the calculus's refusal of untagged/deceptive +collapse. + +.Worked Trope IR — `echo_to_residue` as a `detach` (illustrative, schema-shaped) +[source,json] +---- +{ + "version": "0.1", "profile": "prevent", + "nodes": [ + { "id": "e", "type": "Trope", "present": ["quality","bearer","context","record"] }, + { "id": "res", "type": "FloatingQuality", "present": ["quality"] } + ], + "edges": [ + { "id": "erase", "effect": "detach", "inputs": ["e"], "output": "res", + "grade": { + "fate": { "quality": {"k":"Present"}, "bearer": {"k":"Dropped"}, + "context": {"k":"Dropped"}, "record": {"k":"Dropped"} }, + "bond": { "k": "Severed" }, "merge": { "k": "Single" } }, + "note": "echo_to_residue: witness erased, output reachable" } + ], + "use_model": { "output": "res", "floor": { "bond": { "k": "Withheld" } } } +} +---- + +Here the floor demands `bond ⊒ Withheld` (the use needs a _recoverable_ bearer); +since `detach` delivered `Severed`, the verdict is `p-insufficient`, witness = +`erase`. A use that only reads `echo_output` would declare a quality-only floor and +pass. The score becomes a *reason*. + +=== stabilityFactor → grade + +Each `stabilityFactor` becomes a grade, with its `stabilityImpact` magnitude +feeding the fidelity element `δ`. Crucially, the two *silent* instabilities land +on the deceptive `Conflated` bottom — an untagged merge of particulars — which, +under the `prevent` profile, is a *lowering fault* the validator rejects by name. +Error-Lang's worst bugs are the calculus's moral-core violation. + +[cols="2,3,2",options="header"] +|=== +| Factor | Grade (faithful lowering) | Honesty + +| `TypeInstability{reassignments}` | `fate(quality)=Attenuated(15·r)` | faithful +| `NullPropagation{depth}` | `fate(quality)=Attenuated(20·d)`, `Dropped` at the leaf | faithful +| `UnhandledError{paths}` | `fate=Dropped` on the unguarded error fields | faithful (visible gap) +| `AlgorithmComplexity{time_ms}` | `fate=Attenuated(δ)`, `δ=⊤` when unbounded (matches `fix`→`⊤`, §7) | faithful +| `MutableState{mutations,readers}` | `fate(quality)=Attenuated(10·m+5·r)`; `Fused(τ=write-site)` if writes blend | faithful if tracked +| `MemoryLeak{bytes}` | `detach`: `bond=Severed` (owner unreachable, irrecoverable) | faithful +| `GlobalState{mutations,deps}` | `Fused(τ=global@site)` if threaded; **`Conflated` (fault)** if silent | *deceptive when silent* +| `RaceCondition{conflicts}` | `Fused(τ=lock)` if serialised; **`Conflated` (fault)** if unsynchronised | *deceptive when silent* +|=== + +=== Verdict and witness + +[cols="1,2",options="header"] +|=== +| Error-Lang today | Trope-checker + +| `score = max(0,100+Σ)` | `p-sufficient ⟺ floor(U) ⊑ acc(output)` +| (no locus) | `p-insufficient` + *witness edge* = first edge whose accumulated grade drops below the floor +| `breakdown : dict` | per-coordinate retention at each node +| `recommendStabilization(factor)` | human advice *attached to the witnessed edge* (now principled, not heuristic) +| `Stability.idr`: `score ∈ [0,100]` | grade soundness (`calculus.adoc` §8): declared grade never over-claims retention +|=== + +The witness is, by the calculus's own statement (§6.2), "the trope-particularity +analogue of the invariant-path argmin" — the same argmin shape `Stability.idr` +already reasons about. The verdict thus _subsumes_ the current score: the score is +recoverable as a projection, but the verdict additionally names the edge to repair. + +== Architecture: reference, never vendor + +[cols="1,3",options="header"] +|=== +| Concern | Decision + +| Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary"). +| Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`. +| New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics. +| Precedent | The same trust-tagged "fold external prover output back into our report" pattern the panic-attack repo uses in its `aggregate/` module. +| Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer. +|=== + +== O2 — lowering-correctness obligations (ours to discharge) + +The trope-checker proves the *composition* of grades is sound. It explicitly does +**not** prove that an Error-Lang construct lowered to effect `X` _is_ an `X` +(`calculus.adoc` §8, firewall 2; §10-O2). Those are our proof obligations: + +[cols="1,4",options="header"] +|=== +| ID | Obligation + +| *L-Echo* | `OpEchoToResidue` (`VM.res`) semantically _is_ `detach`: the witness becomes unreachable ⇒ `bond=Severed`; output reachability survives ⇒ `fate(quality)=Present`. **Open decision:** is residue's quality `Present`, or `Attenuated(δ)` (only "reachability", not full `y`)? This must be fixed before Phase 1 freezes the lowering. +| *L-Grade* | Each `stabilityFactor`'s grade is a *faithful over-approximation* of the real loss (grade-soundness direction: never claim more retention than occurs). The current `stabilityImpact` magnitudes are heuristic; for soundness `δ` must be a conservative loss bound. +| *L-Silent* | The `Conflated` lowering of `GlobalState`/`RaceCondition` is correct only when the merge is genuinely untagged. If a provenance tag is recoverable, we MUST emit `Fused(τ)` instead; emitting `Conflated` for a tractable merge is a false positive. +| *L-Floor* | The `use_model` floor Error-Lang emits faithfully encodes the program's declared stability requirement (per-function loss signatures, §7 "Declared signatures at the boundaries"). +|=== + +These mirror, in Error-Lang's setting, the open obligations the calculus states for +itself (O1–O4) — and they are checkable with the *same* Idris2 discipline already +used in `src/abi/`. + +== Phasing + +[cols="1,3",options="header"] +|=== +| Phase | Work + +| *0 (now)* | Shape the AffineScript Echo types (during the ReScript→AffineScript port) so `Echo`/`EchoR`/`echo_to_residue` lower cleanly to `Trope`/`FloatingQuality`/`detach`. This document + cross-references. *No new runtime coupling.* +| *1* | Implement the `trope` lowering backend for the Echo operations only (the tightest correspondence). Emit schema-valid IR; conformance-test against `trope-checker/tests/conformance/fixtures/`. +| *2* | Lower `stabilityFactor` → grade and emit a `use_model`; surface the verdict + witness as diagnostics alongside (then in place of) the scalar score. +| *3* | Discharge L-Echo / L-Grade / L-Silent / L-Floor as Idris2/Agda proofs; CI-gate the lowering. +|=== + +== Open questions + +* *Profile.* Adopt `prevent` (silent merges rejected at validation — strongest, and + on-message for "decomposition must be visible") or `detect` (representable, caught + at the verdict)? This design assumes `prevent`. +* *Residue fidelity* (L-Echo): `Present` vs `Attenuated(δ)` for `echo_to_residue`. +* *Floor authorship.* Where do use-models come from — a whole-program default, or + per-function loss-signature annotations the learner writes? +* *Coverage* (calculus O1): are all eight `stabilityFactor`s expressible with the + six writable effects? The table above is a well-chosen mapping, not yet a theorem. + +== See also + +* `docs/Echo-Decomposition.adoc` — the three decomposition planes this builds on. +* `docs/Design-Philosophy.adoc` — consequence amplification and the stability score. +* `spec/type-system.md` §7 — typing rules and the `[Stab-Erase]` stability debit. +* `src/abi/Stability.idr` — the existing Idris2 bound proof (verdict-soundness anchor). +* External (referenced, not vendored): + https://github.com/hyperpolymath/trope-checker[trope-checker] (`spec/calculus.adoc`, + `spec/trope-ir.adoc`, `schemas/trope-ir.schema.json`), + https://github.com/hyperpolymath/trope-particularity-workbench[trope-particularity-workbench] + (the nine effects), https://github.com/hyperpolymath/echo-types[echo-types] (shared substrate). diff --git a/patches/README.adoc b/patches/README.adoc new file mode 100644 index 0000000..f5711c1 --- /dev/null +++ b/patches/README.adoc @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += AffineScript toolchain patches +:toc: + +Patches applied to a fresh `hyperpolymath/affinescript` checkout by +`scripts/install-affinescript-toolchain.sh` before building the compiler, to +support the ReScript -> AffineScript migration. Each is a stop-gap pending +upstream; drop it from the install script once upstreamed. + +== affinescript-module-struct-fields.patch + +*Problem.* AffineScript's module resolver exported imported *enum* constructors +but dropped imported *struct/alias* type definitions: `lib/resolve.ml` registered +`TyEnum` variant constructors for imported modules but had a bare +`| TyAlias _ | TyStruct _ | TyExtern -> ()`. Field access on an imported struct +therefore failed with `Field 'x' not found in type T` — the named type stayed an +opaque `TCon` and never expanded to its `TRecord`. + +This blocked a per-module `.res -> .affine` port: the shared AST in +`compiler/src/Types.affine` (`Location`, `Token`, `Position`, ...) is +field-accessed by every other compiler module. + +*Fix.* Thread imported modules' `type_env` (struct/alias/enum type definitions) +and `constructor_env` into the importing module's type-check context, mirroring +the existing `name_types` (scheme) threading that already made enums cross: + +* `lib/typecheck.ml` — `check_program` gains `?import_type_env` / + `?import_constructor_env`, seeding `ctx.type_env` / `ctx.constructor_env`. +* `lib/resolve.ml` — a new `import_type_defs` copies a resolved module's + `type_env` / `constructor_env` into the destination context, called from all + three import forms (`use M;`, `use M::{...}`, `use M::*`); the imported-module + check site passes the new params. +* `bin/main.ml` — the `check` / `compile` / `eval` entry points pass the threaded + `type_env` / `constructor_env` to `check_program`. + +*Verification.* A module importing a struct and accessing its (nested) fields, +constructing it, and matching on an imported enum field now type-checks; existing +stdlib cross-module imports (`http_fetch`, `option`, `io`) still pass. + +*Upstream.* This belongs in `hyperpolymath/affinescript` — it fixes any multi-file +AffineScript program, not only error-lang. It could not be pushed from the +migration session (affinescript was outside the session's repo scope); upstream +when convenient, then delete this patch and its hook in the install script. diff --git a/patches/affinescript-module-struct-fields.patch b/patches/affinescript-module-struct-fields.patch new file mode 100644 index 0000000..54aae35 --- /dev/null +++ b/patches/affinescript-module-struct-fields.patch @@ -0,0 +1,142 @@ +diff --git a/bin/main.ml b/bin/main.ml +index 8230ab2..b772a3c 100644 +--- a/bin/main.ml ++++ b/bin/main.ml +@@ -195,6 +195,8 @@ let check_file face json path = + resolve_refs := List.rev resolve_ctx.references; + (match Affinescript.Typecheck.check_program + ~import_types:type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + add (Affinescript.Json_output.of_type_error e) +@@ -242,6 +244,8 @@ let check_file face json path = + | Ok (resolve_ctx, type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + Format.eprintf "@[%s@]@." +@@ -505,6 +509,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc + | Ok (resolve_ctx, import_type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:import_type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + add (Affinescript.Json_output.of_type_error e) +@@ -732,6 +738,8 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc + | Ok (resolve_ctx, import_type_ctx) -> + (match Affinescript.Typecheck.check_program + ~import_types:import_type_ctx.Affinescript.Typecheck.name_types ++ ~import_type_env:import_type_ctx.Affinescript.Typecheck.type_env ++ ~import_constructor_env:import_type_ctx.Affinescript.Typecheck.constructor_env + resolve_ctx.symbols prog with + | Error e -> + Format.eprintf "@[%s@]@." +diff --git a/lib/resolve.ml b/lib/resolve.ml +index 65a6b48..65a9206 100644 +--- a/lib/resolve.ml ++++ b/lib/resolve.ml +@@ -654,6 +654,20 @@ let import_specific_items + Error (UndefinedVariable item.ii_name, item.ii_name.span) + ) (Ok ()) items + ++(** Thread imported struct/alias/enum type definitions and value constructors ++ from a resolved source module into the destination type-check context, so ++ that field access on an imported struct resolves (companion to the scheme ++ imports above — a struct needs its TRecord definition, not just a ++ name_types scheme). *) ++let import_type_defs ++ (dest : Typecheck.context) (source : Typecheck.context) : unit = ++ Hashtbl.iter (fun name ty -> ++ Hashtbl.replace dest.Typecheck.type_env name ty ++ ) source.Typecheck.type_env; ++ Hashtbl.iter (fun name ty -> ++ Hashtbl.replace dest.Typecheck.constructor_env name ty ++ ) source.Typecheck.constructor_env ++ + (** Resolve imports in a program using module loader *) + let rec resolve_and_typecheck_module + (loader : Module_loader.t) +@@ -698,7 +712,10 @@ let rec resolve_and_typecheck_module + imported modules must check the same way top-level programs do.) *) + match + Typecheck.check_program +- ~import_types:type_ctx.Typecheck.name_types symbols prog ++ ~import_types:type_ctx.Typecheck.name_types ++ ~import_type_env:type_ctx.Typecheck.type_env ++ ~import_constructor_env:type_ctx.Typecheck.constructor_env ++ symbols prog + with + | Ok final_ctx -> Ok (symbols, final_ctx) + | Error type_err -> +@@ -729,6 +746,7 @@ and resolve_imports_with_loader + mod_type_ctx.Typecheck.var_types + mod_type_ctx.Typecheck.name_types + alias_str; ++ import_type_defs type_ctx mod_type_ctx; + Ok () + | Error e -> Error e + end +@@ -747,13 +765,15 @@ and resolve_imports_with_loader + (* Resolve and type-check the module *) + begin match resolve_and_typecheck_module loader loaded_mod with + | Ok (mod_symbols, mod_type_ctx) -> +- import_specific_items ctx.symbols ++ let* () = import_specific_items ctx.symbols + type_ctx.Typecheck.var_types + type_ctx.Typecheck.name_types + mod_symbols + mod_type_ctx.Typecheck.var_types + mod_type_ctx.Typecheck.name_types +- items ++ items in ++ import_type_defs type_ctx mod_type_ctx; ++ Ok () + | Error e -> Error e + end + | Error (Module_loader.ModuleNotFound _) -> +@@ -785,6 +805,7 @@ and resolve_imports_with_loader + sym) + | _ -> () + ) mod_symbols.all_symbols; ++ import_type_defs type_ctx mod_type_ctx; + Ok () + | Error e -> Error e + end +diff --git a/lib/typecheck.ml b/lib/typecheck.ml +index e38e302..4390c71 100644 +--- a/lib/typecheck.ml ++++ b/lib/typecheck.ml +@@ -2401,6 +2401,8 @@ let populate_call_effects (ctx : context) (prog : Ast.program) : unit = + Effect_sites.set_async_by_ord async_tbl + + let check_program ?(import_types : (string, scheme) Hashtbl.t option) ++ ?(import_type_env : (string, ty) Hashtbl.t option) ++ ?(import_constructor_env : (string, ty) Hashtbl.t option) + (symbols : Symbol.t) (prog : Ast.program) + : (context, type_error) Result.t = + try +@@ -2423,6 +2425,17 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option) + Option.iter (fun tbl -> + Hashtbl.iter (fun name sc -> Hashtbl.replace ctx.name_types name sc) tbl + ) import_types; ++ (* Thread imported struct/alias/enum type definitions (type_env) and value ++ constructors (constructor_env) so field access on an imported struct ++ resolves: enums already cross via name_types schemes, but a struct's ++ TRecord definition must be present for a named param type to expand to ++ its fields (otherwise it stays an opaque TCon -> FieldNotFound). *) ++ Option.iter (fun tbl -> ++ Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.type_env name ty) tbl ++ ) import_type_env; ++ Option.iter (fun tbl -> ++ Hashtbl.iter (fun name ty -> Hashtbl.replace ctx.constructor_env name ty) tbl ++ ) import_constructor_env; + (* Forward pass: register all types, effects, traits, impls, and + function signatures so that mutually recursive declarations resolve. *) + let* () = List.fold_left (fun acc decl -> diff --git a/scripts/install-affinescript-toolchain.sh b/scripts/install-affinescript-toolchain.sh new file mode 100755 index 0000000..3b4e694 --- /dev/null +++ b/scripts/install-affinescript-toolchain.sh @@ -0,0 +1,57 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# install-affinescript-toolchain.sh — build & install the AffineScript compiler +# (hyperpolymath/affinescript, the OCaml/dune compiler) so error-lang's `.affine` +# sources — which replace the legacy ReScript per the Hyperpolymath language +# policy — can be typechecked and compiled. +# +# Why build from distro OCaml packages instead of opam: some CI/network policies +# block opam.ocaml.org. Every dependency below is available from the Debian/Ubuntu +# archive at a version satisfying affinescript's dune-project constraints +# (notably ocaml-dune 3.14 == `(lang dune 3.14)`). +# +# Network note: this clones github.com/hyperpolymath/affinescript directly; run it +# where GitHub is reachable (a normal CI runner or dev box). +set -euo pipefail + +AFFINE_REPO="${AFFINE_REPO:-https://github.com/hyperpolymath/affinescript}" +AFFINE_SRC="${AFFINE_SRC:-${TMPDIR:-/tmp}/affinescript}" +PREFIX="${PREFIX:-/usr/local}" +SUDO="$(command -v sudo || true)" + +# 1. OCaml toolchain + AffineScript build dependencies. +$SUDO apt-get update +$SUDO apt-get install -y \ + ocaml-dune menhir libmenhir-ocaml-dev libsedlex-ocaml-dev \ + libppx-deriving-ocaml-dev libppx-sexp-conv-ocaml-dev libsexplib0-ocaml-dev \ + libfmt-ocaml-dev libcmdliner-ocaml-dev libyojson-ocaml-dev \ + libppxlib-ocaml-dev libjs-of-ocaml-dev + +# 2. Fetch the compiler. +[ -d "$AFFINE_SRC/.git" ] || git clone --depth 1 "$AFFINE_REPO" "$AFFINE_SRC" + +# 2a. Apply the module-resolver fix (export imported struct field definitions so +# cross-module struct field access type-checks) until it is upstreamed to +# affinescript. See patches/README.adoc. Idempotent: skipped if already applied. +PATCH="$(cd "$(dirname "$0")/.." && pwd)/patches/affinescript-module-struct-fields.patch" +if [ -f "$PATCH" ] && git -C "$AFFINE_SRC" apply --check "$PATCH" 2>/dev/null; then + git -C "$AFFINE_SRC" apply "$PATCH" && echo "applied $PATCH" +else + echo "module-struct-fields patch: already applied or not applicable — continuing" +fi + +# 3. Build the compiler binary. +( cd "$AFFINE_SRC" && dune build bin/main.exe ) + +# 3. Install the binary + stdlib. The module loader discovers the stdlib at +# /../share/affinescript/stdlib, so this needs no env var. +$SUDO install -m755 "$AFFINE_SRC/_build/default/bin/main.exe" "$PREFIX/bin/affinescript" +$SUDO mkdir -p "$PREFIX/share/affinescript" +$SUDO rm -rf "$PREFIX/share/affinescript/stdlib" +$SUDO cp -r "$AFFINE_SRC/stdlib" "$PREFIX/share/affinescript/stdlib" + +echo "Installed: $(command -v affinescript)" +affinescript check "$AFFINE_SRC/examples/hello.affine" || true +echo "AffineScript toolchain installed under $PREFIX." diff --git a/src/abi/Foreign.idr b/src/abi/Foreign.idr index f3158df..1bfa14a 100644 --- a/src/abi/Foreign.idr +++ b/src/abi/Foreign.idr @@ -9,13 +9,39 @@ ||| All functions have type signatures and safety guarantees proven at ||| compile-time through dependent types. -module ErrorLang.ABI.Foreign - -import ErrorLang.ABI.Types -import ErrorLang.ABI.Layout +module Foreign %default total +-------------------------------------------------------------------------------- +-- Minimal ABI value types (inlined so this binding module is self-contained +-- and independently checkable: `idris2 --check Foreign.idr` from src/abi). +-- The previous external `ErrorLang.ABI.Types` / `ErrorLang.ABI.Layout` modules +-- were removed. The fabricated "Safety Proofs" that lived here -- which used +-- `cast ()` / `cast Refl` over IO actions to manufacture evidence -- have been +-- replaced by genuine, machine-checked proofs in the sibling modules +-- Stability.idr, Positional.idr and Paradox.idr. +-- +-- This file is a BINDING-DECLARATION layer only: it declares the C ABI of the +-- Zig haptics library (ffi/zig). It asserts no theorems. +-------------------------------------------------------------------------------- + +||| Result codes (must match the Zig `Result` enum in ffi/zig/src/main.zig). +public export +data Result = Ok | Error | InvalidParam | OutOfMemory | NullPointer + +||| Opaque handle to a library instance (wraps the C pointer as Bits64). +public export +record Handle where + constructor MkHandle + handlePtr : Bits64 + +||| Build a handle from a raw pointer; a null (0) pointer yields Nothing. +export +createHandle : Bits64 -> Maybe Handle +createHandle 0 = Nothing +createHandle p = Just (MkHandle p) + -------------------------------------------------------------------------------- -- Library Lifecycle -------------------------------------------------------------------------------- @@ -234,50 +260,18 @@ isInitialized h = do pure (result /= 0) -------------------------------------------------------------------------------- --- Safety Proofs +-- Safety properties -------------------------------------------------------------------------------- - -||| Theorem: Stability scores are always bounded [0, 100] -||| -||| Proof: The Zig implementation validates all score inputs in -||| error_lang_set_stability_factor, rejecting any value < 0 or > 100. -||| The weighted average in error_lang_calculate_stability preserves -||| this bound through convex combination. -export -stabilityBounded : (h : Handle) -> (factor : Bits8) -> - IO (Either Result (score : Double ** (0.0 <= score, score <= 100.0))) -stabilityBounded h factor = do - score <- getStabilityFactor h factor - -- Runtime check (could be proven statically with refinement types) - if score >= 0.0 && score <= 100.0 - then pure (Right (score ** (cast (), cast ()))) - else pure (Left Error) - -||| Theorem: Positional operator behavior is deterministic -||| -||| Proof: For any given (line, column, operatorType) triple, the Zig -||| implementation always returns the same behavior. The calculation is -||| purely functional (column % n) with no hidden state. -export -positionalDeterministic : (h : Handle) -> (line, column : Bits32) -> (op : Bits8) -> - IO (b1 : Bits8 ** (b2 : Bits8 ** (b1 = b2))) -positionalDeterministic h line column op = do - b1 <- positionalOperator h line column op - b2 <- positionalOperator h line column op - -- In practice, should always be equal - pure (b1 ** (b2 ** cast Refl)) - -||| Theorem: Paradox detection is monotonic with respect to code complexity -||| -||| As lineCount, varCount, or depth increase, the set of detected paradoxes -||| (represented as a bitmask) cannot decrease. -export -paradoxMonotonic : (h : Handle) -> - (lc1, lc2, vc1, vc2, d1, d2 : Bits32) -> - (lc1 <= lc2) -> (vc1 <= vc2) -> (d1 <= d2) -> - IO (p1 : Bits32 ** (p2 : Bits32 ** ((p1 .&. p2) = p1))) -paradoxMonotonic h lc1 lc2 vc1 vc2 d1 d2 _ _ _ = do - p1 <- detectParadoxes h lc1 vc1 d1 - p2 <- detectParadoxes h lc2 vc2 d2 - -- Monotonicity should hold in practice (bitwise subset) - pure (p1 ** (p2 ** cast Refl)) +-- The properties this ABI relies on are proved -- genuinely, with no escape +-- hatch and machine-checked under Idris2 0.8.0 -- in the sibling modules, NOT +-- here: +-- * stability score in [0,100] -> Stability.idr (stabilityUpperBound) +-- * positional operator determinism -> Positional.idr (positionalDeterministic) +-- * paradox-factor monotonicity -> Paradox.idr (superpositionMonotone, +-- temporalMonotone) +-- +-- The earlier `stabilityBounded` / `positionalDeterministic` / `paradoxMonotonic` +-- definitions here were unsound: they used `cast ()` / `cast Refl` over `IO` +-- actions to fabricate evidence. Removed 2026-06-23. Proving the third one +-- honestly also revealed that the *global* monotonicity claim is false of the +-- implementation -- scope leakage is prime-gated; see Paradox.idr. diff --git a/src/abi/Paradox.idr b/src/abi/Paradox.idr new file mode 100644 index 0000000..331c1ff --- /dev/null +++ b/src/abi/Paradox.idr @@ -0,0 +1,77 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Paradox-detection monotonicity (error-lang formal core, property 3 of 3). +||| +||| Mirrors the Zig FFI `error_lang_detect_paradoxes` +||| (`ffi/zig/src/main.zig`, lines 280-315), which sets: +||| * type_superposition when var_count > 10 (threshold; monotone) +||| * scope_leakage when isPrime(line) (prime-gated; NOT monotone) +||| * temporal_corruption when depth > 5 (threshold; monotone) +||| +||| HONEST FINDING. The previously-claimed blanket theorem "paradox detection +||| is monotonic with complexity" (README, WHITEPAPER §7, COMPLETION report) +||| is FALSE of the implementation: scope_leakage is gated on the PRIMALITY of +||| the line number, which is not monotone (line 7 is prime -> active; line 8 +||| is composite -> inactive, although 8 > 7). The original +||| `Foreign.idr :: paradoxMonotonic` hid this with `cast Refl`; attempting the +||| proof honestly surfaces that the blanket claim cannot hold. +||| +||| What IS true, and is proved here: the two THRESHOLD-gated factors are +||| monotone in their driving metric. The blanket claim is therefore retracted +||| in favour of these two component lemmas (see PROOF-NEEDS.md). Non-monotone +||| scope leakage is intentional -- it is the pedagogical point of the paradox. +||| +||| Self-contained; no escape hatches. Machine-check is a CI obligation. +module Paradox + +import Data.Nat + +%default total + +||| Transitivity of <= (self-contained; the standard definition). +lteTrans : LTE a b -> LTE b c -> LTE a c +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc p) (LTESucc q) = LTESucc (lteTrans p q) + +-- ─────────────────────────────────────────────────────────────────────── +-- Threshold-gated factors (monotone) +-- ─────────────────────────────────────────────────────────────────────── + +||| type_superposition fires when var_count exceeds 10 (11 <= var_count). +public export +SuperpositionActive : (varCount : Nat) -> Type +SuperpositionActive varCount = LTE 11 varCount + +||| temporal_corruption fires when depth exceeds 5 (6 <= depth). +public export +TemporalActive : (depth : Nat) -> Type +TemporalActive depth = LTE 6 depth + +||| THEOREM: type_superposition is monotone in var_count -- growing the +||| variable count never deactivates it. +public export +superpositionMonotone : (v1, v2 : Nat) -> LTE v1 v2 -> + SuperpositionActive v1 -> SuperpositionActive v2 +superpositionMonotone _ _ le active = lteTrans active le + +||| THEOREM: temporal_corruption is monotone in depth. +public export +temporalMonotone : (d1, d2 : Nat) -> LTE d1 d2 -> + TemporalActive d1 -> TemporalActive d2 +temporalMonotone _ _ le active = lteTrans active le + +-- ─────────────────────────────────────────────────────────────────────── +-- Scope leakage is NOT monotone (the retraction, made precise) +-- ─────────────────────────────────────────────────────────────────────── + +||| scope_leakage fires on prime line numbers. The obstruction to global +||| monotonicity, stated abstractly: for ANY predicate `p` with `p a = True` +||| and `p b = False` at `a <= b`, the detected set decreases as the metric +||| grows. Primality is such a `p` (witness a = 7, b = 8). Hence no global +||| monotonicity theorem exists -- and that is by design. +public export +scopeLeakObstruction : (p : Nat -> Bool) -> (a, b : Nat) -> LTE a b -> + p a = True -> p b = False -> + (p a = True, p b = False) +scopeLeakObstruction _ _ _ _ activeAtA inactiveAtB = (activeAtA, inactiveAtB) diff --git a/src/abi/Positional.idr b/src/abi/Positional.idr new file mode 100644 index 0000000..d175825 --- /dev/null +++ b/src/abi/Positional.idr @@ -0,0 +1,90 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Positional-operator determinism (error-lang formal core, property 2 of 3). +||| +||| Mirrors the Zig FFI `error_lang_positional_operator` +||| (`ffi/zig/src/main.zig`, lines 222-272): for `+` the behaviour is +||| `addition` when the column is even and `concatenation` when odd; for `*` +||| it is `multiplication` when the column is a multiple of 3 and +||| `exponentiation` otherwise. +||| +||| THEOREM. Operator behaviour is a deterministic (pure, total) function of +||| the operator and the column: `behavior op col = behavior op col`. +||| +||| This is `Refl` -- *because* the model is a pure total function. That is +||| exactly the point: the previous `Foreign.idr :: positionalDeterministic` +||| stated the same property over an `IO Bits8` FFI action and could only +||| "close" it with `cast Refl`, coercing `Refl : x = x` onto two distinct IO +||| results -- a non-proof. Modelling the operation as the pure function it +||| actually is makes determinism genuine. +||| +||| Self-contained; no escape hatches. Machine-check is a CI obligation. +||| +||| NOTE (conformance). `compiler/src/Stability.res` uses a *different* rule +||| (`(line*31+column) mod 4`, four-way). The Zig FFI and the ReScript path +||| therefore disagree; reconciling the two implementations is an open +||| obligation recorded in PROOF-NEEDS.md. +module Positional + +%default total + +||| Operators that carry positional behaviour. +public export +data Op = Plus | Star | OtherOp + +||| Resolved operator behaviours (mirrors Zig `OperatorBehavior`). +public export +data Behavior + = Addition + | Concatenation + | Multiplication + | Exponentiation + +||| Column parity (total, structural). +public export +isEven : Nat -> Bool +isEven Z = True +isEven (S Z) = False +isEven (S (S k)) = isEven k + +||| Divisibility by three (total, structural). +public export +multipleOfThree : Nat -> Bool +multipleOfThree Z = True +multipleOfThree (S Z) = False +multipleOfThree (S (S Z)) = False +multipleOfThree (S (S (S k))) = multipleOfThree k + +||| The positional behaviour function (pure model of the Zig FFI). +public export +behavior : Op -> Nat -> Behavior +behavior Plus col = if isEven col then Addition else Concatenation +behavior Star col = if multipleOfThree col then Multiplication else Exponentiation +behavior OtherOp _ = Addition + +||| THEOREM: behaviour is deterministic -- a genuine `Refl` over a pure +||| total function (contrast the original IO-based `cast Refl`). +public export +positionalDeterministic : (op : Op) -> (col : Nat) -> behavior op col = behavior op col +positionalDeterministic _ _ = Refl + +-- ─────────────────────────────────────────────────────────────────────── +-- Sanity evaluations (match the Zig integration tests + README example) +-- ─────────────────────────────────────────────────────────────────────── + +||| Column 12 (even): `+` is addition. (Zig test "positional semantics".) +exEvenAddition : behavior Plus 12 = Addition +exEvenAddition = Refl + +||| Column 13 (odd): `+` is concatenation. +exOddConcatenation : behavior Plus 13 = Concatenation +exOddConcatenation = Refl + +||| Column 9 (multiple of 3): `*` is multiplication. +exStarMultiplication : behavior Star 9 = Multiplication +exStarMultiplication = Refl + +||| Column 10 (not a multiple of 3): `*` is exponentiation. +exStarExponentiation : behavior Star 10 = Exponentiation +exStarExponentiation = Refl diff --git a/src/abi/Stability.idr b/src/abi/Stability.idr new file mode 100644 index 0000000..7ce3617 --- /dev/null +++ b/src/abi/Stability.idr @@ -0,0 +1,120 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| Stability-score bound (error-lang formal core, property 1 of 3). +||| +||| Mirrors the stability calculation in `compiler/src/Types.res` +||| (`stabilityImpact` / `calculateStability`, lines 258-274). +||| +||| THEOREM. The stability score is always within [0, 100]. +||| +||| The ReScript `calculateStability` computes `Int.max(0, 100 + penalties)` +||| where every penalty is non-positive — i.e. `max(0, 100 - totalPenalty)`. +||| We model the clamp with Nat truncated subtraction (`minus`), which is +||| exactly `max(0, .)`: `minus 100 p` is 0 once `p >= 100`. The upper bound +||| (`<= 100`) is then a property of truncated subtraction; the lower bound +||| (`>= 0`) is inhabited by the Nat type itself. +||| +||| This module is self-contained (only `Data.Nat`) and uses NO escape hatch +||| (`believe_me` / `assert_total` / `cast`-coerced equality / `postulate`). +||| It replaces the previous `Foreign.idr :: stabilityBounded`, which faked +||| the bound with `cast ()` over an `IO` action. +||| +||| Status: written to typecheck under Idris2 (>= 0.7.0). Machine-check is a +||| CI obligation (no idris2 in the current dev image). See PROOF-NEEDS.md. +module Stability + +import Data.Nat + +%default total + +-- ─────────────────────────────────────────────────────────────────────── +-- Self-contained Nat <= lemmas (no reliance on stdlib lemma names) +-- ─────────────────────────────────────────────────────────────────────── + +||| Reflexivity of <=. +lteRefl' : (n : Nat) -> LTE n n +lteRefl' Z = LTEZero +lteRefl' (S k) = LTESucc (lteRefl' k) + +||| Weakening on the right: m <= n => m <= S n. +lteSuccR : LTE m n -> LTE m (S n) +lteSuccR LTEZero = LTEZero +lteSuccR (LTESucc p) = LTESucc (lteSuccR p) + +||| Truncated subtraction never exceeds the minuend: (n - m) <= n. +subLTE : (n, m : Nat) -> LTE (minus n m) n +subLTE Z _ = LTEZero +subLTE (S k) Z = lteRefl' (S k) +subLTE (S k) (S j) = lteSuccR (subLTE k j) + +-- ─────────────────────────────────────────────────────────────────────── +-- Faithful model of compiler/src/Types.res stability factors +-- ─────────────────────────────────────────────────────────────────────── + +||| A consequence factor and its magnitude inputs (mirrors `stabilityFactor`). +public export +data Factor + = MutableState Nat Nat -- mutations, readers + | TypeInstability Nat -- reassignments + | NullPropagation Nat -- depth + | GlobalState Nat Nat -- mutations, dependencies + | UnhandledError Nat -- failure paths + | AlgorithmComplexity Nat -- amplified time units + | MemoryLeak Nat -- kilobytes + | RaceCondition Nat -- conflicts + +||| Penalty magnitude of a factor (mirrors `stabilityImpact`, expressed as a +||| non-negative cost that is subtracted from the base of 100). +public export +factorCost : Factor -> Nat +factorCost (MutableState m r) = 10 * m + 5 * r +factorCost (TypeInstability r) = 15 * r +factorCost (NullPropagation d) = 20 * d +factorCost (GlobalState m d) = 30 * m + 5 * d +factorCost (UnhandledError p) = 25 * p +factorCost (AlgorithmComplexity t) = t +factorCost (MemoryLeak kb) = 10 * kb +factorCost (RaceCondition c) = 40 * c + +||| Total penalty across all active factors. +public export +totalCost : List Factor -> Nat +totalCost [] = 0 +totalCost (f :: fs) = factorCost f + totalCost fs + +||| Stability score = base 100 minus total penalty, clamped at 0. +||| (Nat `minus` is truncated, modelling `Int.max(0, 100 + penalties)`.) +public export +stabilityScore : List Factor -> Nat +stabilityScore fs = minus 100 (totalCost fs) + +-- ─────────────────────────────────────────────────────────────────────── +-- THEOREM: 0 <= stabilityScore fs <= 100 +-- ─────────────────────────────────────────────────────────────────────── + +||| Upper bound: the score never exceeds 100. +public export +stabilityUpperBound : (fs : List Factor) -> LTE (stabilityScore fs) 100 +stabilityUpperBound fs = subLTE 100 (totalCost fs) + +||| Lower bound: the score is never negative (inhabited by the Nat type). +public export +stabilityLowerBound : (fs : List Factor) -> LTE 0 (stabilityScore fs) +stabilityLowerBound _ = LTEZero + +-- ─────────────────────────────────────────────────────────────────────── +-- Sanity evaluations (closed terms; reduce by computation) +-- ─────────────────────────────────────────────────────────────────────── + +||| No factors: full stability. +sanityFull : stabilityScore [] = 100 +sanityFull = Refl + +||| One mutation with two readers: 100 - (10*1 + 5*2) = 80. +sanityOneMutation : stabilityScore [MutableState 1 2] = 80 +sanityOneMutation = Refl + +||| Penalties exceeding 100 clamp to 0 (never negative): 40*3 = 120 -> 0. +sanityClamp : stabilityScore [RaceCondition 3] = 0 +sanityClamp = Refl diff --git a/src/abi/error-lang-abi.ipkg b/src/abi/error-lang-abi.ipkg new file mode 100644 index 0000000..97a8168 --- /dev/null +++ b/src/abi/error-lang-abi.ipkg @@ -0,0 +1,14 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +-- The error-lang formal core + ABI binding layer. +-- Build/typecheck: idris2 --typecheck error-lang-abi.ipkg (from src/abi) +-- or per-module: idris2 --check Stability.idr (from src/abi) +package error-lang-abi +version = 0.1.0 +authors = "Jonathan D.A. Jewell" +sourcedir = "." +modules = Stability + , Positional + , Paradox + , Foreign diff --git a/verification/check-affinescript.sh b/verification/check-affinescript.sh new file mode 100755 index 0000000..549602e --- /dev/null +++ b/verification/check-affinescript.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-affinescript.sh — typecheck every ported `.affine` compiler source with +# the AffineScript compiler. Companion to verification/check-proofs.sh. +# Requires `affinescript` on PATH (see scripts/install-affinescript-toolchain.sh). +set -euo pipefail + +# Check from compiler/src so sibling-module imports (`use Types::{...}`) resolve +# via the loader's current-dir search. +cd "$(dirname "$0")/../compiler/src" + +if ! command -v affinescript >/dev/null 2>&1; then + echo "affinescript not found — run scripts/install-affinescript-toolchain.sh" >&2 + exit 127 +fi + +shopt -s nullglob +sources=(*.affine) +if [ ${#sources[@]} -eq 0 ]; then + echo "no .affine sources yet (ReScript->AffineScript migration in progress)." + exit 0 +fi + +fail=0 +for f in "${sources[@]}"; do + printf 'checking %-28s ... ' "$f" + if affinescript check "$f" >/tmp/as_check.out 2>&1; then + echo ok + else + echo FAIL + cat /tmp/as_check.out + fail=1 + fi +done + +if [ "$fail" -eq 0 ]; then + echo "all .affine sources check." +else + echo "affinescript check failures." >&2 + exit 1 +fi diff --git a/verification/check-proofs.sh b/verification/check-proofs.sh new file mode 100755 index 0000000..ba97369 --- /dev/null +++ b/verification/check-proofs.sh @@ -0,0 +1,41 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# Machine-check the error-lang formal core (src/abi/*.idr) with Idris2. +# +# Requires idris2 >= 0.8.0 on PATH. Each module is self-contained (no local +# cross-imports), so they are checked independently from within src/abi (the +# bare module names match the file names). NO module uses an escape hatch +# (believe_me / assert_total / cast-coerced equality / postulate) -- the point +# of the core is that the proofs are genuine. +set -euo pipefail + +ABI_DIR="$(cd "$(dirname "$0")/../src/abi" && pwd)" + +if ! command -v idris2 >/dev/null 2>&1; then + echo "error: idris2 not found on PATH (need >= 0.8.0)." >&2 + echo "build it from source via Chez Scheme (see PROOF-NEEDS.md), then re-run." >&2 + exit 127 +fi + +echo "idris2: $(idris2 --version)" +cd "$ABI_DIR" +status=0 +for m in Stability Positional Paradox Foreign; do + printf 'checking %-12s ... ' "$m" + if idris2 --check "$m.idr" >/dev/null 2>&1; then + echo ok + else + echo FAIL + idris2 --check "$m.idr" || true + status=1 + fi +done + +if [ "$status" -eq 0 ]; then + echo "all proofs check." +else + echo "one or more proofs failed to check." >&2 +fi +exit "$status"