1use flux_errors::E0999;
2use flux_macros::Diagnostic;
3use flux_middle::{fhir, rty};
4use rustc_span::{Span, Symbol, symbol::Ident};
5
6#[derive(Diagnostic)]
7#[diag(fhir_analysis_sort_mismatch, code = E0999)]
8pub(super) struct SortMismatch {
9 #[primary_span]
10 #[label]
11 span: Span,
12 expected: rty::Sort,
13 found: rty::Sort,
14}
15
16impl SortMismatch {
17 pub(super) fn new(span: Span, expected: rty::Sort, found: rty::Sort) -> Self {
18 Self { span, expected, found }
19 }
20}
21
22#[derive(Diagnostic)]
23#[diag(fhir_analysis_arg_count_mismatch, code = E0999)]
24pub(super) struct ArgCountMismatch {
25 #[primary_span]
26 #[label]
27 span: Option<Span>,
28 expected: usize,
29 found: usize,
30 thing: String,
31}
32
33impl ArgCountMismatch {
34 pub(super) fn new(span: Option<Span>, thing: String, expected: usize, found: usize) -> Self {
35 Self { span, expected, found, thing }
36 }
37}
38
39#[derive(Diagnostic)]
40#[diag(fhir_analysis_duplicated_ensures, code = E0999)]
41pub(super) struct DuplicatedEnsures {
42 #[primary_span]
43 span: Span,
44 loc: String,
45}
46
47impl DuplicatedEnsures {
48 pub(super) fn new(loc: &fhir::PathExpr) -> DuplicatedEnsures {
49 Self { span: loc.span, loc: format!("{loc:?}") }
50 }
51}
52
53#[derive(Diagnostic)]
54#[diag(fhir_analysis_missing_ensures, code = E0999)]
55pub(super) struct MissingEnsures {
56 #[primary_span]
57 span: Span,
58}
59
60impl MissingEnsures {
61 pub(super) fn new(loc: &fhir::PathExpr) -> MissingEnsures {
62 Self { span: loc.span }
63 }
64}
65
66#[derive(Diagnostic)]
67#[diag(fhir_analysis_unsupported_primop, code = E0999)]
68pub(super) struct UnsupportedPrimOp {
69 #[primary_span]
70 span: Span,
71 op: fhir::BinOp,
72}
73
74impl UnsupportedPrimOp {
75 pub(super) fn new(span: Span, op: fhir::BinOp) -> Self {
76 Self { span, op }
77 }
78}
79
80#[derive(Diagnostic)]
81#[diag(fhir_analysis_invalid_wildcard_sort, code = E0999)]
82#[note]
83pub(super) struct InvalidWildcardSort {
84 #[primary_span]
85 #[label]
86 span: Span,
87 found: rty::Sort,
88}
89
90impl InvalidWildcardSort {
91 pub(super) fn new(span: Span, found: rty::Sort) -> Self {
92 Self { span, found }
93 }
94}
95
96#[derive(Diagnostic)]
97#[diag(fhir_analysis_expected_fun, code = E0999)]
98pub(super) struct ExpectedFun<'a> {
99 #[primary_span]
100 span: Span,
101 found: &'a rty::Sort,
102}
103
104impl<'a> ExpectedFun<'a> {
105 pub(super) fn new(span: Span, found: &'a rty::Sort) -> Self {
106 Self { span, found }
107 }
108}
109
110#[derive(Diagnostic)]
111#[diag(fhir_analysis_invalid_param_in_func_pos, code = E0999)]
112pub(super) struct InvalidParamPos<'a> {
113 #[primary_span]
114 #[label]
115 span: Span,
116 sort: &'a rty::Sort,
117 is_pred: bool,
118}
119
120impl<'a> InvalidParamPos<'a> {
121 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
122 Self { span, sort, is_pred: sort.is_pred() }
123 }
124}
125
126#[derive(Diagnostic)]
127#[diag(fhir_analysis_unexpected_fun, code = E0999)]
128pub(super) struct UnexpectedFun<'a> {
129 #[primary_span]
130 #[label]
131 span: Span,
132 sort: &'a rty::Sort,
133}
134
135impl<'a> UnexpectedFun<'a> {
136 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
137 Self { span, sort }
138 }
139}
140
141#[derive(Diagnostic)]
142#[diag(fhir_analysis_unexpected_constructor, code = E0999)]
143pub(super) struct UnexpectedConstructor<'a> {
144 #[primary_span]
145 #[label]
146 span: Span,
147 sort: &'a rty::Sort,
148}
149
150impl<'a> UnexpectedConstructor<'a> {
151 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
152 Self { span, sort }
153 }
154}
155
156#[derive(Diagnostic)]
157#[diag(fhir_analysis_param_count_mismatch, code = E0999)]
158pub(super) struct ParamCountMismatch {
159 #[primary_span]
160 #[label]
161 span: Span,
162 expected: usize,
163 found: usize,
164}
165
166impl ParamCountMismatch {
167 pub(super) fn new(span: Span, expected: usize, found: usize) -> Self {
168 Self { span, expected, found }
169 }
170}
171
172#[derive(Diagnostic)]
173#[diag(fhir_analysis_field_not_found, code = E0999)]
174pub(super) struct FieldNotFound {
175 #[primary_span]
176 span: Span,
177 sort: rty::Sort,
178 fld: Ident,
179}
180
181impl FieldNotFound {
182 pub(super) fn new(sort: rty::Sort, fld: Ident) -> Self {
183 Self { span: fld.span, sort, fld }
184 }
185}
186
187#[derive(Diagnostic)]
188#[diag(fhir_analysis_constructor_missing_fields, code = E0999)]
189pub(super) struct ConstructorMissingFields {
190 #[primary_span]
191 constructor_span: Span,
192 missing_fields: String,
193}
194
195impl ConstructorMissingFields {
196 pub(super) fn new(constructor_span: Span, missing_fields: Vec<Symbol>) -> Self {
197 let missing_fields = missing_fields
198 .into_iter()
199 .map(|x| format!("`{x}`"))
200 .collect::<Vec<String>>()
201 .join(", ");
202 Self { constructor_span, missing_fields }
203 }
204}
205
206#[derive(Diagnostic)]
207#[diag(fhir_analysis_duplicate_field_used, code = E0999)]
208pub(super) struct DuplicateFieldUsed {
209 #[primary_span]
210 span: Span,
211 fld: Ident,
212 #[help]
213 previous_span: Span,
214}
215
216impl DuplicateFieldUsed {
217 pub(super) fn new(fld: Ident, previous_fld: Ident) -> Self {
218 Self { span: fld.span, fld, previous_span: previous_fld.span }
219 }
220}
221
222#[derive(Diagnostic)]
223#[diag(fhir_analysis_invalid_primitive_dot_access, code = E0999)]
224pub(super) struct InvalidPrimitiveDotAccess<'a> {
225 #[primary_span]
226 span: Span,
227 sort: &'a rty::Sort,
228}
229
230impl<'a> InvalidPrimitiveDotAccess<'a> {
231 pub(super) fn new(sort: &'a rty::Sort, fld: Ident) -> Self {
232 Self { sort, span: fld.span }
233 }
234}
235
236#[derive(Diagnostic)]
237#[diag(fhir_analysis_param_not_determined, code = E0999)]
238#[help]
239pub(super) struct ParamNotDetermined {
240 #[primary_span]
241 #[label]
242 span: Span,
243 name: Symbol,
244}
245
246impl ParamNotDetermined {
247 pub(super) fn new(span: Span, name: Symbol) -> Self {
248 Self { span, name }
249 }
250}
251
252#[derive(Diagnostic)]
253#[diag(fhir_analysis_sort_annotation_needed, code = E0999)]
254pub(super) struct SortAnnotationNeeded {
255 #[primary_span]
256 #[label]
257 span: Span,
258}
259
260impl SortAnnotationNeeded {
261 pub(super) fn new(param: &fhir::RefineParam) -> Self {
262 Self { span: param.span }
263 }
264}
265
266#[derive(Diagnostic)]
267#[diag(fhir_analysis_ill_sorted_quantifier, code = E0999)]
268#[note]
269pub(super) struct IllSortedQuantifier {
270 #[primary_span]
271 #[label]
272 span: Span,
273 sort: rty::Sort,
274}
275
276impl IllSortedQuantifier {
277 pub(super) fn new(span: Span, sort: rty::Sort) -> Self {
278 Self { span, sort }
279 }
280}
281
282#[derive(Diagnostic)]
283#[diag(fhir_analysis_cannot_infer_sort, code = E0999)]
284#[note]
285pub(super) struct CannotInferSort {
286 #[primary_span]
287 #[label]
288 span: Span,
289}
290
291impl CannotInferSort {
292 pub(super) fn new(span: Span) -> Self {
293 Self { span }
294 }
295}
296
297#[derive(Diagnostic)]
298#[diag(fhir_analysis_invalid_cast, code = E0999)]
299#[note]
300pub(super) struct InvalidCast {
301 #[primary_span]
302 #[label]
303 span: Span,
304 from: String,
305 to: String,
306}
307
308impl InvalidCast {
309 pub(super) fn new(span: Span, from: &rty::Sort, to: &rty::Sort) -> Self {
310 Self { span, from: format!("{from:?}"), to: format!("{to:?}") }
311 }
312}