oxilean_codegen/
doc_ir.rs

1//! Documentation Intermediate Representation (DocIR) for oxilean-codegen.
2//!
3//! This module defines [`DocIR`] — a flat, serialisable representation of the
4//! documented declarations in a compiled LCNF module — and [`emit_doc_ir`],
5//! which extracts it from an [`LcnfModule`].
6//!
7//! ## Limitations
8//!
9//! Doc comments are attached to declarations at the *parse* stage and are not
10//! propagated into the codegen IR.  Consequently, [`DocIRItem::doc_comment`]
11//! will always be an empty string when produced by [`emit_doc_ir`].  For
12//! richly-documented output, callers should prefer source-level extraction
13//! (see `oxilean-doc`'s `extractor` module) and use [`DocIR`] only as a
14//! lightweight index of compiled declarations.
15
16use crate::lcnf::types::{LcnfExternDecl, LcnfFunDecl, LcnfModule};
17
18// ---------------------------------------------------------------------------
19// Public types
20// ---------------------------------------------------------------------------
21
22/// Documentation IR — a flat list of documented declarations from one module.
23///
24/// Produced by [`emit_doc_ir`] and consumed by `oxilean-doc` to generate
25/// documentation without re-parsing the source file.
26#[derive(Debug, Clone, PartialEq)]
27pub struct DocIR {
28    /// The module name (typically the file path without extension).
29    pub module_name: String,
30    /// Documented declarations in declaration order.
31    pub items: Vec<DocIRItem>,
32}
33
34/// A single documented declaration extracted from an [`LcnfModule`].
35#[derive(Debug, Clone, PartialEq)]
36pub struct DocIRItem {
37    /// Fully-qualified declaration name.
38    pub name: String,
39    /// Declaration kind: `"def"`, `"axiom"`, or `"extern"`.
40    ///
41    /// `"def"` covers all top-level function declarations (including theorems
42    /// and instances whose proofs have been compiled).  `"axiom"` / `"extern"`
43    /// is used for declarations that have no compiled body (external stubs,
44    /// axioms, opaques).
45    pub kind: String,
46    /// Pretty-printed type signature.
47    ///
48    /// Currently always an empty string — type information is partially erased
49    /// by the LCNF lowering pass and cannot be reliably reconstructed here.
50    pub signature: String,
51    /// Doc comment text.
52    ///
53    /// Currently always empty; doc comments are not propagated into codegen.
54    /// Use `oxilean-doc`'s source-level extractor for accurate doc comments.
55    pub doc_comment: String,
56    /// Whether this declaration was annotated with `@[deprecated]`.
57    ///
58    /// Not preserved through the LCNF pipeline; always `false` here.
59    pub deprecated: bool,
60}
61
62// ---------------------------------------------------------------------------
63// Extraction
64// ---------------------------------------------------------------------------
65
66/// Extract documentation IR from a compiled [`LcnfModule`].
67///
68/// Walks the module's [`LcnfFunDecl`]s (kind `"def"`) and
69/// [`LcnfExternDecl`]s (kind `"axiom"`) in order, building one
70/// [`DocIRItem`] per declaration.
71///
72/// # Limitations
73///
74/// - `signature` and `doc_comment` are empty strings: type information is
75///   partially erased in LCNF, and doc comments are not plumbed through from
76///   the parse stage.
77/// - `deprecated` is always `false` for the same reason.
78///
79/// If you need signatures or doc comments, use `oxilean-doc`'s source-level
80/// `extract()` instead, and use this function only for cross-referencing
81/// compiled declaration *names*.
82pub fn emit_doc_ir(module_name: &str, module: &LcnfModule) -> DocIR {
83    let mut items: Vec<DocIRItem> =
84        Vec::with_capacity(module.fun_decls.len() + module.extern_decls.len());
85
86    for decl in &module.fun_decls {
87        items.push(doc_ir_item_from_fun(decl));
88    }
89    for decl in &module.extern_decls {
90        items.push(doc_ir_item_from_extern(decl));
91    }
92
93    DocIR {
94        module_name: module_name.to_string(),
95        items,
96    }
97}
98
99// ---------------------------------------------------------------------------
100// Private helpers
101// ---------------------------------------------------------------------------
102
103fn doc_ir_item_from_fun(decl: &LcnfFunDecl) -> DocIRItem {
104    DocIRItem {
105        name: decl.name.clone(),
106        kind: "def".to_string(),
107        signature: String::new(),
108        doc_comment: String::new(),
109        deprecated: false,
110    }
111}
112
113fn doc_ir_item_from_extern(decl: &LcnfExternDecl) -> DocIRItem {
114    DocIRItem {
115        name: decl.name.clone(),
116        kind: "axiom".to_string(),
117        signature: String::new(),
118        doc_comment: String::new(),
119        deprecated: false,
120    }
121}
122
123// ---------------------------------------------------------------------------
124// Serialisation helpers (JSON via manual formatting — no serde dependency)
125// ---------------------------------------------------------------------------
126
127impl DocIRItem {
128    /// Serialise this item to a JSON object string.
129    pub fn to_json(&self) -> String {
130        format!(
131            r#"{{"name":{},"kind":{},"signature":{},"doc_comment":{},"deprecated":{}}}"#,
132            json_string(&self.name),
133            json_string(&self.kind),
134            json_string(&self.signature),
135            json_string(&self.doc_comment),
136            self.deprecated,
137        )
138    }
139}
140
141impl DocIR {
142    /// Serialise the entire DocIR to a JSON object string.
143    pub fn to_json(&self) -> String {
144        let items_json: Vec<String> = self.items.iter().map(|i| i.to_json()).collect();
145        format!(
146            r#"{{"module_name":{},"items":[{}]}}"#,
147            json_string(&self.module_name),
148            items_json.join(","),
149        )
150    }
151
152    /// Deserialise a [`DocIR`] from a JSON string previously produced by
153    /// [`DocIR::to_json`].
154    ///
155    /// This is a minimal round-trip parser covering only the exact output
156    /// format emitted by `to_json`.  It is not a general JSON parser.
157    ///
158    /// Returns `None` if the input cannot be parsed.
159    pub fn from_json(s: &str) -> Option<DocIR> {
160        let s = s.trim();
161        // Expect: {"module_name":"...","items":[...]}
162        let module_name = extract_json_string_field(s, "module_name")?;
163        let items_raw = extract_json_array_field(s, "items")?;
164        let items = parse_json_items(&items_raw);
165        Some(DocIR { module_name, items })
166    }
167}
168
169/// Escape a string for JSON embedding.
170fn json_string(s: &str) -> String {
171    let mut out = String::with_capacity(s.len() + 2);
172    out.push('"');
173    for ch in s.chars() {
174        match ch {
175            '"' => out.push_str("\\\""),
176            '\\' => out.push_str("\\\\"),
177            '\n' => out.push_str("\\n"),
178            '\r' => out.push_str("\\r"),
179            '\t' => out.push_str("\\t"),
180            c => out.push(c),
181        }
182    }
183    out.push('"');
184    out
185}
186
187/// Extract the value of a JSON string field from a flat JSON object string.
188///
189/// Looks for `"key":"value"` patterns only; does not handle nested objects.
190fn extract_json_string_field(s: &str, key: &str) -> Option<String> {
191    let needle = format!("\"{}\":\"", key);
192    let start = s.find(&needle)? + needle.len();
193    let rest = &s[start..];
194    let mut value = String::new();
195    let mut chars = rest.chars();
196    while let Some(ch) = chars.next() {
197        match ch {
198            '"' => return Some(value),
199            '\\' => match chars.next()? {
200                '"' => value.push('"'),
201                '\\' => value.push('\\'),
202                'n' => value.push('\n'),
203                'r' => value.push('\r'),
204                't' => value.push('\t'),
205                other => {
206                    value.push('\\');
207                    value.push(other);
208                }
209            },
210            c => value.push(c),
211        }
212    }
213    None
214}
215
216/// Extract the raw JSON array value of a field from a flat JSON object string.
217fn extract_json_array_field(s: &str, key: &str) -> Option<String> {
218    let needle = format!("\"{}\":[", key);
219    let start = s.find(&needle)? + needle.len() - 1; // points at '['
220    let rest = &s[start..];
221    let mut depth = 0i32;
222    let mut end = 0;
223    for (i, ch) in rest.char_indices() {
224        match ch {
225            '[' => depth += 1,
226            ']' => {
227                depth -= 1;
228                if depth == 0 {
229                    end = i;
230                    break;
231                }
232            }
233            _ => {}
234        }
235    }
236    if end == 0 && depth != 0 {
237        return None;
238    }
239    Some(rest[1..end].to_string()) // strip outer '[' and ']'
240}
241
242/// Parse a comma-separated list of JSON item objects from the raw array body.
243fn parse_json_items(s: &str) -> Vec<DocIRItem> {
244    if s.trim().is_empty() {
245        return Vec::new();
246    }
247    // Split on `},{` boundaries
248    let mut items = Vec::new();
249    let mut depth = 0i32;
250    let mut current_start = 0;
251    for (i, ch) in s.char_indices() {
252        match ch {
253            '{' => depth += 1,
254            '}' => {
255                depth -= 1;
256                if depth == 0 {
257                    let obj = &s[current_start..=i];
258                    if let Some(item) = parse_json_item(obj) {
259                        items.push(item);
260                    }
261                    current_start = i + 1;
262                }
263            }
264            _ => {}
265        }
266    }
267    items
268}
269
270/// Parse a single `DocIRItem` from a JSON object string.
271fn parse_json_item(s: &str) -> Option<DocIRItem> {
272    let name = extract_json_string_field(s, "name")?;
273    let kind = extract_json_string_field(s, "kind")?;
274    let signature = extract_json_string_field(s, "signature").unwrap_or_default();
275    let doc_comment = extract_json_string_field(s, "doc_comment").unwrap_or_default();
276    let deprecated = s.contains("\"deprecated\":true");
277    Some(DocIRItem {
278        name,
279        kind,
280        signature,
281        doc_comment,
282        deprecated,
283    })
284}
285
286// ---------------------------------------------------------------------------
287// Tests
288// ---------------------------------------------------------------------------
289
290#[cfg(test)]
291mod tests {
292    use super::*;
293    use crate::lcnf::types::{LcnfExpr, LcnfModule, LcnfType};
294
295    fn make_fun_decl(name: &str) -> crate::lcnf::types::LcnfFunDecl {
296        crate::lcnf::types::LcnfFunDecl {
297            name: name.to_string(),
298            original_name: None,
299            params: vec![],
300            ret_type: LcnfType::Unit,
301            body: LcnfExpr::Unreachable,
302            is_recursive: false,
303            is_lifted: false,
304            inline_cost: 0,
305        }
306    }
307
308    fn make_extern_decl(name: &str) -> crate::lcnf::types::LcnfExternDecl {
309        crate::lcnf::types::LcnfExternDecl {
310            name: name.to_string(),
311            params: vec![],
312            ret_type: LcnfType::Unit,
313        }
314    }
315
316    /// DocIRItem can be constructed and Debug-printed.
317    #[test]
318    fn test_doc_ir_item_construct_and_debug() {
319        let item = DocIRItem {
320            name: "Nat.add".to_string(),
321            kind: "def".to_string(),
322            signature: "(n m : Nat) : Nat".to_string(),
323            doc_comment: "Add two natural numbers.".to_string(),
324            deprecated: false,
325        };
326        let debug_str = format!("{:?}", item);
327        assert!(debug_str.contains("Nat.add"));
328        assert!(debug_str.contains("def"));
329    }
330
331    /// DocIR can be serialised to a JSON string.
332    #[test]
333    fn test_doc_ir_to_json() {
334        let ir = DocIR {
335            module_name: "Nat".to_string(),
336            items: vec![DocIRItem {
337                name: "Nat.zero".to_string(),
338                kind: "def".to_string(),
339                signature: String::new(),
340                doc_comment: String::new(),
341                deprecated: false,
342            }],
343        };
344        let json = ir.to_json();
345        assert!(json.contains("\"module_name\":\"Nat\""));
346        assert!(json.contains("\"Nat.zero\""));
347        assert!(json.contains("\"kind\":\"def\""));
348    }
349
350    /// emit_doc_ir with an empty module returns DocIR with no items.
351    #[test]
352    fn test_emit_doc_ir_empty() {
353        let module = LcnfModule::default();
354        let ir = emit_doc_ir("Empty", &module);
355        assert_eq!(ir.module_name, "Empty");
356        assert!(ir.items.is_empty());
357    }
358
359    /// emit_doc_ir with N fun_decls returns N items with correct names.
360    #[test]
361    fn test_emit_doc_ir_fun_decls() {
362        let mut module = LcnfModule::default();
363        module.fun_decls.push(make_fun_decl("Foo.bar"));
364        module.fun_decls.push(make_fun_decl("Foo.baz"));
365        let ir = emit_doc_ir("Foo", &module);
366        assert_eq!(ir.items.len(), 2);
367        assert_eq!(ir.items[0].name, "Foo.bar");
368        assert_eq!(ir.items[0].kind, "def");
369        assert_eq!(ir.items[1].name, "Foo.baz");
370    }
371
372    /// DocIR round-trips through JSON: serialise then deserialise, check equality.
373    #[test]
374    fn test_doc_ir_json_roundtrip() {
375        let original = DocIR {
376            module_name: "MyModule".to_string(),
377            items: vec![
378                DocIRItem {
379                    name: "MyModule.foo".to_string(),
380                    kind: "def".to_string(),
381                    signature: String::new(),
382                    doc_comment: String::new(),
383                    deprecated: false,
384                },
385                DocIRItem {
386                    name: "MyModule.Axiom1".to_string(),
387                    kind: "axiom".to_string(),
388                    signature: String::new(),
389                    doc_comment: String::new(),
390                    deprecated: true,
391                },
392            ],
393        };
394        let json = original.to_json();
395        let recovered = DocIR::from_json(&json).expect("round-trip parse failed");
396        assert_eq!(recovered.module_name, original.module_name);
397        assert_eq!(recovered.items.len(), original.items.len());
398        assert_eq!(recovered.items[0].name, original.items[0].name);
399        assert_eq!(recovered.items[1].name, original.items[1].name);
400    }
401
402    /// The deprecated field is preserved in JSON round-trips.
403    #[test]
404    fn test_deprecated_field_preserved() {
405        let item = DocIRItem {
406            name: "OldApi.fn".to_string(),
407            kind: "def".to_string(),
408            signature: String::new(),
409            doc_comment: String::new(),
410            deprecated: true,
411        };
412        let ir = DocIR {
413            module_name: "OldApi".to_string(),
414            items: vec![item],
415        };
416        let json = ir.to_json();
417        let recovered = DocIR::from_json(&json).expect("parse failed");
418        assert!(recovered.items[0].deprecated);
419    }
420
421    /// emit_doc_ir with extern_decls returns items with kind "axiom".
422    #[test]
423    fn test_emit_doc_ir_extern_decls() {
424        let mut module = LcnfModule::default();
425        module.extern_decls.push(make_extern_decl("Nat.rec"));
426        let ir = emit_doc_ir("Nat", &module);
427        assert_eq!(ir.items.len(), 1);
428        assert_eq!(ir.items[0].kind, "axiom");
429        assert_eq!(ir.items[0].name, "Nat.rec");
430    }
431}
oxilean_codegen/doc_ir.rs

oxilean_codegen/
doc_ir.rs
