oxilean_codegen/ir_serialize/
functions.rs

1//! Functions for the LCNF IR serialization module.
2
3use std::collections::HashMap;
4
5use super::types::{
6    DeclKind, IrDeserializeResult, IrFormat, IrSerializeConfig, SerialDecl, SerializedIr,
7};
8
9// ── Current format version ────────────────────────────────────────────────────
10
11/// The version number embedded into every freshly serialized snapshot.
12pub const CURRENT_VERSION: u32 = 1;
13
14// ── Top-level serialize / deserialize ────────────────────────────────────────
15
16/// Serialize `module` to a string using the format specified in `cfg`.
17pub fn serialize_ir(module: &SerializedIr, cfg: &IrSerializeConfig) -> String {
18    match cfg.format {
19        IrFormat::Text => ir_to_text(module),
20        IrFormat::Json => ir_to_json(module),
21        IrFormat::Binary => ir_to_binary_text(module),
22    }
23}
24
25/// Deserialize the text `data` that was produced in `format`.
26///
27/// Only [`IrFormat::Text`] and [`IrFormat::Json`] are fully supported.
28/// [`IrFormat::Binary`] returns [`IrDeserializeResult::Unsupported`].
29pub fn deserialize_ir(data: &str, format: IrFormat) -> IrDeserializeResult {
30    match format {
31        IrFormat::Text => match ir_from_text(data) {
32            Ok(ir) => {
33                if ir.version != CURRENT_VERSION {
34                    IrDeserializeResult::VersionMismatch {
35                        expected: CURRENT_VERSION,
36                        found: ir.version,
37                    }
38                } else {
39                    IrDeserializeResult::Ok(ir)
40                }
41            }
42            Err(e) => IrDeserializeResult::ParseError(e),
43        },
44        IrFormat::Json => match ir_from_json(data) {
45            Ok(ir) => {
46                if ir.version != CURRENT_VERSION {
47                    IrDeserializeResult::VersionMismatch {
48                        expected: CURRENT_VERSION,
49                        found: ir.version,
50                    }
51                } else {
52                    IrDeserializeResult::Ok(ir)
53                }
54            }
55            Err(e) => IrDeserializeResult::ParseError(e),
56        },
57        IrFormat::Binary => {
58            IrDeserializeResult::Unsupported("binary format is write-only in this version".into())
59        }
60    }
61}
62
63/// Serialize a single declaration according to `cfg`.
64pub fn serialize_decl(decl: &SerialDecl, cfg: &IrSerializeConfig) -> String {
65    let mut out = String::new();
66    out.push_str(&format!("decl {} {}", decl.kind, decl.name));
67    if cfg.include_types {
68        out.push_str(&format!(" : {}", decl.type_));
69    }
70    if !decl.params.is_empty() {
71        out.push_str(&format!(" params=[{}]", decl.params.join(", ")));
72    }
73    if cfg.include_proofs {
74        if let Some(body) = &decl.body {
75            if cfg.pretty {
76                out.push_str(&format!("\n  body: {}", body));
77            } else {
78                out.push_str(&format!(" body={}", body));
79            }
80        }
81    }
82    out
83}
84
85// ── JSON format ───────────────────────────────────────────────────────────────
86
87/// Serialize `module` to a JSON string (always pretty-printed).
88pub fn ir_to_json(module: &SerializedIr) -> String {
89    let mut out = String::new();
90    out.push_str("{\n");
91    out.push_str(&format!("  \"version\": {},\n", module.version));
92    out.push_str(&format!(
93        "  \"module_name\": \"{}\",\n",
94        escape_json(&module.module_name)
95    ));
96    // metadata
97    out.push_str("  \"metadata\": {\n");
98    let meta_entries: Vec<String> = module
99        .metadata
100        .iter()
101        .map(|(k, v)| format!("    \"{}\": \"{}\"", escape_json(k), escape_json(v)))
102        .collect();
103    out.push_str(&meta_entries.join(",\n"));
104    if !meta_entries.is_empty() {
105        out.push('\n');
106    }
107    out.push_str("  },\n");
108    // declarations
109    out.push_str("  \"declarations\": [\n");
110    let decl_strs: Vec<String> = module
111        .declarations
112        .iter()
113        .map(|d| serialize_decl_json(d))
114        .collect();
115    out.push_str(&decl_strs.join(",\n"));
116    if !decl_strs.is_empty() {
117        out.push('\n');
118    }
119    out.push_str("  ]\n");
120    out.push('}');
121    out
122}
123
124fn serialize_decl_json(d: &SerialDecl) -> String {
125    let body_str = match &d.body {
126        Some(b) => format!("\"{}\"", escape_json(b)),
127        None => "null".to_string(),
128    };
129    let params_str: Vec<String> = d
130        .params
131        .iter()
132        .map(|p| format!("\"{}\"", escape_json(p)))
133        .collect();
134    format!(
135        "    {{\"name\": \"{}\", \"kind\": \"{}\", \"type\": \"{}\", \"body\": {}, \"params\": [{}]}}",
136        escape_json(&d.name),
137        d.kind,
138        escape_json(&d.type_),
139        body_str,
140        params_str.join(", ")
141    )
142}
143
144/// Deserialize a JSON-encoded IR snapshot produced by [`ir_to_json`].
145pub fn ir_from_json(s: &str) -> Result<SerializedIr, String> {
146    // Minimal hand-rolled JSON parser sufficient for our own output format.
147    let s = s.trim();
148    if !s.starts_with('{') {
149        return Err("expected JSON object".into());
150    }
151
152    let version = parse_json_u32(s, "version")
153        .ok_or_else(|| "missing or invalid 'version' field".to_string())?;
154    let module_name = parse_json_string(s, "module_name")
155        .ok_or_else(|| "missing 'module_name' field".to_string())?;
156    let metadata = parse_json_metadata(s);
157    let declarations = parse_json_declarations(s)?;
158
159    Ok(SerializedIr {
160        version,
161        module_name,
162        declarations,
163        metadata,
164    })
165}
166
167// ── Text format ───────────────────────────────────────────────────────────────
168
169/// Serialize `module` to a human-readable text format.
170pub fn ir_to_text(module: &SerializedIr) -> String {
171    let mut out = String::new();
172    out.push_str(&format!("-- OxiLean IR version {}\n", module.version));
173    out.push_str(&format!("module {}\n", module.module_name));
174    for (k, v) in &module.metadata {
175        out.push_str(&format!("-- meta {} = {}\n", k, v));
176    }
177    out.push('\n');
178    for decl in &module.declarations {
179        out.push_str(&format!("{} {} : {}", decl.kind, decl.name, decl.type_));
180        if !decl.params.is_empty() {
181            out.push_str(&format!("  -- params: {}", decl.params.join(", ")));
182        }
183        out.push('\n');
184        if let Some(body) = &decl.body {
185            out.push_str(&format!("  := {}\n", body));
186        }
187    }
188    out
189}
190
191/// Deserialize the text format produced by [`ir_to_text`].
192pub fn ir_from_text(s: &str) -> Result<SerializedIr, String> {
193    let mut version: Option<u32> = None;
194    let mut module_name: Option<String> = None;
195    let mut metadata: HashMap<String, String> = HashMap::new();
196    let mut declarations: Vec<SerialDecl> = Vec::new();
197
198    let mut pending_decl: Option<SerialDecl> = None;
199
200    for line in s.lines() {
201        let line = line.trim();
202        if line.is_empty() {
203            continue;
204        }
205        if let Some(rest) = line.strip_prefix("-- OxiLean IR version ") {
206            let v: u32 = rest
207                .trim()
208                .parse()
209                .map_err(|_| format!("invalid version '{}'", rest.trim()))?;
210            version = Some(v);
211        } else if let Some(rest) = line.strip_prefix("-- meta ") {
212            if let Some((k, v)) = rest.split_once(" = ") {
213                metadata.insert(k.trim().to_string(), v.trim().to_string());
214            }
215        } else if let Some(rest) = line.strip_prefix("module ") {
216            module_name = Some(rest.trim().to_string());
217        } else if let Some(rest) = line.strip_prefix(":= ") {
218            if let Some(ref mut d) = pending_decl {
219                // Strip trailing params comment if present
220                let body = if let Some((b, _)) = rest.split_once("  --") {
221                    b.trim().to_string()
222                } else {
223                    rest.trim().to_string()
224                };
225                d.body = Some(body);
226            }
227        } else if line.starts_with("--") {
228            // ignore other comments
229        } else {
230            // Try to parse a declaration line: `<kind> <name> : <type>  -- params: ...`
231            if let Some(d) = parse_text_decl_line(line) {
232                if let Some(prev) = pending_decl.take() {
233                    declarations.push(prev);
234                }
235                pending_decl = Some(d);
236            }
237        }
238    }
239    if let Some(d) = pending_decl {
240        declarations.push(d);
241    }
242
243    Ok(SerializedIr {
244        version: version.unwrap_or(CURRENT_VERSION),
245        module_name: module_name.unwrap_or_default(),
246        declarations,
247        metadata,
248    })
249}
250
251// ── Module operations ─────────────────────────────────────────────────────────
252
253/// Merge two modules into one.  Returns an error if any declaration name
254/// appears in both `a` and `b`.
255pub fn merge_modules(mut a: SerializedIr, b: SerializedIr) -> Result<SerializedIr, String> {
256    let a_names: std::collections::HashSet<&str> =
257        a.declarations.iter().map(|d| d.name.as_str()).collect();
258    for d in &b.declarations {
259        if a_names.contains(d.name.as_str()) {
260            return Err(format!(
261                "name collision: '{}' exists in both modules",
262                d.name
263            ));
264        }
265    }
266    a.declarations.extend(b.declarations);
267    for (k, v) in b.metadata {
268        a.metadata.entry(k).or_insert(v);
269    }
270    Ok(a)
271}
272
273/// Compute the diff between two module snapshots.
274///
275/// Returns `(added, removed, modified)` — each a `Vec<String>` of declaration
276/// names.  A declaration is "modified" when the name exists in both modules but
277/// the [`SerialDecl`] differs in any field.
278pub fn diff_modules(
279    old: &SerializedIr,
280    new: &SerializedIr,
281) -> (Vec<String>, Vec<String>, Vec<String>) {
282    let old_map: HashMap<&str, &SerialDecl> = old
283        .declarations
284        .iter()
285        .map(|d| (d.name.as_str(), d))
286        .collect();
287    let new_map: HashMap<&str, &SerialDecl> = new
288        .declarations
289        .iter()
290        .map(|d| (d.name.as_str(), d))
291        .collect();
292
293    let mut added: Vec<String> = Vec::new();
294    let mut removed: Vec<String> = Vec::new();
295    let mut modified: Vec<String> = Vec::new();
296
297    for (name, new_decl) in &new_map {
298        match old_map.get(name) {
299            None => added.push(name.to_string()),
300            Some(old_decl) => {
301                if old_decl != new_decl {
302                    modified.push(name.to_string());
303                }
304            }
305        }
306    }
307    for name in old_map.keys() {
308        if !new_map.contains_key(name) {
309            removed.push(name.to_string());
310        }
311    }
312
313    added.sort();
314    removed.sort();
315    modified.sort();
316    (added, removed, modified)
317}
318
319// ── Helpers ───────────────────────────────────────────────────────────────────
320
321/// Escape special JSON characters inside a string value.
322fn escape_json(s: &str) -> String {
323    let mut out = String::with_capacity(s.len());
324    for c in s.chars() {
325        match c {
326            '"' => out.push_str("\\\""),
327            '\\' => out.push_str("\\\\"),
328            '\n' => out.push_str("\\n"),
329            '\r' => out.push_str("\\r"),
330            '\t' => out.push_str("\\t"),
331            other => out.push(other),
332        }
333    }
334    out
335}
336
337/// Produce a simple binary-like text representation (base64-ish stub).
338/// Real binary encoding would use a proper byte stream; this placeholder
339/// keeps the format round-trip representable in a `String`.
340fn ir_to_binary_text(module: &SerializedIr) -> String {
341    // For the binary format we emit a compact single-line text that looks like
342    // length-prefixed data while remaining valid UTF-8.
343    let inner = ir_to_text(module);
344    let encoded: String = inner
345        .bytes()
346        .map(|b| format!("{:02x}", b))
347        .collect::<Vec<_>>()
348        .join("");
349    format!("OXI_BIN_V{}:{}", module.version, encoded)
350}
351
352/// Extract a `u32` field from a very simple JSON object string.
353fn parse_json_u32(json: &str, key: &str) -> Option<u32> {
354    let needle = format!("\"{}\":", key);
355    let start = json.find(&needle)? + needle.len();
356    let rest = json[start..].trim_start();
357    let end = rest
358        .find(|c: char| !c.is_ascii_digit())
359        .unwrap_or(rest.len());
360    rest[..end].parse().ok()
361}
362
363/// Extract a string field from a very simple JSON object string.
364fn parse_json_string(json: &str, key: &str) -> Option<String> {
365    let needle = format!("\"{}\":", key);
366    let start = json.find(&needle)? + needle.len();
367    let rest = json[start..].trim_start();
368    if !rest.starts_with('"') {
369        return None;
370    }
371    Some(unescape_json_string(&rest[1..])?.0)
372}
373
374/// Unescape a JSON string starting just after the opening `"`.
375/// Returns `(unescaped, chars_consumed_including_closing_quote)`.
376fn unescape_json_string(s: &str) -> Option<(String, usize)> {
377    let mut out = String::new();
378    let mut chars = s.char_indices();
379    loop {
380        let (i, c) = chars.next()?;
381        match c {
382            '"' => return Some((out, i + 1)),
383            '\\' => {
384                let (_, esc) = chars.next()?;
385                match esc {
386                    '"' => out.push('"'),
387                    '\\' => out.push('\\'),
388                    'n' => out.push('\n'),
389                    'r' => out.push('\r'),
390                    't' => out.push('\t'),
391                    other => {
392                        out.push('\\');
393                        out.push(other);
394                    }
395                }
396            }
397            other => out.push(other),
398        }
399    }
400}
401
402/// Parse the `"metadata"` object from a JSON string.
403fn parse_json_metadata(json: &str) -> HashMap<String, String> {
404    let mut map = HashMap::new();
405    let needle = "\"metadata\":";
406    let start = match json.find(needle) {
407        Some(p) => p + needle.len(),
408        None => return map,
409    };
410    let rest = json[start..].trim_start();
411    if !rest.starts_with('{') {
412        return map;
413    }
414    let inner = &rest[1..];
415    // iterate over key-value pairs
416    let mut pos = 0;
417    loop {
418        let chunk = inner[pos..].trim_start();
419        if chunk.starts_with('}') || chunk.is_empty() {
420            break;
421        }
422        if chunk.starts_with(',') {
423            pos += inner[pos..].find(',').map(|x| x + 1).unwrap_or(1);
424            continue;
425        }
426        if let Some(chunk_after_quote) = chunk.strip_prefix('"') {
427            // parse key
428            match unescape_json_string(chunk_after_quote) {
429                Some((key, k_consumed)) => {
430                    let after_key = chunk[1 + k_consumed..].trim_start();
431                    if !after_key.starts_with(':') {
432                        break;
433                    }
434                    let after_colon = after_key[1..].trim_start();
435                    if let Some(after_colon_stripped) = after_colon.strip_prefix('"') {
436                        match unescape_json_string(after_colon_stripped) {
437                            Some((val, _)) => {
438                                map.insert(key, val);
439                            }
440                            None => break,
441                        }
442                    }
443                    // advance pos past this pair
444                    match inner[pos..].find([',', '}']) {
445                        Some(adv) => pos += adv + 1,
446                        None => break,
447                    }
448                }
449                None => break,
450            }
451        } else {
452            pos += 1;
453        }
454    }
455    map
456}
457
458/// Parse the `"declarations"` array from a JSON string.
459fn parse_json_declarations(json: &str) -> Result<Vec<SerialDecl>, String> {
460    let mut decls = Vec::new();
461    let needle = "\"declarations\":";
462    let start = match json.find(needle) {
463        Some(p) => p + needle.len(),
464        None => return Ok(decls),
465    };
466    let rest = json[start..].trim_start();
467    if !rest.starts_with('[') {
468        return Ok(decls);
469    }
470    // Find each declaration object by looking for `{...}` blocks.
471    let mut depth = 0i32;
472    let mut obj_start: Option<usize> = None;
473    let chars: Vec<(usize, char)> = rest.char_indices().collect();
474    for &(i, c) in &chars {
475        match c {
476            '{' => {
477                depth += 1;
478                if depth == 1 {
479                    obj_start = Some(i);
480                }
481            }
482            '}' => {
483                depth -= 1;
484                if depth == 0 {
485                    if let Some(s) = obj_start.take() {
486                        let obj = &rest[s..=i];
487                        match parse_decl_json_obj(obj) {
488                            Ok(d) => decls.push(d),
489                            Err(e) => return Err(e),
490                        }
491                    }
492                }
493            }
494            ']' if depth == 0 => break,
495            _ => {}
496        }
497    }
498    Ok(decls)
499}
500
501fn parse_decl_json_obj(obj: &str) -> Result<SerialDecl, String> {
502    let name =
503        parse_json_string(obj, "name").ok_or_else(|| "declaration missing 'name'".to_string())?;
504    let kind_str =
505        parse_json_string(obj, "kind").ok_or_else(|| "declaration missing 'kind'".to_string())?;
506    let type_ = parse_json_string(obj, "type").unwrap_or_default();
507    let body = parse_json_nullable_string(obj, "body");
508    let params = parse_json_string_array(obj, "params");
509    let kind = parse_decl_kind(&kind_str)?;
510    Ok(SerialDecl {
511        name,
512        kind,
513        type_,
514        body,
515        params,
516    })
517}
518
519/// Parse a possibly-null JSON string field.
520fn parse_json_nullable_string(json: &str, key: &str) -> Option<String> {
521    let needle = format!("\"{}\":", key);
522    let start = json.find(&needle)? + needle.len();
523    let rest = json[start..].trim_start();
524    if rest.starts_with("null") {
525        return None;
526    }
527    if let Some(rest_stripped) = rest.strip_prefix('"') {
528        return unescape_json_string(rest_stripped).map(|(s, _)| s);
529    }
530    None
531}
532
533/// Parse a JSON array of strings for the given key.
534fn parse_json_string_array(json: &str, key: &str) -> Vec<String> {
535    let needle = format!("\"{}\":", key);
536    let start = match json.find(&needle) {
537        Some(p) => p + needle.len(),
538        None => return Vec::new(),
539    };
540    let rest = json[start..].trim_start();
541    if !rest.starts_with('[') {
542        return Vec::new();
543    }
544    let inner = &rest[1..];
545    let mut result = Vec::new();
546    let mut pos = 0;
547    loop {
548        let chunk = inner[pos..].trim_start();
549        if chunk.starts_with(']') || chunk.is_empty() {
550            break;
551        }
552        if chunk.starts_with(',') {
553            pos += 1;
554            continue;
555        }
556        if let Some(chunk_after_quote) = chunk.strip_prefix('"') {
557            match unescape_json_string(chunk_after_quote) {
558                Some((s, consumed)) => {
559                    result.push(s);
560                    // advance pos
561                    let skip = inner[pos..].trim_start().len();
562                    let leading = inner[pos..].len() - skip;
563                    pos += leading + 1 + consumed;
564                }
565                None => break,
566            }
567        } else {
568            pos += 1;
569        }
570    }
571    result
572}
573
574/// Parse a text-format declaration line.
575fn parse_text_decl_line(line: &str) -> Option<SerialDecl> {
576    // Possible forms:
577    //   `<kind> <name> : <type>  -- params: p1, p2`
578    //   `<kind> <name> : <type>`
579    let line = if let Some((main, _comment)) = line.split_once("  --") {
580        main.trim()
581    } else {
582        line
583    };
584
585    let (params_raw, rest) = if let Some((r, p)) = line.split_once("  -- params: ") {
586        (
587            p.split(',')
588                .map(|s| s.trim().to_string())
589                .collect::<Vec<_>>(),
590            r,
591        )
592    } else {
593        (Vec::new(), line)
594    };
595
596    // Split on first space to get kind token
597    let (kind_token, after_kind) = rest.split_once(' ')?;
598    let kind = parse_decl_kind(kind_token).ok()?;
599    // Split on " : " to get name and type
600    let (name, type_) = after_kind.split_once(" : ")?;
601    Some(SerialDecl {
602        name: name.trim().to_string(),
603        kind,
604        type_: type_.trim().to_string(),
605        body: None,
606        params: params_raw,
607    })
608}
609
610/// Convert a string into a [`DeclKind`].
611fn parse_decl_kind(s: &str) -> Result<DeclKind, String> {
612    match s {
613        "def" => Ok(DeclKind::Def),
614        "theorem" => Ok(DeclKind::Theorem),
615        "axiom" => Ok(DeclKind::Axiom),
616        "inductive" => Ok(DeclKind::Inductive),
617        "constructor" => Ok(DeclKind::Constructor),
618        "recursor" => Ok(DeclKind::Recursor),
619        other => Err(format!("unknown DeclKind '{}'", other)),
620    }
621}
622
623// ── Tests ─────────────────────────────────────────────────────────────────────
624
625#[cfg(test)]
626mod tests {
627    use super::super::types::{DeclKind, IrFormat, IrSerializeConfig, SerialDecl, SerializedIr};
628    use super::*;
629    use std::collections::HashMap;
630
631    fn sample_ir() -> SerializedIr {
632        let mut meta = HashMap::new();
633        meta.insert("compiler".to_string(), "oxilean-0.1.2".to_string());
634        SerializedIr {
635            version: CURRENT_VERSION,
636            module_name: "TestModule".to_string(),
637            declarations: vec![
638                SerialDecl {
639                    name: "myDef".to_string(),
640                    kind: DeclKind::Def,
641                    type_: "Nat".to_string(),
642                    body: Some("42".to_string()),
643                    params: vec![],
644                },
645                SerialDecl {
646                    name: "myTheorem".to_string(),
647                    kind: DeclKind::Theorem,
648                    type_: "a = a".to_string(),
649                    body: Some("rfl".to_string()),
650                    params: vec!["a".to_string()],
651                },
652            ],
653            metadata: meta,
654        }
655    }
656
657    // ── serialize_ir / deserialize_ir ─────────────────────────────────────────
658
659    #[test]
660    fn test_serialize_ir_text_roundtrip() {
661        let ir = sample_ir();
662        let cfg = IrSerializeConfig {
663            format: IrFormat::Text,
664            ..Default::default()
665        };
666        let text = serialize_ir(&ir, &cfg);
667        let result = deserialize_ir(&text, IrFormat::Text);
668        match result {
669            IrDeserializeResult::Ok(deserialized) => {
670                assert_eq!(deserialized.module_name, ir.module_name);
671                assert_eq!(deserialized.declarations.len(), ir.declarations.len());
672            }
673            other => panic!("expected Ok, got {:?}", other),
674        }
675    }
676
677    #[test]
678    fn test_serialize_ir_json_roundtrip() {
679        let ir = sample_ir();
680        let cfg = IrSerializeConfig {
681            format: IrFormat::Json,
682            ..Default::default()
683        };
684        let json = serialize_ir(&ir, &cfg);
685        let result = deserialize_ir(&json, IrFormat::Json);
686        match result {
687            IrDeserializeResult::Ok(deserialized) => {
688                assert_eq!(deserialized.module_name, ir.module_name);
689                assert_eq!(deserialized.version, CURRENT_VERSION);
690            }
691            other => panic!("expected Ok, got {:?}", other),
692        }
693    }
694
695    #[test]
696    fn test_deserialize_binary_returns_unsupported() {
697        let result = deserialize_ir("some data", IrFormat::Binary);
698        assert!(matches!(result, IrDeserializeResult::Unsupported(_)));
699    }
700
701    #[test]
702    fn test_deserialize_invalid_text_returns_parse_error() {
703        // Not a parse error in our lenient parser — it produces an empty module.
704        // A version string with garbage IS a parse error.
705        let result = deserialize_ir("-- OxiLean IR version abc\nmodule Foo", IrFormat::Text);
706        assert!(matches!(result, IrDeserializeResult::ParseError(_)));
707    }
708
709    // ── ir_to_json / ir_from_json ─────────────────────────────────────────────
710
711    #[test]
712    fn test_ir_to_json_contains_module_name() {
713        let ir = sample_ir();
714        let json = ir_to_json(&ir);
715        assert!(json.contains("TestModule"));
716    }
717
718    #[test]
719    fn test_ir_to_json_contains_version() {
720        let ir = sample_ir();
721        let json = ir_to_json(&ir);
722        assert!(json.contains(&CURRENT_VERSION.to_string()));
723    }
724
725    #[test]
726    fn test_ir_from_json_parses_version() {
727        let ir = sample_ir();
728        let json = ir_to_json(&ir);
729        let parsed = ir_from_json(&json).expect("parse failed");
730        assert_eq!(parsed.version, CURRENT_VERSION);
731    }
732
733    #[test]
734    fn test_ir_from_json_parses_declarations() {
735        let ir = sample_ir();
736        let json = ir_to_json(&ir);
737        let parsed = ir_from_json(&json).expect("parse failed");
738        assert_eq!(parsed.declarations.len(), 2);
739    }
740
741    #[test]
742    fn test_ir_from_json_decl_names() {
743        let ir = sample_ir();
744        let json = ir_to_json(&ir);
745        let parsed = ir_from_json(&json).expect("parse failed");
746        let names: Vec<_> = parsed
747            .declarations
748            .iter()
749            .map(|d| d.name.as_str())
750            .collect();
751        assert!(names.contains(&"myDef"));
752        assert!(names.contains(&"myTheorem"));
753    }
754
755    #[test]
756    fn test_ir_from_json_decl_kind() {
757        let ir = sample_ir();
758        let json = ir_to_json(&ir);
759        let parsed = ir_from_json(&json).expect("parse failed");
760        let def_decl = parsed
761            .declarations
762            .iter()
763            .find(|d| d.name == "myDef")
764            .expect("myDef not found");
765        assert_eq!(def_decl.kind, DeclKind::Def);
766    }
767
768    #[test]
769    fn test_ir_from_json_error_on_empty() {
770        assert!(ir_from_json("").is_err());
771    }
772
773    // ── ir_to_text / ir_from_text ─────────────────────────────────────────────
774
775    #[test]
776    fn test_ir_to_text_contains_module() {
777        let ir = sample_ir();
778        let text = ir_to_text(&ir);
779        assert!(text.contains("module TestModule"));
780    }
781
782    #[test]
783    fn test_ir_to_text_contains_def() {
784        let ir = sample_ir();
785        let text = ir_to_text(&ir);
786        assert!(text.contains("def myDef"));
787    }
788
789    #[test]
790    fn test_ir_from_text_roundtrip_module_name() {
791        let ir = sample_ir();
792        let text = ir_to_text(&ir);
793        let parsed = ir_from_text(&text).expect("parse failed");
794        assert_eq!(parsed.module_name, "TestModule");
795    }
796
797    #[test]
798    fn test_ir_from_text_roundtrip_decl_count() {
799        let ir = sample_ir();
800        let text = ir_to_text(&ir);
801        let parsed = ir_from_text(&text).expect("parse failed");
802        assert_eq!(parsed.declarations.len(), 2);
803    }
804
805    #[test]
806    fn test_ir_from_text_roundtrip_body() {
807        let ir = sample_ir();
808        let text = ir_to_text(&ir);
809        let parsed = ir_from_text(&text).expect("parse failed");
810        let d = parsed
811            .declarations
812            .iter()
813            .find(|d| d.name == "myDef")
814            .expect("myDef not found");
815        assert_eq!(d.body, Some("42".to_string()));
816    }
817
818    // ── serialize_decl ────────────────────────────────────────────────────────
819
820    #[test]
821    fn test_serialize_decl_with_type() {
822        let d = SerialDecl {
823            name: "foo".to_string(),
824            kind: DeclKind::Axiom,
825            type_: "Prop".to_string(),
826            body: None,
827            params: vec![],
828        };
829        let cfg = IrSerializeConfig::default();
830        let s = serialize_decl(&d, &cfg);
831        assert!(s.contains("axiom foo"));
832        assert!(s.contains("Prop"));
833    }
834
835    #[test]
836    fn test_serialize_decl_no_type() {
837        let d = SerialDecl {
838            name: "bar".to_string(),
839            kind: DeclKind::Def,
840            type_: "Int".to_string(),
841            body: Some("0".to_string()),
842            params: vec![],
843        };
844        let cfg = IrSerializeConfig {
845            include_types: false,
846            ..Default::default()
847        };
848        let s = serialize_decl(&d, &cfg);
849        assert!(!s.contains("Int"));
850    }
851
852    #[test]
853    fn test_serialize_decl_no_proof() {
854        let d = SerialDecl {
855            name: "thm".to_string(),
856            kind: DeclKind::Theorem,
857            type_: "True".to_string(),
858            body: Some("trivial".to_string()),
859            params: vec![],
860        };
861        let cfg = IrSerializeConfig {
862            include_proofs: false,
863            ..Default::default()
864        };
865        let s = serialize_decl(&d, &cfg);
866        assert!(!s.contains("trivial"));
867    }
868
869    // ── merge_modules ─────────────────────────────────────────────────────────
870
871    #[test]
872    fn test_merge_modules_success() {
873        let a = SerializedIr {
874            version: CURRENT_VERSION,
875            module_name: "A".to_string(),
876            declarations: vec![SerialDecl {
877                name: "x".to_string(),
878                kind: DeclKind::Def,
879                type_: "Nat".to_string(),
880                body: None,
881                params: vec![],
882            }],
883            metadata: HashMap::new(),
884        };
885        let b = SerializedIr {
886            version: CURRENT_VERSION,
887            module_name: "B".to_string(),
888            declarations: vec![SerialDecl {
889                name: "y".to_string(),
890                kind: DeclKind::Def,
891                type_: "Int".to_string(),
892                body: None,
893                params: vec![],
894            }],
895            metadata: HashMap::new(),
896        };
897        let merged = merge_modules(a, b).expect("merge failed");
898        assert_eq!(merged.declarations.len(), 2);
899    }
900
901    #[test]
902    fn test_merge_modules_collision() {
903        let decl = SerialDecl {
904            name: "collision".to_string(),
905            kind: DeclKind::Def,
906            type_: "Nat".to_string(),
907            body: None,
908            params: vec![],
909        };
910        let a = SerializedIr {
911            version: CURRENT_VERSION,
912            module_name: "A".to_string(),
913            declarations: vec![decl.clone()],
914            metadata: HashMap::new(),
915        };
916        let b = SerializedIr {
917            version: CURRENT_VERSION,
918            module_name: "B".to_string(),
919            declarations: vec![decl],
920            metadata: HashMap::new(),
921        };
922        assert!(merge_modules(a, b).is_err());
923    }
924
925    // ── diff_modules ──────────────────────────────────────────────────────────
926
927    #[test]
928    fn test_diff_added() {
929        let old = SerializedIr {
930            version: CURRENT_VERSION,
931            module_name: "M".to_string(),
932            declarations: vec![],
933            metadata: HashMap::new(),
934        };
935        let new = SerializedIr {
936            version: CURRENT_VERSION,
937            module_name: "M".to_string(),
938            declarations: vec![SerialDecl {
939                name: "newDecl".to_string(),
940                kind: DeclKind::Def,
941                type_: "Nat".to_string(),
942                body: None,
943                params: vec![],
944            }],
945            metadata: HashMap::new(),
946        };
947        let (added, removed, modified) = diff_modules(&old, &new);
948        assert_eq!(added, vec!["newDecl"]);
949        assert!(removed.is_empty());
950        assert!(modified.is_empty());
951    }
952
953    #[test]
954    fn test_diff_removed() {
955        let decl = SerialDecl {
956            name: "gone".to_string(),
957            kind: DeclKind::Axiom,
958            type_: "False".to_string(),
959            body: None,
960            params: vec![],
961        };
962        let old = SerializedIr {
963            version: CURRENT_VERSION,
964            module_name: "M".to_string(),
965            declarations: vec![decl],
966            metadata: HashMap::new(),
967        };
968        let new = SerializedIr {
969            version: CURRENT_VERSION,
970            module_name: "M".to_string(),
971            declarations: vec![],
972            metadata: HashMap::new(),
973        };
974        let (added, removed, modified) = diff_modules(&old, &new);
975        assert!(added.is_empty());
976        assert_eq!(removed, vec!["gone"]);
977        assert!(modified.is_empty());
978    }
979
980    #[test]
981    fn test_diff_modified() {
982        let d_old = SerialDecl {
983            name: "f".to_string(),
984            kind: DeclKind::Def,
985            type_: "Nat".to_string(),
986            body: Some("1".to_string()),
987            params: vec![],
988        };
989        let d_new = SerialDecl {
990            name: "f".to_string(),
991            kind: DeclKind::Def,
992            type_: "Nat".to_string(),
993            body: Some("2".to_string()),
994            params: vec![],
995        };
996        let old = SerializedIr {
997            version: CURRENT_VERSION,
998            module_name: "M".to_string(),
999            declarations: vec![d_old],
1000            metadata: HashMap::new(),
1001        };
1002        let new = SerializedIr {
1003            version: CURRENT_VERSION,
1004            module_name: "M".to_string(),
1005            declarations: vec![d_new],
1006            metadata: HashMap::new(),
1007        };
1008        let (added, removed, modified) = diff_modules(&old, &new);
1009        assert!(added.is_empty());
1010        assert!(removed.is_empty());
1011        assert_eq!(modified, vec!["f"]);
1012    }
1013
1014    #[test]
1015    fn test_diff_no_change() {
1016        let ir = sample_ir();
1017        let (added, removed, modified) = diff_modules(&ir, &ir);
1018        assert!(added.is_empty());
1019        assert!(removed.is_empty());
1020        assert!(modified.is_empty());
1021    }
1022
1023    // ── version mismatch ──────────────────────────────────────────────────────
1024
1025    #[test]
1026    fn test_version_mismatch_in_text() {
1027        let text = "-- OxiLean IR version 99\nmodule Foo\n";
1028        let result = deserialize_ir(text, IrFormat::Text);
1029        assert!(matches!(
1030            result,
1031            IrDeserializeResult::VersionMismatch {
1032                expected: _,
1033                found: 99
1034            }
1035        ));
1036    }
1037
1038    #[test]
1039    fn test_version_mismatch_in_json() {
1040        let json =
1041            "{\"version\": 99, \"module_name\": \"Foo\", \"metadata\": {}, \"declarations\": []}";
1042        let result = deserialize_ir(json, IrFormat::Json);
1043        assert!(matches!(
1044            result,
1045            IrDeserializeResult::VersionMismatch {
1046                expected: _,
1047                found: 99
1048            }
1049        ));
1050    }
1051}
oxilean_codegen/ir_serialize/functions.rs

oxilean_codegen/ir_serialize/
functions.rs
