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("mismatched sorts", code = E0999)]
8pub(super) struct SortMismatch {
9 #[primary_span]
10 #[label("expected `{$expected}`, found `{$found}`")]
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("this {$thing} takes {$expected ->
24 [one] {$expected} refinement argument
25 *[other] {$expected} refinement arguments
26 } but {$found ->
27 [one] {$found} was found
28 *[other] {$found} were found
29 }", code = E0999)]
30pub(super) struct ArgCountMismatch {
31 #[primary_span]
32 #[label(
33 "expected {$expected ->
34 [one] {$expected} argument
35 *[other] {$expected} arguments
36 }, found {$found}"
37 )]
38 span: Option<Span>,
39 expected: usize,
40 found: usize,
41 thing: String,
42}
43
44impl ArgCountMismatch {
45 pub(super) fn new(span: Option<Span>, thing: String, expected: usize, found: usize) -> Self {
46 Self { span, expected, found, thing }
47 }
48}
49
50#[derive(Diagnostic)]
51#[diag("an ensures clause already exists for `{$loc}`", code = E0999)]
52pub(super) struct DuplicatedEnsures {
53 #[primary_span]
54 span: Span,
55 loc: String,
56}
57
58impl DuplicatedEnsures {
59 pub(super) fn new(loc: &fhir::PathExpr) -> DuplicatedEnsures {
60 Self { span: loc.span, loc: format!("{loc:?}") }
61 }
62}
63
64#[derive(Diagnostic)]
65#[diag("missing ensures clause for `&strg` reference", code = E0999)]
66pub(super) struct MissingEnsures {
67 #[primary_span]
68 span: Span,
69}
70
71impl MissingEnsures {
72 pub(super) fn new(loc: &fhir::PathExpr) -> MissingEnsures {
73 Self { span: loc.span }
74 }
75}
76
77#[derive(Diagnostic)]
78#[diag("properties for `{$op}` are not yet supported", code = E0999)]
79pub(super) struct UnsupportedPrimOp {
80 #[primary_span]
81 span: Span,
82 op: fhir::BinOp,
83}
84
85impl UnsupportedPrimOp {
86 pub(super) fn new(span: Span, op: fhir::BinOp) -> Self {
87 Self { span, op }
88 }
89}
90
91#[derive(Diagnostic)]
92#[diag("wildcard parameter cannot have sort `{$found}`", code = E0999)]
93#[note(
94 "a wildcard parameter is instantiated with literal constants, so its sort must be one that has literals: `int`, `real`, `str`, or a bit vector"
95)]
96pub(super) struct InvalidWildcardSort {
97 #[primary_span]
98 #[label("this parameter is marked as a wildcard with `#`")]
99 span: Span,
100 found: rty::Sort,
101}
102
103impl InvalidWildcardSort {
104 pub(super) fn new(span: Span, found: rty::Sort) -> Self {
105 Self { span, found }
106 }
107}
108
109#[derive(Diagnostic)]
110#[diag("expected function, found `{$found}`", code = E0999)]
111pub(super) struct ExpectedFun<'a> {
112 #[primary_span]
113 span: Span,
114 found: &'a rty::Sort,
115}
116
117impl<'a> ExpectedFun<'a> {
118 pub(super) fn new(span: Span, found: &'a rty::Sort) -> Self {
119 Self { span, found }
120 }
121}
122
123#[derive(Diagnostic)]
124#[diag("illegal use of refinement parameter", code = E0999)]
125pub(super) struct InvalidParamPos<'a> {
126 #[primary_span]
127 #[label(
128 "{$is_pred ->
129 [true] abstract refinements are only allowed in a top-level conjunction
130 *[false] parameters of sort `{$sort}` are not supported in this position
131 }"
132 )]
133 span: Span,
134 sort: &'a rty::Sort,
135 is_pred: bool,
136}
137
138impl<'a> InvalidParamPos<'a> {
139 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
140 Self { span, sort, is_pred: sort.is_pred() }
141 }
142}
143
144#[derive(Diagnostic)]
145#[diag("mismatched sorts", code = E0999)]
146pub(super) struct UnexpectedFun<'a> {
147 #[primary_span]
148 #[label("expected `{$sort}`, found function")]
149 span: Span,
150 sort: &'a rty::Sort,
151}
152
153impl<'a> UnexpectedFun<'a> {
154 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
155 Self { span, sort }
156 }
157}
158
159#[derive(Diagnostic)]
160#[diag("mismatched sorts", code = E0999)]
161pub(super) struct UnexpectedConstructor<'a> {
162 #[primary_span]
163 #[label("expected `{$sort}`, found constructor")]
164 span: Span,
165 sort: &'a rty::Sort,
166}
167
168impl<'a> UnexpectedConstructor<'a> {
169 pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
170 Self { span, sort }
171 }
172}
173
174#[derive(Diagnostic)]
175#[diag("parameter count mismatch", code = E0999)]
176pub(super) struct ParamCountMismatch {
177 #[primary_span]
178 #[label(
179 "this function has {$found ->
180 [one] {$found} parameter
181 *[other] {$found} parameters
182 }, but a function with {$expected ->
183 [one] {$expected} parameter
184 *[other] {$expected} parameters
185 } was expected"
186 )]
187 span: Span,
188 expected: usize,
189 found: usize,
190}
191
192impl ParamCountMismatch {
193 pub(super) fn new(span: Span, expected: usize, found: usize) -> Self {
194 Self { span, expected, found }
195 }
196}
197
198#[derive(Diagnostic)]
199#[diag("no field `{$fld}` on sort `{$sort}`", code = E0999)]
200pub(super) struct FieldNotFound {
201 #[primary_span]
202 span: Span,
203 sort: rty::Sort,
204 fld: Ident,
205}
206
207impl FieldNotFound {
208 pub(super) fn new(sort: rty::Sort, fld: Ident) -> Self {
209 Self { span: fld.span, sort, fld }
210 }
211}
212
213#[derive(Diagnostic)]
214#[diag("missing fields in constructor: {$missing_fields}", code = E0999)]
215pub(super) struct ConstructorMissingFields {
216 #[primary_span]
217 constructor_span: Span,
218 missing_fields: String,
219}
220
221impl ConstructorMissingFields {
222 pub(super) fn new(constructor_span: Span, missing_fields: Vec<Symbol>) -> Self {
223 let missing_fields = missing_fields
224 .into_iter()
225 .map(|x| format!("`{x}`"))
226 .collect::<Vec<String>>()
227 .join(", ");
228 Self { constructor_span, missing_fields }
229 }
230}
231
232#[derive(Diagnostic)]
233#[diag("field `{$fld}` was previously used in constructor", code = E0999)]
234pub(super) struct DuplicateFieldUsed {
235 #[primary_span]
236 span: Span,
237 fld: Ident,
238 #[help("field `{$fld}` previously used here, consider removing it")]
239 previous_span: Span,
240}
241
242impl DuplicateFieldUsed {
243 pub(super) fn new(fld: Ident, previous_fld: Ident) -> Self {
244 Self { span: fld.span, fld, previous_span: previous_fld.span }
245 }
246}
247
248#[derive(Diagnostic)]
249#[diag("`{$sort}` is a primitive sort and therefore doesn't have fields", code = E0999)]
250pub(super) struct InvalidPrimitiveDotAccess<'a> {
251 #[primary_span]
252 span: Span,
253 sort: &'a rty::Sort,
254}
255
256impl<'a> InvalidPrimitiveDotAccess<'a> {
257 pub(super) fn new(sort: &'a rty::Sort, fld: Ident) -> Self {
258 Self { sort, span: fld.span }
259 }
260}
261
262#[derive(Diagnostic)]
263#[diag("parameter `{$name}` cannot be determined", code = E0999)]
264#[help("try indexing a type with `{$name}` in a position that fully determines its value")]
265pub(super) struct ParamNotDetermined {
266 #[primary_span]
267 #[label("undetermined parameter")]
268 span: Span,
269 name: Symbol,
270}
271
272impl ParamNotDetermined {
273 pub(super) fn new(span: Span, name: Symbol) -> Self {
274 Self { span, name }
275 }
276}
277
278#[derive(Diagnostic)]
279#[diag("sort annotation needed", code = E0999)]
280pub(super) struct SortAnnotationNeeded {
281 #[primary_span]
282 #[label("help: consider giving this parameter an explicit sort")]
283 span: Span,
284}
285
286impl SortAnnotationNeeded {
287 pub(super) fn new(param: &fhir::RefineParam) -> Self {
288 Self { span: param.span }
289 }
290}
291
292#[derive(Diagnostic)]
293#[diag("bounded quantification requires `int`-sorted binders", code = E0999)]
294#[note("binder inferred to have incompatible sort `{$sort}`")]
295pub(super) struct IllSortedQuantifier {
296 #[primary_span]
297 #[label("invalid sort")]
298 span: Span,
299 sort: rty::Sort,
300}
301
302impl IllSortedQuantifier {
303 pub(super) fn new(span: Span, sort: rty::Sort) -> Self {
304 Self { span, sort }
305 }
306}
307
308#[derive(Diagnostic)]
309#[diag("sort annotation needed", code = E0999)]
310#[note("sort must be known at this point")]
311pub(super) struct CannotInferSort {
312 #[primary_span]
313 #[label("cannot infer sort")]
314 span: Span,
315}
316
317impl CannotInferSort {
318 pub(super) fn new(span: Span) -> Self {
319 Self { span }
320 }
321}
322
323#[derive(Diagnostic)]
324#[diag("invalid cast from `{$from}` to `{$to}`", code = E0999)]
325#[note("use `allow_uninterpreted_cast` to enable this cast")]
326pub(super) struct InvalidCast {
327 #[primary_span]
328 #[label("invalid cast")]
329 span: Span,
330 from: String,
331 to: String,
332}
333
334impl InvalidCast {
335 pub(super) fn new(span: Span, from: &rty::Sort, to: &rty::Sort) -> Self {
336 Self { span, from: format!("{from:?}"), to: format!("{to:?}") }
337 }
338}