feat(tg-11): surface syntax for epistemic types + fix a second statement-order bug

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

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

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

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 }

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"]);

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

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]

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