diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d34ce627..22a3e899 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,64 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Added — `echidna lexicon scan`, 2026-10-27 + +* *`+echidna lexicon scan+`* (`+src/rust/lexicon/scan.rs+`, + `+just lexicon-scan+`) — compares `+training_data/+` corpora by theorem + name and by canonical statement shape, and writes cognates, false-friend + and specialisation candidates, and synonym candidates (joined by + identical text, shape or skeleton) as JCS JSON Lines with UUIDv8 pair + ids. Flag-only: every record carries `+evidence = none+`, and + `+data/synonyms/+` is never written. Presets `+learning+`, + `+spanning+` (one corpus per prover family), `+in-family+` and `+full+`. + Per-corpus coverage and key-collision samples are written alongside. + Whitespace runs collapse to one space, or to a newline when they hold + one, so a line comment cannot swallow the rest of a statement. A re-run + removes only the file names the scan writes. + The per-name cap (`+--max-pairs-per-name+`) bounds folded-name pairs + across a whole folded group, not per raw-name pair. Corpus keys may not + start or end with `+_+`, so pair file names stay unambiguous; a hyphen is + allowed, so the shipped `+2026-03-20+` corpus can be scanned. + Anonymous names (`+_+`) are indexed like any other, so + `+--keep-generic+` now joins them. A bare signature over any type names + (`+Tree -> Tree -> Tree+`) no longer proposes a synonym. With the global + `+--format json+`, the scan prints one JCS summary object on stdout. + +==== Fixed — canonicaliser, 2026-10-27 + +* *`+corpus::canonical+` no longer panics* on a statement whose last + token is an unbalanced opening bracket (eight `+open + 1..close+` slices + are now guarded). `+structural_key+` reaches this from `+corpus ingest+` + and the octad identity keys. No key changes. +* *String literals are opaque atoms.* A quoted span is lexed as a formula + only where it wraps one: at the start of a statement, after `+:+`, or + after an Isabelle statement keyword. Elsewhere (`+s = "a//b"+`, ACL2 + `+"Goal"+` hints, Why3 `+meta "…"+`) it is one constant, so its contents + are no longer read as comments, operators or variables, and a backslash + escapes the next character. A quote opens a formula only when its close + also ends the statement (or meets another quote or an Isabelle keyword), + and a quote right after an unwrapped formula is the next proposition, + so `+"a" == "z"+` keeps its leading literal. *Key change*: statements with such a literal + get new keys; distinct literals no longer share one. On + `+training_data/+` this splits a dozen Mizar and seven Why3 key + collisions; coverage moves by at most 0.1 point per corpus. +* *`+StructuralKey::complete+`* (new, `+#[serde(default)]+`) reports + whether the shape accounts for the whole statement: false when the + parser stops early, invents a missing operand, gives a binary-only + prefix operator one operand (`+(= (+ x 1))+`), or the input ends inside + an open bracket, a quoted statement or a block comment; when a closer + meets a group of another kind; when the statement meets + notation `+dk-shape-v1+` has no rule for (HOL binders, `+~+`, `+==>+`, + Isabelle `+\<…>+` escapes), drops a statement's own leading tokens as a + "header", misreads a leading group as a telescope, or cuts off a tree + deeper than 256 levels, counting bracket groups and infix operators + (the parser is now bounded, so neither deep nesting nor a long flat + chain such as `+a -> a -> …+` can overflow a caller's stack). + `+corpus identity+` skips incomplete declarations and says how many. No key changes. + Measured on `+training_data/+`, 0.4 %–94 % of a corpus is read + completely; the rule-level causes are recorded for a `+dk-shape-v2+` + decision in `+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+`. + ==== Added — structural cross-prover identity keys, 2026-10-22 * *`+src/rust/corpus/canonical.rs+`* — normalises a declaration's *type* diff --git a/Justfile b/Justfile index a9b57888..6b82224c 100644 --- a/Justfile +++ b/Justfile @@ -1163,6 +1163,14 @@ lexicon-check: scripts/lexicon-check.sh cargo test --locked --test lexicon_v2_test +# Mine lexicon candidates across training_data/ corpora: cognates, false +# friends and synonym candidates as JCS JSON Lines under target/lexicon-scan. +# Flag-only (evidence = none); never edits data/synonyms/. Presets: learning, +# spanning, in-family, full. +lexicon-scan preset="learning": + cargo run --locked --bin echidna -- lexicon scan --preset {{preset}} + cargo test --locked --test lexicon_scan_test + # Run the saturation-campaign cargo tests only (139 cases + 1 ignored). test-saturation: cargo test --lib -- \ diff --git a/data/synonyms/README.adoc b/data/synonyms/README.adoc index 54e32a44..0a9af866 100644 --- a/data/synonyms/README.adoc +++ b/data/synonyms/README.adoc @@ -219,6 +219,42 @@ Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or Corpus-mined candidates (owner decision D4) are flag-only: they carry `evidence = { kind = "none" }` and never set `semantic_class` on their own. +=== Mining candidates: `echidna lexicon scan` + +`echidna lexicon scan --preset learning` (or `just lexicon-scan`) compares +`training_data/proof_states_.jsonl` corpora on two axes, the theorem +*name* and the canonical *shape* of its statement (`dk-shape-v1`, +`src/rust/corpus/canonical.rs`), and writes review candidates as JCS JSON +Lines under `target/lexicon-scan/`. It never edits this directory. + +[cols="1,2,2"] +|=== +| | same shape | different shape + +| *same name* +| cognate (`cognate_exact`, `cognate_shape`) +| false friend or specialisation (`cognate_skeleton`, `differs`) + +| *different name* +| synonym candidate (joins `text`, `shape`, `skeleton`) +| unrelated, not reported +|=== + +A pair is `unparsed` when either statement was not read completely by the +canonicaliser (`StructuralKey::complete`): its key is then a prefix that +other statements share, so it says nothing. Joins between different names +also skip shapes too thin to identify anything (`informative`: a variable in +function position, fewer than three constants, or a bare type signature). +Every skip is counted in `summary.jsonl`; `coverage.jsonl` reports, per +corpus, how much the canonicaliser read and how often distinct statements +share a key. Each candidate's `id` is the UUIDv8 content id of the +statement pair, independent of scan direction and normaliser version, so a +review decision survives a re-scan. + +A candidate becomes a row here only by curation: a person writes the row +with `evidence = curated` (or `probe` / `kernel` once that evidence exists), +and the Nickel contract checks it like any other. + Nickel checks shape and the cross-field rules; serde checks that `checked_by` names a `ProverKind` and `format` an `ExchangeFormat` when Rust loads a table (`tests/lexicon_v2_test.rs`). @@ -242,8 +278,9 @@ prover no longer accepts (or never accepted in this version). - Cross-prover synonym graph (Isabelle `le_trans` ↔ Coq `Rle_trans` ↔ Lean `le_trans`) is intentionally **out of scope** here — that's `echidna port`, not `echidna suggest`. -- ML-driven synonym discovery from the corpus (mining - `training_data/`) is in §4.4 of the notes, not this layer. +- ML-driven synonym discovery from the corpus is in §4.4 of the notes, + not this layer. Syntactic mining of `training_data/` is + `echidna lexicon scan` (above); it proposes, it never writes here. == Maintenance diff --git a/docs/CORPUS.adoc b/docs/CORPUS.adoc index 13d44e02..3a2e3e42 100644 --- a/docs/CORPUS.adoc +++ b/docs/CORPUS.adoc @@ -242,6 +242,22 @@ Isabelle writes the same fact without binders and Why3 states it over therefore *tiered*: exact structural key first, skeleton key second. Any consumer that only compares one field should compare both. +A key is only as good as the parse behind it. `+StructuralKey::complete+` +says whether the canonicaliser read the *whole* statement; when it did not +(its parser stopped early, invented an operand or found a relation with one +operand, the input ended inside an +open bracket, quote or comment, a closer met a group of another kind, it +met notation it has no rule for — HOL's `+!+` and `+?+` binders, Isabelle's +`+\<…>+` escapes — or a header drop discarded the statement's own leading +tokens), the key is still reported at the +structural tier but is a *prefix* that other statements share. Treat an +incomplete key as no identity at all: `+corpus identity+` skips such +declarations and reports how many it skipped. Measured on `+training_data/+`, the +share of statements read completely ranges from under 1% (Isabelle/ZF) to +over 90% (λProlog); see +`+docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc+` +(PR 3 results) and `+echidna lexicon scan+`. + The CLI surfaces it directly: [source,bash] diff --git a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc index 30b4c41b..53c6b964 100644 --- a/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc +++ b/docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc @@ -2,7 +2,7 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = ADR: lexicon v2 (false friends, phrases, equivalences) and hub-and-probe identity arbitration (stage 6c) :revdate: 2026-10-19 -:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3 and D5 open +:status: accepted in part — D1, D2 and D4 ruled 2026-10-19, D8 ruled 2026-10-27 (§7); D3, D5, D6 and D7 open == Context (measured on `main` at `ed6ef60`, 2026-10-19) @@ -294,11 +294,206 @@ re-running `metrics/run_all.jl` to re-baseline `oov_rate` and verdict's `level` should surface in its trust bridge once dispatch attaches evidence. +== PR 3 results: `echidna lexicon scan` (2026-10-27) + +=== What landed + +`echidna lexicon scan` (`src/rust/lexicon/scan.rs`, `just lexicon-scan`) +compares `training_data/proof_states_.jsonl` corpora on two axes: +the theorem *name*, and the canonical *shape* of its statement. Same name +and same shape is a cognate; same name and a different shape is a false +friend or a specialisation; a different name and the same shape (or +identical text, or the same skeleton) is a synonym candidate. Output is +I-JSON serialised as JCS, one record per line, with a UUIDv8 content id per +statement pair that does not depend on scan direction or normaliser +version, so a review decision survives a re-scan. Every candidate carries +`evidence = { kind = "none" }` and nothing is written to `data/synonyms/` +(D4). The pair sets follow the 2026-10-20 ruling: a learning pass +(HOL4 ↔ HOL Light, Lean 3 ↔ AFP), then one corpus per family +(HOL4, AFP, Lean 3, Mizar, ACL2, Why3, λProlog, Dedukti: 28 pairs) plus one +pair inside each family (5 more). + +=== A departure, labelled + +The 2026-10-20 ruling was a lexical normaliser in this PR and parsed +normalisation in PR 6. Before this PR was written, #449 landed +`src/rust/corpus/canonical.rs` (`dk-shape-v1`), a canonicaliser that +already does the lexical part and more. Building a second one beside it +would have been a parallel normaliser; the scan uses `dk-shape-v1` instead +and measures it. That is the departure, and the measurement is why it paid. + +=== What the measurement found in `dk-shape-v1` + +The scan's first run panicked inside `canonical.rs`: an unbalanced opening +bracket as the last token made eight `open + 1..close` slices panic. That +path is also `corpus ingest`'s. Fixed here with no key change (reproduced +first; the regression test panics on the old code). + +The second finding is larger. When the canonicaliser cannot read a +statement it rarely falls back to its text tier; it returns a +*structural-tier* key for the prefix it did read, and different statements +share that prefix. `StructuralKey::complete` now says whether the whole +statement was read. It is false when the parser stops early, invents a +missing operand (`x + 1 =`), finds a binary-only prefix operator with one +operand (`(= (+ x 1))`), or reaches the end inside an open bracket or +an unclosed `(assert …` wrapper (ACL2s goals truncated mid-expression), +when a closer meets a group of another kind (`(x]`) or a quoted statement +or block comment never closes, +when the statement holds notation the scheme has no rule for (`!`, `?`, +`@` and `\` binders, `~`, `==>`, Isabelle's `\<…>` escapes, Lean 3's `$`; +checked before binders and ascriptions are removed), when a header drop +discarded the statement's own tokens, or when a leading bracket group was +misread as a binder telescope. It changes no key. The scan treats an +incomplete key as no identity: such pairs are `unparsed`, and such +statements take no part in shape joins. + +Share of each corpus read completely (`dk-shape-v1`, 2026-10-27): + +[cols="2,2,2,2,2",options="header"] +|=== +| Corpus | Distinct rows | Read completely | Keys shared by distinct statements | Homonymous names +| acl2 | 135963 | 15.9 % | 779 | 8.0 % +| acl2s | 112742 | 4.8 % | 330 | 4.8 % +| afp | 102717 | 10.6 % | 525 | 2.1 % +| agda | 46028 | 40.8 % | 574 | 8.6 % +| dafny | 10487 | 53.8 % | 153 | 12.2 % +| dedukti | 1453 | 75.4 % | 54 | 20.6 % +| hol4 | 95738 | 8.7 % | 104 | 4.2 % +| hol_light | 43937 | 1.9 % | 15 | 2.9 % +| isabelle_zf | 3577 | 0.4 % | 0 | 0.3 % +| lambda_prolog | 24897 | 93.5 % | 118 | 50.0 % +| lean3 | 92695 | 25.8 % | 2655 | 19.2 % +| mizar | 76522 | 19.2 % | 434 | 1.8 % +| why3 | 25180 | 27.2 % | 346 | 21.9 % +|=== + +"Keys shared by distinct statements" counts complete keys only. Most are +benign (Lean 3 goal fields sometimes repeat the statement with its proof +attached, which the canonicaliser cuts); the rest are the rule-level +causes below. + +Four rule-level causes of false identity cannot be fixed without changing +keys, so they are recorded here for a `dk-shape-v2` decision (D6) rather +than changed under `dk-shape-v1`: + +. *Header drop.* `drop_declared_head` is documented to skip a group that + *starts* the statement, but returns at the first top-level bracket + anywhere. A statement with no `name :` header loses everything before + its first bracket: `exp(0) = 1` and `cos(0) = 1` both key as + `(EQ 0 1)`; `closed (closure M)` keys as `(closure v0)`. +. *Keyword drop.* Declaration keywords match case-insensitively at the + start of any statement: HOL4's `FACT 1 = 1` keys as `1 = 1`. +. *Short names as variables.* Any lower-case name of three characters or + fewer is numbered as a variable, so `cos`, `exp`, `nhd`, `phi` vanish: + `nhd 0 = 0` and `phi 0 = 0` share a key. +. *Unread notation and binders.* No HOL (`!`, `?`, `\`, `==>`, `~`) or + Isabelle `\<…>` notation. No ∃: `exists x : nat, x = 0` and + `exists x : nat, x = 1` both key as `NAT`. A parenthesised quantified + antecedent at the start is read as a binder telescope: + `(forall x : nat, P x) -> Q` keys as `(PI [NAT NAT] v0)`, with `forall` + taken as a bound name. A Lean hypothesis binder `(h : 2 * n ≤ n)` is + reduced to a sort, so `(h : 2 * n ≤ n) : n = 0` and + `(h : n ≤ n / 2) : n = 0` share a key. Binder keywords elsewhere are + lifted into the leading Π (`extract_binders` step 3), which is sound only + in positive positions; the probes found no pair merged by that alone. + +`complete` now flags the header drop, the keyword drop, unread notation, +∃ (the parser stops), truncation inside a group and the telescope +misread. It does not flag the +short-name rule or the hypothesis-as-sort rule, which produce well-formed +but wrong shapes; the scan's `informative` filter catches the short-name +rule's commonest form (a variable in function position). The corpus +identity keys (E6 `cross_prover_identity_key`) inherit all four causes. + +=== What the measurement found in the corpora + +Over all 33 pairs: 167,040 same-name statement pairs, of which 1,070 are +exact cognates, 2,631 shape cognates, 64 skeleton (specialisation) +candidates, 5,469 differ, and 157,806 (94 %) are `unparsed`. A further +90,191 statement pairs under 308 over-large names are counted, not +emitted: the per-name cap (64) bounds exact pairs per raw name and folded +pairs per folded name. Synonym candidates under different names: 315 by +identical text, 433 by shape, 819 by skeleton. Debug build: 175 s for all +thirteen corpora, almost all of it loading and canonicalising; one pair scans in about a second. + +* *HOL4 ↔ HOL Light* (pilot pair): 1,033 exact cognates and 144 text + synonyms (`FACT_0` / `pth_0`), but 5,555 same-name pairs `unparsed`: + `dk-shape-v1` reads 1.9 % of HOL Light. The pilot pair needs HOL + notation in the canonicaliser before shape evidence means anything. +* *Lean 3 ↔ AFP, AFP ↔ Mizar, Lean 3 ↔ Mizar*: the synonym joins find real + cross-family correspondences: `sqrt_zero ~ lemSqrt0`, + `dist_comm ~ dist_sym`, `add_comm ~ plus_commute`, + `cantor ~ x_lt_2_x` (`a < 2^a` over cardinals and naturals), + `lt_add_one_iff ~ Th13`, and Mizar's article-local labels (`Th29`) + matched by content to named AFP and Lean lemmas. +* *ACL2 and ACL2s are dirty at the source*: ACL2s goals are truncated + mid-expression or are comments (`;; (implies …`), and ACL2 goals carry + `:hints` text and terminal escape codes. 95,651 shared names yield 31 + exact cognates. The extractors need fixing (D7). +* *Thin shapes are not synonyms*: a variable in function position (the + short-name rule above), fewer than three constants, or a bare type + signature (λProlog's `int -> int -> int` against Dedukti's + `Int -> Int -> Int`) say nothing about which statement it is. Joins + between different names skip them (3,253 groups, counted). + +=== Equivalence by invariant and by witness + +Knot theory decides the same question echidna faces. Two knots are equal +when one deforms into the other; in practice that is settled two ways. An +*invariant* (the Jones polynomial, quandle colourings) is cheap and can +prove two knots *different*, but agreement proves sameness only if the +invariant is complete. A *witness* (a sequence of Reidemeister moves) is +expensive and proves sameness, step by checkable step. The knot quandle is +complete up to an orientation symmetry (Joyce; Matveev, 1982), which is +why QuandleDB (`nextgen-databases/quandledb`) is built on it. + +Echidna's evidence ladder has the same two halves. Canonical keys and +consequence probes are invariants: agreement is a candidate (`belief`) or +`epi`, never `sound`. A kernel-checked translation is the witness: `sound`. +Three consequences follow. + +. *Difference is cheaper than sameness, but only from a semantic + invariant.* One verified consequence that holds of one statement and + fails of the other, read in one shared standpoint, is a sound + certificate of *distinctness*: a false friend can be proved, not just + suspected. PR 4's probe loop should report `distinct` as a first-class + outcome. A *syntactic* key that differs proves nothing: this PR shows + normalisation gaps separate equal statements and merge different ones. +. *A complete invariant is as good as a witness.* PR 6's injectivity + property test (distinct terms in the fragment never share a `term_hash`) + is exactly a completeness proof for the λΠ projection on its fragment. + `dk-shape-v1` is far from complete, and the table above says how far. +. *The residue of a lossy correspondence* (`fidelity = lossy`) is what the + invariant cannot see; echo-types' loss-with-residue formalism is the + vocabulary for it, as §3 already cites. + +=== Formats: why the scan emits JCS and not TOML + +TOML has no canonical form: the same data has many valid spellings +(inline or standard tables, dotted keys, four string styles, several float +and date forms), and no specification fixes one. So TOML cannot be hashed +or diffed stably, and it carries types I-JSON lacks (datetimes, 64-bit +integers beyond I-JSON's safe range). Machine output is therefore JCS. The +curated tables stay TOML for people (D2); if a table needs a content id, +the id of record is the JCS of its *parsed* data, which gives TOML a +canonical identity without changing how it is written. + +=== Ordering + +Phrase detection (an extractor that finds multi-token idioms at proof +sites, so the canonical spelling of a `phrase` row can be replaced as well +as its aliases) comes after this PR, by the 2026-10-20 ruling. + == Owner decisions Ruled 2026-10-19 through the selector: D1, D2 and D4. D3 and D5 remain open. The owner also ruled the pacing: PRs 1 and 3 proceed now; PRs 4–6 (arbiter -and ABI changes, kernel translation) wait for the stronger model. +and ABI changes, kernel translation) wait for the stronger model. Ruled +2026-10-20: the PR 3 normaliser is lexical with parsed normalisation in +PR 6 (superseded in practice by #449's canonicaliser, see PR 3 results), +the scan covers one corpus per family plus one in-family pair each, its +records carry UUIDv8 ids, the invariant/witness reading goes in this ADR, +and phrase detection follows PR 3. D6 and D7 opened, and D8 ruled, 2026-10-27. [cols="1,5,3,3",options="header"] |=== @@ -308,6 +503,9 @@ and ABI changes, kernel translation) wait for the stronger model. | D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now | open | D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested | as recommended | D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes | open +| D6 | Fix `dk-shape-v1`'s four rule-level false-identity causes (header drop, keyword drop, short names as variables, unread notation and binders) as `dk-shape-v2`, bumping `SCHEME` and so every corpus identity key? | Yes, as its own PR, starting with the header and keyword drops (smallest, largest effect), with the scan as the before/after measure | open +| D7 | Fix the `training_data/` extractors for ACL2 (hints, escape codes) and ACL2s (truncation, comment lines), and strip proof bodies from Lean 3 goals? | Yes, at the extractors, then re-scan | open +| D8 | The VeriSim bridge and the octad export write `cross_prover_identity_key` for every declaration, incomplete keys included, and consumers join on equality (CodeRabbit on #453; predates this stack, from #449). Make the keys `Option`, or add a flag? | Additive `identity_complete: bool` on `DeclGraph` and `GraphPayload`, own PR | As recommended, 2026-10-27: additive flag, serde default and an added capnp field, key fields unchanged, consumers filter on it; own PR after #453, ER schema doc updated. The `Option` shape waits for D6. |=== == Non-claims diff --git a/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc index 1fdc31b5..8475faac 100644 --- a/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc +++ b/docs/decisions/2026-10-22-structural-cross-prover-identity.adoc @@ -146,6 +146,13 @@ legacy name-tail hashes differ. estate's corpora; it is not a grammar for any prover. Statements it cannot parse fall back to a whitespace-normalised text key at tier 3 (`+KeyTier::Text+`), which is honest but weak — worth measuring. + *Measured 2026-10-27* (`+echidna lexicon scan+` over thirteen + `+training_data/+` corpora): statements it cannot *fully* read mostly do + not fall back to tier 3; they get a structural-tier key for the prefix it + did read, which distinct statements share. `+StructuralKey::complete+` + now reports that, without changing any key, and four rule-level causes + of false identity are recorded for a `+dk-shape-v2+` decision in + `+2026-10-19-lexicon-v2-and-identity-arbitration.adoc+` (PR 3 results). * Sorts are compared by name. `+Nat+` in Lean and `+nat+` in Coq agree because both are aliased to `+NAT+`; type classes and universe levels are not modelled. diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index d3558b5d..996f751e 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -128,6 +128,22 @@ pub struct StructuralKey { pub skeleton_key: String, /// Which tier this declaration's shape is trustworthy at. pub tier: KeyTier, + /// Whether the shape accounts for the whole statement. False when the + /// parser stopped early (anything but a trailing `.`/`,`/`;` or an + /// unmatched closing bracket left over), invented a missing operand, or + /// gave a binary-only prefix operator one operand (`(= (+ x 1))`), + /// when the input ended inside an open bracket, quote or block comment + /// (a statement truncated mid-group), when a closer met a group of + /// another kind, when the body holds notation this scheme has no rule + /// for (`!`, `?`, `@`, `\`, `$`, `~`, `==>`), when the header + /// drop discarded tokens that were not a declared head, or when a leading + /// bracket group was misread as a binder telescope. In each case the + /// shape is still reported at the structural tier but stands for part of + /// the statement, and different statements can share it. Always `false` + /// at the text tier. Not part of `key`: it qualifies the key, so adding + /// it changed no key. + #[serde(default)] + pub complete: bool, } // =========================================================================== @@ -166,6 +182,15 @@ fn op_of(name: &str) -> Option<&'static str> { Some(op) } +/// Operators that always take two operands. Unary minus, `not`, and the +/// one-argument `(+ x)` / `(and x)` that ACL2 accepts are not listed. +fn is_binary_only(op: &str) -> bool { + matches!( + op, + "EQ" | "NEQ" | "LT" | "LE" | "GT" | "GE" | "IN" | "ARROW" | "IFF" | "DIV" | "MOD" + ) +} + /// Infix precedence. `ARROW`/`IFF` are right-associative, the rest are /// left-associative (see [`Parser::expr`]). fn precedence(op: &str) -> Option { @@ -290,6 +315,16 @@ fn is_ident_char(c: char) -> bool { } fn lex(src: &str) -> Vec { + lex_flagged(src).0 +} + +/// Lex `src`; the flag is false when a quoted statement or block comment +/// runs off the end of the input (part of the statement was swallowed). +fn lex_flagged(src: &str) -> (Vec, bool) { + let mut terminated = true; + // `out.len()` just after an unwrapped formula: a quote right there is + // the next proposition (`assumes "P x" "Q x"`), not a string literal. + let mut after_wrapper: Option = None; let chars: Vec = src.chars().collect(); let n = chars.len(); let mut out: Vec = Vec::new(); @@ -315,17 +350,37 @@ fn lex(src: &str) -> Vec { while i + 1 < n && !(chars[i] == '*' && chars[i + 1] == ')') { i += 1; } + if i + 1 >= n { + terminated = false; + } i = (i + 2).min(n); continue; } - // quoted statement (Isabelle quotes the whole formula) + // A quoted span is either a formula wrapper (Isabelle quotes the whole + // formula: `"x = y"`, `lemma foo: "…"`, `assumes "…" shows "…"`), + // whose contents are lexed as the statement, or a string literal + // (`s = "a//b"`, ACL2's `"Goal"` hints), which is one opaque atom so + // its contents are never read as comments, operators or variables. if c == '"' { let mut j = i + 1; while j < n && chars[j] != '"' { - j += 1; + // a backslash escapes the next character (`\"` in a literal, + // `\` in an Isabelle formula) + j += if chars[j] == '\\' { 2 } else { 1 }; } let inner: String = chars[i + 1..j.min(n)].iter().collect(); - out.extend(lex(&inner)); + if j >= n { + terminated = false; + } + let wrapper_position = opens_formula(out.last()) || after_wrapper == Some(out.len()); + if wrapper_position && closes_formula(&chars[(j + 1).min(n)..]) { + let (inner_toks, inner_ok) = lex_flagged(&inner); + terminated &= inner_ok; + out.extend(inner_toks); + after_wrapper = Some(out.len()); + } else { + out.push(Tk::Name(format!("\"{inner}\""))); + } i = j + 1; continue; } @@ -379,7 +434,84 @@ fn lex(src: &str) -> Vec { out.push(Tk::Sym(c.to_string())); i += 1; } - out + (out, terminated) +} + +/// Isabelle words that open or continue a quoted statement. +const FORMULA_KEYWORDS: [&str; 9] = [ + "lemma", + "theorem", + "corollary", + "proposition", + "schematic_goal", + "assumes", + "shows", + "obtains", + "and", +]; + +/// Whether a quote after `prev` can wrap a formula rather than a string +/// literal: at the start of the statement, after a `:` (`lemma foo: "…"`), +/// or after an Isabelle statement keyword. [`closes_formula`] must also +/// hold for the text after the closing quote. +fn opens_formula(prev: Option<&Tk>) -> bool { + match prev { + None => true, + Some(Tk::Sym(s)) => s == ":", + Some(Tk::Id(s)) => FORMULA_KEYWORDS.contains(&s.as_str()), + _ => false, + } +} + +/// Whether the text after a closing quote ends the quoted statement: the +/// end of input or a terminator, another quoted proposition +/// (`assumes "A" "B"`), or an Isabelle keyword (`shows`, `and`, `for`, …). +/// Anything else (`"a" == "z"`) means the quote was a string literal. +fn closes_formula(rest: &[char]) -> bool { + const FOLLOWERS: [&str; 6] = ["for", "if", "where", "using", "unfolding", "by"]; + let rest: Vec = rest + .iter() + .copied() + .skip_while(|c| c.is_whitespace()) + .collect(); + match rest.first() { + None | Some('"') => true, + Some('.' | ';') => rest[1..].iter().all(|c| c.is_whitespace()), + Some(c) if is_ident_start(*c) => { + let word: String = rest.iter().take_while(|c| is_ident_char(**c)).collect(); + FORMULA_KEYWORDS.contains(&word.as_str()) || FOLLOWERS.contains(&word.as_str()) + }, + _ => false, + } +} + +/// True when every closer that meets an open group is of that group's kind +/// and nothing is left open. A mismatched closer (`(x]`) is not a structure +/// the parser can read faithfully. A closer with no group open is left to +/// the parser: extraction often keeps the enclosing form's closer at the +/// end (ACL2 `defthm … )`), which `rest_is_ignorable` accepts, while a +/// stray closer followed by more of the statement stops the parse early. +fn brackets_balanced(toks: &[Tk]) -> bool { + let mut stack: Vec = Vec::new(); + for t in toks { + match t { + Tk::Open(c) => stack.push(*c), + Tk::Close(c) => { + let want = match c { + ')' => '(', + ']' => '[', + _ => '{', + }; + match stack.pop() { + None => {}, + Some(open) if open == want => {}, + Some(_) => return false, + } + }, + _ => {}, + } + } + stack.is_empty() } // =========================================================================== @@ -418,6 +550,14 @@ fn matching(toks: &[Tk], at: usize) -> usize { toks.len().saturating_sub(1) } +/// The tokens strictly between an opening bracket at `open` and the index +/// [`matching`] returned for it. Empty when nothing lies between, which +/// includes an unbalanced opening bracket that is the last token: there +/// [`matching`] returns `open` itself, and slicing `open + 1..open` panics. +fn between(toks: &[Tk], open: usize, close: usize) -> &[Tk] { + toks.get(open + 1..close).unwrap_or(&[]) +} + /// Agda writes operators as names: `_<_`, `_+_`, `_≡_`. Read the wrapped /// symbol as one atom so it is not mistaken for three punctuation tokens. fn glue_agda_operators(toks: &[Tk]) -> Vec { @@ -455,15 +595,37 @@ fn has_colon(toks: &[Tk]) -> bool { .any(|t| matches!(t, Tk::Sym(s) if s == ":" || s == "::")) } +/// Whether a top-level `:` or `::=` occurs in `toks` (depth 0 relative to +/// the start of the slice). +fn colon_at_top(toks: &[Tk]) -> bool { + let mut depth = 0usize; + for t in toks { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + } else if depth == 0 && matches!(t, Tk::Sym(s) if s == ":" || s == "::=") { + return true; + } + } + false +} + /// `+-comm : body` and `addComm : body` and `: Π …` all have the declared /// name before a top-level colon; drop it. A group that starts the /// statement (`(x y : Nat) : body`) means there is no head to drop. -fn drop_declared_head(toks: Vec) -> Vec { +/// +/// The second value reports a drop that was *not* a declared head: the +/// first top-level bracket comes after other tokens and no top-level colon +/// follows it, so the dropped tokens were the statement's own (`f (g x) = y` +/// loses `f`). The key is unchanged; [`StructuralKey::complete`] reports it. +fn drop_declared_head(toks: Vec) -> (Vec, bool) { let mut depth = 0usize; for (i, t) in toks.iter().enumerate() { if is_open(t) { if depth == 0 { - return toks[i..].to_vec(); + let unexplained = i > 0 && !colon_at_top(&toks[i..]); + return (toks[i..].to_vec(), unexplained); } depth += 1; } else if is_close(t) { @@ -471,31 +633,38 @@ fn drop_declared_head(toks: Vec) -> Vec { } else if depth == 0 { if let Tk::Sym(s) = t { if s == ":" || s == "::=" { - return toks[i + 1..].to_vec(); + return (toks[i + 1..].to_vec(), false); } } if let Tk::Id(s) = t { if is_pi_kw(s) || is_lam_kw(s) { - return toks[i..].to_vec(); + return (toks[i..].to_vec(), false); } } } } - toks + (toks, false) } /// `(assert (forall …))` → `(forall …)`. -fn unwrap_assert(toks: Vec) -> Vec { +/// +/// The second value reports a wrapper that was unwrapped although its +/// closing bracket is missing (`(assert x y`): [`matching`]'s fallback +/// index is the last token, which also passes the "closes at the end" +/// test, so the wrapper is unwrapped as before (no key changes) and the +/// key is reported incomplete through [`StructuralKey::complete`]. +fn unwrap_assert(toks: Vec) -> (Vec, bool) { let mut cur = toks; + let mut unbalanced = false; loop { if !cur.first().map(is_open).unwrap_or(false) { - return cur; + return (cur, unbalanced); } let j = matching(&cur, 0); if j + 1 != cur.len() { - return cur; + return (cur, unbalanced); } - let inner = cur[1..j].to_vec(); + let inner = between(&cur, 0, j).to_vec(); let head_is_assert = match inner.first() { Some(Tk::Id(s)) => matches!( s.to_lowercase().as_str(), @@ -504,20 +673,49 @@ fn unwrap_assert(toks: Vec) -> Vec { _ => false, }; if !head_is_assert { - return cur; + return (cur, unbalanced); + } + if matching_exact(&cur, 0).is_none() { + unbalanced = true; } cur = inner[1..].to_vec(); } } -fn strip_header(toks: &[Tk]) -> Vec { - let mut cur = unwrap_assert(glue_agda_operators(toks)); +/// Index of the bracket matching `toks[at]`, or `None` when the group is +/// never closed. [`matching`] returns the last index in that case, which +/// callers that need to tell the two apart cannot use. +fn matching_exact(toks: &[Tk], at: usize) -> Option { + let mut depth = 0usize; + for (j, t) in toks.iter().enumerate().skip(at) { + if is_open(t) { + depth += 1; + } else if is_close(t) { + depth = depth.saturating_sub(1); + if depth == 0 { + return Some(j); + } + } + } + None +} + +/// The statement body with any declaration header and proof body removed, and +/// whether the header drop discarded tokens that were not a declared head: +/// a bracket drop (see [`drop_declared_head`]), or a declaration keyword +/// with no top-level `:` or `::=` after it. Keywords match case-insensitively, so a +/// statement that merely *starts* with one (HOL4's `FACT 1 = 1`, keyed as +/// `1 = 1`) loses it; without either separator the drop is flagged. +fn strip_header(toks: &[Tk]) -> (Vec, bool) { + let (mut cur, unbalanced_wrapper) = unwrap_assert(glue_agda_operators(toks)); // declaration keyword + declared name + let mut dropped_kw = false; loop { let drops_kw = matches!(cur.first(), Some(Tk::Id(s)) if is_decl_kw(s)); if !drops_kw { break; } + dropped_kw = true; cur.remove(0); if matches!(cur.first(), Some(Tk::Id(_))) { cur.remove(0); @@ -543,7 +741,12 @@ fn strip_header(toks: &[Tk]) -> Vec { Some(i) => cur[..i].to_vec(), None => cur, }; - drop_declared_head(cur) + let keyword_unexplained = dropped_kw && !colon_at_top(&cur); + let (body, head_unexplained) = drop_declared_head(cur); + ( + body, + head_unexplained || keyword_unexplained || unbalanced_wrapper, + ) } /// `x y : Nat` → (["x","y"], NAT); SMT-LIB `x Nat` likewise. @@ -584,6 +787,11 @@ fn sort_name(toks: &[Tk]) -> String { struct Binders { names: Vec, sorts: Vec, + /// A leading bracket group was read as a telescope although one of its + /// "names" is a binder keyword: `(forall x : nat, P x) -> Q` binds + /// `forall` and `x` and keeps only `Q`. Reported through + /// [`StructuralKey::complete`]; the key is unchanged. + misread: bool, } impl Binders { @@ -609,7 +817,7 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { // 1. leading binder group without a keyword while cur.first().map(is_open).unwrap_or(false) { let j = matching(&cur, 0); - let (names, sort) = split_binder_group(&cur[1..j]); + let (names, sort) = split_binder_group(between(&cur, 0, j)); if names.is_empty() { break; } @@ -620,9 +828,12 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { if !after_ok { break; } - if !has_colon(&cur[1..j]) { + if !has_colon(between(&cur, 0, j)) { break; } + if names.iter().any(|n| is_pi_kw(n) || is_lam_kw(n)) { + bound.misread = true; + } for n in &names { bound.push(std::slice::from_ref(n), &sort); } @@ -633,20 +844,20 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { if cur.first().map(is_open).unwrap_or(false) { let j = matching(&cur, 0); if j + 1 == cur.len() { - let inner: Vec = cur[1..j].to_vec(); + let inner: Vec = between(&cur, 0, j).to_vec(); let head_ok = matches!(inner.first(), Some(Tk::Id(s)) if is_pi_kw(s) || is_lam_kw(s)); if head_ok { let rest: Vec = inner[1..].to_vec(); if rest.first().map(is_open).unwrap_or(false) { let m = matching(&rest, 0); - let group: Vec = rest[1..m].to_vec(); + let group: Vec = between(&rest, 0, m).to_vec(); let mut names: Vec = Vec::new(); let mut sorts: Vec = Vec::new(); if group.first().map(is_open).unwrap_or(false) { let mut k = 0usize; while k < group.len() && is_open(&group[k]) { let e = matching(&group, k); - let (n, s) = split_binder_group(&group[k + 1..e]); + let (n, s) = split_binder_group(between(&group, k, e)); for name in n { names.push(name); sorts.push(s.clone()); @@ -701,7 +912,7 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { } if is_open(&cur[i]) { let m = matching(&cur, i); - let (n, s) = split_binder_group(&cur[i + 1..m]); + let (n, s) = split_binder_group(between(&cur, i, m)); if n.is_empty() { break; } @@ -756,32 +967,74 @@ fn extract_binders(toks: &[Tk]) -> (Vec, Binders) { (out, bound) } -/// Isabelle's `(x :: nat)` is a term ascription, not a binder. +/// Unwrap Isabelle-style `(x :: nat)` ascriptions with recognised sorts, +/// retaining the term identifier. Other groups are preserved. +/// +/// A group qualifies when, between its brackets, there are exactly two +/// identifiers and one symbol, the symbol is `::` and the second identifier +/// is a known sort; numbers and nested brackets do not count. The group is +/// replaced by the first identifier, so `(f 0 :: nat)` and `((x) :: nat)` +/// reduce as `dk-shape-v1` always has. Bracket matches and token counts are +/// computed once, so the pass is linear even on deeply nested input. fn drop_ascriptions(toks: &[Tk]) -> Vec { + let n = toks.len(); + // close[i]: the index `matching(toks, i)` returns for an opener at `i`. + let mut close: Vec = vec![n.saturating_sub(1); n]; + let mut stack: Vec = Vec::new(); + for (j, t) in toks.iter().enumerate() { + if is_open(t) { + stack.push(j); + } else if is_close(t) { + if let Some(i) = stack.pop() { + close[i] = j; + } + } + } + // Prefix counts and next-occurrence tables for identifiers and symbols. + let mut ids_before = vec![0usize; n + 1]; + let mut syms_before = vec![0usize; n + 1]; + for (k, t) in toks.iter().enumerate() { + ids_before[k + 1] = ids_before[k] + usize::from(matches!(t, Tk::Id(_))); + syms_before[k + 1] = syms_before[k] + usize::from(matches!(t, Tk::Sym(_))); + } + let mut next_id = vec![n; n + 1]; + let mut next_sym = vec![n; n + 1]; + for k in (0..n).rev() { + next_id[k] = if matches!(toks[k], Tk::Id(_)) { + k + } else { + next_id[k + 1] + }; + next_sym[k] = if matches!(toks[k], Tk::Sym(_)) { + k + } else { + next_sym[k + 1] + }; + } + let id_at = |k: usize| match &toks[k] { + Tk::Id(s) => s, + _ => unreachable!("next_id points at an identifier"), + }; + let mut out: Vec = Vec::new(); let mut i = 0usize; - while i < toks.len() { + while i < n { if is_open(&toks[i]) { - let j = matching(toks, i); - let inner: Vec = toks[i + 1..j].to_vec(); - let ids: Vec<&String> = inner - .iter() - .filter_map(|t| match t { - Tk::Id(s) => Some(s), - _ => None, - }) - .collect(); - let syms: Vec<&String> = inner - .iter() - .filter_map(|t| match t { - Tk::Sym(s) => Some(s), - _ => None, - }) - .collect(); - if ids.len() == 2 && syms.len() == 1 && syms[0] == "::" && sort_of(ids[1]).is_some() { - out.push(Tk::Id(ids[0].clone())); - i = j + 1; - continue; + let j = close[i]; + // the tokens strictly between, as `between(toks, i, j)` gives them + let (lo, hi) = (i + 1, j.max(i + 1)); + let ids = ids_before[hi] - ids_before[lo]; + let syms = syms_before[hi] - syms_before[lo]; + if ids == 2 && syms == 1 { + let first = next_id[lo]; + let second = next_id[first + 1]; + let is_ascription = matches!(&toks[next_sym[lo]], Tk::Sym(s) if s == "::") + && sort_of(id_at(second)).is_some(); + if is_ascription { + out.push(Tk::Id(id_at(first).clone())); + i = j + 1; + continue; + } } } out.push(toks[i].clone()); @@ -809,17 +1062,60 @@ struct Parser { toks: Vec, i: usize, varmap: std::collections::HashMap, + /// Opening brackets the input ended before closing: a statement + /// truncated inside a group (`(x = y`) parses to the end and would + /// otherwise look complete. + unclosed: usize, + /// Current tree depth (brackets and operator nesting), bounded by + /// [`MAX_NESTING`]. + depth: usize, + /// The tree reached [`MAX_NESTING`]: a group was skipped as a hole, or + /// the rest of an operator chain was skipped. + too_deep: bool, + /// A prefix operator that needs two operands was given one. + under_arity: bool, } +/// Deepest tree the parser builds. Each bracket group and each infix +/// operator nests the tree one level (a bracket costs three stack frames, +/// `expr` → `app` → `atom`; a right-associative operator costs one `expr` +/// frame; a left-associative chain deepens the tree that `render`, +/// `has_hole` and drop then walk). `structural_key` runs on the caller's +/// stack (`corpus ingest`, octad export), so a statement deeper than this +/// is cut off and marked incomplete rather than allowed to overflow it. +/// The shipped corpora reach a bracket depth in the fifties. +const MAX_NESTING: usize = 256; + impl Parser { + /// Start at the first token, using `varmap` to map source names to canonical variables. fn new(toks: Vec, varmap: std::collections::HashMap) -> Self { - Parser { toks, i: 0, varmap } + Parser { + toks, + i: 0, + varmap, + unclosed: 0, + depth: 0, + too_deep: false, + under_arity: false, + } } fn peek(&self) -> Option<&Tk> { self.toks.get(self.i) } + /// Whether everything after the cursor is ignorable: a statement + /// terminator (`.`, `,`, `;`) or an unmatched closing bracket. + fn rest_is_ignorable(&self) -> bool { + self.toks[self.i.min(self.toks.len())..] + .iter() + .all(|t| match t { + Tk::Close(_) => true, + Tk::Sym(s) => matches!(s.as_str(), "." | "," | ";"), + _ => false, + }) + } + /// Canonical operator starting at the cursor, if any. fn op_at(&self) -> Option<&'static str> { match self.peek()? { @@ -828,14 +1124,28 @@ impl Parser { } } + /// Read an atom or bracketed expression, advancing the cursor. Return + /// `None` at end of input, before a closing bracket, or after consuming + /// `:`, `::`, `,` or `.`. Groups beyond the nesting limit become holes + /// and set `too_deep`; groups ending at EOF set `unclosed`. fn atom(&mut self) -> Option { let t = self.peek()?.clone(); match t { Tk::Open(_) => { + if self.depth >= MAX_NESTING { + // Skip the whole group; the key is marked incomplete. + self.too_deep = true; + self.i = matching(&self.toks, self.i) + 1; + return Some(Node::Hole); + } + self.depth += 1; self.i += 1; let inner = self.expr(0); + self.depth -= 1; if matches!(self.peek(), Some(Tk::Close(_))) { self.i += 1; + } else if self.peek().is_none() { + self.unclosed += 1; } Some(inner) }, @@ -924,6 +1234,11 @@ impl Parser { if args.is_empty() { return Node::Name(op_name.to_string()); } + // A relation or other binary-only operator with one operand + // (`(= (+ x 1))`) is a truncated statement, not a shape. + if args.len() < 2 && is_binary_only(op_name) { + self.under_arity = true; + } return Node::Op(op_name, args); } let mut args: Vec = vec![head.clone()]; @@ -952,6 +1267,9 @@ impl Parser { fn expr(&mut self, min_prec: u8) -> Node { let mut left = self.app(); + // Operators applied so far at this level: a left-associative chain + // deepens `left` by one node each time. + let mut chain = 0usize; while let Some(op) = self.op_at() { let Some(prec) = precedence(op) else { break; @@ -959,19 +1277,43 @@ impl Parser { if prec < min_prec { break; } + // Every operator nests the tree one level deeper, whether the + // chain grows left (`a + a + …`) or recurses right (`a -> a -> …`). + // Past MAX_NESTING the rest is skipped and the key marked + // incomplete, so neither this parser nor the recursive passes over + // the tree (`render`, `has_hole`, drop) can overflow the stack. + if self.depth + chain >= MAX_NESTING { + self.too_deep = true; + self.i = self.toks.len(); + break; + } self.i += 1; let rhs_min = if op == "ARROW" || op == "IFF" { prec } else { prec + 1 }; + chain += 1; + self.depth += chain; let right = self.expr(rhs_min); + self.depth -= chain; left = Node::Op(op, vec![left, right]); } left } } +/// Whether the parser had to invent a node: a missing operand after a +/// trailing operator (`x + 1 =`), or a group it refused to descend into. +/// Either way the shape does not describe the statement. +fn has_hole(node: &Node) -> bool { + match node { + Node::Hole => true, + Node::Op(_, kids) | Node::App(kids) => kids.iter().any(has_hole), + _ => false, + } +} + fn render(node: &Node, skeleton: bool) -> String { match node { Node::Var(s) | Node::Name(s) | Node::Num(s) => s.clone(), @@ -1069,13 +1411,60 @@ fn number_variables(body: &[Tk], bound: &Binders) -> std::collections::HashMap (String, String) { - let toks = strip_header(&lex(statement)); +/// Tokens that introduce notation this scheme has no rule for: HOL's `!`, +/// `?`, `@` and `\` binders and `~` negation, Isabelle's `\<…>` symbol +/// escapes (which lex as `\`, `<`, name, `>`), and Lean 3's `$` application. +/// The parser reads them as plain names and consumes them, so a shape can +/// look complete and still be wrong; their presence marks the key +/// incomplete. Over-cautious by design: Lean's `s \ t` set difference is +/// flagged too. +fn is_unread_notation(t: &Tk) -> bool { + matches!(t, Tk::Sym(s) if matches!(s.as_str(), "\\" | "!" | "?" | "@" | "$" | "~")) +} + +/// Whether the body holds unread notation: a token [`is_unread_notation`] +/// names, or HOL's `==>` implication, which the lexer splits into `==` and +/// `>` (the shape it then renders is an equality applied to a comparison). +/// The lexer is left alone so that no key changes; only the flag sees it. +fn has_unread_notation(body: &[Tk]) -> bool { + body.iter().any(is_unread_notation) + || body + .windows(2) + .any(|w| matches!((&w[0], &w[1]), (Tk::Sym(a), Tk::Sym(b)) if a == "==" && b == ">")) +} + +/// Both canonical forms from one pass, and whether the shape accounts for +/// the whole statement: `(shape, skeleton, complete)`. Complete means every +/// quote and block comment closes, no closer meets a group of another kind, +/// the header drop discarded only a declared head, no leading group was misread +/// as a telescope, the body holds no unread notation, and the parser +/// left only ignorable terminators or closing brackets, with no group +/// left open at end of input or skipped beyond [`MAX_NESTING`], invented +/// no missing operand, and gave no binary-only prefix operator one operand. +fn normalise(statement: &str) -> (String, String, bool) { + let (raw, terminated) = lex_flagged(statement); + // Read over the whole statement, header included: a mismatched or + // stray bracket, or a quote or block comment that never closes, means + // the tokens are not the statement as written. + let well_formed = terminated && brackets_balanced(&raw); + let (toks, dropped_body) = strip_header(&raw); + // Checked before ascriptions and binders are removed: a binder's sort + // can hold notation too (`(x : F $ A)`), and extraction would drop it. + let unread = has_unread_notation(&toks); let toks = drop_ascriptions(&toks); let (body, bound) = extract_binders(&toks); let varmap = number_variables(&body, &bound); - let ast = Parser::new(body, varmap).expr(0); + let mut parser = Parser::new(body, varmap); + let ast = parser.expr(0); + let complete = !has_hole(&ast) + && well_formed + && parser.rest_is_ignorable() + && parser.unclosed == 0 + && !parser.too_deep + && !parser.under_arity + && !unread + && !dropped_body + && !bound.misread; let core = render(&ast, false); let skel = render(&ast, true); @@ -1093,7 +1482,7 @@ fn normalise(statement: &str) -> (String, String) { } else { skel }; - (shape, skeleton) + (shape, skeleton, complete) } /// Canonical prefix shape of `statement`, binder prefix included. @@ -1111,8 +1500,11 @@ pub fn canonical_skeleton(statement: &str) -> String { /// The three tiers are tried in order: the shape as written; the shape with /// binders and sorts erased (covers provers that elide them); and finally /// whitespace-normalised text (covers statements that are not terms). +/// A partial parse can still yield a structural key; consult +/// [`StructuralKey::complete`] before treating it as the whole statement. +/// Text-tier keys always have `complete = false`. pub fn structural_key(statement: &str) -> StructuralKey { - let (shape, skeleton) = normalise(statement); + let (shape, skeleton, parsed_all) = normalise(statement); let (shape, skeleton, tier) = if !shape.is_empty() { (shape, skeleton, KeyTier::Structural) @@ -1129,6 +1521,7 @@ pub fn structural_key(statement: &str) -> StructuralKey { skeleton_key: sha256_hex(&skeleton), shape, skeleton, + complete: parsed_all && tier != KeyTier::Text, tier, } } @@ -1137,6 +1530,12 @@ pub fn structural_key(statement: &str) -> StructuralKey { /// /// Falls back to the lower-cased source tokens when the statement does not /// parse, so every declaration contributes *something*. +/// Number of lexical tokens in `statement`, punctuation counted: `f(x)=g(x)` +/// is eight. For callers that need "how much is here" without a parse. +pub fn token_count(statement: &str) -> usize { + lex(statement).len() +} + pub fn canonical_tokens(statement: &str) -> Vec { let shape = canonical_shape(statement); let source = if shape.is_empty() { @@ -1279,4 +1678,292 @@ mod tests { assert!(toks.contains(&"v0".to_string())); assert!(!toks.iter().any(|t| t.contains("forall"))); } + + /// An opening bracket with nothing after it used to make `matching` + /// return the bracket's own index, and every `open + 1..close` slice + /// then panicked. Corpus statements truncated mid-term hit this. + #[test] + fn unbalanced_trailing_bracket_does_not_panic() { + for s in [ + "(", + "f x = (", + "forall (", + "∀ x, x = (", + "(assert (", + "(forall ((x Nat)) (", + "theorem t (x : nat) : x = (", + ] { + let k = structural_key(s); + assert_eq!(k.key.len(), 64, "{s:?}"); + assert_eq!(k.scheme, SCHEME); + } + } + + /// Every fixture spelling parses completely; the flag does not change + /// any key. + #[test] + fn fixture_spellings_parse_completely() { + for (prover, s) in ADD_COMM { + let k = structural_key(s); + assert!(k.complete, "{prover}: {s:?} -> {}", k.shape); + } + assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); + // ACL2 extraction keeps the `defthm` form's closer at the end + assert!(structural_key("(equal (len (rev x)) (len x)))").complete); + // one-operand prefix forms that are legitimate + for s in ["(= (- x) (- 0 x))", "(not (= x y))", "(= (+ x) x)"] { + assert!(structural_key(s).complete, "{s}"); + } + } + + /// `drop_ascriptions` as `dk-shape-v1` shipped it (c03386b), with the + /// slice guarded. The linear version must agree with it exactly. + fn drop_ascriptions_reference(toks: &[Tk]) -> Vec { + let mut out: Vec = Vec::new(); + let mut i = 0usize; + while i < toks.len() { + if is_open(&toks[i]) { + let j = matching(toks, i); + let inner = between(toks, i, j); + let ids: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Id(s) => Some(s), + _ => None, + }) + .collect(); + let syms: Vec<&String> = inner + .iter() + .filter_map(|t| match t { + Tk::Sym(s) => Some(s), + _ => None, + }) + .collect(); + if ids.len() == 2 && syms.len() == 1 && syms[0] == "::" && sort_of(ids[1]).is_some() + { + out.push(Tk::Id(ids[0].clone())); + i = j + 1; + continue; + } + } + out.push(toks[i].clone()); + i += 1; + } + out + } + + #[test] + fn drop_ascriptions_matches_dk_shape_v1() { + for s in [ + "(x :: nat) + 0 = x", + "(f 0 :: nat) = f 0", + "((x) :: nat) = x", + "[x :: int] = y", + "(x :: foo) = x", + "(x :: nat", + "(", + "(x y :: nat) = z", + "((a :: nat) :: nat)", + "(x :: nat] + (y :: int)", + ] { + let toks = lex(s); + assert_eq!( + drop_ascriptions(&toks), + drop_ascriptions_reference(&toks), + "{s}" + ); + } + } + + proptest::proptest! { + #[test] + fn drop_ascriptions_agrees_with_reference_on_random_tokens( + picks in proptest::collection::vec(0usize..9, 0..60) + ) { + const ALPHABET: [&str; 9] = ["(", ")", "[", "]", "x", "nat", "::", "0", "+"]; + let s: String = picks.iter().map(|&p| ALPHABET[p]).collect::>().join(" "); + let toks = lex(&s); + proptest::prop_assert_eq!(drop_ascriptions(&toks), drop_ascriptions_reference(&toks)); + } + } + + /// A string literal is one opaque atom; a formula wrapper is unwrapped. + #[test] + fn string_literals_are_atoms_and_formula_quotes_are_unwrapped() { + let a = structural_key("s = \"a//b\""); + let b = structural_key("s = \"a//c\""); + assert!(a.complete && b.complete); + assert_ne!(a.key, b.key, "the literal's tail is not a comment"); + assert_ne!( + structural_key("s = \"x\"").key, + structural_key("s = x").key, + "a literal is not the variable it spells" + ); + assert_ne!( + structural_key("s = \"a \\\" b\"").key, + structural_key("s = \"a \\\" c\"").key, + "an escaped quote does not end the literal" + ); + // a literal at the start of the statement is still a literal when + // the statement goes on after it + assert_ne!( + structural_key("\"a\" == \"z\"").key, + structural_key("\"b\" == \"z\"").key + ); + // Isabelle's quoted assumptions and conclusion are all unwrapped + assert_eq!( + structural_key("assumes \"x = y\" shows \"y = x\"").shape, + structural_key("assumes x = y shows y = x").shape + ); + // adjacent quoted propositions are all formulas + assert_eq!( + structural_key("assumes \"x = y\" \"y = z\" shows \"x = z\"").shape, + structural_key("assumes x = y y = z shows x = z").shape + ); + let bare = structural_key("x + y = y + x").key; + for s in ["\"x + y = y + x\"", "lemma add_comm: \"x + y = y + x\""] { + assert_eq!(structural_key(s).key, bare, "{s}"); + } + // An anonymous `lemma "…"` loses its first token to the header drop + // (a dk-shape-v1 rule, D6); the drop is reported, never trusted. + let anon = structural_key("lemma \"x + y = y + x\""); + assert!(anon.key == bare || !anon.complete); + } + + /// Statements the scheme cannot read are marked incomplete even though + /// they still get a structural-tier key. + #[test] + fn unread_notation_and_early_stops_are_incomplete() { + for s in [ + // HOL binders, negation and implication (`==>` lexes as `==` `>`) + "!m n. m + n = n + m", + "?x. x = 0", + "(\\x. x) = I", + "~F", + "F ==> T", + // truncated inside a group: the parser reaches the end with the + // group still open + "(x = y", + "(implies (and (bvp m) (< (len m) (expt 2 64))", + // truncated after an operator: the parser invents the operand + "x + 1 =", + "forall x : nat, x = x /\\", + // a wrapper whose close is missing is still unwrapped (no key + // change) and reported + "(assert x y", + "(assert (forall ((x Nat)) (= x x", + // a binary-only prefix operator given one operand + "(= (+ x 1))", + "(< x)", + "(implies (p x) (<= x))", + // a closer of the wrong kind, or a stray one + "(x + y] = z", + "x + y) = z", + // a quote or block comment that runs off the end + "\"x + y = y + x", + "x + y = y + x (* commutes", + // notation inside a binder's sort is dropped by extraction + "forall (x : F $ A), x + 0 = x", + // Isabelle ASCII symbol escapes + "x \\ y \\ f x = f y", + // Lean 3 `$` + "f $ g x = h x", + ] { + let k = structural_key(s); + assert!(!k.complete, "{s:?} -> {} should be incomplete", k.shape); + } + // Text tier is never complete. + assert!(!structural_key("data Bool where true false").complete); + } + + /// A statement with no declared head used to lose everything before its + /// first top-level bracket (`exp(&0) = &1` keyed as `(EQ (& 0) (& 1))`, + /// shared with `cos(&0) = &1`). The key is unchanged here; the drop is + /// reported as incomplete so no consumer treats the prefix as identity. + #[test] + fn header_less_bracket_drop_is_incomplete() { + let exp = structural_key("exp(0) = 1"); + let cos = structural_key("cos(0) = 1"); + assert_eq!(exp.key, cos.key, "the dk-shape-v1 behaviour this flags"); + assert!(!exp.complete && !cos.complete); + assert!(!structural_key("closed (closure M)").complete); + // A real declared head before a group is still a head. + let lean = structural_key("theorem t (x y : nat) : x + y = y + x"); + assert!(lean.complete, "{}", lean.shape); + let idris = structural_key("addComm : (x, y : Nat) -> x + y = y + x"); + assert!(idris.complete, "{}", idris.shape); + } + + /// `FACT` is HOL's factorial and also matches the `fact` keyword: the + /// key drops it (`FACT 1 = 1` keys as `1 = 1`), so the key is reported + /// incomplete. A keyword followed by a declaration is still complete. + #[test] + fn keyword_drop_without_a_declaration_is_incomplete() { + let fact = structural_key("FACT 1 = 1"); + assert_eq!( + fact.key, + structural_key("1 = 1").key, + "the behaviour this flags" + ); + assert!(!fact.complete); + assert!(structural_key("1 = 1").complete); + assert!(structural_key("Lemma add_comm : forall x y : nat, x + y = y + x.").complete); + assert!(structural_key("theorem t (x y : nat) : x + y = y + x").complete); + } + + /// A parenthesised quantified antecedent at the start of a statement is + /// read as a binder telescope (`forall` and `x` become bound names and + /// only `Q` is left). The key is unchanged; it is reported incomplete. + #[test] + fn telescope_misread_of_a_quantified_antecedent_is_incomplete() { + let k = structural_key("(forall x : nat, P x) -> Q"); + assert_eq!(k.shape, "(PI [NAT NAT] v0)", "the behaviour this flags"); + assert!(!k.complete); + // A real telescope is still complete. + assert!(structural_key("(x y : nat) : x + y = y + x").complete); + } + + /// Nesting past `MAX_NESTING` is cut off and marked incomplete instead + /// of recursing once per level. Fifty thousand levels would overflow a + /// test thread's stack without the bound; within the bound keys are as + /// before. + #[test] + fn nesting_is_bounded() { + let deep = format!("{}x{}", "(".repeat(50_000), ")".repeat(50_000)); + let k = structural_key(&deep); + assert!(!k.complete); + assert_eq!(k.key.len(), 64); + let shallow = format!("{}x = y{}", "(".repeat(60), ")".repeat(60)); + let s = structural_key(&shallow); + assert!(s.complete, "{}", s.shape); + assert_eq!(s.key, structural_key("x = y").key); + } + + /// Flat operator chains nest the tree too: a right-associative chain + /// recurses once per operator and a left-associative one builds a tree + /// that deep. Both overflowed a test thread's stack before the bound. + #[test] + fn operator_chains_are_bounded() { + for chain in ["a -> ", "a + ", "a /\\ ", "a = "] { + let long = format!("{}a", chain.repeat(200_000)); + let k = structural_key(&long); + assert!(!k.complete, "{chain}"); + assert_eq!(k.key.len(), 64); + } + let short = format!("{}a", "a + ".repeat(100)); + assert!(structural_key(&short).complete); + } + + /// The guard is a no-op on balanced input: keys stay as they were. + #[test] + fn balanced_input_keys_are_unchanged_by_the_bracket_guard() { + assert_eq!( + canonical_shape("forall x y : nat, x + y = y + x"), + "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" + ); + assert_eq!( + canonical_shape("(assert (forall ((x Nat) (y Nat)) (= (+ x y) (+ y x))))"), + "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" + ); + } } diff --git a/src/rust/lexicon/mod.rs b/src/rust/lexicon/mod.rs new file mode 100644 index 00000000..a81923f6 --- /dev/null +++ b/src/rust/lexicon/mod.rs @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Lexicon tooling that works *on* corpora rather than on one synonym table. +//! +//! The synonym tables themselves (`data/synonyms/*.toml`, loaded by +//! [`crate::suggest::synonyms`]) are curated by hand under the Nickel +//! contract `data/synonyms/schema.ncl`. This module only *proposes*: it +//! mines the training corpora for rows a curator may want to add, and every +//! proposal carries `evidence = none` (owner decision D4 in +//! `docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc`). + +pub mod scan; diff --git a/src/rust/lexicon/scan.rs b/src/rust/lexicon/scan.rs new file mode 100644 index 00000000..7d34a846 --- /dev/null +++ b/src/rust/lexicon/scan.rs @@ -0,0 +1,1498 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! `echidna lexicon scan`: a cross-corpus candidate generator for the lexicon. +//! +//! Two corpora are compared along two axes, the *name* of a theorem and the +//! canonical *shape* of its statement ([`crate::corpus::canonical`], scheme +//! `dk-shape-v1`). The four combinations are the four things a curator +//! wants to know about: +//! +//! | | same shape | different shape | +//! |---|---|---| +//! | **same name** | cognate | false friend, or specialisation | +//! | **different name** | synonym candidate | unrelated (not reported) | +//! +//! A pair joined by name is classified by the strongest tier at which its two +//! statements agree: identical text (`cognate_exact`), the same structural +//! key (`cognate_shape`: same shape up to variable names), the same skeleton +//! key only (`cognate_skeleton`: the shapes differ in binders or sorts, the +//! usual signature of a specialisation such as `nat` against `real`), or +//! none (`differs`). A pair joined by identical text, by shape, or failing +//! those by skeleton has different names and is a synonym candidate; the +//! text join needs no canonicaliser at all. +//! +//! Shape classification needs both statements read *completely* +//! ([`StructuralKey::complete`]). `dk-shape-v1` still returns a +//! structural-tier key when its parser stops early or meets notation it has +//! no rule for (HOL binders, Isabelle `\<…>` escapes), and that key is a +//! prefix many different statements share. Such pairs are `unparsed`, and +//! such statements take no part in shape or skeleton joins. +//! +//! None of this is evidence. The canonical shape is a syntactic key, not a +//! decision procedure; `dk-shape-v1` documents what it does not normalise, +//! and [`Coverage`] measures how much of each corpus it actually reads and +//! how often distinct statements collide on one key. Every candidate is +//! written with `evidence = { kind = "none" }` and never edits +//! `data/synonyms/` (owner decision D4). +//! +//! Output is I-JSON serialised as JCS (RFC 8785), one record per line, so +//! records hash and diff stably. Each candidate's `id` is the UUIDv8 content +//! id ([`crate::ids::content_id`]) of the statement pair alone, with the two +//! sides in a fixed order: the same pair keeps the same id whichever corpus +//! is named first and whichever normaliser version classified it, so a +//! curator's review survives a re-scan. + +use std::collections::{BTreeMap, BTreeSet, HashMap}; +use std::fs::{self, File}; +use std::io::{BufRead, BufReader, BufWriter, Write}; +use std::path::{Path, PathBuf}; +use std::time::{Duration, Instant}; + +use anyhow::{bail, Context, Result}; +use serde::Serialize; + +use crate::corpus::canonical::{self, KeyTier, StructuralKey}; +use crate::suggest::synonyms::LexiconEvidence; + +/// Schema tag of one candidate record. +pub const CANDIDATE_SCHEMA: &str = "echidna.lexicon.candidate/1"; +/// Schema tag of one per-pair summary record. +pub const PAIR_SUMMARY_SCHEMA: &str = "echidna.lexicon.pair-summary/1"; +/// Schema tag of one per-corpus coverage record. +pub const COVERAGE_SCHEMA: &str = "echidna.lexicon.coverage/1"; +/// Schema tag of one sampled key-collision group. +pub const COLLISION_SCHEMA: &str = "echidna.lexicon.collision/1"; + +/// One corpus per prover family, the cross-family spanning set: classical +/// higher-order logic (HOL4), Isabelle/HOL (the AFP), dependent type theory +/// (Lean 3), set theory (Mizar), first-order computational logic (ACL2), +/// auto-active verification (Why3), logic programming (λProlog) and the +/// λΠ-modulo hub (Dedukti). +pub const SPANNING: [&str; 8] = [ + "hol4", + "afp", + "lean3", + "mizar", + "acl2", + "why3", + "lambda_prolog", + "dedukti", +]; + +/// One pair inside each family that has a second corpus, so differences +/// within a family can be told apart from differences across families. +pub const IN_FAMILY: [(&str, &str); 5] = [ + ("hol4", "hol_light"), + ("lean3", "agda"), + ("acl2", "acl2s"), + ("why3", "dafny"), + ("mizar", "isabelle_zf"), +]; + +/// The two pairs read first: the stage-6a pilot pair inside the HOL family, +/// and the cross-family pair with the most shared names. +pub const LEARNING: [(&str, &str); 2] = [("hol4", "hol_light"), ("lean3", "afp")]; + +/// The pairs a named preset expands to, in scan order, or `None` for an +/// unknown preset. `full` is every spanning pair followed by the in-family +/// pairs. +pub fn preset_pairs(preset: &str) -> Option> { + let owned = |pairs: &[(&str, &str)]| { + pairs + .iter() + .map(|(a, b)| (a.to_string(), b.to_string())) + .collect::>() + }; + let spanning = || { + let mut out = Vec::new(); + for (i, a) in SPANNING.iter().enumerate() { + for b in &SPANNING[i + 1..] { + out.push((a.to_string(), b.to_string())); + } + } + out + }; + match preset { + "learning" => Some(owned(&LEARNING)), + "spanning" => Some(spanning()), + "in-family" => Some(owned(&IN_FAMILY)), + "full" => { + let mut out = spanning(); + out.extend(owned(&IN_FAMILY)); + Some(out) + }, + _ => None, + } +} + +/// Parse a `A:B` pair argument. Both sides must be corpus keys as they +/// appear in `proof_states_.jsonl`; their existence is not checked. +/// +/// # Errors +/// +/// The separator is missing, either key fails [`validate_corpus_key`], or +/// both keys are identical. Whitespace is not trimmed. +pub fn parse_pair(arg: &str) -> Result<(String, String)> { + let (a, b) = arg + .split_once(':') + .with_context(|| format!("pair `{arg}` must be written A:B"))?; + validate_corpus_key(a)?; + validate_corpus_key(b)?; + if a == b { + bail!("pair `{arg}` names the same corpus twice"); + } + Ok((a.to_string(), b.to_string())) +} + +/// Validate a corpus key for use in scan file names. +/// +/// # Errors +/// +/// The key is empty, contains characters outside `[a-z0-9_-]` (the shipped +/// `proof_states_2026-03-20.jsonl` needs the hyphen), contains +/// `__`, or starts or ends with `_`. `__` separates the two keys in a pair +/// file name, and a key at either edge of it must not supply a third `_` +/// (`a_:b` and `a:_b` would both write `pairs/a___b.jsonl`). +pub fn validate_corpus_key(key: &str) -> Result<()> { + if key.is_empty() + || !key + .chars() + .all(|c| c.is_ascii_lowercase() || c.is_ascii_digit() || c == '_' || c == '-') + { + bail!("corpus key `{key}` must be non-empty [a-z0-9_-]"); + } + // `pairs/__.jsonl` is unambiguous only if no key contains `__` + // and no key starts or ends with `_`. + if key.contains("__") { + bail!("corpus key `{key}` must not contain `__`"); + } + if key.starts_with('_') || key.ends_with('_') { + bail!("corpus key `{key}` must not start or end with `_`"); + } + Ok(()) +} + +/// Fold a theorem name for cross-prover matching: keep the last component +/// of a dotted or `::`-qualified name, lower-case it, read `-` as `_`, and +/// trim surrounding underscores. `nat.add_comm`, `ADD_COMM` and `add-comm` +/// all fold to `add_comm`. A single `:` also separates components. If the +/// name ends in a separator, the whole name is used before folding. +pub fn fold_name(name: &str) -> String { + let tail = name.rsplit(['.', ':']).next().unwrap_or(name); + let tail = if tail.is_empty() { name } else { tail }; + tail.to_lowercase() + .replace('-', "_") + .trim_matches('_') + .to_string() +} + +/// Folded names that say nothing about the statement: numbered lemmas, +/// examples, auxiliaries, Mizar's anonymous theorems and any stem of two +/// characters or fewer once trailing digits, primes and underscores are +/// removed (`l3`, `th27`, `ex1`, `z`). +const GENERIC_STEMS: [&str; 34] = [ + "anonymous", + "aux", + "auxiliary", + "bar", + "base", + "baz", + "case", + "claim", + "cor", + "corollary", + "def", + "defn", + "example", + "exercise", + "fact", + "foo", + "goal", + "helper", + "ind", + "key", + "lem", + "lemma", + "main", + "prop", + "remark", + "result", + "step", + "sublemma", + "temp", + "test", + "thm", + "theorem", + "tmp", + "unnamed", +]; + +/// Whether a folded name is too generic to join two corpora on. +pub fn is_generic(folded: &str) -> bool { + let stem = folded.trim_end_matches(|c: char| c.is_ascii_digit() || c == '\'' || c == '_'); + stem.chars().count() <= 2 || GENERIC_STEMS.contains(&stem) +} + +/// One distinct `(name, statement)` row of a corpus. +#[derive(Debug, Clone)] +pub struct Entry { + pub name: String, + /// The statement with runs of whitespace collapsed to one space. + pub statement: String, + key: usize, +} + +/// A training corpus, deduplicated and indexed for the scan. +#[derive(Debug, Clone)] +pub struct Corpus { + pub key: String, + /// Distinct rows, sorted by name then statement. + pub entries: Vec, + keys: Vec, + pub lines_read: usize, + /// Lines that are not JSON objects. + pub lines_malformed: usize, + /// Objects without a non-empty string `theorem` and `goal`. + pub lines_without_statement: usize, + by_name: BTreeMap>, + by_fold: BTreeMap>, + by_statement: BTreeMap>, + by_shape: BTreeMap>, + by_skeleton: BTreeMap>, +} + +/// Collapse each whitespace run to one character: a newline if the run +/// holds one, else a space. Line breaks are kept because they end line +/// comments (`-- …`, `// …`); joining the lines would turn the rest of +/// the statement into comment. +fn collapse_whitespace(s: &str) -> String { + let mut out = String::with_capacity(s.len()); + let mut pending: Option = None; + for c in s.trim().chars() { + if c.is_whitespace() { + if c == '\n' { + pending = Some('\n'); + } else if pending.is_none() { + pending = Some(' '); + } + } else { + if let Some(p) = pending.take() { + out.push(p); + } + out.push(c); + } + } + out +} + +/// `__.jsonl` with two valid corpus keys: a name `run` writes. +fn is_pair_file_name(name: &str) -> bool { + name.strip_suffix(".jsonl") + .and_then(|stem| stem.split_once("__")) + .is_some_and(|(a, b)| validate_corpus_key(a).is_ok() && validate_corpus_key(b).is_ok()) +} + +/// Remove the files in `dir` whose names `is_ours` recognises. +fn remove_generated(dir: &Path, is_ours: fn(&str) -> bool) -> Result<()> { + for entry in fs::read_dir(dir).with_context(|| format!("read {}", dir.display()))? { + let path = entry?.path(); + let ours = path.is_file() + && path + .file_name() + .and_then(|n| n.to_str()) + .is_some_and(is_ours); + if ours { + fs::remove_file(&path).with_context(|| format!("remove {}", path.display()))?; + } + } + Ok(()) +} + +/// `.jsonl` with a valid corpus key: a name `run` writes. +fn is_collision_file_name(name: &str) -> bool { + name.strip_suffix(".jsonl") + .is_some_and(|stem| validate_corpus_key(stem).is_ok()) +} + +impl Corpus { + /// Build a corpus from `(name, statement)` rows. Names are trimmed, + /// statement whitespace is collapsed, and rows with an empty side or a + /// duplicate of an earlier row are dropped. Entries are sorted by name + /// then statement; only complete keys enter the shape and skeleton + /// indices. The corpus key is stored without validation. + pub fn from_rows(key: &str, rows: I) -> Self + where + I: IntoIterator, + { + let distinct: BTreeSet<(String, String)> = rows + .into_iter() + .map(|(n, s)| (n.trim().to_string(), collapse_whitespace(&s))) + .filter(|(n, s)| !n.is_empty() && !s.is_empty()) + .collect(); + + let mut keys: Vec = Vec::new(); + let mut key_of: HashMap = HashMap::new(); + let mut entries = Vec::with_capacity(distinct.len()); + for (name, statement) in distinct { + let k = match key_of.get(&statement) { + Some(&k) => k, + None => { + keys.push(canonical::structural_key(&statement)); + key_of.insert(statement.clone(), keys.len() - 1); + keys.len() - 1 + }, + }; + entries.push(Entry { + name, + statement, + key: k, + }); + } + + let mut by_name: BTreeMap> = BTreeMap::new(); + let mut by_fold: BTreeMap> = BTreeMap::new(); + let mut by_shape: BTreeMap> = BTreeMap::new(); + let mut by_statement: BTreeMap> = BTreeMap::new(); + let mut by_skeleton: BTreeMap> = BTreeMap::new(); + for (i, e) in entries.iter().enumerate() { + by_name.entry(e.name.clone()).or_default().push(i); + by_statement.entry(e.statement.clone()).or_default().push(i); + // An anonymous name (`_`) folds to the empty string. It is indexed + // like any other: `is_generic` and `--keep-generic` decide whether + // it joins, and the other joins already treat it as a shared name. + let folded = fold_name(&e.name); + by_fold.entry(folded).or_default().insert(e.name.clone()); + // Only a complete parse can stand for its statement in a join; + // an incomplete shape is a prefix that other statements share. + let k = &keys[e.key]; + if !k.complete { + continue; + } + if k.tier == KeyTier::Structural { + by_shape.entry(k.key.clone()).or_default().push(i); + } + if !k.skeleton.is_empty() { + by_skeleton + .entry(k.skeleton_key.clone()) + .or_default() + .push(i); + } + } + + Corpus { + key: key.to_string(), + entries, + keys, + lines_read: 0, + lines_malformed: 0, + lines_without_statement: 0, + by_name, + by_statement, + by_fold, + by_shape, + by_skeleton, + } + } + + /// Load `training_dir/proof_states_.jsonl`, reading each line's + /// `theorem` and `goal` strings. Blank lines are ignored. Malformed JSON + /// increments `lines_malformed`; valid JSON without non-empty string + /// fields increments `lines_without_statement`. + /// + /// # Errors + /// + /// The key fails [`validate_corpus_key`], or the file is missing, + /// unreadable, not UTF-8, or holds no usable row. Invalid rows are + /// counted and skipped rather than causing an error individually. + pub fn load(training_dir: &Path, key: &str) -> Result { + validate_corpus_key(key)?; + let path = training_dir.join(format!("proof_states_{key}.jsonl")); + let file = File::open(&path).with_context(|| format!("open {}", path.display()))?; + let reader = BufReader::new(file); + let mut rows = Vec::new(); + let (mut read, mut malformed, mut without) = (0usize, 0usize, 0usize); + for line in reader.lines() { + let line = line.with_context(|| format!("read {}", path.display()))?; + if line.trim().is_empty() { + continue; + } + read += 1; + let value: serde_json::Value = match serde_json::from_str(&line) { + Ok(v) => v, + Err(_) => { + malformed += 1; + continue; + }, + }; + let field = |f: &str| value.get(f).and_then(serde_json::Value::as_str); + match (field("theorem"), field("goal")) { + (Some(t), Some(g)) if !t.trim().is_empty() && !g.trim().is_empty() => { + rows.push((t.to_string(), g.to_string())); + }, + _ => without += 1, + } + } + let mut corpus = Corpus::from_rows(key, rows); + if corpus.entries.is_empty() { + bail!("{}: no usable (theorem, goal) rows", path.display()); + } + corpus.lines_read = read; + corpus.lines_malformed = malformed; + corpus.lines_without_statement = without; + Ok(corpus) + } + + /// Look up the canonical key for an index into `entries`. + /// + /// # Panics + /// + /// Panics if `i` is outside `entries`. + fn key_of(&self, i: usize) -> &StructuralKey { + &self.keys[self.entries[i].key] + } + + /// Distinct names that carry more than one distinct statement. + pub fn homonym_names(&self) -> usize { + self.by_name.values().filter(|v| v.len() > 1).count() + } + + /// How much of the corpus the canonicaliser keyed at each tier, and how + /// often distinct statements share one structural key. Tier counts + /// count `(name, statement)` rows; collisions count distinct statement + /// texts among complete structural keys only. + pub fn coverage(&self) -> Coverage { + let mut tiers = TierCounts::default(); + for e in &self.entries { + let k = &self.keys[e.key]; + match k.tier { + KeyTier::Structural => tiers.structural += 1, + KeyTier::Skeleton => tiers.skeleton += 1, + KeyTier::Text => tiers.text += 1, + } + if k.complete { + tiers.complete += 1; + } + } + let (mut collision_keys, mut collision_statements) = (0usize, 0usize); + for group in self.by_shape.values() { + let texts = self.distinct_statements(group); + if texts > 1 { + collision_keys += 1; + collision_statements += texts; + } + } + Coverage { + schema: COVERAGE_SCHEMA, + scheme: canonical::SCHEME, + corpus: self.key.clone(), + lines_read: self.lines_read, + lines_malformed: self.lines_malformed, + lines_without_statement: self.lines_without_statement, + rows: self.entries.len(), + names: self.by_name.len(), + homonym_names: self.homonym_names(), + tiers, + collision_keys, + collision_statements, + } + } + + /// Count distinct statement texts at these entry indices, regardless of name. + fn distinct_statements(&self, group: &[usize]) -> usize { + group + .iter() + .map(|&i| self.entries[i].statement.as_str()) + .collect::>() + .len() + } + + /// Sample at most `limit` complete structural keys shared by distinct + /// statements. Take up to `limit / 2` from the largest groups (trivial + /// shapes), then fill remaining places from groups of exactly two + /// (where a false merge is easiest to read), without repeating a key. + /// Each group lists at most six distinct statements. The result may be + /// shorter than `limit` if too few eligible groups remain. + pub fn collisions(&self, limit: usize) -> Vec { + let mut multi: Vec<(&String, &Vec, usize)> = self + .by_shape + .iter() + .map(|(k, g)| (k, g, self.distinct_statements(g))) + .filter(|(_, _, n)| *n > 1) + .collect(); + let mut picked: Vec<(&String, &Vec, usize)> = Vec::new(); + let mut largest = multi.clone(); + largest.sort_by(|x, y| y.2.cmp(&x.2).then_with(|| x.0.cmp(y.0))); + picked.extend(largest.into_iter().take(limit / 2)); + multi.retain(|(k, _, n)| *n == 2 && !picked.iter().any(|(pk, _, _)| pk == k)); + picked.extend(multi.into_iter().take(limit - picked.len().min(limit))); + + picked + .into_iter() + .map(|(key, group, n)| { + let mut seen = BTreeSet::new(); + let members = group + .iter() + .filter(|&&i| seen.insert(self.entries[i].statement.clone())) + .take(6) + .map(|&i| Member { + name: self.entries[i].name.clone(), + statement: self.entries[i].statement.clone(), + }) + .collect(); + CollisionRecord { + schema: COLLISION_SCHEMA, + scheme: canonical::SCHEME, + corpus: self.key.clone(), + key: key.clone(), + shape: self.key_of(group[0]).shape.clone(), + distinct_statements: n, + members, + } + }) + .collect() + } +} + +/// Entries keyed at each canonicalisation tier, and how many of them the +/// parser read completely ([`StructuralKey::complete`]). +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct TierCounts { + pub structural: usize, + pub skeleton: usize, + pub text: usize, + pub complete: usize, +} + +/// Per-corpus parse coverage and key-collision counts. +#[derive(Debug, Clone, Serialize)] +pub struct Coverage { + pub schema: &'static str, + pub scheme: &'static str, + pub corpus: String, + pub lines_read: usize, + pub lines_malformed: usize, + pub lines_without_statement: usize, + /// Distinct `(name, statement)` rows. + pub rows: usize, + pub names: usize, + /// Names with more than one distinct statement. + pub homonym_names: usize, + pub tiers: TierCounts, + /// Structural keys shared by two or more distinct statement texts: + /// alpha-variants of one statement, or distinct statements the scheme + /// cannot tell apart. + pub collision_keys: usize, + /// Distinct statements inside those keys. + pub collision_statements: usize, +} + +/// One name and statement inside a sampled collision group. +#[derive(Debug, Clone, Serialize)] +pub struct Member { + pub name: String, + pub statement: String, +} + +/// A structural key that distinct statements share, for review. +#[derive(Debug, Clone, Serialize)] +pub struct CollisionRecord { + pub schema: &'static str, + pub scheme: &'static str, + pub corpus: String, + pub key: String, + pub shape: String, + pub distinct_statements: usize, + pub members: Vec, +} + +/// How a candidate pair was found. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Join { + /// The same theorem name in both corpora. + NameExact, + /// Names equal after [`fold_name`] but not before. + NameFolded, + /// Different names, identical statement text. Needs no canonicaliser, + /// so it also finds synonyms among statements `dk-shape-v1` cannot read. + Text, + /// Different names, the same structural key. + Shape, + /// Different names, the same skeleton key and a different structural key. + Skeleton, +} + +/// The strongest tier at which a pair's statements agree. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Candidate { + /// Identical text after whitespace collapsing. + CognateExact, + /// Different text, the same structural key: equal up to variable names + /// and the spellings `dk-shape-v1` normalises. + CognateShape, + /// Only the skeleton keys agree: the statements differ in binders or + /// sorts. For a name join this is a specialisation candidate. + CognateSkeleton, + /// Both statements parsed completely and no key agrees: a false friend + /// or a specialisation the scheme cannot see. Only a probe or a kernel + /// can tell which. + Differs, + /// The texts differ and at least one side did not parse completely, so + /// the keys say nothing either way. + Unparsed, +} + +/// One side of a candidate pair. +#[derive(Debug, Clone, Serialize)] +pub struct Side { + pub corpus: String, + pub name: String, + pub statement: String, + /// `structural`, `skeleton` or `text`: how far the canonicaliser got. + pub tier: &'static str, + /// Whether the canonicaliser read the whole statement; when `false` the + /// shape is a prefix and takes no part in shape classification. + pub complete: bool, + /// The canonical shape at that tier (normalised text for `text`). + pub shape: String, +} + +/// One review candidate. Never evidence: `evidence` is always `none`. +#[derive(Debug, Clone, Serialize)] +pub struct CandidateRecord { + pub schema: &'static str, + /// UUIDv8 content id of the statement pair (see the module docs). + pub id: String, + pub scheme: &'static str, + pub join: Join, + pub candidate: Candidate, + pub a: Side, + pub b: Side, + /// Jaccard similarity, in thousandths, of the two shapes' constant and + /// operator atoms (variables `v0`, `v1`, … and `PI` excluded). A ranking + /// aid for review, not a measure of sameness. + pub similarity_permille: u32, + /// The shared name is generic (only with `--keep-generic`). + pub generic_name: bool, + pub evidence: LexiconEvidence, +} + +/// Counts of candidates by classification. +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct CandidateCounts { + pub cognate_exact: usize, + pub cognate_shape: usize, + pub cognate_skeleton: usize, + pub differs: usize, + pub unparsed: usize, +} + +impl CandidateCounts { + /// Count one emitted candidate in its classification. + fn add(&mut self, c: Candidate) { + match c { + Candidate::CognateExact => self.cognate_exact += 1, + Candidate::CognateShape => self.cognate_shape += 1, + Candidate::CognateSkeleton => self.cognate_skeleton += 1, + Candidate::Differs => self.differs += 1, + Candidate::Unparsed => self.unparsed += 1, + } + } + + /// Count candidates across all classifications, including `unparsed`. + pub fn total(&self) -> usize { + self.cognate_exact + + self.cognate_shape + + self.cognate_skeleton + + self.differs + + self.unparsed + } +} + +/// Candidate counts for each join. +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize)] +pub struct JoinCounts { + pub name_exact: CandidateCounts, + pub name_folded: CandidateCounts, + pub text: CandidateCounts, + pub shape: CandidateCounts, + pub skeleton: CandidateCounts, +} + +impl JoinCounts { + /// Count one candidate under the join that emitted it and its classification. + fn add(&mut self, join: Join, c: Candidate) { + match join { + Join::NameExact => self.name_exact.add(c), + Join::NameFolded => self.name_folded.add(c), + Join::Text => self.text.add(c), + Join::Shape => self.shape.add(c), + Join::Skeleton => self.skeleton.add(c), + } + } +} + +/// What one pair scan found and what it skipped. +#[derive(Debug, Clone, Serialize)] +pub struct PairSummary { + pub schema: &'static str, + pub scheme: &'static str, + pub pair: [String; 2], + /// Folded names present in both corpora. + pub folded_names_shared: usize, + /// Of those, the generic ones not emitted (see [`is_generic`]). + pub generic_names_skipped: usize, + /// Raw-name pairs whose statement cross product exceeded the cap. + pub name_pairs_capped: usize, + /// Statement pairs inside those capped name pairs. + pub statement_pairs_capped: usize, + /// Identical-text groups over the size cap on either side, or too short + /// (fewer than three tokens) to join two names on. + pub text_groups_capped: usize, + pub text_groups_uninformative: usize, + /// Shape or skeleton groups over the size cap on either side. + pub shape_groups_capped: usize, + pub skeleton_groups_capped: usize, + /// Shape or skeleton groups shared by both corpora but skipped as too + /// little structure for a synonym (see [`informative`]). + pub shape_groups_uninformative: usize, + pub skeleton_groups_uninformative: usize, + pub candidates: JoinCounts, +} + +/// Limits that keep a scan's output reviewable. +#[derive(Debug, Clone)] +pub struct ScanOptions { + /// Emit pairs whose shared name is generic. + pub keep_generic: bool, + /// Skip a shared name whose statement cross product exceeds this. + pub max_pairs_per_name: usize, + /// Skip a shape or skeleton group larger than this on either side. + pub max_shape_group: usize, +} + +impl Default for ScanOptions { + /// Skip generic name joins; cap name cross products at 64 pairs and + /// text, shape and skeleton groups at eight entries per corpus. + fn default() -> Self { + ScanOptions { + keep_generic: false, + max_pairs_per_name: 64, + max_shape_group: 8, + } + } +} + +/// Distinct shape atoms for similarity, excluding `PI` and numbered variables. +fn atoms(shape: &str) -> BTreeSet<&str> { + shape + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + .filter(|t| !t.is_empty() && *t != "PI") + .filter(|t| { + !(t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())) + }) + .collect() +} + +/// Canonical sort atoms (`dk-shape-v1`'s `sort_of`) plus `ARROW`: the type +/// language. A shape made only of these and variables is a bare signature. +const TYPE_ATOMS: [&str; 9] = [ + "ARROW", "NAT", "INT", "BOOL", "REAL", "TYPE", "STRING", "LIST", "VEC", +]; + +/// `dk-shape-v1`'s canonical operators other than `ARROW`: the marks of a +/// statement rather than a type. +const NON_TYPE_OPERATORS: [&str; 17] = [ + "ADD", "MUL", "SUB", "DIV", "MOD", "EQ", "NEQ", "LT", "LE", "GT", "GE", "AND", "OR", "NOT", + "IFF", "IN", "APPEND", +]; + +/// Whether a skeleton carries enough structure to propose a synonym between +/// two *differently named* statements: at least three non-variable atoms, +/// at least one of them outside the type language, and no variable applied +/// to arguments. `dk-shape-v1` renames any short lower-case name to a +/// variable, so `cos 0 = 1`, `exp 0 = 1` and `n 0 = 1` all become +/// `(EQ (v0 0) 1)`; a variable in function position is the mark of that. +/// A bare `(summable v0)` says only that something is summable, and a bare +/// signature such as `int -> int -> int` is shared by every function of +/// that type. So is `Tree -> Tree -> Tree`, whose type is not a canonical +/// sort: a shape with arrows, no variables and no operator besides `ARROW` +/// is a signature whatever its type names. Name joins are not filtered: +/// there the shared name anchors. +pub fn informative(skeleton: &str) -> bool { + let chars: Vec = skeleton.chars().collect(); + let variable_head = chars.windows(3).enumerate().any(|(i, w)| { + w[0] == '(' && w[1] == 'v' && w[2].is_ascii_digit() && { + let rest = &chars[i + 2..]; + let digits = rest.iter().take_while(|c| c.is_ascii_digit()).count(); + matches!(rest.get(digits), Some(' ')) + } + }); + let constants: Vec<&str> = skeleton + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + // `?` is an erased sort and `_` a hole: placeholders, not atoms. + .filter(|t| !t.is_empty() && !matches!(*t, "PI" | "?" | "_")) + .filter(|t| { + !(t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())) + }) + .collect(); + let beyond_types = constants.iter().any(|t| !TYPE_ATOMS.contains(t)); + let has_variable = skeleton + .split(|c: char| c.is_whitespace() || matches!(c, '(' | ')' | '[' | ']')) + .any(|t| t.len() > 1 && t.starts_with('v') && t[1..].chars().all(|c| c.is_ascii_digit())); + let bare_signature = !has_variable + && constants.contains(&"ARROW") + && !constants.iter().any(|t| NON_TYPE_OPERATORS.contains(t)); + !variable_head && constants.len() >= 3 && beyond_types && !bare_signature +} + +/// Jaccard similarity of the shapes' non-variable atoms in thousandths, +/// rounded down. Return zero when both atom sets are empty. +fn similarity_permille(a: &str, b: &str) -> u32 { + let (sa, sb) = (atoms(a), atoms(b)); + let union = sa.union(&sb).count(); + if union == 0 { + return 0; + } + (sa.intersection(&sb).count() * 1000 / union) as u32 +} + +/// Prefer identical text, then matching structural and skeleton keys. +/// Differing texts with either key incomplete are `Unparsed` regardless +/// of key equality; complete statements with no match are `Differs`. +fn classify(a: &Entry, ka: &StructuralKey, b: &Entry, kb: &StructuralKey) -> Candidate { + if a.statement == b.statement { + return Candidate::CognateExact; + } + // `complete` is false at the text tier, so this also covers unparsed text. + if !ka.complete || !kb.complete { + return Candidate::Unparsed; + } + if ka.tier == KeyTier::Structural && kb.tier == KeyTier::Structural && ka.key == kb.key { + return Candidate::CognateShape; + } + if !ka.skeleton.is_empty() && ka.skeleton_key == kb.skeleton_key { + return Candidate::CognateSkeleton; + } + Candidate::Differs +} + +#[derive(Serialize)] +struct IdSide<'s> { + corpus: &'s str, + name: &'s str, + statement: &'s str, +} + +#[derive(Serialize)] +struct IdPair<'s> { + a: IdSide<'s>, + b: IdSide<'s>, +} + +/// The order-independent UUIDv8 content id of a statement pair. Each tuple +/// contains the corpus key, theorem name and statement text, used verbatim +/// without name folding or whitespace normalisation. +/// +/// # Errors +/// +/// Propagates errors from JCS serialisation in [`crate::ids::content_id`]. +pub fn pair_id( + (ca, na, sa): (&str, &str, &str), + (cb, nb, sb): (&str, &str, &str), +) -> Result { + let x = IdSide { + corpus: ca, + name: na, + statement: sa, + }; + let y = IdSide { + corpus: cb, + name: nb, + statement: sb, + }; + let pair = if (ca, na, sa) <= (cb, nb, sb) { + IdPair { a: x, b: y } + } else { + IdPair { a: y, b: x } + }; + Ok(crate::ids::content_id(&pair)?.to_string()) +} + +/// Copy an indexed corpus entry and its canonicalisation status into a candidate side. +fn side(c: &Corpus, i: usize) -> Side { + let e = &c.entries[i]; + let k = c.key_of(i); + Side { + corpus: c.key.clone(), + name: e.name.clone(), + statement: e.statement.clone(), + tier: k.tier.as_str(), + complete: k.complete, + shape: k.shape.clone(), + } +} + +/// Build a candidate for the indexed entries with the supplied join and +/// classification, atom similarity and `None` evidence. +/// +/// # Errors +/// +/// Propagates content-id serialisation errors from [`pair_id`]. +fn record( + a: &Corpus, + ia: usize, + b: &Corpus, + ib: usize, + join: Join, + candidate: Candidate, + generic_name: bool, +) -> Result { + let (ea, eb) = (&a.entries[ia], &b.entries[ib]); + Ok(CandidateRecord { + schema: CANDIDATE_SCHEMA, + id: pair_id( + (a.key.as_str(), ea.name.as_str(), ea.statement.as_str()), + (b.key.as_str(), eb.name.as_str(), eb.statement.as_str()), + )?, + scheme: canonical::SCHEME, + join, + candidate, + a: side(a, ia), + b: side(b, ib), + similarity_permille: similarity_permille(&a.key_of(ia).shape, &b.key_of(ib).shape), + generic_name, + evidence: LexiconEvidence::None, + }) +} + +/// Scan one corpus pair, passing every candidate to `emit` in a fixed +/// order: name joins by folded name, then text, shape and skeleton joins, +/// each by key. Later joins exclude pairs meeting an earlier join +/// criterion, even if that earlier group was skipped by a limit. Limits +/// skip whole groups rather than truncating them. Shape and skeleton +/// joins require complete keys and an [`informative`] skeleton; text joins +/// require at least three whitespace-separated tokens. +/// +/// Return candidate counts and skipped-group counts. Every emitted record +/// carries `None` evidence. +/// +/// # Errors +/// +/// Propagates errors from `emit` or content-id serialisation, stopping at +/// the first error. Earlier callback side effects are not rolled back. +pub fn scan_pair( + a: &Corpus, + b: &Corpus, + opts: &ScanOptions, + emit: &mut dyn FnMut(&CandidateRecord) -> Result<()>, +) -> Result { + let mut summary = PairSummary { + schema: PAIR_SUMMARY_SCHEMA, + scheme: canonical::SCHEME, + pair: [a.key.clone(), b.key.clone()], + folded_names_shared: 0, + generic_names_skipped: 0, + name_pairs_capped: 0, + statement_pairs_capped: 0, + text_groups_capped: 0, + text_groups_uninformative: 0, + shape_groups_capped: 0, + skeleton_groups_capped: 0, + shape_groups_uninformative: 0, + skeleton_groups_uninformative: 0, + candidates: JoinCounts::default(), + }; + + // 1. Name joins: same folded name. + for (folded, names_a) in &a.by_fold { + let Some(names_b) = b.by_fold.get(folded) else { + continue; + }; + summary.folded_names_shared += 1; + let generic = is_generic(folded); + if generic && !opts.keep_generic { + summary.generic_names_skipped += 1; + continue; + } + // The cap bounds each join per name: exact pairs per raw name, and + // folded pairs across the whole folded group, so many distinct raw + // names that fold together (`list.map`, `option.map`, …) cannot + // each slip under it. + let rows = |c: &Corpus, n: &String| c.by_name[n].len(); + let exact_product: usize = names_a + .iter() + .filter(|n| names_b.contains(*n)) + .map(|n| rows(a, n) * rows(b, n)) + .sum(); + let all_product = names_a.iter().map(|n| rows(a, n)).sum::() + * names_b.iter().map(|n| rows(b, n)).sum::(); + let folded_product = all_product - exact_product; + let folded_capped = folded_product > opts.max_pairs_per_name; + if folded_capped { + summary.name_pairs_capped += 1; + summary.statement_pairs_capped += folded_product; + } + for na in names_a { + for nb in names_b { + let (ga, gb) = (&a.by_name[na], &b.by_name[nb]); + let join = if na == nb { + let product = ga.len() * gb.len(); + if product > opts.max_pairs_per_name { + summary.name_pairs_capped += 1; + summary.statement_pairs_capped += product; + continue; + } + Join::NameExact + } else { + if folded_capped { + continue; + } + Join::NameFolded + }; + for &ia in ga { + for &ib in gb { + let c = + classify(&a.entries[ia], a.key_of(ia), &b.entries[ib], b.key_of(ib)); + summary.candidates.add(join, c); + emit(&record(a, ia, b, ib, join, c, generic)?)?; + } + } + } + } + } + + let same_name = + |ia: usize, ib: usize| fold_name(&a.entries[ia].name) == fold_name(&b.entries[ib].name); + let same_text = |ia: usize, ib: usize| a.entries[ia].statement == b.entries[ib].statement; + + // 2. Text joins: different names, identical statement text. A statement + // of fewer than three tokens (`T`, `x = y`) says too little to join on. + for (text, ga) in &a.by_statement { + let Some(gb) = b.by_statement.get(text) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.text_groups_capped += 1; + continue; + } + if canonical::token_count(text) < 3 { + summary.text_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + if same_name(ia, ib) { + continue; + } + summary.candidates.add(Join::Text, Candidate::CognateExact); + emit(&record( + a, + ia, + b, + ib, + Join::Text, + Candidate::CognateExact, + false, + )?)?; + } + } + } + + // 3. Shape joins: different names, the same structural key, and not + // already joined by text. + for (key, ga) in &a.by_shape { + let Some(gb) = b.by_shape.get(key) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.shape_groups_capped += 1; + continue; + } + if !informative(&a.key_of(ga[0]).skeleton) { + summary.shape_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + if same_name(ia, ib) || same_text(ia, ib) { + continue; + } + let c = classify(&a.entries[ia], a.key_of(ia), &b.entries[ib], b.key_of(ib)); + summary.candidates.add(Join::Shape, c); + emit(&record(a, ia, b, ib, Join::Shape, c, false)?)?; + } + } + } + + // 4. Skeleton joins: different names, the same skeleton key, and not + // already joined by text or shape. + for (key, ga) in &a.by_skeleton { + let Some(gb) = b.by_skeleton.get(key) else { + continue; + }; + if ga.len() > opts.max_shape_group || gb.len() > opts.max_shape_group { + summary.skeleton_groups_capped += 1; + continue; + } + if !informative(&a.key_of(ga[0]).skeleton) { + summary.skeleton_groups_uninformative += 1; + continue; + } + for &ia in ga { + for &ib in gb { + let (ka, kb) = (a.key_of(ia), b.key_of(ib)); + let shape_match = ka.tier == KeyTier::Structural + && kb.tier == KeyTier::Structural + && ka.key == kb.key; + if same_name(ia, ib) || same_text(ia, ib) || shape_match { + continue; + } + let c = classify(&a.entries[ia], ka, &b.entries[ib], kb); + summary.candidates.add(Join::Skeleton, c); + emit(&record(a, ia, b, ib, Join::Skeleton, c, false)?)?; + } + } + } + + Ok(summary) +} + +/// Serialise `value` as one JCS line (RFC 8785 plus a final LF). +/// +/// # Errors +/// +/// Propagates errors from JSON serialisation or JCS canonicalisation. +pub fn jcs_line(value: &T) -> Result> { + let mut bytes = serde_json_canonicalizer::to_vec(value)?; + bytes.push(b'\n'); + Ok(bytes) +} + +/// A whole scan: which pairs, where the corpora are, where output goes. +#[derive(Debug, Clone)] +pub struct RunOptions { + pub training_dir: PathBuf, + pub pairs: Vec<(String, String)>, + pub out: PathBuf, + pub scan: ScanOptions, + /// Collision groups to sample per corpus. + pub collision_samples: usize, +} + +/// What a run produced, for the CLI to print. Timings are reported here and +/// never written into the JCS files, which stay deterministic. +#[derive(Debug, Clone)] +pub struct RunReport { + pub coverage: Vec, + pub pairs: Vec, + pub load_times: Vec<(String, Duration)>, + pub pair_times: Vec<(String, Duration)>, + pub total: Duration, +} + +/// Create or truncate `path`, write each item as a JCS line, then flush. +/// Parent directories must already exist; an empty slice creates an empty file. +/// +/// # Errors +/// +/// Propagates file creation, serialisation, write and flush errors. A +/// failure may leave the file empty or partially written. +fn write_lines(path: &Path, items: &[T]) -> Result<()> { + let mut w = + BufWriter::new(File::create(path).with_context(|| format!("create {}", path.display()))?); + for item in items { + w.write_all(&jcs_line(item)?)?; + } + w.flush()?; + Ok(()) +} + +/// Load every corpus the pairs name (each once), scan each pair, and write +/// `pairs/__.jsonl`, `summary.jsonl`, `coverage.jsonl` and +/// `collisions/.jsonl` under `opts.out`. Return coverage, pair +/// summaries and timings; timings are omitted from the files. +/// +/// Create output directories as needed, remove existing `.jsonl` files +/// directly inside `pairs/` and `collisions/`, and replace the coverage +/// and summary files. Pairs are scanned in the supplied order. +/// +/// # Errors +/// +/// No pairs are supplied, a corpus fails to load, output directories +/// cannot be created or read, an old file cannot be removed, or +/// serialisation, file creation, writing or flushing fails. Output may +/// already have been removed or partially written when an error occurs. +pub fn run(opts: &RunOptions) -> Result { + let started = Instant::now(); + if opts.pairs.is_empty() { + bail!("no corpus pairs to scan: pass --pair A:B or --preset"); + } + let needed: BTreeSet<&str> = opts + .pairs + .iter() + .flat_map(|(a, b)| [a.as_str(), b.as_str()]) + .collect(); + + let mut corpora: BTreeMap = BTreeMap::new(); + let mut load_times = Vec::new(); + for key in needed { + let t = Instant::now(); + let corpus = Corpus::load(&opts.training_dir, key)?; + load_times.push((key.to_string(), t.elapsed())); + corpora.insert(key.to_string(), corpus); + } + + let pairs_dir = opts.out.join("pairs"); + let collisions_dir = opts.out.join("collisions"); + fs::create_dir_all(&pairs_dir).with_context(|| format!("create {}", pairs_dir.display()))?; + fs::create_dir_all(&collisions_dir) + .with_context(|| format!("create {}", collisions_dir.display()))?; + // A re-run over a different pair set must not leave the previous run's + // files beside this run's summary. Only names this command writes are + // removed (`pairs/__.jsonl` and `collisions/.jsonl`, with + // valid corpus keys); anything else in the directory is left alone. + remove_generated(&pairs_dir, is_pair_file_name)?; + remove_generated(&collisions_dir, is_collision_file_name)?; + + let coverage: Vec = corpora.values().map(Corpus::coverage).collect(); + write_lines(&opts.out.join("coverage.jsonl"), &coverage)?; + for c in corpora.values() { + write_lines( + &collisions_dir.join(format!("{}.jsonl", c.key)), + &c.collisions(opts.collision_samples), + )?; + } + + let mut summaries = Vec::new(); + let mut pair_times = Vec::new(); + for (ka, kb) in &opts.pairs { + let t = Instant::now(); + let path = pairs_dir.join(format!("{ka}__{kb}.jsonl")); + let mut w = BufWriter::new( + File::create(&path).with_context(|| format!("create {}", path.display()))?, + ); + let summary = scan_pair(&corpora[ka], &corpora[kb], &opts.scan, &mut |rec| { + w.write_all(&jcs_line(rec)?)?; + Ok(()) + })?; + w.flush()?; + pair_times.push((format!("{ka}:{kb}"), t.elapsed())); + summaries.push(summary); + } + write_lines(&opts.out.join("summary.jsonl"), &summaries)?; + + Ok(RunReport { + coverage, + pairs: summaries, + load_times, + pair_times, + total: started.elapsed(), + }) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn folding_unifies_case_namespace_and_separator() { + assert_eq!(fold_name("nat.add_comm"), "add_comm"); + assert_eq!(fold_name("ADD_COMM"), "add_comm"); + assert_eq!(fold_name("add-comm"), "add_comm"); + assert_eq!(fold_name("Foo::bar"), "bar"); + assert_eq!(fold_name("_x_"), "x"); + } + + #[test] + fn generic_names_are_recognised() { + for g in [ + "lemma", + "lemma_3", + "lemma3", + "aux2", + "th27", + "ex1", + "z", + "anonymous", + "step2'", + ] { + assert!(is_generic(&fold_name(g)), "{g} should be generic"); + } + for n in ["add_comm", "append_assoc", "cos_add", "zip_unzip", "ext"] { + assert!(!is_generic(&fold_name(n)), "{n} should not be generic"); + } + } + + #[test] + fn presets_expand_as_documented() { + assert_eq!(preset_pairs("learning").unwrap().len(), 2); + assert_eq!(preset_pairs("spanning").unwrap().len(), 28); + assert_eq!(preset_pairs("in-family").unwrap().len(), 5); + assert_eq!(preset_pairs("full").unwrap().len(), 33); + assert!(preset_pairs("everything").is_none()); + } + + #[test] + fn anonymous_names_join_only_when_generic_names_are_kept() { + let side = + |key: &str| Corpus::from_rows(key, [("_".to_string(), "x + y = y + x".to_string())]); + let (a, b) = (side("a"), side("b")); + let run = |keep_generic: bool| { + let opts = ScanOptions { + keep_generic, + ..ScanOptions::default() + }; + scan_pair(&a, &b, &opts, &mut |_| Ok(())).unwrap() + }; + let skipped = run(false); + assert_eq!(skipped.generic_names_skipped, 1); + assert_eq!(skipped.candidates.name_exact.total(), 0); + let kept = run(true); + assert_eq!(kept.candidates.name_exact.total(), 1); + } + + #[test] + fn the_name_cap_bounds_a_whole_folded_group() { + // Five raw names per side fold to `add_comm`; each raw pair is one + // statement pair, but together they make 25 folded pairs. + let side = |prefix: &str| { + Corpus::from_rows( + prefix, + (0..5) + .map(|i| { + ( + format!("{prefix}{i}.add_comm"), + format!("x + y = y + x + {i}"), + ) + }) + .chain(std::iter::once(( + "nat.add_comm".to_string(), + "x + y = y + x".to_string(), + ))), + ) + }; + let (a, b) = (side("a"), side("b")); + let opts = ScanOptions { + max_pairs_per_name: 4, + ..ScanOptions::default() + }; + let mut emitted = 0usize; + let s = scan_pair(&a, &b, &opts, &mut |_| { + emitted += 1; + Ok(()) + }) + .unwrap(); + assert_eq!( + s.candidates.name_folded.total(), + 0, + "folded group is capped" + ); + assert_eq!( + s.candidates.name_exact.total(), + 1, + "the exact name still joins" + ); + assert_eq!(s.name_pairs_capped, 1); + // 6 × 6 rows in the folded group, minus the one exact pair + assert_eq!(s.statement_pairs_capped, 35); + assert!(emitted >= 1); + } + + #[test] + fn pair_arguments_are_validated() { + assert_eq!( + parse_pair("hol4:hol_light").unwrap(), + ("hol4".to_string(), "hol_light".to_string()) + ); + assert!(parse_pair("hol4").is_err()); + assert!(parse_pair("hol4:hol4").is_err()); + assert!(parse_pair("../etc:hol4").is_err()); + // `a__b:c` and `a:b__c` would both write pairs/a__b__c.jsonl + assert!(parse_pair("a__b:c").is_err()); + // `a_:b` and `a:_b` would both write pairs/a___b.jsonl + assert!(parse_pair("a_:b").is_err()); + // the shipped `proof_states_2026-03-20.jsonl` corpus + assert!(parse_pair("2026-03-20:lean3").is_ok()); + assert!(parse_pair("a:_b").is_err()); + } + + #[test] + fn similarity_ignores_variables_and_binders() { + assert_eq!( + similarity_permille("(EQ (ADD v0 v1) (ADD v1 v0))", "(EQ (ADD v2 v3) v4)"), + 1000 + ); + assert_eq!( + similarity_permille("(EQ (ADD v0 v1))", "(LE (MUL v0 v1))"), + 0 + ); + assert_eq!(similarity_permille("", ""), 0); + } + + #[test] + fn informative_rejects_variable_heads_and_bare_predicates() { + // `cos 0 = 1` and `n 0 = 1` under dk-shape-v1 + assert!(!informative("(EQ (v0 0) 1)")); + assert!(!informative("(EQ (v0 v1 v2) (v3 v1 v2))")); + assert!(!informative("(summable v0)")); + assert!(informative("(EQ (ADD v0 0) v0)")); + assert!(informative("(LT v0 (2 ^ v0))")); + assert!(informative( + "(EQ (MUL (MUL v0 v1) v2) (MUL v0 (MUL v1 v2)))" + )); + // `v10` in function position is still a variable head + assert!(!informative("(EQ (v10 0) (ADD 1 1))")); + // bare signatures: λProlog `int -> int -> int`, Dedukti `Int -> Int -> Int` + assert!(!informative("(ARROW INT (ARROW INT INT))")); + assert!(!informative("(ARROW (ARROW v0 v0) (ARROW v0 v0))")); + // ...and their skeletons, where sorts render as `?` + assert!(!informative("(ARROW ? (ARROW ? ?))")); + assert!(!informative("(ARROW ? ?)")); + // a signature over type names that are not canonical sorts + assert!(!informative("(ARROW Tree (ARROW Tree Tree))")); + // an implication between predicates of a variable is a statement + assert!(informative("(ARROW (prime v0) (odd v0))")); + assert!(informative("(ARROW (LE v0 v1) (LE (ADD v0 1) (ADD v1 1)))")); + } + + #[test] + fn text_join_counts_lexical_tokens_not_words() { + // one whitespace field, eight tokens: enough to join two names on + assert!(canonical::token_count("f(x)=g(x)") >= 3); + assert!(canonical::token_count("T") < 3); + assert!(canonical::token_count("x = y") >= 3); + } + + #[test] + fn collapsing_whitespace_keeps_the_line_break_that_ends_a_comment() { + let s = "x = y -- note\n \t /\\ y = x "; + assert_eq!(collapse_whitespace(s), "x = y -- note\n/\\ y = x"); + assert_eq!(collapse_whitespace("a \t b"), "a b"); + // the conjunct after the comment still reaches the canonicaliser + let joined = canonical::structural_key(&collapse_whitespace(s)); + let split = canonical::structural_key("x = y /\\ y = x"); + assert_eq!(joined.shape, split.shape); + } + + #[test] + fn cleanup_matches_only_generated_names() { + assert!(is_pair_file_name("hol4__hol_light.jsonl")); + assert!(!is_pair_file_name("notes.jsonl")); + assert!(!is_pair_file_name("hol4__Hol.jsonl")); + assert!(!is_pair_file_name("hol4__hol_light.json")); + assert!(is_collision_file_name("lean3.jsonl")); + assert!(!is_collision_file_name("notes.v2.jsonl")); + assert!(!is_collision_file_name("lean3.txt")); + } + + #[test] + fn pair_ids_ignore_side_order() { + let x = ("hol4", "ADD_COMM", "!m n. m + n = n + m"); + let y = ("hol_light", "ADD_SYM", "!m n. m + n = n + m"); + assert_eq!(pair_id(x, y).unwrap(), pair_id(y, x).unwrap()); + assert_ne!(pair_id(x, y).unwrap(), pair_id(x, x).unwrap()); + } +} diff --git a/src/rust/lib.rs b/src/rust/lib.rs index 3edf88d6..ec514d67 100644 --- a/src/rust/lib.rs +++ b/src/rust/lib.rs @@ -30,6 +30,7 @@ pub mod ids; // The single ID-minting module: UUIDv7 record ids, UUIDv8 content pub mod integrity; pub mod ipc; // L1: Cap'n Proto IPC transport (UDS primary, TCP fallback) pub mod learning; // Continuous self-learning loop (MCTS + self-play + curriculum + daemon) +pub mod lexicon; // Lexicon candidate mining across corpora (echidna lexicon scan) pub mod llm; // Frontier LLM advisor (via BoJ Server) pub mod neural; pub mod parsers; diff --git a/src/rust/main.rs b/src/rust/main.rs index 60f9616d..a2b4ed4c 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -196,6 +196,12 @@ enum Commands { op: CorpusOp, }, + /// Mine lexicon candidates across training corpora (flag-only) + Lexicon { + #[command(subcommand)] + op: LexiconOp, + }, + /// Search proof-design space via simulated annealing Design { #[command(subcommand)] @@ -361,6 +367,40 @@ enum CorpusOp { }, } +#[derive(Subcommand)] +enum LexiconOp { + /// Pair theorem names and canonical statement shapes across training + /// corpora and write review candidates as JCS JSON Lines. Every + /// candidate carries `evidence = none`; `data/synonyms/` is never edited. + Scan { + /// Directory holding `proof_states_.jsonl` files. + #[arg(long, default_value = "training_data")] + training_dir: PathBuf, + /// A corpus pair, `A:B`. Repeatable; combines with `--preset`. + #[arg(long = "pair", value_name = "A:B")] + pairs: Vec, + /// A named pair set: `learning`, `spanning`, `in-family` or `full`. + #[arg(long)] + preset: Option, + /// Output directory (pairs/, collisions/, summary.jsonl, coverage.jsonl). + #[arg(long, default_value = "target/lexicon-scan")] + out: PathBuf, + /// Also emit pairs whose shared name is generic (`lemma3`, `aux`, `ex1`). + #[arg(long)] + keep_generic: bool, + /// Skip a shared name whose statement cross product exceeds this: + /// exact pairs per raw name, folded pairs per whole folded group. + #[arg(long, default_value_t = 64)] + max_pairs_per_name: usize, + /// Skip a shape or skeleton group larger than this on either side. + #[arg(long, default_value_t = 8)] + max_shape_group: usize, + /// Key-collision groups to sample per corpus. + #[arg(long, default_value_t = 40)] + collision_samples: usize, + }, +} + #[derive(Subcommand)] enum DesignOp { /// Run SA over a named design problem. @@ -413,6 +453,7 @@ enum DesignOp { }, } +/// Run the selected CLI command after configuring tracing, colours and output. #[tokio::main] async fn main() -> Result<()> { // Parse CLI arguments @@ -541,6 +582,10 @@ async fn main() -> Result<()> { corpus_command(op, &formatter)?; }, + Commands::Lexicon { op } => { + lexicon_command(op, &formatter)?; + }, + Commands::Design { op } => { design_command(op, &formatter).await?; }, @@ -1324,6 +1369,150 @@ async fn diagnostics_command() -> Result<()> { Ok(()) } +/// Lexicon command - mine cross-corpus candidates for curation. +/// +/// The scan runs on a thread with a large stack: the canonicaliser's parser +/// recurses on nesting depth, and some corpus statements (ACL2 books) nest +/// deeply. Timings go to stderr; the JCS files under `--out` carry none, so +/// two runs over the same data write the same bytes. +/// +/// # Errors +/// +/// An unknown preset, a malformed `--pair`, no pairs at all, a corpus that +/// fails to load, an output directory that cannot be created or read, an +/// old output file that cannot be removed, or a serialisation or output +/// write failure. Also returns an error if the scan thread cannot be +/// spawned or panics. Failed scans may leave partial output. +fn lexicon_command(op: LexiconOp, formatter: &OutputFormatter) -> Result<()> { + use echidna::lexicon::scan::{self, RunOptions, ScanOptions}; + + let LexiconOp::Scan { + training_dir, + pairs, + preset, + out, + keep_generic, + max_pairs_per_name, + max_shape_group, + collision_samples, + } = op; + + let mut all_pairs = Vec::new(); + if let Some(name) = preset.as_deref() { + all_pairs.extend(scan::preset_pairs(name).with_context(|| { + format!("unknown preset `{name}` (learning, spanning, in-family, full)") + })?); + } + for p in &pairs { + let pair = scan::parse_pair(p)?; + // A pair is the same pair in either direction; the first spelling + // requested is the one scanned. + let seen = all_pairs + .iter() + .any(|(a, b)| (a, b) == (&pair.0, &pair.1) || (a, b) == (&pair.1, &pair.0)); + if !seen { + all_pairs.push(pair); + } + } + let opts = RunOptions { + training_dir, + pairs: all_pairs, + out, + scan: ScanOptions { + keep_generic, + max_pairs_per_name, + max_shape_group, + }, + collision_samples, + }; + + let report = std::thread::Builder::new() + .name("lexicon-scan".into()) + .stack_size(512 * 1024 * 1024) + .spawn(move || scan::run(&opts).map(|r| (r, opts.out))) + .context("spawn the scan thread")? + .join() + .map_err(|_| anyhow::anyhow!("the scan thread panicked"))??; + let (report, out) = report; + + if formatter.is_json() { + // One JCS object on stdout; the timings stay on stderr. + let summary = serde_json::json!({ + "coverage": report.coverage, + "pairs": report.pairs, + "out": out.display().to_string(), + "total_ms": u64::try_from(report.total.as_millis()).unwrap_or(u64::MAX), + }); + std::io::Write::write_all(&mut std::io::stdout(), &scan::jcs_line(&summary)?)?; + eprintln!("total: {:.2?}; output in {}", report.total, out.display()); + return Ok(()); + } + + println!( + "{:<14} {:>8} {:>8} {:>6} {:>7} {:>6} {:>6} {:>6} {:>8}", + "corpus", "rows", "names", "hom%", "struct%", "skel%", "text%", "cmpl%", "collide" + ); + for c in &report.coverage { + let pct = |n: usize| 100.0 * n as f64 / c.rows.max(1) as f64; + println!( + "{:<14} {:>8} {:>8} {:>6.1} {:>7.1} {:>6.1} {:>6.1} {:>6.1} {:>8}", + c.corpus, + c.rows, + c.names, + 100.0 * c.homonym_names as f64 / c.names.max(1) as f64, + pct(c.tiers.structural), + pct(c.tiers.skeleton), + pct(c.tiers.text), + pct(c.tiers.complete), + c.collision_keys + ); + } + println!(); + println!( + "{:<26} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>8} {:>7} {:>7} {:>7}", + "pair", + "shared", + "generic", + "capped", + "exact", + "shape", + "skel", + "differs", + "unparsed", + "syn-tx", + "syn-sh", + "syn-sk" + ); + for s in &report.pairs { + let names = [&s.candidates.name_exact, &s.candidates.name_folded]; + let sum = + |f: fn(&scan::CandidateCounts) -> usize| names.iter().map(|c| f(c)).sum::(); + println!( + "{:<26} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>7} {:>8} {:>7} {:>7} {:>7}", + format!("{}:{}", s.pair[0], s.pair[1]), + s.folded_names_shared, + s.generic_names_skipped, + s.name_pairs_capped, + sum(|c| c.cognate_exact), + sum(|c| c.cognate_shape), + sum(|c| c.cognate_skeleton), + sum(|c| c.differs), + sum(|c| c.unparsed), + s.candidates.text.total(), + s.candidates.shape.total(), + s.candidates.skeleton.total() + ); + } + for (corpus, t) in &report.load_times { + eprintln!("load {corpus}: {:.2?}", t); + } + for (pair, t) in &report.pair_times { + eprintln!("scan {pair}: {:.2?}", t); + } + eprintln!("total: {:.2?}; output in {}", report.total, out.display()); + Ok(()) +} + /// Corpus command - ingest, query, or summarise a project corpus. /// /// First adapter is `agda`, targeted at echo-types' Buchholz / Brouwer @@ -1334,6 +1523,8 @@ async fn diagnostics_command() -> Result<()> { /// /// Crossquery prints exact semantic-class and canonical-name matches from /// per-prover tables and, unless `provers_only` is set, cross-prover dictionaries. +/// Identity queries skip declarations whose canonical keys are incomplete +/// and report the number skipped; only complete keys form identity groups. /// /// # Errors /// @@ -1641,6 +1832,9 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { Vec<(String, String)>, ), > = std::collections::BTreeMap::new(); + // A key the canonicaliser did not derive from the whole statement + // is a shared prefix, not an identity (docs/CORPUS.adoc). + let mut skipped_incomplete = 0usize; for entry in &corpus.entries { let matches = everything || entry.qualified.to_lowercase().contains(&needle) @@ -1649,6 +1843,10 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { continue; } let key = echidna::corpus::canonical::structural_key(&entry.statement); + if !key.complete { + skipped_incomplete += 1; + continue; + } let slot = groups .entry(key.key.clone()) .or_insert_with(|| (key, Vec::new())); @@ -1656,8 +1854,21 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { .push((corpus.adapter.clone(), entry.qualified.clone())); } + if skipped_incomplete > 0 { + formatter.info(&format!( + "{skipped_incomplete} matching declaration(s) skipped: the canonicaliser \ + did not read their statement completely, so they carry no identity" + ))?; + } if groups.is_empty() { - formatter.info(&format!("no declarations matching '{}'", pattern))?; + // When every match was skipped, the name is present but carries + // no identity; saying "no declarations" would mislead. + let what = if skipped_incomplete > 0 { + "no completely read declarations" + } else { + "no declarations" + }; + formatter.info(&format!("{what} matching '{}'", pattern))?; return Ok(()); } diff --git a/src/rust/output.rs b/src/rust/output.rs index b897b387..5f70548b 100644 --- a/src/rust/output.rs +++ b/src/rust/output.rs @@ -53,6 +53,11 @@ impl OutputFormatter { Self { format } } + /// Whether output is machine-readable JSON (`--format json`). + pub fn is_json(&self) -> bool { + matches!(self.format, OutputFormat::Json) + } + /// Output a success message pub fn success(&self, message: &str) -> Result<()> { match self.format { diff --git a/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl new file mode 100644 index 00000000..971c31f0 --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_hol4_mini.jsonl @@ -0,0 +1,6 @@ +{"goal":"!m n. m + n = n + m","theorem":"ADD_SYM"} +{"goal":"!x y d. 0 < d /\\ ((x - d) < y) /\\ (y < (x + d)) <=> abs(y - x) < d","theorem":"ABS_BETWEEN"} +{"goal":"FACT 0 = 1","theorem":"FACT_0"} +{"goal":"T","theorem":"lemma"} +{"goal":"F ==> T","theorem":"lemma"} +{"goal":"0 + n = n","theorem":"ADD_0"} diff --git a/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl new file mode 100644 index 00000000..58c332cb --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_hol_light_mini.jsonl @@ -0,0 +1,5 @@ +{"goal":"!m n. m + n = n + m","theorem":"ADD_SYM"} +{"goal":"!x y d. &0 < d /\\ ((x - d) < y) /\\ (y < (x + d)) <=> abs(y - x) < d","theorem":"ABS_BETWEEN"} +{"goal":"FACT 0 = 1","theorem":"FACT"} +{"goal":"~F","theorem":"lemma"} +{"goal":"0 + n = n","theorem":"ADD_0"} diff --git a/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl new file mode 100644 index 00000000..bb9a251a --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_isabelle_mini.jsonl @@ -0,0 +1,8 @@ +{"goal":"(a b : nat) : a + b = b + a","theorem":"add_comm"} +{"goal":"(p q : nat) : p * q = q * p","theorem":"MUL_COMM"} +{"goal":"(n : int) : n + 0 = n","theorem":"add_zero"} +{"goal":"(x : nat) : 0 ^ x = 0","theorem":"pow_zero"} +{"goal":"(x y z : nat) : x * y * z = x * (y * z)","theorem":"times_assoc"} +{"goal":": exp 0 = 1","theorem":"exp_zero"} +{"goal":"(u v : nat) : u = v","theorem":"ext"} +{"goal":"(u v : int) : u * u = v","theorem":"ext"} diff --git a/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl b/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl new file mode 100644 index 00000000..8a61fad0 --- /dev/null +++ b/tests/lexicon_fixtures/scan/proof_states_lean_mini.jsonl @@ -0,0 +1,9 @@ +{"goal":"(x y : nat) : x + y = y + x","theorem":"add_comm"} +{"goal":"(m n : nat) : m * n = n * m","theorem":"nat.mul_comm"} +{"goal":"(n : nat) : n + 0 = n","theorem":"add_zero"} +{"goal":"(x : nat) : x ^ 0 = 1","theorem":"pow_zero"} +{"goal":"(a b c : nat) : a * b * c = a * (b * c)","theorem":"mul_assoc"} +{"goal":": cos 0 = 1","theorem":"cos_zero"} +{"goal":"(a b : nat) : a = b","theorem":"ext"} +{"goal":"(a b : int) : a + 0 = b","theorem":"ext"} +{"goal":"(p q : nat) : p * 1 = q","theorem":"ext"} diff --git a/tests/lexicon_scan_test.rs b/tests/lexicon_scan_test.rs new file mode 100644 index 00000000..764ec669 --- /dev/null +++ b/tests/lexicon_scan_test.rs @@ -0,0 +1,257 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! `echidna lexicon scan` over small fixture corpora +//! (`tests/lexicon_fixtures/scan/proof_states_*.jsonl`). +//! +//! The HOL fixtures are real rows from `training_data/` for the stage-6a +//! pilot pair. `dk-shape-v1` cannot read HOL notation, so the scan must say +//! so (`unparsed`) rather than invent shape matches. The `lean_mini` / +//! `isabelle_mini` fixtures use syntax the scheme reads completely, so every +//! join and classification can be pinned there. + +use std::collections::BTreeSet; +use std::path::{Path, PathBuf}; + +use echidna::lexicon::scan::{ + self, Candidate, CandidateRecord, Corpus, Join, PairSummary, RunOptions, ScanOptions, +}; + +fn fixtures() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).join("tests/lexicon_fixtures/scan") +} + +fn load(key: &str) -> Corpus { + Corpus::load(&fixtures(), key).unwrap_or_else(|e| panic!("{key}: {e:#}")) +} + +fn scan(a: &str, b: &str, opts: &ScanOptions) -> (PairSummary, Vec) { + let (ca, cb) = (load(a), load(b)); + let mut out = Vec::new(); + let summary = scan::scan_pair(&ca, &cb, opts, &mut |r| { + out.push(r.clone()); + Ok(()) + }) + .expect("scan"); + (summary, out) +} + +fn find<'r>(records: &'r [CandidateRecord], a: &str, b: &str) -> &'r CandidateRecord { + records + .iter() + .find(|r| r.a.name == a && r.b.name == b) + .unwrap_or_else(|| panic!("no record for {a} ~ {b}")) +} + +#[test] +fn hol_pilot_pair_is_classified_honestly() { + let (summary, records) = scan("hol4_mini", "hol_light_mini", &ScanOptions::default()); + + // Identical text is a cognate whatever the canonicaliser makes of it. + assert_eq!( + find(&records, "ADD_SYM", "ADD_SYM").candidate, + Candidate::CognateExact + ); + assert_eq!( + find(&records, "ADD_0", "ADD_0").candidate, + Candidate::CognateExact + ); + + // `0 < d` against `&0 < d`: the HOL Light statement is over the reals. + // dk-shape-v1 cannot read `!` binders, so neither side is complete and + // the pair is `unparsed`, not a shape cognate and not `differs`. + let abs = find(&records, "ABS_BETWEEN", "ABS_BETWEEN"); + assert_eq!(abs.candidate, Candidate::Unparsed); + assert!(!abs.a.complete && !abs.b.complete); + + // Different names, identical text: found by the text join although the + // canonicaliser drops HOL's `FACT` as a declaration keyword. + let fact = find(&records, "FACT_0", "FACT"); + assert_eq!(fact.join, Join::Text); + assert_eq!(fact.candidate, Candidate::CognateExact); + + // `lemma` is shared but generic. + assert_eq!(summary.generic_names_skipped, 1); + assert!(!records.iter().any(|r| r.a.name == "lemma")); + + // Nothing in this pair parses completely, so no shape or skeleton join. + assert_eq!(summary.candidates.shape.total(), 0); + assert_eq!(summary.candidates.skeleton.total(), 0); +} + +#[test] +fn every_join_and_class_on_complete_syntax() { + let (summary, records) = scan("lean_mini", "isabelle_mini", &ScanOptions::default()); + + // Same name, alpha-variants. + let add_comm = find(&records, "add_comm", "add_comm"); + assert_eq!(add_comm.join, Join::NameExact); + assert_eq!(add_comm.candidate, Candidate::CognateShape); + + // Names equal only after folding (`nat.mul_comm` / `MUL_COMM`). + let mul_comm = find(&records, "nat.mul_comm", "MUL_COMM"); + assert_eq!(mul_comm.join, Join::NameFolded); + assert_eq!(mul_comm.candidate, Candidate::CognateShape); + + // `nat` against `int`: the skeletons agree, the shapes do not. + let add_zero = find(&records, "add_zero", "add_zero"); + assert_eq!(add_zero.candidate, Candidate::CognateSkeleton); + + // Same name, different statement: a false-friend candidate. + assert_eq!( + find(&records, "pow_zero", "pow_zero").candidate, + Candidate::Differs + ); + + // Different names, the same shape: a synonym candidate. + let assoc = find(&records, "mul_assoc", "times_assoc"); + assert_eq!(assoc.join, Join::Shape); + assert_eq!(assoc.candidate, Candidate::CognateShape); + + // `cos 0 = 1` and `exp 0 = 1` share a dk-shape-v1 key (`cos`/`exp` are + // renamed as variables); the join refuses it as uninformative. + assert!(!records.iter().any(|r| r.a.name == "cos_zero")); + assert!(summary.shape_groups_uninformative >= 1); + + // Homonyms: `ext` has 3 Lean and 2 Isabelle statements, 6 pairs. + let ext = records.iter().filter(|r| r.a.name == "ext").count(); + assert_eq!(ext, 6); + + // Every record is flag-only. + for r in &records { + assert_eq!( + serde_json::to_value(&r.evidence).unwrap(), + serde_json::json!({"kind": "none"}) + ); + } +} + +#[test] +fn homonym_cross_products_over_the_cap_are_counted_not_emitted() { + let opts = ScanOptions { + max_pairs_per_name: 4, + ..ScanOptions::default() + }; + let (summary, records) = scan("lean_mini", "isabelle_mini", &opts); + assert!(!records.iter().any(|r| r.a.name == "ext")); + assert_eq!(summary.name_pairs_capped, 1); + assert_eq!(summary.statement_pairs_capped, 6); +} + +#[test] +fn records_are_jcs_and_ids_ignore_scan_direction() { + let (_, forward) = scan("lean_mini", "isabelle_mini", &ScanOptions::default()); + let (_, backward) = scan("isabelle_mini", "lean_mini", &ScanOptions::default()); + + for r in &forward { + let line = scan::jcs_line(r).unwrap(); + assert_eq!(*line.last().unwrap(), b'\n'); + let body = &line[..line.len() - 1]; + let reparsed: serde_json::Value = serde_json::from_slice(body).unwrap(); + assert_eq!(serde_json_canonicalizer::to_vec(&reparsed).unwrap(), body); + assert_eq!(uuid::Uuid::parse_str(&r.id).unwrap().get_version_num(), 8); + } + + let ids = |rs: &[CandidateRecord]| rs.iter().map(|r| r.id.clone()).collect::>(); + assert_eq!(ids(&forward), ids(&backward)); + assert_eq!(ids(&forward).len(), forward.len(), "ids are unique"); +} + +#[test] +fn a_run_writes_the_same_bytes_twice() { + let base = std::env::temp_dir().join(format!("echidna-lexicon-scan-{}", std::process::id())); + let run_into = |dir: &str| { + let out = base.join(dir); + let report = scan::run(&RunOptions { + training_dir: fixtures(), + pairs: vec![ + ("lean_mini".into(), "isabelle_mini".into()), + ("hol4_mini".into(), "hol_light_mini".into()), + ], + out: out.clone(), + scan: ScanOptions::default(), + collision_samples: 10, + }) + .expect("run"); + assert_eq!(report.pairs.len(), 2); + assert_eq!(report.coverage.len(), 4); + out + }; + let (one, two) = (run_into("one"), run_into("two")); + for file in [ + "summary.jsonl", + "coverage.jsonl", + "pairs/lean_mini__isabelle_mini.jsonl", + "pairs/hol4_mini__hol_light_mini.jsonl", + "collisions/lean_mini.jsonl", + ] { + let (x, y) = ( + std::fs::read(one.join(file)).unwrap(), + std::fs::read(two.join(file)).unwrap(), + ); + assert_eq!(x, y, "{file} differs between runs"); + } + let _ = std::fs::remove_dir_all(&base); +} + +#[test] +fn unknown_corpus_keys_fail_loudly() { + assert!(Corpus::load(&fixtures(), "no_such_corpus").is_err()); + assert!(Corpus::load(&fixtures(), "../etc").is_err()); +} + +#[test] +fn a_rerun_with_fewer_pairs_leaves_no_stale_pair_files() { + let out = std::env::temp_dir().join(format!("echidna-lexicon-rerun-{}", std::process::id())); + let run_with = |pairs: Vec<(String, String)>| { + scan::run(&RunOptions { + training_dir: fixtures(), + pairs, + out: out.clone(), + scan: ScanOptions::default(), + collision_samples: 10, + }) + .expect("run") + }; + run_with(vec![ + ("lean_mini".into(), "isabelle_mini".into()), + ("hol4_mini".into(), "hol_light_mini".into()), + ]); + run_with(vec![("lean_mini".into(), "isabelle_mini".into())]); + let listed = |dir: &str| { + let mut names: Vec = std::fs::read_dir(out.join(dir)) + .unwrap() + .map(|e| e.unwrap().file_name().to_string_lossy().into_owned()) + .collect(); + names.sort(); + names + }; + assert_eq!(listed("pairs"), vec!["lean_mini__isabelle_mini.jsonl"]); + assert_eq!( + listed("collisions"), + vec!["isabelle_mini.jsonl", "lean_mini.jsonl"] + ); + let _ = std::fs::remove_dir_all(&out); +} + +#[test] +fn the_global_json_format_prints_one_parseable_object() { + let out = tempfile::tempdir().expect("tempdir"); + let run = std::process::Command::new(env!("CARGO_BIN_EXE_echidna")) + .args(["--format", "json", "lexicon", "scan", "--training-dir"]) + .arg(fixtures()) + .args(["--pair", "hol4_mini:hol_light_mini", "--out"]) + .arg(out.path()) + .output() + .expect("run echidna lexicon scan"); + assert!( + run.status.success(), + "{}", + String::from_utf8_lossy(&run.stderr) + ); + let stdout = String::from_utf8(run.stdout).expect("utf-8"); + assert_eq!(stdout.lines().count(), 1, "one JSON line: {stdout}"); + let v: serde_json::Value = serde_json::from_str(&stdout).expect("stdout is JSON"); + assert_eq!(v["pairs"][0]["pair"][0], "hol4_mini"); + assert_eq!(v["coverage"].as_array().map(Vec::len), Some(2)); +}