feat(dag): populate per-node headlines field

CHANGELOG.md

@@ -42,6 +42,10 @@ All notable changes to arghda-core are documented here. The format follows
   `<PATH>/.arghda/config.toml` (or an explicit `--config <file>`). Precedence
   is built-in default < `config.toml` < CLI `--headline-pattern`. Missing file
   ⇒ defaults; unknown keys are rejected so typos surface.
+- DAG `headlines` field: each `dag` node now carries the sorted, deduped list
+  of top-level headline theorem names it declares (the spec's per-node
+  `headlines` array), extracted with the same logic as `unpinned-headline` and
+  honouring the configured headline pattern. Completes the v0 DAG schema.
 - RSR scaffolding: `.machine_readable/6a2/` artefacts, `0-AI-MANIFEST.a2ml`,
   `Justfile`, `.well-known/`, and community-health files.
 - Content-hash invalidation of `proven`: promotion records a SHA-256 of the

README.md

@@ -39,8 +39,9 @@ record.
 - Workspace state machine — transitions are file moves, each logged to
   `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`,
   `invalidate`)
-- `dag` — emits the dependency-DAG JSON (nodes + import edges + blocked
-  list) for a source tree: the contract a visual layer consumes
+- `dag` — emits the dependency-DAG JSON (nodes — each with its lint status
+  and declared `headlines` — plus import edges and a blocked list) for a
+  source tree: the contract a visual layer consumes
 - `check` — runs Agda on a file and combines the typecheck verdict with the
   lint report (degrades gracefully when `agda` is absent)
 - First-class import graph (the `graph` module, lifted out of the orphan rule)
