import Spec.Courseware.Model.Primitives
import Spec.Courseware.Export.Artifact

/-!
# Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)

ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。

- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
  *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
  裸字符串表达不了这个 wiring。presentation(编号、样式)住模板里,不在 manifest。
- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only)。
- `assembleMarkdown field` —— 按 parts 顺序把每个 element 的 `field`(markdown content 叶子,
  ADR-0015)拼成**单文件 markdown** 产物。typed 而非 `cat`,因为按 manifest `[[parts]]` 顺序读取 +
  跳过缺失项 + 写到单文件产物路径这件事,框架 own 比裸 shell 稳。

**渲染覆盖**:ADR-0011 废止了 per-target `RenderRule` 载荷——渲染的"how"已移进模板。
契约只保留覆盖声明 `covers`(该 target 渲染哪些 kind),供种子诊断用。

**shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
`run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
内容)。三条边界是真分歧点,故钉契约:
1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
   绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
   因此它**不**进 `Diagnostic` 的 6 类(那 6 类是 lesson 自身的诊断,见 `Check/Diagnostic.lean`),
   而由 build 执行层报告。诊断分类保持 6 类不变(ADR-0013 显式拒绝新增 `ShellStep` 诊断码)。
3. **非-typst target 不过 typst 编译** —— 一个只含 `shell` step 的 target(教具包即此)由
   执行器跑命令,而非走 typst 引擎;`check` 的 compile 阶段跳过它。

**assembleMarkdown step 的执行语义(ADR-0015)。** 与 `shell` 同属"非-typst target":框架 own
读取每个 element 的 `<field>.md`、按 `[[parts]]` 顺序拼接、写到单文件产物路径(产物是 markdown,
不经 typst 引擎)。同 shell 的三条边界:① 只在显式 `build --target` 跑,`check` 不跑;② 装配失败
(如写盘失败、引用图缺失)是 build-过程错误,不入 6 类诊断;③ 非-typst target,`check` 的 compile
阶段跳过它。**单文件产物**(现):装配器注入课程级标题为文档 h1(课程元数据,非 element 内容),
每份 `slides.md`/`transcript.md` 贡献其 `##` part 与 `###` 小节(presentation 在内容里, ADR-0011),
按 `[[parts]]` 顺序拼接(分隔符空行)。**自包含**:装配器扫描产物里的 `![](rel)` 图引用,把引用到的
本地图从工程根按原相对路径复制进产物所在 build 根,使该 build 目录可独立交付;引用图在工程根缺失属
build-过程错误(不入 6 类)。外部 URL(`http(s)://`/`data:`)不复制。结构化 FileTree 产物延后
(待 parts 树形重组, ADR-0015 OPEN)。
-/

namespace Spec.Courseware

variable (P : Primitives)

/-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
inductive Step where
  /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
      注入这件事裸 shell 写不出。 -/
  | typstCompile (template : String)
  /-- shell 逃生口:执行命令 `run`(ADR-0005 (b) 类落这)。**已实现**(ADR-0013):以工程根
      为 cwd 执行,opt-in(只在显式 build 该 target 时跑,`check` 不跑),失败属 build-过程错误
      而非 lesson 诊断。教具包(如 KenKen 交互 HTML 由外部 `kendoku` 生成)即走此 step。 -/
  | shell (run : String)
  /-- 装配 markdown:按 `[[parts]]` 顺序读取每个 element 的 `field`(markdown content 叶子,
      ADR-0015),注入课程 h1 后拼接成**单文件 markdown** 产物,并收集 `![](rel)` 引用的本地图进
      build 根使产物自包含。typed 而非 `cat`:按序读取+跳过缺失+注入标题+写盘+收集图由框架 own。
      **已实现**(ADR-0015):非-typst target(`check` 不跑,失败属 build-过程错误不入 6 类诊断)。
      slides 大纲面 / 逐字稿口播面即走此 step(直接 markdown+KaTeX 撰写,绕开 typst→md 公式转换,
      ADR-0014 R2)。 -/
  | assembleMarkdown (field : String)

/-- 一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。 -/
structure TargetSpec where
  /-- 产物(带字段, ADR-0011)。决定 build 折叠成单文件还是文件树。 -/
  artifact : Artifact
  /-- **有序** build steps。按序执行;MVP 仅一个 `typstCompile`。 -/
  steps : List Step
  /-- **覆盖声明**:`covers k` 表示此 target 渲染 kind `k`。ADR-0011 把旧
      `renders : KindId → Option RenderRule` 降级后的产物——契约只声明"渲染哪些 kind"
      (种子诊断 `renderIgnored` 用),"how"由 `steps` 的模板实现。 -/
  covers : P.KindId → Prop

/-- 渲染配置(`PINNED` target-中心, ADR-0009/0011)。`spec t = none` 表示 target `t`
未声明(不导出);`some s` 给出其 build 规格。 -/
structure RenderConfig where
  /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
  spec : P.TargetId → Option (TargetSpec P)

/-- kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005)。成立
⟺ `t` 已声明(`spec t = some s`)**且** `s.covers k`。为假即"此 kind 在此 target 下不
被渲染"——checker 据此报 warning(见 `Diagnostic.renderIgnored`)。`P` 隐式以便点记法。 -/
def RenderConfig.covers {P : Primitives} (c : RenderConfig P)
    (k : P.KindId) (t : P.TargetId) : Prop :=
  match c.spec t with
  | none => False
  | some s => s.covers k

end Spec.Courseware