1use super::*;
4use crate::ast::Protocol;
5use std::fmt::Write;
6
7#[derive(Debug, Clone, Copy, PartialEq, Eq)]
9pub enum LintLevel {
10 Off,
11 Warn,
12 Deny,
13}
14
15#[derive(Debug, Clone, PartialEq, Eq)]
17pub struct LintDiagnostic {
18 pub code: String,
19 pub level: LintLevel,
20 pub message: String,
21 pub suggestion: Option<String>,
22}
23
24fn push_lint(
25 diagnostics: &mut Vec<LintDiagnostic>,
26 level: LintLevel,
27 code: &str,
28 message: &str,
29 suggestion: impl Into<Option<String>>,
30) {
31 diagnostics.push(LintDiagnostic {
32 code: code.to_string(),
33 level,
34 message: message.to_string(),
35 suggestion: suggestion.into(),
36 });
37}
38
39pub fn collect_dsl_lints(choreography: &Choreography, level: LintLevel) -> Vec<LintDiagnostic> {
41 if level == LintLevel::Off {
42 return Vec::new();
43 }
44
45 let mut diagnostics = Vec::new();
46 let inferred = choreography.inferred_required_theorem_packs();
47 let required = choreography.required_theorem_packs();
48 if !inferred.is_empty() && inferred == required {
49 push_lint(
50 &mut diagnostics,
51 level,
52 "dsl.inferred_requires",
53 "Protocol requirements were inferred from ProtocolMachine-core capabilities",
54 Some(format!(
55 "Add explicit `requires {}` to the protocol header",
56 inferred.join(", ")
57 )),
58 );
59 }
60
61 diagnostics
62}
63
64fn diagnostics_to_lsp_json(diagnostics: Vec<LintDiagnostic>) -> String {
65 let diagnostics: Vec<serde_json::Value> = diagnostics
66 .into_iter()
67 .map(|lint| {
68 serde_json::json!({
69 "code": lint.code,
70 "severity": match lint.level {
71 LintLevel::Off => "off",
72 LintLevel::Warn => "warning",
73 LintLevel::Deny => "error",
74 },
75 "message": lint.message,
76 "range": {
77 "start": {"line": 0, "character": 0},
78 "end": {"line": 0, "character": 1}
79 },
80 "data": {
81 "quickFix": lint.suggestion
82 }
83 })
84 })
85 .collect();
86 serde_json::to_string_pretty(&diagnostics).unwrap_or_else(|_| "[]".to_string())
87}
88
89pub fn render_lsp_lint_diagnostics(choreography: &Choreography, level: LintLevel) -> String {
91 diagnostics_to_lsp_json(collect_dsl_lints(choreography, level))
92}
93
94#[allow(clippy::too_many_lines)]
95fn render_lowering_protocol(protocol: &Protocol, depth: usize, out: &mut String) {
97 let indent = " ".repeat(depth);
98 match protocol {
99 Protocol::Begin {
100 operation,
101 progress,
102 continuation,
103 ..
104 } => {
105 if let Some(progress) = progress {
106 writeln!(
107 out,
108 "{indent}- begin {operation} progress {}",
109 progress.contract_name
110 )
111 .unwrap();
112 } else {
113 writeln!(out, "{indent}- begin {operation}").unwrap();
114 }
115 render_lowering_protocol(continuation, depth + 1, out);
116 }
117 Protocol::Await {
118 operation,
119 continuation,
120 } => {
121 writeln!(out, "{indent}- await {operation}").unwrap();
122 render_lowering_protocol(continuation, depth + 1, out);
123 }
124 Protocol::Resolve {
125 operation,
126 outcome,
127 continuation,
128 } => {
129 writeln!(out, "{indent}- resolve {operation} as {outcome:?}").unwrap();
130 render_lowering_protocol(continuation, depth + 1, out);
131 }
132 Protocol::Invalidate {
133 operation,
134 continuation,
135 } => {
136 writeln!(out, "{indent}- invalidate {operation}").unwrap();
137 render_lowering_protocol(continuation, depth + 1, out);
138 }
139 Protocol::Send {
140 from,
141 to,
142 message,
143 continuation,
144 ..
145 } => {
146 writeln!(
147 out,
148 "{indent}- send {} -> {} : {}",
149 from.name(),
150 to.name(),
151 message.name
152 )
153 .unwrap();
154 render_lowering_protocol(continuation, depth + 1, out);
155 }
156 Protocol::Broadcast {
157 from,
158 message,
159 continuation,
160 ..
161 } => {
162 writeln!(
163 out,
164 "{indent}- broadcast {} ->* : {}",
165 from.name(),
166 message.name
167 )
168 .unwrap();
169 render_lowering_protocol(continuation, depth + 1, out);
170 }
171 Protocol::Choice { role, branches, .. } => {
172 writeln!(out, "{indent}- choice {} at", role.name()).unwrap();
173 for branch in branches {
174 writeln!(out, "{indent} branch {}", branch.label).unwrap();
175 render_lowering_protocol(&branch.protocol, depth + 2, out);
176 }
177 }
178 Protocol::Let {
179 name, continuation, ..
180 } => {
181 writeln!(out, "{indent}- let {name} = ...").unwrap();
182 render_lowering_protocol(continuation, depth + 1, out);
183 }
184 Protocol::Case { branches, .. } => {
185 writeln!(out, "{indent}- case/of").unwrap();
186 for branch in branches {
187 writeln!(out, "{indent} branch {}", branch.pattern.constructor).unwrap();
188 render_lowering_protocol(&branch.protocol, depth + 2, out);
189 }
190 }
191 Protocol::Timeout {
192 body,
193 on_timeout,
194 on_cancel,
195 ..
196 } => {
197 writeln!(out, "{indent}- timeout").unwrap();
198 render_lowering_protocol(body, depth + 1, out);
199 render_lowering_protocol(on_timeout, depth + 1, out);
200 if let Some(on_cancel) = on_cancel.as_deref() {
201 render_lowering_protocol(on_cancel, depth + 1, out);
202 }
203 }
204 Protocol::Loop { body, .. } => {
205 writeln!(out, "{indent}- loop").unwrap();
206 render_lowering_protocol(body, depth + 1, out);
207 }
208 Protocol::Parallel { protocols } => {
209 writeln!(out, "{indent}- parallel").unwrap();
210 for (idx, branch) in protocols.iter().enumerate() {
211 writeln!(out, "{indent} branch#{idx}").unwrap();
212 render_lowering_protocol(branch, depth + 2, out);
213 }
214 }
215 Protocol::Rec { label, body } => {
216 writeln!(out, "{indent}- rec {label}").unwrap();
217 render_lowering_protocol(body, depth + 1, out);
218 }
219 Protocol::Var(label) => {
220 writeln!(out, "{indent}- continue {label}").unwrap();
221 }
222 Protocol::Publish {
223 event,
224 arg,
225 continuation,
226 } => {
227 if let Some(arg) = arg {
228 writeln!(out, "{indent}- publish {event}{arg}").unwrap();
229 } else {
230 writeln!(out, "{indent}- publish {event}").unwrap();
231 }
232 render_lowering_protocol(continuation, depth + 1, out);
233 }
234 Protocol::PublishAuthority {
235 witness,
236 publication_name,
237 continuation,
238 } => {
239 writeln!(out, "{indent}- publish {witness} as {publication_name}").unwrap();
240 render_lowering_protocol(continuation, depth + 1, out);
241 }
242 Protocol::Materialize {
243 proof,
244 publication,
245 continuation,
246 } => {
247 writeln!(out, "{indent}- materialize {proof} from {publication}").unwrap();
248 render_lowering_protocol(continuation, depth + 1, out);
249 }
250 Protocol::Handoff {
251 operation,
252 target,
253 receipt,
254 continuation,
255 } => {
256 writeln!(
257 out,
258 "{indent}- handoff {operation} to {} using {receipt}",
259 target.name()
260 )
261 .unwrap();
262 render_lowering_protocol(continuation, depth + 1, out);
263 }
264 Protocol::DependentWork {
265 name,
266 arg,
267 required_for,
268 continuation,
269 } => {
270 if let Some(arg) = arg {
271 writeln!(
272 out,
273 "{indent}- dependent work {name}{arg} required for {required_for}"
274 )
275 .unwrap();
276 } else {
277 writeln!(
278 out,
279 "{indent}- dependent work {name} required for {required_for}"
280 )
281 .unwrap();
282 }
283 render_lowering_protocol(continuation, depth + 1, out);
284 }
285 Protocol::Extension {
286 annotations,
287 continuation,
288 ..
289 } => {
290 let kind = annotations
291 .custom("protocol_machine_core_op")
292 .or_else(|| annotations.custom("dsl_combinator"))
293 .unwrap_or("extension");
294 writeln!(out, "{indent}- extension {kind}").unwrap();
295 render_lowering_protocol(continuation, depth + 1, out);
296 }
297 Protocol::End => {
298 writeln!(out, "{indent}- end").unwrap();
299 }
300 }
301}
302
303fn render_lowering_summary(choreography: &Choreography, out: &mut String) {
304 writeln!(out, "Protocol: {}", choreography.qualified_name()).unwrap();
305 writeln!(
306 out,
307 "Roles: {}",
308 choreography
309 .roles
310 .iter()
311 .map(|r| r.name().to_string())
312 .collect::<Vec<_>>()
313 .join(", ")
314 )
315 .unwrap();
316 let bundles = choreography.theorem_packs();
317 if !bundles.is_empty() {
318 writeln!(
319 out,
320 "Proof bundles: {}",
321 bundles
322 .iter()
323 .map(|b| b.name.clone())
324 .collect::<Vec<_>>()
325 .join(", ")
326 )
327 .unwrap();
328 }
329 let required = choreography.required_theorem_packs();
330 if !required.is_empty() {
331 writeln!(out, "Required bundles: {}", required.join(", ")).unwrap();
332 }
333 let inferred = choreography.inferred_required_theorem_packs();
334 if !inferred.is_empty() {
335 writeln!(out, "Inferred bundles: {}", inferred.join(", ")).unwrap();
336 }
337}
338
339fn render_lowering_lints(lints: &[LintDiagnostic], out: &mut String) {
340 if lints.is_empty() {
341 return;
342 }
343 writeln!(out, "Lints:").unwrap();
344 for lint in lints {
345 writeln!(out, "- [{}] {}", lint.code, lint.message).unwrap();
346 if let Some(fix) = &lint.suggestion {
347 writeln!(out, " fix: {fix}").unwrap();
348 }
349 }
350}
351
352pub fn explain_lowering(input: &str) -> std::result::Result<String, ParseError> {
354 let choreography = parse_choreography_str(input)?;
355 let lints = collect_dsl_lints(&choreography, LintLevel::Warn);
356 let mut out = String::new();
357 render_lowering_summary(&choreography, &mut out);
358 writeln!(out, "Lowering:").unwrap();
359 render_lowering_protocol(&choreography.protocol, 1, &mut out);
360 render_lowering_lints(&lints, &mut out);
361 Ok(out)
362}