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