curriculum-project-hub/spec/Spec/Courseware/Diagnostic.lean

import Spec.Courseware.Lesson
import Spec.Courseware.Render

/-!
# Diagnostic —— checker 诊断:分类、严重级别、合法 lesson

产品里"站在 Lean 位置"的那个 rule-based checker,语义在此沉淀(ADR-0010)。它对 lesson
提诊断,每条诊断有**分类**(`DiagKind`)与**严重级别**(`Severity`)。本模块:

1. 钉级别类型(二分,ADR-0005)。
2. 钉 7 类诊断各自的含义与级别(ADR-0010),并把"**合法 lesson = 无 error 级诊断**"
   建成判定——这是 ADR-0005 deferred 的"完整合法判定"的回填。
3. 对**模型外设施**型诊断(typst 能否编过、引用悬否、数据合 schema 否),用**抽象谓词 +
   显式实现边界**表示:契约说"存在这样一条诊断、它什么意思、什么级别",但其**真值由
   实现(checker)提供**,不在 Lean 内计算——保持契约诚实(不内嵌 typst 编译器)。
-/

namespace Spec.Courseware

/--
诊断的严重级别(`PINNED` 二分, ADR-0005)。

`error` 阻断(产物不合法),`warning` 不阻断(产物仍可导出,只是有损/有忽略)。更细的
级别(info/hint)未决策,故只二分。
-/
inductive Severity where
  | warning
  | error

/--
诊断的**分类**(`PINNED` 7 类, ADR-0010)。每类含义见下;级别见 `DiagKind.severity`。

按"谁来判定"分三层(ADR-0010 的边界):
- **结构型**(模型自身可判):`partPathMissing` / `unknownKind`。
- **schema / 外部设施型**(判定靠实现 oracle):`missingContentFile` / `schemaViolation`
  / `danglingReference` / `typstCompile`。
- **语义型**(coverage 规则):`renderIgnored`。
-/
inductive DiagKind where
  /-- manifest 的 part 指向不存在的文件夹(或经 `..` 逃出根)。结构型。 -/
  | partPathMissing
  /-- part 声明了未知 kind(含 part 与 element.toml 的 kind 不一致)。结构型。 -/
  | unknownKind
  /-- kind schema 要求的某 `content` 字段缺对应 `<field>.typ`。结构/schema 型。 -/
  | missingContentFile
  /-- 实例数据不合其 kind 的 JSON Schema(标量类型错/缺必填/多余键);亦作 manifest/
      element.toml 畸形的兜底。schema / 外部设施型。 -/
  | schemaViolation
  /-- 引用不解析:越界的相对 import,或悬空的交叉引用。外部设施型。 -/
  | danglingReference
  /-- 拼装出的 typst 源编译失败(语法错、`@ref` 未解析…)。外部设施型。 -/
  | typstCompile
  /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被该 target 忽略。语义型。 -/
  | renderIgnored

/--
每类诊断的**严重级别**(`PINNED`, ADR-0010)。

六类为 `error`(阻断);**唯 `renderIgnored` 为 `warning`**——即 ADR-0005 的种子规则
"缺渲染 ⇒ warning,不阻断导出"。把级别钉成一个全函数,使"哪类阻断、哪类不阻断"成为
契约里可引用、可对齐的事实(实现侧 `DiagCode` 的级别据此对齐)。
-/
def DiagKind.severity : DiagKind → Severity
  | .partPathMissing   => .error
  | .unknownKind       => .error
  | .missingContentFile => .error
  | .schemaViolation   => .error
  | .danglingReference => .error
  | .typstCompile      => .error
  | .renderIgnored     => .warning

/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。

保留为具名常量,使"它是 warning 不是 error"可被实现侧 grep 对齐(实现里同名常量
`RENDER_IGNORED_SEVERITY` 引用本定义)。等价于 `DiagKind.severity .renderIgnored`。 -/
def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity

variable (P : Primitives)

/--
**缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`, ADR-0005/0009)。

成立 ⟺ 存在某 element,其 kind 在 `t` 下未配渲染规则(`covers` 为假,见 `Render`)。这条
是 checker 的**语义型**诊断,级别由 `renderIgnoredSeverity` 钉为 warning。`covers` 已随
ADR-0009 下沉到 target 的 build 规格,但本判定式不变。
-/
def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
  ∃ e ∈ l, ¬ c.covers e.kind t

/-!
## 模型外设施型诊断:抽象谓词 + 实现边界(ADR-0010)

`typstCompile` / `danglingReference` / `schemaViolation`(的 schema-合规面)断言的是
**模型自身无法判定**的事实——要跑 typst 编译器、要跑 schema 校验器。契约因此把它们建成
**抽象谓词**,真值由一个**实现提供的 oracle** 给出。Lean 只说"这条诊断存在、什么意思、
什么级别",**不**在 Lean 内计算其真假。

下面用一个 `Oracle` 结构收口这些实现侧判定。它**不是**要在 Lean 里实现 checker,而是
把"这些事实来自模型外"这件事显式化、类型化:谁想谈论一节 lesson 合不合法,就得先有一个
oracle 提供这些外部判定。
-/

/--
**实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。

收口那些"模型外设施"才能回答的判定。每个字段是一个谓词,**真值由实现(checker)提供**:

- `compiles` —— 该 lesson 在 target `t` 下拼装出的 typst 源能否编译通过(否 ⇒ `typstCompile`)。
- `refsResolve` —— 该 lesson 的引用(相对 import / 交叉引用)是否全部解析(否 ⇒ `danglingReference`)。
- `dataConforms` —— 每个 element 的数据是否合其 kind schema(否 ⇒ `schemaViolation`)。
- `contentFilesPresent` —— schema 要求的 `content` 文件是否齐备(否 ⇒ `missingContentFile`)。

把它们作为参数,正是"显式实现边界":契约能据此**定义**合法性,却不假装自己能算出这些
外部事实。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。
-/
structure Oracle (l : Lesson P) (c : RenderConfig P) where
  /-- target `t` 下拼装源可编译。 -/
  compiles : P.TargetId → Prop
  /-- 引用全部解析。 -/
  refsResolve : Prop
  /-- 每个 element 数据合 schema。 -/
  dataConforms : Prop
  /-- schema 要求的 content 文件齐备。 -/
  contentFilesPresent : Prop

/--
**合法 lesson**(`PINNED`, ADR-0010;回填 ADR-0005 deferred 的"完整合法判定")。

一节 lesson 合法 ⟺ 检查管线产出**零条 error 级诊断**。warning(如 `renderIgnored`)
不影响合法性——带 warning 的 lesson 仍合法、仍可(有损)导出。

这里把"无 error 级诊断"展开为:模型外设施判定(经 `Oracle`)全部为真,**且**每个声明的
target 都编译通过。结构型诊断(part 路径、未知 kind、kind 不一致)由 `cph-model` 在加载
期判定;能走到这一步谈合法性,意味着已加载成功,故此处聚焦 schema/外部设施层。注意
`renderIgnored` 是 warning,**不**进合法性合取——这正是 ADR-0005 种子规则的体现。

`targets` 是该工程文件声明的 target 列表(`RenderConfig.spec t` 非 `none` 者);为保持
本层抽象、不绑定 `TargetId` 的可枚举性,这里用"对所有满足前提的 t"的全称式表达。
-/
def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
  o.refsResolve ∧ o.dataConforms ∧ o.contentFilesPresent ∧
    (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)

end Spec.Courseware