import Spec.Courseware.Model.Lesson
import Spec.Courseware.Export.Render

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

产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
编译器)。引用解析(`@ref`、相对 import)不另设诊断:它们都是 typst 编译期失败,归
`typstCompile`(ADR-0012)。版本契约诊断 `cphVersionMismatch`(ADR-0016)是第 7 类。
-/

namespace Spec.Courseware

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

/-- 诊断**分类**(`PINNED` 7 类, ADR-0010,经 ADR-0012 修订为 6 类,经 ADR-0016 增至 7
类)。按"谁来判定"分三层:**结构型**(模型自身可判):`partPathMissing`/`unknownKind`/
`cphVersionMismatch`;**schema/外部设施型**(靠实现 oracle):
`missingContentFile`/`schemaViolation`/`typstCompile`;**语义型**:`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 畸形的兜底。 -/
  | schemaViolation
  /-- 拼装出的 typst 源编译失败:语法错、未解析的交叉引用 `@ref`、越界或缺失的相对
      `import`/`include`(后两者即旧 `danglingReference` 的两种情形——typst 在编译期
      检出,故归此类,ADR-0012)。外部设施型。 -/
  | typstCompile
  /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
  | renderIgnored
  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。**结构型**(加载期
      判)。工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时按**兼容性判
      定**比对自身版本(实现侧 `CARGO_PKG_VERSION`),不相容即产此类。**当前判定为版本
      完全相等才相容**(MVP;后续可放宽为 semver 区间,判定逻辑可逐步修改而不动本分类)。
      `error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
  | cphVersionMismatch

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

/-- 缺渲染诊断的级别 = **warning**(`PINNED`, ADR-0005/0010,**非 error**)。具名常量,
使"它是 warning"可被实现侧 grep 对齐(实现里同名常量 `RENDER_IGNORED_SEVERITY` 引用
本定义)。等价于 `DiagKind.renderIgnored.severity`。 -/
def renderIgnoredSeverity : Severity := DiagKind.renderIgnored.severity

variable (P : Primitives)

/-- **缺渲染诊断**:lesson 在 target `t` 下存在无法渲染的 element(`PINNED`,
ADR-0005/0009)。成立 ⟺ 存在某 element,其 kind 在 `t` 下 `covers` 为假。语义型诊断,
级别 warning。 -/
def renderIgnored (l : Lesson P) (c : RenderConfig P) (t : P.TargetId) : Prop :=
  ∃ e ∈ l, ¬ c.covers e.kind t

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

`typstCompile`/`schemaViolation`(的 schema-合规面)断言的是模型自身无法判定的事实——
要跑 typst 编译器、schema 校验器。契约把它们建成**抽象谓词**,真值由实现提供的 oracle
给出。下面用 `Oracle` 收口这些判定:它不是要在 Lean 里实现 checker,而是把"这些事实
来自模型外"显式化、类型化。
-/

/-- **实现侧判定 oracle**(`PINNED` 实现边界, ADR-0010)。每个字段是一个谓词,真值由
实现(checker)提供。结构型诊断(part 路径、未知 kind)不入此 oracle——那些模型自身可判。 -/
structure Oracle (l : Lesson P) (c : RenderConfig P) where
  /-- target `t` 下拼装源可编译(否 ⇒ `typstCompile`)。**含引用解析**:源能编译即蕴含
      其 `@ref`、相对 import 全部解析(ADR-0012 已把引用诊断并入 `typstCompile`)。 -/
  compiles : P.TargetId → Prop
  /-- 每个 element 数据合 schema(否 ⇒ `schemaViolation`)。 -/
  dataConforms : Prop
  /-- schema 要求的 content 文件齐备(否 ⇒ `missingContentFile`)。 -/
  contentFilesPresent : Prop

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

合法 ⟺ 检查管线产出**零条 error 级诊断**。展开为:模型外设施判定(经 `Oracle`)全为真,
**且**每个声明的 target 都编译通过。结构型诊断由 `cph-model` 在加载期判定;能走到这步
谈合法性意味着已加载成功,故此处聚焦 schema/外部设施层。引用解析不单列——已被
`compiles` 蕴含(ADR-0012)。`renderIgnored` 是 warning,**不**进合取——ADR-0005 种子
规则的体现。`targets` 用全称式表达以不绑定 `TargetId` 的可枚举性。 -/
def Legal (l : Lesson P) (c : RenderConfig P) (o : Oracle P l c) : Prop :=
  o.dataConforms ∧ o.contentFilesPresent ∧
    (∀ t : P.TargetId, (c.spec t).isSome → o.compiles t)

end Spec.Courseware