diff --git a/crates/utopia-core/src/models.rs b/crates/utopia-core/src/models.rs index f4fb8879b..06e1a0b41 100644 --- a/crates/utopia-core/src/models.rs +++ b/crates/utopia-core/src/models.rs @@ -924,6 +924,37 @@ pub struct DerivedFactView { pub premises: Vec, } +/// 证明的一步：一条断言前提，连同它的证据（0002 R2）。 +/// +/// 前提一律是断言（`fact_derivations` 不记派生），所以证明是一条链而不是一棵树： +/// 派生 → 按 `seq` 排好的断言 → 每条断言的原句。叶子就是 chunk。 +#[derive(Debug, Clone, Serialize)] +pub struct ProofStep { + pub seq: i32, + pub fact_id: Uuid, + pub subject_id: Uuid, + pub subject: String, + pub predicate_id: Option, + /// 本体里的关系名；空谓词事实（0010）不参与推导，这里理论上恒有值， + /// 留 Option 是不在读路径上撒谎 + pub predicate: Option, + pub object_id: Option, + pub object: Option, + pub valid_from: Option>, + pub valid_to: Option>, + pub confidence: f32, + /// 这条前提后来被撤了。派生随之失效，但证明还要读得出「当时靠的是什么」 + pub retracted: bool, + pub evidence: Vec, +} + +/// 一条派生事实的完整证明：它本身，加上按顺序展开到原句的前提。 +#[derive(Debug, Clone, Serialize)] +pub struct Proof { + pub derived: DerivedFactView, + pub steps: Vec, +} + /// 审核队列各档的**真实条数**。 /// /// 与列表分开取是有意的：列表有上限（一页十条），数数没有。从前左栏读的是 diff --git a/crates/utopia-server/src/api/graph_routes.rs b/crates/utopia-server/src/api/graph_routes.rs index 48081132e..d693382d9 100644 --- a/crates/utopia-server/src/api/graph_routes.rs +++ b/crates/utopia-server/src/api/graph_routes.rs @@ -228,6 +228,18 @@ pub async fn fact_evidence( Ok(Json(json!({ "evidence": evidence }))) } +/// 一条派生事实的证明（0002 R2）：前提按推导顺序，每条带证据，一路到原句。 +/// 派生已失效或不存在时 `proof` 为 null——不是错误，界面据此退回文本前提 +pub async fn derived_proof( + State(state): State, + AuthUser(user): AuthUser, + Path((kb_id, derived_id)): Path<(Uuid, Uuid)>, +) -> ApiResult> { + require_kb(&state, &user, kb_id, Role::Viewer).await?; + let proof = utopia_store::reasoning::proof(&state.pool, kb_id, derived_id).await?; + Ok(Json(json!({ "proof": proof }))) +} + /// 手动触发抽取（failed 重试 / 补配模型后补抽）。 pub async fn extract( State(state): State, diff --git a/crates/utopia-server/src/api/mod.rs b/crates/utopia-server/src/api/mod.rs index 8818406b2..bb646e08c 100644 --- a/crates/utopia-server/src/api/mod.rs +++ b/crates/utopia-server/src/api/mod.rs @@ -290,6 +290,11 @@ pub fn router(state: AppState, cfg: &AppConfig) -> Router { "/kbs/{id}/facts/{fact_id}/evidence", get(graph_routes::fact_evidence), ) + // 派生事实的证明（0002 R2）：前提按顺序展开到原句 + .route( + "/kbs/{id}/derived/{derived_id}/proof", + get(graph_routes::derived_proof), + ) .route("/kbs/{id}/events", get(events_routes::kb_events)) .route( "/kbs/{id}/sources", diff --git a/crates/utopia-store/src/reasoning.rs b/crates/utopia-store/src/reasoning.rs index a05620784..37c42f54a 100644 --- a/crates/utopia-store/src/reasoning.rs +++ b/crates/utopia-store/src/reasoning.rs @@ -857,6 +857,129 @@ pub async fn mark_inference_ran(pool: &PgPool, kb_id: Uuid) -> AppResult<()> { Ok(()) } +/// 一条派生事实的证明，展开到原句（0002 R2）。 +/// +/// `fact_derivations` 只记直接前提，而前提一律是断言，所以「递归展开」在这里 +/// 退化成一条链：派生 → 按 `seq` 的断言 → 每条断言的证据。叶子是 chunk， +/// 界面上一路点到文档。**撤了的前提照样列出并打上标记**：派生随前提失效， +/// 但「当时靠的是什么」要读得出来，那正是记录轴存在的理由。 +/// +/// 派生已失效或不存在时回 None——不是错误，界面据此收起。 +pub async fn proof( + pool: &PgPool, + kb_id: Uuid, + derived_id: Uuid, +) -> AppResult> { + let Some(derived) = derived_one(pool, kb_id, derived_id).await? else { + return Ok(None); + }; + #[allow(clippy::type_complexity)] + let rows: Vec<( + i32, + Uuid, + Uuid, + String, + Option, + Option, + Option, + Option, + Option>, + Option>, + f32, + bool, + )> = sqlx::query_as( + "SELECT fd.seq, f.id, f.subject_id, s.canonical_name, + f.predicate_id, r.label, f.object_id, o.canonical_name, + f.valid_from, f.valid_to, f.confidence, + f.invalidated_at IS NOT NULL + FROM fact_derivations fd + JOIN facts f ON f.id = fd.premise_fact_id + JOIN entities s ON s.id = f.subject_id + LEFT JOIN relation_types r ON r.id = f.predicate_id + LEFT JOIN entities o ON o.id = f.object_id + WHERE fd.derived_fact_id = $1 + ORDER BY fd.seq", + ) + .bind(derived_id) + .fetch_all(pool) + .await?; + let mut steps = Vec::with_capacity(rows.len()); + for ( + seq, + fact_id, + subject_id, + subject, + predicate_id, + predicate, + object_id, + object, + valid_from, + valid_to, + confidence, + retracted, + ) in rows + { + // 一条链最多 MAX_DEPTH 步，逐条取证据是可数的几次往返 + let evidence = crate::graph::fact_evidence(pool, fact_id).await?; + steps.push(utopia_core::models::ProofStep { + seq, + fact_id, + subject_id, + subject, + predicate_id, + predicate, + object_id, + object, + valid_from, + valid_to, + confidence, + retracted, + evidence, + }); + } + Ok(Some(utopia_core::models::Proof { derived, steps })) +} + +/// 按 id 取一条派生（失效的也取：证明要能回看）。 +async fn derived_one( + pool: &PgPool, + kb_id: Uuid, + derived_id: Uuid, +) -> AppResult> { + Ok(sqlx::query_as( + "SELECT d.id, + d.subject_id, s.canonical_name AS subject, + d.object_id, o.canonical_name AS object, + r.label AS predicate, + ru.kind AS rule, + d.valid_from, d.valid_to, d.confidence, d.derived_at, + COALESCE( + (SELECT array_agg( + ps.canonical_name || ' · ' + || COALESCE(pr.label, '?') || ' · ' + || COALESCE(po.canonical_name, '?') + ORDER BY fd.seq) + FROM fact_derivations fd + JOIN facts pf ON pf.id = fd.premise_fact_id + JOIN entities ps ON ps.id = pf.subject_id + LEFT JOIN relation_types pr ON pr.id = pf.predicate_id + LEFT JOIN entities po ON po.id = pf.object_id + WHERE fd.derived_fact_id = d.id), + ARRAY[]::text[] + ) AS premises + FROM derived_facts d + JOIN entities s ON s.id = d.subject_id + JOIN entities o ON o.id = d.object_id + JOIN relation_types r ON r.id = d.predicate_id + JOIN rules ru ON ru.id = d.rule_id + WHERE d.kb_id = $1 AND d.id = $2", + ) + .bind(kb_id) + .bind(derived_id) + .fetch_optional(pool) + .await?) +} + /// 一条派生事实，配好展示与证明所需的文本（实体面板的「推出来的」那一档）。 /// /// **证明一起取回来**：这一档存在的理由就是「这条边不是谁说的，是这么推出来的」， diff --git a/crates/utopia-store/tests/a_proof_reaches_the_sentence.rs b/crates/utopia-store/tests/a_proof_reaches_the_sentence.rs new file mode 100644 index 000000000..e7139a272 --- /dev/null +++ b/crates/utopia-store/tests/a_proof_reaches_the_sentence.rs @@ -0,0 +1,254 @@ +//! R2：一条派生的证明要能一路读到原句（`docs/decisions/0002`）。 +//! +//! 前提一律是断言（`fact_derivations` 不记派生），所以证明是一条链： +//! 派生 → 按 `seq` 排好的断言 → 每条断言的证据 → chunk。这里守三件事： +//! +//! 1. **顺序对**。`A part_of B`、`B part_of C` 推出 `A part_of C`，证明第一步是 A→B。 +//! 2. **叶子是原句**。每一步带着它的证据，引句就是当初抽出它的那句话。 +//! 3. **撤了的前提照样列出并打标记**。派生随之失效，`proof` 仍能回看当时靠的是什么。 +//! +//! 没有 `UTOPIA_DATABASE_URL` 时跳过而不是失败。自建自拆，绝不碰已有的库。 + +use sqlx::PgPool; +use utopia_store::reasoning; +use uuid::Uuid; + +struct Fixture { + org: Uuid, + kb: Uuid, + part_of: Uuid, + a: Uuid, + b: Uuid, + c: Uuid, + doc: Uuid, + chunk_ab: Uuid, + chunk_bc: Uuid, +} + +async fn seed(pool: &PgPool) -> anyhow::Result { + let (org, ws, kb) = (Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()); + let etype = Uuid::now_v7(); + let part_of = Uuid::now_v7(); + let (a, b, c) = (Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()); + let (src, doc, chunk_ab, chunk_bc) = ( + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + ); + + sqlx::query("INSERT INTO organizations (id, name) VALUES ($1, 'proof-test')") + .bind(org) + .execute(pool) + .await?; + sqlx::query("INSERT INTO workspaces (id, org_id, name) VALUES ($1, $2, 'proof-test')") + .bind(ws) + .bind(org) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO knowledge_bases (id, workspace_id, name, materialize_inferences) + VALUES ($1, $2, 'proof-test', TRUE)", + ) + .bind(kb) + .bind(ws) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO entity_types (id, kb_id, key, label) VALUES ($1, $2, 'thing', 'Thing')", + ) + .bind(etype) + .bind(kb) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO relation_types (id, kb_id, key, label, is_transitive) + VALUES ($1, $2, 'part_of', 'part of', TRUE)", + ) + .bind(part_of) + .bind(kb) + .execute(pool) + .await?; + for (id, name) in [(a, "FarmBeats"), (b, "Azure"), (c, "Microsoft")] { + sqlx::query( + "INSERT INTO entities (id, kb_id, type_id, canonical_name) VALUES ($1, $2, $3, $4)", + ) + .bind(id) + .bind(kb) + .bind(etype) + .bind(name) + .execute(pool) + .await?; + } + sqlx::query("INSERT INTO sources (id, kb_id, name) VALUES ($1, $2, 'proof-test')") + .bind(src) + .bind(kb) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO documents (id, kb_id, source_id, filename, sha256, status) + VALUES ($1, $2, $3, 'press.md', 'proof', 'ready')", + ) + .bind(doc) + .bind(kb) + .bind(src) + .execute(pool) + .await?; + for (id, seq, text) in [ + (chunk_ab, 0i32, "FarmBeats is part of Azure."), + (chunk_bc, 1i32, "Azure is part of Microsoft."), + ] { + sqlx::query( + "INSERT INTO chunks (id, kb_id, document_id, seq, text) VALUES ($1, $2, $3, $4, $5)", + ) + .bind(id) + .bind(kb) + .bind(doc) + .bind(seq) + .bind(text) + .execute(pool) + .await?; + } + Ok(Fixture { + org, + kb, + part_of, + a, + b, + c, + doc, + chunk_ab, + chunk_bc, + }) +} + +/// 一条断言，带一句原文当证据 +async fn asserted( + pool: &PgPool, + f: &Fixture, + subject: Uuid, + object: Uuid, + chunk: Uuid, + quote: &str, +) -> anyhow::Result { + let id = Uuid::now_v7(); + sqlx::query( + "INSERT INTO facts (id, kb_id, subject_id, predicate_id, object_id, confidence) + VALUES ($1, $2, $3, $4, $5, 0.9)", + ) + .bind(id) + .bind(f.kb) + .bind(subject) + .bind(f.part_of) + .bind(object) + .execute(pool) + .await?; + sqlx::query( + "INSERT INTO fact_evidence (fact_id, chunk_id, quote, proposed_predicate, document_id, doc_version) + VALUES ($1, $2, $3, 'part of', $4, 1)", + ) + .bind(id) + .bind(chunk) + .bind(quote) + .bind(f.doc) + .execute(pool) + .await?; + Ok(id) +} + +#[tokio::test] +async fn a_proof_reaches_the_sentence() -> anyhow::Result<()> { + let Ok(url) = std::env::var("UTOPIA_DATABASE_URL") else { + eprintln!("跳过：未设 UTOPIA_DATABASE_URL"); + return Ok(()); + }; + let pool = PgPool::connect(&url).await?; + let f = seed(&pool).await?; + + let run = async { + let ab = asserted( + &pool, + &f, + f.a, + f.b, + f.chunk_ab, + "FarmBeats is part of Azure", + ) + .await?; + let bc = asserted( + &pool, + &f, + f.b, + f.c, + f.chunk_bc, + "Azure is part of Microsoft", + ) + .await?; + reasoning::materialize(&pool, f.kb).await?; + + let derived: Vec = + reasoning::derived_for_entity(&pool, f.kb, f.a).await?; + let ac = derived + .iter() + .find(|d| d.subject_id == f.a && d.object_id == f.c) + .expect("A part_of C should be derived"); + + // 1. 顺序对，2. 叶子是原句 + let proof = reasoning::proof(&pool, f.kb, ac.id) + .await? + .expect("live derivation has a proof"); + assert_eq!(proof.derived.id, ac.id); + assert_eq!(proof.steps.len(), 2); + assert_eq!( + proof.steps[0].fact_id, ab, + "the chain starts where the derivation starts" + ); + assert_eq!(proof.steps[1].fact_id, bc); + assert_eq!(proof.steps[0].subject, "FarmBeats"); + assert_eq!(proof.steps[0].object.as_deref(), Some("Azure")); + assert_eq!(proof.steps[0].predicate.as_deref(), Some("part of")); + assert_eq!(proof.steps[0].evidence.len(), 1); + assert_eq!( + proof.steps[0].evidence[0].quote.as_deref(), + Some("FarmBeats is part of Azure"), + "the leaf of a proof is the sentence it was extracted from" + ); + assert_eq!(proof.steps[0].evidence[0].chunk_id, f.chunk_ab); + assert_eq!(proof.steps[1].evidence[0].chunk_id, f.chunk_bc); + assert!(proof.steps.iter().all(|s| !s.retracted)); + + // 一个不存在的 id 不是错误，是「没有证明」 + assert!(reasoning::proof(&pool, f.kb, Uuid::now_v7()) + .await? + .is_none()); + + // 3. 撤掉一条前提：派生失效，证明还在，且那一步打上标记 + sqlx::query("UPDATE facts SET invalidated_at = now() WHERE id = $1") + .bind(bc) + .execute(&pool) + .await?; + reasoning::materialize(&pool, f.kb).await?; + let (gone,): (bool,) = + sqlx::query_as("SELECT invalidated_at IS NOT NULL FROM derived_facts WHERE id = $1") + .bind(ac.id) + .fetch_one(&pool) + .await?; + assert!(gone, "a derivation falls with its premise"); + let proof = reasoning::proof(&pool, f.kb, ac.id) + .await? + .expect("an invalidated derivation still explains itself"); + assert!(!proof.steps[0].retracted); + assert!( + proof.steps[1].retracted, + "the retracted premise is marked, not hidden" + ); + anyhow::Ok(()) + } + .await; + + let _ = sqlx::query("DELETE FROM organizations WHERE id = $1") + .bind(f.org) + .execute(&pool) + .await; + run +} diff --git a/docs/decisions/0002-reasoning-engine.md b/docs/decisions/0002-reasoning-engine.md index 3dec2e005..976eb23fb 100644 --- a/docs/decisions/0002-reasoning-engine.md +++ b/docs/decisions/0002-reasoning-engine.md @@ -122,7 +122,7 @@ CREATE TABLE fact_derivations ( > 冷启动自动扩本体现在**一位公理都不替人声明**（`Axioms::default()`）：推理机的判据必须是人写下来的。 ### R2 · 解释 -证明树 API + UI。展开到叶子（chunk）为止，中间节点是派生事实与规则。〔**只做了一层**：`derived_for_entity` 把直接前提展开成文本。递归到叶子的 API 与 UI 未建，数据结构已足够支撑。〕 +证明树 API + UI。展开到叶子（chunk）为止，中间节点是派生事实与规则。〔**已做**（0016 B1，`feat/proof-tree`）：`reasoning::proof` + `GET /kbs/{id}/derived/{id}/proof`，实体面板里派生行展开即证明链。**形状是链不是树**——`fact_derivations` 只记断言前提（推导的输入排除派生），所以「递归展开」退化成按 `seq` 的一条链：派生 → 断言 → 各自的证据 → chunk，界面一路点到文档。撤了的前提照样列出并打标记，派生失效后证明仍可回看——记录轴的用法。先前写的「中间节点是派生事实」在这个数据模型里不会出现。〕 ### R3 · 增量维护 diff --git a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md index eca4adf53..02fff13e2 100644 --- a/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md +++ b/docs/decisions/0016-close-the-open-seams-before-cutting-new-ones.md @@ -66,7 +66,7 @@ Chat memory 与 MCP 两处在 A1 / A2 落地前标 in development。中英两份 ### B · 推理机补完——A 之后，与 C 并行 -**B1 · R2 证明树。** 递归展开到叶子 chunk 的 API + 实体面板里可展开的树。数据结构（`fact_derivations`）已够。 +**B1 · R2 证明树。**〔已做，`feat/proof-tree`；实际是链不是树，理由见 0002 R2 的修订〕递归展开到叶子 chunk 的 API + 实体面板里可展开的树。数据结构（`fact_derivations`）已够。 **B2 · 派生 vs 断言矛盾要有信号。** `axiom_violations` 加一种 kind（`derived_contradiction`），进 Review 同一档——0002 写了没做的那一行。 **B3 · `disjointWith` 进消解，合并路径复核签名。** `classify_type_drift` 改从 `entity_type_disjoint` 读（没声明就退回今天的行为，不硬编码）； `merge_entities` 搬事实前跑一遍与写入时相同的 domain / range 检查，违反的进 `axiom_violations` 而不是静默搬过去。这是 0009 与 0012 各自待做的同一件事。 diff --git a/docs/decisions/README.md b/docs/decisions/README.md index ce399d59d..81142c040 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -27,7 +27,7 @@ | | 文档 | 状态 | |---|---|---| | 0001 | [本体导入与治理路线](0001-ontology-import-and-governance.md) | 进行中 · P0–P2c 全建成；P3 按预算落地、P3a 只能手动跑；P3b 建成但形态不同；**P4b/P4c 待做**；P5 已由 0002 落地；判据 2 被 0012 推翻一半 | -| 0002 | [推理机](0002-reasoning-engine.md) | R0 建成（事实层五类含签名、本体自检八类）· R1 建成带开关默认关 · **R2 只一层、R3 未做** · 派生 vs 断言矛盾无信号 | +| 0002 | [推理机](0002-reasoning-engine.md) | R0 建成（事实层五类含签名、本体自检八类）· R1 建成带开关默认关 · R2 证明链到原句（B1）· **R3 未做** · 派生 vs 断言矛盾无信号 | | 0003 | [本体从语料里长出来，人站在哪一环](0003-ontology-growth-loop.md) | 已建成且仍在跑 · 起点已被 0010 与种子退场改写 · 「拒绝有记忆」被 0007 推翻重做 · 新说法提醒待做 | | 0004 | [语言：哪些字跟着看的人走，哪些跟着语料走](0004-language-and-localization.md) | 已建成 · L0–L3 全落地 · 界面刻意不猜浏览器语言 · 「中文内置本体」随播种退场作废 | | 0005 | [告警中心](0005-alert-center.md) | 已建成 · 五种告警 · 三个决定推翻两个（就地留痕）· `no_text_layer` 待接 | diff --git a/web/src/api.ts b/web/src/api.ts index 4b835cad6..9fa6adf77 100644 --- a/web/src/api.ts +++ b/web/src/api.ts @@ -324,6 +324,29 @@ export interface DerivedFact { premises: string[]; } +/** 证明的一步：一条断言前提，带它的证据。前提一律是断言，所以证明是链不是树 */ +export interface ProofStep { + seq: number; + fact_id: string; + subject_id: string; + subject: string; + predicate_id: string | null; + predicate: string | null; + object_id: string | null; + object: string | null; + valid_from: string | null; + valid_to: string | null; + confidence: number; + /** 这条前提后来被撤了；派生随之失效，证明仍要读得出当时靠的是什么 */ + retracted: boolean; + evidence: Evidence[]; +} + +export interface Proof { + derived: DerivedFact; + steps: ProofStep[]; +} + /** 审核页的分档。**与服务端的 queue 参数是同一组字面量**——拼错会拿到 * 一个明确的 unknown_queue 错误，而不是悄悄的空列表。 */ export type ReviewQueue = @@ -1318,6 +1341,12 @@ export const api = { request<{ evidence: Evidence[] }>( `/api/v1/kbs/${kbId}/facts/${factId}/evidence`, ), + /** 一条派生事实的证明（0002 R2）：前提按推导顺序，每条带证据，一路到原句。 + * 派生已失效时回 null——不是错误 */ + derivedProof: (kbId: string, derivedId: string) => + request<{ proof: Proof | null }>( + `/api/v1/kbs/${kbId}/derived/${derivedId}/proof`, + ), documentDetail: (id: string) => request<{ document: Doc; chunks: ChunkFull[] }>(`/api/v1/documents/${id}`), extractDocument: (id: string) => diff --git a/web/src/i18n/en.ts b/web/src/i18n/en.ts index 613c9ad58..c2cce2958 100644 --- a/web/src/i18n/en.ts +++ b/web/src/i18n/en.ts @@ -732,6 +732,10 @@ export const en = { derivedHint: "Edges no one asserted — the engine worked them out from axioms your ontology declares. Each one shows the premises it came from.", derivedNoProof: "The premises are gone.", + /** 证明链（0002 R2）：每一步是一条断言前提，展开到原句 */ + proofStep: (n: number) => `Step ${n}`, + proofRetracted: "since retracted", + proofLoading: "Tracing the proof…", derivedPanel: "Inference", derivedRunAsk: "Re-run inference for the whole base?", derivedRunGo: "Run", diff --git a/web/src/i18n/zh.ts b/web/src/i18n/zh.ts index 14c01d8e0..c5915ed25 100644 --- a/web/src/i18n/zh.ts +++ b/web/src/i18n/zh.ts @@ -674,6 +674,9 @@ export const zh: Strings = { derivedHint: "没有人断言过的边——引擎按本体声明的公理推出来的。每一条都附着它用到的前提。", derivedNoProof: "前提已经不在了。", + proofStep: (n: number) => `第 ${n} 步`, + proofRetracted: "后来撤了", + proofLoading: "正在展开证明…", derivedPanel: "推理", derivedRunAsk: "对整个库重跑一遍推理？", derivedRunGo: "跑", diff --git a/web/src/pages/Graph.tsx b/web/src/pages/Graph.tsx index 1ec96c230..5f32501fa 100644 --- a/web/src/pages/Graph.tsx +++ b/web/src/pages/Graph.tsx @@ -2443,6 +2443,7 @@ function DerivedPanel({ * Relations/Timeline/History 的紧凑行里显得是另一个产品的东西，而且十几条 * 推导堆起来是一面墙。证明是「问了才看」的东西，收进展开区正合适。 */ function DerivedRow({ + kbId, d, otherId, otherName, @@ -2450,6 +2451,7 @@ function DerivedRow({ onToggle, onNavigate, }: { + kbId: string; d: DerivedFact; otherId: string; otherName: string; @@ -2490,23 +2492,91 @@ function DerivedRow({ {d.premises.length} - {/* 证明：前提按推导顺序。**边框与 EvidenceList 同一档**—— - 两者是同一件事的两种形态：一个给出处，一个给推理链 */} - {open && ( -
-
    - {d.premises.map((p, i) => ( -
  1. - {p} -
    2. - ))} -
