import Spec.Courseware.Primitives
import Spec.Courseware.Artifact

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

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

- `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
  *typed* 而非裸 shell,正因框架要把 **manifest 注入**模板(经 `--input manifest=…`),
  裸 `typst compile` 字符串表达不了这个 wiring。presentation(numbly 编号、样式)住在
  模板里,**不**在 manifest。
- `shell run` —— 逃生口,给难以声明的步骤(ADR-0005 的 (b) 类 medium-only:HTML 交互、
  npm build 落这)。

MVP 每个 target 只有一个 `typstCompile` step,但 `steps` 是 **list**,因为 `FileTree` /
第三方 build 会需要多步。

**渲染覆盖**:ADR-0011 废止了 per-target 的 `RenderRule` 载荷——渲染的"how"已移进模板。
契约只保留**覆盖声明** `covers : KindId → Prop`(该 target 渲染哪些 kind),供种子诊断用;
模板是其实现。`RenderConfig.covers`/`renderIgnored` 据此,ADR-0005 种子规则不变。
-/

namespace Spec.Courseware

variable (P : Primitives)

/--
一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。

- `typstCompile (template)` —— 编译模板文件(相对工程根的路径)成产物;框架把 manifest
  注入它。**typed** 的理由:注入这件事裸 shell 写不出。
- `shell (run)` —— 逃生口,执行 `run` 命令(ADR-0005 的 (b) 类落这)。MVP 不实现,先建结构。

**刻意不**把模板内部、shell 命令的解析结构写进来:那是实现细节(ADR-0011 OPEN)。此处只钉
"step 是有类型操作,目前两型,可扩展"这一骨架。
-/
inductive Step where
  /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。 -/
  | typstCompile (template : String)
  /-- shell 逃生口:执行命令 `run`。 -/
  | shell (run : String)

/--
一个 export target 的 build 规格(`PINNED` artifact + 有序 steps, ADR-0011)。

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

/--
渲染配置(`PINNED` target-中心, ADR-0009/0011)。

`spec t = none` 表示 target `t` **未声明**(此工程文件不导出该 target);`some s` 给出该
target 的 build 规格 `s`(artifact + steps + 覆盖声明)。
-/
structure RenderConfig where
  /-- target ↦ 该 target 的 build 规格(未声明则 `none`)。 -/
  spec : P.TargetId → Option (TargetSpec P)

/--
kind `k` 在 target `t` 下**被渲染**(`PINNED`, ADR-0009/0011;承接 ADR-0005 `covers`)。

成立 ⟺ target `t` 已声明(`spec t = some s`)**且**其覆盖声明含 `k`(`s.covers k`)。
`covers` 为假即"此 kind 在此 target 下不被渲染"——checker 据此报 warning(见
`Spec.Courseware.Diagnostic.renderIgnored`)。语义与 ADR-0005 连续,只是判定基底从
"有无 RenderRule"换成"覆盖声明是否含此 kind"(ADR-0011 废 RenderRule 载荷)。`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