feat(tg-11): surface syntax for epistemic types + fix a second statement-order bug - #99
Conversation
…ent-order bug
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 <noreply@anthropic.com>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedAdds surface syntax for epistemic types and fixes a statement-order bug in the checker that caused cross-definition references to resolve placeholders. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
TG-11 (#98) landed the type former, typing, evaluation and six proofs — but there was no way to write one. Zero occurrences of the constructors in
lexer.mllorparser.mly, against 4 for echo. Fully implemented and unreachable.Surface syntax
The standpoint is bracketed because it's an index, not an operand — the same reading as a braid generator's subscript. No grammar conflicts.
Non-factivity reaches the syntax. There is deliberately no keyword extracting the claim:
claim(w)parses as an ordinary call to an undefined function, never as a language form. A test pins that distinction — if aClaimform ever appears, it contradictsepi_only_yields_evidence.A second copy of the statement-order bug
Writing the first epistemic program surfaced it immediately:
That
Word[0]is the pass-1a placeholder —tokwas being checked beforewwas refined. Same root cause as #95 (stmts := prog @ !stmtsthenList.revon the flattened list), but in a second copy, inlib/check.ml.That copy feeds
tanglec --checkand the LSP. Both have been analysing programs with their statements reversed.And it was never epistemic-specific:
Any cross-definition reference to a non-
Wordtype was mis-typed. Echo has been broken this way for as long as the recovering path has existed.The test suites missed both copies for the same reason: they call
Parser.programdirectly and never exercise the recovering path.Tests
Parser — warrant with bracketed standpoint; evidence; TG-4 round-trip; the no-claim-form guard.
Check — three cross-definition cases (plain, echo, epistemic), all of which would have failed before this.
Example
examples/epistemic.tangle, wired into the corpus gate's must-run set — warrants at three standpoints, evidence recovery, and the echo compositionresidue(evidence(we)). All assertions pass.It also documents why the claim is unreachable: if it were extractable, anything anyone attested would become true by fiat — precisely the bug you don't want in a provenance system.
All gates green: Lean 0 errors, full suite, corpus, RSR.
🤖 Generated with Claude Code