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