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

/-!
# Diagnostic —— 产品 checker 的诊断

这个 codebase 是要拿去卖的产品。LLM 辅助操作提效是它的核心卖点之一——但 LLM 判不了
一节课合不合法:它不能真的去跑 typst 编译器、不能可靠地断言一段数据合不合 schema、
也不能可靠地检查文件齐不齐。所以产品里有一个 rule-based checker 来做这件事:它真跑
工具、给确定性的诊断,补上 LLM 判不了的这块。这个 checker 的语义在这里(ADR-0010,
经 ADR-0012、ADR-0016 修订)。它对 lesson 提诊断,每条有一个分类(`DiagKind`)和一
个严重级别(`Severity`)。

注意区分两个"检查":这里的 checker 是**产品功能**——用户把教研工程文件喂给 `cph`,
检查这个工程文件合不合法。它和"开发时 spec 与实现是否一致"是两回事,后者没有自动
闸门,靠核对。

本模块钉三件事:严重级别二分;7 类诊断各自的含义和级别;"合法 lesson = 无 error 级
诊断"这条判定。其中有些诊断是 LLM 判不了、得 checker 真跑工具才能判的(typst 编不编
得过、数据合不合 schema、content 文件齐不齐)——这些用抽象谓词加 `Oracle` 表示:契约
说"存在这条诊断、什么意思、什么级别",真值由 checker 给(契约不在 Lean 里内嵌 typst
编译器去算)。引用解析(`@ref`、相对 import)不单列:它们都是 typst 编译期失败,归
`typstCompile`(ADR-0012)。版本契约 `cphVersionMismatch`(ADR-0016)是第 7 类。
-/

namespace Spec.Courseware

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

/-- 诊断分类(ADR-0010,经 ADR-0012 折并为 6 类、ADR-0016 增至 7 类)。按 checker 怎么判分三层:
    结构型(checker 自己按结构判):`partPathMissing`/`unknownKind`/`cphVersionMismatch`;
    schema/外部工具型(得真跑工具):`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`。后两者 typst 在编译期检出,故归此类(ADR-0012)。外部工具型。 -/
  | typstCompile
  /-- 某被用到的 kind 在某声明的 target 下无渲染规则,该 element 被忽略。语义型。 -/
  | renderIgnored
  /-- 工程文件的 `.cph-version` 与 CLI(cph)版本不相容(ADR-0016)。结构型(加载期判)。
      工程文件根的 `.cph-version` 声明它所面向的 cph 版本;CLI 加载时比对自身版本,不相容
      即产此类。当前判定为版本完全相等才相容(MVP;后续可放宽为 semver 区间,判定逻辑可
      逐步改而不动本分类)。`error` 级——版本不相容的工程文件不应被该 CLI 处理。 -/
  | cphVersionMismatch

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

/-- 缺渲染诊断的级别 = warning(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(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

/-!
## 要真跑工具才能判的诊断:抽象谓词 + Oracle

诊断分两类(按 checker 怎么判):有些 checker 自己按工程文件结构就能判(part 路径
在不在、kind 知不知道、某 kind 在某 target 下有没有被覆盖);有些 checker 自己也判
不了,得真跑外部工具——typst 编不编得过(要跑 typst 编译器)、数据合不合 schema(要
跑 schema 校验器)、content 文件齐不齐(要看磁盘)。后者就是 `Oracle` 收口的。

`Oracle` 把这些"得 checker 委托外部工具才能判"的事实建成抽象谓词,真值由 checker 给。
它不是要在 Lean 里实现 checker,而是把"这几件事 checker 自己算不了、得委托出去"显式
表达、类型化。它只收 Legal 需要的、得委托外部工具的事实;checker 自己能判的(如
`renderIgnored`)不进 Oracle。

(这两类 checker 都判得了;但 LLM 两类都判不了——这正是产品里要有个 rule-based
checker 的理由,见本模块顶部。)
-/

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

/-- 合法 lesson(ADR-0010)。合法 ⟺ 检查管线产出零条 error 级诊断。展开为:得委托外部
    工具的判定(经 `Oracle`)全为真,且每个声明的 target 都编译通过。checker 自己按结构
    能判的诊断(part 路径、未知 kind)在加载期已判;能走到这步谈合法性意味着那些已过,
    故此处聚焦 schema/外部工具层。`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