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

flux_fhir_analysis/wf/
errors.rs
