From fed2eeec86d24f35a0dbb6c272c8344d427d87f4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 07:26:52 +0100 Subject: [PATCH] feat(tg-11): surface syntax for epistemic types + fix a second statement-order bug MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TG-11 landed the type former, typing, evaluation and six proofs — but there was no way to WRITE one. Zero occurrences of the constructors in lexer.mll or parser.mly, against 4 for echo. Fully implemented and unreachable. ## Surface syntax warrant[k](claim, evidence) -- at standpoint k evidence(w) -- the ONLY elimination The standpoint is bracketed because it is an index, not an operand — the same reading as a braid generator's subscript. Non-factivity reaches the syntax too: there is deliberately NO keyword that extracts the claim. `claim(w)` parses as an ordinary call to an undefined function, never as a language form, and a test pins that distinction — if a `Claim` form ever appears, it contradicts epi_only_yields_evidence. No grammar conflicts. ## A SECOND copy of the statement-order bug Writing the first epistemic program surfaced it. `def w = warrant[...]` then `def tok = evidence(w)` failed with In definition 'tok': evidence requires an Epi[k, rho, tau], got Word[0] The Word[0] is the pass-1a placeholder: `tok` was being checked BEFORE `w` had been refined. Same root cause as #95 — `stmts := prog @ !stmts` followed by `List.rev` on the flattened list — but in a SECOND copy, in lib/check.ml. That copy feeds `tanglec --check` AND the LSP, so both have been analysing programs with their statements reversed. It was not epistemic-specific: def e = echoClose(braid[s1]) def r = residue(e) -- "residue requires Echo[_, _], got Word[0]" Any cross-definition reference to a non-Word type was mis-typed. Echo has been broken this way for as long as the recovering path has existed. Fixed identically: accumulate segments, flatten in order. The test suites missed BOTH copies because they call Parser.program directly and never exercise the recovering path. ## Tests Parser: warrant with bracketed standpoint, evidence, TG-4 round-trip, and the no-claim-form guard. Check: three cross-definition cases — plain, echo, and epistemic — that would all have failed before. examples/epistemic.tangle added and wired into the corpus gate's must-run set: warrants at three standpoints, evidence recovery, and the echo composition (`residue(evidence(we))`). All assertions pass. Co-Authored-By: Claude Opus 5 --- compiler/bin/main.ml | 4 ++- compiler/lib/check.ml | 20 ++++++++++++--- compiler/lib/lexer.mll | 4 +++ compiler/lib/parser.mly | 12 +++++++++ compiler/test/test_check.ml | 18 +++++++++++++ compiler/test/test_parser.ml | 45 ++++++++++++++++++++++++++++++++ examples/epistemic.tangle | 50 ++++++++++++++++++++++++++++++++++++ scripts/check-corpus.sh | 1 + 8 files changed, 150 insertions(+), 4 deletions(-) create mode 100644 examples/epistemic.tangle diff --git a/compiler/bin/main.ml b/compiler/bin/main.ml index 81ce622..c34d520 100644 --- a/compiler/bin/main.ml +++ b/compiler/bin/main.ml @@ -187,7 +187,9 @@ let dump_tokens (filename : string) : unit = | FST -> print_string "FST" | SND -> print_string "SND" | ECHOADD -> print_string "ECHOADD" - | ECHOEQ -> print_string "ECHOEQ"); + | ECHOEQ -> print_string "ECHOEQ" + | WARRANT -> print_string "WARRANT" + | EVIDENCE -> print_string "EVIDENCE"); print_newline (); if tok <> EOF then loop () in diff --git a/compiler/lib/check.ml b/compiler/lib/check.ml index 35db67d..d38e767 100644 --- a/compiler/lib/check.ml +++ b/compiler/lib/check.ml @@ -35,12 +35,25 @@ let parse_with_recovery (source : string) : Ast.program * diag list = lexbuf.Lexing.lex_curr_p <- { lexbuf.Lexing.lex_curr_p with Lexing.pos_lnum = 1 }; let diags = ref [] in - let stmts = ref [] in + (* Accumulate SEGMENTS (each a statement list from one parser run), newest + first, and flatten in order at the end. + + This is the SECOND copy of this bug. bin/main.ml had the identical + `stmts := prog @ !stmts` followed by `List.rev` on the flattened list — + correct for an accumulator built by prepending single items (as `diags` + is) but wrong when whole segments are prepended, so every program came out + with its statements REVERSED. That copy was fixed in #95; this one feeds + `--check` AND the LSP, so both have been analysing reversed programs: + `def w = ...` / `def tok = f(w)` reported "In definition 'tok': ... got + Word[0]" because `tok` was checked before `w` was refined past its + placeholder. The test suites missed it — they call Parser.program + directly. *) + let segments = ref [] in let at_eof = ref false in while not !at_eof do (try let prog = Parser.program Lexer.token lexbuf in - stmts := prog @ !stmts; + segments := prog :: !segments; at_eof := true with | Lexer.Lexer_error msg -> @@ -56,7 +69,8 @@ let parse_with_recovery (source : string) : Ast.program * diag list = message = "Parse error: unexpected token" } :: !diags; at_eof := synchronize lexbuf) done; - (List.rev !stmts, List.rev !diags) + (* Flatten oldest-segment-first, preserving order WITHIN each segment. *) + (List.concat (List.rev !segments), List.rev !diags) (* The full diagnostic set for a source string: parse diagnostics followed by type-checker diagnostics. This is exactly the set of failures that would diff --git a/compiler/lib/lexer.mll b/compiler/lib/lexer.mll index 4064104..ac11be2 100644 --- a/compiler/lib/lexer.mll +++ b/compiler/lib/lexer.mll @@ -54,6 +54,10 @@ | "snd" -> SND | "echoAdd" -> ECHOADD | "echoEq" -> ECHOEQ + (* Epistemic forms (TG-11). `evidence` is the ONLY elimination — there is + deliberately no keyword that extracts the claim from a warrant. *) + | "warrant" -> WARRANT + | "evidence" -> EVIDENCE | "jones" -> JONES | "alexander" -> ALEXANDER | "homfly" -> HOMFLY diff --git a/compiler/lib/parser.mly b/compiler/lib/parser.mly index 1197d2c..66d2010 100644 --- a/compiler/lib/parser.mly +++ b/compiler/lib/parser.mly @@ -34,6 +34,7 @@ (* Echo / product forms — surface syntax mirrors pretty.ml output *) %token ECHOCLOSE LOWER RESIDUE PAIR FST SND ECHOADD ECHOEQ +%token WARRANT EVIDENCE (* Invariant names *) %token JONES ALEXANDER HOMFLY KAUFFMAN WRITHE LINKING @@ -290,6 +291,17 @@ unary_expr: { EchoAdd (e1, e2) } | ECHOEQ LPAREN e1 = expr COMMA e2 = expr RPAREN { EchoEq (e1, e2) } + (* ---- Epistemic (TG-11) ---- + `warrant[k](claim, evidence)` — at standpoint k, evidence purporting to + support claim. The standpoint is bracketed like a braid index because it + is an index, not an operand. + `evidence(e)` is the sole elimination: it yields the TOKEN. There is no + surface form that extracts the claim, because there is no such rule — + see epi_only_yields_evidence in proofs/Tangle.lean. *) + | WARRANT LBRACKET k = INT RBRACKET LPAREN c = expr COMMA ev = expr RPAREN + { Warrant (k, c, ev) } + | EVIDENCE LPAREN e = expr RPAREN + { Evidence e } | t = twist_expr { t } | MINUS e = primary_expr { UnaryOp (Neg, e) } | e = primary_expr { e } diff --git a/compiler/test/test_check.ml b/compiler/test/test_check.ml index 83a929c..52e2894 100644 --- a/compiler/test/test_check.ml +++ b/compiler/test/test_check.ml @@ -72,6 +72,24 @@ let () = test "a single type error yields exactly one diagnostic (no duplicate)" (fun () -> let ds = check_source "def bad = braid[s1] + 3\n" in List.length (List.filter (fun d -> d.level = Error) ds) = 1); + (* Statement ORDER through the recovering parser. This path (check.ml) is + what --check and the LSP use, and it reversed every program: the copy in + bin/main.ml was fixed in #95, this one was not. A definition referring to + an earlier definition was therefore checked BEFORE that definition was + refined past its Word[0] placeholder. *) + test "cross-definition reference typechecks (statement order)" (fun () -> + not (has_error (check_source + "def a = braid[s1]\ndef b = a . a\n"))); + + test "echo cross-reference typechecks" (fun () -> + (* Was broken: "residue requires Echo[_, _], got Word[0]". *) + not (has_error (check_source + "def e = echoClose(braid[s1])\ndef r = residue(e)\n"))); + + test "epistemic cross-reference typechecks" (fun () -> + not (has_error (check_source + "def w = warrant[0](42, braid[s1])\ndef tok = evidence(w)\n"))); + test "format_diag is tab-separated with 4 fields" (fun () -> let line = format_diag { level = Error; line = 3; col = 5; message = "boom" } in String.split_on_char '\t' line = ["ERROR"; "3"; "5"; "boom"]); diff --git a/compiler/test/test_parser.ml b/compiler/test/test_parser.ml index 117bdc1..dd4d4ba 100644 --- a/compiler/test/test_parser.ml +++ b/compiler/test/test_parser.ml @@ -210,6 +210,51 @@ let test_weave_blocks () = let p2 = parse_ok printed in assert_eq "pretty then re-parse yields the same AST" p1 p2); + (* TG-11 surface syntax: warrant[k](claim, evidence) and evidence(e). *) + test "TG-11 warrant parses with a bracketed standpoint" (fun () -> + let prog = parse_ok "def w = warrant[3](42, braid[s1])" in + match prog with + | [Definition d] -> + (match d.def_body with + | Warrant (3, IntLit 42, BraidLit _) -> () + | _ -> failwith "expected Warrant with standpoint 3") + | _ -> failwith "expected a single Definition"); + + test "TG-11 evidence parses" (fun () -> + let prog = parse_ok "def t = evidence(w)" in + match prog with + | [Definition d] -> + (match d.def_body with + | Evidence (Var "w") -> () + | _ -> failwith "expected Evidence") + | _ -> failwith "expected a single Definition"); + + test "TG-11 there is NO surface form extracting the claim" (fun () -> + (* Non-factivity reaches the syntax. `evidence` is a KEYWORD and becomes + the Evidence form; `claim` is not a keyword, so `claim(w)` is just an + ordinary call to an undefined function — it can never be an elimination + the proofs forbid. If a `Claim` form ever appears here, someone has + added a rule that contradicts epi_only_yields_evidence. *) + (match parse "def c = claim(w)" with + | Some [Definition d] -> + (match d.def_body with + | Call ("claim", _) -> () (* plain call — correct *) + | _ -> failwith "claim(w) must parse as an ordinary Call, not a form") + | _ -> failwith "expected claim(w) to parse as a call"); + (* Whereas `evidence` IS a form: *) + match parse "def c = evidence(w)" with + | Some [Definition d] -> + (match d.def_body with + | Evidence _ -> () + | _ -> failwith "evidence(w) must parse as the Evidence form") + | _ -> failwith "expected evidence(w) to parse"); + + test "TG-11 warrant round-trips (TG-4 property)" (fun () -> + let src = "def w = warrant[0](42, braid[s1])" in + let p1 = parse_ok src in + let p2 = parse_ok (Tangle.Pretty.program_to_string p1) in + assert_eq "pretty then re-parse" p1 p2); + test "#88 weave is still valid as a statement" (fun () -> (* Regression guard: the change is additive. *) let prog = parse_ok diff --git a/examples/epistemic.tangle b/examples/epistemic.tangle new file mode 100644 index 0000000..2a3d773 --- /dev/null +++ b/examples/epistemic.tangle @@ -0,0 +1,50 @@ +# SPDX-License-Identifier: MPL-2.0 +# epistemic.tangle — warranted claims (TG-11) +# +# A warrant is EVIDENCE FOR a claim, not the claim itself. Holding one does +# not give you the thing warranted. That is the difference between knowing +# something and having a reason to believe it. +# +# Demonstrates: +# - warrant[k](claim, evidence) — at standpoint k +# - evidence(w) — the ONLY elimination +# - non-factivity: nothing extracts the claim + +# --- A warrant at standpoint 0 --- + +# "At standpoint 0, this braid is my evidence for the claim 42." +def w = warrant[0](42, braid[s1, s2]) + +# The evidence can be recovered. +def token = evidence(w) +assert token == braid[s1, s2] + +# --- The claim is NOT recoverable --- +# +# There is no `claim(w)`. It is not a language form, and no typing rule +# produces the claim's type from a warrant. See epi_only_yields_evidence +# and epi_claim_is_opaque in proofs/Tangle.lean. +# +# If it were extractable, anything anyone attested would become true by +# fiat — which is exactly the bug you do not want in a provenance system. + +# --- Standpoints are distinct positions --- +# +# The same evidence for the same claim, held at different standpoints, is a +# different warrant. Who holds it is part of what it is. + +def w1 = warrant[1](42, braid[s1, s2]) +def w2 = warrant[2](42, braid[s1, s2]) + +# Both still yield their evidence. +assert evidence(w1) == braid[s1, s2] +assert evidence(w2) == braid[s1, s2] + +# --- Epistemic composes over echo --- +# +# A warrant whose evidence is an echo: standpoint 1 has access to an echo of +# a braid. The two modalities nest — echo grades irrecoverability, epi +# indexes standpoints. Neither absorbs the other. + +def we = warrant[1](0, echoClose(braid[s1])) +assert residue(evidence(we)) == braid[s1] diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 4556d91..9e71d40 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -44,6 +44,7 @@ fi # Examples that must fully TYPECHECK and EVALUATE (all their asserts hold). EXAMPLES_MUST_RUN=( braids_as_data.tangle + epistemic.tangle # TG-11 — warranted claims, non-factive compositional_pd.tangle echo_pd.tangle isotopy.tangle # the TG-7 witness — see header