@@ -66,11 +67,8 @@ built-in default < `config.toml` < CLI flag. Current schema:
 headline_pattern = "^[a-z][A-Za-z0-9-]*$"
 ```
 
-Not yet: the DAG `headlines` field (the extractor now exists for
-`unpinned-headline`, but the per-node `headlines` array in the DAG schema is
-still unpopulated); the Groove service manifest. (`missing-without-k` is
-subsumed by `missing-safe-pragma`, which already reports a missing
-`--without-K`.)
+Not yet: the Groove service manifest. (`missing-without-k` is subsumed by
+`missing-safe-pragma`, which already reports a missing `--without-K`.)
 
 ## Build
 

src/dag.rs

@@ -9,9 +9,10 @@
 
 use crate::diagnostic::Severity;
 use crate::graph::{self, Edge};
-use crate::lint::{run_lints, LintContext, LintRule};
+use crate::lint::{run_lints, unpinned_headline, LintContext, LintRule};
 use crate::timestamp::now_rfc3339;
-use anyhow::Result;
+use anyhow::{Context, Result};
+use regex::Regex;
 use serde::Serialize;
 use std::collections::{BTreeMap, BTreeSet};
 use std::path::{Path, PathBuf};
@@ -31,6 +32,9 @@ pub struct DagNode {
     /// `clean` | `warn` | `blocked` (lint-derived; not a proof claim).
     pub status: &'static str,
     pub lint: LintSummary,
+    /// Top-level theorem names this module declares that match the headline
+    /// pattern (sorted, deduped). The spec's per-node `headlines` array.
+    pub headlines: Vec<String>,
 }
 
 /// A module that cannot advance, and why.
@@ -54,13 +58,17 @@ pub struct DagDocument {
 }
 
 /// Build the DAG document for the source tree at `include_root`, using
-/// `entry_modules` (the union of CI roots) for the orphan-reachability rule
-/// and `rules` as the lint pack.
+/// `entry_modules` (the union of CI roots) for the orphan-reachability rule,
+/// `rules` as the lint pack, and `headline_pattern` (the same regex the
+/// `unpinned-headline` rule uses) to populate each node's `headlines` array.
 pub fn build(
     include_root: &Path,
     entry_modules: &[PathBuf],
     rules: &[Box<dyn LintRule>],
+    headline_pattern: &str,
 ) -> Result<DagDocument> {
+    let headline_matcher = Regex::new(headline_pattern)
+        .with_context(|| format!("compiling headline pattern `{headline_pattern}`"))?;
     let graph = graph::build(include_root)?;
     let ctx = LintContext {
         include_root,
@@ -95,11 +103,23 @@ pub fn build(
             "clean"
         };
 
+        // Headline theorem names this module declares (sorted, deduped),
+        // extracted with the same logic as the `unpinned-headline` rule.
+        let contents = std::fs::read_to_string(&abs).unwrap_or_default();
+        let mut headlines: Vec<String> =
+            unpinned_headline::headline_decls(&contents, &headline_matcher)
+                .into_iter()
+                .map(|(name, _line)| name)
+                .collect();
+        headlines.sort();
+        headlines.dedup();
+
         nodes.push(DagNode {
             id: gn.id.clone(),
             file: gn.file.clone(),
             status,
             lint: summary,
+            headlines,
         });
     }
 

src/lint/unpinned_headline.rs

@@ -211,7 +211,10 @@ fn collect_pinned(contents: &str, out: &mut BTreeSet<String>) {
 
 /// Top-level (column-0) type-signature names matching `matcher`, paired with
 /// the 1-based line they were declared on. `a b c : T` yields each name.
-fn headline_decls(contents: &str, matcher: &Regex) -> Vec<(String, usize)> {
+///
+/// Public so the `dag` builder can populate each node's `headlines` array
+/// (the spec's DAG schema) from the same extractor this rule uses.
+pub fn headline_decls(contents: &str, matcher: &Regex) -> Vec<(String, usize)> {
     let mut out = Vec::new();
     let mut in_block_comment = false;
 

src/main.rs

@@ -174,7 +174,8 @@ fn scan(
     unused: bool,
     json: bool,
 ) -> Result<()> {
-    let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?;
+    let (roots, rules, _cfg) =
+        resolve_roots_and_rules(include_root, entry, headline_pattern, config)?;
     let ctx = LintContext {
         include_root,
         entry_modules: &roots,
@@ -324,8 +325,9 @@ fn dag(
     headline_pattern: Option<&str>,
     config: Option<&Path>,
 ) -> Result<()> {
-    let (roots, rules) = resolve_roots_and_rules(include_root, entry, headline_pattern, config)?;
-    let doc = build_dag(include_root, &roots, &rules)?;
+    let (roots, rules, cfg) =
+        resolve_roots_and_rules(include_root, entry, headline_pattern, config)?;
+    let doc = build_dag(include_root, &roots, &rules, &cfg.headline_pattern)?;
     println!("{}", serde_json::to_string_pretty(&doc)?);
     Ok(())
 }
@@ -364,7 +366,7 @@ fn resolve_roots_and_rules(
     entry: &[PathBuf],
     headline_pattern: Option<&str>,
     config: Option<&Path>,
-) -> Result<(Vec<PathBuf>, RuleSet)> {
+) -> Result<(Vec<PathBuf>, RuleSet, RuleConfig)> {
     for e in entry {
         if !e.is_file() {
             anyhow::bail!("entry module not found: {}", e.display());
@@ -388,7 +390,7 @@ fn resolve_roots_and_rules(
     } else {
         rules_with_config(&cfg)?
     };
-    Ok((roots, rules))
+    Ok((roots, rules, cfg))
 }
 
 fn transition(workspace: &Path, file: &str, from: State, to: State) -> Result<()> {

tests/dag.rs

@@ -1,5 +1,6 @@
 //! `dag` document construction over the fixtures.
 
+use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN;
 use arghda_core::{build_dag, default_rules};
 use std::path::PathBuf;
 
@@ -15,7 +16,7 @@ fn fixture(name: &str) -> PathBuf {
 fn dag_over_orphan_fixture_has_expected_shape() {
     let root = fixture("orphan");
     let roots = [root.join("All.agda")];
-    let doc = build_dag(&root, &roots, &default_rules()).unwrap();
+    let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap();
 
     // Nodes are deterministic and sorted by module id.
     let ids: Vec<&str> = doc.nodes.iter().map(|n| n.id.as_str()).collect();
@@ -53,7 +54,7 @@ fn dag_over_orphan_fixture_has_expected_shape() {
 fn dag_over_wellformed_fixture_is_all_clean() {
     let root = fixture("wellformed");
     let roots = [root.join("All.agda")];
-    let doc = build_dag(&root, &roots, &default_rules()).unwrap();
+    let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap();
 
     assert_eq!(doc.version, "0.1");
     assert!(
@@ -65,3 +66,22 @@ fn dag_over_wellformed_fixture_is_all_clean() {
     assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Good"));
     assert!(doc.edges.iter().any(|e| e.from == "All" && e.to == "Util"));
 }
+
+#[test]
+fn dag_populates_node_headlines() {
+    let root = fixture("headlines");
+    let roots = [root.join("All.agda")];
+    let doc = build_dag(&root, &roots, &default_rules(), DEFAULT_HEADLINE_PATTERN).unwrap();
+
+    // `Thm` declares two top-level headline signatures (sorted, deduped); its
+    // indented `private` helper is not top-level and is not surfaced.
+    let thm = doc.nodes.iter().find(|n| n.id == "Thm").unwrap();
+    assert_eq!(
+        thm.headlines,
+        vec!["thm-one".to_string(), "thm-two".to_string()]
+    );
+
+    // The entry module has only imports, so no headlines.
+    let all = doc.nodes.iter().find(|n| n.id == "All").unwrap();
+    assert!(all.headlines.is_empty());
+}

tests/fixtures/headlines/All.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
+module All where
+
+open import Thm

tests/fixtures/headlines/Thm.agda

@@ -0,0 +1,15 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Thm where
+
+-- Two top-level headline signatures the DAG should surface, plus an
+-- indented (non-top-level) helper that must NOT be surfaced.
+thm-one : Set₁
+thm-one = Set
+
+thm-two : Set₁
+thm-two = Set
+
+private
+  helper : Set₁
+  helper = Set