elenchus_solver/report/
json.rs

1//! JSON serialization of a [`Report`] (stable, machine-readable output).
2use super::{Report, Status, TraceReason, TraceStep};
3use alloc::string::String;
4use elenchus_compiler::{Origin, PlaceholderStatus, Value};
5
6impl Report {
7    /// CLI-style exit code: 0 = consistent, 1 = underdetermined/warnings, 2 = conflicts.
8    pub fn exit_code(&self) -> i32 {
9        match self.status {
10            Status::Conflict => 2,
11            Status::Underdetermined | Status::Warning => 1,
12            Status::Consistent => 0,
13        }
14    }
15
16    /// Render the report as a single-line JSON object (for tooling / MCP).
17    /// Hand-written so the crate stays dependency-free and `no_std`.
18    pub fn to_json(&self) -> String {
19        use core::fmt::Write as _;
20        let mut s = String::new();
21        let _ = write!(s, "{{\"status\":");
22        status_name(self.status).write_json(&mut s);
23        let _ = write!(s, ",\"exit_code\":{}", self.exit_code());
24
25        s.push_str(",\"conflicts\":[");
26        for (i, c) in self.conflicts.iter().enumerate() {
27            if i > 0 {
28                s.push(',');
29            }
30            json_origin(&c.origin, &mut s);
31            s.push_str(",\"atoms\":");
32            c.atoms.write_json(&mut s);
33            s.push_str(",\"trace\":[");
34            for (j, step) in c.trace.iter().enumerate() {
35                if j > 0 {
36                    s.push(',');
37                }
38                step.write_json(&mut s);
39            }
40            s.push_str("]}");
41        }
42        s.push_str("],\"warnings\":[");
43        for (i, w) in self.warnings.iter().enumerate() {
44            if i > 0 {
45                s.push(',');
46            }
47            json_origin(&w.origin, &mut s);
48            s.push_str(",\"blocked_by\":");
49            w.blocked_by.write_json(&mut s);
50            s.push_str(",\"hint\":");
51            match &w.hint {
52                Some(h) => h.write_json(&mut s),
53                None => s.push_str("null"),
54            }
55            s.push('}');
56        }
57        s.push_str("],\"derived\":[");
58        for (i, d) in self.derived.iter().enumerate() {
59            if i > 0 {
60                s.push(',');
61            }
62            s.push('{');
63            json_origin_fields(&d.origin, &mut s);
64            s.push_str(",\"atom\":");
65            d.atom.write_json(&mut s);
66            let _ = write!(s, ",\"value\":{}", matches!(d.value, Value::True));
67            s.push('}');
68        }
69        s.push_str("],\"underdetermined\":");
70        match &self.underdetermined {
71            Some(atom) => atom.write_json(&mut s),
72            None => s.push_str("null"),
73        }
74        s.push_str(",\"unsat_core\":[");
75        for (i, it) in self.unsat_core.iter().enumerate() {
76            if i > 0 {
77                s.push(',');
78            }
79            json_origin(&it.origin, &mut s);
80            s.push_str(",\"label\":");
81            it.label.write_json(&mut s);
82            s.push('}');
83        }
84        s.push_str("],\"retract\":[");
85        for (i, it) in self.retract.iter().enumerate() {
86            if i > 0 {
87                s.push(',');
88            }
89            json_origin(&it.origin, &mut s);
90            s.push_str(",\"label\":");
91            it.label.write_json(&mut s);
92            s.push('}');
93        }
94        s.push_str("],\"hints\":[");
95        for (i, h) in self.hints.iter().enumerate() {
96            if i > 0 {
97                s.push(',');
98            }
99            s.push_str("{\"a\":");
100            h.a.write_json(&mut s);
101            s.push_str(",\"b\":");
102            h.b.write_json(&mut s);
103            s.push_str(",\"reason\":");
104            h.reason.write_json(&mut s);
105            s.push('}');
106        }
107        s.push_str("],\"orphans\":[");
108        for (i, o) in self.orphans.iter().enumerate() {
109            if i > 0 {
110                s.push(',');
111            }
112            json_origin(&o.origin, &mut s);
113            s.push_str(",\"atom\":");
114            o.atom.write_json(&mut s);
115            let _ = write!(s, ",\"value\":{}", matches!(o.value, Value::True));
116            s.push('}');
117        }
118        s.push_str("],\"unused_imports\":[");
119        for (i, u) in self.unused_imports.iter().enumerate() {
120            if i > 0 {
121                s.push(',');
122            }
123            s.push_str("{\"file\":");
124            u.file.write_json(&mut s);
125            s.push_str(",\"domain\":");
126            u.domain.write_json(&mut s);
127            s.push_str(",\"alias\":");
128            match &u.alias {
129                Some(a) => a.write_json(&mut s),
130                None => s.push_str("null"),
131            }
132            let _ = write!(s, ",\"line\":{}", u.line);
133            s.push('}');
134        }
135        s.push_str("],\"placeholders\":[");
136        for (i, p) in self.placeholders.iter().enumerate() {
137            if i > 0 {
138                s.push(',');
139            }
140            s.push_str("{\"key\":");
141            p.key.write_json(&mut s);
142            let status = match p.status {
143                PlaceholderStatus::Supplied => "supplied",
144                PlaceholderStatus::DefaultUsed => "default",
145                PlaceholderStatus::Unset => "unset",
146            };
147            s.push_str(",\"status\":");
148            status.write_json(&mut s);
149            match p.value {
150                Some(v) => {
151                    let _ = write!(s, ",\"value\":{v}");
152                }
153                None => s.push_str(",\"value\":null"),
154            }
155            s.push_str(",\"origin\":");
156            match &p.origin {
157                Some(o) => o.write_json(&mut s),
158                None => s.push_str("null"),
159            }
160            s.push('}');
161        }
162        s.push_str("]}");
163        s
164    }
165}
166
167/// Append a value's JSON encoding to `out`. Hand-rolled (no serde) so the crate
168/// stays dependency-free and `no_std` — one trait so every leaf (strings, string
169/// arrays, trace steps) shares the same `.write_json(out)` spelling.
170trait ToJson {
171    fn write_json(&self, out: &mut String);
172}
173
174/// A JSON string literal, with the mandatory escapes (`\uXXXX` for controls).
175impl ToJson for str {
176    fn write_json(&self, out: &mut String) {
177        use core::fmt::Write as _;
178        out.push('"');
179        for ch in self.chars() {
180            match ch {
181                '"' => out.push_str("\\\""),
182                '\\' => out.push_str("\\\\"),
183                '\n' => out.push_str("\\n"),
184                '\r' => out.push_str("\\r"),
185                '\t' => out.push_str("\\t"),
186                c if (c as u32) < 0x20 => {
187                    let _ = write!(out, "\\u{:04x}", c as u32);
188                }
189                c => out.push(c),
190            }
191        }
192        out.push('"');
193    }
194}
195
196/// A JSON array of strings.
197impl ToJson for [String] {
198    fn write_json(&self, out: &mut String) {
199        out.push('[');
200        for (i, item) in self.iter().enumerate() {
201            if i > 0 {
202                out.push(',');
203            }
204            item.write_json(out);
205        }
206        out.push(']');
207    }
208}
209
210/// One derivation-trace step as a JSON object.
211impl ToJson for TraceStep {
212    fn write_json(&self, out: &mut String) {
213        use core::fmt::Write as _;
214        out.push_str("{\"atom\":");
215        self.atom.write_json(out);
216        let _ = write!(out, ",\"value\":{}", matches!(self.value, Value::True));
217        match &self.reason {
218            TraceReason::Asserted(o) => {
219                out.push_str(",\"how\":\"asserted\",");
220                json_origin_fields(o, out);
221                out.push_str(",\"from\":[]");
222            }
223            TraceReason::Derived { origin, from } => {
224                out.push_str(",\"how\":\"derived\",");
225                json_origin_fields(origin, out);
226                out.push_str(",\"from\":");
227                from.write_json(out);
228            }
229        }
230        out.push('}');
231    }
232}
233
234pub(crate) fn status_name(s: Status) -> &'static str {
235    match s {
236        Status::Consistent => "CONSISTENT",
237        Status::Underdetermined => "UNDERDETERMINED",
238        Status::Warning => "WARNING",
239        Status::Conflict => "CONFLICT",
240    }
241}
242
243/// `"premise":..,"kind":..,"source":..,"line":..` (no braces).
244pub(crate) fn json_origin_fields(o: &Origin, out: &mut String) {
245    use core::fmt::Write as _;
246    out.push_str("\"premise\":");
247    match &o.premise {
248        Some(name) => name.write_json(out),
249        None => out.push_str("null"),
250    }
251    out.push_str(",\"kind\":");
252    o.kind.write_json(out);
253    out.push_str(",\"source\":");
254    o.source.write_json(out);
255    let _ = write!(out, ",\"line\":{}", o.line);
256}
257
258/// Open an object `{` and write the origin fields.
259pub(crate) fn json_origin(o: &Origin, out: &mut String) {
260    out.push('{');
261    json_origin_fields(o, out);
262}
elenchus_solver/report/json.rs

elenchus_solver/report/
json.rs
