flux_fhir_analysis/wf/
errors.rs

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_expected_fun, code = E0999)]
82pub(super) struct ExpectedFun<'a> {
83    #[primary_span]
84    span: Span,
85    found: &'a rty::Sort,
86}
87
88impl<'a> ExpectedFun<'a> {
89    pub(super) fn new(span: Span, found: &'a rty::Sort) -> Self {
90        Self { span, found }
91    }
92}
93
94#[derive(Diagnostic)]
95#[diag(fhir_analysis_invalid_param_in_func_pos, code = E0999)]
96pub(super) struct InvalidParamPos<'a> {
97    #[primary_span]
98    #[label]
99    span: Span,
100    sort: &'a rty::Sort,
101    is_pred: bool,
102}
103
104impl<'a> InvalidParamPos<'a> {
105    pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
106        Self { span, sort, is_pred: sort.is_pred() }
107    }
108}
109
110#[derive(Diagnostic)]
111#[diag(fhir_analysis_unexpected_fun, code = E0999)]
112pub(super) struct UnexpectedFun<'a> {
113    #[primary_span]
114    #[label]
115    span: Span,
116    sort: &'a rty::Sort,
117}
118
119impl<'a> UnexpectedFun<'a> {
120    pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
121        Self { span, sort }
122    }
123}
124
125#[derive(Diagnostic)]
126#[diag(fhir_analysis_unexpected_constructor, code = E0999)]
127pub(super) struct UnexpectedConstructor<'a> {
128    #[primary_span]
129    #[label]
130    span: Span,
131    sort: &'a rty::Sort,
132}
133
134impl<'a> UnexpectedConstructor<'a> {
135    pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
136        Self { span, sort }
137    }
138}
139
140#[derive(Diagnostic)]
141#[diag(fhir_analysis_param_count_mismatch, code = E0999)]
142pub(super) struct ParamCountMismatch {
143    #[primary_span]
144    #[label]
145    span: Span,
146    expected: usize,
147    found: usize,
148}
149
150impl ParamCountMismatch {
151    pub(super) fn new(span: Span, expected: usize, found: usize) -> Self {
152        Self { span, expected, found }
153    }
154}
155
156#[derive(Diagnostic)]
157#[diag(fhir_analysis_field_not_found, code = E0999)]
158pub(super) struct FieldNotFound {
159    #[primary_span]
160    span: Span,
161    sort: rty::Sort,
162    fld: Ident,
163}
164
165impl FieldNotFound {
166    pub(super) fn new(sort: rty::Sort, fld: Ident) -> Self {
167        Self { span: fld.span, sort, fld }
168    }
169}
170
171#[derive(Diagnostic)]
172#[diag(fhir_analysis_constructor_missing_fields, code = E0999)]
173pub(super) struct ConstructorMissingFields {
174    #[primary_span]
175    constructor_span: Span,
176    missing_fields: String,
177}
178
179impl ConstructorMissingFields {
180    pub(super) fn new(constructor_span: Span, missing_fields: Vec<Symbol>) -> Self {
181        let missing_fields = missing_fields
182            .into_iter()
183            .map(|x| format!("`{x}`"))
184            .collect::<Vec<String>>()
185            .join(", ");
186        Self { constructor_span, missing_fields }
187    }
188}
189
190#[derive(Diagnostic)]
191#[diag(fhir_analysis_duplicate_field_used, code = E0999)]
192pub(super) struct DuplicateFieldUsed {
193    #[primary_span]
194    span: Span,
195    fld: Ident,
196    #[help]
197    previous_span: Span,
198}
199
200impl DuplicateFieldUsed {
201    pub(super) fn new(fld: Ident, previous_fld: Ident) -> Self {
202        Self { span: fld.span, fld, previous_span: previous_fld.span }
203    }
204}
205
206#[derive(Diagnostic)]
207#[diag(fhir_analysis_invalid_primitive_dot_access, code = E0999)]
208pub(super) struct InvalidPrimitiveDotAccess<'a> {
209    #[primary_span]
210    span: Span,
211    sort: &'a rty::Sort,
212}
213
214impl<'a> InvalidPrimitiveDotAccess<'a> {
215    pub(super) fn new(sort: &'a rty::Sort, fld: Ident) -> Self {
216        Self { sort, span: fld.span }
217    }
218}
219
220#[derive(Diagnostic)]
221#[diag(fhir_analysis_param_not_determined, code = E0999)]
222#[help]
223pub(super) struct ParamNotDetermined {
224    #[primary_span]
225    #[label]
226    span: Span,
227    name: Symbol,
228}
229
230impl ParamNotDetermined {
231    pub(super) fn new(span: Span, name: Symbol) -> Self {
232        Self { span, name }
233    }
234}
235
236#[derive(Diagnostic)]
237#[diag(fhir_analysis_sort_annotation_needed, code = E0999)]
238pub(super) struct SortAnnotationNeeded {
239    #[primary_span]
240    #[label]
241    span: Span,
242}
243
244impl SortAnnotationNeeded {
245    pub(super) fn new(param: &fhir::RefineParam) -> Self {
246        Self { span: param.span }
247    }
248}
249
250#[derive(Diagnostic)]
251#[diag(fhir_analysis_constant_annotation_needed, code = E0999)]
252pub(super) struct ConstantAnnotationNeeded {
253    #[primary_span]
254    #[label]
255    span: Span,
256}
257
258impl ConstantAnnotationNeeded {
259    pub(super) fn new(span: Span) -> Self {
260        Self { span }
261    }
262}
263
264#[derive(Diagnostic)]
265#[diag(fhir_analysis_cannot_infer_sort, code = E0999)]
266#[note]
267pub(super) struct CannotInferSort {
268    #[primary_span]
269    #[label]
270    span: Span,
271}
272
273impl CannotInferSort {
274    pub(super) fn new(span: Span) -> Self {
275        Self { span }
276    }
277}
flux_fhir_analysis/wf/errors.rs

flux_fhir_analysis/wf/
errors.rs