+ {/* 证明：前提按推导顺序，每条展开到原句（0002 R2）。**边框与 EvidenceList + 同一档**——两者是同一件事的两种形态：一个给出处，一个给推理链 */} + {open && } +
+ ); +} + +/** 一条派生的证明链。展开时才取——证明是「问了才看」的东西。 + * + * 每一步是一条断言前提：三元组在上，它的原句在下，原句可点进文档。 + * 前提被撤过的打标记但不藏：派生随之失效，而「当时靠的是什么」正是记录轴要答的。 + * 取不到（派生已失效）就退回列表里带来的那几行文本，不空着。 */ +function ProofChain({ kbId, d }: { kbId: string; d: DerivedFact }) { + const proof = useQuery({ + queryKey: ["proof", d.id], + queryFn: () => api.derivedProof(kbId, d.id), + }); + const steps = proof.data?.proof?.steps; + return ( +
+ {proof.isPending && ( +

{S.graph.proofLoading}

+ )} + {steps && ( +
    + {steps.map((st) => ( +
  1. +
    + + {S.graph.proofStep(st.seq + 1)} + + + {st.subject} + — {st.predicate ?? "?"} → + {st.object ?? "?"} + + {st.retracted && ( + {S.graph.proofRetracted} + )} +
    +
    + {st.evidence.map((ev) => ( + +
    + {ev.quote ? `“${ev.quote}”` : S.graph.noQuote} +
    +
    + {S.graph.sectionRef(ev.filename, ev.seq + 1)} + {ev.stale && ( + + {S.graph.fromVersion(ev.doc_version)} + + )} +
    + + ))} + {st.evidence.length === 0 && ( +

    {S.graph.noEvidence}

    + )} +
    +
    2. + ))} +
+ )} + {/* 派生已失效、证明取不到：退回列表里带来的那几行文本 */} + {!proof.isPending && !steps && ( +
    + {d.premises.map((p, i) => ( +
  1. + {p} +
    2. + ))} {d.premises.length === 0 && ( -

    - {S.graph.derivedNoProof} -

    +
  2. {S.graph.derivedNoProof}
    3. )} -
+ )} ); @@ -2966,6 +3036,7 @@ function EntityPanel({ return (